Average Error: 3.9 → 0.9
Time: 13.5s
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 \cdot 3 \le -1.679549677934962912371060912947000332007 \cdot 10^{-9}:\\ \;\;\;\;\left(x - 0.3333333333333333148296162562473909929395 \cdot \frac{y}{z}\right) + \frac{\frac{t}{3}}{z \cdot y}\\ \mathbf{elif}\;z \cdot 3 \le 1.988546582597582853711732660366369539647 \cdot 10^{129}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z \cdot 3} \cdot \frac{t}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + 0.3333333333333333148296162562473909929395 \cdot \frac{\frac{t}{z}}{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 \cdot 3 \le -1.679549677934962912371060912947000332007 \cdot 10^{-9}:\\
\;\;\;\;\left(x - 0.3333333333333333148296162562473909929395 \cdot \frac{y}{z}\right) + \frac{\frac{t}{3}}{z \cdot y}\\

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

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

\end{array}
double f(double x, double y, double z, double t) {
        double r474617 = x;
        double r474618 = y;
        double r474619 = z;
        double r474620 = 3.0;
        double r474621 = r474619 * r474620;
        double r474622 = r474618 / r474621;
        double r474623 = r474617 - r474622;
        double r474624 = t;
        double r474625 = r474621 * r474618;
        double r474626 = r474624 / r474625;
        double r474627 = r474623 + r474626;
        return r474627;
}
↓
double f(double x, double y, double z, double t) {
        double r474628 = z;
        double r474629 = 3.0;
        double r474630 = r474628 * r474629;
        double r474631 = -1.679549677934963e-09;
        bool r474632 = r474630 <= r474631;
        double r474633 = x;
        double r474634 = 0.3333333333333333;
        double r474635 = y;
        double r474636 = r474635 / r474628;
        double r474637 = r474634 * r474636;
        double r474638 = r474633 - r474637;
        double r474639 = t;
        double r474640 = r474639 / r474629;
        double r474641 = r474628 * r474635;
        double r474642 = r474640 / r474641;
        double r474643 = r474638 + r474642;
        double r474644 = 1.988546582597583e+129;
        bool r474645 = r474630 <= r474644;
        double r474646 = r474635 / r474630;
        double r474647 = r474633 - r474646;
        double r474648 = 1.0;
        double r474649 = r474648 / r474630;
        double r474650 = r474639 / r474635;
        double r474651 = r474649 * r474650;
        double r474652 = r474647 + r474651;
        double r474653 = r474639 / r474628;
        double r474654 = r474653 / r474635;
        double r474655 = r474634 * r474654;
        double r474656 = r474647 + r474655;
        double r474657 = r474645 ? r474652 : r474656;
        double r474658 = r474632 ? r474643 : r474657;
        return r474658;
}

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.9
Target1.7
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 3.0) < -1.679549677934963e-09

    1. Initial program 0.5

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

    2. Taylor expanded around 0 0.5

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

    4. Applied associate-/r*0.5

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

    5. Taylor expanded around 0 0.5

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

    if -1.679549677934963e-09 < (* z 3.0) < 1.988546582597583e+129

    1. Initial program 7.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-identity7.9

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

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

    if 1.988546582597583e+129 < (* z 3.0)

    1. Initial program 0.4

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

    2. Taylor expanded around 0 0.5

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

    4. Applied associate-/r*1.5

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

  4. Final simplification0.9

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

Reproduce

herbie shell --seed 2019325 +o rules:numerics
(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))))