(- (/ 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 r136783 = x0;
        double r136784 = 1.0;
        double r136785 = x1;
        double r136786 = r136784 - r136785;
        double r136787 = r136783 / r136786;
        double r136788 = r136787 - r136783;
        return r136788;
}

↓

double f(double x0, double x1) {
        double r136789 = x0;
        double r136790 = 3.0;
        double r136791 = pow(r136789, r136790);
        double r136792 = 1.0;
        double r136793 = x1;
        double r136794 = r136792 - r136793;
        double r136795 = 6.0;
        double r136796 = pow(r136794, r136795);
        double r136797 = r136791 / r136796;
        double r136798 = r136797 - r136791;
        double r136799 = exp(r136798);
        double r136800 = sqrt(r136799);
        double r136801 = log(r136800);
        double r136802 = r136801 + r136801;
        double r136803 = r136789 * r136789;
        double r136804 = r136789 / r136794;
        double r136805 = pow(r136794, r136790);
        double r136806 = r136789 / r136805;
        double r136807 = r136806 + r136804;
        double r136808 = r136804 * r136807;
        double r136809 = r136803 + r136808;
        double r136810 = r136802 / r136809;
        double r136811 = r136789 * r136810;
        double r136812 = r136804 + r136789;
        double r136813 = r136811 / r136812;
        return r136813;
}

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))