[SMT-LIB] Draft of SMT-LIB 2.5: request for feedback

[Adrien Champion]

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