Rosa's DopplerBench

Average Error: 17.4 → 2.2

Time: 3.1s

Precision: binary64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;t1 \le -1.45023077431149694 \cdot 10^{-289} \lor \neg \left(t1 \le 2.4582845282065442 \cdot 10^{-193}\right):\\ \;\;\;\;\frac{t1}{t1 + u} \cdot \frac{v}{-\left(t1 + u\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{t1 \cdot \left(-v\right)}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\\ \end{array}\]

Error

Bits error versus u

Bits error versus v

Bits error versus t1

Derivation

1. Split input into 2 regimes

2. if t1 < -1.45023077431149694e-289 or 2.4582845282065442e-193 < t1

   1. Initial program 17.9

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

   2. Simplified 17.9

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

   4. Applied *-un-lft-identity 17.9

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

   5. Applied times-frac 10.8

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

   6. Applied associate-*r* 1.0

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

   7. Simplified 0.9

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

   if -1.45023077431149694e-289 < t1 < 2.4582845282065442e-193

   1. Initial program 13.7

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
3. Recombined 2 regimes into one program.

4. Final simplification 2.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;t1 \le -1.45023077431149694 \cdot 10^{-289} \lor \neg \left(t1 \le 2.4582845282065442 \cdot 10^{-193}\right):\\ \;\;\;\;\frac{t1}{t1 + u} \cdot \frac{v}{-\left(t1 + u\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{t1 \cdot \left(-v\right)}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\\ \end{array}\]

Reproduce

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