Average Error: 34.5 → 6.9
Time: 5.3s
Precision: binary64
\[\]
\[\]

Error

Bits error versus a

Bits error versus b_2

Bits error versus c

Derivation

  1. Split input into 4 regimes
  2. if b_2 < -1.8605498001882586e27

    1. Initial program 34.5

      \[\]
    2. Simplified34.5

      \[\leadsto \]
    3. Using strategy rm
    4. Applied div-inv34.6

      \[\leadsto \]
    5. Taylor expanded around -inf 6.2

      \[\leadsto \]
    6. Simplified6.2

      \[\leadsto \]

    if -1.8605498001882586e27 < b_2 < -3.670160880532066e-242

    1. Initial program 8.8

      \[\]
    2. Simplified8.8

      \[\leadsto \]
    3. Using strategy rm
    4. Applied div-inv9.0

      \[\leadsto \]

    if -3.670160880532066e-242 < b_2 < 3.6240060206103599e133

    1. Initial program 32.2

      \[\]
    2. Simplified32.2

      \[\leadsto \]
    3. Using strategy rm
    4. Applied flip--32.3

      \[\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. Simplified9.0

      \[\leadsto \]

    if 3.6240060206103599e133 < b_2

    1. Initial program 62.1

      \[\]
    2. Simplified62.1

      \[\leadsto \]
    3. Using strategy rm
    4. Applied flip--62.1

      \[\leadsto \]
    5. Simplified35.4

      \[\leadsto \]
    6. Simplified35.4

      \[\leadsto \]
    7. Using strategy rm
    8. Applied distribute-rgt-neg-out35.4

      \[\leadsto \]
    9. Applied distribute-frac-neg35.4

      \[\leadsto \]
    10. Applied distribute-frac-neg35.4

      \[\leadsto \]
    11. Simplified34.2

      \[\leadsto \]
    12. Taylor expanded around inf 6.5

      \[\leadsto \]
    13. Simplified2.0

      \[\leadsto \]
  3. Recombined 4 regimes into one program.
  4. Final simplification6.9

    \[\leadsto \]

Reproduce

herbie shell --seed 2020191 
(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))