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

Average Error: 7.8 → 4.0

Time: 3.4s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 1.855
  2. x1 = 0.0186

\[x0 = 1.855 \land x1 = 2.09000000000000012 \cdot 10^{-4} \lor x0 = 2.98499999999999988 \land x1 = 0.018599999999999998\]

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;1 - x1 \le 0.99059549999999996:\\ \;\;\;\;\frac{\frac{\left(\left(\left(x0 \cdot x0\right) \cdot x0\right) \cdot \frac{1}{\left(\left(1 - x1\right) \cdot \left(1 - x1\right)\right) \cdot \left(1 - x1\right)}\right) \cdot \left(\left(\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right) - {\left(x0 \cdot x0\right)}^{3}}{\frac{x0}{1 - x1} \cdot \left({\left(\frac{x0}{1 - x1}\right)}^{3} + \frac{{x0}^{3}}{1 - x1}\right) + {x0}^{4}}}{\frac{x0}{1 - x1} + x0}\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\left(\sqrt[3]{\frac{x0}{1 - x1} + x0} \cdot \sqrt[3]{\frac{x0}{1 - x1} + x0}\right) \cdot \sqrt[3]{\frac{x0}{1 - x1} + x0}}\\ \end{array}\]

C

double f(double x0, double x1) {
        double r207945 = x0;
        double r207946 = 1.0;
        double r207947 = x1;
        double r207948 = r207946 - r207947;
        double r207949 = r207945 / r207948;
        double r207950 = r207949 - r207945;
        return r207950;
}

↓

double f(double x0, double x1) {
        double r207951 = 1.0;
        double r207952 = x1;
        double r207953 = r207951 - r207952;
        double r207954 = 0.9905955;
        bool r207955 = r207953 <= r207954;
        double r207956 = x0;
        double r207957 = r207956 * r207956;
        double r207958 = r207957 * r207956;
        double r207959 = 1.0;
        double r207960 = r207953 * r207953;
        double r207961 = r207960 * r207953;
        double r207962 = r207959 / r207961;
        double r207963 = r207958 * r207962;
        double r207964 = r207956 / r207953;
        double r207965 = r207964 * r207964;
        double r207966 = r207965 * r207964;
        double r207967 = r207963 * r207966;
        double r207968 = 3.0;
        double r207969 = pow(r207957, r207968);
        double r207970 = r207967 - r207969;
        double r207971 = pow(r207964, r207968);
        double r207972 = pow(r207956, r207968);
        double r207973 = r207972 / r207953;
        double r207974 = r207971 + r207973;
        double r207975 = r207964 * r207974;
        double r207976 = 4.0;
        double r207977 = pow(r207956, r207976);
        double r207978 = r207975 + r207977;
        double r207979 = r207970 / r207978;
        double r207980 = r207964 + r207956;
        double r207981 = r207979 / r207980;
        double r207982 = r207959 / r207953;
        double r207983 = r207956 * r207982;
        double r207984 = r207983 * r207964;
        double r207985 = r207984 - r207957;
        double r207986 = cbrt(r207980);
        double r207987 = r207986 * r207986;
        double r207988 = r207987 * r207986;
        double r207989 = r207985 / r207988;
        double r207990 = r207955 ? r207981 : r207989;
        return r207990;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.8
Target	0.2
Herbie	4.0

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

Derivation

1. Split input into 2 regimes

2. if (- 1.0 x1) < 0.9905955

   1. Initial program 4.5

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

   3. Applied flip-- 3.2

      \[\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 3.2

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

   7. Applied flip3-- 3.3

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

   8. Simplified 3.4

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

   10. Applied add-cbrt-cube 4.1

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

   11. Applied add-cbrt-cube 4.1

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

   12. Applied add-cbrt-cube 4.1

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

   13. Applied cbrt-undiv 4.5

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

   14. Applied add-cbrt-cube 4.1

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

   15. Applied cbrt-unprod 4.6

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

   16. Applied cbrt-unprod 4.1

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

   17. Applied rem-cube-cbrt 0

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

   if 0.9905955 < (- 1.0 x1)

   1. Initial program 11.2

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

   3. Applied flip-- 11.4

      \[\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 8.1

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

   7. Applied add-cube-cbrt 8.0

      \[\leadsto \frac{\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\color{blue}{\left(\sqrt[3]{\frac{x0}{1 - x1} + x0} \cdot \sqrt[3]{\frac{x0}{1 - x1} + x0}\right) \cdot \sqrt[3]{\frac{x0}{1 - x1} + x0}}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 4.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;1 - x1 \le 0.99059549999999996:\\ \;\;\;\;\frac{\frac{\left(\left(\left(x0 \cdot x0\right) \cdot x0\right) \cdot \frac{1}{\left(\left(1 - x1\right) \cdot \left(1 - x1\right)\right) \cdot \left(1 - x1\right)}\right) \cdot \left(\left(\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right) - {\left(x0 \cdot x0\right)}^{3}}{\frac{x0}{1 - x1} \cdot \left({\left(\frac{x0}{1 - x1}\right)}^{3} + \frac{{x0}^{3}}{1 - x1}\right) + {x0}^{4}}}{\frac{x0}{1 - x1} + x0}\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\left(\sqrt[3]{\frac{x0}{1 - x1} + x0} \cdot \sqrt[3]{\frac{x0}{1 - x1} + x0}\right) \cdot \sqrt[3]{\frac{x0}{1 - x1} + x0}}\\ \end{array}\]

Reproduce

herbie shell --seed 2020056 
(FPCore (x0 x1)
  :name "(- (/ x0 (- 1 x1)) x0)"
  :precision binary64
  :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))