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

[David R. Cok]

I should have prefaced my list of typos etc with this: Thanks much to 
the coordinators for taking the interest to incorporate feedback from 
the last few years into a new version and taking the time to produce a 
new document.

I will work to implement the proposed (as eventually adopted) changes in 
jSMTLIB (which process may, of course, elicit more comments and 
clarifications...)

- David

On 9/27/2014 1:16 PM, Tinelli, Cesare 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