Average Error: 0.2 → 0.2
Time: 27.8s
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 r1023001 = a;
        double r1023002 = 1.0;
        double r1023003 = /* ERROR: no posit support in C */;
        double r1023004 = 3.0;
        double r1023005 = /* ERROR: no posit support in C */;
        double r1023006 = r1023003 / r1023005;
        double r1023007 = r1023001 - r1023006;
        double r1023008 = 1.0;
        double r1023009 = /* ERROR: no posit support in C */;
        double r1023010 = 9.0;
        double r1023011 = /* ERROR: no posit support in C */;
        double r1023012 = r1023011 * r1023007;
        double r1023013 = sqrt(r1023012);
        double r1023014 = r1023009 / r1023013;
        double r1023015 = rand;
        double r1023016 = r1023014 * r1023015;
        double r1023017 = r1023009 + r1023016;
        double r1023018 = r1023007 * r1023017;
        return r1023018;
}
↓
double f(double a, double rand) {
        double r1023019 = a;
        double r1023020 = 1.0;
        double r1023021 = 3.0;
        double r1023022 = r1023020 / r1023021;
        double r1023023 = r1023019 - r1023022;
        double r1023024 = 1.0;
        double r1023025 = 9.0;
        double r1023026 = r1023019 * r1023025;
        double r1023027 = -r1023022;
        double r1023028 = r1023027 * r1023025;
        double r1023029 = r1023026 + r1023028;
        double r1023030 = sqrt(r1023029);
        double r1023031 = r1023024 / r1023030;
        double r1023032 = rand;
        double r1023033 = r1023031 * r1023032;
        double r1023034 = r1023024 + r1023033;
        double r1023035 = r1023023 * r1023034;
        return r1023035;
}

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 2019153 +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))))