Average Error: 5.5 → 0.5
Time: 20.6s
Precision: 64
\[x - \frac{y \cdot \left(z - t\right)}{a}\]
↓
\[\begin{array}{l} \mathbf{if}\;\left(z - t\right) \cdot y = -\infty:\\ \;\;\;\;x - \frac{z - t}{a} \cdot y\\ \mathbf{elif}\;\left(z - t\right) \cdot y \le 4.602631262379337 \cdot 10^{+178}:\\ \;\;\;\;x - \frac{\left(z - t\right) \cdot y}{a}\\ \mathbf{else}:\\ \;\;\;\;x - \left(z - t\right) \cdot \frac{y}{a}\\ \end{array}\]
x - \frac{y \cdot \left(z - t\right)}{a}
↓
\begin{array}{l}
\mathbf{if}\;\left(z - t\right) \cdot y = -\infty:\\
\;\;\;\;x - \frac{z - t}{a} \cdot y\\

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

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

\end{array}
double f(double x, double y, double z, double t, double a) {
        double r28096784 = x;
        double r28096785 = y;
        double r28096786 = z;
        double r28096787 = t;
        double r28096788 = r28096786 - r28096787;
        double r28096789 = r28096785 * r28096788;
        double r28096790 = a;
        double r28096791 = r28096789 / r28096790;
        double r28096792 = r28096784 - r28096791;
        return r28096792;
}
↓
double f(double x, double y, double z, double t, double a) {
        double r28096793 = z;
        double r28096794 = t;
        double r28096795 = r28096793 - r28096794;
        double r28096796 = y;
        double r28096797 = r28096795 * r28096796;
        double r28096798 = -inf.0;
        bool r28096799 = r28096797 <= r28096798;
        double r28096800 = x;
        double r28096801 = a;
        double r28096802 = r28096795 / r28096801;
        double r28096803 = r28096802 * r28096796;
        double r28096804 = r28096800 - r28096803;
        double r28096805 = 4.602631262379337e+178;
        bool r28096806 = r28096797 <= r28096805;
        double r28096807 = r28096797 / r28096801;
        double r28096808 = r28096800 - r28096807;
        double r28096809 = r28096796 / r28096801;
        double r28096810 = r28096795 * r28096809;
        double r28096811 = r28096800 - r28096810;
        double r28096812 = r28096806 ? r28096808 : r28096811;
        double r28096813 = r28096799 ? r28096804 : r28096812;
        return r28096813;
}

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

Original5.5
Target0.7
Herbie0.5
\[\begin{array}{l} \mathbf{if}\;y \lt -1.0761266216389975 \cdot 10^{-10}:\\ \;\;\;\;x - \frac{1}{\frac{\frac{a}{z - t}}{y}}\\ \mathbf{elif}\;y \lt 2.894426862792089 \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 3 regimes

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

    1. Initial program 60.1

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

    3. Applied *-un-lft-identity60.1

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

    4. Applied times-frac0.2

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

    5. Simplified0.2

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

    if -inf.0 < (* y (- z t)) < 4.602631262379337e+178

    1. Initial program 0.4

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

    if 4.602631262379337e+178 < (* y (- z t))

    1. Initial program 23.3

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

    3. Applied *-un-lft-identity23.3

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

    4. Applied *-commutative23.3

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

    5. Applied times-frac0.7

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

    6. Simplified0.7

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

  4. Final simplification0.5

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

Reproduce

herbie shell --seed 2019158 
(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 (/ (/ a (- z t)) y))) (if (< y 2.894426862792089e-49) (- x (/ (* y (- z t)) a)) (- x (/ y (/ a (- z t))))))

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