diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 211 |
1 files changed, 138 insertions, 73 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6c8341345..63fc1ae65 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -110,6 +110,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_propagationMapTimestamp(context, 0), d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), + d_atomRequests(context), d_iteRemover(iteRemover), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_true(), @@ -411,43 +412,13 @@ void TheoryEngine::combineTheories() { Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst()); Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst()); - //AJR-temp Assert(!d_sharedTerms.areEqual(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); - //AJR-temp 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 < carePair.b ? - carePair.a.eqNode(carePair.b) : - carePair.b.eqNode(carePair.a); - - // Normalize the equality - Node normalizedEquality = Rewriter::rewrite(equality); - - // 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; - } else { - Message() << "mark propagation fail: " << literal << " " << normalizedLiteral << " " << carePair.theory << std::endl; - Unreachable(); - } - } - } + // The equality in question (order for no repetition) + Node equality = carePair.a.eqNode(carePair.b); // We need to split on it Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl; - lemma(equality.orNode(equality.notNode()), false, false); + lemma(equality.orNode(equality.notNode()), false, false, carePair.theory); } } @@ -893,7 +864,7 @@ bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, the } -void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { +void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << std::endl; @@ -915,6 +886,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, // If sharing is disabled, things are easy if (!d_logicInfo.isSharingEnabled()) { + Assert(assertion == originalAssertion); if (fromTheoryId == THEORY_SAT_SOLVER) { // Send to the apropriate theory theory::Theory* toTheory = theoryOf(toTheoryId); @@ -948,7 +920,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, // If sending to the shared terms database, it's also simple if (toTheoryId == THEORY_BUILTIN) { Assert(atom.getKind() == kind::EQUAL, "atom should be an EQUALity, not `%s'", atom.toString().c_str()); - if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) { + if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { d_sharedTerms.assertEquality(atom, polarity, assertion); } return; @@ -958,9 +930,9 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, // 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)) { + if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { // We assert it, and we know it's preregistereed coming from the SAT solver directly - theoryOf(toTheoryId)->assertFact(assertion, true); + theoryOf(toTheoryId)->assertFact(assertion, assertion == originalAssertion); // Mark that we have more information d_factsAsserted = true; } @@ -970,7 +942,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, // 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)) { + if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { // Enqueue for propagation to the SAT solver d_propagatedLiterals.push_back(assertion); // Check for propositional conflicts @@ -982,18 +954,16 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, return; } - // See if it rewrites to true or false directly + Assert(atom.getKind() == kind::EQUAL); + + // Normalize Node normalizedLiteral = Rewriter::rewrite(assertion); + + // See if it rewrites false directly -> conflict if (normalizedLiteral.isConst()) { - if (normalizedLiteral.getConst<bool>()) { - // trivially true, but theories need to share even trivially true facts - // unless of course it is the theory that normalized it - if (Theory::theoryOf(atom) == toTheoryId) { - return; - } - } else { + if (!normalizedLiteral.getConst<bool>()) { // Mark the propagation for explanations - if (markPropagation(normalizedLiteral, assertion, toTheoryId, fromTheoryId)) { + if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) { // Get the explanation (conflict will figure out where it came from) conflict(normalizedLiteral, toTheoryId); } else { @@ -1003,25 +973,12 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, } } - // Normalize to lhs < rhs if not a sat literal - Assert(atom.getKind() == kind::EQUAL); - Assert(atom[0] != atom[1]); - - Node normalizedAtom = atom; - if (!d_propEngine->isSatLiteral(normalizedAtom)) { - Node reverse = atom[1].eqNode(atom[0]); - if (d_propEngine->isSatLiteral(reverse) || atom[0] > atom[1]) { - normalizedAtom = reverse; - } - } - Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode(); - // Try and assert (note that we assert the non-normalized one) - if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) { + if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { // Check if has been pre-registered with the theory - bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAtom) == toTheoryId; + bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId; // Assert away - theoryOf(toTheoryId)->assertFact(normalizedAssertion, preregistered); + theoryOf(toTheoryId)->assertFact(assertion, preregistered); d_factsAsserted = true; } @@ -1067,16 +1024,27 @@ void TheoryEngine::assertFact(TNode literal) // 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); + assertToTheory(literal, 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); + assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER); + + // Now, let's check for any atom triggers from lemmas + AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom); + while (!it.done()) { + const AtomRequests::Request& request = it.get(); + Node toAssert = polarity ? (Node) request.atom : request.atom.notNode(); + Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal << "): sending requested " << toAssert << std::endl; + assertToTheory(toAssert, literal, request.toTheory, THEORY_SAT_SOLVER); + it.next(); + } + } else { // Not an equality, just assert to the appropriate theory - assertToTheory(literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER); + assertToTheory(literal, 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); + assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER); } } @@ -1101,16 +1069,16 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { 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); + assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); } if (theory != THEORY_BUILTIN) { // Assert to the shared terms database - assertToTheory(literal, /* to */ THEORY_BUILTIN, /* from */ theory); + assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory); } } else { // Just send off to the SAT solver Assert(d_propEngine->isSatLiteral(literal)); - assertToTheory(literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); + assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); } return !d_inConflict; @@ -1193,7 +1161,104 @@ Node TheoryEngine::getExplanation(TNode node) { return explanation; } -theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable) { +struct AtomsCollect { + + std::vector<TNode> d_atoms; + std::hash_set<TNode, TNodeHashFunction> d_visited; + +public: + + typedef void return_type; + + bool alreadyVisited(TNode current, TNode parent) { + // Check if already visited + d_visited.find(current) != d_visited.end(); + // Don't visit non-boolean + if (!current.getType().isBoolean()) return true; + // New node + return false; + } + + void visit(TNode current, TNode parent) { + if (Theory::theoryOf(current) != theory::THEORY_BOOL) { + d_atoms.push_back(current); + } + d_visited.insert(current); + } + + void start(TNode node) {} + void done(TNode node) {} + + std::vector<TNode> getAtoms() const { + return d_atoms; + } +}; + +void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId atomsTo) { + for (unsigned i = 0; i < atoms.size(); ++ i) { + + // Non-equality atoms are either owned by theory or they don't make sense + if (atoms[i].getKind() != kind::EQUAL) { + continue; + } + + // The equality + Node eq = atoms[i]; + // Simple normalization to not repeat stuff + if (eq[0] > eq[1]) { + eq = eq[1].eqNode(eq[0]); + } + + // Rewrite the equality + Node eqNormalized = Rewriter::rewrite(atoms[i]); + // If the equality is a boolean constant, we send immediately + if (eqNormalized.isConst()) { + if (eqNormalized.getConst<bool>()) { + assertToTheory(eq, eqNormalized, /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER); + } else { + assertToTheory(eq.notNode(), eqNormalized.notNode(), /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER); + } + continue; + } + + // If the normalization did the just flips, keep the flip + if (eqNormalized[0] == eq[1]) { + eq = eqNormalized; + } + + // Check if the equality is already known by the sat solver + if (d_propEngine->isSatLiteral(eqNormalized)) { + bool value; + if (d_propEngine->hasValue(eqNormalized, value)) { + if (value) { + assertToTheory(eq, eqNormalized, atomsTo, theory::THEORY_SAT_SOLVER); + continue; + } else { + assertToTheory(eq.notNode(), eqNormalized.notNode(), atomsTo, theory::THEORY_SAT_SOLVER); + continue; + } + } + } + + // If the theory is asking about a different form, or the form is ok but if will go to a different theory + // then we must figure it out + if (eqNormalized != eq || Theory::theoryOf(eq) != atomsTo) { + // If you get eqNormalized, send atoms[i] to atomsTo + d_atomRequests.add(eqNormalized, eq, atomsTo); + } + } +} + +theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, theory::TheoryId atomsTo) { + + // Do we need to check atoms + if (atomsTo != theory::THEORY_LAST) { + Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << std::endl; + AtomsCollect collectAtoms; + NodeVisitor<AtomsCollect>::run(collectAtoms, node); + ensureLemmaAtoms(collectAtoms.getAtoms(), atomsTo); + } + if(Dump.isOn("t-lemmas")) { Node n = node; if (negated) { @@ -1269,11 +1334,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Node fullConflict = mkExplanation(explanationVector); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << std::endl; Assert(properConflict(fullConflict)); - lemma(fullConflict, true, true); + lemma(fullConflict, true, true, THEORY_LAST); } else { // When only one theory, the conflict should need no processing Assert(properConflict(conflict)); - lemma(conflict, true, true); + lemma(conflict, true, true, THEORY_LAST); } } |