Average Error: 3.5 → 1.3
Time: 4.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 -3.40096777770621427 \cdot 10^{158}:\\ \;\;\;\;\left(x - \frac{y}{z} \cdot \frac{1}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\\ \mathbf{elif}\;z \le 5.541098349876343 \cdot 10^{-21}:\\ \;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{1}{z} \cdot \frac{\frac{t}{3}}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{t}{\left(z \cdot 3\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 -3.40096777770621427 \cdot 10^{158}:\\
\;\;\;\;\left(x - \frac{y}{z} \cdot \frac{1}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\\

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

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

\end{array}
double f(double x, double y, double z, double t) {
        double r691789 = x;
        double r691790 = y;
        double r691791 = z;
        double r691792 = 3.0;
        double r691793 = r691791 * r691792;
        double r691794 = r691790 / r691793;
        double r691795 = r691789 - r691794;
        double r691796 = t;
        double r691797 = r691793 * r691790;
        double r691798 = r691796 / r691797;
        double r691799 = r691795 + r691798;
        return r691799;
}
↓
double f(double x, double y, double z, double t) {
        double r691800 = z;
        double r691801 = -3.4009677777062143e+158;
        bool r691802 = r691800 <= r691801;
        double r691803 = x;
        double r691804 = y;
        double r691805 = r691804 / r691800;
        double r691806 = 1.0;
        double r691807 = 3.0;
        double r691808 = r691806 / r691807;
        double r691809 = r691805 * r691808;
        double r691810 = r691803 - r691809;
        double r691811 = t;
        double r691812 = r691800 * r691807;
        double r691813 = r691811 / r691812;
        double r691814 = r691813 / r691804;
        double r691815 = r691810 + r691814;
        double r691816 = 5.541098349876343e-21;
        bool r691817 = r691800 <= r691816;
        double r691818 = r691806 / r691800;
        double r691819 = r691804 / r691807;
        double r691820 = r691818 * r691819;
        double r691821 = r691803 - r691820;
        double r691822 = r691811 / r691807;
        double r691823 = r691822 / r691804;
        double r691824 = r691818 * r691823;
        double r691825 = r691821 + r691824;
        double r691826 = r691805 / r691807;
        double r691827 = r691803 - r691826;
        double r691828 = r691812 * r691804;
        double r691829 = r691811 / r691828;
        double r691830 = r691827 + r691829;
        double r691831 = r691817 ? r691825 : r691830;
        double r691832 = r691802 ? r691815 : r691831;
        return r691832;
}

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.7
Herbie1.3
\[\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 < -3.4009677777062143e+158

    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.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-identity1.4

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

    6. Applied times-frac1.4

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

    8. Applied div-inv1.5

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

    9. Applied associate-*r*1.5

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

    10. Simplified1.5

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

    if -3.4009677777062143e+158 < z < 5.541098349876343e-21

    1. Initial program 6.9

      \[\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.3

      \[\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.3

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

    6. Applied times-frac2.4

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

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

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

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

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

    10. Applied times-frac2.4

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

    11. Applied times-frac2.0

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

    12. Simplified2.0

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

    if 5.541098349876343e-21 < z

    1. Initial program 0.4

      \[\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.3

      \[\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 simplification1.3

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

Reproduce

herbie shell --seed 2020081 
(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))))