SMT-LIB proposal

[Aaron Stump]

Dear Silvio, Cesare, Cormac, Rajeev, Greg, Shaz, Sherdar, and other
smt-lib participants,

We are very pleased to participate in this engaging discussion about
the Satisfiability Modulo Theories Library.  We will take advantage of
the fact that we are adding our thoughts after those of others to try
to tie some ideas together.  Our proposal follows.

Sincerely,
Clark Barrett, barrett at cs.nyu.edu
Aaron Stump, stump at cs.wustl.edu, http://www.cs.wustl.edu/~stump/

of the CVC development team.
----------------------------------------------------------------------
TITLE: Benchmark classes for SMT-LIB

PROPOSAL: We propose that SMT-LIB be organized into different classes
of problems, called benchmark classes, where each class is defined by:

-- a signature Sigma, giving arities of function and predicate symbols,
-- a Sigma-theory T, described either axiomatically or alebraically, and
-- an (optional) syntactic restriction R on input Sigma-formulas.

A benchmark should then be a Sigma-formula satisfying the restriction R,
together with a designation as to whether that formula is believed to be
satisfiable or not in T (T-satisfiable).  A solver correctly runs the benchmark
iff it correctly indicates whether or not that benchmark is T-satisfiable.

DISCUSSION:

1. We agree with earlier proposals that all benchmark classes in
SMT-LIB should use unsorted FOL-EQ as the underlying logic.  We
resisted the temptation to include the underlying logic as part of the
definition of benchmark classes (to allow things like constructive
theories, of potential interest for program synthesis).

2. We included the signature as part of the definition of the
benchmark class, because even in unsorted FOL-EQ, it is standard to
have a signature giving the argument counts of symbols and indicating
which are predicates and which are functions.  We also agree, however,
that it is often convenient to have the signature inferred.  Thus, we
propose that whenever the signature is not explicitly provided, it
should be inferred to be the smallest signature which includes all the
symbols in the theory and the benchmark (note that it would be easy to
provide a tool to do this for solvers which require a signature).
Signatures need not be finite, but they will presumably be recursive.

3. Benchmark classes will be created in a grass-roots fashion, as
people find benchmarks that do not fit into an existing benchmark
class.  Judging by previous comments, the first benchmark classes to
be created are likely to have restrictions R on input formulas like
"quantifier-free" or "conjunction of literals".

4. Another restriction on input formulas that we think may be useful
is: "well-sorted with respect to a given sort system".  Note that this
restriction does not require the solver to implement type-checking.
It actually makes life easier for the solver, since it no longer has
to worry about ill-sorted formulas.

5. We are happy to include an if-then-else operator in the logic, as
was suggested in previous proposals (so the logic might be called
unsorted FOL-EQ-ITE).

RATIONALE: Allowing the creation of new benchmark classes will allow
researchers to include their benchmarks even if they fall in very
specialized niches that require heavy restrictions on input formulas
(e.g., for high performance).

BENEFITS FOR DEPLOYMENT: Under this proposal, the local web pages
created by SMT-LIB contributors for their benchmarks probably already
define benchmark classes.  Transitioning to a unified suite of
benchmarks might then be achieved by agreeing upon

-- a concrete syntax for unsorted FOL-EQ-ITE signatures,
-- a concrete syntax for unsorted FOL-EQ-ITE formulas,  
-- a language for describing the syntactic restrictions R.

More flexibly, we could agree simply upon a concrete syntax for
grammars defining the concrete syntax of signatures and formulas, and
then write generic tools based on these grammars for things like

-- translating between source and target languages
-- checking that a formula satisfies a given syntactic restriction