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

Average Error: 7.9 → 2.1

Time: 10.5s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 1.855
  2. x1 = 0.0186

\[x0 = 1.854999999999999982236431605997495353222 \land x1 = 2.090000000000000115064208161541614572343 \cdot 10^{-4} \lor x0 = 2.984999999999999875655021241982467472553 \land x1 = 0.01859999999999999847899445626353553961962\]

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x1 \le 2.1826724243164061516238316773552696759 \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 + \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + x0\right) \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\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 + \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + x0\right) \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}}}{\frac{x0}{1 - x1} + x0}\\ \end{array}\]

C

double f(double x0, double x1) {
        double r143277 = x0;
        double r143278 = 1.0;
        double r143279 = x1;
        double r143280 = r143278 - r143279;
        double r143281 = r143277 / r143280;
        double r143282 = r143281 - r143277;
        return r143282;
}

↓

double f(double x0, double x1) {
        double r143283 = x1;
        double r143284 = 0.00021826724243164062;
        bool r143285 = r143283 <= r143284;
        double r143286 = x0;
        double r143287 = 3.0;
        double r143288 = pow(r143286, r143287);
        double r143289 = 1.0;
        double r143290 = r143289 - r143283;
        double r143291 = 6.0;
        double r143292 = pow(r143290, r143291);
        double r143293 = r143288 / r143292;
        double r143294 = r143293 - r143288;
        double r143295 = exp(r143294);
        double r143296 = sqrt(r143295);
        double r143297 = log(r143296);
        double r143298 = r143297 + r143297;
        double r143299 = r143286 * r143286;
        double r143300 = r143290 * r143290;
        double r143301 = r143286 / r143300;
        double r143302 = r143301 + r143286;
        double r143303 = r143302 * r143301;
        double r143304 = r143299 + r143303;
        double r143305 = r143298 / r143304;
        double r143306 = r143286 * r143305;
        double r143307 = r143286 / r143290;
        double r143308 = r143307 + r143286;
        double r143309 = r143306 / r143308;
        double r143310 = sqrt(r143289);
        double r143311 = sqrt(r143283);
        double r143312 = r143310 + r143311;
        double r143313 = pow(r143312, r143291);
        double r143314 = r143310 - r143311;
        double r143315 = pow(r143314, r143291);
        double r143316 = r143313 * r143315;
        double r143317 = r143288 / r143316;
        double r143318 = r143317 - r143288;
        double r143319 = exp(r143318);
        double r143320 = log(r143319);
        double r143321 = r143320 / r143304;
        double r143322 = r143286 * r143321;
        double r143323 = r143322 / r143308;
        double r143324 = r143285 ? r143309 : r143323;
        return r143324;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.2
Herbie	2.1

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

Derivation

1. Split input into 2 regimes

2. if x1 < 0.00021826724243164062

   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-- 6.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 6.0

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

   9. Applied add-log-exp 6.0

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

   10. Applied add-log-exp 6.0

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

   11. Applied diff-log 5.2

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

   12. Simplified 5.2

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

   14. Applied add-sqr-sqrt 3.5

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

   15. Applied log-prod 2.6

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

   if 0.00021826724243164062 < x1

   1. Initial program 4.5

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

   3. Applied flip-- 3.1

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

   4. Simplified 3.8

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

   11. Applied diff-log 4.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 + \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + x0\right) \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\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 + \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + x0\right) \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\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 + \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + x0\right) \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\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 + \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + x0\right) \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\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 + \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + x0\right) \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}}}{\frac{x0}{1 - x1} + x0}\]

   17. Applied unpow-prod-down 1.6

       \[\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 + \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + x0\right) \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}}}{\frac{x0}{1 - x1} + x0}\]
3. Recombined 2 regimes into one program.

4. Final simplification 2.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;x1 \le 2.1826724243164061516238316773552696759 \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 + \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + x0\right) \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\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 + \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + x0\right) \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}}}{\frac{x0}{1 - x1} + x0}\\ \end{array}\]

Reproduce

herbie shell --seed 2019303 
(FPCore (x0 x1)
  :name "(- (/ x0 (- 1 x1)) x0)"
  :precision binary64
  :pre (or (and (== x0 1.855) (== x1 2.09000000000000012e-4)) (and (== x0 2.98499999999999988) (== x1 0.018599999999999998)))

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

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