Average Error: 0.2 → 0.2
Time: 1.2m
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(\left(\left(a - \frac{1.0}{3.0}\right) \cdot \left(\frac{rand \cdot 1}{\sqrt{\left(a - \frac{1.0}{3.0}\right) \cdot 9}} + 1\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)
↓
\left(\left(\left(a - \frac{1.0}{3.0}\right) \cdot \left(\frac{rand \cdot 1}{\sqrt{\left(a - \frac{1.0}{3.0}\right) \cdot 9}} + 1\right)\right)\right)
double f(double a, double rand) {
        double r2326077 = a;
        double r2326078 = 1.0;
        double r2326079 = /* ERROR: no posit support in C */;
        double r2326080 = 3.0;
        double r2326081 = /* ERROR: no posit support in C */;
        double r2326082 = r2326079 / r2326081;
        double r2326083 = r2326077 - r2326082;
        double r2326084 = 1.0;
        double r2326085 = /* ERROR: no posit support in C */;
        double r2326086 = 9.0;
        double r2326087 = /* ERROR: no posit support in C */;
        double r2326088 = r2326087 * r2326083;
        double r2326089 = sqrt(r2326088);
        double r2326090 = r2326085 / r2326089;
        double r2326091 = rand;
        double r2326092 = r2326090 * r2326091;
        double r2326093 = r2326085 + r2326092;
        double r2326094 = r2326083 * r2326093;
        return r2326094;
}
↓
double f(double a, double rand) {
        double r2326095 = a;
        double r2326096 = 1.0;
        double r2326097 = 3.0;
        double r2326098 = r2326096 / r2326097;
        double r2326099 = r2326095 - r2326098;
        double r2326100 = rand;
        double r2326101 = 1.0;
        double r2326102 = r2326100 * r2326101;
        double r2326103 = 9.0;
        double r2326104 = r2326099 * r2326103;
        double r2326105 = sqrt(r2326104);
        double r2326106 = r2326102 / r2326105;
        double r2326107 = r2326106 + r2326101;
        double r2326108 = r2326099 * r2326107;
        double r2326109 = /*Error: no posit support in C */;
        double r2326110 = /*Error: no posit support in C */;
        return r2326110;
}

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. Using strategy rm

  6. Applied introduce-quire0.2

    \[\leadsto \color{blue}{\left(\left(\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(\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)\right)\right)}\]

  7. Simplified0.2

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

  8. Final simplification0.2

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

Reproduce

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