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, 16 insertions, 12 deletions

diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h
index d4239ff13..01178b453 100644
--- a/src/theory/bv/bv_subtheory_eq.h
+++ b/src/theory/bv/bv_subtheory_eq.h
@@ -40,6 +40,10 @@ class EqualitySolver : public SubtheorySolver {
     bool eqNotifyTriggerPredicate(TNode predicate, bool value);
     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
     void eqNotifyConstantTermMerge(TNode t1, TNode t2);
+    void eqNotifyNewClass(TNode t) { }
+    void eqNotifyPreMerge(TNode t1, TNode t2) { }
+    void eqNotifyPostMerge(TNode t1, TNode t2) { }
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
 };
 
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 30493737a..66f443d50 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -33,8 +33,8 @@ using namespace CVC4::theory::bv::utils;
 
 
 
-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
-  : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
+  : Theory(THEORY_BV, c, u, out, valuation, logicInfo, qe),
     d_context(c),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 9c27f62c5..f79b7ab71 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -49,8 +49,8 @@ class TheoryBV : public Theory {
   EqualitySolver d_equalitySolver;
 public:
 
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
-  ~TheoryBV(); 
+  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+  ~TheoryBV();
 
   void preRegisterTerm(TNode n);
 
@@ -64,21 +64,21 @@ public:
 
   std::string identify() const { return std::string("TheoryBV"); }
 
-  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); 
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 
 private:
-  
+
   class Statistics {
   public:
     AverageStat d_avgConflictSize;
     IntStat     d_solveSubstitutions;
-    TimerStat   d_solveTimer;  
+    TimerStat   d_solveTimer;
     Statistics();
-    ~Statistics(); 
-  }; 
-  
+    ~Statistics();
+  };
+
   Statistics d_statistics;
-  
+
   // Are we in conflict?
   context::CDO<bool> d_conflict;
 
@@ -133,7 +133,7 @@ private:
   }
 
   bool inConflict() { return d_conflict == true; }
-  
+
   friend class Bitblaster;
   friend class BitblastSolver;
   friend class EqualitySolver;