From 62a50760346e130345b24e8a14ad0dac0dca5d38 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Wed, 7 Sep 2011 16:25:15 +0000 Subject: [PATCH] fixes for uf/equality engine from the quantifiers branch. mainly backtracking issues. --- src/theory/uf/equality_engine.h | 12 ++++-------- src/theory/uf/equality_engine_impl.h | 29 ++++++++++++++++------------ src/theory/uf/theory_uf.cpp | 6 ++---- 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 d_nodes; + /** Map from ids to the nodes (these need to be nodes as we pick-up the opreators) */ + std::vector d_nodes; /** A context-dependents count of nodes */ context::CDO d_nodesCount; @@ -302,9 +302,6 @@ private: /** Memory for the use-list nodes */ std::vector d_useListNodes; - /** Context dependent size of the use-list memory */ - context::CDO 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 d_equalityTriggersOriginal; + std::vector 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& 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::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::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::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::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& assumptions); /** Literals to propagate */ - std::vector d_literalsToPropagate; + context::CDList d_literalsToPropagate; + + /** Index of the next literal to propagate */ + context::CDO 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); -- 2.30.2