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

Average Error: 7.8 → 4.5

Time: 8.9s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 2.985
  2. x1 = 0.000209

\[x0 = 1.854999999999999982236431605997495353222 \land x1 = 2.090000000000000115064208161541614572343 \cdot 10^{-4} \lor x0 = 2.984999999999999875655021241982467472553 \land x1 = 0.01859999999999999847899445626353553961962\]

Math

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

↓

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

C

double f(double x0, double x1) {
        double r155872 = x0;
        double r155873 = 1.0;
        double r155874 = x1;
        double r155875 = r155873 - r155874;
        double r155876 = r155872 / r155875;
        double r155877 = r155876 - r155872;
        return r155877;
}

↓

double f(double x0, double x1) {
        double r155878 = x0;
        double r155879 = 3.0;
        double r155880 = pow(r155878, r155879);
        double r155881 = 1.0;
        double r155882 = x1;
        double r155883 = r155881 - r155882;
        double r155884 = 6.0;
        double r155885 = pow(r155883, r155884);
        double r155886 = r155880 / r155885;
        double r155887 = r155886 - r155880;
        double r155888 = exp(r155887);
        double r155889 = log(r155888);
        double r155890 = r155883 * r155883;
        double r155891 = r155878 / r155890;
        double r155892 = r155891 + r155878;
        double r155893 = r155892 * r155891;
        double r155894 = r155878 * r155878;
        double r155895 = r155893 + r155894;
        double r155896 = r155889 / r155895;
        double r155897 = r155878 * r155896;
        double r155898 = r155878 / r155883;
        double r155899 = r155898 + r155878;
        double r155900 = r155897 / r155899;
        return r155900;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.8
Target	0.2
Herbie	4.5

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

Derivation

1. Initial program 7.8

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

3. Applied div-inv 7.6

   \[\leadsto \color{blue}{x0 \cdot \frac{1}{1 - x1}} - x0\]
4. Using strategy rm

5. Applied flip-- 6.0

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

6. Simplified 6.9

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

7. Simplified 6.9

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

9. Applied flip3-- 6.6

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

10. Simplified 4.9

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

11. Simplified 4.9

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

13. Applied add-log-exp 4.9

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

14. Applied add-log-exp 4.9

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

15. Applied diff-log 4.6

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

16. Simplified 4.5

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

17. Final simplification 4.5

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

Reproduce

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