Average Error: 3.6 → 0.7
Time: 10.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}\;z \cdot 3 \le -73562257687642543292240068825919258624:\\ \;\;\;\;\left(x - \frac{1}{\frac{z \cdot 3}{y}}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\ \mathbf{elif}\;z \cdot 3 \le 2.357897429842402930998768322142604435202 \cdot 10^{78}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{t}{y}}{z \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{\frac{1}{z} \cdot \frac{t}{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 \cdot 3 \le -73562257687642543292240068825919258624:\\
\;\;\;\;\left(x - \frac{1}{\frac{z \cdot 3}{y}}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\

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

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

\end{array}
double f(double x, double y, double z, double t) {
        double r470413 = x;
        double r470414 = y;
        double r470415 = z;
        double r470416 = 3.0;
        double r470417 = r470415 * r470416;
        double r470418 = r470414 / r470417;
        double r470419 = r470413 - r470418;
        double r470420 = t;
        double r470421 = r470417 * r470414;
        double r470422 = r470420 / r470421;
        double r470423 = r470419 + r470422;
        return r470423;
}
↓
double f(double x, double y, double z, double t) {
        double r470424 = z;
        double r470425 = 3.0;
        double r470426 = r470424 * r470425;
        double r470427 = -7.356225768764254e+37;
        bool r470428 = r470426 <= r470427;
        double r470429 = x;
        double r470430 = 1.0;
        double r470431 = y;
        double r470432 = r470426 / r470431;
        double r470433 = r470430 / r470432;
        double r470434 = r470429 - r470433;
        double r470435 = t;
        double r470436 = r470426 * r470431;
        double r470437 = r470435 / r470436;
        double r470438 = r470434 + r470437;
        double r470439 = 2.357897429842403e+78;
        bool r470440 = r470426 <= r470439;
        double r470441 = r470431 / r470426;
        double r470442 = r470429 - r470441;
        double r470443 = r470435 / r470431;
        double r470444 = r470443 / r470426;
        double r470445 = r470442 + r470444;
        double r470446 = r470430 / r470424;
        double r470447 = r470431 / r470425;
        double r470448 = r470446 * r470447;
        double r470449 = r470429 - r470448;
        double r470450 = r470435 / r470425;
        double r470451 = r470446 * r470450;
        double r470452 = r470451 / r470431;
        double r470453 = r470449 + r470452;
        double r470454 = r470440 ? r470445 : r470453;
        double r470455 = r470428 ? r470438 : r470454;
        return r470455;
}

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.6
Target1.9
Herbie0.7
\[\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) < -7.356225768764254e+37

    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 clear-num0.4

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

    if -7.356225768764254e+37 < (* z 3.0) < 2.357897429842403e+78

    1. Initial program 7.8

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

    3. Applied add-cube-cbrt8.0

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

    4. Applied times-frac0.9

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

    6. Applied associate-*l/0.9

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

    7. Simplified0.6

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

    if 2.357897429842403e+78 < (* z 3.0)

    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 add-cube-cbrt0.7

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

    4. Applied times-frac2.3

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

    6. Applied *-un-lft-identity2.3

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

    7. Applied associate-*l*2.3

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

    8. Simplified1.2

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

    10. Applied *-un-lft-identity1.2

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

    11. Applied times-frac1.2

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

    13. Applied *-un-lft-identity1.2

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

    14. Applied times-frac1.2

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

  4. Final simplification0.7

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

Reproduce

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