Average Error: 3.9 → 0.9
Time: 14.8s
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 r439196 = x;
        double r439197 = y;
        double r439198 = z;
        double r439199 = 3.0;
        double r439200 = r439198 * r439199;
        double r439201 = r439197 / r439200;
        double r439202 = r439196 - r439201;
        double r439203 = t;
        double r439204 = r439200 * r439197;
        double r439205 = r439203 / r439204;
        double r439206 = r439202 + r439205;
        return r439206;
}
↓
double f(double x, double y, double z, double t) {
        double r439207 = z;
        double r439208 = 3.0;
        double r439209 = r439207 * r439208;
        double r439210 = -1.679549677934963e-09;
        bool r439211 = r439209 <= r439210;
        double r439212 = x;
        double r439213 = 0.3333333333333333;
        double r439214 = y;
        double r439215 = r439214 / r439207;
        double r439216 = r439213 * r439215;
        double r439217 = r439212 - r439216;
        double r439218 = t;
        double r439219 = r439218 / r439208;
        double r439220 = r439207 * r439214;
        double r439221 = r439219 / r439220;
        double r439222 = r439217 + r439221;
        double r439223 = 1.988546582597583e+129;
        bool r439224 = r439209 <= r439223;
        double r439225 = r439214 / r439209;
        double r439226 = r439212 - r439225;
        double r439227 = 1.0;
        double r439228 = r439227 / r439209;
        double r439229 = r439218 / r439214;
        double r439230 = r439228 * r439229;
        double r439231 = r439226 + r439230;
        double r439232 = r439218 / r439207;
        double r439233 = r439232 / r439214;
        double r439234 = r439213 * r439233;
        double r439235 = r439226 + r439234;
        double r439236 = r439224 ? r439231 : r439235;
        double r439237 = r439211 ? r439222 : r439236;
        return r439237;
}

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))))