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

Average Error: 7.9 → 3.2

Time: 6.3s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 2.985
  2. x1 = 0.000209

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

Math

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

↓

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

C

double f(double x0, double x1) {
        double r152490 = x0;
        double r152491 = 1.0;
        double r152492 = x1;
        double r152493 = r152491 - r152492;
        double r152494 = r152490 / r152493;
        double r152495 = r152494 - r152490;
        return r152495;
}

↓

double f(double x0, double x1) {
        double r152496 = x0;
        double r152497 = 2.0;
        double r152498 = r152496 * r152497;
        double r152499 = 1.0;
        double r152500 = x1;
        double r152501 = r152499 - r152500;
        double r152502 = r152501 * r152501;
        double r152503 = r152496 / r152502;
        double r152504 = r152496 + r152503;
        double r152505 = r152503 * r152504;
        double r152506 = r152496 * r152496;
        double r152507 = r152505 + r152506;
        double r152508 = r152498 / r152507;
        double r152509 = 3.0;
        double r152510 = pow(r152503, r152509);
        double r152511 = pow(r152496, r152509);
        double r152512 = r152510 - r152511;
        double r152513 = exp(r152512);
        double r152514 = sqrt(r152513);
        double r152515 = log(r152514);
        double r152516 = r152496 / r152501;
        double r152517 = r152516 + r152496;
        double r152518 = r152515 / r152517;
        double r152519 = r152508 * r152518;
        return r152519;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.3
Herbie	3.2

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

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

11. Applied diff-log 4.6

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

12. Simplified 4.6

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

15. Applied log-prod 3.3

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

16. Final simplification 3.2

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

Reproduce

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