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

Average Error: 7.9 → 5.5

Time: 26.2s

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

C

double f(double x0, double x1) {
        double r6624295 = x0;
        double r6624296 = 1.0;
        double r6624297 = x1;
        double r6624298 = r6624296 - r6624297;
        double r6624299 = r6624295 / r6624298;
        double r6624300 = r6624299 - r6624295;
        return r6624300;
}

↓

double f(double x0, double x1) {
        double r6624301 = x0;
        double r6624302 = r6624301 * r6624301;
        double r6624303 = r6624302 * r6624301;
        double r6624304 = 1.0;
        double r6624305 = x1;
        double r6624306 = r6624304 - r6624305;
        double r6624307 = r6624303 / r6624306;
        double r6624308 = r6624306 * r6624306;
        double r6624309 = r6624307 / r6624308;
        double r6624310 = r6624309 * r6624309;
        double r6624311 = r6624303 * r6624303;
        double r6624312 = r6624310 - r6624311;
        double r6624313 = log(r6624312);
        double r6624314 = exp(r6624313);
        double r6624315 = r6624303 + r6624309;
        double r6624316 = r6624314 / r6624315;
        double r6624317 = r6624301 / r6624306;
        double r6624318 = r6624317 * r6624317;
        double r6624319 = r6624301 * r6624317;
        double r6624320 = r6624302 + r6624319;
        double r6624321 = r6624318 + r6624320;
        double r6624322 = r6624316 / r6624321;
        return r6624322;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.3
Herbie	5.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. Simplified 7.3

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

6. Applied associate-*l/ 7.3

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

7. Applied frac-times 6.2

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

8. Simplified 6.0

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

10. Applied flip-- 5.9

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

12. Applied add-exp-log 5.5

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

13. Final simplification 5.5

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

Reproduce

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