diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 200 |
1 files changed, 168 insertions, 32 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2cd3f4d72..c03b09be2 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -42,12 +42,13 @@ TheoryEngine::TheoryEngine(context::Context* context, : d_propEngine(NULL), d_context(context), d_userContext(userContext), - d_activeTheories(0), + d_activeTheories(context, 0), d_sharedTerms(context), d_atomPreprocessingCache(), d_possiblePropagations(), d_hasPropagated(context), d_inConflict(context, false), + d_sharedTermsExist(context, false), d_hasShutDown(false), d_incomplete(context, false), d_sharedAssertions(context), @@ -91,6 +92,8 @@ void TheoryEngine::preRegister(TNode preprocessed) { if (multipleTheories) { // Collect the shared terms if there are multipe theories NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed); + // Mark the multiple theories flag + d_sharedTermsExist = true; } } @@ -124,6 +127,8 @@ void TheoryEngine::check(Theory::Effort effort) { while (true) { + Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl; + // Do the checking CVC4_FOR_EACH_THEORY; @@ -133,26 +138,32 @@ void TheoryEngine::check(Theory::Effort effort) { << CheckSatCommand() << endl; } + Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << std::endl; + // We are still satisfiable, propagate as much as possible propagate(effort); // If we have any propagated equalities, we enqueue them to the theories and re-check if (d_propagatedEqualities.size() > 0) { + Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared equalities" << std::endl; assertSharedEqualities(); 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)) { + if (Theory::fullEffort(effort) && d_sharedTermsExist) { // Do the combination + Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << std::endl; combineTheories(); // If we have any propagated equalities, we enqueue them to the theories and re-check if (d_propagatedEqualities.size() > 0) { + Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared equalities" << std::endl; assertSharedEqualities(); } else { // No propagated equalities, we're either sat, or there are lemmas added @@ -166,6 +177,8 @@ void TheoryEngine::check(Theory::Effort effort) { // Clear any leftover propagated equalities d_propagatedEqualities.clear(); + Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << std::endl; + } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::check() => conflict" << endl; } @@ -176,9 +189,11 @@ void TheoryEngine::assertSharedEqualities() { for (unsigned i = 0; i < d_propagatedEqualities.size(); ++ i) { const SharedEquality& eq = d_propagatedEqualities[i]; // Check if the theory already got this one - if (d_sharedAssertions.find(eq.toAssert) != d_sharedAssertions.end()) { + // TODO: the real shared (non-sat) equalities + if (d_sharedAssertions.find(eq.toAssert) == d_sharedAssertions.end()) { + Debug("sharing") << "TheoryEngine::assertSharedEqualities(): asserting " << eq.toAssert.node << " to " << eq.toAssert.theory << " from " << eq.toExplain.theory << std::endl; d_sharedAssertions[eq.toAssert] = eq.toExplain; - theoryOf(eq.toAssert.theory)->assertFact(eq.toAssert.node); + theoryOf(eq.toAssert.theory)->assertFact(eq.toAssert.node, false); } } // Clear the equalities @@ -188,6 +203,8 @@ void TheoryEngine::assertSharedEqualities() { void TheoryEngine::combineTheories() { + Debug("sharing") << "TheoryEngine::combineTheories()" << std::endl; + CareGraph careGraph; #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT @@ -205,20 +222,31 @@ void TheoryEngine::combineTheories() { for (unsigned i = 0; i < careGraph.size(); ++ i) { const CarePair& carePair = careGraph[i]; + Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl; + Node equality = carePair.a.eqNode(carePair.b); Node normalizedEquality = Rewriter::rewrite(equality); // If the node has a literal, it has been asserted so we should just check it bool value; if (d_propEngine->isSatLiteral(normalizedEquality) && d_propEngine->hasValue(normalizedEquality, value)) { + Debug("sharing") << "TheoryEngine::combineTheories(): has a literal " << std::endl; + // Normalize the equality to the theory that requested it - Node toAssert = Rewriter::rewriteTo(carePair.theory, equality); + Node toAssert = Rewriter::rewriteEquality(carePair.theory, equality); + if (value) { - d_propagatedEqualities.push_back(SharedEquality(toAssert, normalizedEquality, theory::THEORY_LAST, carePair.theory)); + SharedEquality sharedEquality(toAssert, normalizedEquality, theory::THEORY_LAST, carePair.theory); + Assert(d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()); + d_propagatedEqualities.push_back(sharedEquality); } else { - d_propagatedEqualities.push_back(SharedEquality(toAssert.notNode(), normalizedEquality.notNode(), theory::THEORY_LAST, carePair.theory)); + SharedEquality sharedEquality(toAssert.notNode(), normalizedEquality.notNode(), theory::THEORY_LAST, carePair.theory); + Assert(d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()); + d_propagatedEqualities.push_back(sharedEquality); } } else { + Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl; + // There is no value, so we need to split on it lemma(equality.orNode(equality.notNode()), false, false); } @@ -251,16 +279,6 @@ void TheoryEngine::propagate(Theory::Effort effort) { } } -Node TheoryEngine::getExplanation(TNode node, theory::Theory* theory) { - Node explanation = theory->explain(node); - if(Dump.isOn("t-explanations")) { - Dump("t-explanations") - << CommentCommand(string("theory explanation from ") + theory->identify() + ": expect valid") << endl - << QueryCommand(explanation.impNode(node).toExpr()) << endl; - } - return explanation; -} - bool TheoryEngine::properConflict(TNode conflict) const { bool value; if (conflict.getKind() == kind::AND) { @@ -497,7 +515,7 @@ void TheoryEngine::assertFact(TNode node) TNode atom = node.getKind() == kind::NOT ? node[0] : node; // Assert the fact to the apropriate theory - theoryOf(atom)->assertFact(node); + theoryOf(atom)->assertFact(node, true); // If any shared terms, notify the theories if (d_sharedTerms.hasSharedTerms(atom)) { @@ -512,13 +530,14 @@ void TheoryEngine::assertFact(TNode node) } } d_sharedTerms.markNotified(term, theories); + markActive(theories); } } } void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { - Debug("theory") << "EngineOutputChannel::propagate(" << literal << ")" << std::endl; + Debug("theory") << "EngineOutputChannel::propagate(" << literal << ", " << theory << ")" << std::endl; d_propEngine->checkTime(); @@ -530,7 +549,9 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { d_hasPropagated.insert(literal); } - if (literal.getKind() != kind::EQUAL) { + TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; + + if (!d_sharedTermsExist || atom.getKind() != kind::EQUAL) { // If not an equality it must be a SAT literal so we enlist it, and it can only // be propagated by the theory that owns it, as it is the only one that got // a preregister call with it. @@ -541,24 +562,139 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Node normalizedEquality = Rewriter::rewrite(literal); if (d_propEngine->isSatLiteral(normalizedEquality)) { // If there is a literal, just enqueue it, same as above - d_propagatedLiterals.push_back(literal); - } else { - // Otherwise, we assert it to all interested theories + d_propagatedLiterals.push_back(normalizedEquality); + } + // Otherwise, we assert it to all interested theories + Theory::Set lhsNotified = d_sharedTerms.getNotifiedTheories(atom[0]); + Theory::Set rhsNotified = d_sharedTerms.getNotifiedTheories(atom[1]); + // Now notify the theories + if (Theory::setIntersection(lhsNotified, rhsNotified) != 0) { bool negated = literal.getKind() == kind::NOT; - Node equality = negated ? literal[0] : literal; - Theory::Set lhsNotified = d_sharedTerms.getNotifiedTheories(equality[0]); - Theory::Set rhsNotified = d_sharedTerms.getNotifiedTheories(equality[1]); - // Now notify the theories - for (TheoryId current = theory::THEORY_FIRST; current != theory::THEORY_LAST; ++ current) { - if (Theory::setContains(current, lhsNotified) && Theory::setContains(current, rhsNotified)) { + for (TheoryId currentTheory = theory::THEORY_FIRST; currentTheory != theory::THEORY_LAST; ++ currentTheory) { + if (currentTheory == theory) { + // Don't reassert to the same theory + continue; + } + // Assert if theory is interested in both terms + if (Theory::setContains(currentTheory, lhsNotified) && Theory::setContains(currentTheory, rhsNotified)) { // Normalize the equality - Node equalityNormalized = Rewriter::rewriteTo(current, equality); + Node equality = Rewriter::rewriteEquality(currentTheory, atom); // The assertion - Node assertion = negated ? equalityNormalized.notNode() : equalityNormalized; + Node assertion = negated ? equality.notNode() : equality; // Remember it to assert later - d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, current)); + d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, currentTheory)); } } } } } + +theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { + Assert(a.getType() == b.getType()); + return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); +} + +Node TheoryEngine::getExplanation(TNode node) +{ + Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl; + + TNode atom = node.getKind() == kind::NOT ? node[0] : node; + + Node explanation; + + // The theory that has explaining to do + Theory* theory = theoryOf(atom); + if (d_sharedTermsExist && atom.getKind() == kind::EQUAL) { + SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(node, theory::THEORY_LAST)); + if (find == d_sharedAssertions.end()) { + theory = theoryOf(atom); + } + } + + // Get the explanation + explanation = theory->explain(node); + + // Explain any shared equalities that might be in the explanation + if (d_sharedTermsExist) { + NodeBuilder<> nb(kind::AND); + explainEqualities(theory->getId(), explanation, nb); + explanation = nb; + } + + Assert(!explanation.isNull()); + if(Dump.isOn("t-explanations")) { + Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid") << std::endl + << QueryCommand(explanation.impNode(node).toExpr()) << std::endl; + } + Assert(properExplanation(node, explanation)); + + return explanation; +} + +void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { + + // Mark that we are in conflict + d_inConflict = true; + + if(Dump.isOn("t-conflicts")) { + Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << std::endl + << CheckSatCommand(conflict.toExpr()) << std::endl; + } + + if (d_sharedTermsExist) { + // In the multiple-theories case, we need to reconstruct the conflict + NodeBuilder<> nb(kind::AND); + explainEqualities(theoryId, conflict, nb); + Node fullConflict = nb; + Assert(properConflict(fullConflict)); + Debug("theory") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): " << fullConflict << std::endl; + lemma(fullConflict, true, false); + } else { + // When only one theory, the conflict should need no processing + Assert(properConflict(conflict)); + lemma(conflict, true, false); + } +} + +void TheoryEngine::explainEqualities(TheoryId theoryId, TNode literals, NodeBuilder<>& builder) { + Debug("theory") << "TheoryEngine::explainEqualities(" << theoryId << ", " << literals << ")" << std::endl; + if (literals.getKind() == kind::AND) { + for (unsigned i = 0, i_end = literals.getNumChildren(); i != i_end; ++ i) { + TNode literal = literals[i]; + TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; + if (atom.getKind() == kind::EQUAL) { + explainEquality(theoryId, literal, builder); + } else { + builder << literal; + } + } + } else { + TNode atom = literals.getKind() == kind::NOT ? literals[0] : literals; + if (atom.getKind() == kind::EQUAL) { + explainEquality(theoryId, literals, builder); + } else { + builder << literals; + } + } +} + +void TheoryEngine::explainEquality(TheoryId theoryId, TNode eqLiteral, NodeBuilder<>& builder) { + Assert(eqLiteral.getKind() == kind::EQUAL || (eqLiteral.getKind() == kind::NOT && eqLiteral[0].getKind() == kind::EQUAL)); + + SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(eqLiteral, theoryId)); + if (find == d_sharedAssertions.end()) { + // Not a shared assertion, just add it since it must be SAT literal + builder << eqLiteral; + } else { + TheoryId explainingTheory = (*find).second.theory; + if (explainingTheory == theory::THEORY_LAST) { + // If the theory is from the SAT solver, just take the normalized one + builder << (*find).second.node; + } else { + // Explain it using the theory that propagated it + Node explanation = theoryOf(explainingTheory)->explain((*find).second.node); + explainEqualities(explainingTheory, explanation, builder); + } + } +} + |