Average Error: 0.2 → 0.2
Time: 20.6s
Precision: 64
\[\left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right) \cdot \left(\frac{\left(1\right)}{\left(\left(\frac{\left(1\right)}{\left(\sqrt{\left(\left(9\right) \cdot \left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}\right)}\right) \cdot rand\right)}\right)\]
↓
\[\left(a - \frac{1.0}{3.0}\right) \cdot \left(1 + \frac{1}{\sqrt{9 \cdot a + 9 \cdot \left(-\frac{1.0}{3.0}\right)}} \cdot rand\right)\]
\left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right) \cdot \left(\frac{\left(1\right)}{\left(\left(\frac{\left(1\right)}{\left(\sqrt{\left(\left(9\right) \cdot \left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}\right)}\right) \cdot rand\right)}\right)
↓
\left(a - \frac{1.0}{3.0}\right) \cdot \left(1 + \frac{1}{\sqrt{9 \cdot a + 9 \cdot \left(-\frac{1.0}{3.0}\right)}} \cdot rand\right)
double f(double a, double rand) {
        double r2109558 = a;
        double r2109559 = 1.0;
        double r2109560 = /* ERROR: no posit support in C */;
        double r2109561 = 3.0;
        double r2109562 = /* ERROR: no posit support in C */;
        double r2109563 = r2109560 / r2109562;
        double r2109564 = r2109558 - r2109563;
        double r2109565 = 1.0;
        double r2109566 = /* ERROR: no posit support in C */;
        double r2109567 = 9.0;
        double r2109568 = /* ERROR: no posit support in C */;
        double r2109569 = r2109568 * r2109564;
        double r2109570 = sqrt(r2109569);
        double r2109571 = r2109566 / r2109570;
        double r2109572 = rand;
        double r2109573 = r2109571 * r2109572;
        double r2109574 = r2109566 + r2109573;
        double r2109575 = r2109564 * r2109574;
        return r2109575;
}
↓
double f(double a, double rand) {
        double r2109576 = a;
        double r2109577 = 1.0;
        double r2109578 = 3.0;
        double r2109579 = r2109577 / r2109578;
        double r2109580 = r2109576 - r2109579;
        double r2109581 = 1.0;
        double r2109582 = 9.0;
        double r2109583 = r2109582 * r2109576;
        double r2109584 = -r2109579;
        double r2109585 = r2109582 * r2109584;
        double r2109586 = r2109583 + r2109585;
        double r2109587 = sqrt(r2109586);
        double r2109588 = r2109581 / r2109587;
        double r2109589 = rand;
        double r2109590 = r2109588 * r2109589;
        double r2109591 = r2109581 + r2109590;
        double r2109592 = r2109580 * r2109591;
        return r2109592;
}

Error

Bits error versus a

Bits error versus rand

Derivation

  1. Initial program 0.2

    \[\left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right) \cdot \left(\frac{\left(1\right)}{\left(\left(\frac{\left(1\right)}{\left(\sqrt{\left(\left(9\right) \cdot \left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}\right)}\right) \cdot rand\right)}\right)\]
  2. Using strategy rm

  3. Applied sub-neg0.2

    \[\leadsto \left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right) \cdot \left(\frac{\left(1\right)}{\left(\left(\frac{\left(1\right)}{\left(\sqrt{\left(\left(9\right) \cdot \color{blue}{\left(\frac{a}{\left(-\left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)}\right)}\right)}\right)}\right) \cdot rand\right)}\right)\]

  4. Applied distribute-lft-in0.2

    \[\leadsto \left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right) \cdot \left(\frac{\left(1\right)}{\left(\left(\frac{\left(1\right)}{\left(\sqrt{\color{blue}{\left(\frac{\left(\left(9\right) \cdot a\right)}{\left(\left(9\right) \cdot \left(-\left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}\right)}}\right)}\right) \cdot rand\right)}\right)\]

  5. Final simplification0.2

    \[\leadsto \left(a - \frac{1.0}{3.0}\right) \cdot \left(1 + \frac{1}{\sqrt{9 \cdot a + 9 \cdot \left(-\frac{1.0}{3.0}\right)}} \cdot rand\right)\]

Reproduce

herbie shell --seed 2019112 +o rules:numerics
(FPCore (a rand)
  :name "Octave 3.8, oct_fill_randg"
  (*.p16 (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0))) (+.p16 (real->posit16 1) (*.p16 (/.p16 (real->posit16 1) (sqrt.p16 (*.p16 (real->posit16 9) (-.p16 a (/.p16 (real->posit16 1.0) (real->posit16 3.0)))))) rand))))