summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/Makefile.am4
-rw-r--r--src/theory/arrays/theory_arrays.cpp18
-rw-r--r--src/theory/atom_requests.cpp62
-rw-r--r--src/theory/atom_requests.h107
-rw-r--r--src/theory/bv/bitblaster.cpp5
-rw-r--r--src/theory/output_channel.h5
-rw-r--r--src/theory/shared_terms_database.cpp4
-rw-r--r--src/theory/theory_engine.cpp211
-rw-r--r--src/theory/theory_engine.h32
9 files changed, 362 insertions, 86 deletions
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<TNode, TNode> > 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<TNode>::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<Request, RequestHashFunction> 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<Element> d_requests;
+
+ typedef context::CDHashMap<Node, element_index, NodeHashFunction> 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<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);
}
}
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<TNode>& atoms, theory::TheoryId theory);
RemoveITE& d_iteRemover;
@@ -535,13 +556,18 @@ private:
context::CDO<bool> 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)
* @param original the assertion as it was sent in from the propagating theory
* @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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback