Average Error: 7.8 → 5.0
Time: 8.4s
Precision: 64
\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]
\[\frac{x0}{1 - x1} - x0\]
↓
\[\mathsf{fma}\left(\left(-\sqrt{x0}\right), \left(\sqrt{x0}\right), x0\right) + \frac{\frac{\left(1 + x1\right) \cdot x0}{1 - x1 \cdot x1} \cdot \frac{\left(1 + x1\right) \cdot x0}{1 - x1 \cdot x1} - x0 \cdot x0}{x0 + \frac{\left(1 + x1\right) \cdot x0}{1 - x1 \cdot x1}}\]
\frac{x0}{1 - x1} - x0
↓
\mathsf{fma}\left(\left(-\sqrt{x0}\right), \left(\sqrt{x0}\right), x0\right) + \frac{\frac{\left(1 + x1\right) \cdot x0}{1 - x1 \cdot x1} \cdot \frac{\left(1 + x1\right) \cdot x0}{1 - x1 \cdot x1} - x0 \cdot x0}{x0 + \frac{\left(1 + x1\right) \cdot x0}{1 - x1 \cdot x1}}
double f(double x0, double x1) {
        double r3135873 = x0;
        double r3135874 = 1.0;
        double r3135875 = x1;
        double r3135876 = r3135874 - r3135875;
        double r3135877 = r3135873 / r3135876;
        double r3135878 = r3135877 - r3135873;
        return r3135878;
}
↓
double f(double x0, double x1) {
        double r3135879 = x0;
        double r3135880 = sqrt(r3135879);
        double r3135881 = -r3135880;
        double r3135882 = fma(r3135881, r3135880, r3135879);
        double r3135883 = 1.0;
        double r3135884 = x1;
        double r3135885 = r3135883 + r3135884;
        double r3135886 = r3135885 * r3135879;
        double r3135887 = r3135884 * r3135884;
        double r3135888 = r3135883 - r3135887;
        double r3135889 = r3135886 / r3135888;
        double r3135890 = r3135889 * r3135889;
        double r3135891 = r3135879 * r3135879;
        double r3135892 = r3135890 - r3135891;
        double r3135893 = r3135879 + r3135889;
        double r3135894 = r3135892 / r3135893;
        double r3135895 = r3135882 + r3135894;
        return r3135895;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original7.8
Target0.3
Herbie5.0
\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

  1. Initial program 7.8

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

  3. Applied add-sqr-sqrt7.8

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

  4. Applied flip--7.6

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

  5. Applied associate-/r/8.1

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

  6. Applied prod-diff7.3

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

  7. Simplified5.6

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

  8. Simplified5.6

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

  10. Applied flip--5.0

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

  11. Final simplification5.0

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

Reproduce

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