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

Average Error: 7.9 → 6.3

Time: 8.5s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 2.985
  2. x1 = 0.000209

\[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{\sqrt{x0 \cdot \left(-x0\right) + \sqrt{x0} \cdot {\left(\frac{\sqrt{x0}}{1 - x1}\right)}^{3}}}{\frac{\left(\frac{x0}{1 - x1} + \frac{\sqrt{x0}}{1 - x1} \cdot \frac{\sqrt{x0}}{1 - x1}\right) + x0}{\sqrt{x0 \cdot \left(-x0\right) + \sqrt{x0} \cdot {\left(\frac{\sqrt{x0}}{1 - x1}\right)}^{3}}}}\]

C

double f(double x0, double x1) {
        double r207897 = x0;
        double r207898 = 1.0;
        double r207899 = x1;
        double r207900 = r207898 - r207899;
        double r207901 = r207897 / r207900;
        double r207902 = r207901 - r207897;
        return r207902;
}

↓

double f(double x0, double x1) {
        double r207903 = x0;
        double r207904 = -r207903;
        double r207905 = r207903 * r207904;
        double r207906 = sqrt(r207903);
        double r207907 = 1.0;
        double r207908 = x1;
        double r207909 = r207907 - r207908;
        double r207910 = r207906 / r207909;
        double r207911 = 3.0;
        double r207912 = pow(r207910, r207911);
        double r207913 = r207906 * r207912;
        double r207914 = r207905 + r207913;
        double r207915 = sqrt(r207914);
        double r207916 = r207903 / r207909;
        double r207917 = r207910 * r207910;
        double r207918 = r207916 + r207917;
        double r207919 = r207918 + r207903;
        double r207920 = r207919 / r207915;
        double r207921 = r207915 / r207920;
        return r207921;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.3
Herbie	6.3

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

Derivation

1. Initial program 7.9

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

3. Applied add-sqr-sqrt 7.9

   \[\leadsto \frac{\color{blue}{\sqrt{x0} \cdot \sqrt{x0}}}{1 - x1} - x0\]

4. Applied associate-/l* 7.7

   \[\leadsto \color{blue}{\frac{\sqrt{x0}}{\frac{1 - x1}{\sqrt{x0}}}} - x0\]
5. Using strategy rm

6. Applied add-sqr-sqrt 7.7

   \[\leadsto \frac{\sqrt{x0}}{\frac{1 - x1}{\sqrt{x0}}} - \color{blue}{\sqrt{x0} \cdot \sqrt{x0}}\]

7. Applied associate-/r/ 8.2

   \[\leadsto \color{blue}{\frac{\sqrt{x0}}{1 - x1} \cdot \sqrt{x0}} - \sqrt{x0} \cdot \sqrt{x0}\]

8. Applied distribute-rgt-out-- 7.2

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

10. Applied flip3-- 7.3

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

11. Applied associate-*r/ 7.3

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

12. Simplified 6.5

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

14. Applied add-sqr-sqrt 6.5

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

15. Applied associate-/l* 6.3

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

16. Simplified 6.3

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

17. Final simplification 6.3

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

Reproduce

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