Rosa's DopplerBench

Average Error: 18.5 → 1.8

Time: 8.6s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]

↓

\[\frac{\left(-t1\right) \cdot \frac{1}{\frac{t1 + u}{v}}}{t1 + u}\]

C

double f(double u, double v, double t1) {
        double r20738 = t1;
        double r20739 = -r20738;
        double r20740 = v;
        double r20741 = r20739 * r20740;
        double r20742 = u;
        double r20743 = r20738 + r20742;
        double r20744 = r20743 * r20743;
        double r20745 = r20741 / r20744;
        return r20745;
}

↓

double f(double u, double v, double t1) {
        double r20746 = t1;
        double r20747 = -r20746;
        double r20748 = 1.0;
        double r20749 = u;
        double r20750 = r20746 + r20749;
        double r20751 = v;
        double r20752 = r20750 / r20751;
        double r20753 = r20748 / r20752;
        double r20754 = r20747 * r20753;
        double r20755 = r20754 / r20750;
        return r20755;
}

Error

Bits error versus u

Bits error versus v

Bits error versus t1

Derivation

1. Initial program 18.5

   \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
2. Using strategy rm

3. Applied associate-/r* 11.7

   \[\leadsto \color{blue}{\frac{\frac{\left(-t1\right) \cdot v}{t1 + u}}{t1 + u}}\]

4. Simplified 1.4

   \[\leadsto \frac{\color{blue}{\left(-t1\right) \cdot \frac{v}{t1 + u}}}{t1 + u}\]
5. Using strategy rm

6. Applied clear-num 1.8

   \[\leadsto \frac{\left(-t1\right) \cdot \color{blue}{\frac{1}{\frac{t1 + u}{v}}}}{t1 + u}\]

7. Final simplification 1.8

   \[\leadsto \frac{\left(-t1\right) \cdot \frac{1}{\frac{t1 + u}{v}}}{t1 + u}\]

Reproduce

herbie shell --seed 2020047 
(FPCore (u v t1)
  :name "Rosa's DopplerBench"
  :precision binary64
  (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))