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

Average Error: 7.9 → 5.3

Time: 10.3s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 2.985
  2. x1 = 0.000209

\[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 r5289146 = x0;
        double r5289147 = 1.0;
        double r5289148 = x1;
        double r5289149 = r5289147 - r5289148;
        double r5289150 = r5289146 / r5289149;
        double r5289151 = r5289150 - r5289146;
        return r5289151;
}

↓

double f(double x0, double x1) {
        double r5289152 = 1.0;
        double r5289153 = x1;
        double r5289154 = r5289152 - r5289153;
        double r5289155 = r5289152 / r5289154;
        double r5289156 = x0;
        double r5289157 = r5289155 * r5289156;
        double r5289158 = r5289156 / r5289154;
        double r5289159 = r5289157 * r5289158;
        double r5289160 = r5289159 * r5289159;
        double r5289161 = r5289156 * r5289156;
        double r5289162 = r5289161 * r5289161;
        double r5289163 = r5289160 - r5289162;
        double r5289164 = r5289161 + r5289159;
        double r5289165 = r5289163 / r5289164;
        double r5289166 = cbrt(r5289158);
        double r5289167 = r5289166 * r5289166;
        double r5289168 = r5289167 * r5289166;
        double r5289169 = r5289168 + r5289156;
        double r5289170 = r5289165 / r5289169;
        return r5289170;
}

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 2019144 
(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))