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

[David R. Cok]

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