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

Average Error: 7.9 → 5.3

Time: 11.5s

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 r6676469 = x0;
        double r6676470 = 1.0;
        double r6676471 = x1;
        double r6676472 = r6676470 - r6676471;
        double r6676473 = r6676469 / r6676472;
        double r6676474 = r6676473 - r6676469;
        return r6676474;
}

↓

double f(double x0, double x1) {
        double r6676475 = 1.0;
        double r6676476 = x1;
        double r6676477 = r6676475 - r6676476;
        double r6676478 = r6676475 / r6676477;
        double r6676479 = x0;
        double r6676480 = r6676478 * r6676479;
        double r6676481 = r6676479 / r6676477;
        double r6676482 = r6676480 * r6676481;
        double r6676483 = r6676482 * r6676482;
        double r6676484 = r6676479 * r6676479;
        double r6676485 = r6676484 * r6676484;
        double r6676486 = r6676483 - r6676485;
        double r6676487 = r6676484 + r6676482;
        double r6676488 = r6676486 / r6676487;
        double r6676489 = cbrt(r6676481);
        double r6676490 = r6676489 * r6676489;
        double r6676491 = r6676490 * r6676489;
        double r6676492 = r6676491 + r6676479;
        double r6676493 = r6676488 / r6676492;
        return r6676493;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.2
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 2019142 
(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))