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

Average Error: 7.8 → 5.5

Time: 12.4s

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

C

double f(double x0, double x1) {
        double r7643864 = x0;
        double r7643865 = 1.0;
        double r7643866 = x1;
        double r7643867 = r7643865 - r7643866;
        double r7643868 = r7643864 / r7643867;
        double r7643869 = r7643868 - r7643864;
        return r7643869;
}

↓

double f(double x0, double x1) {
        double r7643870 = x0;
        double r7643871 = r7643870 * r7643870;
        double r7643872 = r7643870 * r7643871;
        double r7643873 = 1.0;
        double r7643874 = x1;
        double r7643875 = r7643873 - r7643874;
        double r7643876 = r7643872 / r7643875;
        double r7643877 = r7643875 * r7643875;
        double r7643878 = r7643876 / r7643877;
        double r7643879 = r7643878 * r7643878;
        double r7643880 = r7643872 * r7643872;
        double r7643881 = r7643879 - r7643880;
        double r7643882 = log(r7643881);
        double r7643883 = exp(r7643882);
        double r7643884 = r7643878 + r7643872;
        double r7643885 = r7643883 / r7643884;
        double r7643886 = r7643870 / r7643875;
        double r7643887 = r7643886 * r7643886;
        double r7643888 = r7643870 * r7643886;
        double r7643889 = r7643888 + r7643871;
        double r7643890 = r7643887 + r7643889;
        double r7643891 = r7643885 / r7643890;
        return r7643891;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.8
Target	0.3
Herbie	5.5

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

Derivation

1. Initial program 7.8

   \[\frac{x0}{1 - x1} - x0\]
2. Using strategy rm

3. Applied flip3-- 7.6

   \[\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.2

   \[\leadsto \frac{\color{blue}{\frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} \cdot \frac{x0}{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)}\]
5. Using strategy rm

6. Applied associate-*l/ 7.2

   \[\leadsto \frac{\frac{x0}{1 - x1} \cdot \color{blue}{\frac{x0 \cdot \frac{x0}{1 - x1}}{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{x0 \cdot \left(x0 \cdot \frac{x0}{1 - x1}\right)}{\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{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 \frac{x0}{1 - x1} + x0 \cdot x0\right)}\]

Reproduce

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