Optimisation.CirclePacking:place from circle-packing-0.1.0.4, D

Average Error: 6.7 → 1.4

Time: 18.8s

Precision: 64

Math

\[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 -3.044655729417007005910857198088774777123 \cdot 10^{-65}:\\ \;\;\;\;x + \frac{\left(z - x\right) \cdot y}{t}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{t} \cdot \left(z - x\right) + x\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r18580925 = x;
        double r18580926 = y;
        double r18580927 = z;
        double r18580928 = r18580927 - r18580925;
        double r18580929 = r18580926 * r18580928;
        double r18580930 = t;
        double r18580931 = r18580929 / r18580930;
        double r18580932 = r18580925 + r18580931;
        return r18580932;
}

↓

double f(double x, double y, double z, double t) {
        double r18580933 = x;
        double r18580934 = z;
        double r18580935 = r18580934 - r18580933;
        double r18580936 = y;
        double r18580937 = r18580935 * r18580936;
        double r18580938 = t;
        double r18580939 = r18580937 / r18580938;
        double r18580940 = r18580933 + r18580939;
        double r18580941 = -inf.0;
        bool r18580942 = r18580940 <= r18580941;
        double r18580943 = r18580938 / r18580935;
        double r18580944 = r18580936 / r18580943;
        double r18580945 = r18580933 + r18580944;
        double r18580946 = -3.044655729417007e-65;
        bool r18580947 = r18580940 <= r18580946;
        double r18580948 = r18580936 / r18580938;
        double r18580949 = r18580948 * r18580935;
        double r18580950 = r18580949 + r18580933;
        double r18580951 = r18580947 ? r18580940 : r18580950;
        double r18580952 = r18580942 ? r18580945 : r18580951;
        return r18580952;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	6.7
Target	2.1
Herbie	1.4

\[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 64.0

      \[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)) < -3.044655729417007e-65

   1. Initial program 0.1

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

   if -3.044655729417007e-65 < (+ x (/ (* y (- z x)) t))

   1. Initial program 6.2

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

   2. Taylor expanded around 0 6.2

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

   3. Simplified 2.2

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

4. Final simplification 1.4

   \[\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 -3.044655729417007005910857198088774777123 \cdot 10^{-65}:\\ \;\;\;\;x + \frac{\left(z - x\right) \cdot y}{t}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{t} \cdot \left(z - x\right) + x\\ \end{array}\]

Reproduce

herbie shell --seed 2019169 
(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)))