SArray scoping issue / weird SMT error

[Torrencem]

When I try to run a very simple example with constructing and indexing an SArray:

import qualified Data.SBV as S

myArray :: S.Symbolic (S.SArray Bool Bool)
myArray = S.newArray_ Nothing

main :: IO ()
main = do
  d1 <- S.runSMT myArray

  let sboolOfInterest = S.readArray d1 S.sTrue

  b <- S.isSatisfiableWith S.z3{S.verbose = True} sboolOfInterest

  print b

errors with:

** 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 QF_BV)
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- top level inputs ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[FAIL] (define-fun s0 () Bool (select array_0 true))
example-exe: 
*** Data.SBV: Unexpected non-success response from Z3:
***
***    Sent      : (define-fun s0 () Bool (select array_0 true))
***    Expected  : success
***    Received  : (error "line 7 column 31: unknown constant array_0")
***
***    Exit code : ExitFailure (-15)
***    Executable: /opt/homebrew/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!

I'm not sure if the code I have written is correct; it is a constructed MWE from a much larger code that I'm working on, and I'm not sure if the overall structure here is flawed or not.

Obviously the error from the SMT solvers point of view is from the fact that no array_0 is being passed to it in the --- arrays --- section.

At first I thought this was a scoping issue because of the two instances of calling the SMT solver (runSMT and isSatisfiable), but I'm not sure how else to really accomplish something that looks like this because the SArray given out by SBV is wrapped in a Symbolic, so I might just be missing something simple.

[lucaspena]

This seems to work for me:

import qualified Data.SBV as S

myArray :: S.Symbolic (S.SArray Bool Bool)
myArray = S.newArray_ Nothing

getSymBool :: S.Symbolic S.SBool
getSymBool = do
  arr <- myArray
  return $ S.readArray arr S.sTrue

main :: IO ()
main = do
  b <- S.isSatisfiableWith S.z3{S.verbose = True} getSymBool
  print b

It seems that the first runSMT call will refresh the context. I'm not sure if it's possible to perform the read like you did after that function call.

[LeventErkok]

@lucaspena is correct. You're essentially "conflating" two different contexts: (1) The one created by runSMT, (2) The one created by isSatisfiableWith. These calls run in their own contexts, and when you mix/match them like this, things go haywire.

While this is not a bug (strictly speaking), it is annoying. The error message you get is utterly horrible. I'll see if I can improve that.

In the mean-time; simply stick to only one context and you should be fine. I suspect the above came from some bigger example, so if you're trying to express some other property let me know. Otherwise, this is an "incorrect" use of the API, with a horrible error message that's not really helpful at all.

[LeventErkok]

@Torrencem I've added some extra check to improve the error message. If you try your program on the latest head, you get:

*** Exception: Data.SBV: Mismatched contexts detected.
***
*** Current context: SBVContext (-1982494627262160466)
*** Mixed with     : SBVContext (-1575809082749540661)
***
*** This happens if you call a proof-function (prove/sat/runSMT/isSatisfiable) etc.
*** while another one is in execution, or use results from one such call in another.
*** Please avoid such nested calls, all interactions should be from the same context.
*** See https://github.com/LeventErkok/sbv/issues/71 for several examples.

CallStack (from HasCallStack):
  error, called at ./Data/SBV/Core/Symbolic.hs:1934:48 in sbv-10.3-5a4be265:Data.SBV.Core.Symbolic

Admittedly, this isn't ideal either; as it doesn't really point to where exactly the problem is in the code. Alas, this is the best we can do right now without getting much fancier with types; something that I've thought about in the past but the return-on-investment isn't very high. But at least the error now comes from SBV, and not from the backend SMT solver; and is hopefully descriptive enough.

[Torrencem]

This is excellent information! Much appreciated with the new error message.

I suspect the above came from some bigger example, so if you're trying to express some other property let me know.

Yes, in our full example, myArray is called as part of the initialization of some state for some component (in IO), then that state is stepped forward (pure, outside of IO), and then finally the sat call is performed (again from the top level IO). I'll have to think of a way to keep this all in one context then, hmm... a bit of a puzzle, but it's great to know that this is what the problem is!

[LeventErkok]

yes; all data-structures should be created within the same context. A new context is created when you call prove/sat/isSatisfiable etc.; i.e., anything that has a return type IO ThmResult, IO SatResult, or with runSMT which can execute queries. You can pass information from one call to one of these to the other, but the new call has to encapsulate all its data-structures and recreate them.

Note that while this is an SBV issue, it's not unique to SBV. Z3 itself has a similar "context" parameter; so even if you were programming directly in z3 API (via C/C++/Python etc.), you'd have to keep your contexts separate there as well. (With catastrophic failures ensuing in those cases too.)

[LeventErkok]

@Torrencem Just released 10.3 (https://hackage.haskell.org/package/sbv-10.3) on hackage, which improves error-messages in these cases. (amongst bunch of other changes accumulated over the last 6 months or so.)

Give it a try and let m know if you run other instances of this where SBV fails to catch context-mismatch issues.