Average Error: 3.5 → 1.0
Time: 18.7s
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 -3.812840139410096 \cdot 10^{-05}:\\ \;\;\;\;\frac{t}{\left(z \cdot y\right) \cdot 3.0} + \left(x - \frac{y}{z \cdot 3.0}\right)\\ \mathbf{elif}\;z \cdot 3.0 \le 1.640266769777498 \cdot 10^{+158}:\\ \;\;\;\;\left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right) + \frac{\frac{t}{y}}{z \cdot 3.0}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right) + \frac{\frac{t}{z}}{3.0} \cdot \frac{1}{y}\\ \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 -3.812840139410096 \cdot 10^{-05}:\\
\;\;\;\;\frac{t}{\left(z \cdot y\right) \cdot 3.0} + \left(x - \frac{y}{z \cdot 3.0}\right)\\

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

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

\end{array}
double f(double x, double y, double z, double t) {
        double r36446844 = x;
        double r36446845 = y;
        double r36446846 = z;
        double r36446847 = 3.0;
        double r36446848 = r36446846 * r36446847;
        double r36446849 = r36446845 / r36446848;
        double r36446850 = r36446844 - r36446849;
        double r36446851 = t;
        double r36446852 = r36446848 * r36446845;
        double r36446853 = r36446851 / r36446852;
        double r36446854 = r36446850 + r36446853;
        return r36446854;
}
↓
double f(double x, double y, double z, double t) {
        double r36446855 = z;
        double r36446856 = 3.0;
        double r36446857 = r36446855 * r36446856;
        double r36446858 = -3.812840139410096e-05;
        bool r36446859 = r36446857 <= r36446858;
        double r36446860 = t;
        double r36446861 = y;
        double r36446862 = r36446855 * r36446861;
        double r36446863 = r36446862 * r36446856;
        double r36446864 = r36446860 / r36446863;
        double r36446865 = x;
        double r36446866 = r36446861 / r36446857;
        double r36446867 = r36446865 - r36446866;
        double r36446868 = r36446864 + r36446867;
        double r36446869 = 1.640266769777498e+158;
        bool r36446870 = r36446857 <= r36446869;
        double r36446871 = r36446861 / r36446856;
        double r36446872 = 1.0;
        double r36446873 = r36446872 / r36446855;
        double r36446874 = r36446871 * r36446873;
        double r36446875 = r36446865 - r36446874;
        double r36446876 = r36446860 / r36446861;
        double r36446877 = r36446876 / r36446857;
        double r36446878 = r36446875 + r36446877;
        double r36446879 = r36446860 / r36446855;
        double r36446880 = r36446879 / r36446856;
        double r36446881 = r36446872 / r36446861;
        double r36446882 = r36446880 * r36446881;
        double r36446883 = r36446875 + r36446882;
        double r36446884 = r36446870 ? r36446878 : r36446883;
        double r36446885 = r36446859 ? r36446868 : r36446884;
        return r36446885;
}

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.9
Herbie1.0
\[\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) < -3.812840139410096e-05

    1. Initial program 0.4

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

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

    if -3.812840139410096e-05 < (* z 3.0) < 1.640266769777498e+158

    1. Initial program 6.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 add-cube-cbrt6.9

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

    4. Applied times-frac1.1

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

    6. Applied div-inv1.1

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

    7. Applied associate-*r*2.8

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

    8. Simplified2.5

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

    10. Applied *-un-lft-identity2.5

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

    11. Applied times-frac2.5

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

    13. Applied associate-*l/1.4

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

    14. Simplified1.4

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

    if 1.640266769777498e+158 < (* z 3.0)

    1. Initial program 0.7

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

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

    4. Applied times-frac3.3

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

    6. Applied div-inv3.3

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

    7. Applied associate-*r*1.5

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

    8. Simplified1.3

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

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

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

    11. Applied times-frac1.3

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

    13. Applied associate-/r*1.3

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

  4. Final simplification1.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot 3.0 \le -3.812840139410096 \cdot 10^{-05}:\\ \;\;\;\;\frac{t}{\left(z \cdot y\right) \cdot 3.0} + \left(x - \frac{y}{z \cdot 3.0}\right)\\ \mathbf{elif}\;z \cdot 3.0 \le 1.640266769777498 \cdot 10^{+158}:\\ \;\;\;\;\left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right) + \frac{\frac{t}{y}}{z \cdot 3.0}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right) + \frac{\frac{t}{z}}{3.0} \cdot \frac{1}{y}\\ \end{array}\]

Reproduce

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