[SMT-LIB] Version 1.2 of the format released

[Cesare Tinelli]

Hi all,

this is to announce that the document describing Version 1.2 of the 
SMT-LIB format is now available on the SMT-LIB website.
The new changes to the format with respect to the previous version are 
as previously discussed in this list, and as already reflected in the 
latest release (24-07-06) of the benchmark library.

Here is a summary of the changes:

(1) The format now allows (ad-hoc) overloading of function and
     predicate symbols.
(2) The concrete syntax now has "indexed identifiers", identifiers
     of the form a[n_1:n_2: ... :n_k] where a is an identifier in the
     previous sense and n_1,...,n_k are k>0 numerals.
     In the concrete syntax, the old non-terminal <identifier> is
     now called <simple_identifier>, and <identifier> is now
     the union of <simple_identifier> and <indexed_identifier>.
     Sort, function and predicate symbols, and theory, logic and
     benchmark names are now defined as indexed identifiers.
(3) Rational constants of the form <numeral>.0*<numeral> have been
     added to the format. Grammar-wise they are completely analogous
     to numerals.

Notable minor fixes are:

- The grammar for the concrete syntax has been slightly restructured,
   but without changing to the generated language except for the
   introduction of indexed identifiers.
- An error in Figure 4 of the document has been fixed:
   f s+ alpha  was replaced with the intended   f s+ alpha*
   p s* alpha  was replaced with the intended   p s* alpha*
- Several small changes have been made to the document to improve
   the presentation and its readability.

Best,


Silvio & Cesare