The postprocessors from smt-comp

postprocessors's People

Contributors

Stargazers

Watchers

postprocessors's Issues

Model validator: failed unittest and Real values.

The unit test ("QF_LIRA", "LCTES_smtopt.smt2", "model.LCTES_smtopt.cvc4-broken.smt2") now reports VALID instead of UNKNOWN. The problem seems to be that pySMT has automatic Int to Real casts beyond what the SMT-LIB standard allows.

We may also want to make more unit-tests, e.g.

(define-fun x () Real (- 1))                           ; invalid in QF_LIRA, model value in QF_LRA
(define-fun x () Real (- 1.0))                         ; model value in QF_LIRA, valid in QF_LRA
(define-fun x () Real (/ (- 1) 2))                     ; valid in QF_LIRA (automatic cast), model value in QF_LRA
(define-fun x () Real (/ (- (to_real 1)) (to_real 2))) ; model value in QF_LIRA, not valid in QF_LRA
(define-fun x () Real (/ (- 1.0) 2.0))                 ; valid in QF_LIRA and QF_LRA (but not model value)
(define-fun x () Real (- (/ 1 2)))                     ; valid in QF_LIRA and QF_LRA (but not model value)
(define-fun x () Real (- 0.5))                         ; valid in QF_LIRA and QF_LRA (but not model value)

If you interpret the standard strictly, the constants should be defined by model values, not arbitrary valid expressions. But IMHO we shouldn't be too strict here, especially since the model values vary from logic to logic and that is not very intuitive.

Recommend Projects