Average Error: 17.4 → 2.2
Time: 3.3s
Precision: binary64
\[\]
↓
\[\]

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

      \[\]

    2. Simplified17.9

      \[\leadsto \]
    3. Using strategy rm

    4. Applied *-un-lft-identity17.9

      \[\leadsto \]

    5. Applied times-frac10.8

      \[\leadsto \]

    6. Applied associate-*r*1.0

      \[\leadsto \]

    7. Simplified0.9

      \[\leadsto \]

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

    1. Initial program 13.7

      \[\]
  3. Recombined 2 regimes into one program.

  4. Final simplification2.2

    \[\leadsto \]

Reproduce

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