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

Average Error: 7.9 → 5.3

Time: 10.0s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 1.855
  2. x1 = 0.0186

\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]

Math

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

↓

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

C

double f(double x0, double x1) {
        double r4820333 = x0;
        double r4820334 = 1.0;
        double r4820335 = x1;
        double r4820336 = r4820334 - r4820335;
        double r4820337 = r4820333 / r4820336;
        double r4820338 = r4820337 - r4820333;
        return r4820338;
}

↓

double f(double x0, double x1) {
        double r4820339 = 1.0;
        double r4820340 = x1;
        double r4820341 = r4820339 - r4820340;
        double r4820342 = r4820339 / r4820341;
        double r4820343 = x0;
        double r4820344 = r4820342 * r4820343;
        double r4820345 = r4820343 / r4820341;
        double r4820346 = r4820344 * r4820345;
        double r4820347 = r4820346 * r4820346;
        double r4820348 = r4820343 * r4820343;
        double r4820349 = r4820348 * r4820348;
        double r4820350 = r4820347 - r4820349;
        double r4820351 = r4820348 + r4820346;
        double r4820352 = r4820350 / r4820351;
        double r4820353 = cbrt(r4820345);
        double r4820354 = r4820353 * r4820353;
        double r4820355 = r4820354 * r4820353;
        double r4820356 = r4820355 + r4820343;
        double r4820357 = r4820352 / r4820356;
        return r4820357;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.3
Herbie	5.3

\[\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. Using strategy rm

5. Applied div-inv 5.6

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

7. Applied flip-- 5.6

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

9. Applied add-cube-cbrt 5.3

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

10. Final simplification 5.3

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

Reproduce

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

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