Average Error: 12.6 → 9.7
Time: 32.6s
Precision: binary64
\[\]
↓
\[\]

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Bits error versus b

Bits error versus c

Bits error versus i

Bits error versus j

Target

Original12.6
Target16.4
Herbie9.7
\[\]

Derivation

  1. Split input into 3 regimes

  2. if y < -2.97181150100609534e-117 or 1.26727423582944899e67 < y

    1. Initial program 16.5

      \[\]
    2. Using strategy rm

    3. Applied sub-neg16.5

      \[\leadsto \]

    4. Applied distribute-lft-in16.5

      \[\leadsto \]

    5. Simplified16.5

      \[\leadsto \]

    6. Simplified12.6

      \[\leadsto \]
    7. Using strategy rm

    8. Applied add-cube-cbrt12.9

      \[\leadsto \]
    9. Using strategy rm

    10. Applied sub-neg12.9

      \[\leadsto \]

    11. Applied distribute-lft-in12.9

      \[\leadsto \]

    12. Simplified8.8

      \[\leadsto \]

    13. Simplified8.8

      \[\leadsto \]

    if -2.97181150100609534e-117 < y < 1.2488829962253369e-200 or 223028217536890110 < y < 1.26727423582944899e67

    1. Initial program 10.1

      \[\]
    2. Using strategy rm

    3. Applied sub-neg10.1

      \[\leadsto \]

    4. Applied distribute-lft-in10.1

      \[\leadsto \]

    5. Simplified9.8

      \[\leadsto \]

    6. Simplified9.7

      \[\leadsto \]

    if 1.2488829962253369e-200 < y < 223028217536890110

    1. Initial program 8.4

      \[\]
    2. Using strategy rm

    3. Applied sub-neg8.4

      \[\leadsto \]

    4. Applied distribute-lft-in8.4

      \[\leadsto \]

    5. Simplified9.4

      \[\leadsto \]

    6. Simplified11.7

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

  4. Final simplification9.7

    \[\leadsto \]

Reproduce

herbie shell --seed 2020180 
(FPCore (x y z t a b c i j)
  :name "Linear.Matrix:det33 from linear-1.19.1.3"
  :precision binary64

  :herbie-target
  (if (< t -8.120978919195912e-33) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j))) (if (< t -4.712553818218485e-169) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (/ (* j (- (pow (* c t) 2.0) (pow (* i y) 2.0))) (+ (* c t) (* i y)))) (if (< t -7.633533346031584e-308) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j))) (if (< t 1.0535888557455487e-139) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (/ (* j (- (pow (* c t) 2.0) (pow (* i y) 2.0))) (+ (* c t) (* i y)))) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j)))))))

  (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (* j (- (* c t) (* i y)))))