x / (x^2 + 1)

Average Error: 15.1 → 0.0

Time: 2.5s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r67966 = x;
        double r67967 = r67966 * r67966;
        double r67968 = 1.0;
        double r67969 = r67967 + r67968;
        double r67970 = r67966 / r67969;
        return r67970;
}

↓

double f(double x) {
        double r67971 = x;
        double r67972 = -24215928678.961597;
        bool r67973 = r67971 <= r67972;
        double r67974 = 3500.8467687195057;
        bool r67975 = r67971 <= r67974;
        double r67976 = !r67975;
        bool r67977 = r67973 || r67976;
        double r67978 = 1.0;
        double r67979 = 1.0;
        double r67980 = 5.0;
        double r67981 = pow(r67971, r67980);
        double r67982 = r67978 / r67981;
        double r67983 = 3.0;
        double r67984 = pow(r67971, r67983);
        double r67985 = r67978 / r67984;
        double r67986 = r67982 - r67985;
        double r67987 = r67979 * r67986;
        double r67988 = r67978 / r67971;
        double r67989 = r67987 + r67988;
        double r67990 = r67978 * r67989;
        double r67991 = r67971 * r67971;
        double r67992 = r67991 + r67979;
        double r67993 = r67971 / r67992;
        double r67994 = r67978 * r67993;
        double r67995 = r67977 ? r67990 : r67994;
        return r67995;
}

Error

Bits error versus x

Target

Original	15.1
Target	0.1
Herbie	0.0

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

Derivation

1. Split input into 2 regimes

2. if x < -24215928678.961597 or 3500.8467687195057 < x

   1. Initial program 30.8

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

   3. Applied add-sqr-sqrt 30.8

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

   4. Applied associate-/r* 30.7

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

   6. Applied *-un-lft-identity 30.7

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

   7. Applied sqrt-prod 30.7

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

   8. Applied *-un-lft-identity 30.7

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

   9. Applied sqrt-prod 30.7

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

   10. Applied *-un-lft-identity 30.7

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

   11. Applied times-frac 30.7

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

   12. Applied times-frac 30.7

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

   13. Simplified 30.7

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

   14. Simplified 30.8

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

   15. Taylor expanded around inf 0.0

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

   16. Simplified 0.0

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

   if -24215928678.961597 < x < 3500.8467687195057

   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 associate-/r* 0.0

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

   6. Applied *-un-lft-identity 0.0

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

   7. Applied sqrt-prod 0.0

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

   8. Applied *-un-lft-identity 0.0

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

   9. Applied sqrt-prod 0.0

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

   10. Applied *-un-lft-identity 0.0

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

   11. Applied times-frac 0.0

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

   12. Applied times-frac 0.0

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

   13. Simplified 0.0

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

   14. Simplified 0.0

       \[\leadsto 1 \cdot \color{blue}{\frac{x}{x \cdot x + 1}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.0

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

Reproduce

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

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

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