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

Average Error: 7.9 → 5.2

Time: 3.5s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 2.985
  2. x1 = 0.000209

\[x0 = 1.855 \land x1 = 2.09000000000000012 \cdot 10^{-4} \lor x0 = 2.98499999999999988 \land x1 = 0.018599999999999998\]

Math

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

↓

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

C

double f(double x0, double x1) {
        double r289358 = x0;
        double r289359 = 1.0;
        double r289360 = x1;
        double r289361 = r289359 - r289360;
        double r289362 = r289358 / r289361;
        double r289363 = r289362 - r289358;
        return r289363;
}

↓

double f(double x0, double x1) {
        double r289364 = x0;
        double r289365 = 1.0;
        double r289366 = r289365 * r289365;
        double r289367 = x1;
        double r289368 = r289367 * r289367;
        double r289369 = r289366 - r289368;
        double r289370 = r289364 / r289369;
        double r289371 = r289370 * r289365;
        double r289372 = r289365 - r289367;
        double r289373 = r289364 / r289372;
        double r289374 = r289371 * r289373;
        double r289375 = r289367 * r289370;
        double r289376 = r289375 * r289373;
        double r289377 = r289364 * r289364;
        double r289378 = r289376 - r289377;
        double r289379 = r289374 + r289378;
        double r289380 = exp(r289379);
        double r289381 = log(r289380);
        double r289382 = r289373 + r289364;
        double r289383 = r289381 / r289382;
        return r289383;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.3
Herbie	5.2

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

Derivation

1. Initial program 7.9

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

3. Applied flip-- 7.3

   \[\leadsto \color{blue}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\frac{x0}{1 - x1} + x0}}\]
4. Using strategy rm

5. Applied flip-- 5.6

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

6. Applied associate-/r/ 6.1

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

8. Applied add-log-exp 6.1

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

9. Applied add-log-exp 6.1

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

10. Applied diff-log 5.8

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

11. Simplified 5.8

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

13. Applied distribute-lft-in 6.3

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

14. Applied distribute-rgt-in 5.2

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

15. Applied associate--l+ 5.2

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

16. Simplified 5.2

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

17. Final simplification 5.2

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

Reproduce

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

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

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