x / (x^2 + 1)

Average Error: 15.3 → 0.0

Time: 3.1s

Precision: 64

Math

\[\frac{x}{x \cdot x + 1}\]

↓

\[\begin{array}{l} \mathbf{if}\;x \le -60718579425352480 \lor \neg \left(x \le 938.420929804902585\right):\\ \;\;\;\;\left(\frac{1}{x} - 1 \cdot \frac{1}{{x}^{3}}\right) + \frac{1}{{x}^{5}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{\frac{\sqrt{{\left(x \cdot x\right)}^{3} + {1}^{3}}}{\sqrt{\left(x \cdot x\right) \cdot \left(x \cdot x\right) + \left(1 \cdot 1 - \left(x \cdot x\right) \cdot 1\right)}}} \cdot \frac{1}{\sqrt{x \cdot x + 1}}\\ \end{array}\]

C

double f(double x) {
        double r77497 = x;
        double r77498 = r77497 * r77497;
        double r77499 = 1.0;
        double r77500 = r77498 + r77499;
        double r77501 = r77497 / r77500;
        return r77501;
}

↓

double f(double x) {
        double r77502 = x;
        double r77503 = -6.071857942535248e+16;
        bool r77504 = r77502 <= r77503;
        double r77505 = 938.4209298049026;
        bool r77506 = r77502 <= r77505;
        double r77507 = !r77506;
        bool r77508 = r77504 || r77507;
        double r77509 = 1.0;
        double r77510 = r77509 / r77502;
        double r77511 = 1.0;
        double r77512 = 3.0;
        double r77513 = pow(r77502, r77512);
        double r77514 = r77509 / r77513;
        double r77515 = r77511 * r77514;
        double r77516 = r77510 - r77515;
        double r77517 = 5.0;
        double r77518 = pow(r77502, r77517);
        double r77519 = r77511 / r77518;
        double r77520 = r77516 + r77519;
        double r77521 = r77502 * r77502;
        double r77522 = pow(r77521, r77512);
        double r77523 = pow(r77511, r77512);
        double r77524 = r77522 + r77523;
        double r77525 = sqrt(r77524);
        double r77526 = r77521 * r77521;
        double r77527 = r77511 * r77511;
        double r77528 = r77521 * r77511;
        double r77529 = r77527 - r77528;
        double r77530 = r77526 + r77529;
        double r77531 = sqrt(r77530);
        double r77532 = r77525 / r77531;
        double r77533 = r77502 / r77532;
        double r77534 = r77521 + r77511;
        double r77535 = sqrt(r77534);
        double r77536 = r77509 / r77535;
        double r77537 = r77533 * r77536;
        double r77538 = r77508 ? r77520 : r77537;
        return r77538;
}

Error

Bits error versus x

Target

Original	15.3
Target	0.1
Herbie	0.0

\[\frac{1}{x + \frac{1}{x}}\]

Derivation

1. Split input into 2 regimes

2. if x < -6.071857942535248e+16 or 938.4209298049026 < x

   1. Initial program 31.6

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

   3. Applied add-sqr-sqrt 31.6

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

   4. Applied *-un-lft-identity 31.6

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

   5. Applied times-frac 31.5

      \[\leadsto \color{blue}{\frac{1}{\sqrt{x \cdot x + 1}} \cdot \frac{x}{\sqrt{x \cdot x + 1}}}\]
   6. Using strategy rm

   7. Applied div-inv 31.5

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

   8. Applied associate-*r* 31.5

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

   9. Simplified 31.5

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

   10. Taylor expanded around inf 0.0

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

   11. Simplified 0.0

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

   if -6.071857942535248e+16 < x < 938.4209298049026

   1. Initial program 0.0

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

   3. Applied add-sqr-sqrt 0.0

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

   4. Applied *-un-lft-identity 0.0

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

   5. Applied times-frac 0.0

      \[\leadsto \color{blue}{\frac{1}{\sqrt{x \cdot x + 1}} \cdot \frac{x}{\sqrt{x \cdot x + 1}}}\]
   6. Using strategy rm

   7. Applied div-inv 0.0

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

   8. Applied associate-*r* 0.0

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

   9. Simplified 0.0

      \[\leadsto \color{blue}{\frac{x}{\sqrt{x \cdot x + 1}}} \cdot \frac{1}{\sqrt{x \cdot x + 1}}\]
   10. Using strategy rm

   11. Applied flip3-+ 0.0

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

   12. Applied sqrt-div 0.0

       \[\leadsto \frac{x}{\color{blue}{\frac{\sqrt{{\left(x \cdot x\right)}^{3} + {1}^{3}}}{\sqrt{\left(x \cdot x\right) \cdot \left(x \cdot x\right) + \left(1 \cdot 1 - \left(x \cdot x\right) \cdot 1\right)}}}} \cdot \frac{1}{\sqrt{x \cdot x + 1}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le -60718579425352480 \lor \neg \left(x \le 938.420929804902585\right):\\ \;\;\;\;\left(\frac{1}{x} - 1 \cdot \frac{1}{{x}^{3}}\right) + \frac{1}{{x}^{5}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{\frac{\sqrt{{\left(x \cdot x\right)}^{3} + {1}^{3}}}{\sqrt{\left(x \cdot x\right) \cdot \left(x \cdot x\right) + \left(1 \cdot 1 - \left(x \cdot x\right) \cdot 1\right)}}} \cdot \frac{1}{\sqrt{x \cdot x + 1}}\\ \end{array}\]

Reproduce

herbie shell --seed 2020024 
(FPCore (x)
  :name "x / (x^2 + 1)"
  :precision binary64

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

  (/ x (+ (* x x) 1)))