Rosa's DopplerBench

Average Error: 18.5 → 1.8

Time: 8.0s

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 r20362 = t1;
        double r20363 = -r20362;
        double r20364 = v;
        double r20365 = r20363 * r20364;
        double r20366 = u;
        double r20367 = r20362 + r20366;
        double r20368 = r20367 * r20367;
        double r20369 = r20365 / r20368;
        return r20369;
}

↓

double f(double u, double v, double t1) {
        double r20370 = t1;
        double r20371 = -r20370;
        double r20372 = 1.0;
        double r20373 = u;
        double r20374 = r20370 + r20373;
        double r20375 = v;
        double r20376 = r20374 / r20375;
        double r20377 = r20372 / r20376;
        double r20378 = r20371 * r20377;
        double r20379 = r20378 / r20374;
        return r20379;
}

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