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

[Andrew Gacek]

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

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.

-Andrew