Average Error: 7.8 → 4.6
Time: 26.3s
Precision: 64
\[\frac{x0}{1 - x1} - x0\]
↓
\[\frac{\log \left(e^{\left(\frac{1}{1 - x1} \cdot x0\right) \cdot \frac{x0}{1 - x1} - x0 \cdot x0}\right)}{x0 + \frac{x0}{1 - x1}}\]
double f(double x0, double x1) {
        double r20998381 = x0;
        double r20998382 = 1.0;
        double r20998383 = x1;
        double r20998384 = r20998382 - r20998383;
        double r20998385 = r20998381 / r20998384;
        double r20998386 = r20998385 - r20998381;
        return r20998386;
}
↓
double f(double x0, double x1) {
        double r20998387 = 1.0;
        double r20998388 = x1;
        double r20998389 = r20998387 - r20998388;
        double r20998390 = r20998387 / r20998389;
        double r20998391 = x0;
        double r20998392 = r20998390 * r20998391;
        double r20998393 = r20998391 / r20998389;
        double r20998394 = r20998392 * r20998393;
        double r20998395 = r20998391 * r20998391;
        double r20998396 = r20998394 - r20998395;
        double r20998397 = exp(r20998396);
        double r20998398 = log(r20998397);
        double r20998399 = r20998391 + r20998393;
        double r20998400 = r20998398 / r20998399;
        return r20998400;
}


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

Error

Bits error versus x0

Bits error versus x1

Target

Original7.8
Target0.2
Herbie4.6
\[\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.2

    \[\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-inv5.6

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

  7. Applied add-log-exp4.6

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

  8. Final simplification4.6

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

Reproduce

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