Average Error: 5.9 → 0.8
Time: 16.2s
Precision: 64
\[x + \frac{y \cdot \left(z - x\right)}{t}\]
↓
\[\begin{array}{l} \mathbf{if}\;x + \frac{\left(z - x\right) \cdot y}{t} = -\infty:\\ \;\;\;\;x + \frac{y}{\frac{t}{z - x}}\\ \mathbf{elif}\;x + \frac{\left(z - x\right) \cdot y}{t} \le 6.397153737655851 \cdot 10^{+305}:\\ \;\;\;\;x + \frac{\left(z - x\right) \cdot y}{t}\\ \mathbf{else}:\\ \;\;\;\;\frac{z - x}{\frac{t}{y}} + x\\ \end{array}\]
x + \frac{y \cdot \left(z - x\right)}{t}
↓
\begin{array}{l}
\mathbf{if}\;x + \frac{\left(z - x\right) \cdot y}{t} = -\infty:\\
\;\;\;\;x + \frac{y}{\frac{t}{z - x}}\\

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

\mathbf{else}:\\
\;\;\;\;\frac{z - x}{\frac{t}{y}} + x\\

\end{array}
double f(double x, double y, double z, double t) {
        double r29145217 = x;
        double r29145218 = y;
        double r29145219 = z;
        double r29145220 = r29145219 - r29145217;
        double r29145221 = r29145218 * r29145220;
        double r29145222 = t;
        double r29145223 = r29145221 / r29145222;
        double r29145224 = r29145217 + r29145223;
        return r29145224;
}
↓
double f(double x, double y, double z, double t) {
        double r29145225 = x;
        double r29145226 = z;
        double r29145227 = r29145226 - r29145225;
        double r29145228 = y;
        double r29145229 = r29145227 * r29145228;
        double r29145230 = t;
        double r29145231 = r29145229 / r29145230;
        double r29145232 = r29145225 + r29145231;
        double r29145233 = -inf.0;
        bool r29145234 = r29145232 <= r29145233;
        double r29145235 = r29145230 / r29145227;
        double r29145236 = r29145228 / r29145235;
        double r29145237 = r29145225 + r29145236;
        double r29145238 = 6.397153737655851e+305;
        bool r29145239 = r29145232 <= r29145238;
        double r29145240 = r29145230 / r29145228;
        double r29145241 = r29145227 / r29145240;
        double r29145242 = r29145241 + r29145225;
        double r29145243 = r29145239 ? r29145232 : r29145242;
        double r29145244 = r29145234 ? r29145237 : r29145243;
        return r29145244;
}

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

Original5.9
Target2.0
Herbie0.8
\[x - \left(x \cdot \frac{y}{t} + \left(-z\right) \cdot \frac{y}{t}\right)\]

Derivation

  1. Split input into 3 regimes

  2. if (+ x (/ (* y (- z x)) t)) < -inf.0

    1. Initial program 60.2

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

    3. Applied associate-/l*0.2

      \[\leadsto x + \color{blue}{\frac{y}{\frac{t}{z - x}}}\]

    if -inf.0 < (+ x (/ (* y (- z x)) t)) < 6.397153737655851e+305

    1. Initial program 0.8

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

    if 6.397153737655851e+305 < (+ x (/ (* y (- z x)) t))

    1. Initial program 57.9

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

    3. Applied *-un-lft-identity57.9

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

    4. Applied *-commutative57.9

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

    5. Applied times-frac0.5

      \[\leadsto x + \color{blue}{\frac{z - x}{1} \cdot \frac{y}{t}}\]

    6. Simplified0.5

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

    8. Applied clear-num0.6

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

    9. Applied un-div-inv0.5

      \[\leadsto x + \color{blue}{\frac{z - x}{\frac{t}{y}}}\]
  3. Recombined 3 regimes into one program.

  4. Final simplification0.8

    \[\leadsto \begin{array}{l} \mathbf{if}\;x + \frac{\left(z - x\right) \cdot y}{t} = -\infty:\\ \;\;\;\;x + \frac{y}{\frac{t}{z - x}}\\ \mathbf{elif}\;x + \frac{\left(z - x\right) \cdot y}{t} \le 6.397153737655851 \cdot 10^{+305}:\\ \;\;\;\;x + \frac{\left(z - x\right) \cdot y}{t}\\ \mathbf{else}:\\ \;\;\;\;\frac{z - x}{\frac{t}{y}} + x\\ \end{array}\]

Reproduce

herbie shell --seed 2019158 
(FPCore (x y z t)
  :name "Optimisation.CirclePacking:place from circle-packing-0.1.0.4, D"

  :herbie-target
  (- x (+ (* x (/ y t)) (* (- z) (/ y t))))

  (+ x (/ (* y (- z x)) t)))