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

Average Error: 7.8 → 6.1

Time: 7.2s

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 1.874921874999999849009668650978710502386:\\ \;\;\;\;\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}}, \frac{\sqrt[3]{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 r190777 = x0;
        double r190778 = 1.0;
        double r190779 = x1;
        double r190780 = r190778 - r190779;
        double r190781 = r190777 / r190780;
        double r190782 = r190781 - r190777;
        return r190782;
}

↓

double f(double x0, double x1) {
        double r190783 = x0;
        double r190784 = 1.8749218749999998;
        bool r190785 = r190783 <= r190784;
        double r190786 = sqrt(r190783);
        double r190787 = 1.0;
        double r190788 = sqrt(r190787);
        double r190789 = x1;
        double r190790 = sqrt(r190789);
        double r190791 = r190788 + r190790;
        double r190792 = r190786 / r190791;
        double r190793 = r190788 - r190790;
        double r190794 = r190786 / r190793;
        double r190795 = -r190783;
        double r190796 = fma(r190792, r190794, r190795);
        double r190797 = r190795 + r190783;
        double r190798 = r190796 + r190797;
        double r190799 = 0.6666666666666666;
        double r190800 = pow(r190783, r190799);
        double r190801 = r190800 / r190791;
        double r190802 = cbrt(r190783);
        double r190803 = r190802 / r190793;
        double r190804 = fma(r190801, r190803, r190795);
        double r190805 = 3.0;
        double r190806 = pow(r190804, r190805);
        double r190807 = cbrt(r190806);
        double r190808 = r190807 + r190797;
        double r190809 = r190785 ? r190798 : r190808;
        return r190809;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.8
Target	0.3
Herbie	6.1

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

Derivation

1. Split input into 2 regimes

2. if x0 < 1.8749218749999998

   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.5

      \[\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.5

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

   4. Applied add-sqr-sqrt 8.3

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

   5. Applied add-sqr-sqrt 8.3

      \[\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.3

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

      \[\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.2

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

       \[\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)\]
3. Recombined 2 regimes into one program.

4. Final simplification 6.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;x0 \le 1.874921874999999849009668650978710502386:\\ \;\;\;\;\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}}, \frac{\sqrt[3]{x0}}{\sqrt{1} - \sqrt{x1}}, -x0\right)\right)}^{3}} + \left(\left(-x0\right) + x0\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019209 +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))