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

Average Error: 8.0 → 2.4

Time: 8.7s

Precision: 64

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

• 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\]

↓

\[\begin{array}{l} \mathbf{if}\;x1 \le 2.78888122558593676 \cdot 10^{-4}:\\ \;\;\;\;\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}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{\frac{x0}{1 - x1} + x0}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\log \left(e^{\frac{{x0}^{3}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{6} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}} - {x0}^{3}}\right)}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{\frac{x0}{1 - x1} + x0}\\ \end{array}\]

C

double f(double x0, double x1) {
        double r161705 = x0;
        double r161706 = 1.0;
        double r161707 = x1;
        double r161708 = r161706 - r161707;
        double r161709 = r161705 / r161708;
        double r161710 = r161709 - r161705;
        return r161710;
}

↓

double f(double x0, double x1) {
        double r161711 = x1;
        double r161712 = 0.0002788881225585937;
        bool r161713 = r161711 <= r161712;
        double r161714 = x0;
        double r161715 = 3.0;
        double r161716 = pow(r161714, r161715);
        double r161717 = 1.0;
        double r161718 = r161717 - r161711;
        double r161719 = 6.0;
        double r161720 = pow(r161718, r161719);
        double r161721 = r161716 / r161720;
        double r161722 = r161721 - r161716;
        double r161723 = exp(r161722);
        double r161724 = sqrt(r161723);
        double r161725 = log(r161724);
        double r161726 = r161725 + r161725;
        double r161727 = r161714 * r161714;
        double r161728 = r161714 / r161718;
        double r161729 = pow(r161718, r161715);
        double r161730 = r161714 / r161729;
        double r161731 = r161728 + r161730;
        double r161732 = r161728 * r161731;
        double r161733 = r161727 + r161732;
        double r161734 = r161726 / r161733;
        double r161735 = r161714 * r161734;
        double r161736 = r161728 + r161714;
        double r161737 = r161735 / r161736;
        double r161738 = sqrt(r161717);
        double r161739 = sqrt(r161711);
        double r161740 = r161738 + r161739;
        double r161741 = pow(r161740, r161719);
        double r161742 = r161738 - r161739;
        double r161743 = pow(r161742, r161719);
        double r161744 = r161741 * r161743;
        double r161745 = r161716 / r161744;
        double r161746 = r161745 - r161716;
        double r161747 = exp(r161746);
        double r161748 = log(r161747);
        double r161749 = r161748 / r161733;
        double r161750 = r161714 * r161749;
        double r161751 = r161750 / r161736;
        double r161752 = r161713 ? r161737 : r161751;
        return r161752;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	8.0
Target	0.2
Herbie	2.4

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

Derivation

1. Split input into 2 regimes

2. if x1 < 0.0002788881225585937

   1. Initial program 11.2

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

   3. Applied flip-- 11.4

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

   4. Simplified 8.7

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

      \[\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 5.8

      \[\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}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}}{\frac{x0}{1 - x1} + x0}\]
   8. Using strategy rm

   9. Applied add-log-exp 5.8

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

   10. Applied add-log-exp 5.8

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

   11. Applied diff-log 5.0

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

   12. Simplified 5.0

       \[\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}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{\frac{x0}{1 - x1} + x0}\]
   13. Using strategy rm

   14. Applied add-sqr-sqrt 3.3

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

   15. Applied log-prod 2.9

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

   if 0.0002788881225585937 < x1

   1. Initial program 4.6

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

   3. Applied flip-- 3.2

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

   4. Simplified 3.9

      \[\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-- 3.9

      \[\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 3.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}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}}{\frac{x0}{1 - x1} + x0}\]
   8. Using strategy rm

   9. Applied add-log-exp 3.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}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{\frac{x0}{1 - x1} + x0}\]

   10. Applied add-log-exp 3.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}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{\frac{x0}{1 - x1} + x0}\]

   11. Applied diff-log 3.9

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

   12. Simplified 3.8

       \[\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}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{\frac{x0}{1 - x1} + x0}\]
   13. Using strategy rm

   14. Applied add-sqr-sqrt 3.8

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

   15. Applied add-sqr-sqrt 3.8

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

   16. Applied difference-of-squares 3.8

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

   17. Applied unpow-prod-down 1.8

       \[\leadsto \frac{x0 \cdot \frac{\log \left(e^{\frac{{x0}^{3}}{\color{blue}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{6} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}}} - {x0}^{3}}\right)}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{\frac{x0}{1 - x1} + x0}\]
3. Recombined 2 regimes into one program.

4. Final simplification 2.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;x1 \le 2.78888122558593676 \cdot 10^{-4}:\\ \;\;\;\;\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}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{\frac{x0}{1 - x1} + x0}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\log \left(e^{\frac{{x0}^{3}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{6} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}} - {x0}^{3}}\right)}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{\frac{x0}{1 - x1} + x0}\\ \end{array}\]

Reproduce

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