Skolemization issue using constrain in query

[bts]

Hi Levent,

I have some code that was working fine until I moved a constrain from outside, to inside, the use of query.

It seems likely that the problem is related to skolemization bookkeeping?

module Issue where

import Data.SBV
import Data.SBV.Control

issue :: Symbolic CheckSatResult
issue = do
  x <- forall_ :: Symbolic (SBV Bool)
  y <- exists_ :: Symbolic (SBV Bool)
  query $ constrain y *> checkSat

main :: IO ()
main = putStrLn . show =<< runSMTWith z3 issue

*** Data.SBV: Unexpected response from the solver, context: assert:
***
***    Sent      : (assert s1)
***    Expected  : success
***    Received  : (error "line 13 column 8: invalid function application, missing arguments s1")
***
***    Executable: z3
***    Options   : -nw -in -smt2

If I move the constrain back outside of query, things work as expected:

works :: Symbolic CheckSatResult
works = do
  x <- forall_ :: Symbolic (SBV Bool)
  y <- exists_ :: Symbolic (SBV Bool)
  constrain y
  query checkSat

Sat

I can reproduce this for both sbv 7.8 and HEAD.

Thanks,
Brian

[LeventErkok]

Good catch. In fact, the issue isn't that skolemization isn't working (it actually is), but access from the query portion to any skolemized variable is something we cannot support. Consider:

issue :: Symbolic (Bool, Bool)
issue = do
  x :: SBool <- forall_
  y :: SBool <- exists_
  constrain y
  query $ do checkSat
             (,) <$> getValue x <*> getValue y

This requests both x and y, but at this point in the query x is hidden inside the quantifier. (Worse than y, which is at least still available at the top-level.) If you inspect the generated code you can see this: (Simplified and annotated:)

(declare-fun s1 (Bool) Bool)   ; s1 is the function that corresponds to the skolemized 'y'
(assert (forall ((s0 Bool))    ; s0 is 'x'
            (s1 s0)))          ; s1 applied to s0 is the actual 'y'
(check-sat)
(get-value (s0))        ; s0 simply not visible here
(get-value (s1))        ; s1 is visible, but only via 's1 s0', so it is also not available.

The right thing to do is to recognize if there are quantifiers and reject user queiries if they are present.

@bts Before I implement this (and reject the query dynamically), I want to double check: Is there an actual use case here that we should consider, or is this a mere curioisty? (i.e., is recognizing and rejecting these cases with an error message acceptable?)

[bts]

Thanks a lot for looking into this.

There is indeed a use-case, but I suspect there's probably another way that we can achieve our goal. Ultimately the primary motivation is that @joelburget and I are trying to reuse work with push & pop (inNewAssertionStack), for which we need query mode. We're performing symbolic evaluation of programs, and for each program, we want to validate multiple properties (one at a time). Instead of re-analyzing our program for every single property, we want to perform the program analysis only once, and then introduce temporary stack frames to test each property. Our properties utilize universal and existential quantification.

Before this refactor, we had been using output for each property. output is defined with respect to Symbolic (e.g. instead of living on SolverContext typeclass and being stack-aware, which I don't know would even be possible) so with our desired use of push/pop, we've tried moving to using constrain more manually.

See this (very rough) pseudocode:

results = runSMTWith z3 $ do
  analyzeProgram program -- this accumulates constraints along the way
  preds <- analyzeProperties properties -- these can use any quantifiers. this never calls 'constrain'
  query $
    for preds $ \pred ->
      inNewAssertionStack $ do
        -- Note that we can't use 'output' here. Also this is the problematic 'constrain'
        -- in the face of quantifiers:
        constrain $ bnot pred
        queryResult -- uses checkSat and extracts a falsifying model, if applicable

If it were possible to use output in query mode (i.e. output were "stack aware") then it would look like:

results = runSMTWith z3 $ do
  analyzeProgram program -- this accumulates constraints along the way
  preds <- analyzeProperties properties -- these can use any quantifiers. this never calls 'constrain'
  query $
    for preds $ \pred ->
      inNewAssertionStack $ do
        -- this output would be "rolled back" between stack frames. normally instead
        -- of manually negating the output, we'd use valid (vs sat mode), but let's ignore that:
        output $ bnot pred
        queryResult -- uses checkSat and extracts a falsifying model, if applicable

While we're using stacks now, we would like to introduce constraint vacuity checking if possible. We can add this to either of the two above approaches, but we notice that if we add it to our latter/output approach, we are now using constrain in a query again, making our fancier stack-aware output moot; the constrain in query will again be problematic in the face of quantifiers:

results = runSMTWith z3 $ do
  analyzeProgram program -- this accumulates constraints along the way
  preds <- analyzeProperties properties -- these can use any quantifiers. this never calls 'constrain'
  query $
    for preds $ \pred -> do
      inNewAssertionStack $ do
        -- this 'constrain' is problematic in the face of quantifiers:
        constrain pred
        checkConstraintVacuity -- uses checkSat
      inNewAssertionStack $ do
        -- this output would be "rolled back" between stack frames:
        output $ bnot pred
        queryResult -- uses checkSat and extracts a falsifying model, if applicable

Thank you again for all of your help! It's very much appreciated.

[LeventErkok]

Unfortunately, I don't see an easy/safe way to support both user queries and quantifiers at the same time. The issue is rather historical: Support for quantifiers in SBV has always been such that they scoped over the entire program. In the early days, this was the easiest thing to do. In hindsight, however, this isn't quite right: When quantifiers are used in SMTLib, they are usually intended for small delimited assertions. The scoping rules we have for quantifiers just don't match their intended use case.

I'm not sure how to go about solving your issue; but I'd question if quantifiers are really necessary. Would be best to avoid them if at all possible. An isolated replicable example might help clarify.

In the meantime, I will go ahead and make the changes to reject user queries if quantifiers are present. This is the safe thing to do, though I do understand it doesn't really help you at all.

[LeventErkok]

@bts We now catch and reject these cases:

*** Exception:
*** Data.SBV: Unsupported query call in the presence of quantified inputs.
***
*** The following variable requires explicit quantification:
***
***    x
***
*** While quantification and queries can co-exist in principle, SBV currently
*** does not support this scenario. Avoid using quantifiers with user queries
*** if possible. Please do get in touch if your use case does require such
*** a feature to see how we can accommodate such scenarios.

I know this isn't ideal for you, but I feel it's the right thing to do.

When you have an isolated use case, please report that as a seperate ticket and see if we can somehow relax this restriction. Till that time, I'm inclined to reject all quantification if we go into user queries. Thanks for reporting.

[bts]

Thanks Levent. I agree that this is the right thing to do.

In our case, unfortunately we are nearly certain that quantifiers are necessary. It's okay though; we can survive without query mode, and if we need speed-ups, we can try resorting to concurrency. Thanks again for your help!