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

Average Error: 7.8 → 5.5

Time: 13.5s

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 r7990838 = x0;
        double r7990839 = 1.0;
        double r7990840 = x1;
        double r7990841 = r7990839 - r7990840;
        double r7990842 = r7990838 / r7990841;
        double r7990843 = r7990842 - r7990838;
        return r7990843;
}

↓

double f(double x0, double x1) {
        double r7990844 = x0;
        double r7990845 = r7990844 * r7990844;
        double r7990846 = r7990844 * r7990845;
        double r7990847 = 1.0;
        double r7990848 = x1;
        double r7990849 = r7990847 - r7990848;
        double r7990850 = r7990846 / r7990849;
        double r7990851 = r7990849 * r7990849;
        double r7990852 = r7990850 / r7990851;
        double r7990853 = r7990852 * r7990852;
        double r7990854 = r7990846 * r7990846;
        double r7990855 = r7990853 - r7990854;
        double r7990856 = log(r7990855);
        double r7990857 = exp(r7990856);
        double r7990858 = r7990852 + r7990846;
        double r7990859 = r7990857 / r7990858;
        double r7990860 = r7990844 / r7990849;
        double r7990861 = r7990860 * r7990860;
        double r7990862 = r7990844 * r7990860;
        double r7990863 = r7990862 + r7990845;
        double r7990864 = r7990861 + r7990863;
        double r7990865 = r7990859 / r7990864;
        return r7990865;
}

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