diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-06 06:12:40 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-06 06:12:40 +0000 |
commit | fd9e22c4a2e57c3dfeda4de3842a3fb3ca4776ba (patch) | |
tree | 047e4d27f725e9157ed5bef5357d0d72560218ae /src/theory | |
parent | 2799ae1cf57ed2b98387a1de1325bccd89bd2a30 (diff) |
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
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 104 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 12 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_eq.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 57 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 23 | ||||
-rw-r--r-- | src/theory/output_channel.h | 3 | ||||
-rw-r--r-- | src/theory/shared_terms_database.cpp | 268 | ||||
-rw-r--r-- | src/theory/shared_terms_database.h | 158 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 757 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 245 | ||||
-rw-r--r-- | src/theory/theory_test_utils.h | 3 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 170 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 7 | ||||
-rw-r--r-- | src/theory/uf/equality_engine_types.h | 37 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 76 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 19 |
16 files changed, 945 insertions, 1000 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 65e409012..4ba4aeba5 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -319,33 +319,12 @@ bool TheoryArrays::propagate(TNode literal) return false; } - // See if the literal has been asserted already - Node normalized = Rewriter::rewrite(literal); - bool satValue = false; - bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue); - - // If asserted, we're done or in conflict - if (isAsserted) { - if (!satValue) { - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; - std::vector<TNode> 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 even if already known in SAT - could be a new equation between shared terms - // (terms that weren't shared when the literal was asserted!) + // Propagate away + bool ok = d_out->propagate(literal); + if (!ok) { + d_conflict = true; } - - // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl; - d_literalsToPropagate.push_back(literal); - - return true; + return ok; }/* TheoryArrays::propagate(TNode) */ @@ -479,29 +458,7 @@ void TheoryArrays::preRegisterTerm(TNode node) void TheoryArrays::propagate(Effort e) { - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl; - if (!d_conflict) { - for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { - TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl; - bool satValue; - Node normalized = Rewriter::rewrite(literal); - if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { - d_out->propagate(literal); - } else { - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl; - Node negatedLiteral; - std::vector<TNode> assumptions; - 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; - } - } - } - + // direct propagation now } @@ -634,6 +591,7 @@ void TheoryArrays::computeCareGraph() break; case EQUALITY_FALSE_IN_MODEL: Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl; + continue; break; default: break; @@ -700,11 +658,21 @@ void TheoryArrays::check(Effort e) { Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl; - // If the assertion doesn't have a literal, it's a shared equality - Assert(assertion.isPreregistered || - ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) || - (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL && - d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1])))); + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + + if (!assertion.isPreregistered) { + if (atom.getKind() == kind::EQUAL) { + if (!d_equalityEngine.hasTerm(atom[0])) { + Assert(atom[0].isConst()); + d_equalityEngine.addTerm(atom[0]); + } + if (!d_equalityEngine.hasTerm(atom[1])) { + Assert(atom[1].isConst()); + d_equalityEngine.addTerm(atom[1]); + } + } + } // Do the work switch (fact.getKind()) { @@ -758,19 +726,10 @@ void TheoryArrays::check(Effort e) { } // If in conflict, output the conflict - if (d_conflict) { - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl; - d_out->conflict(d_conflictNode); - } - else { - // Otherwise we propagate - propagate(e); - - if(!d_eagerLemmas && fullEffort(e) && !d_conflict) { - // generate the lemmas on the worklist - Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n"; - dischargeLemmas(); - } + if(!d_eagerLemmas && fullEffort(e) && !d_conflict) { + // generate the lemmas on the worklist + Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n"; + dischargeLemmas(); } Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; @@ -1138,6 +1097,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) TNode b = lem.second; TNode i = lem.third; TNode j = lem.fourth; + Assert(a.getType().isArray() && b.getType().isArray()); if (d_equalityEngine.areEqual(a,b) || d_equalityEngine.areEqual(i,j)) { @@ -1345,6 +1305,16 @@ void TheoryArrays::dischargeLemmas() } } +void TheoryArrays::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; +} + }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index d17caba45..6592e86cf 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -261,11 +261,8 @@ class TheoryArrays : public Theory { bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; - if (Theory::theoryOf(t1) == THEORY_BOOL) { - return d_arrays.propagate(t1.iffNode(t2)); - } else { - return d_arrays.propagate(t1.eqNode(t2)); - } + d_arrays.conflict(t1, t2); + return false; } }; @@ -275,9 +272,12 @@ class TheoryArrays : public Theory { /** Equaltity engine */ eq::EqualityEngine d_equalityEngine; - // Are we in conflict? + /** Are we in conflict? */ context::CDO<bool> d_conflict; + /** Conflict when merging constants */ + void conflict(TNode a, TNode b); + /** The conflict node */ Node d_conflictNode; diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp index 807d90137..98678a9b4 100644 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -134,7 +134,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool v } bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) { - BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl; + BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl; if (value) { return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY); } else { @@ -143,7 +143,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool } bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl; + Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl; if (value) { return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY); } else { @@ -152,7 +152,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNod } bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; + 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); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 251650bf2..30493737a 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -141,58 +141,9 @@ void TheoryBV::propagate(Effort e) { } // go through stored propagations - for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); - d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) - { + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - Node normalized = Rewriter::rewrite(literal); - - TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; - bool isSharedLiteral = (atom.getKind() == kind::EQUAL && - (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() && - d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end())); - - // Check if this is a SAT literal - if (d_valuation.isSatLiteral(normalized)) { - bool satValue = false; - if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { - // check if we already propagated the negation - Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal); - if (d_alreadyPropagatedSet.find(negLiteral) != d_alreadyPropagatedSet.end()) { - Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; - // we are in conflict - std::vector<TNode> assumptions; - explain(literal, assumptions); - explain(negLiteral, assumptions); - setConflict(mkAnd(assumptions)); - return; - } - // If it's not a shared literal and hasn't already been set to true, we propagate the normalized version - // shared literals are handled below - if (!isSharedLiteral && !satValue) { - BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << normalized << std::endl; - d_out->propagate(normalized); - d_alreadyPropagatedSet.insert(normalized); - return; - } - } else { - // - Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; - Node negatedLiteral; - std::vector<TNode> assumptions; - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - explain(literal, assumptions); - setConflict(mkAnd(assumptions)); - return; - } - } - // Either it was not a SAT literal or it was but it is also shared - in that case we have to propagate the original literal (not the normalized one) - if (isSharedLiteral) { - BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl; - d_out->propagate(literal); - d_alreadyPropagatedSet.insert(literal); - } + d_out->propagate(literal); } } @@ -269,16 +220,18 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) { // Ask the appropriate subtheory for the explanation if (propagatedBy(literal, SUB_EQUALITY)) { + BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl; d_equalitySolver.explain(literal, assumptions); } else { Assert(propagatedBy(literal, SUB_BITBLAST)); + BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl; d_bitblastSolver.explain(literal, assumptions); } } Node TheoryBV::explain(TNode node) { - BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; + BVDebug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl; std::vector<TNode> assumptions; // Ask for the explanation diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 3736da639..c456ef73f 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -72,11 +72,26 @@ inline Node mkVar(unsigned size) { } inline Node mkAnd(std::vector<TNode>& children) { - if (children.size() > 1) { - return NodeManager::currentNM()->mkNode(kind::AND, children); - } else { - return children[0]; + std::set<TNode> distinctChildren; + distinctChildren.insert(children.begin(), children.end()); + + if (children.size() == 0) { + return mkTrue(); + } + + if (children.size() == 1) { + return *children.begin(); } + + NodeBuilder<> conjunction(kind::AND); + std::set<TNode>::const_iterator it = distinctChildren.begin(); + std::set<TNode>::const_iterator it_end = distinctChildren.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + + return conjunction; } inline Node mkSortedNode(Kind kind, std::vector<Node>& children) { diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 71bbefb6a..5c2cedf5b 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -103,8 +103,9 @@ public: * Propagate a theory literal. * * @param n - a theory consequence at the current decision level + * @return false if an immediate conflict was encountered */ - virtual void propagate(TNode n) throw(AssertionException) = 0; + virtual bool propagate(TNode n) throw(AssertionException) = 0; /** * Request that the core make a decision on this atom. The decision diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 0c893482a..b081e27ef 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -15,25 +15,26 @@ ** \todo document this file **/ + #include "theory/shared_terms_database.h" +#include "theory/theory_engine.h" using namespace std; using namespace CVC4; using namespace theory; -SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context) - : ContextNotifyObj(context), - d_context(context), - d_statSharedTerms("theory::shared_terms", 0), - d_addedSharedTermsSize(context, 0), - d_termsToTheories(context), - d_alreadyNotifiedMap(context), - d_sharedNotify(notify), - d_termToNotifyList(context), - d_allocatedNLSize(0), - d_allocatedNLNext(context, 0), - d_EENotify(*this), - d_equalityEngine(d_EENotify, context, "SharedTermsDatabase") +SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context) +: ContextNotifyObj(context) +, d_context(context) +, d_statSharedTerms("theory::shared_terms", 0) +, d_addedSharedTermsSize(context, 0) +, d_termsToTheories(context) +, d_alreadyNotifiedMap(context) +, d_registeredEqualities(context) +, d_EENotify(*this) +, d_equalityEngine(d_EENotify, context, "SharedTermsDatabase") +, d_theoryEngine(theoryEngine) +, d_inConflict(context, false) { StatisticsRegistry::registerStat(&d_statSharedTerms); } @@ -41,11 +42,15 @@ SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException) { StatisticsRegistry::unregisterStat(&d_statSharedTerms); - for (unsigned i = 0; i < d_allocatedNLSize; ++i) { - d_allocatedNL[i]->deleteSelf(); - } } +void SharedTermsDatabase::addEqualityToPropagate(TNode equality) { + d_registeredEqualities.insert(equality); + d_equalityEngine.addTriggerEquality(equality); + checkForConflict(); +} + + void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) { Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl; @@ -57,9 +62,6 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo d_addedSharedTerms.push_back(atom); d_addedSharedTermsSize = d_addedSharedTermsSize + 1; d_termsToTheories[search_pair] = theories; - if (!d_equalityEngine.hasTerm(term)) { - d_equalityEngine.addTriggerTerm(term, THEORY_UF); - } } else { Assert(theories != (*find).second); d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second); @@ -120,104 +122,26 @@ Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const { } } - -SharedTermsDatabase::NotifyList* SharedTermsDatabase::getNewNotifyList() +bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNode b, bool value) { - NotifyList* retval; - if (d_allocatedNLSize == d_allocatedNLNext) { - retval = new (true) NotifyList(d_context); - d_allocatedNL.push_back(retval); - d_allocatedNLNext = ++d_allocatedNLSize; - } - else { - retval = d_allocatedNL[d_allocatedNLNext]; - d_allocatedNLNext = d_allocatedNLNext + 1; - } - Assert(retval->empty()); - return retval; -} + Debug("shared-terms-database") << "SharedTermsDatabase::newEquality(" << theory << a << "," << b << ", " << (value ? "true" : "false") << ")" << endl; - -void SharedTermsDatabase::mergeSharedTerms(TNode a, TNode b) -{ - // Note: a is the new representative - Debug("shared-terms-database") << "SharedTermsDatabase::mergeSharedTerms(" << a << "," << b << ")" << endl; - - NotifyList* pnlLeft = NULL; - NotifyList* pnlRight = NULL; - - TermToNotifyList::iterator it = d_termToNotifyList.find(a); - if (it == d_termToNotifyList.end()) { - pnlLeft = getNewNotifyList(); - d_termToNotifyList[a] = pnlLeft; - } - else { - pnlLeft = (*it).second; - } - it = d_termToNotifyList.find(b); - if (it != d_termToNotifyList.end()) { - pnlRight = (*it).second; + if (d_inConflict) { + return false; } - // Get theories interested in EC for lhs - Theory::Set lhsSet = getNotifiedTheories(a); - Theory::Set rhsSet = getNotifiedTheories(b); - NotifyList::iterator nit; - TNode left, right; - - for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) { - - if (Theory::setContains(currentTheory, rhsSet)) { - right = b; - } - else if (pnlRight != NULL && - ((nit = pnlRight->find(currentTheory)) != pnlRight->end())) { - right = (*nit).second; - } - else { - // no match for right: continue - continue; - } - - if (Theory::setContains(currentTheory, lhsSet)) { - left = a; - } - else if ((nit = pnlLeft->find(currentTheory)) != pnlLeft->end()) { - left = (*nit).second; - } - else { - // no match for left: insert right into left - (*pnlLeft)[currentTheory] = right; - continue; - } - - // New shared equality: notify the client - - // TODO: add propagation of disequalities? - - assertEq(left.eqNode(right), currentTheory); + // Propagate away + Node equality = a.eqNode(b); + if (value) { + d_theoryEngine->assertToTheory(equality, theory, THEORY_BUILTIN); + } else { + d_theoryEngine->assertToTheory(equality.notNode(), theory, THEORY_BUILTIN); } -} - - -void SharedTermsDatabase::assertEq(TNode equality, TheoryId theory) -{ - Debug("shared-terms-database") << "SharedTermsDatabase::assertEq(" << equality << ") to theory " << theory << endl; - Node normalized = Rewriter::rewriteEquality(theory, equality); - if (normalized.getKind() != kind::CONST_BOOLEAN || !normalized.getConst<bool>()) { - // Notify client - d_sharedNotify.notify(normalized, equality, theory); - } + // As you were + return true; } - -// term was just part of an assertion that makes it shared for theories -// Let's mark that the set theories has now been notified -// In addition, we make sure the equivalence class containing term knows a -// representative for each theory in theories. -// Finally, if the EC already knows a rep for a theory that was just notified, we -// have to tell the theory that these two terms are equal. void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { // Find out if there are any new theories that were notified about this term @@ -232,87 +156,46 @@ void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { if (newlyNotified == 0) { return; } - + Debug("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term << ")" << endl; // First update the set of notified theories for this term d_alreadyNotifiedMap[term] = Theory::setUnion(newlyNotified, alreadyNotified); - // Now get the representative of the equivalence class and find out which theories it represents - TNode rep = d_equalityEngine.getRepresentative(term); - if (rep != term) { - alreadyNotified = 0; - theoriesFind = d_alreadyNotifiedMap.find(rep); - if (theoriesFind != d_alreadyNotifiedMap.end()) { - alreadyNotified = (*theoriesFind).second; - } - } - - // For each theory that is newly notified - for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) { - if (Theory::setContains(theory, newlyNotified)) { - - Debug("shared-terms-database") << "SharedTermsDatabase::markNotified: processing theory " << theory << endl; - - if (Theory::setContains(theory, alreadyNotified)) { - // rep represents this theory already, need to assert that term = rep - Assert(rep != term); - assertEq(rep.eqNode(term), theory); - } - else { - // Get the list of terms representing theories for this EC - TermToNotifyList::iterator it = d_termToNotifyList.find(rep); - if (it == d_termToNotifyList.end()) { - // No need to do anything - no list associated with this EC - Assert(term == rep); - } - else { - NotifyList* pnl = (*it).second; - Assert(pnl != NULL); - - // Check if this theory is already represented - NotifyList::iterator nit = pnl->find(theory); - if (nit != pnl->end()) { - // Already have a representative for this theory, assert term equal to it - assertEq((*nit).second.eqNode(term), theory); - } - else { - // if term == rep, no need to do anything, as term will represent the theory via alreadyNotifiedMap - if (term != rep) { - // No term in this EC represents this theory, so add term as a new representative - Debug("shared-terms-database") << "SharedTermsDatabase::markNotified: adding " << term << " to representative " << rep << " for theory " << theory << endl; - (*pnl)[theory] = term; - } - } - } - } - } + // Mark the shared terms in the equality engine + theory::TheoryId currentTheory; + while ((currentTheory = Theory::setPop(newlyNotified)) != THEORY_LAST) { + d_equalityEngine.addTriggerTerm(term, currentTheory); } + + // Check for any conflits + checkForConflict(); } - -bool SharedTermsDatabase::areEqual(TNode a, TNode b) { +bool SharedTermsDatabase::areEqual(TNode a, TNode b) const { return d_equalityEngine.areEqual(a,b); } - -bool SharedTermsDatabase::areDisequal(TNode a, TNode b) { +bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const { return d_equalityEngine.areDisequal(a,b,false); } -void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason) +void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode reason) { - bool negated = literal.getKind() == kind::NOT; - TNode atom = negated ? literal[0] : literal; - if (negated) { - Assert(!d_equalityEngine.areDisequal(atom[0], atom[1],false)); - d_equalityEngine.assertEquality(atom, false, reason); - // !!! need to send this out - } - else { - Assert(!d_equalityEngine.areEqual(atom[0], atom[1])); - d_equalityEngine.assertEquality(atom, true, reason); + Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl; + // Add it to the equality engine + d_equalityEngine.assertEquality(equality, polarity, reason); + // Check for conflict + checkForConflict(); +} + +bool SharedTermsDatabase::propagateEquality(TNode equality, bool polarity) { + if (polarity) { + d_theoryEngine->propagate(equality, THEORY_BUILTIN); + } else { + d_theoryEngine->propagate(equality.notNode(), THEORY_BUILTIN); } + return true; } static Node mkAnd(const std::vector<TNode>& conjunctions) { @@ -335,18 +218,35 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) { } return conjunction; -}/* mkAnd() */ +} +void SharedTermsDatabase::checkForConflict() { + if (d_inConflict) { + d_inConflict = false; + std::vector<TNode> assumptions; + d_equalityEngine.explainEquality(d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions); + Node conflict = mkAnd(assumptions); + d_theoryEngine->conflict(conflict, THEORY_BUILTIN); + d_conflictLHS = d_conflictRHS = Node::null(); + } +} -Node SharedTermsDatabase::explain(TNode literal) -{ - std::vector<TNode> assumptions; - if (literal.getKind() == kind::NOT) { - Assert(literal[0].getKind() == kind::EQUAL); - d_equalityEngine.explainEquality(literal[0][0], literal[0][1], false, assumptions); +bool SharedTermsDatabase::isKnown(TNode literal) const { + bool polarity = literal.getKind() != kind::NOT; + TNode equality = polarity ? literal : literal[0]; + if (polarity) { + return d_equalityEngine.areEqual(equality[0], equality[1]); } else { - Assert(literal.getKind() == kind::EQUAL); - d_equalityEngine.explainEquality(literal[0], literal[1], true, assumptions); + return d_equalityEngine.areDisequal(equality[0], equality[1], false); } - return mkAnd(assumptions); } + +Node SharedTermsDatabase::explain(TNode literal) const { + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + Assert(atom.getKind() == kind::EQUAL); + std::vector<TNode> assumptions; + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + return mkAnd(assumptions); +} + diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index c044097ff..1a38d7332 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -18,12 +18,14 @@ #include "expr/node.h" #include "theory/theory.h" -#include "context/context.h" -#include "util/stats.h" #include "theory/uf/equality_engine.h" +#include "util/stats.h" +#include "context/cdhashset.h" namespace CVC4 { +class TheoryEngine; + class SharedTermsDatabase : public context::ContextNotifyObj { public: @@ -54,51 +56,20 @@ private: /** Context-dependent size of the d_addedSharedTerms list */ context::CDO<unsigned> d_addedSharedTermsSize; - typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; - /** A map from atoms and subterms to the theories that use it */ + typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; SharedTermsTheoriesMap d_termsToTheories; - typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap; - /** Map from term to theories that have already been notified about the shared term */ + typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap; AlreadyNotifiedMap d_alreadyNotifiedMap; -public: - - /** Class for notifications about new shared term equalities */ - class SharedTermsNotifyClass { - public: - SharedTermsNotifyClass() {} - virtual ~SharedTermsNotifyClass() {} - virtual void notify(TNode literal, TNode original, theory::TheoryId theory) = 0; - }; + /** The registered equalities for propagation */ + typedef context::CDHashSet<TNode, TNodeHashFunction> RegisteredEqualitiesSet; + RegisteredEqualitiesSet d_registeredEqualities; private: - // Instance of class to send shared term notifications to - SharedTermsNotifyClass& d_sharedNotify; - - // Type for list of theory, node pairs: theory is theory to be notified, - // node is the representative for this equivalence class known to the - // theory that will be notified - typedef context::CDHashMap<theory::TheoryId, TNode, __gnu_cxx::hash<unsigned> > NotifyList; - typedef context::CDHashMap<TNode, NotifyList*, TNodeHashFunction> TermToNotifyList; - - // Map from terms (only valid for reps) to their notify lists - // Note that theory, term pairs only need to be in the notify list if the - // representative term is not a valid shared term for the theory. - TermToNotifyList d_termToNotifyList; - - // List of allocated NotifyList* objects - std::vector<NotifyList*> d_allocatedNL; - - // Total number of allocated NotifyList* objects - unsigned d_allocatedNLSize; - - // Size of portion of d_allocatedNL that is currently in use - context::CDO<unsigned> d_allocatedNLNext; - /** This method removes all the un-necessary stuff from the maps */ void backtrack(); @@ -108,7 +79,7 @@ private: public: EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {} bool eqNotifyTriggerEquality(TNode equality, bool value) { - Unreachable(); + d_sharedTerms.propagateEquality(equality, value); return true; } @@ -118,14 +89,12 @@ private: } bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) { - if (value) { - d_sharedTerms.mergeSharedTerms(t1, t2); - } - return true; + return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value); } bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { - return true; + d_sharedTerms.conflict(t1, t2, true); + return false; } }; @@ -135,24 +104,83 @@ private: /** Equality engine */ theory::eq::EqualityEngine d_equalityEngine; - /** Attach a new notify list to an equivalence class representative */ - NotifyList* getNewNotifyList(); + /** + * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with + * the theory. Returns false if there is a direct conflict (via rewrite for example). + */ + bool propagateSharedEquality(theory::TheoryId theory, TNode a, TNode b, bool value); + + /** + * Called from the equality engine when a trigger equality is deduced. + */ + bool propagateEquality(TNode equality, bool polarity); + + /** Theory engine */ + TheoryEngine* d_theoryEngine; + + /** Are we in conflict */ + context::CDO<bool> d_inConflict; + + /** Conflicting terms, if any */ + Node d_conflictLHS, d_conflictRHS; + + /** Polarity of the conflict */ + bool d_conflictPolarity; + + /** Called by the equality engine notify to mark the conflict */ + void conflict(TNode lhs, TNode rhs, bool polarity) { + if (!d_inConflict) { + // Only remember it if we're not already in conflict + d_inConflict = true; + d_conflictLHS = lhs; + d_conflictRHS = rhs; + d_conflictPolarity = polarity; + } + } - /** Method called by equalityEngine when a becomes equal to b */ - void mergeSharedTerms(TNode a, TNode b); + /** + * Should be called before any public non-const method in order to + * enqueue the conflict to the theory engine. + */ + void checkForConflict(); public: - SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context); + SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context); ~SharedTermsDatabase() throw(AssertionException); /** + * Asserts the equality to the shared terms database, + */ + void assertEquality(TNode equality, bool polarity, TNode reason); + + /** + * Return whether the equality is alreday known to the engine + */ + bool isKnown(TNode literal) const; + + /** + * Returns an explanation of the propagation that came from the database. + */ + Node explain(TNode literal) const; + + /** + * Add an equality to propagate. + */ + void addEqualityToPropagate(TNode equality); + + /** * Add a shared term to the database. The shared term is a subterm of the atom and * should be associated with the given theory. */ void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories); /** + * Mark that the given theories have been notified of the given shared term. + */ + void markNotified(TNode term, theory::Theory::Set theories); + + /** * Returns true if the atom contains any shared terms, false otherwise. */ bool hasSharedTerms(TNode atom) const; @@ -176,26 +204,32 @@ public: * Get the theories that share the term and have been notified already. */ theory::Theory::Set getNotifiedTheories(TNode term) const; - - // Notify theory about a new equality between shared terms - void assertEq(TNode equality, theory::TheoryId theory); - + /** - * Mark that the given theories have been notified of the given shared term. + * Returns true if the term is currently registered as shared with some theory. */ - void markNotified(TNode term, theory::Theory::Set theories); - bool isShared(TNode term) const { - return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end(); + return term.isConst() || d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end(); } - bool areEqual(TNode a, TNode b); - - bool areDisequal(TNode a, TNode b); + /** + * Returns true if the literal is an (dis-)equality with both sides registered as shared with + * some theory. + */ + bool isSharedEquality(TNode literal) const { + TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; + return atom.getKind() == kind::EQUAL && isShared(atom[0]) && isShared(atom[1]); + } - void processSharedLiteral(TNode literal, TNode reason); + /** + * Returns true if the shared terms a and b are known to be equal. + */ + bool areEqual(TNode a, TNode b) const; - Node explain(TNode literal); + /** + * Retursn true if the shared terms a and b are known to be dis-equal. + */ + bool areDisequal(TNode a, TNode b) const; protected: diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 3e1dc6fe4..ca2460805 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -45,22 +45,22 @@ TheoryEngine::TheoryEngine(context::Context* context, d_context(context), d_userContext(userContext), d_logicInfo(logicInfo), - d_notify(*this), - d_sharedTerms(d_notify, context), + d_sharedTerms(this, context), d_ppCache(), d_possiblePropagations(context), d_hasPropagated(context), d_inConflict(context, false), d_hasShutDown(false), d_incomplete(context, false), - d_sharedLiteralsIn(context), - d_assertedLiteralsOut(context), + d_propagationMap(context), + d_propagationMapTimestamp(context, 0), d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_decisionRequests(context), d_decisionRequestsIndex(context, 0), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_inPreregister(false), + d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), d_unconstrainedSimp(context, logicInfo) @@ -105,6 +105,11 @@ void TheoryEngine::preRegister(TNode preprocessed) { preprocessed = d_preregisterQueue.front(); d_preregisterQueue.pop(); + if (d_logicInfo.isSharingEnabled() && preprocessed.getKind() == kind::EQUAL) { + // When sharing is enabled, we propagate from the shared terms manager also + d_sharedTerms.addEqualityToPropagate(preprocessed); + } + // Pre-register the terms in the atom bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed); if (multipleTheories) { @@ -148,6 +153,50 @@ void TheoryEngine::printAssertions(const char* tag) { } } +void TheoryEngine::dumpAssertions(const char* tag) { + if (Dump.isOn(tag)) { + Dump(tag) << CommentCommand("Starting completeness check"); + for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { + Theory* theory = d_theoryTable[theoryId]; + if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { + Dump(tag) << CommentCommand("Completeness check"); + Dump(tag) << PushCommand(); + + // Dump the shared terms + if (d_logicInfo.isSharingEnabled()) { + Dump(tag) << CommentCommand("Shared terms"); + context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); + for (unsigned i = 0; it != it_end; ++ it, ++i) { + stringstream ss; + ss << (*it); + Dump(tag) << CommentCommand(ss.str()); + } + } + + // Dump the assertions + Dump(tag) << CommentCommand("Assertions"); + context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (; it != it_end; ++ it) { + // Get the assertion + Node assertionNode = (*it).assertion; + // Purify all the terms + + BoolExpr assertionExpr(assertionNode.toExpr()); + if ((*it).isPreregistered) { + Dump(tag) << CommentCommand("Preregistered"); + } else { + Dump(tag) << CommentCommand("Shared assertion"); + } + Dump(tag) << AssertCommand(assertionExpr); + } + Dump(tag) << CheckSatCommand(); + Dump(tag) << PopCommand(); + } + } + } +} + + template<typename T, bool doAssert> class scoped_vector_clear { vector<T>& d_v; @@ -181,8 +230,6 @@ void TheoryEngine::check(Theory::Effort effort) { } \ } - // make sure d_propagatedSharedLiterals is cleared on exit - scoped_vector_clear<SharedLiteral, true> clear_shared_literals(d_propagatedSharedLiterals); // Do the checking try { @@ -194,15 +241,25 @@ void TheoryEngine::check(Theory::Effort effort) { // Mark the lemmas flag (no lemmas added) d_lemmasAdded = false; - while (true) { + Debug("theory") << "TheoryEngine::check(" << effort << "): d_factsAsserted = " << (d_factsAsserted ? "true" : "false") << std::endl; + + // If in full effort, we have a fake new assertion just to jumpstart the checking + if (Theory::fullEffort(effort)) { + d_factsAsserted = true; + } + + // Check until done + while (d_factsAsserted && !d_inConflict && !d_lemmasAdded) { Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl; - Assert(d_propagatedSharedLiterals.empty()); if (Debug.isOn("theory::assertions")) { printAssertions("theory::assertions"); } + // Note that we've discharged all the facts + d_factsAsserted = false; + // Do the checking CVC4_FOR_EACH_THEORY; @@ -217,34 +274,11 @@ void TheoryEngine::check(Theory::Effort effort) { // We are still satisfiable, propagate as much as possible propagate(effort); - // If we have any propagated shared literals, we enqueue them to the theories and re-check - if (d_propagatedSharedLiterals.size() > 0) { - Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl; - outputSharedLiterals(); - continue; - } - - // If we added any lemmas, we're done - if (d_lemmasAdded) { - Debug("theory") << "TheoryEngine::check(" << effort << "): lemmas added, done" << std::endl; - break; - } - - // If in full check and no lemmas added, run the combination - if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled()) { + // We do combination if all has been processed and we are in fullcheck + if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded) { // Do the combination Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << std::endl; combineTheories(); - // If we have any propagated shared literals, we enqueue them to the theories and re-check - if (d_propagatedSharedLiterals.size() > 0) { - Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl; - outputSharedLiterals(); - } else { - // No propagated shared literals, we're either sat, or there are lemmas added - break; - } - } else { - break; } } @@ -253,30 +287,15 @@ void TheoryEngine::check(Theory::Effort effort) { } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::check() => conflict" << endl; } -} - -void TheoryEngine::outputSharedLiterals() { - - scoped_vector_clear<SharedLiteral, false> clear_shared_literals(d_propagatedSharedLiterals); - - // Assert all the shared literals - for (unsigned i = 0; i < d_propagatedSharedLiterals.size(); ++ i) { - const SharedLiteral& eq = d_propagatedSharedLiterals[i]; - // Check if the theory already got this one - if (d_assertedLiteralsOut.find(eq.toAssert) == d_assertedLiteralsOut.end()) { - Debug("sharing") << "TheoryEngine::outputSharedLiterals(): asserting " << eq.toAssert.node << " to " << eq.toAssert.theory << std::endl; - Debug("sharing") << "TheoryEngine::outputSharedLiterals(): orignal " << eq.toExplain << std::endl; - d_assertedLiteralsOut[eq.toAssert] = eq.toExplain; - if (eq.toAssert.theory == theory::THEORY_LAST) { - d_propagatedLiterals.push_back(eq.toAssert.node); - } else { - theoryOf(eq.toAssert.theory)->assertFact(eq.toAssert.node, false); - } + + // If fulleffort, check all theories + if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) { + if (!d_inConflict && !d_lemmasAdded) { + dumpAssertions("theory::fullcheck"); } } } - void TheoryEngine::combineTheories() { Debug("sharing") << "TheoryEngine::combineTheories()" << std::endl; @@ -305,44 +324,38 @@ void TheoryEngine::combineTheories() { Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl; - if (d_sharedTerms.areEqual(carePair.a, carePair.b) || - d_sharedTerms.areDisequal(carePair.a, carePair.b)) { - continue; - } - - if (carePair.a.isConst() && carePair.b.isConst()) { - // TODO: equality engine should auto-detect these as disequal - d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), d_true); - continue; - } + Assert(!d_sharedTerms.areEqual(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); + Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); + // The equality in question Node equality = carePair.a.eqNode(carePair.b); + + // Normalize the equality Node normalizedEquality = Rewriter::rewrite(equality); - bool isTrivial = normalizedEquality.getKind() == kind::CONST_BOOLEAN; - bool value; - if (isTrivial || (d_propEngine->isSatLiteral(normalizedEquality) && d_propEngine->hasValue(normalizedEquality, value))) { - // Missed propagation! - Debug("sharing") << "TheoryEngine::combineTheories(): has a literal or is trivial" << std::endl; - - if (isTrivial) { - value = normalizedEquality.getConst<bool>(); - normalizedEquality = d_true; - } - else { - d_sharedLiteralsIn[normalizedEquality] = theory::THEORY_LAST; - if (!value) normalizedEquality = normalizedEquality.notNode(); - } - if (!value) { - equality = equality.notNode(); + + // Check if the normalized equality already has a value (this also + // covers constants, since they always have values + if (d_propEngine->isSatLiteral(normalizedEquality)) { + bool value; + if (d_propEngine->hasValue(normalizedEquality, value)) { + Assert(equality != normalizedEquality); + Node literal = value ? equality : equality.notNode(); + Node normalizedLiteral = value ? normalizedEquality : normalizedEquality.notNode(); + // We're sending the original literal back, backed by the normalized one + if (markPropagation(literal, normalizedLiteral, /* to */ carePair.theory, /* from */ THEORY_SAT_SOLVER)) { + // We assert it, and we know it's preregistereed if it's the same theory + bool preregistered = Theory::theoryOf(literal) == carePair.theory; + theoryOf(carePair.theory)->assertFact(literal, preregistered); + // Mark that we have more information + d_factsAsserted = true; + continue; + } } - d_sharedTerms.processSharedLiteral(equality, normalizedEquality); - continue; } - - // There is no value, so we need to split on it + + // We need to split on it Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl; lemma(equality.orNode(equality.notNode()), false, false); - } } @@ -363,7 +376,7 @@ void TheoryEngine::propagate(Theory::Effort effort) { for(unsigned i = 0; i < d_possiblePropagations.size(); ++ i) { Node atom = d_possiblePropagations[i]; bool value; - if (d_propEngine->hasValue(atom, value)) continue; + if (!d_propEngine->hasValue(atom, value)) continue; // Doesn't have a value, check it (and the negation) if(d_hasPropagated.find(atom) == d_hasPropagated.end()) { Dump("missed-t-propagations") @@ -662,24 +675,160 @@ Node TheoryEngine::preprocess(TNode assertion) { return d_ppCache[assertion]; } -void TheoryEngine::assertFact(TNode node) -{ - Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; - // Trace("theory::assertions") << "TheoryEngine::assertFact(" << node << "): d_sharedTermsExist = " << (d_sharedTermsExist ? "true" : "false") << std::endl; +bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { + + // What and where we are asserting + NodeTheoryPair toAssert(assertion, toTheoryId, d_propagationMapTimestamp); + // What and where it came from + NodeTheoryPair toExplain(originalAssertion, fromTheoryId, d_propagationMapTimestamp); + + // See if the theory already got this literal + PropagationMap::const_iterator find = d_propagationMap.find(toAssert); + if (find != d_propagationMap.end()) { + // The theory already knows this + Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << std::endl; + return false; + } + + Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp << "] " << assertion << ", " << toTheoryId << " from " << originalAssertion << ", " << fromTheoryId << std::endl; + + // Mark the propagation + d_propagationMap[toAssert] = toExplain; + d_propagationMapTimestamp = d_propagationMapTimestamp + 1; + + return true; +} + + +void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { + + Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << std::endl; + + Assert(toTheoryId != fromTheoryId); + + if (d_inConflict) { + return; + } + + // If sharing is disabled, things are easy + if (!d_logicInfo.isSharingEnabled()) { + if (fromTheoryId == THEORY_SAT_SOLVER) { + // Send to the apropriate theory + theory::Theory* toTheory = theoryOf(toTheoryId); + // We assert it, and we know it's preregistereed + toTheory->assertFact(assertion, true); + // Mark that we have more information + 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; + } + } + return; + } + + // Polarity of the assertion + bool polarity = assertion.getKind() != kind::NOT; + + // Atom of the assertion + TNode atom = polarity ? assertion : assertion[0]; + + // If sending to the shared terms database, it's also simple + if (toTheoryId == THEORY_BUILTIN) { + Assert(atom.getKind() == kind::EQUAL); + if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) { + d_sharedTerms.assertEquality(atom, polarity, assertion); + } + return; + } + + // Things from the SAT solver are already normalized, so they go + // directly to the apropriate theory + if (fromTheoryId == THEORY_SAT_SOLVER) { + // We know that this is normalized, so just send it off to the theory + if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) { + // We assert it, and we know it's preregistereed coming from the SAT solver directly + theoryOf(toTheoryId)->assertFact(assertion, true); + // Mark that we have more information + d_factsAsserted = true; + } + return; + } + + // Propagations to the SAT solver are just enqueued for pickup by + // the SAT solver later + if (toTheoryId == THEORY_SAT_SOLVER) { + if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) { + // Enqueue for propagation to the SAT solver + d_propagatedLiterals.push_back(assertion); + // Check for propositional conflicts + bool value; + if (d_propEngine->hasValue(assertion, value) && !value) { + d_inConflict = true; + } + } + return; + } + + // We are left with internal distribution of shared literals + Assert(atom.getKind() == kind::EQUAL); + Node normalizedAtom = Rewriter::rewriteEquality(toTheoryId, atom); + Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode(); + + // If we normalize to true or false, it's a special case + if (normalizedAtom.isConst()) { + if (polarity == normalizedAtom.getConst<bool>()) { + // Trivially true, just ignore + return; + } else { + // Mark the propagation for explanations + if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) { + // Get the explanation (conflict will figure out where it came from) + conflict(normalizedAssertion, toTheoryId); + } else { + Unreachable(); + } + return; + } + } + + // Try and assert + if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) { + // Check if has been pre-registered with the theory + bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAtom) == toTheoryId; + // Assert away + theoryOf(toTheoryId)->assertFact(normalizedAssertion, preregistered); + d_factsAsserted = true; + } + + return; +} +void TheoryEngine::assertFact(TNode literal) +{ + Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << std::endl; + d_propEngine->checkTime(); + // If we're in conflict, nothing to do + if (d_inConflict) { + return; + } + // Get the atom - bool negated = node.getKind() == kind::NOT; - TNode atom = negated ? node[0] : node; - Theory* theory = theoryOf(atom); + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; if (d_logicInfo.isSharingEnabled()) { - Trace("theory::assertions") << "TheoryEngine::assertFact(" << node << "): hasShared terms = " << (d_sharedTerms.hasSharedTerms(atom) ? "true" : "false") << std::endl; - - // If any shared terms, notify the theories + // If any shared terms, it's time to do sharing work if (d_sharedTerms.hasSharedTerms(atom)) { + // Notify the theories the shared terms SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); for (; it != it_end; ++ it) { @@ -692,48 +841,27 @@ void TheoryEngine::assertFact(TNode node) } d_sharedTerms.markNotified(term, theories); } - if (d_propagatedSharedLiterals.size() > 0) { - Debug("theory") << "TheoryEngine::assertFact: distributing shared literals from new shared terms" << std::endl; - outputSharedLiterals(); - } } - if (atom.getKind() == kind::EQUAL && - d_sharedTerms.isShared(atom[0]) && - d_sharedTerms.isShared(atom[1])) { - Debug("sharing") << "TheoryEngine::assertFact: asserting shared node: " << node << std::endl; - // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain - if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) || - ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) { - Debug("sharing") << "TheoryEngine::assertFact: sharedLiteral already known(" << node << ")" << std::endl; - return; - } - d_sharedLiteralsIn[node] = THEORY_LAST; - d_sharedTerms.processSharedLiteral(node, node); - if (d_propagatedSharedLiterals.size() > 0) { - Debug("theory") << "TheoryEngine::assertFact: distributing shared literals from new assertion" << std::endl; - outputSharedLiterals(); - } - // TODO: have processSharedLiteral propagate disequalities? - if (node.getKind() == kind::EQUAL) { - // Don't have to assert it - this will be taken care of by processSharedLiteral - Assert(d_logicInfo.isTheoryEnabled(theory->getId())); - return; - } - } - // If theory didn't already get this literal, add to the map - NodeTheoryPair ntp(node, theory->getId()); - if (d_assertedLiteralsOut.find(ntp) == d_assertedLiteralsOut.end()) { - d_assertedLiteralsOut[ntp] = Node(); + // If it's an equality, assert it to the shared term manager, even though the terms are not + // yet shared. As the terms become shared later, the shared terms manager will then add them + // to the assert the equality to the interested theories + if (atom.getKind() == kind::EQUAL) { + // Assert it to the the owning theory + assertToTheory(literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER); + // Shared terms manager will assert to interested theories directly, as the terms become shared + assertToTheory(literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER); + } else { + // Not an equality, just assert to the appropriate theory + assertToTheory(literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER); } + } else { + // Assert the fact to the appropriate theory directly + assertToTheory(literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER); } - - // Assert the fact to the appropriate theory and mark it active - theory->assertFact(node, true); - Assert(d_logicInfo.isTheoryEnabled(theory->getId())); } -void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { +bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Debug("theory") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << std::endl; @@ -747,42 +875,26 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { d_hasPropagated.insert(literal); } - bool negated = (literal.getKind() == kind::NOT); - TNode atom = negated ? literal[0] : literal; - bool value; + // Get the atom + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; - if (!d_logicInfo.isSharingEnabled() || atom.getKind() != kind::EQUAL || - !d_sharedTerms.isShared(atom[0]) || !d_sharedTerms.isShared(atom[1])) { - // If not an equality or if an equality between terms that are not both shared, - // it must be a SAT literal so we enqueue it - Assert(d_propEngine->isSatLiteral(literal)); - if (d_propEngine->hasValue(literal, value)) { - // if we are propagting something that already has a sat value we better be the same - Debug("theory") << "literal " << literal << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl; - Assert(value); - } else { - d_propagatedLiterals.push_back(literal); + if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) { + if (d_propEngine->isSatLiteral(literal)) { + // We propagate SAT literals to SAT + assertToTheory(literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); } - } else { - // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain - if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) || - ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) { - Debug("sharing") << "TheoryEngine::propagate: sharedLiteral already known(" << literal << ")" << std::endl; - return; + if (theory != THEORY_BUILTIN) { + // Assert to the shared terms database + assertToTheory(literal, /* to */ THEORY_BUILTIN, /* from */ theory); } - - // Otherwise it is a shared-term (dis-)equality - Node normalizedLiteral = Rewriter::rewrite(literal); - if (d_propEngine->isSatLiteral(normalizedLiteral)) { - // If there is a literal, propagate it to SAT - SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST); - d_propagatedSharedLiterals.push_back(sharedLiteral); - } - // Assert to interested theories - Debug("shared-in") << "TheoryEngine::propagate: asserting shared node: " << literal << std::endl; - d_sharedLiteralsIn[literal] = theory; - d_sharedTerms.processSharedLiteral(literal, literal); + } else { + // Just send off to the SAT solver + Assert(d_propEngine->isSatLiteral(literal)); + assertToTheory(literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); } + + return !d_inConflict; } @@ -809,160 +921,112 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); } -Node TheoryEngine::getExplanation(TNode node) { - Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl; +static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { - TNode atom = node.getKind() == kind::NOT ? node[0] : node; - - Node explanation; - - // The theory that has explaining to do - Theory* theory; - - //This is true if atom is a shared assertion - bool sharedLiteral = false; - - AssertedLiteralsOutMap::iterator find; - // "find" will have a value when sharedAssertion is true - if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) { - find = d_assertedLiteralsOut.find(NodeTheoryPair(node, theory::THEORY_LAST)); - sharedLiteral = (find != d_assertedLiteralsOut.end()); + std::set<TNode> all; + for (unsigned i = 0; i < explanation.size(); ++ i) { + Assert(explanation[i].theory == THEORY_SAT_SOLVER); + all.insert(explanation[i].node); } - // Get the explanation - if(sharedLiteral) { - explanation = explain(ExplainTask((*find).second, SHARED_LITERAL_OUT)); - } else { - theory = theoryOf(atom); - explanation = theory->explain(node); - - // Explain any shared equalities that might be in the explanation - if (d_logicInfo.isSharingEnabled()) { - explanation = explain(ExplainTask(explanation, THEORY_EXPLANATION, theory->getId())); - } + if (all.size() == 0) { + // Normalize to true + return NodeManager::currentNM()->mkConst<bool>(true); } - Assert(!explanation.isNull()); - if(Dump.isOn("t-explanations")) { - Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid") - << QueryCommand(explanation.impNode(node).toExpr()); + if (all.size() == 1) { + // All the same, or just one + return explanation[0].node; } - Assert(properExplanation(node, explanation)); - Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << std::endl; + NodeBuilder<> conjunction(kind::AND); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } - return explanation; + return conjunction; } -Node TheoryEngine::explain(ExplainTask toExplain) -{ - Debug("theory") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl; - - std::set<TNode> satAssertions; - std::deque<ExplainTask> explainQueue; - // TODO: benchmark whether this helps - std::hash_set<ExplainTask, ExplainTaskHashFunction> explained; -#ifdef CVC4_ASSERTIONS - bool value; -#endif - - // No need to explain "true" - explained.insert(ExplainTask(d_true, SHARED_DATABASE_EXPLANATION)); - - while (true) { - - Debug("theory-explain") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl; - - if (explained.find(toExplain) == explained.end()) { +Node TheoryEngine::getExplanation(TNode node) { + Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl; - explained.insert(toExplain); + bool polarity = node.getKind() != kind::NOT; + TNode atom = polarity ? node : node[0]; - if (toExplain.node.getKind() == kind::AND) { - for (unsigned i = 0, i_end = toExplain.node.getNumChildren(); i != i_end; ++ i) { - explainQueue.push_back(ExplainTask(toExplain.node[i], toExplain.kind, toExplain.theory)); - } - } - else { - - switch (toExplain.kind) { - - // toExplain.node contains a shared literal sent out from theory engine (before being rewritten) - case SHARED_LITERAL_OUT: { - // Shortcut - see if this came directly from a theory - SharedLiteralsInMap::iterator it = d_sharedLiteralsIn.find(toExplain.node); - if (it != d_sharedLiteralsIn.end()) { - TheoryId id = (*it).second; - if (id == theory::THEORY_LAST) { - Assert(d_propEngine->isSatLiteral(toExplain.node)); - Assert(d_propEngine->hasValue(toExplain.node, value) && value); - satAssertions.insert(toExplain.node); - break; - } - explainQueue.push_back(ExplainTask(theoryOf((*it).second)->explain(toExplain.node), THEORY_EXPLANATION, (*it).second)); - } - // Otherwise, get explanation from shared terms database - else { - explainQueue.push_back(ExplainTask(d_sharedTerms.explain(toExplain.node), SHARED_DATABASE_EXPLANATION)); - } - break; - } + // If we're not in shared mode, explanations are simple + if (!d_logicInfo.isSharingEnabled()) { + Node explanation = theoryOf(atom)->explain(node); + Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << std::endl; + return explanation; + } - // toExplain.node contains explanation from theory, toExplain.theory contains theory that produced explanation - case THEORY_EXPLANATION: { - AssertedLiteralsOutMap::iterator find = d_assertedLiteralsOut.find(NodeTheoryPair(toExplain.node, toExplain.theory)); - if (find == d_assertedLiteralsOut.end() || (*find).second.isNull()) { - Assert(d_propEngine->isSatLiteral(toExplain.node)); - Assert(d_propEngine->hasValue(toExplain.node, value) && value); - satAssertions.insert(toExplain.node); - } - else { - explainQueue.push_back(ExplainTask((*find).second, SHARED_LITERAL_OUT)); - } - break; - } + // Initial thing to explain + NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp); + Assert(d_propagationMap.find(toExplain) != d_propagationMap.end()); + // Create the workplace for explanations + std::vector<NodeTheoryPair> explanationVector; + explanationVector.push_back(d_propagationMap[toExplain]); + // Process the explanation + getExplanation(explanationVector); + Node explanation = mkExplanation(explanationVector); + + Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << std::endl; + + return explanation; +} - // toExplain.node contains an explanation from the shared terms database - // Each literal in the explanation should be in the d_sharedLiteralsIn map - case SHARED_DATABASE_EXPLANATION: { - Assert(d_sharedLiteralsIn.find(toExplain.node) != d_sharedLiteralsIn.end()); - TheoryId id = d_sharedLiteralsIn[toExplain.node]; - if (id == theory::THEORY_LAST) { - Assert(d_propEngine->isSatLiteral(toExplain.node)); - Assert(d_propEngine->hasValue(toExplain.node, value) && value); - satAssertions.insert(toExplain.node); - } - else { - explainQueue.push_back(ExplainTask(theoryOf(id)->explain(toExplain.node), THEORY_EXPLANATION, id)); - } - break; - } - default: - Unreachable(); - } - } - } +theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable) { + if(Dump.isOn("t-lemmas")) { + Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") + << QueryCommand(node.toExpr()); + } - if (explainQueue.empty()) break; + // Share with other portfolio threads + if(Options::current()->lemmaOutputChannel != NULL) { + Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr()); + } - toExplain = explainQueue.front(); - explainQueue.pop_front(); + // Remove the ITEs + std::vector<Node> additionalLemmas; + IteSkolemMap iteSkolemMap; + additionalLemmas.push_back(node); + RemoveITE::run(additionalLemmas, iteSkolemMap); + additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); + + // assert to prop engine + d_propEngine->assertLemma(additionalLemmas[0], negated, removable); + for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { + additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); + d_propEngine->assertLemma(additionalLemmas[i], false, removable); } - Assert(satAssertions.size() > 0); - if (satAssertions.size() == 1) { - return *(satAssertions.begin()); + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. + if(negated) { + // Can't we just get rid of passing around this 'negated' stuff? + // Is it that hard for the propEngine to figure that out itself? + // (I like the use of triple negation <evil laugh>.) --K + additionalLemmas[0] = additionalLemmas[0].notNode(); + negated = false; } + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. - // Now build the explanation - NodeBuilder<> conjunction(kind::AND); - std::set<TNode>::const_iterator it = satAssertions.begin(); - std::set<TNode>::const_iterator it_end = satAssertions.end(); - while (it != it_end) { - conjunction << *it; - ++ it; + // assert to decision engine + if(!removable) { + d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap); } - return conjunction; + + // Mark that we added some lemmas + d_lemmasAdded = true; + + // Lemma analysis isn't online yet; this lemma may only live for this + // user level. + return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel()); } void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { @@ -974,12 +1038,16 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << CheckSatCommand(conflict.toExpr()); } - + + // In the multiple-theories case, we need to reconstruct the conflict if (d_logicInfo.isSharingEnabled()) { - // In the multiple-theories case, we need to reconstruct the conflict - Node fullConflict = explain(ExplainTask(conflict, THEORY_EXPLANATION, theoryId)); - Assert(properConflict(fullConflict)); - Debug("theory") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): " << fullConflict << std::endl; + // Create the workplace for explanations + std::vector<NodeTheoryPair> explanationVector; + explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp)); + // Process the explanation + getExplanation(explanationVector); + Node fullConflict = mkExplanation(explanationVector); + Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << std::endl; lemma(fullConflict, true, false); } else { // When only one theory, the conflict should need no processing @@ -988,24 +1056,6 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } } - -//Conflict from shared terms database -void TheoryEngine::sharedConflict(TNode conflict) { - // Mark that we are in conflict - d_inConflict = true; - - if(Dump.isOn("t-conflicts")) { - Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") - << CheckSatCommand(conflict.toExpr()); - } - - Node fullConflict = explain(ExplainTask(d_sharedTerms.explain(conflict), SHARED_DATABASE_EXPLANATION)); - Assert(properConflict(fullConflict)); - Debug("theory") << "TheoryEngine::sharedConflict(" << conflict << "): " << fullConflict << std::endl; - lemma(fullConflict, true, false); -} - - Node TheoryEngine::ppSimpITE(TNode assertion) { Node result = d_iteSimplifier.simpITE(assertion); @@ -1014,6 +1064,77 @@ Node TheoryEngine::ppSimpITE(TNode assertion) return result; } +void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector) +{ + Assert(explanationVector.size() > 0); + + unsigned i = 0; // Index of the current literal we are processing + unsigned j = 0; // Index of the last literal we are keeping + + while (i < explanationVector.size()) { + + // Get the current literal to explain + NodeTheoryPair toExplain = explanationVector[i]; + + Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << std::endl; + + // If a treu constant or a negation of a false constant we can ignore it + if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) { + ++ i; + continue; + } + if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst<bool>()) { + ++ i; + continue; + } + + // If from the SAT solver, keep it + if (toExplain.theory == THEORY_SAT_SOLVER) { + explanationVector[j++] = explanationVector[i++]; + continue; + } + + // If an and, expand it + if (toExplain.node.getKind() == kind::AND) { + Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain.node << " got from " << toExplain.theory << std::endl; + for (unsigned k = 0; k < toExplain.node.getNumChildren(); ++ k) { + NodeTheoryPair newExplain(toExplain.node[k], toExplain.theory, toExplain.timestamp); + explanationVector.push_back(newExplain); + } + ++ i; + continue; + } + + // See if it was sent to the theory by another theory + PropagationMap::const_iterator find = d_propagationMap.find(toExplain); + if (find != d_propagationMap.end()) { + // There is some propagation, check if its a timely one + if ((*find).second.timestamp < toExplain.timestamp) { + explanationVector.push_back((*find).second); + ++ i; + continue; + } + } + + // It was produced by the theory, so ask for an explanation + Node explanation; + if (toExplain.theory == THEORY_BUILTIN) { + explanation = d_sharedTerms.explain(toExplain.node); + } 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; + // Mark the explanation + NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); + explanationVector.push_back(newExplain); + ++ i; + } + + // Keep only the relevant literals + explanationVector.resize(j); +} + void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index bc9f4c889..ed95149b3 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -46,16 +46,19 @@ namespace CVC4 { -// In terms of abstraction, this is below (and provides services to) -// PropEngine. - +/** + * A pair of a theory and a node. This is used to mark the flow of + * propagations between theories. + */ struct NodeTheoryPair { Node node; theory::TheoryId theory; - NodeTheoryPair(TNode node, theory::TheoryId theory) - : node(node), theory(theory) {} + size_t timestamp; + NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp) + : node(node), theory(theory), timestamp(timestamp) {} NodeTheoryPair() : theory(theory::THEORY_LAST) {} + // Comparison doesn't take into account the timestamp bool operator == (const NodeTheoryPair& pair) const { return node == pair.node && theory == pair.theory; } @@ -63,6 +66,7 @@ struct NodeTheoryPair { struct NodeTheoryPairHashFunction { NodeHashFunction hashFunction; + // Hash doesn't take into account the timestamp size_t operator()(const NodeTheoryPair& pair) const { return hashFunction(pair.node)*0x9e3779b9 + pair.theory; } @@ -75,6 +79,9 @@ struct NodeTheoryPairHashFunction { * CVC4. */ class TheoryEngine { + + /** Shared terms database can use the internals notify the theories */ + friend class SharedTermsDatabase; /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; @@ -103,21 +110,6 @@ class TheoryEngine { */ const LogicInfo& d_logicInfo; - // NotifyClass: template helper class for Shared Terms Database - class NotifyClass :public SharedTermsDatabase::SharedTermsNotifyClass { - TheoryEngine& d_theoryEngine; - public: - NotifyClass(TheoryEngine& engine): d_theoryEngine(engine) {} - ~NotifyClass() {} - - void notify(TNode literal, TNode original, theory::TheoryId theory) { - d_theoryEngine.propagateSharedLiteral(literal, original, theory); - } - }; - - // Instance of NotifyClass - NotifyClass d_notify; - /** * The database of shared terms. */ @@ -221,11 +213,11 @@ class TheoryEngine { d_engine->conflict(conflictNode, d_theory); } - void propagate(TNode literal) throw(AssertionException) { + bool propagate(TNode literal) throw(AssertionException) { Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; ++ d_statistics.propagations; d_engine->d_outputChannelUsed = true; - d_engine->propagate(literal, d_theory); + return d_engine->propagate(literal, d_theory); } void propagateAsDecision(TNode literal) throw(AssertionException) { @@ -263,28 +255,11 @@ class TheoryEngine { context::CDO<bool> d_inConflict; /** - * Explain the equality literals and push all the explaining literals - * into the builder. All the non-equality literals are pushed to the - * builder. - */ - void explainEqualities(theory::TheoryId theoryId, TNode literals, NodeBuilder<>& builder); - - /** - * Same as above, but just for single equalities. - */ - void explainEquality(theory::TheoryId theoryId, TNode eqLiteral, NodeBuilder<>& builder); - - /** * Called by the theories to notify of a conflict. */ void conflict(TNode conflict, theory::TheoryId theoryId); /** - * Called by shared terms database to notify of a conflict. - */ - void sharedConflict(TNode conflict); - - /** * Debugging flag to ensure that shutdown() is called before the * destructor. */ @@ -310,63 +285,16 @@ class TheoryEngine { d_propEngine->spendResource(); } - struct SharedLiteral { - /** - * The node/theory pair for the assertion. THEORY_LAST indicates this is a SAT - * literal and should be sent to the SAT solver - */ - NodeTheoryPair toAssert; - /** This is the node that we will use to explain it */ - Node toExplain; - - SharedLiteral(TNode assertion, TNode original, theory::TheoryId receivingTheory) - : toAssert(assertion, receivingTheory), - toExplain(original) - { } - }; - - /** - * Map from nodes to theories. - */ - typedef context::CDHashMap<Node, theory::TheoryId, NodeHashFunction> SharedLiteralsInMap; - /** - * All shared literals asserted to theory engine. - * Maps from literal to the theory that sent the literal (THEORY_LAST means sent from SAT). + * Mapping of propagations from recievers to senders. */ - SharedLiteralsInMap d_sharedLiteralsIn; - - /** - * Map from literals asserted by theory engine to literal that can explain - */ - typedef context::CDHashMap<NodeTheoryPair, Node, NodeTheoryPairHashFunction> AssertedLiteralsOutMap; - - /** - * All literals asserted to theories from theory engine. - * Maps from literal/theory pair to literal that can explain this assertion. - */ - AssertedLiteralsOutMap d_assertedLiteralsOut; - - /** - * Shared literals queud up to be asserted to the individual theories. - */ - std::vector<SharedLiteral> d_propagatedSharedLiterals; - - void propagateSharedLiteral(TNode literal, TNode original, theory::TheoryId theory) - { - if (literal.getKind() == kind::CONST_BOOLEAN) { - Assert(!literal.getConst<bool>()); - sharedConflict(original); - } - else { - d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory)); - } - } + typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> PropagationMap; + PropagationMap d_propagationMap; /** - * Assert the shared literals that are queued up to the theories. + * Timestamp of propagations */ - void outputSharedLiterals(); + context::CDO<size_t> d_propagationMapTimestamp; /** * Literals that are propagated by the theory. Note that these are TNodes. @@ -395,8 +323,9 @@ class TheoryEngine { /** * Called by the output channel to propagate literals and facts + * @return false if immediate conflict */ - void propagate(TNode literal, theory::TheoryId theory); + bool propagate(TNode literal, theory::TheoryId theory); /** * Internal method to call the propagation routines and collect the @@ -427,55 +356,8 @@ class TheoryEngine { /** * Adds a new lemma, returning its status. */ - theory::LemmaStatus lemma(TNode node, bool negated, bool removable) { - if(Dump.isOn("t-lemmas")) { - Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") - << QueryCommand(node.toExpr()); - } - - // Share with other portfolio threads - if(Options::current()->lemmaOutputChannel != NULL) { - Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr()); - } - - // Remove the ITEs - std::vector<Node> additionalLemmas; - IteSkolemMap iteSkolemMap; - additionalLemmas.push_back(node); - RemoveITE::run(additionalLemmas, iteSkolemMap); - additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); - - // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable); - for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { - additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); - d_propEngine->assertLemma(additionalLemmas[i], false, removable); - } - - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. - if(negated) { - // Can't we just get rid of passing around this 'negated' stuff? - // Is it that hard for the propEngine to figure that out itself? - // (I like the use of triple negation <evil laugh>.) --K - additionalLemmas[0] = additionalLemmas[0].notNode(); - negated = false; - } - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. - - // assert to decision engine - if(!removable) - d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap); - - // Mark that we added some lemmas - d_lemmasAdded = true; - - // Lemma analysis isn't online yet; this lemma may only live for this - // user level. - return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel()); - } - + theory::LemmaStatus lemma(TNode node, bool negated, bool removable); + /** Time spent in theory combination */ TimerStat d_combineTheoriesTime; @@ -535,6 +417,45 @@ private: */ bool d_inPreregister; + /** + * Did the theories get any new facts since the last time we called + * check() + */ + context::CDO<bool> d_factsAsserted; + + /** + * Assert the formula to the given theory. + * @param assertion the assertion to send (not necesserily normalized) + * @param original the assertion as it was sent in from the propagating theory + * @param toTheoryId the theory to assert to + * @param fromTheoryId the theory that sent it + */ + void assertToTheory(TNode assertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); + + /** + * Marks a theory propagation from a theory to a theory where a + * theory could be the THEORY_SAT_SOLVER for literals coming from + * or being propagated to the SAT solver. If the receiving theory + * already recieved the literal, the method returns false, otherwise + * it returns true. + * + * @param assertion the normalized assertion being sent + * @param originalAssertion the actual assertion that was sent + * @param toTheoryId the theory that is on the receiving end + * @param fromTheoryId the theory that sent the assertino + * @return true if a new assertion, false if theory already got it + */ + bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); + + /** + * Computes the explanation by travarsing the propagation graph and + * asking relevant theories to explain the propagations. Initially + * the explanation vector should contain only the element (node, theory) + * where the node is the one to be explained, and the theory is the + * theory that sent the literal. + */ + void getExplanation(std::vector<NodeTheoryPair>& explanationVector); + public: /** @@ -657,40 +578,14 @@ public: bool properPropagation(TNode lit) const; bool properExplanation(TNode node, TNode expl) const; - enum ExplainTaskKind { - // Literal sent out from the theory engine - SHARED_LITERAL_OUT, - // Explanation produced by a theory - THEORY_EXPLANATION, - // Explanation produced by the shared terms database - SHARED_DATABASE_EXPLANATION - }; - - struct ExplainTask { - Node node; - ExplainTaskKind kind; - theory::TheoryId theory; - ExplainTask(Node n, ExplainTaskKind k, theory::TheoryId tid = theory::THEORY_LAST) : - node(n), kind(k), theory(tid) {} - bool operator == (const ExplainTask& other) const { - return node == other.node && kind == other.kind && theory == other.theory; - } - }; - - struct ExplainTaskHashFunction { - size_t operator () (const ExplainTask& task) const { - size_t hash = 0; - hash = 0x9e3779b9 + NodeHashFunction().operator()(task.node); - hash ^= 0x9e3779b9 + task.kind + (hash << 6) + (hash >> 2); - hash ^= 0x9e3779b9 + task.theory + (hash << 6) + (hash >> 2); - return hash; - } - }; - + /** + * Returns an explanation of the node propagated to the SAT solver. + */ Node getExplanation(TNode node); - Node explain(ExplainTask toExplain); - + /** + * Returns the value of the given node. + */ Node getValue(TNode node); /** @@ -732,6 +627,9 @@ private: /** Prints the assertions to the debug stream */ void printAssertions(const char* tag); + /** Dump the assertions to the dump */ + void dumpAssertions(const char* tag); + /** For preprocessing pass simplifying ITEs */ ITESimplifier d_iteSimplifier; @@ -739,6 +637,7 @@ private: UnconstrainedSimplifier d_unconstrainedSimp; public: + Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector<Node>& assertions); diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index aaf47425b..bf1370090 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -78,9 +78,10 @@ public: push(CONFLICT, n); } - void propagate(TNode n) + bool propagate(TNode n) throw(AssertionException) { push(PROPAGATE, n); + return true; } void propagateAsDecision(TNode n) 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<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(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<USE_LIST_FUNCTIONS>(funId, d_useListNodes); - d_equalityNodes[t2ClassId].usedIn<USE_LIST_FUNCTIONS>(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<USE_LIST_FUNCTIONS>(); + 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<true>(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<USE_LIST_FUNCTIONS>(d_useListNodes); + getEqualityNode(app.b).removeTopFromUseList(d_useListNodes); // Remove a from use-list - getEqualityNode(app.a).removeTopFromUseList<USE_LIST_FUNCTIONS>(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<TriggerId> 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<EqualityNodeId> 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<TNode>& output) { // Get the current node EqualityNode& currentNode = getEqualityNode(currentId); // Go through the use-list - UseListNodeId currentUseId = currentNode.getUseList<USE_LIST_FUNCTIONS>(); + 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 @@ -345,6 +345,13 @@ private: std::vector<bool> 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. */ std::vector<bool> d_isBoolean; 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<UseListType type> 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<UseListType type, typename memory_class> + template<typename memory_class> 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<UseListType type, typename memory_class> + template<typename memory_class> 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<TNode> 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<TNode>& 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 { |