Average Error: 30.3 → 0.2
Time: 18.2s
Precision: 64
\[\sqrt{x + 1} - \sqrt{x}\]
\[\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{\sqrt{x + 1} + \sqrt{x}}\right)\right)\]
\sqrt{x + 1} - \sqrt{x}
\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{\sqrt{x + 1} + \sqrt{x}}\right)\right)
double f(double x) {
        double r19648674 = x;
        double r19648675 = 1.0;
        double r19648676 = r19648674 + r19648675;
        double r19648677 = sqrt(r19648676);
        double r19648678 = sqrt(r19648674);
        double r19648679 = r19648677 - r19648678;
        return r19648679;
}

double f(double x) {
        double r19648680 = 1.0;
        double r19648681 = x;
        double r19648682 = r19648681 + r19648680;
        double r19648683 = sqrt(r19648682);
        double r19648684 = sqrt(r19648681);
        double r19648685 = r19648683 + r19648684;
        double r19648686 = r19648680 / r19648685;
        double r19648687 = log1p(r19648686);
        double r19648688 = expm1(r19648687);
        return r19648688;
}

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original30.3
Target0.2
Herbie0.2
\[\frac{1}{\sqrt{x + 1} + \sqrt{x}}\]

Derivation

  1. Initial program 30.3

    \[\sqrt{x + 1} - \sqrt{x}\]
  2. Using strategy rm
  3. Applied flip--30.1

    \[\leadsto \color{blue}{\frac{\sqrt{x + 1} \cdot \sqrt{x + 1} - \sqrt{x} \cdot \sqrt{x}}{\sqrt{x + 1} + \sqrt{x}}}\]
  4. Simplified0.2

    \[\leadsto \frac{\color{blue}{1 + 0}}{\sqrt{x + 1} + \sqrt{x}}\]
  5. Using strategy rm
  6. Applied expm1-log1p-u0.2

    \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1 + 0}{\sqrt{x + 1} + \sqrt{x}}\right)\right)}\]
  7. Simplified0.2

    \[\leadsto \mathsf{expm1}\left(\color{blue}{\mathsf{log1p}\left(\frac{1}{\sqrt{x + 1} + \sqrt{x}}\right)}\right)\]
  8. Final simplification0.2

    \[\leadsto \mathsf{expm1}\left(\mathsf{log1p}\left(\frac{1}{\sqrt{x + 1} + \sqrt{x}}\right)\right)\]

Reproduce

herbie shell --seed 2019179 +o rules:numerics
(FPCore (x)
  :name "Main:bigenough3 from C"

  :herbie-target
  (/ 1.0 (+ (sqrt (+ x 1.0)) (sqrt x)))

  (- (sqrt (+ x 1.0)) (sqrt x)))