[SMT-LIB] Sublogics mixing reals, ints and quantifiers

[Tjark Weber]

On Sat, 2009-07-25 at 12:13 +0200, Cesare Tinelli wrote:
> Thanks for your suggestion. We are going to overhaul all current SMT- 
> LIB theories and logics as we move to Version 2 of the SMT-LIB  
> language (more on Version 2 soon). We will take this addition into  
> account as well.

May I suggest then that you add syntax for data types, type nat, type
bool (dare I mention identifying formulas and terms?), and for other
features commonly supported by SMT solvers?

The fact that there is no single, solver-independent input language that
covers these features means that one has to write custom translators for
each SMT solver that supports them separately.  This is unfortunate, as
it causes additional work and undermines the SMT-LIB's status as a
de-facto language standard.

The SMT-LIB language should arguably offer a rich set of features, even
if they are not used in any benchmark problem yet.  The SMT-LIB's
modular structure would then allow SMT solvers to implement well-defined
subsets, just like now.

Regards,
Tjark