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

Average Error: 7.9 → 3.5

Time: 7.8s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

• could not determine a ground truth for program pre

  1. x0 = 1.855
  2. x1 = 0.0186

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

C

double f(double x0, double x1) {
        double r131540 = x0;
        double r131541 = 1.0;
        double r131542 = x1;
        double r131543 = r131541 - r131542;
        double r131544 = r131540 / r131543;
        double r131545 = r131544 - r131540;
        return r131545;
}

↓

double f(double x0, double x1) {
        double r131546 = x0;
        double r131547 = 3.0;
        double r131548 = pow(r131546, r131547);
        double r131549 = 1.0;
        double r131550 = x1;
        double r131551 = r131549 - r131550;
        double r131552 = 6.0;
        double r131553 = pow(r131551, r131552);
        double r131554 = r131548 / r131553;
        double r131555 = r131554 - r131548;
        double r131556 = exp(r131555);
        double r131557 = sqrt(r131556);
        double r131558 = log(r131557);
        double r131559 = r131558 + r131558;
        double r131560 = r131546 * r131546;
        double r131561 = r131546 / r131551;
        double r131562 = pow(r131551, r131547);
        double r131563 = r131546 / r131562;
        double r131564 = r131563 + r131561;
        double r131565 = r131561 * r131564;
        double r131566 = r131560 + r131565;
        double r131567 = r131559 / r131566;
        double r131568 = r131546 * r131567;
        double r131569 = r131561 + r131546;
        double r131570 = r131568 / r131569;
        return r131570;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.2
Herbie	3.5

\[\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. Simplified 6.3

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

6. Applied flip3-- 5.0

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

7. Simplified 4.9

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

9. Applied add-log-exp 4.9

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

10. Applied add-log-exp 4.9

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

11. Applied diff-log 4.5

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

12. Simplified 4.5

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

14. Applied add-sqr-sqrt 3.6

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

15. Applied log-prod 3.5

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

16. Final simplification 3.5

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

Reproduce

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