Average Error: 3.6 → 0.9
Time: 24.0s
Precision: 64
\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
↓
\[\begin{array}{l} \mathbf{if}\;z \le -1.876078776862118321950943559866525589816 \cdot 10^{147}:\\ \;\;\;\;\frac{\frac{\frac{t}{z}}{3}}{y} + \left(x - \frac{y}{3 \cdot z}\right)\\ \mathbf{elif}\;z \le 101100649468898151561565306880:\\ \;\;\;\;\frac{\frac{1}{z}}{\frac{y}{\frac{t}{3}}} + \left(x - \frac{y}{3 \cdot z}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{t}{\left(3 \cdot z\right) \cdot y}\\ \end{array}\]
\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}
↓
\begin{array}{l}
\mathbf{if}\;z \le -1.876078776862118321950943559866525589816 \cdot 10^{147}:\\
\;\;\;\;\frac{\frac{\frac{t}{z}}{3}}{y} + \left(x - \frac{y}{3 \cdot z}\right)\\

\mathbf{elif}\;z \le 101100649468898151561565306880:\\
\;\;\;\;\frac{\frac{1}{z}}{\frac{y}{\frac{t}{3}}} + \left(x - \frac{y}{3 \cdot z}\right)\\

\mathbf{else}:\\
\;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{t}{\left(3 \cdot z\right) \cdot y}\\

\end{array}
double f(double x, double y, double z, double t) {
        double r32872602 = x;
        double r32872603 = y;
        double r32872604 = z;
        double r32872605 = 3.0;
        double r32872606 = r32872604 * r32872605;
        double r32872607 = r32872603 / r32872606;
        double r32872608 = r32872602 - r32872607;
        double r32872609 = t;
        double r32872610 = r32872606 * r32872603;
        double r32872611 = r32872609 / r32872610;
        double r32872612 = r32872608 + r32872611;
        return r32872612;
}
↓
double f(double x, double y, double z, double t) {
        double r32872613 = z;
        double r32872614 = -1.8760787768621183e+147;
        bool r32872615 = r32872613 <= r32872614;
        double r32872616 = t;
        double r32872617 = r32872616 / r32872613;
        double r32872618 = 3.0;
        double r32872619 = r32872617 / r32872618;
        double r32872620 = y;
        double r32872621 = r32872619 / r32872620;
        double r32872622 = x;
        double r32872623 = r32872618 * r32872613;
        double r32872624 = r32872620 / r32872623;
        double r32872625 = r32872622 - r32872624;
        double r32872626 = r32872621 + r32872625;
        double r32872627 = 1.0110064946889815e+29;
        bool r32872628 = r32872613 <= r32872627;
        double r32872629 = 1.0;
        double r32872630 = r32872629 / r32872613;
        double r32872631 = r32872616 / r32872618;
        double r32872632 = r32872620 / r32872631;
        double r32872633 = r32872630 / r32872632;
        double r32872634 = r32872633 + r32872625;
        double r32872635 = r32872620 / r32872613;
        double r32872636 = r32872635 / r32872618;
        double r32872637 = r32872622 - r32872636;
        double r32872638 = r32872623 * r32872620;
        double r32872639 = r32872616 / r32872638;
        double r32872640 = r32872637 + r32872639;
        double r32872641 = r32872628 ? r32872634 : r32872640;
        double r32872642 = r32872615 ? r32872626 : r32872641;
        return r32872642;
}

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.6
Target1.8
Herbie0.9
\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]

Derivation

  1. Split input into 3 regimes

  2. if z < -1.8760787768621183e+147

    1. Initial program 0.5

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

    3. Applied associate-/r*1.1

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

    5. Applied *-un-lft-identity1.1

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

    6. Applied associate-/r*1.1

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

    7. Simplified1.0

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

    if -1.8760787768621183e+147 < z < 1.0110064946889815e+29

    1. Initial program 6.5

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

    3. Applied associate-/r*2.4

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

    5. Applied *-un-lft-identity2.4

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

    6. Applied times-frac2.4

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

    7. Applied associate-/l*1.1

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

    if 1.0110064946889815e+29 < z

    1. Initial program 0.5

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

    3. Applied associate-/r*0.5

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

  4. Final simplification0.9

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.876078776862118321950943559866525589816 \cdot 10^{147}:\\ \;\;\;\;\frac{\frac{\frac{t}{z}}{3}}{y} + \left(x - \frac{y}{3 \cdot z}\right)\\ \mathbf{elif}\;z \le 101100649468898151561565306880:\\ \;\;\;\;\frac{\frac{1}{z}}{\frac{y}{\frac{t}{3}}} + \left(x - \frac{y}{3 \cdot z}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{t}{\left(3 \cdot z\right) \cdot y}\\ \end{array}\]

Reproduce

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

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

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