diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/uf/equality_engine.h | 12 | ||||
-rw-r--r-- | src/theory/uf/equality_engine_impl.h | 29 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 6 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 11 |
4 files changed, 31 insertions, 27 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index ba607526f..18a525f2d 100644 --- 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 1a4673be9..b31d04a32 100644 --- 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 401c18203..b388dd1cb 100644 --- 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 1f4c2372f..a3871f3a2 100644 --- 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); |