sqrt sqr

Average Error: 32.6 → 0

Time: 5.7s

Precision: 64

Math

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

↓

\[1 - \frac{1 \cdot \left|x\right|}{x}\]

C

double f(double x) {
        double r97925 = x;
        double r97926 = r97925 / r97925;
        double r97927 = 1.0;
        double r97928 = r97927 / r97925;
        double r97929 = r97925 * r97925;
        double r97930 = sqrt(r97929);
        double r97931 = r97928 * r97930;
        double r97932 = r97926 - r97931;
        return r97932;
}

↓

double f(double x) {
        double r97933 = 1.0;
        double r97934 = 1.0;
        double r97935 = x;
        double r97936 = fabs(r97935);
        double r97937 = r97934 * r97936;
        double r97938 = r97937 / r97935;
        double r97939 = r97933 - r97938;
        return r97939;
}

Error

Bits error versus x

Target

Original	32.6
Target	0
Herbie	0

\[\begin{array}{l} \mathbf{if}\;x \lt 0.0:\\ \;\;\;\;2\\ \mathbf{else}:\\ \;\;\;\;0.0\\ \end{array}\]

Derivation

1. Initial program 32.6

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

2. Simplified 5.0

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

4. Applied pow1 5.0

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

5. Applied pow1 5.0

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

6. Applied pow-prod-down 5.0

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

7. Simplified 0

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

8. Final simplification 0

   \[\leadsto 1 - \frac{1 \cdot \left|x\right|}{x}\]

Reproduce

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