Average Error: 34.3 → 6.5

Time: 4.6s

Precision: binary64

\[\]

↓

\[\]

Error

The X axis uses an exponential scale — Bits error versus a

The X axis uses an exponential scale — Bits error versus a

The X axis uses an exponential scale — Bits error versus b_2

The X axis uses an exponential scale — Bits error versus b_2

The X axis uses an exponential scale — Bits error versus c

The X axis uses an exponential scale — Bits error versus c

Derivation

Split input into 4 regimes
if b_2 < -1.5492270254018601e152
1. Initial program 62.8
  \[\]
2. Simplified62.8
  \[\leadsto \]
3. Taylor expanded around -inf 9.0
  \[\leadsto \]
4. Simplified2.2
  \[\leadsto \]
if -1.5492270254018601e152 < b_2 < -4.178574910302904e-307
1. Initial program 8.8
  \[\]
2. Simplified8.8
  \[\leadsto \]
3. Using strategy rm
4. Applied div-sub8.8
  \[\leadsto \]
if -4.178574910302904e-307 < b_2 < 2.137098258150163e110
1. Initial program 33.5
  \[\]
2. Simplified33.5
  \[\leadsto \]
3. Using strategy rm
4. Applied flip--33.5
  \[\leadsto \]
5. Simplified16.3
  \[\leadsto \]
6. Simplified16.3
  \[\leadsto \]
7. Using strategy rm
8. Applied distribute-rgt-neg-out16.3
  \[\leadsto \]
9. Applied distribute-frac-neg16.3
  \[\leadsto \]
10. Applied distribute-frac-neg16.3
  \[\leadsto \]
11. Simplified8.4
  \[\leadsto \]
if 2.137098258150163e110 < b_2
1. Initial program 59.7
  \[\]
2. Simplified59.7
  \[\leadsto \]
3. Using strategy rm
4. Applied flip--59.7
  \[\leadsto \]
5. Simplified32.7
  \[\leadsto \]
6. Simplified32.7
  \[\leadsto \]
7. Using strategy rm
8. Applied distribute-rgt-neg-out32.7
  \[\leadsto \]
9. Applied distribute-frac-neg32.7
  \[\leadsto \]
10. Applied distribute-frac-neg32.7
  \[\leadsto \]
11. Simplified30.8
  \[\leadsto \]
12. Taylor expanded around inf 6.6
  \[\leadsto \]
13. Simplified2.5
  \[\leadsto \]
Recombined 4 regimes into one program.
Final simplification6.5
\[\leadsto \]

Reproduce

herbie shell --seed 2020190 
(FPCore (a b_2 c)
  :name "quad2p (problem 3.2.1, positive)"
  :precision binary64
  (/ (+ (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a))