4

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.

Trevor Forentz
  • 147
  • 7

2 Answers2

3

I don't think there's a good way, if what you want is to have one "SMT" file to rule the whole transaction.

This issue comes up often in interacting with SMT-solvers from other languages. The solution I adopted is that I keep an open pipe with the solver and feed it the lines of the script, read the responses, and decide on what to send next based on the responses I get. Essentially programmed interaction. (This is what the Haskell SBV library does, for instance.)

However, I do agree that this is a pain; and it would be nice if there was an SMT2-lib sanctioned way of handling such common interaction.

alias
  • 28,120
  • 2
  • 23
  • 40
  • This is the intended interaction model for better or worse. It is not exactly clear what should be added to SMT though. Loops are clearly out of the intended scope of the language, but what about a "(check-sat :print-model-if-sat)"? I am sure Clark and Cesare would appreciate suggestions for adding simple usability features if they can fit neatly into the framework. – Tim Jun 25 '14 at 18:22
1

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.)

Tim
  • 1,008
  • 5
  • 13
  • Thanks, Tim. This solves my issue, although the initial question still stands. I suppose each solver will have it's own solution. One thing to note is that `--dump-models` requires that the produce-models option also be set from command line, not from the parser, i.e. `-m --dump-models` is required. Is this a bug? Regardless, it's a non-issue for me, but took me a bit to figure out why `--dump-models` wasn't working at first. Also: `CVC4 -h` says absolutely nothing about the `--dump-models` option. Maybe consider adding it in? – Trevor Forentz Jun 25 '14 at 22:22
  • Nevermind, `CVC4 -h` does contain a message about `--dump-models`, I just missed it initially. – Trevor Forentz Jun 25 '14 at 22:29
  • Yep, each solver will have its own solution. You can always implement Levent's suggestion for textual interaction. This is the intended use model for now. – Tim Jun 26 '14 at 23:23