[SMT-LIB] SMT-COMP 2010

[Clark Barrett]

======================================================================

       6th International Satisfiability Modulo Theories Competition
                               (SMT-COMP'10)

                              Edinburgh, Scotland
                                 July 2010

                            CALL FOR BENCHMARKS
                             CALL FOR ENTRANTS

======================================================================

SMT-COMP is the annual competition for Satisfiability Modulo Theories
(SMT).  The goals of SMT-COMP are to spur solver advances, collect
benchmarks, and encourage adoption of the SMT-LIB standard, through
friendly competition.  Highlights of SMT-COMP 2010 are covered below.
For the latest information, please see the SMT-COMP web page at:

http://www.smtcomp.org/

------------------------------------------
Main changes with respect to SMT-COMP 2009
------------------------------------------

- adoption of the recently announced SMT-LIB 2.0 standard.

- updates to the benchmark-selection and difficulty-computation algorithms.

- a track for concurrent solvers, to run before the regular competition.

- 5 random "check" benchmarks will be computed based on the random seed
  (and hence not known in advance by entrants).

For more detailed information please refer to the rules posted at
http://www.smtcomp.org/.

----------
Benchmarks
----------

The potential benchmark divisions for this year include all of the
divisions represented last year. We do not anticipate new divisions
this year unless quality benchmarks are collected. For detailed
descriptions of the divisions, refer to the SMT-LIB web page at
http://www.smtlib.org/

* QF_UF (Uninterpreted Functions): quantifier-free formulas whose
  satisfiability is to be decided modulo the empty theory. Each
  benchmark may introduce its own uninterpreted function and predicate
  symbols.

* QF_IDL (Integer Difference Logic): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of integer
  arithmetic.  The syntax of atomic formulas is restricted to
  difference logic, i.e. x - y op c, where op is either equality or
  inequality and c is an integer constant.

* QF_RDL (Real Difference Logic): this division is like QF_IDL, except
  that the background theory is real arithmetic.

* QF_UFIDL (Integer Difference Logic with Uninterpreted Functions):
  this division contains benchmarks in a logic which is similar to
  QF_IDL, except that it also allows uninterpreted functions and
  predicates.

* QF_LIA (Linear Integer Arithmetic): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of integer
  arithmetic.  The syntax of atomic formulas is restricted to contain
  only linear terms.

* QF_LRA (Linear Real Arithmetic): this division is like QF_LIA,
  except that the background theory is real arithmetic.

* QF_NIA (Nonlinear Integer Arithmetic): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of integer
  arithmetic.  There is no restriction to linear terms.

* QF_UFLIA (Linear Integer Arithmetic with Uninterpreted Functions):
  this division contains benchmarks in a logic which is similar to
  QF_LIA, except that it also allows uninterpreted functions and
  predicates.

* QF_UFLRA (Linear Real Arithmetic with Uninterpreted Functions):
  this division is similar to QF_LRA, except that it also allows
  uninterpreted functions and predicates.

* QF_AX (Arrays with Extensionality): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of arrays which
  includes the extensionality axiom.

* QF_AUFLIA (Linear Integer Arithmetic with Uninterpreted Functions
  and Arrays): quantifier-free formulas to be tested for
  satisfiability modulo a background theory combining linear integer
  arithmetic, uninterpreted function and predicate symbols, and
  extensional arrays.

* QF_BV (Fixed-size Bit-vectors): quantifier-free formulas over bit
  vectors of fixed size.

* QF_AUFBV (Bit-vectors with Arrays and Uninterpreted Functions):
  quantifier-free formulas over bit vectors of fixed size, with arrays
  and uninterpreted functions and predicate symbols.

* AUFLIA+p (Linear Integer Arithmetic with Uninterpreted Functions and
  Arrays, with patterns): quantified formulas to be tested for
  satisfiability modulo a background theory combining linear integer
  arithmetic, uninterpreted function and predicate symbols, and
  extensional arrays. Benchmarks include patterns for guiding
  instantiation mechanisms.

* AUFLIA-p (Linear Integer Arithmetic with Uninterpreted Functions and
  Arrays, without patterns): formulas from AUFLIA+p once all patterns
  have been removed.

* AUFLIRA (Arrays, Uninterpreted Functions, and Linear Arithmetic):
  quantifier formulas with arrays of reals indexed by integers
  (Array1), arrays of Array1 indexed by integers (Array2), and linear
  arithmetic over the integers and reals.

* UFNIA+p (Uninterpreted Functions and Nonlinear Arithmetic, patterns
  included): quantifier formulas with uninterpreted functions and
  nonlinear integer arithmetic.

* AUFNIRA (Arrays, Uninterpreted Functions, and Nonlinear Arithmetic):
  quantifier formulas with arrays of reals indexed by integers
  (Array1), arrays of Array1 indexed by integers (Array2), and
  nonlinear arithmetic over the integers and reals.

As with last year, we reserve the right to remove benchmark divisions
if we do not receive enough quality benchmarks or enough solvers in a
particular division.  If you have access to benchmarks in any of these
divisions, even if they are not in the SMT-LIB format, please contact
one of the organizers (see below).

-------
Solvers
-------

Solvers will be submitted via the SMT-Exec service
(http://www.smtexec.org/).  Please refer to http://www.smtcomp.org/
for complete details on entering the competition.

---------------
Important Dates
---------------

 * May 1:      First version of SMT-COMP 2010 benchmarks posted for 
               comment.

 * June 1:     No new benchmarks can be added after this date, but 
               problems with existing benchmarks may be fixed.

 * June 15:    Benchmark library is frozen.

 * July 8:     Final version of solvers due via SMT-Exec, including 
   (7pm ET)    system descriptions and magic numbers for pseudo-random
               selection of benchmarks.

 * July 10:    Close of two-day grace period for resubmission of  
   (7pm ET)    entries.

 * July 12:    Opening value of NYSE Composite Index used to complete 
               random seed.

 * July 14-16: Anticipated dates for the concurrent track (demonstraction). 

 * July 16-19: Anticipated dates for the sequential track (competition). 

----------
Organizers
----------

Clark Barrett   (New York University, barrett at cs.nyu.edu)
Morgan Deters   (Technical Univ. of Catalonia, mdeters at lsi.upc.edu)
Albert Oliveras (Technical Univ. of Catalonia, oliveras at lsi.upc.edu)
Aaron Stump     (The University of Iowa, astump at cs.uiowa.edu )

----------------
More Information
----------------

For details on the competition, see
http://www.smtcomp.org/

For more information on the SMT-LIB format, see
http://www.smtlib.org/

For more information about the SMT Workshop, see
http://www.cprover.org/SMT10/