Average Error: 3.5 → 0.6
Time: 16.4s
Precision: 64
\[\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}\]
\[\begin{array}{l} \mathbf{if}\;z \cdot 3.0 \le -2.785931663043419 \cdot 10^{-13}:\\ \;\;\;\;0.3333333333333333 \cdot \frac{t}{z \cdot y} + \left(x - \frac{y}{z \cdot 3.0}\right)\\ \mathbf{elif}\;z \cdot 3.0 \le 4.76391805126407 \cdot 10^{-15}:\\ \;\;\;\;\frac{1}{z \cdot 3.0} \cdot \frac{t}{y} + \left(x - \frac{y}{z \cdot 3.0}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{\frac{t}{z}}{y \cdot 3.0}\\ \end{array}\]
\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}
\begin{array}{l}
\mathbf{if}\;z \cdot 3.0 \le -2.785931663043419 \cdot 10^{-13}:\\
\;\;\;\;0.3333333333333333 \cdot \frac{t}{z \cdot y} + \left(x - \frac{y}{z \cdot 3.0}\right)\\

\mathbf{elif}\;z \cdot 3.0 \le 4.76391805126407 \cdot 10^{-15}:\\
\;\;\;\;\frac{1}{z \cdot 3.0} \cdot \frac{t}{y} + \left(x - \frac{y}{z \cdot 3.0}\right)\\

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

\end{array}
double f(double x, double y, double z, double t) {
        double r35835637 = x;
        double r35835638 = y;
        double r35835639 = z;
        double r35835640 = 3.0;
        double r35835641 = r35835639 * r35835640;
        double r35835642 = r35835638 / r35835641;
        double r35835643 = r35835637 - r35835642;
        double r35835644 = t;
        double r35835645 = r35835641 * r35835638;
        double r35835646 = r35835644 / r35835645;
        double r35835647 = r35835643 + r35835646;
        return r35835647;
}

double f(double x, double y, double z, double t) {
        double r35835648 = z;
        double r35835649 = 3.0;
        double r35835650 = r35835648 * r35835649;
        double r35835651 = -2.785931663043419e-13;
        bool r35835652 = r35835650 <= r35835651;
        double r35835653 = 0.3333333333333333;
        double r35835654 = t;
        double r35835655 = y;
        double r35835656 = r35835648 * r35835655;
        double r35835657 = r35835654 / r35835656;
        double r35835658 = r35835653 * r35835657;
        double r35835659 = x;
        double r35835660 = r35835655 / r35835650;
        double r35835661 = r35835659 - r35835660;
        double r35835662 = r35835658 + r35835661;
        double r35835663 = 4.76391805126407e-15;
        bool r35835664 = r35835650 <= r35835663;
        double r35835665 = 1.0;
        double r35835666 = r35835665 / r35835650;
        double r35835667 = r35835654 / r35835655;
        double r35835668 = r35835666 * r35835667;
        double r35835669 = r35835668 + r35835661;
        double r35835670 = r35835654 / r35835648;
        double r35835671 = r35835655 * r35835649;
        double r35835672 = r35835670 / r35835671;
        double r35835673 = r35835661 + r35835672;
        double r35835674 = r35835664 ? r35835669 : r35835673;
        double r35835675 = r35835652 ? r35835662 : r35835674;
        return r35835675;
}

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

Derivation

  1. Split input into 3 regimes
  2. if (* z 3.0) < -2.785931663043419e-13

    1. Initial program 0.3

      \[\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}\]
    2. Taylor expanded around 0 0.3

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

    if -2.785931663043419e-13 < (* z 3.0) < 4.76391805126407e-15

    1. Initial program 10.6

      \[\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}\]
    2. Using strategy rm
    3. Applied *-un-lft-identity10.6

      \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \frac{\color{blue}{1 \cdot t}}{\left(z \cdot 3.0\right) \cdot y}\]
    4. Applied times-frac0.3

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

    if 4.76391805126407e-15 < (* z 3.0)

    1. Initial program 0.3

      \[\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}\]
    2. Using strategy rm
    3. Applied associate-/r*1.1

      \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \color{blue}{\frac{\frac{t}{z \cdot 3.0}}{y}}\]
    4. Using strategy rm
    5. Applied *-un-lft-identity1.1

      \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \frac{\frac{t}{z \cdot 3.0}}{\color{blue}{1 \cdot y}}\]
    6. Applied associate-/r*1.1

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

      \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \frac{\color{blue}{\frac{\frac{t}{z}}{3.0}}}{y}\]
    8. Using strategy rm
    9. Applied div-inv1.1

      \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \frac{\color{blue}{\frac{t}{z} \cdot \frac{1}{3.0}}}{y}\]
    10. Applied associate-/l*1.1

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

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

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot 3.0 \le -2.785931663043419 \cdot 10^{-13}:\\ \;\;\;\;0.3333333333333333 \cdot \frac{t}{z \cdot y} + \left(x - \frac{y}{z \cdot 3.0}\right)\\ \mathbf{elif}\;z \cdot 3.0 \le 4.76391805126407 \cdot 10^{-15}:\\ \;\;\;\;\frac{1}{z \cdot 3.0} \cdot \frac{t}{y} + \left(x - \frac{y}{z \cdot 3.0}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{\frac{t}{z}}{y \cdot 3.0}\\ \end{array}\]

Reproduce

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