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

[Adrien Champion]

Hi all,

Just to make sure we are all talking about the same thing.
My understanding is that using push/pop generally impacts performance as it switches the solver to an incremental mode far less efficient than the normal one --to allow backtracking when popping. To me, check-sat-assuming is/should be a way for SMT solver devs to support “efficient restricted incrementality”, a feature some us are expecting eagerly.

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.

In any case, “More precisely, [check-sat-assuming] has the same effect as (push 1) … (pop 1)” page 54 seems to vague for me. Assuming what I said so far makes any sense, then:
“check-sat-assuming should be functionally equivalent to (push 1) … (pop 1). However, SMT-solver developers are encouraged to take advantage of this command to offer more efficient incremental satisfiability checks than the very permissive push/pop mechanism.”
English is not my native language, sorry if it is a bit cumbersome.

Also, apologies if my understanding is wrong :-)

Cheers,

Adrien


On Sep 27, 2014, at 6:44 PM, Jürgen Christ <christj at informatik.uni-freiburg.de> wrote:

>> The standardized get-model and check-sat-assuming look great, but I'm
>> concerned that you can't use them together. From the description of
>> check-sat-assuming on page 54:
>> 
>> "Note that after the command executes the current context does not
>> contain the assumptions anymore; as a consequence, it is not
>> meaningful, and so not permitted, to call model inspection commands
>> such as get-model or get-assignment immediately after
>> check-sat-assuming."
> 
> That seems very limiting.  Why not remove check-sat-assuming and add an assume 
> command and a clear-assumptions command?  Then, we can simply declare both 
> commands as modifications of the assertion stack and have a solution to the 
> model problem.
> 
>> In my case, I'm always interested in getting a model after a sat
>> result. So what would the workflow be like for me?
>> 
>> (check-sat-assuming a1 ... an)
>> ;; Receive sat response
>> (push 1)
>> (assert a1 ... an)
>> (check-sat)
>> (get-model)
>> (pop 1)
>> 
>> This feels cumbersome and I worry about the efficiency implications.
>> It would be nice if one could somehow inspect the model created via
>> check-sat-assuming, or at least have a command like
>> check-sat-assuming-and-get-model-if-sat. That's a bit tongue in cheek,
>> but you get the idea.
> 
> My proposal:
> 
> (assume a1 ... an)
> (check-sat)
> (get-model)
> (clear-assumptions)
> 
> I see that an assume command raises the problem of "additive" assumptions like
> (assume a1 ... an)
> (check-sat)
> (assume b1 ... bm)
> (check-sat)
> 
> But it should be easy to forbid that or implement it...
> 
> At first glance I also found an inconsistency on page 43.  The abstract values 
> are not written using (as ...), but this syntax made it into the draft.
> 
> Regards,
> 
> Jürgen
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib