Average Error: 32.4 → 0
Time: 1.7s
Precision: 64
\[\frac{x}{x} - \frac{1}{x} \cdot \sqrt{x \cdot x}\]
↓
\[\frac{1 - {\left(1 \cdot \frac{\left|x\right|}{x}\right)}^{3}}{\left(1 \cdot \frac{\left|x\right|}{x}\right) \cdot \mathsf{fma}\left(1, \frac{\left|x\right|}{x}, 1\right) + 1}\]
\frac{x}{x} - \frac{1}{x} \cdot \sqrt{x \cdot x}
↓
\frac{1 - {\left(1 \cdot \frac{\left|x\right|}{x}\right)}^{3}}{\left(1 \cdot \frac{\left|x\right|}{x}\right) \cdot \mathsf{fma}\left(1, \frac{\left|x\right|}{x}, 1\right) + 1}
double f(double x) {
        double r217891 = x;
        double r217892 = r217891 / r217891;
        double r217893 = 1.0;
        double r217894 = r217893 / r217891;
        double r217895 = r217891 * r217891;
        double r217896 = sqrt(r217895);
        double r217897 = r217894 * r217896;
        double r217898 = r217892 - r217897;
        return r217898;
}
↓
double f(double x) {
        double r217899 = 1.0;
        double r217900 = 1.0;
        double r217901 = x;
        double r217902 = fabs(r217901);
        double r217903 = r217902 / r217901;
        double r217904 = r217900 * r217903;
        double r217905 = 3.0;
        double r217906 = pow(r217904, r217905);
        double r217907 = r217899 - r217906;
        double r217908 = fma(r217900, r217903, r217899);
        double r217909 = r217904 * r217908;
        double r217910 = r217909 + r217899;
        double r217911 = r217907 / r217910;
        return r217911;
}

Error

Bits error versus x

Target

Original32.4
Target0
Herbie0
\[\begin{array}{l} \mathbf{if}\;x \lt 0.0:\\ \;\;\;\;2\\ \mathbf{else}:\\ \;\;\;\;0.0\\ \end{array}\]

Derivation

  1. Initial program 32.4

    \[\frac{x}{x} - \frac{1}{x} \cdot \sqrt{x \cdot x}\]

  2. Simplified31.3

    \[\leadsto \color{blue}{\mathsf{fma}\left(-\frac{1}{x}, \left|x\right|, 1\right)}\]
  3. Using strategy rm

  4. Applied fma-udef4.8

    \[\leadsto \color{blue}{\left(-\frac{1}{x}\right) \cdot \left|x\right| + 1}\]
  5. Using strategy rm

  6. Applied flip3-+4.9

    \[\leadsto \color{blue}{\frac{{\left(\left(-\frac{1}{x}\right) \cdot \left|x\right|\right)}^{3} + {1}^{3}}{\left(\left(-\frac{1}{x}\right) \cdot \left|x\right|\right) \cdot \left(\left(-\frac{1}{x}\right) \cdot \left|x\right|\right) + \left(1 \cdot 1 - \left(\left(-\frac{1}{x}\right) \cdot \left|x\right|\right) \cdot 1\right)}}\]

  7. Simplified0.1

    \[\leadsto \frac{\color{blue}{1 - {\left(1 \cdot \frac{\left|x\right|}{x}\right)}^{3}}}{\left(\left(-\frac{1}{x}\right) \cdot \left|x\right|\right) \cdot \left(\left(-\frac{1}{x}\right) \cdot \left|x\right|\right) + \left(1 \cdot 1 - \left(\left(-\frac{1}{x}\right) \cdot \left|x\right|\right) \cdot 1\right)}\]

  8. Simplified0

    \[\leadsto \frac{1 - {\left(1 \cdot \frac{\left|x\right|}{x}\right)}^{3}}{\color{blue}{\left(1 \cdot \frac{\left|x\right|}{x}\right) \cdot \mathsf{fma}\left(1, \frac{\left|x\right|}{x}, 1\right) + 1}}\]

  9. Final simplification0

    \[\leadsto \frac{1 - {\left(1 \cdot \frac{\left|x\right|}{x}\right)}^{3}}{\left(1 \cdot \frac{\left|x\right|}{x}\right) \cdot \mathsf{fma}\left(1, \frac{\left|x\right|}{x}, 1\right) + 1}\]

Reproduce

herbie shell --seed 2019353 +o rules:numerics
(FPCore (x)
  :name "sqrt sqr"
  :precision binary64

  :herbie-target
  (if (< x 0.0) 2 0.0)

  (- (/ x x) (* (/ 1 x) (sqrt (* x x)))))