Average Error: 62.0 → 1.0
Time: 14.0s
Precision: 64
\[lo \lt -1.000000000000000010979063629440455417405 \cdot 10^{308} \land hi \gt 1.000000000000000010979063629440455417405 \cdot 10^{308}\]
\[\frac{x - lo}{hi - lo}\]
↓
\[\frac{x}{hi - lo} - \frac{1}{\mathsf{fma}\left(\sqrt{hi}, \frac{\sqrt{hi}}{lo}, -1\right)}\]
\frac{x - lo}{hi - lo}
↓
\frac{x}{hi - lo} - \frac{1}{\mathsf{fma}\left(\sqrt{hi}, \frac{\sqrt{hi}}{lo}, -1\right)}
double f(double lo, double hi, double x) {
        double r30068 = x;
        double r30069 = lo;
        double r30070 = r30068 - r30069;
        double r30071 = hi;
        double r30072 = r30071 - r30069;
        double r30073 = r30070 / r30072;
        return r30073;
}
↓
double f(double lo, double hi, double x) {
        double r30074 = x;
        double r30075 = hi;
        double r30076 = lo;
        double r30077 = r30075 - r30076;
        double r30078 = r30074 / r30077;
        double r30079 = 1.0;
        double r30080 = sqrt(r30075);
        double r30081 = r30080 / r30076;
        double r30082 = -1.0;
        double r30083 = fma(r30080, r30081, r30082);
        double r30084 = r30079 / r30083;
        double r30085 = r30078 - r30084;
        return r30085;
}

Error

Bits error versus lo

Bits error versus hi

Bits error versus x

Derivation

  1. Initial program 62.0

    \[\frac{x - lo}{hi - lo}\]
  2. Using strategy rm

  3. Applied div-sub62.0

    \[\leadsto \color{blue}{\frac{x}{hi - lo} - \frac{lo}{hi - lo}}\]
  4. Using strategy rm

  5. Applied clear-num62.0

    \[\leadsto \frac{x}{hi - lo} - \color{blue}{\frac{1}{\frac{hi - lo}{lo}}}\]

  6. Simplified1.0

    \[\leadsto \frac{x}{hi - lo} - \frac{1}{\color{blue}{\frac{hi}{lo} - 1}}\]
  7. Using strategy rm

  8. Applied *-un-lft-identity1.0

    \[\leadsto \frac{x}{hi - lo} - \frac{1}{\frac{hi}{\color{blue}{1 \cdot lo}} - 1}\]

  9. Applied add-sqr-sqrt1.1

    \[\leadsto \frac{x}{hi - lo} - \frac{1}{\frac{\color{blue}{\sqrt{hi} \cdot \sqrt{hi}}}{1 \cdot lo} - 1}\]

  10. Applied times-frac1.1

    \[\leadsto \frac{x}{hi - lo} - \frac{1}{\color{blue}{\frac{\sqrt{hi}}{1} \cdot \frac{\sqrt{hi}}{lo}} - 1}\]

  11. Applied fma-neg1.0

    \[\leadsto \frac{x}{hi - lo} - \frac{1}{\color{blue}{\mathsf{fma}\left(\frac{\sqrt{hi}}{1}, \frac{\sqrt{hi}}{lo}, -1\right)}}\]

  12. Simplified1.0

    \[\leadsto \frac{x}{hi - lo} - \frac{1}{\mathsf{fma}\left(\frac{\sqrt{hi}}{1}, \frac{\sqrt{hi}}{lo}, \color{blue}{-1}\right)}\]

  13. Final simplification1.0

    \[\leadsto \frac{x}{hi - lo} - \frac{1}{\mathsf{fma}\left(\sqrt{hi}, \frac{\sqrt{hi}}{lo}, -1\right)}\]

Reproduce

herbie shell --seed 2019322 +o rules:numerics
(FPCore (lo hi x)
  :name "(/ (- x lo) (- hi lo))"
  :precision binary64
  :pre (and (< lo -1e+308) (> hi 1e+308))
  (/ (- x lo) (- hi lo)))