diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
commit | d01d291be3213368985f28d0072905c4f033d5ff (patch) | |
tree | 8524a2b6a00c012221ecca9266c3ab9fb11989ed /src/theory/uf | |
parent | 889853e225687dfef36b15ca1dccf74682e0fd66 (diff) |
merge from arrays-clark branch
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/equality_engine.h | 17 | ||||
-rw-r--r-- | src/theory/uf/equality_engine_impl.h | 65 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 47 |
3 files changed, 76 insertions, 53 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index d8757926a..4eabf63de 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -558,6 +558,11 @@ private: /** The false node */ Node d_false; + /** + * Adds an equality of terms t1 and t2 to the database. + */ + void addEqualityInternal(TNode t1, TNode t2, TNode reason); + public: /** @@ -617,6 +622,11 @@ public: bool hasTerm(TNode t) const; /** + * Adds aa predicate t with given polarity + */ + void addPredicate(TNode t, bool polarity, TNode reason); + + /** * Adds an equality t1 = t2 to the database. */ void addEquality(TNode t1, TNode t2, TNode reason); @@ -693,6 +703,13 @@ public: * Check whether the two term are dis-equal. */ bool areDisequal(TNode t1, TNode t2); + + /** + * Return the number of nodes in the equivalence class contianing t + * Adds t if not already there. + */ + size_t getSize(TNode t); + }; } // Namespace uf diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h index dd1bf0cbc..be12e5f19 100644 --- a/src/theory/uf/equality_engine_impl.h +++ b/src/theory/uf/equality_engine_impl.h @@ -188,9 +188,9 @@ const EqualityNode& EqualityEngine<NotifyClass>::getEqualityNode(EqualityNodeId } template <typename NotifyClass> -void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason) { +void EqualityEngine<NotifyClass>::addEqualityInternal(TNode t1, TNode t2, TNode reason) { - Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << "EqualityEngine::addEqualityInternal(" << t1 << "," << t2 << ")" << std::endl; // Add the terms if they are not already in the database addTerm(t1); @@ -200,19 +200,39 @@ void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason) EqualityNodeId t1Id = getNodeId(t1); EqualityNodeId t2Id = getNodeId(t2); enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason)); + propagate(); } template <typename NotifyClass> +void EqualityEngine<NotifyClass>::addPredicate(TNode t, bool polarity, TNode reason) { + + Debug("equality") << "EqualityEngine::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl; + + addEqualityInternal(t, polarity ? d_true : d_false, reason); +} + +template <typename NotifyClass> +void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason) { + + Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl; + + addEqualityInternal(t1, t2, reason); + + Node equality = t1.eqNode(t2); + addEqualityInternal(equality, d_true, reason); +} + +template <typename NotifyClass> void EqualityEngine<NotifyClass>::addDisequality(TNode t1, TNode t2, TNode reason) { Debug("equality") << "EqualityEngine::addDisequality(" << t1 << "," << t2 << ")" << std::endl; Node equality1 = t1.eqNode(t2); - addEquality(equality1, d_false, reason); - + addEqualityInternal(equality1, d_false, reason); + Node equality2 = t2.eqNode(t1); - addEquality(equality2, d_false, reason); + addEqualityInternal(equality2, d_false, reason); } @@ -516,9 +536,6 @@ void EqualityEngine<NotifyClass>::explainEquality(TNode t1, TNode t2, std::vecto // Don't notify during this check ScopedBool turnOfNotify(d_performNotify, false); - // Push the context, so that we can remove the terms later - d_context->push(); - // Add the terms (they might not be there) addTerm(t1); addTerm(t2); @@ -537,8 +554,6 @@ void EqualityEngine<NotifyClass>::explainEquality(TNode t1, TNode t2, std::vecto EqualityNodeId t2Id = getNodeId(t2); getExplanation(t1Id, t2Id, equalities); - // Pop the possible extra information - d_context->pop(); } template <typename NotifyClass> @@ -548,9 +563,6 @@ void EqualityEngine<NotifyClass>::explainDisequality(TNode t1, TNode t2, std::ve // Don't notify during this check ScopedBool turnOfNotify(d_performNotify, false); - // Push the context, so that we can remove the terms later - d_context->push(); - // Add the terms addTerm(t1); addTerm(t2); @@ -573,8 +585,6 @@ void EqualityEngine<NotifyClass>::explainDisequality(TNode t1, TNode t2, std::ve EqualityNodeId falseId = getNodeId(d_false); getExplanation(equalityId, falseId, equalities); - // Pop the possible extra information - d_context->pop(); } @@ -722,6 +732,10 @@ void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode t } } + if (Debug.isOn("equality::internal")) { + debugPrintGraph(); + } + Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl; } @@ -809,17 +823,11 @@ bool EqualityEngine<NotifyClass>::areEqual(TNode t1, TNode t2) // Don't notify during this check ScopedBool turnOfNotify(d_performNotify, false); - // Push the context, so that we can remove the terms later - d_context->push(); - // Add the terms addTerm(t1); addTerm(t2); bool equal = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind(); - // Pop the context (triggers new term removal) - d_context->pop(); - // Return whether the two terms are equal return equal; } @@ -830,9 +838,6 @@ bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2) // Don't notify during this check ScopedBool turnOfNotify(d_performNotify, false); - // Push the context, so that we can remove the terms later - d_context->push(); - // Add the terms addTerm(t1); addTerm(t2); @@ -841,18 +846,22 @@ bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2) Node equality = t1.eqNode(t2); addTerm(equality); if (getEqualityNode(equality).getFind() == getEqualityNode(d_false).getFind()) { - d_context->pop(); return true; } - // Pop the context (triggers new term removal) - d_context->pop(); - // Return whether the terms are disequal return false; } template <typename NotifyClass> +size_t EqualityEngine<NotifyClass>::getSize(TNode t) +{ + // Add the term + addTerm(t); + return getEqualityNode(getEqualityNode(t).getFind()).getSize(); +} + +template <typename NotifyClass> void EqualityEngine<NotifyClass>::addTriggerTerm(TNode t) { Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ")" << std::endl; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 4ac81bc74..f53918683 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -96,11 +96,11 @@ void TheoryUF::check(Effort level) { d_equalityEngine.addEquality(fact[0], fact[1], fact); break; case kind::APPLY_UF: - d_equalityEngine.addEquality(fact, d_true, fact); + d_equalityEngine.addPredicate(fact, true, fact); break; case kind::NOT: if (fact[0].getKind() == kind::APPLY_UF) { - d_equalityEngine.addEquality(fact[0], d_false, fact); + d_equalityEngine.addPredicate(fact[0], false, fact); } else { // Assert the dis-equality d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact); @@ -132,24 +132,21 @@ void TheoryUF::propagate(Effort level) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl; bool satValue; - if (!d_valuation.hasSatValue(literal, satValue)) { + Node normalized = Rewriter::rewrite(literal); + if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { d_out->propagate(literal); } else { - if (!satValue) { - Debug("uf") << "TheoryUF::propagate(): in conflict" << std::endl; - Node negatedLiteral; - std::vector<TNode> assumptions; - if (literal != d_false) { - negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); - assumptions.push_back(negatedLiteral); - } - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - break; - } else { - Debug("uf") << "TheoryUF::propagate(): already asserted" << std::endl; + Debug("uf") << "TheoryUF::propagate(): in conflict, normalized = " << normalized << std::endl; + Node negatedLiteral; + std::vector<TNode> assumptions; + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); } + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + break; } } } @@ -196,20 +193,18 @@ bool TheoryUF::propagate(TNode literal) { } // See if the literal has been asserted already + Node normalized = Rewriter::rewrite(literal); bool satValue = false; - bool isAsserted = literal == d_false || d_valuation.hasSatValue(literal, satValue); + bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue); // If asserted, we're done or in conflict if (isAsserted) { - if (satValue) { - Debug("uf") << "TheoryUF::propagate(" << literal << ") => already known" << std::endl; - return true; - } else { - Debug("uf") << "TheoryUF::propagate(" << literal << ") => conflict" << std::endl; + if (!satValue) { + Debug("uf") << "TheoryUF::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; std::vector<TNode> assumptions; Node negatedLiteral; - if (literal != d_false) { - negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); assumptions.push_back(negatedLiteral); } explain(literal, assumptions); @@ -217,6 +212,8 @@ bool TheoryUF::propagate(TNode literal) { d_conflict = true; return false; } + // Propagate even if already known in SAT - could be a new equation between shared terms + // (terms that weren't shared when the literal was asserted!) } // Nothing, just enqueue it for propagation and mark it as asserted already |