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

[Andrew Gacek]

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

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.

-Andrew

On Sat, Sep 27, 2014 at 12:16 PM, Tinelli, Cesare
<cesare-tinelli at uiowa.edu> wrote:
> Dear all,
>
> We, the SMT-LIB coordinators, have been working for some time on the next version of the SMT-LIB 2 standard to incorporate several requests from the community and fix a few issues in the current language.
> A close-to-final draft of the new version, Version 2.5, can be found at
>
>   http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-draft.pdf
>
> We are submitting this document to the community for a final feedback round. See below for a few notes on it.
>
> If you have ***any comments, corrections, suggestions or exceptions***, please send them to this list as soon as possible but no later than ***Oct 27, 2014***.
>
> We will have round of discussion on those as needed. We hope to finalize and make the new version official by Nov 15, 2014.
>
> Thanks,
>
>
> Cesare, Clark & Pascal
>
>
> ------------------------
> Notes on the new version
> ------------------------
>
> With a couple of minor exceptions, the new version is backward compatible with Version 2.0. A summary of the differences between them is provided in Section 1.1.1 of the draft.
>
> The draft is a substantial revision of the Version 2.0 document. In particular, the operational semantics of the SMT-LIB language is now provided in terms of concrete syntax. Abstract syntax is used, in the unchanged Section 5, only to describe the logical semantics of formulas.
>
> Any text specific to Version 2.5 is written in red. As with the Version 2.0 document, end notes are used to provide the rationale for salient design choices in the extension. Those too are in red.
>
> The current version does not include any changes to the way SMT-LIB logics are defined and named. In response to several requests to tame the explosion of logics, we are working on a new mechanism for that. This is a major change that requires considerable thought and discussion within the community, so it will be introduced in a later version.
>
>
>
>
>
>
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib