Issue with initializing state with multiple symbolic arrays

[lucaspena]

Hello,

I am having an issue with a simple example using multiple symbolic arrays:

import qualified Data.SBV as S

data St = St
  { f1 :: !Arr
  , f2 :: !Arr
  } deriving Show

type Arr = S.SArray Integer Integer

freshSt :: S.Symbolic St
freshSt = do
  field1 <- S.newArray "f1" Nothing
  field2 <- S.newArray "f2" Nothing
  return $ St { f1 = field1, f2 = field2 }

test :: S.Symbolic St
test = do
  st <- freshSt
  let newSt = st { f1 = S.writeArray (f1 st) 16 10 }
  let testOut = f1Test newSt 16 10
  P.liftIO $ do
    x <- testOut
    print x
  return st

f1Test :: St -> S.SInteger -> S.SInteger -> IO S.ThmResult
f1Test st k v = S.proveWith S.z3{S.verbose = True} $ S.readArray (f1 st) k S..== v

When I call test, the smt output looks as expected, and returns Q.E.D. However, if I swap the two initialization lines in freshSt

freshSt :: S.Symbolic St
freshSt = do
  field2 <- S.newArray "f2" Nothing
  field1 <- S.newArray "f1" Nothing
  return $ St { f1 = field1, f2 = field2 }

and call test, I get the following output:

** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s0 () Int 16)
[GOOD] (define-fun s1 () Int 10)
[GOOD] ; --- top level inputs ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- arrays ---
[GOOD] (declare-fun array_0 () (Array Int Int))
[FAIL] (define-fun array_0_initializer_0 () Bool (= array_0 (store array_1 s0 s1)))
draconic-runes-exe:
*** Data.SBV: Unexpected non-success response from Z3:
***
***    Sent      : (define-fun array_0_initializer_0 () Bool (= array_0 (store array_1 s0 s1)))
***    Expected  : success
***    Received  : (error "line 10 column 60: unknown constant array_1")
***
***    Exit code : ExitFailure (-15)
***    Executable: /Users/lucas.pena/.opam/default/bin/z3
***    Options   : -nw -in -smt2
***
***    Reason    : Check solver response for further information. If your code is correct,
***                please report this as an issue either with SBV or the solver itself!

Notably, the [FAIL] line seems to attempt to initialize array_0 from array_1 which doesn't exist yet. In the successful version, the corresponding line looks like

[GOOD] (define-fun array_0_initializer_0 () Bool (= array_0 (store array_0 s0 s1)))

It seems that reading/writing from the array that was not initialized first is causing problems. I don't understand why the order of initialization of the two arrays would be an issue. Please let me know if I am misunderstanding something or using symbolic arrays incorrectly or what. Thank you.

[LeventErkok]

Which version of SBV are you using? Can you confirm it's the latest? (i.e., 10.3 from https://hackage.haskell.org/package/sbv)

The fundamental problem here is that you're mixing and matching contexts, which is not allowed. Prior versions of SBV did not enforce context-consistency, leading to confusing errors like you get above. But if you're using 10.3, you should get a proper error message.

Can you try with 10.3 and let me know if you still see an issue? (Note that you'll get an error message from SBV when you run it, but hopefully it should be self-explanatory. If not, let me know.)

[lucaspena]

Ah ok thanks, yea switching to 10.3 gets the mixing contexts error for each case. However, this arose from attempting to just read a (concrete) value from a symbolic array. First, I tried something like this:

main :: IO ()
main = S.runSMT readTest >>= print

readTest :: S.Symbolic (Maybe Integer)
readTest = do
  st <- freshSt
  let newSt = st { f1 = S.writeArray (f1 st) 16 10 }
  return $ readSym (f1 newSt) 16

readSym :: S.SArray Integer Integer -> S.SInteger -> Maybe Integer
readSym arr k = S.unliteral $ S.readArray arr k

but this prints Nothing where I would like it to print Just 10. Then I resorted to trying to "prove" the value was as expected as in my original post, but that led to the mixing contexts issue. Is there an easy way to just print out the value in a symbolic array? Provided a concrete key/value was written. Thanks, let me know.

[LeventErkok]

Once you're in a symbolic context, you cannot call a "nested" prove/sat etc. All the interactions have to be in the same context. (Note that this isn't an SBV limitation. This is just how SMT-solvers work, every model is constructed with respect to one unique context. If you mix/match them, then all bets are off.)

Also, the idea that "reading a concrete value" is a bit misleading. In a symbolic context, there are no concrete values: Until you call check-sat in the underlying prover, all you have are assertions. (Which may or may not be consistent at the point where you eventually call check-sat.) So, to do things like you want, you should start interacting with the solver instead, using the query mode. Here's an example:

import Data.SBV
import Data.SBV.Control

data St = St
  { f1 :: !Arr
  , f2 :: !Arr
  } deriving Show

type Arr = SArray Integer Integer

freshSt :: Symbolic St
freshSt = do
  field1 <- newArray "f1" Nothing
  field2 <- newArray "f2" Nothing
  return $ St { f1 = field1, f2 = field2 }

main :: IO ()
main = print =<< runSMT go
 where go = do st <- freshSt
               let newSt = st { f1 = writeArray (f1 st) 16 10 }

               readVal <- sInteger "readVal"
               constrain $ readVal .== readArray (f1 newSt) 16

               query $ do ensureSat
                          getValue readVal

This prints:

*Main> main
10

You can now use the read-value of that location and do additional assertions etc., and call check-sat again.

I should note that query mode is a bit of an advanced feature, that you shouldn't really need for basic SBV usage. In general, you don't access any value until after a model is computed, which happens at the end of a prove/sat call; at which point the context gets destroyed. The query mode example is how we stay in the same context to do additional programming with values that are computed by the solver, but for most uses of SBV it shouldn't be needed.

To sum up: No value is concrete till you call check-sat, implicitly by prove/sat, or explicitly in the query mode yourself. And you shouldn't mix/match contexts.

I hope that gets you going. Symbolic programming is a bit of a different beast, you need to carefully orchestrate what are constraints and what are regular values; and it isn't always easy to tell which. As a rule of thumb, if you ever feel like you need to call unliteral yourself, you're probably modeling the problem incorrectly. Calls to unliteral shouldn't be needed by end-user programs. (It's useful for internal SBV programming, but that's a whole another topic.)

[lucaspena]

Ok, thank you, this is certainly very helpful. This issue arose from a larger program where I was trying to inspect the state as an intermediate step. I see now that's not really possible the ways I was trying before, since the context gets destroyed at each prove/runSMT/checkSat/etc call. I think I have a better understanding as to how to go about this now, though I may post a new issue if I have further questions. I really appreciate your prompt and in-depth responses, thanks again!

[LeventErkok]

If you need to inspect intermediate values to constrain further values then query is the way to go. It can be finicky to use the query mode, as it's definitely a lower-model of programming, but perhaps your use case calls for it. There are some query examples on hackage: See the examples under Documentation.SBV.Examples.Queries.

I'm closing this ticket, but feel free to open others if you run into issues. Note that the stack-overflow forum has an sbv tag which is more appropriate for questions about SBV. (And issue tracker is better suited for bug reports.) See here: https://stackoverflow.com/questions/tagged/sbv