Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

1 files changed, 18 insertions, 2 deletions

diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 2d3b4a43a..297df1f36 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -2,7 +2,7 @@
 #
 # mktheorytraits
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2011  The CVC4 Project
+# Copyright (c) 2010-2012  The CVC4 Project
 #
 # The purpose of this script is to create theory_traits.h from a template
 # and a list of theory kinds.
@@ -14,7 +14,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2011
+copyright=2010-2012
 
 cat <<EOF
 /*********************                                                        */
@@ -55,6 +55,9 @@ theory_parametric="false"
 rewriter_class=
 rewriter_header=
 
+instantiator_class=void
+instantiator_header=
+
 theory_id=
 theory_class=
 
@@ -123,6 +126,7 @@ template<>
 struct TheoryTraits<${theory_id}> {
     typedef ${theory_class} theory_class;
     typedef ${rewriter_class} rewriter_class;
+    typedef ${instantiator_class} instantiator_class;
 
     static const bool isStableInfinite = ${theory_stable_infinite};
     static const bool isFinite = ${theory_finite};
@@ -188,6 +192,18 @@ function typerule {
   check_theory_seen
 }
 
+function instantiator {
+  # instantiator class header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+
+  instantiator_class="$1"
+  instantiator_header="$2"
+
+  theory_includes="${theory_includes}#include \"$2\"
+"
+}
+
 function properties {
   # properties property*
   lineno=${BASH_LINENO[0]}