search

kperun / SATPrakPDW

Interval Constraint Propagation strategy implementation for SMTRAT
MIT License
2 stars 0 forks source link

Check our solver with NEQ #22

Closed DavidWz closed 7 years ago

DavidWz commented 7 years ago

Check what happens if our solver is feeded with a constraint of the form Polynom != 0

If something fails, fix it! We will ignore these kind of constraints for now and only check them after we found a model.

kperun commented 7 years ago

@DavidWz , @Verdict7 . I have used the following smt file to check if our system is able to work with inequalities. On first glance it looks like it is able to handle such in-equations, but I think here we have to test even more examples. Code: (set-logic QF_LRA) (declare-fun x () Real) ; x = 3 (declare-fun y () Real) ; y = -4 (assert (and (!= (+ (* x x) (* y y)) 25) (<= (+ (* x x) (* y y)) 26) (<= (* x y) -10) (<= x 10) (>= x -10) (<= y 10) (>= y -10) ) ) (check-sat) ; sat (exit)