Average Error: 7.9 → 5.5
Time: 11.2s
Precision: 64
\[x0 = 1.854999999999999982236431605997495353222 \land x1 = 2.090000000000000115064208161541614572343 \cdot 10^{-4} \lor x0 = 2.984999999999999875655021241982467472553 \land x1 = 0.01859999999999999847899445626353553961962\]
\[\frac{x0}{1 - x1} - x0\]
↓
\[\frac{{x0}^{3} \cdot \frac{1}{{\left(1 - x1\right)}^{3}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \frac{{x0}^{3} + {\left({\left(\frac{x0}{1 - x1}\right)}^{\left(\sqrt{3}\right)}\right)}^{\left(\sqrt{3}\right)}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + x0 \cdot \left(x0 - \frac{x0}{1 - x1}\right)}}\]
\frac{x0}{1 - x1} - x0
↓
\frac{{x0}^{3} \cdot \frac{1}{{\left(1 - x1\right)}^{3}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \frac{{x0}^{3} + {\left({\left(\frac{x0}{1 - x1}\right)}^{\left(\sqrt{3}\right)}\right)}^{\left(\sqrt{3}\right)}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + x0 \cdot \left(x0 - \frac{x0}{1 - x1}\right)}}
double f(double x0, double x1) {
        double r157404 = x0;
        double r157405 = 1.0;
        double r157406 = x1;
        double r157407 = r157405 - r157406;
        double r157408 = r157404 / r157407;
        double r157409 = r157408 - r157404;
        return r157409;
}
↓
double f(double x0, double x1) {
        double r157410 = x0;
        double r157411 = 3.0;
        double r157412 = pow(r157410, r157411);
        double r157413 = 1.0;
        double r157414 = 1.0;
        double r157415 = x1;
        double r157416 = r157414 - r157415;
        double r157417 = pow(r157416, r157411);
        double r157418 = r157413 / r157417;
        double r157419 = r157412 * r157418;
        double r157420 = r157419 - r157412;
        double r157421 = r157410 * r157410;
        double r157422 = r157410 / r157416;
        double r157423 = sqrt(r157411);
        double r157424 = pow(r157422, r157423);
        double r157425 = pow(r157424, r157423);
        double r157426 = r157412 + r157425;
        double r157427 = r157422 * r157422;
        double r157428 = r157410 - r157422;
        double r157429 = r157410 * r157428;
        double r157430 = r157427 + r157429;
        double r157431 = r157426 / r157430;
        double r157432 = r157422 * r157431;
        double r157433 = r157421 + r157432;
        double r157434 = r157420 / r157433;
        return r157434;
}

Error

Bits error versus x0

Bits error versus x1

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original7.9
Target0.3
Herbie5.5
\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

  1. Initial program 7.9

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

  3. Applied flip3--7.7

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

  4. Simplified7.7

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

  6. Applied div-inv7.4

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

  7. Applied unpow-prod-down6.5

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

  8. Simplified5.6

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

  10. Applied flip3-+5.6

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

  11. Simplified5.6

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

  13. Applied add-sqr-sqrt5.5

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

  14. Applied pow-unpow5.5

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

  15. Final simplification5.5

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

Reproduce

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

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

  (- (/ x0 (- 1.0 x1)) x0))