diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 276 |
1 files changed, 222 insertions, 54 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 040582c9f..d5ac8ddbb 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -37,40 +37,40 @@ using namespace std; using namespace CVC4; using namespace CVC4::theory; -TheoryEngine::TheoryEngine(context::Context* ctxt) : - d_propEngine(NULL), +TheoryEngine::TheoryEngine(context::Context* ctxt) +: d_propEngine(NULL), d_context(ctxt), d_activeTheories(0), + d_sharedTerms(ctxt), d_atomPreprocessingCache(), d_possiblePropagations(), d_hasPropagated(ctxt), - d_theoryOut(this, ctxt), - d_sharedTermManager(NULL), + d_inConflict(ctxt, false), d_hasShutDown(false), d_incomplete(ctxt, false), + d_sharedAssertions(ctxt), d_logic(""), - d_statistics(), - d_preRegistrationVisitor(*this, ctxt) { - - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + d_propagatedLiterals(ctxt), + d_propagatedLiteralsIndex(ctxt, 0), + d_preRegistrationVisitor(this, ctxt), + d_sharedTermsVisitor(d_sharedTerms) +{ + for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { d_theoryTable[theoryId] = NULL; + d_theoryOut[theoryId] = NULL; } - Rewriter::init(); - - d_sharedTermManager = new SharedTermManager(this, ctxt); } TheoryEngine::~TheoryEngine() { Assert(d_hasShutDown); - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { if(d_theoryTable[theoryId] != NULL) { delete d_theoryTable[theoryId]; + delete d_theoryOut[theoryId]; } } - - delete d_sharedTermManager; } void TheoryEngine::setLogic(std::string logic) { @@ -79,62 +79,156 @@ void TheoryEngine::setLogic(std::string logic) { d_logic = logic; } -struct preregister_stack_element { - TNode node; - bool children_added; - preregister_stack_element(TNode node) - : node(node), children_added(false) {} -};/* struct preprocess_stack_element */ - void TheoryEngine::preRegister(TNode preprocessed) { if(Dump.isOn("missed-t-propagations")) { d_possiblePropagations.push_back(preprocessed); } - NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed); + // Pre-register the terms in the atom + bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed); + if (multipleTheories) { + // Collect the shared terms if there are multipe theories + NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed); + } } /** * Check all (currently-active) theories for conflicts. * @param effort the effort level to use */ -void TheoryEngine::check(theory::Theory::Effort effort) { - - d_theoryOut.d_propagatedLiterals.clear(); +void TheoryEngine::check(Theory::Effort effort) { #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasCheck && isActive(THEORY)) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \ - if (d_theoryOut.d_inConflict) { \ - return; \ - } \ - } + if (theory::TheoryTraits<THEORY>::hasCheck && isActive(THEORY)) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->check(effort); \ + if (d_inConflict) { \ + break; \ + } \ + } // Do the checking try { - CVC4_FOR_EACH_THEORY; - if(Dump.isOn("missed-t-conflicts")) { - Dump("missed-t-conflicts") - << CommentCommand("Completeness check for T-conflicts; expect sat") << endl - << CheckSatCommand() << endl; + // Clear any leftover propagated equalities + d_propagatedEqualities.clear(); + + // Mark the lemmas flag (no lemmas added) + d_lemmasAdded = false; + + while (true) { + + // Do the checking + CVC4_FOR_EACH_THEORY; + + if(Dump.isOn("missed-t-conflicts")) { + Dump("missed-t-conflicts") + << CommentCommand("Completeness check for T-conflicts; expect sat") << endl + << CheckSatCommand() << 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) { + assertSharedEqualities(); + continue; + } + + // If we added any lemmas, we're done + if (d_lemmasAdded) { + break; + } + + // If in full check and no lemmas added, run the combination + if (Theory::fullEffort(effort)) { + // Do the combination + combineTheories(); + // If we have any propagated equalities, we enqueue them to the theories and re-check + if (d_propagatedEqualities.size() > 0) { + assertSharedEqualities(); + } else { + // No propagated equalities, we're either sat, or there are lemmas added + break; + } + } else { + break; + } } + + // Clear any leftover propagated equalities + d_propagatedEqualities.clear(); + } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::check() => conflict" << endl; } } -void TheoryEngine::propagate() { +void TheoryEngine::assertSharedEqualities() { + // Assert all the shared equalities + 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()) { + d_sharedAssertions[eq.toAssert] = eq.toExplain; + theoryOf(eq.toAssert.theory)->assertFact(eq.toAssert.node); + } + } + // Clear the equalities + d_propagatedEqualities.clear(); +} + + +void TheoryEngine::combineTheories() { + + CareGraph careGraph; +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::isParametric && isActive(THEORY)) { \ + CareGraph theoryGraph; \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->computeCareGraph(theoryGraph); \ + careGraph.insert(careGraph.end(), theoryGraph.begin(), theoryGraph.end()); \ + } + + CVC4_FOR_EACH_THEORY; + + // Now add splitters for the ones we are interested in + for (unsigned i = 0; i < careGraph.size(); ++ i) { + const CarePair& carePair = careGraph[i]; + + 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)) { + // Normalize the equality to the theory that requested it + Node toAssert = Rewriter::rewriteTo(carePair.theory, equality); + if (value) { + d_propagatedEqualities.push_back(SharedEquality(toAssert, normalizedEquality, theory::THEORY_LAST, carePair.theory)); + } else { + d_propagatedEqualities.push_back(SharedEquality(toAssert.notNode(), normalizedEquality.notNode(), theory::THEORY_LAST, carePair.theory)); + } + } else { + // There is no value, so we need to split on it + lemma(equality.orNode(equality.notNode()), false, false); + } + } +} + +void TheoryEngine::propagate(Theory::Effort effort) { // Definition of the statement that is to be run by every theory #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasPropagate && isActive(THEORY)) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->propagate(effort); \ } // Propagate for each theory using the statement above @@ -154,21 +248,26 @@ void TheoryEngine::propagate() { } Node TheoryEngine::getExplanation(TNode node, theory::Theory* theory) { - theory->explain(node); + Node explanation = theory->explain(node); if(Dump.isOn("t-explanations")) { Dump("t-explanations") - << CommentCommand(string("theory explanation from ") + - theory->identify() + ": expect valid") << endl - << QueryCommand(d_theoryOut.d_explanationNode.get().impNode(node).toExpr()) - << endl; + << CommentCommand(string("theory explanation from ") + theory->identify() + ": expect valid") << endl + << QueryCommand(explanation.impNode(node).toExpr()) << endl; } - Assert(properExplanation(node, d_theoryOut.d_explanationNode.get())); - return d_theoryOut.d_explanationNode; + return explanation; } bool TheoryEngine::properConflict(TNode conflict) const { - Assert(!conflict.isNull()); -#warning fixme + bool value; + if (conflict.getKind() == kind::AND) { + for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) { + if (!getPropEngine()->hasValue(conflict[i], value)) return false; + if (!value) return false; + } + } else { + if (!getPropEngine()->hasValue(conflict, value)) return false; + return value; + } return true; } @@ -206,8 +305,6 @@ bool TheoryEngine::presolve() { // at doing something with the input formula, even if it wouldn't // otherwise be active. - d_theoryOut.d_propagatedLiterals.clear(); - try { // Definition of the statement that is to be run by every theory #ifdef CVC4_FOR_EACH_THEORY_STATEMENT @@ -215,8 +312,8 @@ bool TheoryEngine::presolve() { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasPresolve) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \ - if(d_theoryOut.d_inConflict) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->presolve(); \ + if(d_inConflict) { \ return true; \ } \ } @@ -238,7 +335,7 @@ void TheoryEngine::notifyRestart() { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasNotifyRestart && isActive(THEORY)) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->notifyRestart(); \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->notifyRestart(); \ } // notify each theory using the statement above @@ -258,7 +355,7 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasStaticLearning) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->staticLearning(in, learned); \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->staticLearning(in, learned); \ } // static learning for each theory using the statement above @@ -274,7 +371,7 @@ void TheoryEngine::shutdown() { // Shutdown all the theories for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { if(d_theoryTable[theoryId]) { - d_theoryTable[theoryId]->shutdown(); + theoryOf(static_cast<TheoryId>(theoryId))->shutdown(); } } @@ -367,3 +464,74 @@ Node TheoryEngine::preprocess(TNode assertion) { return d_atomPreprocessingCache[assertion]; } +void TheoryEngine::assertFact(TNode node) +{ + Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + + // Get the atom + TNode atom = node.getKind() == kind::NOT ? node[0] : node; + + // Assert the fact to the apropriate theory + theoryOf(atom)->assertFact(node); + + // If any shared terms, notify the theories + if (d_sharedTerms.hasSharedTerms(atom)) { + SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); + SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); + for (; it != it_end; ++ it) { + TNode term = *it; + Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term); + for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) { + if (Theory::setContains(theory, theories)) { + theoryOf(theory)->addSharedTermInternal(term); + } + } + d_sharedTerms.markNotified(term, theories); + } + } +} + +void TheoryEngine::propagate(TNode literal, TheoryId theory) { + + Debug("theory") << "EngineOutputChannel::propagate(" << literal << ")" << std::endl; + + if(Dump.isOn("t-propagations")) { + Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") << std::endl + << QueryCommand(literal.toExpr()) << std::endl; + } + if(Dump.isOn("missed-t-propagations")) { + d_hasPropagated.insert(literal); + } + + if (literal.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. + Assert(d_propEngine->isSatLiteral(literal)); + d_propagatedLiterals.push_back(literal); + } else { + // Otherwise it might be a shared-term (dis-)equality + 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 + 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)) { + // Normalize the equality + Node equalityNormalized = Rewriter::rewriteTo(current, equality); + // The assertion + Node assertion = negated ? equalityNormalized.notNode() : equalityNormalized; + // Remember it to assert later + d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, current)); + } + } + } + } +} |