Average Error: 3.4 → 1.7
Time: 4.2s
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 -6.40431597217532072 \cdot 10^{-100}:\\ \;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{t}{z \cdot 3}}{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 -6.40431597217532072 \cdot 10^{-100}:\\
\;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\

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

\end{array}
double f(double x, double y, double z, double t) {
        double r789094 = x;
        double r789095 = y;
        double r789096 = z;
        double r789097 = 3.0;
        double r789098 = r789096 * r789097;
        double r789099 = r789095 / r789098;
        double r789100 = r789094 - r789099;
        double r789101 = t;
        double r789102 = r789098 * r789095;
        double r789103 = r789101 / r789102;
        double r789104 = r789100 + r789103;
        return r789104;
}
↓
double f(double x, double y, double z, double t) {
        double r789105 = z;
        double r789106 = -6.404315972175321e-100;
        bool r789107 = r789105 <= r789106;
        double r789108 = x;
        double r789109 = 1.0;
        double r789110 = r789109 / r789105;
        double r789111 = y;
        double r789112 = 3.0;
        double r789113 = r789111 / r789112;
        double r789114 = r789110 * r789113;
        double r789115 = r789108 - r789114;
        double r789116 = t;
        double r789117 = r789105 * r789112;
        double r789118 = r789117 * r789111;
        double r789119 = r789116 / r789118;
        double r789120 = r789115 + r789119;
        double r789121 = r789111 / r789105;
        double r789122 = r789121 / r789112;
        double r789123 = r789108 - r789122;
        double r789124 = r789116 / r789117;
        double r789125 = r789124 / r789111;
        double r789126 = r789123 + r789125;
        double r789127 = r789107 ? r789120 : r789126;
        return r789127;
}

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.4
Target1.8
Herbie1.7
\[\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 < -6.404315972175321e-100

    1. Initial program 0.9

      \[\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-identity0.9

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

    4. Applied times-frac1.0

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

    if -6.404315972175321e-100 < z

    1. Initial program 5.3

      \[\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.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 associate-/r*2.2

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

  4. Final simplification1.7

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

Reproduce

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