Average Error: 0.2 → 0.2
Time: 34.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(1 + \frac{rand \cdot 1}{\sqrt{\left(a - \frac{1.0}{3.0}\right) \cdot 9}}\right) \cdot \left(a - \frac{1.0}{3.0}\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(1 + \frac{rand \cdot 1}{\sqrt{\left(a - \frac{1.0}{3.0}\right) \cdot 9}}\right) \cdot \left(a - \frac{1.0}{3.0}\right)
double f(double a, double rand) {
        double r5309186 = a;
        double r5309187 = 1.0;
        double r5309188 = /* ERROR: no posit support in C */;
        double r5309189 = 3.0;
        double r5309190 = /* ERROR: no posit support in C */;
        double r5309191 = r5309188 / r5309190;
        double r5309192 = r5309186 - r5309191;
        double r5309193 = 1.0;
        double r5309194 = /* ERROR: no posit support in C */;
        double r5309195 = 9.0;
        double r5309196 = /* ERROR: no posit support in C */;
        double r5309197 = r5309196 * r5309192;
        double r5309198 = sqrt(r5309197);
        double r5309199 = r5309194 / r5309198;
        double r5309200 = rand;
        double r5309201 = r5309199 * r5309200;
        double r5309202 = r5309194 + r5309201;
        double r5309203 = r5309192 * r5309202;
        return r5309203;
}
↓
double f(double a, double rand) {
        double r5309204 = 1.0;
        double r5309205 = rand;
        double r5309206 = r5309205 * r5309204;
        double r5309207 = a;
        double r5309208 = 1.0;
        double r5309209 = 3.0;
        double r5309210 = r5309208 / r5309209;
        double r5309211 = r5309207 - r5309210;
        double r5309212 = 9.0;
        double r5309213 = r5309211 * r5309212;
        double r5309214 = sqrt(r5309213);
        double r5309215 = r5309206 / r5309214;
        double r5309216 = r5309204 + r5309215;
        double r5309217 = r5309216 * r5309211;
        return r5309217;
}

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. Simplified0.2

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

  6. Applied p16-flip--0.2

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

  7. Simplified0.2

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

  8. Simplified0.2

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

  9. Final simplification0.2

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

Reproduce

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