Average Error: 0.2 → 0.2
Time: 19.7s
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{a \cdot 9 + \left(-\frac{1.0}{3.0}\right) \cdot 9}} \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{a \cdot 9 + \left(-\frac{1.0}{3.0}\right) \cdot 9}} \cdot rand\right)
double f(double a, double rand) {
        double r2603039 = a;
        double r2603040 = 1.0;
        double r2603041 = /* ERROR: no posit support in C */;
        double r2603042 = 3.0;
        double r2603043 = /* ERROR: no posit support in C */;
        double r2603044 = r2603041 / r2603043;
        double r2603045 = r2603039 - r2603044;
        double r2603046 = 1.0;
        double r2603047 = /* ERROR: no posit support in C */;
        double r2603048 = 9.0;
        double r2603049 = /* ERROR: no posit support in C */;
        double r2603050 = r2603049 * r2603045;
        double r2603051 = sqrt(r2603050);
        double r2603052 = r2603047 / r2603051;
        double r2603053 = rand;
        double r2603054 = r2603052 * r2603053;
        double r2603055 = r2603047 + r2603054;
        double r2603056 = r2603045 * r2603055;
        return r2603056;
}
↓
double f(double a, double rand) {
        double r2603057 = a;
        double r2603058 = 1.0;
        double r2603059 = 3.0;
        double r2603060 = r2603058 / r2603059;
        double r2603061 = r2603057 - r2603060;
        double r2603062 = 1.0;
        double r2603063 = 9.0;
        double r2603064 = r2603057 * r2603063;
        double r2603065 = -r2603060;
        double r2603066 = r2603065 * r2603063;
        double r2603067 = r2603064 + r2603066;
        double r2603068 = sqrt(r2603067);
        double r2603069 = r2603062 / r2603068;
        double r2603070 = rand;
        double r2603071 = r2603069 * r2603070;
        double r2603072 = r2603062 + r2603071;
        double r2603073 = r2603061 * r2603072;
        return r2603073;
}

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-rgt-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(a \cdot \left(9\right)\right)}{\left(\left(-\left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right) \cdot \left(9\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{a \cdot 9 + \left(-\frac{1.0}{3.0}\right) \cdot 9}} \cdot rand\right)\]

Reproduce

herbie shell --seed 2019120 
(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))))