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

[Tinelli, Cesare]

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.