From: Dejan Jovanović Date: Sun, 10 Jun 2012 03:03:17 +0000 (+0000) Subject: fixes for bug347 X-Git-Tag: cvc5-1.0.0~8095 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e761ec344a7c9d9b5bff5f312cdb8932083e0bc8;p=cvc5.git 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 --- 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]))) +)