Average Error: 0.2 → 0.2
Time: 31.1s
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 1 + \left(\left(\frac{\left(a - \frac{1.0}{3.0}\right) \cdot 1}{\sqrt{9 \cdot \left(a - \frac{1.0}{3.0}\right)}} \cdot rand\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(a - \frac{1.0}{3.0}\right) \cdot 1 + \left(\left(\frac{\left(a - \frac{1.0}{3.0}\right) \cdot 1}{\sqrt{9 \cdot \left(a - \frac{1.0}{3.0}\right)}} \cdot rand\right)\right)
double f(double a, double rand) {
        double r957803 = a;
        double r957804 = 1.0;
        double r957805 = /* ERROR: no posit support in C */;
        double r957806 = 3.0;
        double r957807 = /* ERROR: no posit support in C */;
        double r957808 = r957805 / r957807;
        double r957809 = r957803 - r957808;
        double r957810 = 1.0;
        double r957811 = /* ERROR: no posit support in C */;
        double r957812 = 9.0;
        double r957813 = /* ERROR: no posit support in C */;
        double r957814 = r957813 * r957809;
        double r957815 = sqrt(r957814);
        double r957816 = r957811 / r957815;
        double r957817 = rand;
        double r957818 = r957816 * r957817;
        double r957819 = r957811 + r957818;
        double r957820 = r957809 * r957819;
        return r957820;
}

double f(double a, double rand) {
        double r957821 = a;
        double r957822 = 1.0;
        double r957823 = 3.0;
        double r957824 = r957822 / r957823;
        double r957825 = r957821 - r957824;
        double r957826 = 1.0;
        double r957827 = r957825 * r957826;
        double r957828 = 9.0;
        double r957829 = r957828 * r957825;
        double r957830 = sqrt(r957829);
        double r957831 = r957827 / r957830;
        double r957832 = rand;
        double r957833 = r957831 * r957832;
        double r957834 = /*Error: no posit support in C */;
        double r957835 = /*Error: no posit support in C */;
        double r957836 = r957827 + r957835;
        return r957836;
}

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-lft-in0.2

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

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

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

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

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

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

Reproduce

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