Average Error: 0.2 → 0.2
Time: 23.3s
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)\]
↓
\[1 \cdot \left(a - \frac{1.0}{3.0}\right) + \left(\frac{1}{\sqrt{a \cdot 9 + \left(-\frac{1.0}{3.0}\right) \cdot 9}} \cdot rand\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)
↓
1 \cdot \left(a - \frac{1.0}{3.0}\right) + \left(\frac{1}{\sqrt{a \cdot 9 + \left(-\frac{1.0}{3.0}\right) \cdot 9}} \cdot rand\right) \cdot \left(a - \frac{1.0}{3.0}\right)
double f(double a, double rand) {
        double r2208670 = a;
        double r2208671 = 1.0;
        double r2208672 = /* ERROR: no posit support in C */;
        double r2208673 = 3.0;
        double r2208674 = /* ERROR: no posit support in C */;
        double r2208675 = r2208672 / r2208674;
        double r2208676 = r2208670 - r2208675;
        double r2208677 = 1.0;
        double r2208678 = /* ERROR: no posit support in C */;
        double r2208679 = 9.0;
        double r2208680 = /* ERROR: no posit support in C */;
        double r2208681 = r2208680 * r2208676;
        double r2208682 = sqrt(r2208681);
        double r2208683 = r2208678 / r2208682;
        double r2208684 = rand;
        double r2208685 = r2208683 * r2208684;
        double r2208686 = r2208678 + r2208685;
        double r2208687 = r2208676 * r2208686;
        return r2208687;
}
↓
double f(double a, double rand) {
        double r2208688 = 1.0;
        double r2208689 = a;
        double r2208690 = 1.0;
        double r2208691 = 3.0;
        double r2208692 = r2208690 / r2208691;
        double r2208693 = r2208689 - r2208692;
        double r2208694 = r2208688 * r2208693;
        double r2208695 = 9.0;
        double r2208696 = r2208689 * r2208695;
        double r2208697 = -r2208692;
        double r2208698 = r2208697 * r2208695;
        double r2208699 = r2208696 + r2208698;
        double r2208700 = sqrt(r2208699);
        double r2208701 = r2208688 / r2208700;
        double r2208702 = rand;
        double r2208703 = r2208701 * r2208702;
        double r2208704 = r2208703 * r2208693;
        double r2208705 = r2208694 + r2208704;
        return r2208705;
}

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

  5. Applied sub-neg0.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(\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) \cdot \left(a - \left(\frac{\left(1.0\right)}{\left(3.0\right)}\right)\right)\right)}\]

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

  7. Final simplification0.2

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

Reproduce

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