(- (/ x0 (- 1 x1)) x0)

Average Error: 7.9 → 5.6

Time: 10.4s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 1.855
  2. x1 = 0.0186

\[x0 = 1.854999999999999982236431605997495353222 \land x1 = 2.090000000000000115064208161541614572343 \cdot 10^{-4} \lor x0 = 2.984999999999999875655021241982467472553 \land x1 = 0.01859999999999999847899445626353553961962\]

Math

\[\frac{x0}{1 - x1} - x0\]

↓

\[\frac{{x0}^{3} \cdot \frac{1}{{\left(1 - x1\right)}^{3}} - {x0}^{3}}{\left(\sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}} \cdot \sqrt[3]{\frac{x0}{1 - x1}}\right) \cdot \left(\sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}} \cdot \sqrt[3]{\frac{x0}{1 - x1}}\right)\right) + x0\right) \cdot \frac{x0}{1 - x1} + x0 \cdot x0}\]

C

double f(double x0, double x1) {
        double r160412 = x0;
        double r160413 = 1.0;
        double r160414 = x1;
        double r160415 = r160413 - r160414;
        double r160416 = r160412 / r160415;
        double r160417 = r160416 - r160412;
        return r160417;
}

↓

double f(double x0, double x1) {
        double r160418 = x0;
        double r160419 = 3.0;
        double r160420 = pow(r160418, r160419);
        double r160421 = 1.0;
        double r160422 = 1.0;
        double r160423 = x1;
        double r160424 = r160422 - r160423;
        double r160425 = pow(r160424, r160419);
        double r160426 = r160421 / r160425;
        double r160427 = r160420 * r160426;
        double r160428 = r160427 - r160420;
        double r160429 = r160418 / r160424;
        double r160430 = cbrt(r160429);
        double r160431 = cbrt(r160430);
        double r160432 = r160431 * r160430;
        double r160433 = r160432 * r160432;
        double r160434 = r160431 * r160433;
        double r160435 = r160434 + r160418;
        double r160436 = r160435 * r160429;
        double r160437 = r160418 * r160418;
        double r160438 = r160436 + r160437;
        double r160439 = r160428 / r160438;
        return r160439;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.3
Herbie	5.6

\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

1. Initial program 7.9

   \[\frac{x0}{1 - x1} - x0\]
2. Using strategy rm

3. Applied flip3-- 7.7

   \[\leadsto \color{blue}{\frac{{\left(\frac{x0}{1 - x1}\right)}^{3} - {x0}^{3}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}}\]

4. Simplified 7.7

   \[\leadsto \frac{{\left(\frac{x0}{1 - x1}\right)}^{3} - {x0}^{3}}{\color{blue}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + x0\right)}}\]
5. Using strategy rm

6. Applied div-inv 7.4

   \[\leadsto \frac{{\color{blue}{\left(x0 \cdot \frac{1}{1 - x1}\right)}}^{3} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + x0\right)}\]

7. Applied unpow-prod-down 6.5

   \[\leadsto \frac{\color{blue}{{x0}^{3} \cdot {\left(\frac{1}{1 - x1}\right)}^{3}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + x0\right)}\]

8. Simplified 5.7

   \[\leadsto \frac{{x0}^{3} \cdot \color{blue}{\frac{1}{{\left(1 - x1\right)}^{3}}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + x0\right)}\]
9. Using strategy rm

10. Applied add-cube-cbrt 5.6

    \[\leadsto \frac{{x0}^{3} \cdot \frac{1}{{\left(1 - x1\right)}^{3}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\color{blue}{\left(\sqrt[3]{\frac{x0}{1 - x1}} \cdot \sqrt[3]{\frac{x0}{1 - x1}}\right) \cdot \sqrt[3]{\frac{x0}{1 - x1}}} + x0\right)}\]
11. Using strategy rm

12. Applied add-cube-cbrt 5.5

    \[\leadsto \frac{{x0}^{3} \cdot \frac{1}{{\left(1 - x1\right)}^{3}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\left(\sqrt[3]{\frac{x0}{1 - x1}} \cdot \sqrt[3]{\frac{x0}{1 - x1}}\right) \cdot \color{blue}{\left(\left(\sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}} \cdot \sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}}\right) \cdot \sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}}\right)} + x0\right)}\]

13. Applied associate-*r* 5.5

    \[\leadsto \frac{{x0}^{3} \cdot \frac{1}{{\left(1 - x1\right)}^{3}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\color{blue}{\left(\left(\sqrt[3]{\frac{x0}{1 - x1}} \cdot \sqrt[3]{\frac{x0}{1 - x1}}\right) \cdot \left(\sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}} \cdot \sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}}\right)\right) \cdot \sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}}} + x0\right)}\]

14. Simplified 5.6

    \[\leadsto \frac{{x0}^{3} \cdot \frac{1}{{\left(1 - x1\right)}^{3}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\color{blue}{\left(\left(\sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}} \cdot \sqrt[3]{\frac{x0}{1 - x1}}\right) \cdot \left(\sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}} \cdot \sqrt[3]{\frac{x0}{1 - x1}}\right)\right)} \cdot \sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}} + x0\right)}\]

15. Final simplification 5.6

    \[\leadsto \frac{{x0}^{3} \cdot \frac{1}{{\left(1 - x1\right)}^{3}} - {x0}^{3}}{\left(\sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}} \cdot \left(\left(\sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}} \cdot \sqrt[3]{\frac{x0}{1 - x1}}\right) \cdot \left(\sqrt[3]{\sqrt[3]{\frac{x0}{1 - x1}}} \cdot \sqrt[3]{\frac{x0}{1 - x1}}\right)\right) + x0\right) \cdot \frac{x0}{1 - x1} + x0 \cdot x0}\]

Reproduce

herbie shell --seed 2019194 
(FPCore (x0 x1)
  :name "(- (/ x0 (- 1 x1)) x0)"
  :pre (or (and (== x0 1.855) (== x1 0.000209)) (and (== x0 2.985) (== x1 0.0186)))

  :herbie-target
  (/ (* x0 x1) (- 1.0 x1))

  (- (/ x0 (- 1.0 x1)) x0))