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

[Tim King]

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
>
>