=========== Version 1.2 =========== ---------------- 30-08-06 Release ---------------- This is a minor release fixing a glaring omission in both the abstract and concrete syntax rules. As given in the previous release, the syntax did not allow to declare numerals or rationals and their sort in a theory declaration (something meant to be allowed). The problem is fixed by replacing the rule: D_f ::= f s+ alpha* in Figure 4 with the rule: D_f ::= f s+ alpha* | n s alpha* | r s alpha* and the rule ::= ( + * ) in Figure 11 with the rule: ::= ( + * ) | ( * ) | ( * ) ---------------- 05-08-06 Release ---------------- This is the first release of Version 1.2 of the format, which contains 3 major changes with respect to the previous version: (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 is now called , and is now the union of and . Sort, function and predicate symbols, and theory, logic and benchmark names are now defined as indexed identifiers. (3) Rational constants of the form .0* 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 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. =========== Version 1.1 =========== ---------------- 08-04-05 Release ---------------- Minor release, with a few small fixes. The only notable change is that class in the concrete syntax now allows single quotes (') among its non-starting characters. ---------------- 18-03-05 Release ---------------- This is the first release of Version 1.1 of the format, which contains two major changes with respect to the previous version of the SMT-LIB Language: (i) There is now a new syntactical category called "logic". A logic is basically a pair of a theory and a sublanguage of SMT-LIB formulas. Benchmarks now refer to a logic instead of directly to a theory. (ii) The language does not contain the "benchmark set" category anymore. The attributes of that category have migrated to the "logic" and the "benchmark" categories. In addition, this release fills almost all the holes left in the previous document, and fixes several minor errors or typos. =========== Version 1.0 =========== ---------------- 17-09-04 Release ---------------- This is a minor release, fixing a few errors. Significant changes with respect to the previous release: p. 25, fig. 9 ::= ( + * ) replaced by ::= ( + * ) [ was meant to be ] p. 26, fig. 10 ::= ( * * ) replaced by ::= ( + * ) [* was meant to be +] ---------------- 26-07-04 Release ---------------- This is the first release of Version 1.0 of the SMT-LIB format, based on the paper: The SMT-LIB Format: An Initial Proposal, by Silvio Ranise and Cesare Tinelli. Proceedings of PDPAR'03, July 2003.