Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

3 files changed, 74 insertions, 5 deletions

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 6dd4e78f3..568f3bb92 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -244,6 +244,19 @@ annotatedFormula[CVC4::Expr& expr]
       }
     }
 
+  | /* A quantifier */
+    LPAREN_TOK
+    ( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } )
+    { PARSER_STATE->pushScope(); }
+    ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK
+      { args.push_back(PARSER_STATE->mkVar(name, t)); }
+    )+
+    annotatedFormula[expr] RPAREN_TOK
+    { args.push_back(expr);
+      expr = MK_EXPR(kind, args);
+      PARSER_STATE->popScope();
+    }
+
   | /* A non-built-in function application */
 
     // Semantic predicate not necessary if parenthesized subexpressions
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index c3b81655c..4d3c1d086 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -29,6 +29,10 @@ namespace parser {
 
 std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newLogicMap() {
   std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap;
+  logicMap["AUFLIA"] = AUFLIA;
+  logicMap["AUFLIRA"] = AUFLIRA;
+  logicMap["AUFNIRA"] = AUFNIRA;
+  logicMap["LRA"] = LRA;
   logicMap["QF_AX"] = QF_AX;
   logicMap["QF_BV"] = QF_BV;
   logicMap["QF_IDL"] = QF_IDL;
@@ -54,6 +58,9 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   logicMap["QF_UFNIRA"] = QF_UFNIRA;
   logicMap["QF_AUFLIA"] = QF_AUFLIA;
   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
+  logicMap["UFNIA"] = UFNIA;
+  logicMap["UFNIRA"] = UFNIRA;
+  logicMap["UFLRA"] = UFLRA;
   logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED;
   logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
   return logicMap;
@@ -109,6 +116,22 @@ void Smt::addTheory(Theory theory) {
     break;
   }
 
+  case THEORY_BITVECTOR_ARRAYS_EX: {
+    Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)");
+    //addOperator(kind::SELECT);
+    //addOperator(kind::STORE);
+    break;
+  }
+
+  case THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX: {
+    defineType("Array1", getExprManager()->mkArrayType(getSort("Int"), getSort("Real")));
+    defineType("Array2", getExprManager()->mkArrayType(getSort("Int"), getSort("Array1")));
+    addOperator(kind::SELECT);
+    addOperator(kind::STORE);
+    break;
+  }
+
+  case THEORY_INT_ARRAYS:
   case THEORY_INT_ARRAYS_EX: {
     defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
 
@@ -140,6 +163,9 @@ void Smt::addTheory(Theory theory) {
   case THEORY_BITVECTORS:
     break;
 
+  case THEORY_QUANTIFIERS:
+    break;
+
   default:
     Unhandled(theory);
   }
@@ -244,13 +270,14 @@ void Smt::setLogic(const std::string& name) {
     break;
 
   case QF_AUFLIRA:
-    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
     addUf();
     addTheory(THEORY_INTS);
     addTheory(THEORY_REALS);
     break;
 
   case ALL_SUPPORTED:
+    addTheory(THEORY_QUANTIFIERS);
     /* fall through */
   case QF_ALL_SUPPORTED:
     addTheory(THEORY_ARRAYS_EX);
@@ -261,14 +288,41 @@ void Smt::setLogic(const std::string& name) {
     break;
 
   case AUFLIA:
+    addUf();
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_INT_ARRAYS_EX);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+
   case AUFLIRA:
   case AUFNIRA:
+    addUf();
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+
   case LRA:
-  case UFLRA:
   case UFNIA:
-    Unhandled(name);
+    addUf();
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+  case UFNIRA:
+    addUf();
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+
+  case UFLRA:
+    addUf();
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
   }
-}
+}/* Smt::setLogic() */
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index d77808930..7b1dfc345 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -65,6 +65,7 @@ public:
     QF_UFNIRA, // nonstandard
     QF_UFNRA,
     UFLRA,
+    UFNIRA, // nonstandard
     UFNIA,
     QF_ALL_SUPPORTED, // nonstandard
     ALL_SUPPORTED // nonstandard
@@ -75,7 +76,7 @@ public:
     THEORY_ARRAYS_EX,
     THEORY_BITVECTORS,
     THEORY_BITVECTORS_32,
-    THEORY_BITVECTORS_ARRAYS_EX,
+    THEORY_BITVECTOR_ARRAYS_EX,
     THEORY_EMPTY,
     THEORY_INTS,
     THEORY_INT_ARRAYS,
@@ -83,6 +84,7 @@ public:
     THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX,
     THEORY_REALS,
     THEORY_REALS_INTS,
+    THEORY_QUANTIFIERS
   };
 
 private: