Average Error: 1.0 → 1.0
Time: 1.1m
Precision: 64
\[\frac{\left(\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\frac{\left(2\right)}{x}\right)\right)}{\left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right)}\]
↓
\[\left(\mathsf{qma}\left(\left(\mathsf{qms}\left(\left(\left(\frac{1}{x + 1}\right)\right), 1.0, \left(\frac{2}{x}\right)\right)\right), \left(\frac{1}{x - 1}\right), 1.0\right)\right)\]
\frac{\left(\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\frac{\left(2\right)}{x}\right)\right)}{\left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right)}
↓
\left(\mathsf{qma}\left(\left(\mathsf{qms}\left(\left(\left(\frac{1}{x + 1}\right)\right), 1.0, \left(\frac{2}{x}\right)\right)\right), \left(\frac{1}{x - 1}\right), 1.0\right)\right)
double f(double x) {
        double r1579288 = 1.0;
        double r1579289 = /* ERROR: no posit support in C */;
        double r1579290 = x;
        double r1579291 = r1579290 + r1579289;
        double r1579292 = r1579289 / r1579291;
        double r1579293 = 2.0;
        double r1579294 = /* ERROR: no posit support in C */;
        double r1579295 = r1579294 / r1579290;
        double r1579296 = r1579292 - r1579295;
        double r1579297 = r1579290 - r1579289;
        double r1579298 = r1579289 / r1579297;
        double r1579299 = r1579296 + r1579298;
        return r1579299;
}
↓
double f(double x) {
        double r1579300 = 1.0;
        double r1579301 = x;
        double r1579302 = r1579301 + r1579300;
        double r1579303 = r1579300 / r1579302;
        double r1579304 = /*Error: no posit support in C */;
        double r1579305 = 1.0;
        double r1579306 = 2.0;
        double r1579307 = r1579306 / r1579301;
        double r1579308 = /*Error: no posit support in C */;
        double r1579309 = r1579301 - r1579300;
        double r1579310 = r1579300 / r1579309;
        double r1579311 = /*Error: no posit support in C */;
        double r1579312 = /*Error: no posit support in C */;
        return r1579312;
}

Error

Bits error versus x

Derivation

  1. Initial program 1.0

    \[\frac{\left(\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right) - \left(\frac{\left(2\right)}{x}\right)\right)}{\left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right)}\]
  2. Using strategy rm

  3. Applied p16-*-un-lft-identity1.0

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

  4. Applied introduce-quire1.0

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

  5. Applied insert-quire-fdp-sub1.0

    \[\leadsto \frac{\color{blue}{\left(\left(\mathsf{qms}\left(\left(\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right)\right), \left(1.0\right), \left(\frac{\left(2\right)}{x}\right)\right)\right)\right)}}{\left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right)}\]

  6. Applied insert-quire-add1.0

    \[\leadsto \color{blue}{\left(\mathsf{qma}\left(\left(\mathsf{qms}\left(\left(\left(\frac{\left(1\right)}{\left(\frac{x}{\left(1\right)}\right)}\right)\right), \left(1.0\right), \left(\frac{\left(2\right)}{x}\right)\right)\right), \left(\frac{\left(1\right)}{\left(x - \left(1\right)\right)}\right), \left(1.0\right)\right)\right)}\]

  7. Final simplification1.0

    \[\leadsto \left(\mathsf{qma}\left(\left(\mathsf{qms}\left(\left(\left(\frac{1}{x + 1}\right)\right), 1.0, \left(\frac{2}{x}\right)\right)\right), \left(\frac{1}{x - 1}\right), 1.0\right)\right)\]

Reproduce

herbie shell --seed 2019154 
(FPCore (x)
  :name "3frac (problem 3.3.3)"
  (+.p16 (-.p16 (/.p16 (real->posit16 1) (+.p16 x (real->posit16 1))) (/.p16 (real->posit16 2) x)) (/.p16 (real->posit16 1) (-.p16 x (real->posit16 1)))))