Average Error: 6.0 → 0.6
Time: 18.3s
Precision: 64
\[x - \frac{y \cdot \left(z - t\right)}{a}\]
↓
\[\begin{array}{l} \mathbf{if}\;y \cdot \left(z - t\right) = -\infty \lor \neg \left(y \cdot \left(z - t\right) \le 1.99823853113780918 \cdot 10^{149}\right):\\ \;\;\;\;x + \left(-y \cdot \frac{z - t}{a}\right)\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y \cdot \left(z - t\right)}{a}\\ \end{array}\]
x - \frac{y \cdot \left(z - t\right)}{a}
↓
\begin{array}{l}
\mathbf{if}\;y \cdot \left(z - t\right) = -\infty \lor \neg \left(y \cdot \left(z - t\right) \le 1.99823853113780918 \cdot 10^{149}\right):\\
\;\;\;\;x + \left(-y \cdot \frac{z - t}{a}\right)\\

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

\end{array}
double f(double x, double y, double z, double t, double a) {
        double r188831 = x;
        double r188832 = y;
        double r188833 = z;
        double r188834 = t;
        double r188835 = r188833 - r188834;
        double r188836 = r188832 * r188835;
        double r188837 = a;
        double r188838 = r188836 / r188837;
        double r188839 = r188831 - r188838;
        return r188839;
}
↓
double f(double x, double y, double z, double t, double a) {
        double r188840 = y;
        double r188841 = z;
        double r188842 = t;
        double r188843 = r188841 - r188842;
        double r188844 = r188840 * r188843;
        double r188845 = -inf.0;
        bool r188846 = r188844 <= r188845;
        double r188847 = 1.9982385311378092e+149;
        bool r188848 = r188844 <= r188847;
        double r188849 = !r188848;
        bool r188850 = r188846 || r188849;
        double r188851 = x;
        double r188852 = a;
        double r188853 = r188843 / r188852;
        double r188854 = r188840 * r188853;
        double r188855 = -r188854;
        double r188856 = r188851 + r188855;
        double r188857 = r188844 / r188852;
        double r188858 = r188851 - r188857;
        double r188859 = r188850 ? r188856 : r188858;
        return r188859;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original6.0
Target0.6
Herbie0.6
\[\begin{array}{l} \mathbf{if}\;y \lt -1.07612662163899753 \cdot 10^{-10}:\\ \;\;\;\;x - \frac{1}{\frac{\frac{a}{z - t}}{y}}\\ \mathbf{elif}\;y \lt 2.8944268627920891 \cdot 10^{-49}:\\ \;\;\;\;x - \frac{y \cdot \left(z - t\right)}{a}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y}{\frac{a}{z - t}}\\ \end{array}\]

Derivation

  1. Split input into 2 regimes

  2. if (* y (- z t)) < -inf.0 or 1.9982385311378092e+149 < (* y (- z t))

    1. Initial program 31.7

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

    3. Applied div-inv31.7

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

    5. Applied sub-neg31.7

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

    6. Simplified1.7

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

    if -inf.0 < (* y (- z t)) < 1.9982385311378092e+149

    1. Initial program 0.3

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

  4. Final simplification0.6

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

Reproduce

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

  :herbie-target
  (if (< y -1.0761266216389975e-10) (- x (/ 1.0 (/ (/ a (- z t)) y))) (if (< y 2.894426862792089e-49) (- x (/ (* y (- z t)) a)) (- x (/ y (/ a (- z t))))))

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