Query mode: Calls to getValue might need calling ensureSat first

[LeventErkok]

In query mode, we can issue calls to getValue to evaluate arbitrary expressions. When these are simple variables that are already in the program, all goes well. However, if we have a more complicated expression, then SBV will first send the instructions to compute this value, and then ask the solver for the value itself: But this can fail since the solver might need a check-sat call first to make sure the model is presently available.

Here's a simple example:

import Data.SBV
import Data.SBV.Control

test :: IO ()
test = runSMTWith z3{verbose=True} $ do
         a :: SArray Integer Integer <- newArray "a" Nothing
         query $ do ensureSat
                    v <- getValue (readArray (writeArray a 1 2) 1)
                    io $ print v

Currently, this produces:

*** Exception:
*** Data.SBV: Unexpected response from the solver, context: getModel:
***
***    Sent      : (get-value (s2))
***    Expected  : a value binding for kind: SInteger
***    Received  : (error "line 17 column 15: model is not available")
***
***    Executable: z3
***    Options   : -nw -in -smt2
***
***    Reason    : Solver returned an error: "line 17 column 15: model is not available"

And this is because we sent an assert after the check-sat:

[SEND] (check-sat)
[RECV] sat
[GOOD] (define-fun s0 () Int 1)
[GOOD] (define-fun s1 () Int 2)
[GOOD] (declare-fun array_1 () (Array Int Int))
[GOOD] (define-fun array_1_initializer_0 () Bool (= array_1 (store array_0 s0 s1)))
[GOOD] (define-fun s2 () Int (select array_1 s0))
[GOOD] (define-fun array_1_initializer () Bool array_1_initializer_0)
[GOOD] (assert array_1_initializer)
[SEND] (get-value (s2))
[RECV] (error "line 17 column 15: model is not available")

The fix is relatively easy: We should keep track of "how many asserts are pending,", initialized to 0, reset by any call to check-sat. And if we're issuing a get-value with outstanding asserts, we should first issue an ensureSat to make sure the solver is ready to respond.

Note that this isn't that big a deal as usually such get-values don't cause assertions: They might define new values and that's perfectly fine. But in cases where an assert is issued, then we need to make sure check-sat is called again.