Average Error: 18.1 → 1.2
Time: 15.2s
Precision: 64
\[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
↓
\[\frac{\frac{-t1}{t1 + u} \cdot v}{t1 + u}\]
\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}
↓
\frac{\frac{-t1}{t1 + u} \cdot v}{t1 + u}
double f(double u, double v, double t1) {
        double r28461 = t1;
        double r28462 = -r28461;
        double r28463 = v;
        double r28464 = r28462 * r28463;
        double r28465 = u;
        double r28466 = r28461 + r28465;
        double r28467 = r28466 * r28466;
        double r28468 = r28464 / r28467;
        return r28468;
}
↓
double f(double u, double v, double t1) {
        double r28469 = t1;
        double r28470 = -r28469;
        double r28471 = u;
        double r28472 = r28469 + r28471;
        double r28473 = r28470 / r28472;
        double r28474 = v;
        double r28475 = r28473 * r28474;
        double r28476 = r28475 / r28472;
        return r28476;
}

Error

Bits error versus u

Bits error versus v

Bits error versus t1

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 18.1

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

  3. Applied times-frac1.3

    \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}}\]
  4. Using strategy rm

  5. Applied clear-num1.6

    \[\leadsto \frac{-t1}{t1 + u} \cdot \color{blue}{\frac{1}{\frac{t1 + u}{v}}}\]
  6. Using strategy rm

  7. Applied associate-*l/1.7

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

  8. Simplified1.5

    \[\leadsto \frac{\color{blue}{\frac{-t1}{\frac{t1 + u}{v}}}}{t1 + u}\]
  9. Using strategy rm

  10. Applied associate-/r/1.2

    \[\leadsto \frac{\color{blue}{\frac{-t1}{t1 + u} \cdot v}}{t1 + u}\]

  11. Final simplification1.2

    \[\leadsto \frac{\frac{-t1}{t1 + u} \cdot v}{t1 + u}\]

Reproduce

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