From fb05d8411fdf905550d0bfdef56f4a4c3ed6a8ef Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Fri, 26 Apr 2013 12:55:13 -0400 Subject: [PATCH] * splitLemma to request atoms * normalizing in bv before bitblasting --- src/theory/Makefile.am | 4 +- src/theory/arrays/theory_arrays.cpp | 18 ++- src/theory/atom_requests.cpp | 62 ++++++++ src/theory/atom_requests.h | 107 ++++++++++++++ src/theory/bv/bitblaster.cpp | 5 +- src/theory/output_channel.h | 5 +- src/theory/shared_terms_database.cpp | 4 +- src/theory/theory_engine.cpp | 211 ++++++++++++++++++--------- src/theory/theory_engine.h | 32 +++- 9 files changed, 362 insertions(+), 86 deletions(-) create mode 100644 src/theory/atom_requests.cpp create mode 100644 src/theory/atom_requests.h diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index bd7b881e1..70962e6ed 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -42,7 +42,9 @@ libtheory_la_SOURCES = \ model.h \ model.cpp \ rep_set.h \ - rep_set.cpp + rep_set.cpp \ + atom_requests.h \ + atom_requests.cpp nodist_libtheory_la_SOURCES = \ rewriter_tables.h \ diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 801893107..9f7419b87 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -588,7 +588,10 @@ void TheoryArrays::computeCareGraph() } } } - if (options::arraysModelBased()) return; + if (options::arraysModelBased()) { + checkModel(EFFORT_COMBINATION); + return; + } if (d_sharedTerms) { vector< pair > currentPairs; @@ -1009,7 +1012,7 @@ void TheoryArrays::checkModel(Effort e) Assert(d_skolemAssertions.empty()); Assert(d_lemmas.empty()); - if (fullEffort(e)) { + if (combination(e)) { // Add constraints for shared terms context::CDList::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(), shared_it2; Node modelVal, modelVal2, d; @@ -1294,7 +1297,7 @@ void TheoryArrays::checkModel(Effort e) d_skolemIndex = 0; while (!d_lemmas.empty()) { Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl; - d_out->lemma(d_lemmas.back()); + d_out->splitLemma(d_lemmas.back()); #ifdef CVC4_ASSERTIONS Assert(d_lemmasSaved.find(d_lemmas.back()) == d_lemmasSaved.end()); d_lemmasSaved.insert(d_lemmas.back()); @@ -1633,9 +1636,14 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, return true; } } - getSatContext()->push(); Node d = node.eqNode(val); - d_decisions.push_back(invert ? d.notNode() : d); + Node r = Rewriter::rewrite(d); + if (r.isConst()) { + d_equalityEngine.assertEquality(d, r == d_true, d_true); + return ((r == d_true) == (!invert)); + } + getSatContext()->push(); + d_decisions.push_back(invert ? d.negate() : d); d_equalityEngine.assertEquality(d, !invert, d_decisions.back()); Debug("arrays-model-based") << "Asserting " << d_decisions.back() << " with explanation " << d_decisions.back() << endl; ++d_numSetModelValSplits; diff --git a/src/theory/atom_requests.cpp b/src/theory/atom_requests.cpp new file mode 100644 index 000000000..3d111f9f8 --- /dev/null +++ b/src/theory/atom_requests.cpp @@ -0,0 +1,62 @@ +#include "theory/atom_requests.h" + +using namespace CVC4; + +AtomRequests::AtomRequests(context::Context* context) +: d_allRequests(context) +, d_requests(context) +, d_triggerToRequestMap(context) +{} + +AtomRequests::element_index AtomRequests::getList(TNode trigger) const { + trigger_to_list_map::const_iterator find = d_triggerToRequestMap.find(trigger); + if (find == d_triggerToRequestMap.end()) { + return null_index; + } else { + return (*find).second; + } +} + +bool AtomRequests::isTrigger(TNode atom) const { + return getList(atom) != null_index; +} + +AtomRequests::atom_iterator AtomRequests::getAtomIterator(TNode trigger) const { + return atom_iterator(*this, getList(trigger)); +} + +void AtomRequests::add(TNode triggerAtom, TNode atomToSend, theory::TheoryId toTheory) { + + Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << ")" << std::endl; + + Request request(atomToSend, toTheory); + + if (d_allRequests.find(request) != d_allRequests.end()) { + // Have it already + Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << "): already there" << std::endl; + return; + } + Debug("theory::atoms") << "AtomRequests::add(" << triggerAtom << ", " << atomToSend << ", " << toTheory << "): adding" << std::endl; + + /// Mark the new request + d_allRequests.insert(request); + + // Index of the new request in the list of trigger + element_index index = d_requests.size(); + element_index previous = getList(triggerAtom); + d_requests.push_back(Element(request, previous)); + d_triggerToRequestMap[triggerAtom] = index; +} + +bool AtomRequests::atom_iterator::done() const { + return index == null_index; +} + +void AtomRequests::atom_iterator::next() { + index = requests.d_requests[index].previous; +} + +const AtomRequests::Request& AtomRequests::atom_iterator::get() const { + return requests.d_requests[index].request; +} + diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h new file mode 100644 index 000000000..99878125a --- /dev/null +++ b/src/theory/atom_requests.h @@ -0,0 +1,107 @@ +#pragma once + +#include "expr/node.h" +#include "theory/theory.h" +#include "context/cdlist.h" +#include "context/cdhashset.h" +#include "context/cdhashmap.h" + +namespace CVC4 { + +class AtomRequests { + +public: + + /** Which atom and where to send it */ + struct Request { + /** Atom */ + Node atom; + /** Where to send it */ + theory::TheoryId toTheory; + + Request(TNode atom, theory::TheoryId toTheory) + : atom(atom), toTheory(toTheory) {} + Request() + : toTheory(theory::THEORY_LAST) + {} + + bool operator == (const Request& other) const { + return atom == other.atom && toTheory == other.toTheory; + } + + size_t hash() const { + return atom.getId(); + } + + }; + + AtomRequests(context::Context* context); + + /** Mark the atom to be sent to a theory, when the trigger atom gets assigned */ + void add(TNode triggerAtom, TNode atomToSend, theory::TheoryId toTheory); + + /** Returns true if the node is a trigger and has a list of atoms to send */ + bool isTrigger(TNode atom) const; + + /** Indices in lists */ + typedef size_t element_index; + + class atom_iterator { + const AtomRequests& requests; + element_index index; + friend class AtomRequests; + atom_iterator(const AtomRequests& requests, element_index start) + : requests(requests), index(start) {} + public: + /** Is this iterator done */ + bool done() const; + /** Go to the next element */ + void next(); + /** Get the actual request */ + const Request& get() const; + }; + + atom_iterator getAtomIterator(TNode trigger) const; + +private: + + struct RequestHashFunction { + size_t operator () (const Request& r) const { + return r.hash(); + } + }; + + /** Set of all requests so we don't add twice */ + context::CDHashSet d_allRequests; + + static const element_index null_index = -1; + + struct Element { + /** Current request */ + Request request; + /** Previous request */ + element_index previous; + + Element(const Request& request, element_index previous) + : request(request), previous(previous) + {} + }; + + /** We index the requests in this vector, it's a list */ + context::CDList d_requests; + + typedef context::CDHashMap trigger_to_list_map; + + /** Map from triggers, to the list of elements they trigger */ + trigger_to_list_map d_triggerToRequestMap; + + /** Get the list index of the trigger */ + element_index getList(TNode trigger) const; + +}; + +} + + + + diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 8579012ab..7960b0320 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -95,7 +95,10 @@ void Bitblaster::bbAtom(TNode node) { Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numAtoms; // the bitblasted definition of the atom - Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this)); + Node normalized = Rewriter::rewrite(node); + Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ? + Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) : + normalized; // asserting that the atom is true iff the definition holds Node atom_definition = mkNode(kind::IFF, node, atom_bb); diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index af3065404..524c9606d 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -127,9 +127,12 @@ public: */ LemmaStatus split(TNode n) throw(TypeCheckingExceptionPrivate, AssertionException) { - return lemma(n.orNode(n.notNode())); + return splitLemma(n.orNode(n.notNode())); } + virtual LemmaStatus splitLemma(TNode n, bool removable = false) + throw(TypeCheckingExceptionPrivate, AssertionException) = 0; + /** * If a decision is made on n, it must be in the phase specified. * Note that this is enforced *globally*, i.e., it is completely diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 58b8cf697..3a767b5c3 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -131,9 +131,9 @@ bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNod // Propagate away Node equality = a.eqNode(b); if (value) { - d_theoryEngine->assertToTheory(equality, theory, THEORY_BUILTIN); + d_theoryEngine->assertToTheory(equality, equality, theory, THEORY_BUILTIN); } else { - d_theoryEngine->assertToTheory(equality.notNode(), theory, THEORY_BUILTIN); + d_theoryEngine->assertToTheory(equality.notNode(), equality.notNode(), theory, THEORY_BUILTIN); } // As you were 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()) { - // 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()) { // 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 d_atoms; + std::hash_set 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 getAtoms() const { + return d_atoms; + } +}; + +void TheoryEngine::ensureLemmaAtoms(const std::vector& 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()) { + 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::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); } } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index c21819ea1..3aa3a1ec5 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -46,6 +46,7 @@ #include "theory/unconstrained_simplifier.h" #include "theory/uf/equality_engine.h" #include "theory/bv/bv_to_bool.h" +#include "theory/atom_requests.h" namespace CVC4 { @@ -75,6 +76,9 @@ struct NodeTheoryPairHashFunction { } };/* struct NodeTheoryPairHashFunction */ + + + namespace theory { class TheoryModel; class TheoryEngineModelBuilder; @@ -293,7 +297,14 @@ class TheoryEngine { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, false, removable); + return d_engine->lemma(lemma, false, removable, theory::THEORY_LAST); + } + + theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { + Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; + ++ d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + return d_engine->lemma(lemma, false, removable, d_theory); } void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) { @@ -430,10 +441,20 @@ class TheoryEngine { */ bool d_outputChannelUsed; + /** Atom requests from lemmas */ + AtomRequests d_atomRequests; + /** * Adds a new lemma, returning its status. + * @param node the lemma + * @param negated should the lemma be asserted negated + * @param removable can the lemma be remove (restrictions apply) + * @param needAtoms if not THEORY_LAST, then */ - theory::LemmaStatus lemma(TNode node, bool negated, bool removable); + theory::LemmaStatus lemma(TNode node, bool negated, bool removable, theory::TheoryId atomsTo); + + /** Enusre that the given atoms are send to the given theory */ + void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId theory); RemoveITE& d_iteRemover; @@ -534,6 +555,11 @@ private: */ context::CDO d_factsAsserted; + /** + * Map from equality atoms to theories that would like to be notified about them. + */ + + /** * Assert the formula to the given theory. * @param assertion the assertion to send (not necesserily normalized) @@ -541,7 +567,7 @@ private: * @param toTheoryId the theory to assert to * @param fromTheoryId the theory that sent it */ - void assertToTheory(TNode assertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); + void assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); /** * Marks a theory propagation from a theory to a theory where a -- 2.30.2