Announcing Version 2.7 of SMT-LIB

[Cesare Tinelli]

Hi all,

We are happy to announce a new version of the SMT-LIB standard, Version 2.7.
The main difference with Version 2.6 is the inclusion of two extensions
to the SMT-LIB base logic:

1. Support for a form of prenex polymorphism in user-defined sorts and functions.
   
2. An extension to higher-order logic syntax obtained with the introduction  of a theory of maps (called HO-Core).

Aside from the new functionality, which required introducing a new command and
assigning special meaning to the symbols _, lambda, and ->, Version 2.7 is
fully backward-compatible with Version 2.6 and is designed to ease the transition
to the upcoming Version 3, whose base logic will be a higher-order logic
with dependent (and polymorphic) types.

We thank Andrew Jones, Nikolaj Bjørner, and Andrew Reynolds for proposing a
transitional version to SMT-LIB 3. Special thanks go to Nikolaj Bjørner and
Andrew Reynolds for their feedback and useful suggestions. We also thank
Haniel Barbosa, Guillaume Bury, and Levent Erkök for their feedback on the
reference document and the standard, and Andrei Paskevich and Jasmin Blanchette
for illuminating conversations on the semantics of logics with polymorphism.

Best,

Cesare, Clark, and Pascal

SMT-LIB coordinators