From fd9e22c4a2e57c3dfeda4de3842a3fb3ca4776ba Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Wed, 6 Jun 2012 06:12:40 +0000 Subject: Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better. http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5 --- src/theory/uf/equality_engine.cpp | 170 +++++++++++++++++++++++++++------- src/theory/uf/equality_engine.h | 7 ++ src/theory/uf/equality_engine_types.h | 37 +++----- src/theory/uf/theory_uf.cpp | 76 ++++----------- src/theory/uf/theory_uf.h | 19 ++-- 5 files changed, 180 insertions(+), 129 deletions(-) (limited to 'src/theory/uf') diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 5093e5a7b..4cd54a2bf 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -62,14 +62,14 @@ void EqualityEngine::init() { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); + d_triggerDatabaseAllocatedSize = 100000; + d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize); + addTerm(d_true); addTerm(d_false); d_trueId = getNodeId(d_true); d_falseId = getNodeId(d_false); - - d_triggerDatabaseAllocatedSize = 100000; - d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize); } EqualityEngine::~EqualityEngine() throw(AssertionException) { @@ -114,7 +114,8 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c } void EqualityEngine::enqueue(const MergeCandidate& candidate) { - d_propagationQueue.push(candidate); + Debug("equality") << "EqualityEngine::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl; + d_propagationQueue.push(candidate); } EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality) { @@ -144,7 +145,15 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId if (isEquality && d_isConstant[t1ClassId] && d_isConstant[t2ClassId]) { if (t1ClassId != t2ClassId) { Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl; + Assert(d_nodes[funId].getKind() == kind::EQUAL); enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); + // Also enqueue the symmetric one + TNode eq = d_nodes[funId]; + Node symmetricEq = eq[1].eqNode(eq[0]); + if (hasTerm(symmetricEq)) { + EqualityNodeId symmFunId = getNodeId(symmetricEq); + enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); + } } } } else { @@ -154,8 +163,8 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId } // Add to the use lists - d_equalityNodes[t1ClassId].usedIn(funId, d_useListNodes); - d_equalityNodes[t2ClassId].usedIn(funId, d_useListNodes); + d_equalityNodes[t1].usedIn(funId, d_useListNodes); + d_equalityNodes[t2].usedIn(funId, d_useListNodes); // Return the new id Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl; @@ -238,6 +247,20 @@ void EqualityEngine::addTerm(TNode t) { // We set this here as this only applies to actual terms, not the // intermediate application terms d_isBoolean[result] = true; + } else if (t.isConst()) { + // Non-Boolean constants are trigger terms for all tags + EqualityNodeId tId = getNodeId(t); + d_newSetTags = 0; + d_newSetTriggersSize = THEORY_LAST; + for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) { + d_newSetTags = Theory::setInsert(currentTheory, d_newSetTags); + d_newSetTriggers[currentTheory] = tId; + } + // Add it to the list for backtracking + d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id)); + d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1; + // Mark the the new set as a trigger + d_nodeIndividualTrigger[tId] = newTriggerTermSet(); } propagate(); @@ -319,15 +342,20 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { assertEqualityInternal(eq, d_false, reason); propagate(); assertEqualityInternal(eq[1].eqNode(eq[0]), d_false, reason); - propagate(); + propagate(); if (d_done) { return; } - // If we are adding a disequality, notify of the shared term representatives + // If both have constant representatives, we don't notify anyone EqualityNodeId a = getNodeId(eq[0]); EqualityNodeId b = getNodeId(eq[1]); + if (isConstant(a) && isConstant(b)) { + return; + } + + // If we are adding a disequality, notify of the shared term representatives EqualityNodeId eqId = getNodeId(eq); TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[a]; TriggerTermSetRef bTriggerRef = d_nodeIndividualTrigger[b]; @@ -356,6 +384,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { d_deducedDisequalityReasons.push_back(EqualityPair(bSharedId, b)); d_deducedDisequalityReasons.push_back(EqualityPair(eqId, d_falseId)); storePropagatedDisequality(d_nodes[aSharedId], d_nodes[bSharedId], 3); + // We notify even if the it's already been sent (they are not // disequal at assertion, and we need to notify for each tag) if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) { @@ -383,7 +412,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl; Assert(triggersFired.empty()); - + ++ d_stats.mergesCount; EqualityNodeId class1Id = class1.getFind(); @@ -391,6 +420,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Check for constant merges bool isConstant = d_isConstant[class1Id]; + Assert(isConstant || !d_isConstant[class2Id]); // Update class2 representative information Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl; @@ -438,13 +468,13 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl; // Go through the uselist and check for congruences - UseListNodeId currentUseId = currentNode.getUseList(); + UseListNodeId currentUseId = currentNode.getUseList(); while (currentUseId != null_uselist_id) { // Get the node of the use list UseListNode& useNode = d_useListNodes[currentUseId]; // Get the function application EqualityNodeId funId = useNode.getApplicationId(); - Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl; + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl; const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; // Check if there is an application with find arguments EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); @@ -460,11 +490,16 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // There is no representative, so we can add one, we remove this when backtracking storeApplicationLookup(funNormalized, funId); // Now, if we're constant and it's an equality, check if the other guy is also a constant - if (isConstant && funNormalized.isEquality) { - if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) { - // both constants - if (funNormalized.a != funNormalized.b) { - enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); + if (funNormalized.isEquality) { + if (d_isConstant[aNormalized] && d_isConstant[bNormalized] && aNormalized != bNormalized) { + Assert(d_nodes[funId].getKind() == kind::EQUAL); + enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); + // Also enqueue the symmetric one + TNode eq = d_nodes[funId]; + Node symmetricEq = eq[1].eqNode(eq[0]); + if (hasTerm(symmetricEq)) { + EqualityNodeId symmFunId = getNodeId(symmetricEq); + enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); } } } @@ -482,6 +517,17 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Now merge the lists class1.merge(class2); + // Notify of the constants merge + bool constantMerge = false; + if (isConstant && d_isConstant[class2Id]) { + constantMerge = true; + if (d_performNotify) { + if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) { + return false; + } + } + } + // Go through the triggers and store the dis-equalities unsigned i = 0, j = 0; for (; i < triggersFired.size();) { @@ -543,7 +589,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // copy tag1 EqualityNodeId tag1id = d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++]; // since they are both tagged notify of merge - if (d_performNotify) { + if (d_performNotify && !constantMerge) { EqualityNodeId tag2id = class2triggers.triggers[i2++]; if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) { return false; @@ -566,15 +612,6 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } } - // Notify of the constants merge - if (isConstant && d_isConstant[class2Id]) { - if (d_performNotify) { - if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) { - return false; - } - } - } - // Everything fine return true; } @@ -680,12 +717,12 @@ void EqualityEngine::backtrack() { Debug("equality") << "EqualityEngine::backtrack(): removing node " << d_nodes[i] << std::endl; d_nodeIds.erase(d_nodes[i]); - const FunctionApplication& app = d_applications[i].normalized; + const FunctionApplication& app = d_applications[i].original; if (app.isApplication()) { // Remove b from use-list - getEqualityNode(app.b).removeTopFromUseList(d_useListNodes); + getEqualityNode(app.b).removeTopFromUseList(d_useListNodes); // Remove a from use-list - getEqualityNode(app.a).removeTopFromUseList(d_useListNodes); + getEqualityNode(app.a).removeTopFromUseList(d_useListNodes); } } @@ -818,8 +855,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // Go through the equality edges of this node EqualityEdgeId currentEdge = d_equalityGraph[currentNode]; - Debug("equality") << "EqualityEngine::getExplanation(): edgesId = " << currentEdge << std::endl; - Debug("equality") << "EqualityEngine::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl; + if (Debug.isOn("equality")) { + Debug("equality") << "EqualityEngine::getExplanation(): edgesId = " << currentEdge << std::endl; + Debug("equality") << "EqualityEngine::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl; + } while (currentEdge != null_edge) { // Get the edge @@ -871,8 +910,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << push; // Explain why a is a constant + Assert(isConstant(eq.a)); getExplanation(eq.a, getEqualityNode(eq.a).getFind(), equalities); // Explain why b is a constant + Assert(isConstant(eq.b)); getExplanation(eq.b, getEqualityNode(eq.b).getFind(), equalities); Debug("equality") << pop; @@ -1062,7 +1103,7 @@ void EqualityEngine::propagate() { // Depending on the merge preference (such as size, or being a constant), merge them std::vector triggers; - if (node2.getSize() > node1.getSize() || d_isConstant[t2classId]) { + if ((node2.getSize() > node1.getSize() && !d_isConstant[t1classId]) || d_isConstant[t2classId]) { Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl; d_assertedEqualities.push_back(Equality(t2classId, t1classId)); if (!merge(node2, node1, triggers)) { @@ -1222,7 +1263,7 @@ size_t EqualityEngine::getSize(TNode t) void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) { - Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; + Debug("equality::trigger") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; Assert(tag != THEORY_LAST); if (d_done) { @@ -1243,12 +1284,71 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // If the term already is in the equivalence class that a tagged representative, just notify if (d_performNotify) { EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag); - if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) { + if (eqNodeId != triggerId && !d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) { d_done = true; } } } else { + // Check for disequalities by going through the equivalence class looking for equalities in the + // uselists that have been asserted to false. All the representatives appearing on the other + // side of such disequalities, that have the tag on, are put in a set. + std::set disequalSet; + EqualityNodeId currentId = classId; + do { + // Current node + EqualityNode& currentNode = getEqualityNode(currentId); + // Go through the uselist and look for disequalities + UseListNodeId currentUseId = currentNode.getUseList(); + while (!d_done && currentUseId != null_uselist_id) { + // Get the normalized equality + UseListNode& useNode = d_useListNodes[currentUseId]; + EqualityNodeId funId = useNode.getApplicationId(); + const FunctionApplication& fun = d_applications[useNode.getApplicationId()].original; + // Check for asserted disequalities + if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) { + // Get the other equality member + EqualityNodeId toCompare = fun.b; + if (toCompare == currentId) { + toCompare = fun.a; + } + // Representative of the other member + EqualityNodeId toCompareRep = getEqualityNode(toCompare).getFind(); + Assert(toCompareRep != classId); + // Get the trigger set + TriggerTermSetRef toCompareTriggerSetRef = d_nodeIndividualTrigger[toCompareRep]; + // Only notify if we're not both constants + if ((!d_isConstant[classId] || !d_isConstant[toCompareRep]) && toCompareTriggerSetRef != null_set_id) { + TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef); + if (Theory::setContains(tag, toCompareTriggerSet.tags)) { + // Get the tag representative + EqualityNodeId tagRep = toCompareTriggerSet.getTrigger(tag); + // Propagate the disequality if not already done + if (!disequalSet.count(tagRep) && d_performNotify) { + // Mark as propagated + disequalSet.insert(tagRep); + // Store the propagation + d_deducedDisequalityReasons.push_back(EqualityPair(eqNodeId, currentId)); + d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep)); + d_deducedDisequalityReasons.push_back(EqualityPair(funId, d_falseId)); + storePropagatedDisequality(t, d_nodes[tagRep], 3); + // We don't check if it's been propagated already, as we need one per tag + if (d_performNotify) { + if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[tagRep], false)) { + d_done = true; + } + } + } + } + } + } + // Go to the next one in the use list + currentUseId = useNode.getNext(); + } + // Next in equivalence class + currentId = currentNode.getNext(); + } while (!d_done && currentId != classId); + // Setup the data for the new set if (triggerSetRef != null_set_id) { // Get the existing set @@ -1322,7 +1422,7 @@ void EqualityEngine::getUseListTerms(TNode t, std::set& output) { // Get the current node EqualityNode& currentNode = getEqualityNode(currentId); // Go through the use-list - UseListNodeId currentUseId = currentNode.getUseList(); + UseListNodeId currentUseId = currentNode.getUseList(); while (currentUseId != null_uselist_id) { // Get the node of the use list UseListNode& useNode = d_useListNodes[currentUseId]; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 5ff8ee4dc..f40c79df3 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -344,6 +344,13 @@ private: */ std::vector d_isConstant; + /** + * Returns true if it's a constant + */ + bool isConstant(EqualityNodeId id) const { + return d_isConstant[getEqualityNode(id).getFind()]; + } + /** * Map from ids to wheather they are Boolean. */ diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 0baf70fcf..056ee0b84 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -94,8 +94,9 @@ struct MergeCandidate { EqualityNodeId t1Id, t2Id; MergeReasonType type; TNode reason; - MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason): - t1Id(x), t2Id(y), type(type), reason(reason) {} + MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason) + : t1Id(x), t2Id(y), type(type), reason(reason) + {} }; /** @@ -145,15 +146,6 @@ public: } }; -/** Main types of uselists */ -enum UseListType { - /** Use list of functions where the term appears in */ - USE_LIST_FUNCTIONS, - /** Use list of asserted disequalities */ - USE_LIST_DISEQUALITIES -}; - - /** * Main class for representing nodes in the equivalence class. The * nodes are a circular list, with the representative carrying the @@ -178,9 +170,6 @@ private: /** The use list of this node */ UseListNodeId d_useList; - /** The list of asserted disequalities that this node appears in */ - UseListNodeId d_diseqList; - public: /** @@ -191,15 +180,13 @@ public: , d_findId(nodeId) , d_nextId(nodeId) , d_useList(null_uselist_id) - , d_diseqList(null_uselist_id) {} /** * Returns the requested uselist. */ - template UseListNodeId getUseList() const { - return type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList; + return d_useList; } /** @@ -244,22 +231,20 @@ public: * Note that this node is used in a function application funId, or * a negatively asserted equality (dis-equality) with funId. */ - template + template void usedIn(EqualityNodeId funId, memory_class& memory) { - UseListNodeId& useList = type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList; UseListNodeId newUseId = memory.size(); - memory.push_back(UseListNode(funId, useList)); - useList = newUseId; + memory.push_back(UseListNode(funId, d_useList)); + d_useList = newUseId; } /** * For backtracking: remove the first element from the uselist and pop the memory. */ - template + template void removeTopFromUseList(memory_class& memory) { - UseListNodeId& useList = type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList; - Assert ((int) useList == (int)memory.size() - 1); - useList = memory.back().getNext(); + Assert ((int) d_useList == (int)memory.size() - 1); + d_useList = memory.back().getNext(); memory.pop_back(); } }; @@ -288,7 +273,7 @@ struct FunctionApplication { FunctionApplication(bool isEquality = false, EqualityNodeId a = null_id, EqualityNodeId b = null_id) : isEquality(isEquality), a(a), b(b) {} bool operator == (const FunctionApplication& other) const { - return a == other.a && b == other.b; + return isEquality == other.isEquality && a == other.a && b == other.b; } bool isApplication() const { return a != null_id && b != null_id; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index ae8bdc8da..7583f8ee7 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -70,16 +70,6 @@ void TheoryUF::check(Effort level) { Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl; - // If the assertion doesn't have a literal, it's a shared equality, so we set it up - if (!assertion.isPreregistered) { - Debug("uf") << "TheoryUF::check(): shared equality, setting up " << fact << std::endl; - if (fact.getKind() == kind::NOT) { - preRegisterTerm(fact[0]); - } else { - preRegisterTerm(fact); - } - } - // Do the work bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; @@ -90,31 +80,8 @@ void TheoryUF::check(Effort level) { } } - // If in conflict, output the conflict - if (d_conflict) { - Debug("uf") << "TheoryUF::check(): conflict " << d_conflictNode << std::endl; - d_out->conflict(d_conflictNode); - } - - // Otherwise we propagate in order to detect a weird conflict like - // p, x = y - // p -> f(x) != f(y) -- f(x) = f(y) gets added to the propagation list at preregistration time - // but when f(x) != f(y) is deduced by the sat solver, so it's asserted, and we don't detect the conflict - // until we go through the propagation list - propagate(level); }/* TheoryUF::check() */ -void TheoryUF::propagate(Effort level) { - Debug("uf") << "TheoryUF::propagate()" << std::endl; - if (!d_conflict) { - 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; - d_out->propagate(literal); - } - } -}/* TheoryUF::propagate(Effort) */ - void TheoryUF::preRegisterTerm(TNode node) { Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl; @@ -143,37 +110,18 @@ void TheoryUF::preRegisterTerm(TNode node) { }/* TheoryUF::preRegisterTerm() */ bool TheoryUF::propagate(TNode literal) { - Debug("uf") << "TheoryUF::propagate(" << literal << ")" << std::endl; - + Debug("uf::propagate") << "TheoryUF::propagate(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("uf") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl; + Debug("uf::propagate") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl; return false; } - - // See if the literal has been asserted already - Node normalized = Rewriter::rewrite(literal); - - // If asserted and is false, we're done or in conflict - // Note that even trivial equalities have a SAT value (i.e. 1 = 2 -> false) - bool satValue = false; - if (d_valuation.hasSatValue(normalized, satValue) && !satValue) { - Debug("uf") << "TheoryUF::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; - std::vector assumptions; - Node negatedLiteral; - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - return false; + // Propagate out + bool ok = d_out->propagate(literal); + if (!ok) { + d_conflict = true; } - - // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("uf") << "TheoryUF::propagate(" << literal << ") => enqueuing for propagation" << std::endl; - d_literalsToPropagate.push_back(literal); - - return true; + return ok; }/* TheoryUF::propagate(TNode) */ void TheoryUF::explain(TNode literal, std::vector& assumptions) { @@ -437,3 +385,13 @@ void TheoryUF::computeCareGraph() { } } }/* TheoryUF::computeCareGraph() */ + +void TheoryUF::conflict(TNode a, TNode b) { + if (Theory::theoryOf(a) == theory::THEORY_BOOL) { + d_conflictNode = explain(a.iffNode(b)); + } else { + d_conflictNode = explain(a.eqNode(b)); + } + d_out->conflict(d_conflictNode); + d_conflict = true; +} diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 1dfcb86f0..0d35d57d8 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -55,7 +55,7 @@ public: } bool eqNotifyTriggerPredicate(TNode predicate, bool value) { - Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl; + Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { return d_uf.propagate(predicate); } else { @@ -64,7 +64,7 @@ public: } bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << std::endl; + Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; if (value) { return d_uf.propagate(t1.eqNode(t2)); } else { @@ -73,12 +73,9 @@ public: } bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; - if (Theory::theoryOf(t1) == THEORY_BOOL) { - return d_uf.propagate(t1.iffNode(t2)); - } else { - return d_uf.propagate(t1.eqNode(t2)); - } + Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + d_uf.conflict(t1, t2); + return false; } }; @@ -119,13 +116,15 @@ private: /** Symmetry analyzer */ SymmetryBreaker d_symb; + /** Conflict when merging two constants */ + void conflict(TNode a, TNode b); + public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); void check(Effort); - void propagate(Effort); void preRegisterTerm(TNode term); Node explain(TNode n); @@ -135,6 +134,8 @@ public: void addSharedTerm(TNode n); void computeCareGraph(); + void propagate(Effort effort) {} + EqualityStatus getEqualityStatus(TNode a, TNode b); std::string identify() const { -- cgit v1.2.3