Average Error: 3.8 → 1.0
Time: 3.9s
Precision: 64
\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
↓
\[\begin{array}{l} \mathbf{if}\;t \le -6.1053505195899897 \cdot 10^{65} \lor \neg \left(t \le 2.6408832632668682 \cdot 10^{135}\right):\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z \cdot 3} \cdot \frac{t}{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}\;t \le -6.1053505195899897 \cdot 10^{65} \lor \neg \left(t \le 2.6408832632668682 \cdot 10^{135}\right):\\
\;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\

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

\end{array}
double f(double x, double y, double z, double t) {
        double r645101 = x;
        double r645102 = y;
        double r645103 = z;
        double r645104 = 3.0;
        double r645105 = r645103 * r645104;
        double r645106 = r645102 / r645105;
        double r645107 = r645101 - r645106;
        double r645108 = t;
        double r645109 = r645105 * r645102;
        double r645110 = r645108 / r645109;
        double r645111 = r645107 + r645110;
        return r645111;
}
↓
double f(double x, double y, double z, double t) {
        double r645112 = t;
        double r645113 = -6.10535051958999e+65;
        bool r645114 = r645112 <= r645113;
        double r645115 = 2.6408832632668682e+135;
        bool r645116 = r645112 <= r645115;
        double r645117 = !r645116;
        bool r645118 = r645114 || r645117;
        double r645119 = x;
        double r645120 = y;
        double r645121 = z;
        double r645122 = r645120 / r645121;
        double r645123 = 3.0;
        double r645124 = r645122 / r645123;
        double r645125 = r645119 - r645124;
        double r645126 = r645121 * r645123;
        double r645127 = r645126 * r645120;
        double r645128 = r645112 / r645127;
        double r645129 = r645125 + r645128;
        double r645130 = r645120 / r645126;
        double r645131 = r645119 - r645130;
        double r645132 = 1.0;
        double r645133 = r645132 / r645126;
        double r645134 = r645112 / r645120;
        double r645135 = r645133 * r645134;
        double r645136 = r645131 + r645135;
        double r645137 = r645118 ? r645129 : r645136;
        return r645137;
}

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

Derivation

  1. Split input into 2 regimes

  2. if t < -6.10535051958999e+65 or 2.6408832632668682e+135 < t

    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 associate-/r*0.9

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

    if -6.10535051958999e+65 < t < 2.6408832632668682e+135

    1. Initial program 4.8

      \[\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-identity4.8

      \[\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-frac1.0

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

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

Reproduce

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