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

Average Error: 7.8 → 6.1

Time: 9.8s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 1.855
  2. x1 = 0.0186

\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]

Math

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

↓

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

C

double f(double x0, double x1) {
        double r5319118 = x0;
        double r5319119 = 1.0;
        double r5319120 = x1;
        double r5319121 = r5319119 - r5319120;
        double r5319122 = r5319118 / r5319121;
        double r5319123 = r5319122 - r5319118;
        return r5319123;
}

↓

double f(double x0, double x1) {
        double r5319124 = x0;
        double r5319125 = 1.8749218749999998;
        bool r5319126 = r5319124 <= r5319125;
        double r5319127 = sqrt(r5319124);
        double r5319128 = x1;
        double r5319129 = sqrt(r5319128);
        double r5319130 = 1.0;
        double r5319131 = r5319129 + r5319130;
        double r5319132 = r5319127 / r5319131;
        double r5319133 = r5319130 - r5319129;
        double r5319134 = r5319127 / r5319133;
        double r5319135 = -r5319124;
        double r5319136 = fma(r5319132, r5319134, r5319135);
        double r5319137 = cbrt(r5319124);
        double r5319138 = r5319137 * r5319137;
        double r5319139 = r5319138 / r5319131;
        double r5319140 = r5319137 / r5319133;
        double r5319141 = fma(r5319139, r5319140, r5319135);
        double r5319142 = cbrt(r5319141);
        double r5319143 = r5319142 * r5319142;
        double r5319144 = r5319142 * r5319143;
        double r5319145 = r5319126 ? r5319136 : r5319144;
        return r5319145;
}

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

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

   3. Applied add-sqr-sqrt 7.3

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

   4. Applied *-un-lft-identity 7.3

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

   5. Applied difference-of-squares 7.3

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

   6. Applied add-sqr-sqrt 7.3

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

   7. Applied times-frac 7.3

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

   8. Applied fma-neg 5.2

      \[\leadsto \color{blue}{\mathsf{fma}\left(\left(\frac{\sqrt{x0}}{1 + \sqrt{x1}}\right), \left(\frac{\sqrt{x0}}{1 - \sqrt{x1}}\right), \left(-x0\right)\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 - \color{blue}{\sqrt{x1} \cdot \sqrt{x1}}} - x0\]

   4. Applied *-un-lft-identity 8.3

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

   5. Applied difference-of-squares 8.3

      \[\leadsto \frac{x0}{\color{blue}{\left(1 + \sqrt{x1}\right) \cdot \left(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(1 + \sqrt{x1}\right) \cdot \left(1 - \sqrt{x1}\right)} - x0\]

   7. Applied times-frac 8.2

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

   8. Applied fma-neg 7.0

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

   10. Applied add-cube-cbrt 7.0

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

4. Final simplification 6.1

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

Reproduce

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

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