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

[Jürgen Christ]

> 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