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

Average Error: 6.5 → 0.6

Time: 3.7s

Precision: 64

Math

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

↓

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

C

double f(double x, double y, double z, double t, double a) {
        double r296761 = x;
        double r296762 = y;
        double r296763 = z;
        double r296764 = t;
        double r296765 = r296763 - r296764;
        double r296766 = r296762 * r296765;
        double r296767 = a;
        double r296768 = r296766 / r296767;
        double r296769 = r296761 - r296768;
        return r296769;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r296770 = y;
        double r296771 = z;
        double r296772 = t;
        double r296773 = r296771 - r296772;
        double r296774 = r296770 * r296773;
        double r296775 = a;
        double r296776 = r296774 / r296775;
        double r296777 = -inf.0;
        bool r296778 = r296776 <= r296777;
        double r296779 = x;
        double r296780 = r296770 / r296775;
        double r296781 = 1.0;
        double r296782 = r296781 / r296773;
        double r296783 = r296780 / r296782;
        double r296784 = r296779 - r296783;
        double r296785 = 1.3025853576837356e+290;
        bool r296786 = r296776 <= r296785;
        double r296787 = pow(r296776, r296781);
        double r296788 = r296779 - r296787;
        double r296789 = r296773 / r296775;
        double r296790 = r296770 * r296789;
        double r296791 = r296779 - r296790;
        double r296792 = r296786 ? r296788 : r296791;
        double r296793 = r296778 ? r296784 : r296792;
        return r296793;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Target

Original	6.5
Target	0.8
Herbie	0.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 3 regimes

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

   1. Initial program 64.0

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

   3. Applied associate-/l* 0.2

      \[\leadsto x - \color{blue}{\frac{y}{\frac{a}{z - t}}}\]
   4. Using strategy rm

   5. Applied div-inv 0.2

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

   6. Applied associate-/r* 0.3

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

   if -inf.0 < (/ (* y (- z t)) a) < 1.3025853576837356e+290

   1. Initial program 0.4

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

   3. Applied *-un-lft-identity 0.4

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

   4. Applied times-frac 6.2

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

   5. Simplified 6.2

      \[\leadsto x - \color{blue}{y} \cdot \frac{z - t}{a}\]
   6. Using strategy rm

   7. Applied *-un-lft-identity 6.2

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

   8. Applied add-cube-cbrt 6.6

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

   9. Applied times-frac 6.6

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

   10. Applied associate-*r* 1.9

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

   11. Simplified 1.9

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

   13. Applied pow1 1.9

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

   14. Applied pow1 1.9

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

   15. Applied pow1 1.9

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

   16. Applied pow1 1.9

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

   17. Applied pow-prod-down 1.9

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

   18. Applied pow-prod-down 1.9

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

   19. Applied pow-prod-down 1.9

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

   20. Simplified 0.4

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

   if 1.3025853576837356e+290 < (/ (* y (- z t)) a)

   1. Initial program 52.7

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

   3. Applied *-un-lft-identity 52.7

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

   4. Applied times-frac 4.8

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

   5. Simplified 4.8

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

4. Final simplification 0.6

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

Reproduce

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

  :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)))