22 files changed, 170 insertions, 38 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7c913578b..03834825d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -554,6 +554,7 @@ void SmtEngine::finishInit() {
 
   d_theoryEngine->setPropEngine(d_propEngine);
   d_theoryEngine->setDecisionEngine(d_decisionEngine);
+  d_theoryEngine->finishInit();
 
   // [MGD 10/20/2011] keep around in incremental mode, due to a
   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 09410f15b..5ee250c09 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -65,6 +65,10 @@ ArithCongruenceManager::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_conflicts);
 }
 
+void ArithCongruenceManager::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_ee.setMasterEqualityEngine(eq);
+}
+
 void ArithCongruenceManager::watchedVariableIsZero(Constraint lb, Constraint ub){
   Assert(lb->isLowerBound());
   Assert(ub->isUpperBound());
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 502ea5cf0..5e2c80a63 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -144,6 +144,8 @@ public:
     return d_explanationMap.find(n) != d_explanationMap.end();
   }
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
 private:
   Node externalToInternal(TNode n) const{
     Assert(canExplain(n));
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 141b22dc6..6ec6c7090 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -91,6 +91,10 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
 
 TheoryArith::~TheoryArith(){}
 
+void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_congruenceManager.setMasterEqualityEngine(eq);
+}
+
 Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){
   NodeManager* currNM = NodeManager::currentNM();
   TypeNode functionType = currNM->mkFunctionType(dom, range);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 0773ab7ba..ad041208d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -341,6 +341,8 @@ public:
    */
   void preRegisterTerm(TNode n);
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   void check(Effort e);
   void propagate(Effort e);
   Node explain(TNode n);
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f40fea0ba..b8c1ace4b 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -111,7 +111,6 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   }
 }
 
-
 TheoryArrays::~TheoryArrays() {
 
   StatisticsRegistry::unregisterStat(&d_numRow);
@@ -124,6 +123,10 @@ TheoryArrays::~TheoryArrays() {
 
 }
 
+void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
 
 /////////////////////////////////////////////////////////////////////////////
 // PREPROCESSING
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index eaa3ca431..240cfad9a 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -123,6 +123,8 @@ class TheoryArrays : public Theory {
   TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
   ~TheoryArrays();
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   std::string identify() const { return std::string("TheoryArrays"); }
 
   /////////////////////////////////////////////////////////////////////////////
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index 17ea7034b..ca3e3e35c 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -67,6 +67,10 @@ EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv)
   }
 }
 
+void EqualitySolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
 void EqualitySolver::preRegister(TNode node) {
   if (!d_useEqualityEngine)
     return;
diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h
index 64fe12706..2b024cfd4 100644
--- a/src/theory/bv/bv_subtheory_eq.h
+++ b/src/theory/bv/bv_subtheory_eq.h
@@ -63,7 +63,7 @@ class EqualitySolver : public SubtheorySolver {
 public:
 
   EqualitySolver(context::Context* c, TheoryBV* bv);
-
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
   void  preRegister(TNode node);
   bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index a37ed59c8..7acb93cc2 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -50,6 +50,11 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
 
 TheoryBV::~TheoryBV() {}
 
+
+void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalitySolver.setMasterEqualityEngine(eq);
+}
+
 TheoryBV::Statistics::Statistics():
   d_avgConflictSize("theory::bv::AvgBVConflictSize"),
   d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 933fd8700..0c8df3fca 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -50,6 +50,8 @@ public:
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
   ~TheoryBV();
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   void preRegisterTerm(TNode n);
 
   void check(Effort e);
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 6b576cba8..8ec45efb9 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -56,6 +56,10 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
 TheoryDatatypes::~TheoryDatatypes() {
 }
 
+void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
 TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake ){
   std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
   if( !hasEqcInfo( n ) ){
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 16e403e95..5cda9eeae 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -179,6 +179,9 @@ public:
   TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation,
                   const LogicInfo& logicInfo, QuantifiersEngine* qe);
   ~TheoryDatatypes();
+
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   /** propagate */
   void propagate(Effort effort);
   /** propagate */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 6e704ba1c..446c9285e 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -36,17 +36,22 @@ using namespace CVC4::theory::quantifiers;
 
 TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, qe),
-  d_numRestarts(0){
+  d_numRestarts(0),
+  d_masterEqualityEngine(0)
+{
   d_numInstantiations = 0;
   d_baseDecLevel = -1;
   out.handleUserAttribute( "axiom", this );
   out.handleUserAttribute( "conjecture", this );
 }
 
-
 TheoryQuantifiers::~TheoryQuantifiers() {
 }
 
+void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_masterEqualityEngine = eq;
+}
+
 void TheoryQuantifiers::addSharedTerm(TNode t) {
   Debug("quantifiers-other") << "TheoryQuantifiers::addSharedTerm(): "
                      << t << endl;
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 7b050bb1c..12b735497 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -31,6 +31,7 @@ namespace CVC4 {
 class TheoryEngine;
 
 namespace theory {
+
 namespace quantifiers {
 
 class ModelEngine;
@@ -49,10 +50,14 @@ private:
 
   KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::quantifiers::theoryTime");
 
+  eq::EqualityEngine* d_masterEqualityEngine;
+
 public:
   TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
   ~TheoryQuantifiers();
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   void addSharedTerm(TNode t);
   void notifyEq(TNode lhs, TNode rhs);
   void preRegisterTerm(TNode n);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 95fe03c82..4d535a8af 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -54,6 +54,10 @@ namespace rrinst{
 class CandidateGenerator;
 }
 
+namespace eq {
+class EqualityEngine;
+}
+
 /**
  * Information about an assertion for the theories.
  */
@@ -246,7 +250,8 @@ protected:
    * Construct a Theory.
    */
   Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
-         OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) throw()
+         OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
+         QuantifiersEngine* qe, eq::EqualityEngine* master = 0) throw()
   : d_id(id)
   , d_satContext(satContext)
   , d_userContext(userContext)
@@ -515,6 +520,11 @@ public:
   virtual void addSharedTerm(TNode n) { }
 
   /**
+   * Called to set the master equality engine.
+   */
+  virtual void setMasterEqualityEngine(eq::EqualityEngine* eq) { }
+
+  /**
    * Return the current theory care graph. Theories should overload computeCareGraph to do
    * the actual computation, and use addCarePair to add pairs to the care graph.
    */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4b4316db1..cd3b34879 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -42,12 +42,26 @@
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/first_order_model.h"
 
+#include "theory/uf/equality_engine.h"
 
 using namespace std;
 
 using namespace CVC4;
 using namespace CVC4::theory;
 
+void TheoryEngine::finishInit() {
+  if (d_logicInfo.isQuantified()) {
+    Assert(d_masterEqualityEngine == 0);
+    d_masterEqualityEngine = new eq::EqualityEngine(getSatContext(), "theory::master");
+
+    for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
+      if (d_theoryTable[theoryId]) {
+        d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
+      }
+    }
+  }
+}
+
 TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
                            RemoveITE& iteRemover,
@@ -58,6 +72,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_userContext(userContext),
   d_logicInfo(logicInfo),
   d_sharedTerms(this, context),
+  d_masterEqualityEngine(NULL),
   d_quantEngine(NULL),
   d_curr_model(NULL),
   d_curr_model_builder(NULL),
@@ -114,6 +129,8 @@ TheoryEngine::~TheoryEngine() {
 
   delete d_quantEngine;
 
+  delete d_masterEqualityEngine;
+
   StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
 }
 
@@ -229,21 +246,6 @@ void TheoryEngine::dumpAssertions(const char* tag) {
   }
 }
 
-
-template<typename T, bool doAssert>
-class scoped_vector_clear {
-  vector<T>& d_v;
-public:
-  scoped_vector_clear(vector<T>& v)
-  : d_v(v) {
-    Assert(!doAssert || d_v.empty());
-  }
-  ~scoped_vector_clear() {
-    d_v.clear();
-  }
-
-};
-
 /**
  * Check all (currently-active) theories for conflicts.
  * @param effort the effort level to use
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index d6e984f8f..de872db42 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -76,8 +76,13 @@ namespace theory {
   class Instantiator;
   class TheoryModel;
   class TheoryEngineModelBuilder;
+
+  namespace eq {
+    class EqualityEngine;
+  }
 }/* CVC4::theory namespace */
 
+
 class DecisionEngine;
 
 /**
@@ -124,6 +129,11 @@ class TheoryEngine {
   SharedTermsDatabase d_sharedTerms;
 
   /**
+   * Master equality engine, to share with theories.
+   */
+  theory::eq::EqualityEngine* d_masterEqualityEngine;
+
+  /**
    * The quantifiers engine
    */
   theory::QuantifiersEngine* d_quantEngine;
@@ -428,6 +438,9 @@ public:
     d_decisionEngine = decisionEngine;
   }
 
+  /** Called when all initialization of options/logic is done */
+  void finishInit();
+
   /**
    * Get a pointer to the underlying propositional engine.
    */
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 90de8d0d2..636427ed1 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -79,8 +79,9 @@ EqualityEngine::~EqualityEngine() throw(AssertionException) {
 }
 
 
-EqualityEngine::EqualityEngine(context::Context* context, std::string name) 
+EqualityEngine::EqualityEngine(context::Context* context, std::string name)
 : ContextNotifyObj(context)
+, d_masterEqualityEngine(0)
 , d_context(context)
 , d_done(context, false)
 , d_performNotify(true)
@@ -102,6 +103,7 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name)
 
 EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name)
 : ContextNotifyObj(context)
+, d_masterEqualityEngine(0)
 , d_context(context)
 , d_done(context, false)
 , d_performNotify(true)
@@ -121,6 +123,11 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c
   init();
 }
 
+void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) {
+  Assert(d_masterEqualityEngine == 0);
+  d_masterEqualityEngine = master;
+}
+
 void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
   Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl;
   if (back) {
@@ -294,6 +301,11 @@ void EqualityEngine::addTerm(TNode t) {
     d_nodeIndividualTrigger[tId] = newTriggerTermSet();
   }
 
+  // If this is not an internal node, add it to the master
+  if (d_masterEqualityEngine && !d_isInternal[result]) {
+    d_masterEqualityEngine->addTerm(t);
+  }
+
   propagate();
 
   Debug("equality") << d_name << "::eq::addTerm(" << t << ") => " << result << std::endl;
@@ -1213,9 +1225,34 @@ void EqualityEngine::propagate() {
       continue;
     }
 
-    // Depending on the merge preference (such as size, or being a constant), merge them
+    // Vector to collect the triggered events
     std::vector<TriggerId> triggers;
-    if ((node2.getSize() > node1.getSize() && !d_isConstant[t1classId]) || d_isConstant[t2classId]) {
+
+    // Figure out the merge preference
+    EqualityNodeId mergeInto = t1classId;
+    if (d_isInternal[t2classId] != d_isInternal[t1classId]) {
+      // We always keep non-internal nodes as representatives: if any node in
+      // the class is non-internal, then the representative will be non-internal
+      if (d_isInternal[t1classId]) {
+        mergeInto = t2classId;
+      } else {
+        mergeInto = t1classId;
+      }
+    } else if (d_isConstant[t2classId] != d_isConstant[t1classId]) {
+      // We always keep constants as representatives: if any (at most one) node
+      // in the class in a constant, then the representative will be a constant
+      if (d_isConstant[t2classId]) {
+        mergeInto = t2classId;
+      } else {
+        mergeInto = t1classId;
+      }
+    } else if (node2.getSize() > node1.getSize()) {
+      // We always merge into the bigger class to reduce the amount of traversing
+      // we need to do
+      mergeInto = t2classId;
+    }
+
+    if (mergeInto == t2classId) {
       Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
       d_assertedEqualities.push_back(Equality(t2classId, t1classId));
       d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
@@ -1231,6 +1268,12 @@ void EqualityEngine::propagate() {
       }
     }
 
+    // If not merging internal nodes, notify the master
+    if (d_masterEqualityEngine && !d_isInternal[mergeInto]) {
+      d_masterEqualityEngine->assertEqualityInternal(d_nodes[t1classId], d_nodes[t2classId], TNode::null());
+      d_masterEqualityEngine->propagate();
+    }
+
     // Notify the triggers
     if (d_performNotify && !d_done) {
       for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) {
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 166362951..9bc2cb61c 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -151,8 +151,35 @@ class EqualityEngine : public context::ContextNotifyObj {
   /** Default implementation of the notification object */
   static EqualityEngineNotifyNone s_notifyNone;
 
+  /**
+   * Master equality engine that gets all the equality information from
+   * this one, or null if none.
+   */
+  EqualityEngine* d_masterEqualityEngine;
+
 public:
 
+  /**
+   * Initialize the equality engine, given the notification class.
+   */
+  EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name);
+
+  /**
+   * Initialize the equality engine with no notification class.
+   */
+  EqualityEngine(context::Context* context, std::string name);
+
+  /**
+   * Just a destructor.
+   */
+  virtual ~EqualityEngine() throw(AssertionException);
+
+  /**
+   * Set the master equality engine for this one. Master engine will get copies of all
+   * the terms and equalities from this engine.
+   */
+  void setMasterEqualityEngine(EqualityEngine* master);
+
   /** Statistics about the equality engine instance */
   struct Statistics {
     /** Total number of merges */
@@ -640,21 +667,6 @@ private:
 public:
 
   /**
-   * Initialize the equality engine, given the notification class.
-   */
-  EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name);
-
-  /**
-   * Initialize the equality engine with no notification class.
-   */
-  EqualityEngine(context::Context* context, std::string name);
-
-  /**
-   * Just a destructor.
-   */
-  virtual ~EqualityEngine() throw(AssertionException);
-
-  /**
    * Adds a term to the term database.
    */
   void addTerm(TNode t);
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index d76d95adb..e6ae3747c 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -45,6 +45,10 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel&
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 }
 
+void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
 static Node mkAnd(const std::vector<TNode>& conjunctions) {
   Assert(conjunctions.size() > 0);
 
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index f30619e2e..46a17a5e0 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -187,6 +187,8 @@ public:
     }
   }
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
   void check(Effort);
   void preRegisterTerm(TNode term);
   Node explain(TNode n);