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, 28 insertions, 7 deletions

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index b4d5c0086..48b9b2d35 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -22,6 +22,7 @@
 
 #include "theory/theory.h"
 #include "theory/arith/theory_arith.h"
+#include "theory/quantifiers_engine.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "context/context.h"
@@ -51,6 +52,7 @@ class TheoryArithWhite : public CxxTest::TestSuite {
   LogicInfo d_logicInfo;
   Theory::Effort d_level;
 
+  QuantifiersEngine* d_quantifiersEngine;
   TheoryArith* d_arith;
 
   TypeNode* d_booleanType;
@@ -99,7 +101,9 @@ public:
     d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
-    d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo);
+    d_logicInfo.lock();
+    d_quantifiersEngine = new QuantifiersEngine(d_ctxt, NULL);
+    d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_quantifiersEngine);
 
     preregistered = new std::set<Node>();
 
@@ -115,6 +119,7 @@ public:
     delete preregistered;
 
     delete d_arith;
+    delete d_quantifiersEngine;
     d_outputChannel.clear();
     delete d_scope;
     delete d_nm;
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 34536445f..74f5870a3 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -74,6 +74,16 @@ public:
     return LemmaStatus(Node::null(), 0);
   }
 
+  void requirePhase(TNode, bool)
+    throw(Interrupted, AssertionException) {
+    Unreachable();
+  }
+
+  bool flipDecision()
+    throw(Interrupted, AssertionException) {
+    Unreachable();
+  }
+
   void setIncomplete()
     throw(AssertionException) {
     Unreachable();
@@ -102,8 +112,8 @@ public:
   set<Node> d_registered;
   vector<Node> d_getSequence;
 
-  DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-    Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo) {
+  DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
+    Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, qe) {
   }
 
   void registerTerm(TNode n) {
@@ -167,8 +177,8 @@ public:
     d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_logicInfo = new LogicInfo();
-
-    d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo);
+    d_logicInfo->lock();
+    d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo, NULL);
     d_outputChannel.clear();
     atom0 = d_nm->mkConst(true);
     atom1 = d_nm->mkConst(false);
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 2d6730949..ae61bd0d3 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -60,6 +60,12 @@ class FakeOutputChannel : public OutputChannel {
   LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) {
     Unimplemented();
   }
+  void requirePhase(TNode, bool) throw(AssertionException) {
+    Unimplemented();
+  }
+  bool flipDecision() throw(AssertionException) {
+    Unimplemented();
+  }
   void explanation(TNode n) throw(AssertionException) {
     Unimplemented();
   }
@@ -107,8 +113,8 @@ class FakeTheory : public Theory {
   // static std::deque<RewriteItem> s_expected;
 
 public:
-  FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-    Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
+  FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
+    Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, qe)
   { }
 
   /** Register an expected rewrite call */