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

Average Error: 7.9 → 5.5

Time: 25.8s

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

C

double f(double x0, double x1) {
        double r6610922 = x0;
        double r6610923 = 1.0;
        double r6610924 = x1;
        double r6610925 = r6610923 - r6610924;
        double r6610926 = r6610922 / r6610925;
        double r6610927 = r6610926 - r6610922;
        return r6610927;
}

↓

double f(double x0, double x1) {
        double r6610928 = x0;
        double r6610929 = r6610928 * r6610928;
        double r6610930 = r6610929 * r6610928;
        double r6610931 = 1.0;
        double r6610932 = x1;
        double r6610933 = r6610931 - r6610932;
        double r6610934 = r6610930 / r6610933;
        double r6610935 = r6610933 * r6610933;
        double r6610936 = r6610934 / r6610935;
        double r6610937 = r6610936 * r6610936;
        double r6610938 = r6610930 * r6610930;
        double r6610939 = r6610937 - r6610938;
        double r6610940 = log(r6610939);
        double r6610941 = exp(r6610940);
        double r6610942 = r6610930 + r6610936;
        double r6610943 = r6610941 / r6610942;
        double r6610944 = r6610928 / r6610933;
        double r6610945 = r6610944 * r6610944;
        double r6610946 = r6610928 * r6610944;
        double r6610947 = r6610929 + r6610946;
        double r6610948 = r6610945 + r6610947;
        double r6610949 = r6610943 / r6610948;
        return r6610949;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.3
Herbie	5.5

\[\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.3

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

6. Applied associate-*l/ 7.3

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

7. Applied frac-times 6.2

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

8. Simplified 6.0

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

10. Applied flip-- 5.9

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

12. Applied add-exp-log 5.5

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

13. Final simplification 5.5

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

Reproduce

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