Diagrams.Trail:splitAtParam from diagrams-lib-1.3.0.3, A

Average Error: 7.6 → 3.4

Time: 4.9s

Precision: 64

Math

\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\]

↓

\[\begin{array}{l} \mathbf{if}\;z \le -4.58103787244507047 \cdot 10^{135} \lor \neg \left(z \le 1.453781022003014 \cdot 10^{102}\right):\\ \;\;\;\;\frac{x + \frac{y}{t}}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{x + \left(y \cdot z - x\right) \cdot \frac{1}{t \cdot z - x}}{x + 1}\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r620859 = x;
        double r620860 = y;
        double r620861 = z;
        double r620862 = r620860 * r620861;
        double r620863 = r620862 - r620859;
        double r620864 = t;
        double r620865 = r620864 * r620861;
        double r620866 = r620865 - r620859;
        double r620867 = r620863 / r620866;
        double r620868 = r620859 + r620867;
        double r620869 = 1.0;
        double r620870 = r620859 + r620869;
        double r620871 = r620868 / r620870;
        return r620871;
}

↓

double f(double x, double y, double z, double t) {
        double r620872 = z;
        double r620873 = -4.5810378724450705e+135;
        bool r620874 = r620872 <= r620873;
        double r620875 = 1.453781022003014e+102;
        bool r620876 = r620872 <= r620875;
        double r620877 = !r620876;
        bool r620878 = r620874 || r620877;
        double r620879 = x;
        double r620880 = y;
        double r620881 = t;
        double r620882 = r620880 / r620881;
        double r620883 = r620879 + r620882;
        double r620884 = 1.0;
        double r620885 = r620879 + r620884;
        double r620886 = r620883 / r620885;
        double r620887 = r620880 * r620872;
        double r620888 = r620887 - r620879;
        double r620889 = 1.0;
        double r620890 = r620881 * r620872;
        double r620891 = r620890 - r620879;
        double r620892 = r620889 / r620891;
        double r620893 = r620888 * r620892;
        double r620894 = r620879 + r620893;
        double r620895 = r620894 / r620885;
        double r620896 = r620878 ? r620886 : r620895;
        return r620896;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	7.6
Target	0.3
Herbie	3.4

\[\frac{x + \left(\frac{y}{t - \frac{x}{z}} - \frac{x}{t \cdot z - x}\right)}{x + 1}\]

Derivation

1. Split input into 2 regimes

2. if z < -4.5810378724450705e+135 or 1.453781022003014e+102 < z

   1. Initial program 20.8

      \[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\]

   2. Taylor expanded around inf 7.0

      \[\leadsto \frac{x + \color{blue}{\frac{y}{t}}}{x + 1}\]

   if -4.5810378724450705e+135 < z < 1.453781022003014e+102

   1. Initial program 1.9

      \[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\]
   2. Using strategy rm

   3. Applied div-inv 1.9

      \[\leadsto \frac{x + \color{blue}{\left(y \cdot z - x\right) \cdot \frac{1}{t \cdot z - x}}}{x + 1}\]
3. Recombined 2 regimes into one program.

4. Final simplification 3.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -4.58103787244507047 \cdot 10^{135} \lor \neg \left(z \le 1.453781022003014 \cdot 10^{102}\right):\\ \;\;\;\;\frac{x + \frac{y}{t}}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{x + \left(y \cdot z - x\right) \cdot \frac{1}{t \cdot z - x}}{x + 1}\\ \end{array}\]

Reproduce

herbie shell --seed 2020064 
(FPCore (x y z t)
  :name "Diagrams.Trail:splitAtParam  from diagrams-lib-1.3.0.3, A"
  :precision binary64

  :herbie-target
  (/ (+ x (- (/ y (- t (/ x z))) (/ x (- (* t z) x)))) (+ x 1))

  (/ (+ x (/ (- (* y z) x) (- (* t z) x))) (+ x 1)))