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

Average Error: 7.9 → 5.5

Time: 11.0s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 1.855
  2. x1 = 0.0186

\[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 1.99445312499999971578290569595992565155:\\ \;\;\;\;\mathsf{fma}\left(\frac{\sqrt{x0}}{\sqrt{1} + \sqrt{x1}}, \frac{\sqrt{x0}}{\sqrt{1} - \sqrt{x1}}, -x0\right)\\ \mathbf{else}:\\ \;\;\;\;\sqrt[3]{{\left(\mathsf{fma}\left(\frac{{x0}^{\frac{2}{3}}}{\sqrt{1} + \sqrt{x1}}, \sqrt{\sqrt[3]{x0}} \cdot \frac{\sqrt{\sqrt[3]{x0}}}{\sqrt{1} - \sqrt{x1}}, -x0\right)\right)}^{3}}\\ \end{array}\]

C

double f(double x0, double x1) {
        double r142619 = x0;
        double r142620 = 1.0;
        double r142621 = x1;
        double r142622 = r142620 - r142621;
        double r142623 = r142619 / r142622;
        double r142624 = r142623 - r142619;
        return r142624;
}

↓

double f(double x0, double x1) {
        double r142625 = x0;
        double r142626 = 1.9944531249999997;
        bool r142627 = r142625 <= r142626;
        double r142628 = sqrt(r142625);
        double r142629 = 1.0;
        double r142630 = sqrt(r142629);
        double r142631 = x1;
        double r142632 = sqrt(r142631);
        double r142633 = r142630 + r142632;
        double r142634 = r142628 / r142633;
        double r142635 = r142630 - r142632;
        double r142636 = r142628 / r142635;
        double r142637 = -r142625;
        double r142638 = fma(r142634, r142636, r142637);
        double r142639 = 0.6666666666666666;
        double r142640 = pow(r142625, r142639);
        double r142641 = r142640 / r142633;
        double r142642 = cbrt(r142625);
        double r142643 = sqrt(r142642);
        double r142644 = r142643 / r142635;
        double r142645 = r142643 * r142644;
        double r142646 = fma(r142641, r142645, r142637);
        double r142647 = 3.0;
        double r142648 = pow(r142646, r142647);
        double r142649 = cbrt(r142648);
        double r142650 = r142627 ? r142638 : r142649;
        return r142650;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.3
Herbie	5.5

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

Derivation

1. Split input into 2 regimes

2. if x0 < 1.9944531249999997

   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 - \color{blue}{\sqrt{x1} \cdot \sqrt{x1}}} - x0\]

   4. Applied add-sqr-sqrt 7.4

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

   5. Applied difference-of-squares 7.4

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

   6. 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)} - x0\]

   7. Applied times-frac 7.4

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

   8. Applied fma-neg 5.3

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

   if 1.9944531249999997 < x0

   1. Initial program 8.3

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

   3. Applied add-sqr-sqrt 8.3

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

   4. Applied add-sqr-sqrt 8.3

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

   5. Applied difference-of-squares 8.3

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

   6. Applied add-cube-cbrt 8.3

      \[\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)} - x0\]

   7. Applied times-frac 8.1

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

   8. Applied fma-neg 6.9

      \[\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)}\]
   9. Using strategy rm

   10. Applied add-cbrt-cube 6.9

       \[\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)}}\]

   11. 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}}}\]
   12. Using strategy rm

   13. 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}}\]

   14. Applied add-sqr-sqrt 7.0

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

   15. Applied times-frac 5.7

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

   16. Simplified 5.7

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

4. Final simplification 5.5

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

Reproduce

herbie shell --seed 2019326 +o rules:numerics
(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))