Search code examples
z3smtcvc4

Dynamically call get-value only when check-sat returns "sat"

The SMT2 standard states that calling get-value is only legal after a call to check-sat and only when check-sat returns "sat" or "unknown".

Here is a simple example of an unsat problem:

(set-option :produce-models true)
(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(declare-fun a ()(_ BitVec 4))
(declare-fun b ()(_ BitVec 4))
(declare-fun c ()(_ BitVec 4))
(declare-fun z ()(_ BitVec 4))
(assert (= #b1111 z))
(assert (= a b))
(assert (= (bvxor a z) c))
(assert (= b c))
(check-sat)
(get-value ( a ))
(get-value ( b ))
(get-value ( c ))

Since the problem is unsat, the get-value commands are illegal. Take out any one assert and it becomes sat and the get-value commands become legal. So my question is, how do you write a SMT2 script that checks the return value of check-sat and only calls get-value if it returned sat?

Illegally calling get-value is an issue for me as I am running different smt solvers in a flow and checking the program's return value and then parsing their output. CVC4 change's its return value to an error state if get-value is called illegally.

Solution

  • For CVC4 being run from the command line, add the flag

    --dump-models          output models after every SAT/INVALID/UNKNOWN
                       response [*]

    This is not as specific as get-value. This option is non-standard and CVC4 currently does not support setting this flag from the SMT2 parser. (Let us know if you would like this to be supported.)