Average Error: 20.1 → 20.5
Time: 20.7s
Precision: 64
\[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
↓
\[\mathsf{fma}\left(\frac{1}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}}, \frac{1}{\sqrt{\sqrt[3]{x}}}, \frac{1}{\sqrt{\sqrt[3]{1 + x} \cdot \sqrt[3]{1 + x}}} \cdot \frac{-1}{\sqrt{\sqrt[3]{1 + x}}}\right) + \mathsf{fma}\left(\frac{-1}{\sqrt{\sqrt[3]{1 + x}}}, \frac{1}{\sqrt{\sqrt[3]{1 + x} \cdot \sqrt[3]{1 + x}}}, \frac{1}{\sqrt{\sqrt[3]{1 + x} \cdot \sqrt[3]{1 + x}}} \cdot \frac{1}{\sqrt{\sqrt[3]{1 + x}}}\right)\]
\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}
↓
\mathsf{fma}\left(\frac{1}{\sqrt{\sqrt[3]{x} \cdot \sqrt[3]{x}}}, \frac{1}{\sqrt{\sqrt[3]{x}}}, \frac{1}{\sqrt{\sqrt[3]{1 + x} \cdot \sqrt[3]{1 + x}}} \cdot \frac{-1}{\sqrt{\sqrt[3]{1 + x}}}\right) + \mathsf{fma}\left(\frac{-1}{\sqrt{\sqrt[3]{1 + x}}}, \frac{1}{\sqrt{\sqrt[3]{1 + x} \cdot \sqrt[3]{1 + x}}}, \frac{1}{\sqrt{\sqrt[3]{1 + x} \cdot \sqrt[3]{1 + x}}} \cdot \frac{1}{\sqrt{\sqrt[3]{1 + x}}}\right)
double f(double x) {
        double r4505082 = 1.0;
        double r4505083 = x;
        double r4505084 = sqrt(r4505083);
        double r4505085 = r4505082 / r4505084;
        double r4505086 = r4505083 + r4505082;
        double r4505087 = sqrt(r4505086);
        double r4505088 = r4505082 / r4505087;
        double r4505089 = r4505085 - r4505088;
        return r4505089;
}
↓
double f(double x) {
        double r4505090 = 1.0;
        double r4505091 = x;
        double r4505092 = cbrt(r4505091);
        double r4505093 = r4505092 * r4505092;
        double r4505094 = sqrt(r4505093);
        double r4505095 = r4505090 / r4505094;
        double r4505096 = sqrt(r4505092);
        double r4505097 = r4505090 / r4505096;
        double r4505098 = r4505090 + r4505091;
        double r4505099 = cbrt(r4505098);
        double r4505100 = r4505099 * r4505099;
        double r4505101 = sqrt(r4505100);
        double r4505102 = r4505090 / r4505101;
        double r4505103 = -1.0;
        double r4505104 = sqrt(r4505099);
        double r4505105 = r4505103 / r4505104;
        double r4505106 = r4505102 * r4505105;
        double r4505107 = fma(r4505095, r4505097, r4505106);
        double r4505108 = r4505090 / r4505104;
        double r4505109 = r4505102 * r4505108;
        double r4505110 = fma(r4505105, r4505102, r4505109);
        double r4505111 = r4505107 + r4505110;
        return r4505111;
}

Error

Bits error versus x

Target

Original20.1
Target0.6
Herbie20.5
\[\frac{1}{\left(x + 1\right) \cdot \sqrt{x} + x \cdot \sqrt{x + 1}}\]

Derivation

  1. Initial program 20.1

    \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
  2. Using strategy rm

  3. Applied add-cube-cbrt25.6

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

  4. Applied sqrt-prod25.9

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

  5. Applied add-sqr-sqrt25.9

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

  6. Applied times-frac26.7

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

  7. Applied add-cube-cbrt25.0

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

  8. Applied sqrt-prod24.1

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

  9. Applied add-sqr-sqrt24.1

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

  10. Applied times-frac20.5

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

  11. Applied prod-diff20.5

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

  12. Final simplification20.5

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

Reproduce

herbie shell --seed 2019162 +o rules:numerics
(FPCore (x)
  :name "2isqrt (example 3.6)"

  :herbie-target
  (/ 1 (+ (* (+ x 1) (sqrt x)) (* x (sqrt (+ x 1)))))

  (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))