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

[David R. Cok]

I concur with the following points made by other commenters, and would 
revise my proposal accordingly.

- I proposed a check-sat-assuming mode in effect after a 
check-sat-assuming command. In fact, there is already essentially a 
check-sat mode in effect after a (check-sat) command: certain commands 
are allowed in that mode, and the mode is disabled once an 
assertion-set-changing command is issued.
- Consequently, we might as well just use (check-sat) with additional 
arguments, instead of adding (check-sat-assuming...). The behavior is 
the same as before with respect to other commands, and model inspection 
commands, including get-unsat-assumptions, are allowed up to an 
assertion-set-changing command. Of course, if (check-sat) has no 
arguments, (get-unsat-assumptions) will necessarily return an empty 
list. The only difference now is the implicit pop that occurs if 
assumptions need to be removed from the context once the first 
assertion-set-changing command is received.

- I'd prefer not to add a new (assume...) command to accumulate 
assumptions prior to a (check-sat) command, but I can't claim enough 
experience with this facility to have a firm opinion. Already, to be 
used in (check-sat), an assumption (a.k.a. assertion) has to be defined 
as a constant function symbol, so it seems not a problem to list those 
explicitly in the check-sat command.

David


On 9/30/2014 11:23 AM, Aina Niemetz 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