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

Average Error: 8.0 → 6.2

Time: 28.3s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 1.855
  2. x1 = 0.0186

\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]

Math

\[\frac{x0}{1.0 - x1} - x0\]

↓

\[\frac{\frac{\left(\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1}\right) \cdot x0}{1.0 - x1} - x0 \cdot \left(x0 \cdot x0\right)}{\sqrt[3]{\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1} + \left(\sqrt[3]{\frac{x0}{1.0 - x1} \cdot \left(\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1}\right)} \cdot x0 + x0 \cdot x0\right)} \cdot \left(\sqrt[3]{\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1} + \left(\sqrt[3]{\frac{x0}{1.0 - x1} \cdot \left(\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1}\right)} \cdot x0 + x0 \cdot x0\right)} \cdot \sqrt[3]{\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1} + \left(\sqrt[3]{\frac{x0}{1.0 - x1} \cdot \left(\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1}\right)} \cdot x0 + x0 \cdot x0\right)}\right)}\]

C

double f(double x0, double x1) {
        double r7003748 = x0;
        double r7003749 = 1.0;
        double r7003750 = x1;
        double r7003751 = r7003749 - r7003750;
        double r7003752 = r7003748 / r7003751;
        double r7003753 = r7003752 - r7003748;
        return r7003753;
}

↓

double f(double x0, double x1) {
        double r7003754 = x0;
        double r7003755 = 1.0;
        double r7003756 = x1;
        double r7003757 = r7003755 - r7003756;
        double r7003758 = r7003754 / r7003757;
        double r7003759 = r7003758 * r7003758;
        double r7003760 = r7003759 * r7003754;
        double r7003761 = r7003760 / r7003757;
        double r7003762 = r7003754 * r7003754;
        double r7003763 = r7003754 * r7003762;
        double r7003764 = r7003761 - r7003763;
        double r7003765 = r7003758 * r7003759;
        double r7003766 = cbrt(r7003765);
        double r7003767 = r7003766 * r7003754;
        double r7003768 = r7003767 + r7003762;
        double r7003769 = r7003759 + r7003768;
        double r7003770 = cbrt(r7003769);
        double r7003771 = r7003770 * r7003770;
        double r7003772 = r7003770 * r7003771;
        double r7003773 = r7003764 / r7003772;
        return r7003773;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	8.0
Target	0.2
Herbie	6.2

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

Derivation

1. Initial program 8.0

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

3. Applied flip3-- 7.8

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

4. Simplified 7.4

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

6. Applied associate-*l/ 7.4

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

7. Applied associate-*l/ 6.7

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

8. Simplified 6.2

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

10. Applied add-cbrt-cube 6.2

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

11. Applied add-cbrt-cube 6.2

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

12. Applied cbrt-undiv 6.2

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

13. Simplified 6.2

    \[\leadsto \frac{\frac{x0 \cdot \left(\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1}\right)}{1.0 - x1} - x0 \cdot \left(x0 \cdot x0\right)}{\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1} + \left(x0 \cdot x0 + \sqrt[3]{\color{blue}{\frac{x0}{1.0 - x1} \cdot \left(\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1}\right)}} \cdot x0\right)}\]
14. Using strategy rm

15. Applied add-cube-cbrt 6.2

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

16. Final simplification 6.2

    \[\leadsto \frac{\frac{\left(\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1}\right) \cdot x0}{1.0 - x1} - x0 \cdot \left(x0 \cdot x0\right)}{\sqrt[3]{\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1} + \left(\sqrt[3]{\frac{x0}{1.0 - x1} \cdot \left(\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1}\right)} \cdot x0 + x0 \cdot x0\right)} \cdot \left(\sqrt[3]{\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1} + \left(\sqrt[3]{\frac{x0}{1.0 - x1} \cdot \left(\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1}\right)} \cdot x0 + x0 \cdot x0\right)} \cdot \sqrt[3]{\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1} + \left(\sqrt[3]{\frac{x0}{1.0 - x1} \cdot \left(\frac{x0}{1.0 - x1} \cdot \frac{x0}{1.0 - x1}\right)} \cdot x0 + x0 \cdot x0\right)}\right)}\]

Reproduce

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