Symbolic Evaluator

[abdoo8080]

We should add sevals to immediately solve problems like the following:

(set-info :smt-lib-version 2.6)
(set-info :category "crafted")
(set-info :source |Christoph M. Wintersteiger (cwinter@microsoft.com). Randomly generated floating-point testcases.|)
; Rounding mode: to negative
; Precision: double (11/53)
; X = -1.355355640892073498804393238970078527927398681640625p-550 {- 1600379531905546 -550 (-3.67753e-166)}
; Y = 1.8675408139965694598316758856526575982570648193359375p-949 {+ 3907056486643647 -949 (3.92468e-286)}
; -1.355355640892073498804393238970078527927398681640625p-550 + 1.8675408139965694598316758856526575982570648193359375p-949 == -1.355355640892073498804393238970078527927398681640625p-550
; [HW: -1.355355640892073498804393238970078527927398681640625p-550] 

; mpf : - 1600379531905546 -550
; mpfd: - 1600379531905546 -550 (-3.67753e-166) class: Neg. norm. non-zero
; hwf : - 1600379531905546 -550 (-3.67753e-166) class: Neg. norm. non-zero

(set-logic QF_FP)
(set-info :status unsat)
(define-sort FPN () (_ FloatingPoint 11 53))
(declare-fun x () FPN)
(declare-fun y () FPN)
(declare-fun r () FPN)
(assert (= x (fp #b1 #b00111011001 #b0101101011111000100101100101100000010100101000001010)))
(assert (= y (fp #b0 #b00001001010 #b1101111000010111001001111010000000001111011110111111)))
(assert (= r (fp #b1 #b00111011001 #b0101101011111000100101100101100000010100101000001010)))
(assert  (not (= (fp.add roundTowardNegative x y) r)))
(check-sat)
(exit)