fixes for uf/equality engine from the quantifiers branch. mainly backtracking issues.

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index ba607526ffafe30dd21c133912b2cf7a281ee73a..18a525f2d9da9570fdb61d0500c6da4d5285c9c7 100644 (file)
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -284,8 +284,8 @@ private:
    */
   ApplicationIdsMap d_applicationLookup;
 
-  /** Map from ids to the nodes */
-  std::vector<TNode> d_nodes;
+  /** Map from ids to the nodes (these need to be nodes as we pick-up the opreators) */
+  std::vector<Node> d_nodes;
 
   /** A context-dependents count of nodes */
   context::CDO<size_t> d_nodesCount;
@@ -302,9 +302,6 @@ private:
   /** Memory for the use-list nodes */
   std::vector<UseListNode> d_useListNodes;
 
-  /** Context dependent size of the use-list memory */
-  context::CDO<size_t> d_useListNodeSize;
-
   /**
    * We keep a list of asserted equalities. Not among original terms, but
    * among the class representatives.
@@ -444,7 +441,7 @@ private:
   /**
    * Vector of original equalities of the triggers.
    */
-  std::vector<TNode> d_equalityTriggersOriginal;
+  std::vector<Node> d_equalityTriggersOriginal;
 
   /**
    * Context dependent count of triggers
@@ -497,7 +494,7 @@ private:
   /**
    * Get an explanation of the equality t1 = t2. Returns the asserted equalities that
    * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
-   * else. TODO: mark the phantom equalities (skolems).
+   * else. 
    */
   void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const;
 
@@ -517,7 +514,6 @@ public:
     d_notify(notify),
     d_nodesCount(context, 0),
     d_assertedEqualitiesCount(context, 0),
-    d_useListNodeSize(context, 0),
     d_equalityTriggersCount(context, 0),
     d_stats(name)
   {

diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
index 1a4673be96fdeede578b08a7a0651e8358409af5..b31d04a32d8797b6ec2db2ea5058975513ddd8b6 100644 (file)
--- a/src/theory/uf/equality_engine_impl.h
+++ b/src/theory/uf/equality_engine_impl.h
@@ -64,9 +64,8 @@ EqualityNodeId EqualityEngine<NotifyClass>::newApplicationNode(TNode original, E
   }
 
   // Add to the use lists
-  d_equalityNodes[t1].usedIn(funId, d_useListNodes);
-  d_equalityNodes[t2].usedIn(funId, d_useListNodes);
-  d_useListNodeSize = d_useListNodes.size();
+  d_equalityNodes[t1ClassId].usedIn(funId, d_useListNodes);
+  d_equalityNodes[t2ClassId].usedIn(funId, d_useListNodes);
 
   // Return the new id
   Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl;
@@ -438,10 +437,22 @@ void EqualityEngine<NotifyClass>::backtrack() {
     d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
   }
 
+  if (d_equalityTriggers.size() > d_equalityTriggersCount) {
+    // Unlink the triggers from the lists
+    for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) {
+       const Trigger& trigger = d_equalityTriggers[i];
+       d_nodeTriggers[trigger.classId] = trigger.nextTrigger;
+    }
+    // Get rid of the triggers 
+    d_equalityTriggers.resize(d_equalityTriggersCount);
+    d_equalityTriggersOriginal.resize(d_equalityTriggersCount);
+  }
+
   if (d_nodes.size() > d_nodesCount) {
     // Go down the nodes, check the application nodes and remove them from use-lists
-    for(int i = d_nodes.size() - 1, i_end = (int)d_nodesCount; i >= i_end; ++ i) {
+    for(int i = d_nodes.size() - 1, i_end = (int)d_nodesCount; i >= i_end; -- i) {
       // Remove from the node -> id map
+      Debug("equality") << "EqualityEngine::backtrack(): removing node " << d_nodes[i] << std::endl;
       d_nodeIds.erase(d_nodes[i]);
 
       const FunctionApplication& app = d_applications[i];
@@ -461,12 +472,6 @@ void EqualityEngine<NotifyClass>::backtrack() {
     d_nodeTriggers.resize(d_nodesCount);
     d_equalityGraph.resize(d_nodesCount);
     d_equalityNodes.resize(d_nodesCount);
-    d_useListNodes.resize(d_useListNodeSize);
-  }
-
-  if (d_equalityTriggers.size() > d_equalityTriggersCount) {
-    d_equalityTriggers.resize(d_equalityTriggersCount);
-    d_equalityTriggersOriginal.resize(d_equalityTriggersCount);
   }
 }
 
@@ -640,8 +645,8 @@ void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode t
   d_equalityTriggersCount = d_equalityTriggersCount + 2;
 
   // Add the trigger to the trigger graph
-  d_nodeTriggers[t1Id] = t1NewTriggerId;
-  d_nodeTriggers[t2Id] = t2NewTriggerId;
+  d_nodeTriggers[t1classId] = t1NewTriggerId;
+  d_nodeTriggers[t2classId] = t2NewTriggerId;
 
   // If the trigger is already on, we propagate
   if (t1classId == t2classId) {

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 401c182034961662959802c24ceb2089404a2e37..b388dd1cb9db776d4f524eaa5eab156a288097df 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -89,7 +89,6 @@ void TheoryUF::check(Effort level) {
   if (d_conflict) {
     Debug("uf") << "TheoryUF::check(): conflict " << d_conflictNode << std::endl;
     d_out->conflict(d_conflictNode);
-    d_literalsToPropagate.clear();
   }
 
   // Otherwise we propagate in order to detect a weird conflict like
@@ -103,8 +102,8 @@ void TheoryUF::check(Effort level) {
 void TheoryUF::propagate(Effort level) {
   Debug("uf") << "TheoryUF::propagate()" << std::endl;
   if (!d_conflict) {
-    for (unsigned i = 0; i < d_literalsToPropagate.size(); ++ i) {
-      TNode literal = d_literalsToPropagate[i];
+    for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
+      TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
       Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl;
       bool satValue;
       if (!d_valuation.hasSatValue(literal, satValue)) {
@@ -127,7 +126,6 @@ void TheoryUF::propagate(Effort level) {
       }
     }
   }
-  d_literalsToPropagate.clear();
 }
 
 void TheoryUF::preRegisterTerm(TNode node) {

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 1f4c2372f41afe038af819395add1e6fe8adfccf..a3871f3a20bdbd9eb0dee09bfae56fbca9af03d8 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -37,7 +37,6 @@ namespace theory {
 namespace uf {
 
 class TheoryUF : public Theory {
-
 public:
 
   class NotifyClass {
@@ -80,7 +79,11 @@ private:
   void explain(TNode literal, std::vector<TNode>& assumptions);
 
   /** Literals to propagate */
-  std::vector<TNode> d_literalsToPropagate;
+  context::CDList<TNode> d_literalsToPropagate;
+
+  /** Index of the next literal to propagate */
+  context::CDO<unsigned> d_literalsToPropagateIndex;
+
 
   /** True node for predicates = true */
   Node d_true;
@@ -99,7 +102,9 @@ public:
     d_notify(*this),
     d_equalityEngine(d_notify, ctxt, "theory::uf::TheoryUF"),
     d_knownFacts(ctxt),
-    d_conflict(ctxt, false)
+    d_conflict(ctxt, false),
+    d_literalsToPropagate(ctxt),
+    d_literalsToPropagateIndex(ctxt, 0)
   {
     // The kinds we are treating as function application in congruence
     d_equalityEngine.addFunctionKind(kind::APPLY_UF);