Average Error: 0.2 → 0.2
Time: 17.9s
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)\]
\[1 \cdot a + \left(1 \cdot \left(-\frac{1.0}{3.0}\right) + \left(\left(\frac{1}{\sqrt{9 \cdot \left(a - \frac{1.0}{3.0}\right)}} \cdot rand\right) \cdot a + \left(\frac{1}{\sqrt{9 \cdot \left(a - \frac{1.0}{3.0}\right)}} \cdot rand\right) \cdot \left(-\frac{1.0}{3.0}\right)\right)\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)
1 \cdot a + \left(1 \cdot \left(-\frac{1.0}{3.0}\right) + \left(\left(\frac{1}{\sqrt{9 \cdot \left(a - \frac{1.0}{3.0}\right)}} \cdot rand\right) \cdot a + \left(\frac{1}{\sqrt{9 \cdot \left(a - \frac{1.0}{3.0}\right)}} \cdot rand\right) \cdot \left(-\frac{1.0}{3.0}\right)\right)\right)
double f(double a, double rand) {
        double r1459231 = a;
        double r1459232 = 1.0;
        double r1459233 = /* ERROR: no posit support in C */;
        double r1459234 = 3.0;
        double r1459235 = /* ERROR: no posit support in C */;
        double r1459236 = r1459233 / r1459235;
        double r1459237 = r1459231 - r1459236;
        double r1459238 = 1.0;
        double r1459239 = /* ERROR: no posit support in C */;
        double r1459240 = 9.0;
        double r1459241 = /* ERROR: no posit support in C */;
        double r1459242 = r1459241 * r1459237;
        double r1459243 = sqrt(r1459242);
        double r1459244 = r1459239 / r1459243;
        double r1459245 = rand;
        double r1459246 = r1459244 * r1459245;
        double r1459247 = r1459239 + r1459246;
        double r1459248 = r1459237 * r1459247;
        return r1459248;
}

double f(double a, double rand) {
        double r1459249 = 1.0;
        double r1459250 = a;
        double r1459251 = r1459249 * r1459250;
        double r1459252 = 1.0;
        double r1459253 = 3.0;
        double r1459254 = r1459252 / r1459253;
        double r1459255 = -r1459254;
        double r1459256 = r1459249 * r1459255;
        double r1459257 = 9.0;
        double r1459258 = r1459250 - r1459254;
        double r1459259 = r1459257 * r1459258;
        double r1459260 = sqrt(r1459259);
        double r1459261 = r1459249 / r1459260;
        double r1459262 = rand;
        double r1459263 = r1459261 * r1459262;
        double r1459264 = r1459263 * r1459250;
        double r1459265 = r1459263 * r1459255;
        double r1459266 = r1459264 + r1459265;
        double r1459267 = r1459256 + r1459266;
        double r1459268 = r1459251 + r1459267;
        return r1459268;
}

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 distribute-rgt-in0.2

    \[\leadsto \color{blue}{\frac{\left(\left(1\right) \cdot \left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}{\left(\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) \cdot \left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}}\]
  4. Using strategy rm
  5. Applied sub-neg0.2

    \[\leadsto \frac{\left(\left(1\right) \cdot \color{blue}{\left(\frac{a}{\left(-\left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)}\right)}\right)}{\left(\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) \cdot \left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}\]
  6. Applied distribute-lft-in0.2

    \[\leadsto \frac{\color{blue}{\left(\frac{\left(\left(1\right) \cdot a\right)}{\left(\left(1\right) \cdot \left(-\left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}\right)}}{\left(\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) \cdot \left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}\]
  7. Applied associate-+l+0.2

    \[\leadsto \color{blue}{\frac{\left(\left(1\right) \cdot a\right)}{\left(\frac{\left(\left(1\right) \cdot \left(-\left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}{\left(\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) \cdot \left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}\right)}}\]
  8. Using strategy rm
  9. Applied sub-neg0.2

    \[\leadsto \frac{\left(\left(1\right) \cdot a\right)}{\left(\frac{\left(\left(1\right) \cdot \left(-\left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}{\left(\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) \cdot \color{blue}{\left(\frac{a}{\left(-\left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)}\right)}\right)}\right)}\]
  10. Applied distribute-lft-in0.2

    \[\leadsto \frac{\left(\left(1\right) \cdot a\right)}{\left(\frac{\left(\left(1\right) \cdot \left(-\left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}{\color{blue}{\left(\frac{\left(\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) \cdot a\right)}{\left(\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) \cdot \left(-\left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}\right)}}\right)}\]
  11. Final simplification0.2

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

Reproduce

herbie shell --seed 2019128 +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))))