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

Average Error: 7.8 → 5.9

Time: 8.6s

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\]

↓

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

C

double f(double x0, double x1) {
        double r130225 = x0;
        double r130226 = 1.0;
        double r130227 = x1;
        double r130228 = r130226 - r130227;
        double r130229 = r130225 / r130228;
        double r130230 = r130229 - r130225;
        return r130230;
}

↓

double f(double x0, double x1) {
        double r130231 = x0;
        double r130232 = 1.0;
        double r130233 = r130232 * r130232;
        double r130234 = x1;
        double r130235 = r130234 * r130234;
        double r130236 = r130233 - r130235;
        double r130237 = r130231 / r130236;
        double r130238 = r130232 - r130234;
        double r130239 = r130231 / r130238;
        double r130240 = r130237 * r130239;
        double r130241 = r130232 + r130234;
        double r130242 = r130240 * r130241;
        double r130243 = r130239 + r130231;
        double r130244 = r130242 / r130243;
        double r130245 = r130231 * r130231;
        double r130246 = r130245 / r130243;
        double r130247 = r130244 - r130246;
        return r130247;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.8
Target	0.2
Herbie	5.9

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

Derivation

1. Initial program 7.8

   \[\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 flip-- 5.6

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

6. Applied associate-/r/ 6.1

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

8. Applied add-log-exp 6.1

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

9. Applied add-log-exp 6.1

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

10. Applied diff-log 5.8

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

11. Simplified 5.8

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

13. Applied distribute-rgt-in 6.3

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

14. Applied distribute-rgt-in 5.1

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

15. Applied associate--l+ 5.1

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

16. Final simplification 5.9

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

Reproduce

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