diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 757 |
1 files changed, 439 insertions, 318 deletions
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) { |