Average Error: 32.0 → 0
Time: 19.9s
Precision: 64
\[\frac{x}{x} - \frac{1.0}{x} \cdot \sqrt{x \cdot x}\]
↓
\[1 - \left(\left(\frac{1.0}{x} \cdot \left|x\right|\right)\right)\]
\frac{x}{x} - \frac{1.0}{x} \cdot \sqrt{x \cdot x}
↓
1 - \left(\left(\frac{1.0}{x} \cdot \left|x\right|\right)\right)
double f(double x) {
        double r4440515 = x;
        double r4440516 = r4440515 / r4440515;
        double r4440517 = 1.0;
        double r4440518 = r4440517 / r4440515;
        double r4440519 = r4440515 * r4440515;
        double r4440520 = sqrt(r4440519);
        double r4440521 = r4440518 * r4440520;
        double r4440522 = r4440516 - r4440521;
        return r4440522;
}
↓
double f(double x) {
        double r4440523 = 1.0;
        double r4440524 = 1.0;
        double r4440525 = x;
        double r4440526 = r4440524 / r4440525;
        double r4440527 = fabs(r4440525);
        double r4440528 = r4440526 * r4440527;
        double r4440529 = /* ERROR: no posit support in C */;
        double r4440530 = /* ERROR: no posit support in C */;
        double r4440531 = r4440523 - r4440530;
        return r4440531;
}

Error

Bits error versus x

Target

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

Derivation

  1. Initial program 32.0

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

  2. Simplified4.6

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

  4. Applied insert-posit160

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

  5. Final simplification0

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

Reproduce

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

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

  (- (/ x x) (* (/ 1.0 x) (sqrt (* x x)))))