From e761ec344a7c9d9b5bff5f312cdb8932083e0bc8 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Sun, 10 Jun 2012 03:03:17 +0000 Subject: [PATCH] fixes for bug347 it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately --- src/theory/arith/congruence_manager.h | 6 +- src/theory/arrays/theory_arrays.h | 3 +- src/theory/bv/bv_subtheory_eq.cpp | 33 +-- src/theory/bv/bv_subtheory_eq.h | 12 +- src/theory/shared_terms_database.h | 3 +- src/theory/theory_engine.cpp | 18 +- src/theory/uf/equality_engine.cpp | 263 ++++++++++++++++-------- src/theory/uf/equality_engine.h | 33 ++- src/theory/uf/theory_uf.h | 3 +- test/regress/regress0/aufbv/Makefile.am | 1 + test/regress/regress0/aufbv/bug347.smt | 11 + 11 files changed, 260 insertions(+), 126 deletions(-) create mode 100644 test/regress/regress0/aufbv/bug347.smt diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 5e4616628..5f49ab3ab 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -65,12 +65,12 @@ private: } } - bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; if (t1.getKind() == kind::CONST_BOOLEAN) { - return d_acm.propagate(t1.iffNode(t2)); + d_acm.propagate(t1.iffNode(t2)); } else { - return d_acm.propagate(t1.eqNode(t2)); + d_acm.propagate(t1.eqNode(t2)); } } }; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 3ae0146c1..54d20d478 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -266,10 +266,9 @@ class TheoryArrays : public Theory { return true; } - bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; d_arrays.conflict(t1, t2); - return false; } }; diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp index 98678a9b4..afb4a8b4a 100644 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -29,7 +29,7 @@ using namespace CVC4::theory::bv::utils; EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), - d_notify(bv), + d_notify(*this), d_equalityEngine(d_notify, c, "theory::bv::TheoryBV") { if (d_useEqualityEngine) { @@ -127,34 +127,41 @@ bool EqualitySolver::addAssertions(const std::vector& assertions, Theory: bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) { BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; if (value) { - return d_bv->storePropagation(equality, TheoryBV::SUB_EQUALITY); + return d_solver.storePropagation(equality); } else { - return d_bv->storePropagation(equality.notNode(), TheoryBV::SUB_EQUALITY); + return d_solver.storePropagation(equality.notNode()); } } bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) { BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl; if (value) { - return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY); + return d_solver.storePropagation(predicate); } else { - return d_bv->storePropagation(predicate.notNode(), TheoryBV::SUB_EQUALITY); + return d_solver.storePropagation(predicate.notNode()); } } bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl; if (value) { - return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY); + return d_solver.storePropagation(t1.eqNode(t2)); } else { - return d_bv->storePropagation(t1.eqNode(t2).notNode(), TheoryBV::SUB_EQUALITY); + return d_solver.storePropagation(t1.eqNode(t2).notNode()); } } -bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; - if (Theory::theoryOf(t1) == THEORY_BOOL) { - return d_bv->storePropagation(t1.iffNode(t2), TheoryBV::SUB_EQUALITY); - } - return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY); +void EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { + d_solver.conflict(t1, t2); +} + +bool EqualitySolver::storePropagation(TNode literal) { + return d_bv->storePropagation(literal, TheoryBV::SUB_EQUALITY); } + +void EqualitySolver::conflict(TNode a, TNode b) { + std::vector assumptions; + d_equalityEngine.explainEquality(a, b, true, assumptions); + d_bv->setConflict(mkAnd(assumptions)); +} + diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h index 356d12a06..d4239ff13 100644 --- a/src/theory/bv/bv_subtheory_eq.h +++ b/src/theory/bv/bv_subtheory_eq.h @@ -32,14 +32,14 @@ class EqualitySolver : public SubtheorySolver { // NotifyClass: handles call-back from congruence closure module class NotifyClass : public eq::EqualityEngineNotify { - TheoryBV* d_bv; + EqualitySolver& d_solver; public: - NotifyClass(TheoryBV* bv): d_bv(bv) {} + NotifyClass(EqualitySolver& solver): d_solver(solver) {} bool eqNotifyTriggerEquality(TNode equality, bool value); bool eqNotifyTriggerPredicate(TNode predicate, bool value); bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value); - bool eqNotifyConstantTermMerge(TNode t1, TNode t2); + void eqNotifyConstantTermMerge(TNode t1, TNode t2); }; @@ -49,6 +49,12 @@ class EqualitySolver : public SubtheorySolver { /** Equality engine */ eq::EqualityEngine d_equalityEngine; + /** Store a propagation to the bv solver */ + bool storePropagation(TNode literal); + + /** Store a conflict from merging two constants */ + void conflict(TNode a, TNode b); + public: EqualitySolver(context::Context* c, TheoryBV* bv); diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 1a38d7332..fccd2e6bc 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -92,9 +92,8 @@ private: return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value); } - bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { d_sharedTerms.conflict(t1, t2, true); - return false; } }; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a7b13dc2f..0be232bfa 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -763,13 +763,17 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, d_factsAsserted = true; } else { Assert(toTheoryId == THEORY_SAT_SOLVER); - // Enqueue for propagation to the SAT solver - d_propagatedLiterals.push_back(assertion); // Check for propositional conflict bool value; - if (d_propEngine->hasValue(assertion, value) && !value) { - d_inConflict = true; - } + if (d_propEngine->hasValue(assertion, value)) { + if (!value) { + Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict" << std::endl; + d_inConflict = true; + } else { + return; + } + } + d_propagatedLiterals.push_back(assertion); } return; } @@ -994,7 +998,7 @@ static Node mkExplanation(const std::vector& explanation) { Node TheoryEngine::getExplanation(TNode node) { - Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl; + Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current proagation index = " << d_propagationMapTimestamp << std::endl; bool polarity = node.getKind() != kind::NOT; TNode atom = polarity ? node : node[0]; @@ -1165,8 +1169,8 @@ void TheoryEngine::getExplanation(std::vector& explanationVector } else { explanation = theoryOf(toExplain.theory)->explain(toExplain.node); } - Assert(explanation != toExplain.node, "wansn't sent to you, so why are you explaining it trivially"); Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << std::endl; + Assert(explanation != toExplain.node, "wansn't sent to you, so why are you explaining it trivially"); // Mark the explanation NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); explanationVector.push_back(newExplain); diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 1f45b7827..25645c472 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -91,6 +91,9 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name) , d_triggerDatabaseSize(context, 0) , d_triggerTermSetUpdatesSize(context, 0) , d_deducedDisequalitiesSize(context, 0) +, d_deducedDisequalityReasonsSize(context, 0) +, d_propagatedDisequalities(context) +, d_name(name) { init(); } @@ -109,6 +112,8 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c , d_triggerDatabaseSize(context, 0) , d_triggerTermSetUpdatesSize(context, 0) , d_deducedDisequalitiesSize(context, 0) +, d_deducedDisequalityReasonsSize(context, 0) +, d_propagatedDisequalities(context) , d_name(name) { init(); @@ -388,16 +393,21 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { // Same tags, notify EqualityNodeId aSharedId = aTriggerTerms.triggers[a_i++]; EqualityNodeId bSharedId = bTriggerTerms.triggers[b_i++]; - d_deducedDisequalityReasons.push_back(EqualityPair(aSharedId, a)); - 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) - Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ": notifying " << aTag << " for " << d_nodes[aSharedId] << " != " << d_nodes[bSharedId] << std::endl; - if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) { - break; + // Propagate + if (!hasPropagatedDisequality(aTag, aSharedId, bSharedId)) { + // Store a proof if not there already + if (!hasPropagatedDisequality(aSharedId, bSharedId)) { + d_deducedDisequalityReasons.push_back(EqualityPair(aSharedId, a)); + d_deducedDisequalityReasons.push_back(EqualityPair(bSharedId, b)); + d_deducedDisequalityReasons.push_back(EqualityPair(eqId, d_falseId)); + } + // Store the propagation + storePropagatedDisequality(aTag, aSharedId, bSharedId); + // Notify + Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ": notifying " << aTag << " for " << d_nodes[aSharedId] << " != " << d_nodes[bSharedId] << std::endl; + if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) { + break; + } } // Pop the next tags aTag = Theory::setPop(aTags); @@ -431,6 +441,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect bool class1isConstant = d_isConstant[class1Id]; bool class2isConstant = d_isConstant[class2Id]; Assert(class1isConstant || !class2isConstant, "Should always merge into constants"); + Assert(!class1isConstant || !class2isConstant, "Don't merge constants"); // Trigger set of class 1 TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id]; @@ -548,36 +559,6 @@ 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 (class1isConstant && 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();) { - const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggersFired[i]]; - if (triggerInfo.trigger.getKind() == kind::EQUAL && !triggerInfo.polarity) { - TNode equality = triggerInfo.trigger; - EqualityNodeId original = getNodeId(equality); - d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId)); - if (!storePropagatedDisequality(equality[0], equality[1], 1)) { - // Already notified, go to the next trigger - ++ i; - continue; - } - } - // Copy - triggersFired[j++] = triggersFired[i++]; - } - triggersFired.resize(j); // Go through the trigger term disequalities and propagate if (!propagateTriggerTermDisequalities(class1OnlyTags, class1triggerRef, class2disequalitiesToNotify)) { @@ -627,7 +608,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 && !constantMerge) { + if (d_performNotify) { EqualityNodeId tag2id = class2triggers.triggers[i2++]; if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) { return false; @@ -704,7 +685,9 @@ void EqualityEngine::backtrack() { // Get the ids of the merged classes Equality& eq = d_assertedEqualities[i]; // Undo the merge - undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs); + if (eq.lhs != null_id) { + undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs); + } } d_assertedEqualities.resize(d_assertedEqualitiesCount); @@ -778,14 +761,13 @@ void EqualityEngine::backtrack() { if (d_deducedDisequalities.size() > d_deducedDisequalitiesSize) { for(int i = d_deducedDisequalities.size() - 1, i_end = (int)d_deducedDisequalitiesSize; i >= i_end; -- i) { EqualityPair pair = d_deducedDisequalities[i]; - DisequalityReasonRef reason = d_disequalityReasonsMap[pair]; + Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end()); // Remove from the map d_disequalityReasonsMap.erase(pair); std::swap(pair.first, pair.second); d_disequalityReasonsMap.erase(pair); - // Resize the reasons vector - d_deducedDisequalityReasons.resize(reason.mergesStart); } + d_deducedDisequalityReasons.resize(d_deducedDisequalityReasonsSize); d_deducedDisequalities.resize(d_deducedDisequalitiesSize); } } @@ -859,7 +841,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // We can only explain the nodes that got merged #ifdef CVC4_ASSERTIONS - bool canExplain = getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind(); + bool canExplain = getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind() + || (d_done && isConstant(t1Id) && isConstant(t2Id)); + if (!canExplain) { Warning() << "Can't explain equality:" << std::endl; Warning() << d_nodes[t1Id] << " with find " << d_nodes[getEqualityNode(t1Id).getFind()] << std::endl; @@ -954,7 +938,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Assert(isConstant(eq.b)); getExplanation(eq.b, getEqualityNode(eq.b).getFind(), equalities); Debug("equality") << pop; - + // If the constants were merged, we're in trouble + Assert(getEqualityNode(eq.a).getFind() != getEqualityNode(eq.b).getFind()); + break; } default: @@ -1136,21 +1122,36 @@ void EqualityEngine::propagate() { // Add the actual equality to the equality graph addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason); - // One more equality added - d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; + // If constants are being merged we're done + if (d_isConstant[t1classId] && d_isConstant[t2classId]) { + // When merging constants we are inconsistent, hence done + d_done = true; + // But in order to keep invariants (edges = 2*equalities) we put an equalities in + // Note that we can explain this merge as we have a graph edge + d_assertedEqualities.push_back(Equality(null_id, null_id)); + d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; + // Notify + if (d_performNotify) { + d_notify.eqNotifyConstantTermMerge(d_nodes[t1classId], d_nodes[t2classId]); + } + // Empty the queue and exit + continue; + } // Depending on the merge preference (such as size, or being a constant), merge them std::vector triggers; if ((node2.getSize() > node1.getSize() && !d_isConstant[t1classId]) || d_isConstant[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; if (!merge(node2, node1, triggers)) { d_done = true; } } else { Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl; d_assertedEqualities.push_back(Equality(t1classId, t2classId)); - if (!merge(node1, node2, triggers)) { + d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; + if (!merge(node1, node2, triggers)) { d_done = true; } } @@ -1159,10 +1160,30 @@ void EqualityEngine::propagate() { if (d_performNotify && !d_done) { for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) { const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggers[trigger_i]]; - // Notify the trigger and exit if it fails if (triggerInfo.trigger.getKind() == kind::EQUAL) { - if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) { - d_done = true; + // Special treatment for disequalities + if (!triggerInfo.polarity) { + // Store that we are propagating a diseauality + TNode equality = triggerInfo.trigger; + EqualityNodeId original = getNodeId(equality); + TNode lhs = equality[0]; + TNode rhs = equality[1]; + EqualityNodeId lhsId = getNodeId(lhs); + EqualityNodeId rhsId = getNodeId(rhs); + if (!hasPropagatedDisequality(THEORY_BOOL, lhsId, rhsId)) { + if (!hasPropagatedDisequality(lhsId, rhsId)) { + d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId)); + } + storePropagatedDisequality(THEORY_BOOL, lhsId, rhsId); + if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) { + d_done = true; + } + } + } else { + // Equalities are simple + if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) { + d_done = true; + } } } else { if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.trigger, triggerInfo.polarity)) { @@ -1211,6 +1232,11 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const EqualityNodeId t1Id = getNodeId(t1); EqualityNodeId t2Id = getNodeId(t2); + // If we propagated this disequality we're true + if (hasPropagatedDisequality(t1Id, t2Id)) { + return true; + } + // Get equivalence classes EqualityNodeId t1ClassId = getEqualityNode(t1Id).getFind(); EqualityNodeId t2ClassId = getEqualityNode(t2Id).getFind(); @@ -1223,7 +1249,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const if (ensureProof) { nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, t1ClassId)); nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, t2ClassId)); - storePropagatedDisequality(t1, t2, 2); + nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } return true; } @@ -1234,7 +1260,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const if (getEqualityNode(eq).getFind() == getEqualityNode(d_falseId).getFind()) { if (ensureProof) { nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(getNodeId(eq), d_falseId)); - storePropagatedDisequality(t1, t2, 1); + nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } return true; } @@ -1246,7 +1272,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const if (getEqualityNode(eq).getFind() == getEqualityNode(d_false).getFind()) { if (ensureProof) { nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(getNodeId(eq), d_falseId)); - storePropagatedDisequality(t1, t2, 1); + nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } return true; } @@ -1264,7 +1290,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.a, t1ClassId)); nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.b, t2ClassId)); nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId)); - storePropagatedDisequality(t1, t2, 5); + nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } return true; } @@ -1282,7 +1308,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.a, t2ClassId)); nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.b, t1ClassId)); nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId)); - storePropagatedDisequality(t1, t2, 5); + nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } return true; } @@ -1302,7 +1328,9 @@ size_t EqualityEngine::getSize(TNode t) void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) { Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; + Assert(tag != THEORY_LAST); + Assert(tag != THEORY_BOOL, "This one is used internally, bummer"); if (d_done) { return; @@ -1453,38 +1481,84 @@ EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet() { return newTriggerSetRef; } -bool EqualityEngine::storePropagatedDisequality(TNode lhs, TNode rhs, unsigned reasonsCount) const { +bool EqualityEngine::hasPropagatedDisequality(EqualityNodeId lhsId, EqualityNodeId rhsId) const { + EqualityPair eq(lhsId, rhsId); + bool propagated = d_propagatedDisequalities.find(eq) != d_propagatedDisequalities.end(); +#ifdef CVC4_ASSERTIONS + bool stored = d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end(); + Assert(propagated == stored, "These two should be in sync"); +#endif + Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (propagated ? "true" : "false") << std::endl; + return propagated; +} + +bool EqualityEngine::hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) const { - Assert(reasonsCount > 0); + EqualityPair eq(lhsId, rhsId); + PropagatedDisequalitiesMap::const_iterator it = d_propagatedDisequalities.find(eq); + if (it == d_propagatedDisequalities.end()) { + Assert(d_disequalityReasonsMap.find(eq) == d_disequalityReasonsMap.end(), "Why do we have a proof if not propagated"); + Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => false" << std::endl; + return false; + } + Assert(d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end(), "We propagated but there is no proof"); + bool result = Theory::setContains(tag, (*it).second); + Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (result ? "true" : "false") << std::endl; + return result; +} - EqualityNodeId lhsId = getNodeId(lhs); - EqualityNodeId rhsId = getNodeId(rhs); - // We are semantically const, just remembering stuff for later - EqualityEngine* nonConst = const_cast(this); +void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) { - Assert(d_deducedDisequalityReasons.size() >= reasonsCount); - DisequalityReasonRef ref(d_deducedDisequalityReasons.size() - reasonsCount, d_deducedDisequalityReasons.size()); + Assert(!hasPropagatedDisequality(tag, lhsId, rhsId), "Check before you store it"); + Assert(lhsId != rhsId, "Wow, wtf!"); -#ifdef CVC4_ASSERTIONS - for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) { - Assert(getEqualityNode(d_deducedDisequalityReasons[i].first).getFind() == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind()); + Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ")" << std::endl; + + EqualityPair pair1(lhsId, rhsId); + EqualityPair pair2(rhsId, lhsId); + + // Store the fact that we've propagated this already + Theory::Set notified = 0; + PropagatedDisequalitiesMap::const_iterator find = d_propagatedDisequalities.find(pair1); + if (find == d_propagatedDisequalities.end()) { + notified = Theory::setInsert(tag); + } else { + notified = Theory::setInsert(tag, (*find).second); } + d_propagatedDisequalities[pair1] = notified; + d_propagatedDisequalities[pair2] = notified; + + // Store the proof if provided + if (d_deducedDisequalityReasons.size() > d_deducedDisequalityReasonsSize) { + Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << "): storing proof" << std::endl; + Assert(d_disequalityReasonsMap.find(pair1) == d_disequalityReasonsMap.end(), "There can't be a proof if you're adding a new one"); + DisequalityReasonRef ref(d_deducedDisequalityReasonsSize, d_deducedDisequalityReasons.size()); +#ifdef CVC4_ASSERTIONS + // Check that the reasons are valid + for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) { + Assert(getEqualityNode(d_deducedDisequalityReasons[i].first).getFind() == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind()); + } #endif + if (Debug.isOn("equality::disequality")) { + for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) { + TNode lhs = d_nodes[d_deducedDisequalityReasons[i].first]; + TNode rhs = d_nodes[d_deducedDisequalityReasons[i].second]; + Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(): because " << lhs << " == " << rhs << std::endl; + } - EqualityPair pair(lhsId, rhsId); - DisequalityReasonsMap::const_iterator find = d_disequalityReasonsMap.find(pair); - if (find == d_disequalityReasonsMap.end()) { - nonConst->d_disequalityReasonsMap[pair] = ref; - nonConst->d_deducedDisequalities.push_back(pair); - nonConst->d_deducedDisequalitiesSize = d_deducedDisequalities.size(); - std::swap(pair.first, pair.second); - nonConst->d_disequalityReasonsMap[pair] = ref; - return true; + } + + // Store for backtracking + d_deducedDisequalities.push_back(pair1); + d_deducedDisequalitiesSize = d_deducedDisequalities.size(); + d_deducedDisequalityReasonsSize = d_deducedDisequalityReasons.size(); + // Store the proof reference + d_disequalityReasonsMap[pair1] = ref; + d_disequalityReasonsMap[pair2] = ref; } else { - nonConst->d_deducedDisequalities.resize(d_deducedDisequalitiesSize); - return false; + Assert(d_disequalityReasonsMap.find(pair1) != d_disequalityReasonsMap.end(), "You must provide a proof initially"); } } @@ -1583,21 +1657,32 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger // Figure out who we are comparing to in the original equality EqualityNodeId toCompare = disequalityInfo.lhs ? fun.a : fun.b; EqualityNodeId myCompare = disequalityInfo.lhs ? fun.b : fun.a; + if (getEqualityNode(toCompare).getFind() == getEqualityNode(myCompare).getFind()) { + // We're propagating a != a, which means we're inconsistent, just bail and let it go into + // a regular conflict + return !d_done; + } // Go through the tags, and add the disequalities TheoryId currentTag; while (!d_done && ((currentTag = Theory::setPop(commonTags)) != THEORY_LAST)) { // Get the tag representative EqualityNodeId tagRep = disequalityTriggerSet.getTrigger(currentTag); EqualityNodeId myRep = triggerSet.getTrigger(currentTag); - // Store the propagation - d_deducedDisequalityReasons.push_back(EqualityPair(myCompare, myRep)); - d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep)); - d_deducedDisequalityReasons.push_back(EqualityPair(disequalityInfo.equalityId, d_falseId)); - storePropagatedDisequality(d_nodes[myRep], 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(currentTag, d_nodes[myRep], d_nodes[tagRep], false)) { - d_done = true; + // Propagate + if (!hasPropagatedDisequality(currentTag, myRep, tagRep)) { + // Construct the proof if not there already + if (!hasPropagatedDisequality(myRep, tagRep)) { + d_deducedDisequalityReasons.push_back(EqualityPair(myCompare, myRep)); + d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep)); + d_deducedDisequalityReasons.push_back(EqualityPair(disequalityInfo.equalityId, d_falseId)); + } + // Store the propagation + storePropagatedDisequality(currentTag, myRep, tagRep); + // Notify + if (d_performNotify) { + if (!d_notify.eqNotifyTriggerTermEquality(currentTag, d_nodes[myRep], d_nodes[tagRep], false)) { + d_done = true; + } } } } diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index ac6f458e9..8cf159cd7 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -78,12 +78,13 @@ public: virtual bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) = 0; /** - * Notifies about the merge of two constant terms. + * Notifies about the merge of two constant terms. After this, all work is suspended and all you + * can do is ask for explanations. * * @param t1 a constant term * @param t2 a constnat term */ - virtual bool eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0; + virtual void eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0; }; /** @@ -95,7 +96,7 @@ public: bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; } bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; } bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; } - bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { return true; } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { } }; @@ -521,9 +522,31 @@ private: std::vector d_deducedDisequalityReasons; /** - * Stores a propagated disequality for explanation purpooses and remembers the reasons. + * Size of the memory for disequality reasons. */ - bool storePropagatedDisequality(TNode lhs, TNode rhs, unsigned reasonsCount) const; + context::CDO d_deducedDisequalityReasonsSize; + + /** + * Map from equalities to the tags that have received the notification. + */ + typedef context::CDHashMap PropagatedDisequalitiesMap; + PropagatedDisequalitiesMap d_propagatedDisequalities; + + /** + * Has this equality been propagated to anyone. + */ + bool hasPropagatedDisequality(EqualityNodeId lhsId, EqualityNodeId rhsId) const; + + /** + * Has this equality been propagated to the tag owner. + */ + bool hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) const; + + /** + * Stores a propagated disequality for explanation purpooses and remembers the reasons. The + * reasons should be pushed on the reasons vector. + */ + void storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId); /** * An equality tagged with a set of tags. diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 0d35d57d8..eceead38a 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -72,10 +72,9 @@ public: } } - bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; d_uf.conflict(t1, t2); - return false; } }; diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index bdcaaa2d0..bec83183a 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -13,6 +13,7 @@ MAKEFLAGS = -k TESTS = \ bug00.smt \ bug338.smt2 \ + bug347.smt \ try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \ diseqprop.01.smt \ wchains010ue.delta01.smt \ diff --git a/test/regress/regress0/aufbv/bug347.smt b/test/regress/regress0/aufbv/bug347.smt new file mode 100644 index 000000000..f467cd4b3 --- /dev/null +++ b/test/regress/regress0/aufbv/bug347.smt @@ -0,0 +1,11 @@ +(benchmark B_ + :status sat + :category { unknown } + :logic QF_AUFBV + :extrafuns ((delete_0_val_1 BitVec[32])) + :extrafuns ((delete_0_curr_6 BitVec[32])) + :extrafuns ((arr_next_13 Array[32:32])) + :extrafuns ((arr_next_14 Array[32:32])) + :extrafuns ((delete_0_head_1 BitVec[32])) + :formula (and (= bv0[32] (ite (= bv0[32] delete_0_head_1) (select arr_next_14 delete_0_curr_6) delete_0_curr_6)) (= arr_next_14 arr_next_13) (= bv1[32] (select arr_next_13 bv1[32])) (= delete_0_curr_6 (ite (= bv0[32] delete_0_val_1) bv0[32] bv1[32]))) +) -- 2.30.2