[SMT-LIB] new quantified benchmarks

[Cesare Tinelli]

Hi all,

courtesy of Bernd Fischer (who provided them) and Yeting Ge (who 
translated them into CVC format) we will soon have about 28,000 
quantified benchmarks over a theory combining integers, reals, arrays 
and free symbols.

FYI, here is a formalization of the theory and related logic.

We anticipate that the logic will become a division in SMT-COMP.

Best,


Clark and Cesare

-------------------------------------------------

(theory ArrayIntArrayIntReal

  :written_by {Cesare Tinelli}
  :date {10/05/05}

  :sorts (Int Array1, Array2)

  :funs ((0 Int)
         (1 Int)
         (- Int Int)     ; unary minus
         (- Int Int Int) ; binary minus
         (+ Int Int Int)
         (* Int Int Int)

  :preds ((<= Int Int)
          (< Int Int)
          (>= Int Int)
          (> Int Int)
         )

  :funs ((0.0 Real)   ; requires extending SMT-LIB grammar
         (1.0 Real)   ; requires extending SMT-LIB grammar
         (- Real Real)      ; unary minus
         (- Real Real Real) ; binary minus
         (+ Real Real Real)
         (* Real Real Real)
        )

  :preds ((<= Real Real)
          (< Real Real)
          (>= Real Real)
          (> Real Real)
         )

  :funs ((select Array1 Int Real)
         (store Array1 Int Real Array1)

         (select Array2 Int Array1)
         (store Array2 Int Array1 Array2)
        )


  :definition
  "This is a theory of functional arrays (with extensionality) with sort
   name Array1, integer indeces and real elements, plus arrays with sort
   name Array2, integer indeces and Array1 elements.
   It can be formally defined as the union of the following variants of
   the SMT-LIB theories Int and ArraysEx produced by these signature
   morphisms:

   - the trivial variant of Int produced by the identity morphism;

   - the variant of Real produced by the morphism mapping
     0 to 0.0 and 1 to 1.0, and every other symbol to itself;

   - the variant of ArraysEx produced by the morphism mapping
     Index to Int, Element to Real, and every other symbol to itself;

   - the variant of ArraysEx under the morphism mapping
     Index to Int, Element to Array, and every other symbol to itself;
"
)


(logic AUFLIRA

:written_by {Cesare Tinelli}
:date {10/05/2006}

:theory ArrayIntArrayIntReal

:language
  "Closed formulas built over an arbitrary expansion of the
   ArrayIntArrayIntReal signature with free function and
   predicate symbols but containing only linear atoms, that is,
   atoms with no occurrences of the function symbol * (but see
   the notational conventions below).

   Formulas in ite terms must satisfy the same restriction, with the
   exception that they need not be closed.
  "

:extensions
  "As in the logic QF_LIA and QF_LRA, with difference that numerals
   for real numbers must end with .0 (as in 5.0)."