Average Error: 6.7 → 0.9
Time: 13.7s
Precision: 64
\[x + \frac{y \cdot \left(z - x\right)}{t}\]
↓
\[\begin{array}{l} \mathbf{if}\;x + \frac{y \cdot \left(z - x\right)}{t} = -\infty \lor \neg \left(x + \frac{y \cdot \left(z - x\right)}{t} \le 1.173312102384923336966143672822790105936 \cdot 10^{295}\right):\\ \;\;\;\;x + y \cdot \frac{z - x}{t}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{y \cdot \left(z - x\right)}{t}\\ \end{array}\]
x + \frac{y \cdot \left(z - x\right)}{t}
↓
\begin{array}{l}
\mathbf{if}\;x + \frac{y \cdot \left(z - x\right)}{t} = -\infty \lor \neg \left(x + \frac{y \cdot \left(z - x\right)}{t} \le 1.173312102384923336966143672822790105936 \cdot 10^{295}\right):\\
\;\;\;\;x + y \cdot \frac{z - x}{t}\\

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

\end{array}
double f(double x, double y, double z, double t) {
        double r233573 = x;
        double r233574 = y;
        double r233575 = z;
        double r233576 = r233575 - r233573;
        double r233577 = r233574 * r233576;
        double r233578 = t;
        double r233579 = r233577 / r233578;
        double r233580 = r233573 + r233579;
        return r233580;
}
↓
double f(double x, double y, double z, double t) {
        double r233581 = x;
        double r233582 = y;
        double r233583 = z;
        double r233584 = r233583 - r233581;
        double r233585 = r233582 * r233584;
        double r233586 = t;
        double r233587 = r233585 / r233586;
        double r233588 = r233581 + r233587;
        double r233589 = -inf.0;
        bool r233590 = r233588 <= r233589;
        double r233591 = 1.1733121023849233e+295;
        bool r233592 = r233588 <= r233591;
        double r233593 = !r233592;
        bool r233594 = r233590 || r233593;
        double r233595 = r233584 / r233586;
        double r233596 = r233582 * r233595;
        double r233597 = r233581 + r233596;
        double r233598 = r233594 ? r233597 : r233588;
        return r233598;
}

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

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

Derivation

  1. Split input into 2 regimes

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

    1. Initial program 56.7

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

    3. Applied *-un-lft-identity56.7

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

    4. Applied times-frac2.5

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

    5. Simplified2.5

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

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

    1. Initial program 0.7

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

  4. Final simplification0.9

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

Reproduce

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

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

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