[SMT-LIB] New version of the SMT-LIB standard

[Cesare Tinelli]

Dear all,

a while ago the coordinators of the SMT-LIB initiative established a  
few work groups with the goal of improving the functionality and  
usability of the SMT-LIB standard in response to the requests and  
needs of the SMT-LIB user community.

The new standard would streamline and improve the current basic  
language for specifying theories, sublogics and benchmarks, and would  
define a command language for interactive session with SMT solvers.  
The command language would also include provisions for querying  
solvers on models for a satisfiable input formula or refutation  
proofs for an unsatisfiable one.

The following work groups were created:

SMT-LOGIC, in charge of Version 2 of the new basic logic and language
SMT-API, in charge of the new command language, including the model  
querying aspects
SMT-PROOF, focusing just on the output proof format for the command  
language

After much discussion within the work groups and with external users  
(as well as long intervals of inactivity due to everybody being busy  
with other things :) ), we are ready to propose to the SMT-LIB  
community:
(i) a Version 2 of the basic logic and language and
(ii) an initial version of the command language.

A draft presenting and discussing (i) is coming in the next message  
to this list. Drafts for (ii) will be sent in the next few of days.  
We ask your feedback on all of them.

Our goal for the next 1-2 months is to collect additional comments  
and suggestions on (i) and (ii) from members of this list, answer any  
questions on the proposals and the rationale for their many design  
decisions, and adjust the proposals as needed before producing  
official documents on the new standard.

Best,


The SMT-LIB coordinators
Clark Barrett,
Aaron Stump, and
Cesare Tinelli