Average Error: 3.5 → 1.5
Time: 9.5s
Precision: 64
\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
↓
\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{t}{z}}{3 \cdot y}\]
\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}
↓
\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{t}{z}}{3 \cdot y}
double f(double x, double y, double z, double t) {
        double r476112 = x;
        double r476113 = y;
        double r476114 = z;
        double r476115 = 3.0;
        double r476116 = r476114 * r476115;
        double r476117 = r476113 / r476116;
        double r476118 = r476112 - r476117;
        double r476119 = t;
        double r476120 = r476116 * r476113;
        double r476121 = r476119 / r476120;
        double r476122 = r476118 + r476121;
        return r476122;
}
↓
double f(double x, double y, double z, double t) {
        double r476123 = x;
        double r476124 = y;
        double r476125 = z;
        double r476126 = 3.0;
        double r476127 = r476125 * r476126;
        double r476128 = r476124 / r476127;
        double r476129 = r476123 - r476128;
        double r476130 = t;
        double r476131 = r476130 / r476125;
        double r476132 = r476126 * r476124;
        double r476133 = r476131 / r476132;
        double r476134 = r476129 + r476133;
        return r476134;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original3.5
Target1.5
Herbie1.5
\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]

Derivation

  1. Split input into 2 regimes

  2. if (* z 3.0) < -2112989681.902512 or 7.66940248024694e+15 < (* z 3.0)

    1. Initial program 0.3

      \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
    2. Using strategy rm

    3. Applied div-inv0.3

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

    if -2112989681.902512 < (* z 3.0) < 7.66940248024694e+15

    1. Initial program 9.3

      \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
    2. Using strategy rm

    3. Applied *-un-lft-identity9.3

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

    4. Applied times-frac0.3

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

  4. Final simplification1.5

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

Reproduce

herbie shell --seed 2019297 
(FPCore (x y z t)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, H"
  :precision binary64

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

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