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

Average Error: 7.9 → 5.6

Time: 11.1s

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\]

↓

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

C

double f(double x0, double x1) {
        double r175027 = x0;
        double r175028 = 1.0;
        double r175029 = x1;
        double r175030 = r175028 - r175029;
        double r175031 = r175027 / r175030;
        double r175032 = r175031 - r175027;
        return r175032;
}

↓

double f(double x0, double x1) {
        double r175033 = x0;
        double r175034 = 2.1482812499999993;
        bool r175035 = r175033 <= r175034;
        double r175036 = sqrt(r175033);
        double r175037 = 1.0;
        double r175038 = sqrt(r175037);
        double r175039 = x1;
        double r175040 = sqrt(r175039);
        double r175041 = r175038 + r175040;
        double r175042 = r175036 / r175041;
        double r175043 = r175038 - r175040;
        double r175044 = r175036 / r175043;
        double r175045 = -r175033;
        double r175046 = fma(r175042, r175044, r175045);
        double r175047 = r175045 + r175033;
        double r175048 = r175046 + r175047;
        double r175049 = 0.6666666666666666;
        double r175050 = pow(r175033, r175049);
        double r175051 = r175050 / r175041;
        double r175052 = cbrt(r175036);
        double r175053 = r175052 / r175043;
        double r175054 = r175052 * r175053;
        double r175055 = fma(r175051, r175054, r175045);
        double r175056 = 3.0;
        double r175057 = pow(r175055, r175056);
        double r175058 = cbrt(r175057);
        double r175059 = r175058 + r175047;
        double r175060 = r175035 ? r175048 : r175059;
        return r175060;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.2
Herbie	5.6

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

Derivation

1. Split input into 2 regimes

2. if x0 < 2.1482812499999993

   1. Initial program 7.4

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

   3. Applied add-sqr-sqrt 7.4

      \[\leadsto \frac{x0}{1 - x1} - \color{blue}{\sqrt{x0} \cdot \sqrt{x0}}\]

   4. Applied add-sqr-sqrt 7.4

      \[\leadsto \frac{x0}{1 - \color{blue}{\sqrt{x1} \cdot \sqrt{x1}}} - \sqrt{x0} \cdot \sqrt{x0}\]

   5. Applied add-sqr-sqrt 7.4

      \[\leadsto \frac{x0}{\color{blue}{\sqrt{1} \cdot \sqrt{1}} - \sqrt{x1} \cdot \sqrt{x1}} - \sqrt{x0} \cdot \sqrt{x0}\]

   6. Applied difference-of-squares 7.4

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

   7. Applied add-sqr-sqrt 7.4

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

   8. Applied times-frac 7.4

      \[\leadsto \color{blue}{\frac{\sqrt{x0}}{\sqrt{1} + \sqrt{x1}} \cdot \frac{\sqrt{x0}}{\sqrt{1} - \sqrt{x1}}} - \sqrt{x0} \cdot \sqrt{x0}\]

   9. Applied prod-diff 7.6

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

   10. Simplified 7.6

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

   11. Simplified 5.3

       \[\leadsto \mathsf{fma}\left(\frac{\sqrt{x0}}{\sqrt{1} + \sqrt{x1}}, \frac{\sqrt{x0}}{\sqrt{1} - \sqrt{x1}}, -x0\right) + \color{blue}{\left(\left(-x0\right) + x0\right)}\]

   if 2.1482812499999993 < x0

   1. Initial program 8.4

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

   3. Applied add-sqr-sqrt 8.4

      \[\leadsto \frac{x0}{1 - x1} - \color{blue}{\sqrt{x0} \cdot \sqrt{x0}}\]

   4. Applied add-sqr-sqrt 8.4

      \[\leadsto \frac{x0}{1 - \color{blue}{\sqrt{x1} \cdot \sqrt{x1}}} - \sqrt{x0} \cdot \sqrt{x0}\]

   5. Applied add-sqr-sqrt 8.4

      \[\leadsto \frac{x0}{\color{blue}{\sqrt{1} \cdot \sqrt{1}} - \sqrt{x1} \cdot \sqrt{x1}} - \sqrt{x0} \cdot \sqrt{x0}\]

   6. Applied difference-of-squares 8.4

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

   7. Applied add-cube-cbrt 8.4

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

   8. Applied times-frac 8.2

      \[\leadsto \color{blue}{\frac{\sqrt[3]{x0} \cdot \sqrt[3]{x0}}{\sqrt{1} + \sqrt{x1}} \cdot \frac{\sqrt[3]{x0}}{\sqrt{1} - \sqrt{x1}}} - \sqrt{x0} \cdot \sqrt{x0}\]

   9. Applied prod-diff 7.3

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

   10. Simplified 7.3

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

   11. Simplified 7.0

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

   13. Applied add-cbrt-cube 7.0

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

   14. Simplified 7.0

       \[\leadsto \sqrt[3]{\color{blue}{{\left(\mathsf{fma}\left(\frac{{x0}^{\frac{2}{3}}}{\sqrt{1} + \sqrt{x1}}, \frac{\sqrt[3]{x0}}{\sqrt{1} - \sqrt{x1}}, -x0\right)\right)}^{3}}} + \left(\left(-x0\right) + x0\right)\]
   15. Using strategy rm

   16. Applied *-un-lft-identity 7.0

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

   17. Applied add-sqr-sqrt 7.0

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

   18. Applied cbrt-prod 7.0

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

   19. Applied times-frac 5.8

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

   20. Simplified 5.8

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

4. Final simplification 5.6

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

Reproduce

herbie shell --seed 2019235 +o rules:numerics
(FPCore (x0 x1)
  :name "(- (/ x0 (- 1 x1)) x0)"
  :precision binary64
  :pre (or (and (== x0 1.855) (== x1 2.09000000000000012e-4)) (and (== x0 2.98499999999999988) (== x1 0.018599999999999998)))

  :herbie-target
  (/ (* x0 x1) (- 1 x1))

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