[SMT-LIB] check-sat-assuming - Was: Re: Draft of SMT-LIB 2.5: request for feedback

Tue Sep 30 15:44:55 EDT 2014

Unless I’m very mistaken:

The current definition of check-sat-assuming is confusing. The point of this command is to avoid information loss (in particular for cdcl) on pop as requested by (a part of) the model checking community —and possibly others— to make the most of activation literals. So check-sat-assuming should not be implemented with push/pop.

In practice, the semantics of (check-sat-assuming a1 … an) for the SMT solver should be something like:
 - force DPLL(T) to decide true for a1 … an
 - (1) forbid backtracking the forced decisions on a1 … an
 - run normal DPLL(T), resulting in sat or unsat
 - remove constraint (1) and return the result

If the result is sat, then the model is obviously a model for the assertion set, it is simply “directed” by a1…an. There is thus no inconsistency in doing model exploration.
If it is unsat then requesting an unsat core is arguably inconsistent with the assertion set, but should still be allowed because of how valuable the core is for the user.

As Andrew pointed out, this is how z3 currently works except the command is simply (check-sat a1 … an). Well, I don’t know if the semantics I gave to check-sat-assuming correspond exactly to how z3 works internally but it sure looks like it’s close.
Andrew is already using it, and so am I for k-induction in kind2. And as he said “it works very well in practice”.

Does this make any sense?

Adrien

On Sep 30, 2014, at 10:23 AM, Aina Niemetz <aina.niemetz at jku.at> wrote:

> Hi all,
> 
> I second David's and Jürgen's (and consequently Tim's) suggestions,
> which in a sense come very close to how assumptions are handled in SAT.
> 
> I don't see the need for an extra (check-sat-with-assumptions) command,
> as it seems somewhat redudant (see Tim's point 2). I'd therefore propose
> to introduce an assume command (as Jürgen suggested), let (check-sat)
> (internally) handle assumptions (if given), and implicitly (pop) on all
> commands that alter the internal state of the solver.
> 
> E.g.,
> 
> (assume a1 ... an)  --> assumption-list: {a1, ..., an}
> (check-sat)
> (get-model)
> (assume b1 ... bm)  --> implicit pop, assumption-list: {b1, ..., bm}
> (assert c1)         --> assumption-list still {b1, ..., bm}
> (check-sat)
> (get-model)
> (assert d1)         --> implicit pop, assumption-list: {}
> (get-model)
> 
> Let me point out that introducing an (assume) command has one big
> advantage over (check-sat <term>*) and consequently,
> (check-sat-with-assumptions: it is possible to alternately issue
> (assume) and (assert) commands until (check-sat) is called (see the
> example above). This is NOT possible with either of (check-sat <term>*)
> and (check-sat-with-assumptions).
> 
> The solution proposed above is thererfore much more flexible.
> 
> I agree with Tim that this may be a little cumbersome to incorporate
> into the standard, but maybe (as Tim suggested) a list of commands that
> alter (or do not alter, whichever is shorter) the internal state might
> make it a little easier.
> 
> My proposal is maybe motivated by the fact that the above is exactly how
> assumptions are implemented in Boolector (even though we currently do
> not support (push) and (pop) via smtlib2 input, we support
> incrementality and assumptions via the API).
> 
> Aina
> 
> 
> On 09/30/2014 04:19 PM, Tim King wrote:
>> Dear Cesare, Clark, Pascal and the rest of the SMT list,
>> 
>> I would like to second David's proposal. (I was in the process of writing
>> an equivalent proposal myself.) I believe David has not properly sold its
>> strengths. I think David's proposal (which I call the "implicit pop"
>> solution) has a number of advantages over the current proposal (which I
>> will call the "macro" solution):
>> 
>> 1) It keeps the stateful model of (check-sat) and
>> (check-sat-with-assumptions ...) exactly the same. I think this is *very*
>> important as users are going to expect and want the interaction of various
>> solvers states queries (models, proofs, values, etc.) for both and will
>> expect both to have the same stateful model. The solver may internally want
>> the state for check-sat with/without assumptions to be different, but the
>> user will not expect these to change.
>> 
>> 2) (check-sat) can instead be an synonym for "(check-sat-with-assumptions)"
>> i.e. an empty list of assumptions. This may simplify the standard author's
>> lives if they wish to take advantage of it. I see no problem with returning
>> the empty list of assumptions as the unsat core of (check-sat). (Returning
>> an empty list is already going to happen with non-empty lists of
>> assumptions i.e. the assert statements without the assumptions are unsat.)
>> 
>> 3) The dangling pop already must already be in some sense supported. For
>> the solver to support queries about models, proofs, etc., the solver to
>> keep around the objects to query. These objects need to be potentially
>> modified (conservatively speaking thrown out) at the next command that
>> changes the assertion stack (the set of functions) in order to be sound.
>> Now not all solvers must support these features to be compliant, but those
>> solvers can also chose not to support them with assumptions either.
>> Perhaps, some authors may also wish to not allow these features with
>> assumptions but allow them with (check-sat)? In which case, these solvers
>> are free to internally use the macro solution.
>> 
>> 4) The changes to the solver interface are minimal and are not likely to
>> need to be changed again in the future. The macro proposal is not going to
>> last because of the obvious user demand for models (see 1).
>> 
>> I appreciate that David's "implicit dangling pop" may be a bit cumbersome
>> to weasel into the standard so that the assumptions can be defined via
>> assert commands. The simplest solution I have heard is to explicitly list
>> the commands that force the "dangling pop" in the standard. (Alternatively,
>> the ones it skips.) The current proposed command is much simpler. But I
>> think that if (check-sat-with-assumptions ...) is going to be added, it
>> ought to be added in a way such that it not immediately inadequate for the
>> users of the feature.
>> 
>> Jurgen's suggestion also has a lot of merit. It does however requires
>> adding more commands and increasing the size of the user interface. So I
>> think that the idea will take some time to iron out. So maybe this is a
>> good idea for the next draft?
>> 
>> Cheers,
>> Tim
>> 
>> On Sun, Sep 28, 2014 at 10:21 PM, David R. Cok <dcok at grammatech.com> wrote:
>> 
>>> Without offering an opinion on whether the change suggested in this thread
>>> should be made, I would propose the following.
>>> - As I understand it, having a means to temporarily state some assertions
>>> and check the satisfiability in the current context has efficiency
>>> advantages over the equivalent push...pop sequence stated in the document.
>>> - But that makes it impossible or cumbersome to inspect any resulting
>>> model.
>>> - Here is a suggested design that requires fewer syntactic changes than
>>> those suggested so far
>>> ** Issuing a (check-sat-assuming ...) command is equivalent to a (push 1)
>>> (assert ...)(check-sat) sequence but also puts the solver in a
>>> check-sat-assuming mode.
>>> ** In check-sat-assuming mode, get-option, get-info, and proof and model
>>> inspection commands are permitted (both unsat and set varieties) if they
>>> would be permitted after a (check-sat) command
>>> ** The first of any other commands, e.g. a subsequent (assert ...) or
>>> (declare-fun...) or (set-option...),  is implicitly preceded by a (pop 1)
>>> command that restores the solver to the state prior to the
>>> (check-sat-assuming ...) command (and exits the check-sat-assuming mode).
>>> 
>>> - David
>>> 
>>> On 9/28/2014 12:55 PM, Adrien Champion wrote:
>>> 
>>>> So if this is what check-sat-assuming is for, then my proposal is the
>>>>>> following:
>>>>>> (check-sat-assuming (<command>*))
>>>>>> where <command>  is in some subset of the SMT-LIB commands.
>>>>>> This set should be side-effect-free for the solver, i.e. should not
>>>>>> include declare-fun define-fun…
>>>>>> It should allow get-unsat-core, get-model and get-value to be useable
>>>>>> for model checking.
>>>>>> 
>>>>> One problem with this approach is that it requires you to know ahead
>>>>> of time all the commands you want to execute. As a simple example,
>>>>> even doing
>>>>> 
>>>>> (check-sat-assuming a1 ... an (get-model))
>>>>> 
>>>>> Would lead to an error when the check-sat-assuming returns unsat.
>>>>> 
>>>> Right, then something like
>>>> (check-sat-assuming a1 … aN (<commandIfSat>*) (<commandIfUnsat>*))
>>>> might make more sense. Actually, the following might be simpler and
>>>> better:
>>>> (check-sat-assuming a1 … aN (<exprToEvaluateIfSat>*)
>>>> (<unsatCoreFlagIfUnsat>))
>>>> But as you pointed out,
>>>> 
>>>>> In more advanced situations, you may want to execute a series of
>>>>> get-value commands where the values you are interested in depend on
>>>>> previous values returned from the model.
>>>>> 
>>>> Touché. Also it’s not very elegant.
>>>> 
>>>> My preference would be for check-sat-assuming to act just like
>>>>> check-sat and allow you to do arbitrary get-model, get-value, etc
>>>>> commands afterwards. In fact, it's not clear from the document why
>>>>> this isn't the case. Is there a performance concern? Or is there some
>>>>> useful invariant which this would break?
>>>>> 
>>>>> Currently Z3 allows check-sat-assuming (but still calls it check-sat)
>>>>> and then you can run model inspection commands afterwards. I find this
>>>>> works very nicely in practice.
>>>>> 
>>>> I concur, and that’s also what I use. It also allows get-unsat-core by
>>>> the way.
>>>> 
>>>> I think check-sat-assuming tries to prevent working with a context that
>>>> is not consistent with what is actually asserted in the solver --as is the
>>>> case with the z3 solution-- in a very restrictive way. So restrictive most
>>>> of us would probably not use it.
>>>> Jürgen’s proposal and mine aim at keeping this consistency but are more
>>>> permissive. They raise other issues however and wouldn’t fit every use
>>>> case, as you pointed out.
>>>> 
>>>> Adrien
>>>> 
>>>> _______________________________________________
>>>> SMT-LIB mailing list
>>>> SMT-LIB at cs.nyu.edu
>>>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>>> 
>>> 
>>> _______________________________________________
>>> SMT-LIB mailing list
>>> SMT-LIB at cs.nyu.edu
>>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>> 
>>> 
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>> 
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib