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

[Aina Niemetz]

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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 473 bytes
Desc: OpenPGP digital signature
URL: </pipermail/smt-lib/attachments/20140930/e0e69951/attachment.asc>