Average Error: 0.2 → 0.2
Time: 39.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)\]
\[\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 r5246136 = a;
        double r5246137 = 1.0;
        double r5246138 = /* ERROR: no posit support in C */;
        double r5246139 = 3.0;
        double r5246140 = /* ERROR: no posit support in C */;
        double r5246141 = r5246138 / r5246140;
        double r5246142 = r5246136 - r5246141;
        double r5246143 = 1.0;
        double r5246144 = /* ERROR: no posit support in C */;
        double r5246145 = 9.0;
        double r5246146 = /* ERROR: no posit support in C */;
        double r5246147 = r5246146 * r5246142;
        double r5246148 = sqrt(r5246147);
        double r5246149 = r5246144 / r5246148;
        double r5246150 = rand;
        double r5246151 = r5246149 * r5246150;
        double r5246152 = r5246144 + r5246151;
        double r5246153 = r5246142 * r5246152;
        return r5246153;
}

double f(double a, double rand) {
        double r5246154 = a;
        double r5246155 = 1.0;
        double r5246156 = 3.0;
        double r5246157 = r5246155 / r5246156;
        double r5246158 = r5246154 - r5246157;
        double r5246159 = 1.0;
        double r5246160 = 9.0;
        double r5246161 = r5246160 * r5246154;
        double r5246162 = -r5246157;
        double r5246163 = r5246160 * r5246162;
        double r5246164 = r5246161 + r5246163;
        double r5246165 = sqrt(r5246164);
        double r5246166 = r5246159 / r5246165;
        double r5246167 = rand;
        double r5246168 = r5246166 * r5246167;
        double r5246169 = r5246159 + r5246168;
        double r5246170 = r5246158 * r5246169;
        return r5246170;
}

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 2019133 
(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))))