summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arrays/theory_arrays.cpp104
-rw-r--r--src/theory/arrays/theory_arrays.h12
-rw-r--r--src/theory/bv/bv_subtheory_eq.cpp6
-rw-r--r--src/theory/bv/theory_bv.cpp57
-rw-r--r--src/theory/bv/theory_bv_utils.h23
-rw-r--r--src/theory/output_channel.h3
-rw-r--r--src/theory/shared_terms_database.cpp268
-rw-r--r--src/theory/shared_terms_database.h158
-rw-r--r--src/theory/theory_engine.cpp757
-rw-r--r--src/theory/theory_engine.h245
-rw-r--r--src/theory/theory_test_utils.h3
-rw-r--r--src/theory/uf/equality_engine.cpp170
-rw-r--r--src/theory/uf/equality_engine.h7
-rw-r--r--src/theory/uf/equality_engine_types.h37
-rw-r--r--src/theory/uf/theory_uf.cpp76
-rw-r--r--src/theory/uf/theory_uf.h19
16 files changed, 945 insertions, 1000 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 65e409012..4ba4aeba5 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -319,33 +319,12 @@ bool TheoryArrays::propagate(TNode literal)
return false;
}
- // See if the literal has been asserted already
- Node normalized = Rewriter::rewrite(literal);
- bool satValue = false;
- bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
-
- // If asserted, we're done or in conflict
- if (isAsserted) {
- if (!satValue) {
- Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
- std::vector<TNode> assumptions;
- Node negatedLiteral;
- negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
- assumptions.push_back(negatedLiteral);
- explain(literal, assumptions);
- d_conflictNode = mkAnd(assumptions);
- d_conflict = true;
- return false;
- }
- // Propagate even if already known in SAT - could be a new equation between shared terms
- // (terms that weren't shared when the literal was asserted!)
+ // Propagate away
+ bool ok = d_out->propagate(literal);
+ if (!ok) {
+ d_conflict = true;
}
-
- // Nothing, just enqueue it for propagation and mark it as asserted already
- Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
- d_literalsToPropagate.push_back(literal);
-
- return true;
+ return ok;
}/* TheoryArrays::propagate(TNode) */
@@ -479,29 +458,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
void TheoryArrays::propagate(Effort e)
{
- Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl;
- if (!d_conflict) {
- for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
- TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
- Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl;
- bool satValue;
- Node normalized = Rewriter::rewrite(literal);
- if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
- d_out->propagate(literal);
- } else {
- Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl;
- Node negatedLiteral;
- std::vector<TNode> assumptions;
- negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
- assumptions.push_back(negatedLiteral);
- explain(literal, assumptions);
- d_conflictNode = mkAnd(assumptions);
- d_conflict = true;
- break;
- }
- }
- }
-
+ // direct propagation now
}
@@ -634,6 +591,7 @@ void TheoryArrays::computeCareGraph()
break;
case EQUALITY_FALSE_IN_MODEL:
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl;
+ continue;
break;
default:
break;
@@ -700,11 +658,21 @@ void TheoryArrays::check(Effort e) {
Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
- // If the assertion doesn't have a literal, it's a shared equality
- Assert(assertion.isPreregistered ||
- ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) ||
- (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL &&
- d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1]))));
+ bool polarity = fact.getKind() != kind::NOT;
+ TNode atom = polarity ? fact : fact[0];
+
+ if (!assertion.isPreregistered) {
+ if (atom.getKind() == kind::EQUAL) {
+ if (!d_equalityEngine.hasTerm(atom[0])) {
+ Assert(atom[0].isConst());
+ d_equalityEngine.addTerm(atom[0]);
+ }
+ if (!d_equalityEngine.hasTerm(atom[1])) {
+ Assert(atom[1].isConst());
+ d_equalityEngine.addTerm(atom[1]);
+ }
+ }
+ }
// Do the work
switch (fact.getKind()) {
@@ -758,19 +726,10 @@ void TheoryArrays::check(Effort e) {
}
// If in conflict, output the conflict
- if (d_conflict) {
- Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl;
- d_out->conflict(d_conflictNode);
- }
- else {
- // Otherwise we propagate
- propagate(e);
-
- if(!d_eagerLemmas && fullEffort(e) && !d_conflict) {
- // generate the lemmas on the worklist
- Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
- dischargeLemmas();
- }
+ if(!d_eagerLemmas && fullEffort(e) && !d_conflict) {
+ // generate the lemmas on the worklist
+ Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
+ dischargeLemmas();
}
Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
@@ -1138,6 +1097,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
TNode b = lem.second;
TNode i = lem.third;
TNode j = lem.fourth;
+
Assert(a.getType().isArray() && b.getType().isArray());
if (d_equalityEngine.areEqual(a,b) ||
d_equalityEngine.areEqual(i,j)) {
@@ -1345,6 +1305,16 @@ void TheoryArrays::dischargeLemmas()
}
}
+void TheoryArrays::conflict(TNode a, TNode b) {
+ if (Theory::theoryOf(a) == theory::THEORY_BOOL) {
+ d_conflictNode = explain(a.iffNode(b));
+ } else {
+ d_conflictNode = explain(a.eqNode(b));
+ }
+ d_out->conflict(d_conflictNode);
+ d_conflict = true;
+}
+
}/* CVC4::theory::arrays namespace */
}/* CVC4::theory namespace */
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index d17caba45..6592e86cf 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -261,11 +261,8 @@ class TheoryArrays : public Theory {
bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
- if (Theory::theoryOf(t1) == THEORY_BOOL) {
- return d_arrays.propagate(t1.iffNode(t2));
- } else {
- return d_arrays.propagate(t1.eqNode(t2));
- }
+ d_arrays.conflict(t1, t2);
+ return false;
}
};
@@ -275,9 +272,12 @@ class TheoryArrays : public Theory {
/** Equaltity engine */
eq::EqualityEngine d_equalityEngine;
- // Are we in conflict?
+ /** Are we in conflict? */
context::CDO<bool> d_conflict;
+ /** Conflict when merging constants */
+ void conflict(TNode a, TNode b);
+
/** The conflict node */
Node d_conflictNode;
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index 807d90137..98678a9b4 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -134,7 +134,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool v
}
bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
- BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+ BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
if (value) {
return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY);
} else {
@@ -143,7 +143,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool
}
bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
- Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl;
+ Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
if (value) {
return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
} else {
@@ -152,7 +152,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNod
}
bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
- Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
+ Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
if (Theory::theoryOf(t1) == THEORY_BOOL) {
return d_bv->storePropagation(t1.iffNode(t2), TheoryBV::SUB_EQUALITY);
}
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 251650bf2..30493737a 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -141,58 +141,9 @@ void TheoryBV::propagate(Effort e) {
}
// go through stored propagations
- for (; d_literalsToPropagateIndex < d_literalsToPropagate.size();
- d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1)
- {
+ for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
- Node normalized = Rewriter::rewrite(literal);
-
- TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
- bool isSharedLiteral = (atom.getKind() == kind::EQUAL &&
- (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() &&
- d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end()));
-
- // Check if this is a SAT literal
- if (d_valuation.isSatLiteral(normalized)) {
- bool satValue = false;
- if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
- // check if we already propagated the negation
- Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal);
- if (d_alreadyPropagatedSet.find(negLiteral) != d_alreadyPropagatedSet.end()) {
- Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n";
- // we are in conflict
- std::vector<TNode> assumptions;
- explain(literal, assumptions);
- explain(negLiteral, assumptions);
- setConflict(mkAnd(assumptions));
- return;
- }
- // If it's not a shared literal and hasn't already been set to true, we propagate the normalized version
- // shared literals are handled below
- if (!isSharedLiteral && !satValue) {
- BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << normalized << std::endl;
- d_out->propagate(normalized);
- d_alreadyPropagatedSet.insert(normalized);
- return;
- }
- } else {
- //
- Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
- Node negatedLiteral;
- std::vector<TNode> assumptions;
- negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
- assumptions.push_back(negatedLiteral);
- explain(literal, assumptions);
- setConflict(mkAnd(assumptions));
- return;
- }
- }
- // Either it was not a SAT literal or it was but it is also shared - in that case we have to propagate the original literal (not the normalized one)
- if (isSharedLiteral) {
- BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl;
- d_out->propagate(literal);
- d_alreadyPropagatedSet.insert(literal);
- }
+ d_out->propagate(literal);
}
}
@@ -269,16 +220,18 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
// Ask the appropriate subtheory for the explanation
if (propagatedBy(literal, SUB_EQUALITY)) {
+ BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
d_equalitySolver.explain(literal, assumptions);
} else {
Assert(propagatedBy(literal, SUB_BITBLAST));
+ BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
d_bitblastSolver.explain(literal, assumptions);
}
}
Node TheoryBV::explain(TNode node) {
- BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
+ BVDebug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
std::vector<TNode> assumptions;
// Ask for the explanation
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 3736da639..c456ef73f 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -72,11 +72,26 @@ inline Node mkVar(unsigned size) {
}
inline Node mkAnd(std::vector<TNode>& children) {
- if (children.size() > 1) {
- return NodeManager::currentNM()->mkNode(kind::AND, children);
- } else {
- return children[0];
+ std::set<TNode> distinctChildren;
+ distinctChildren.insert(children.begin(), children.end());
+
+ if (children.size() == 0) {
+ return mkTrue();
+ }
+
+ if (children.size() == 1) {
+ return *children.begin();
}
+
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = distinctChildren.begin();
+ std::set<TNode>::const_iterator it_end = distinctChildren.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
+ }
+
+ return conjunction;
}
inline Node mkSortedNode(Kind kind, std::vector<Node>& children) {
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 71bbefb6a..5c2cedf5b 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -103,8 +103,9 @@ public:
* Propagate a theory literal.
*
* @param n - a theory consequence at the current decision level
+ * @return false if an immediate conflict was encountered
*/
- virtual void propagate(TNode n) throw(AssertionException) = 0;
+ virtual bool propagate(TNode n) throw(AssertionException) = 0;
/**
* Request that the core make a decision on this atom. The decision
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 0c893482a..b081e27ef 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -15,25 +15,26 @@
** \todo document this file
**/
+
#include "theory/shared_terms_database.h"
+#include "theory/theory_engine.h"
using namespace std;
using namespace CVC4;
using namespace theory;
-SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context)
- : ContextNotifyObj(context),
- d_context(context),
- d_statSharedTerms("theory::shared_terms", 0),
- d_addedSharedTermsSize(context, 0),
- d_termsToTheories(context),
- d_alreadyNotifiedMap(context),
- d_sharedNotify(notify),
- d_termToNotifyList(context),
- d_allocatedNLSize(0),
- d_allocatedNLNext(context, 0),
- d_EENotify(*this),
- d_equalityEngine(d_EENotify, context, "SharedTermsDatabase")
+SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context)
+: ContextNotifyObj(context)
+, d_context(context)
+, d_statSharedTerms("theory::shared_terms", 0)
+, d_addedSharedTermsSize(context, 0)
+, d_termsToTheories(context)
+, d_alreadyNotifiedMap(context)
+, d_registeredEqualities(context)
+, d_EENotify(*this)
+, d_equalityEngine(d_EENotify, context, "SharedTermsDatabase")
+, d_theoryEngine(theoryEngine)
+, d_inConflict(context, false)
{
StatisticsRegistry::registerStat(&d_statSharedTerms);
}
@@ -41,11 +42,15 @@ SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context
SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException)
{
StatisticsRegistry::unregisterStat(&d_statSharedTerms);
- for (unsigned i = 0; i < d_allocatedNLSize; ++i) {
- d_allocatedNL[i]->deleteSelf();
- }
}
+void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
+ d_registeredEqualities.insert(equality);
+ d_equalityEngine.addTriggerEquality(equality);
+ checkForConflict();
+}
+
+
void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) {
Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl;
@@ -57,9 +62,6 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo
d_addedSharedTerms.push_back(atom);
d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
d_termsToTheories[search_pair] = theories;
- if (!d_equalityEngine.hasTerm(term)) {
- d_equalityEngine.addTriggerTerm(term, THEORY_UF);
- }
} else {
Assert(theories != (*find).second);
d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second);
@@ -120,104 +122,26 @@ Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const {
}
}
-
-SharedTermsDatabase::NotifyList* SharedTermsDatabase::getNewNotifyList()
+bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNode b, bool value)
{
- NotifyList* retval;
- if (d_allocatedNLSize == d_allocatedNLNext) {
- retval = new (true) NotifyList(d_context);
- d_allocatedNL.push_back(retval);
- d_allocatedNLNext = ++d_allocatedNLSize;
- }
- else {
- retval = d_allocatedNL[d_allocatedNLNext];
- d_allocatedNLNext = d_allocatedNLNext + 1;
- }
- Assert(retval->empty());
- return retval;
-}
+ Debug("shared-terms-database") << "SharedTermsDatabase::newEquality(" << theory << a << "," << b << ", " << (value ? "true" : "false") << ")" << endl;
-
-void SharedTermsDatabase::mergeSharedTerms(TNode a, TNode b)
-{
- // Note: a is the new representative
- Debug("shared-terms-database") << "SharedTermsDatabase::mergeSharedTerms(" << a << "," << b << ")" << endl;
-
- NotifyList* pnlLeft = NULL;
- NotifyList* pnlRight = NULL;
-
- TermToNotifyList::iterator it = d_termToNotifyList.find(a);
- if (it == d_termToNotifyList.end()) {
- pnlLeft = getNewNotifyList();
- d_termToNotifyList[a] = pnlLeft;
- }
- else {
- pnlLeft = (*it).second;
- }
- it = d_termToNotifyList.find(b);
- if (it != d_termToNotifyList.end()) {
- pnlRight = (*it).second;
+ if (d_inConflict) {
+ return false;
}
- // Get theories interested in EC for lhs
- Theory::Set lhsSet = getNotifiedTheories(a);
- Theory::Set rhsSet = getNotifiedTheories(b);
- NotifyList::iterator nit;
- TNode left, right;
-
- for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) {
-
- if (Theory::setContains(currentTheory, rhsSet)) {
- right = b;
- }
- else if (pnlRight != NULL &&
- ((nit = pnlRight->find(currentTheory)) != pnlRight->end())) {
- right = (*nit).second;
- }
- else {
- // no match for right: continue
- continue;
- }
-
- if (Theory::setContains(currentTheory, lhsSet)) {
- left = a;
- }
- else if ((nit = pnlLeft->find(currentTheory)) != pnlLeft->end()) {
- left = (*nit).second;
- }
- else {
- // no match for left: insert right into left
- (*pnlLeft)[currentTheory] = right;
- continue;
- }
-
- // New shared equality: notify the client
-
- // TODO: add propagation of disequalities?
-
- assertEq(left.eqNode(right), currentTheory);
+ // Propagate away
+ Node equality = a.eqNode(b);
+ if (value) {
+ d_theoryEngine->assertToTheory(equality, theory, THEORY_BUILTIN);
+ } else {
+ d_theoryEngine->assertToTheory(equality.notNode(), theory, THEORY_BUILTIN);
}
-}
-
-
-void SharedTermsDatabase::assertEq(TNode equality, TheoryId theory)
-{
- Debug("shared-terms-database") << "SharedTermsDatabase::assertEq(" << equality << ") to theory " << theory << endl;
- Node normalized = Rewriter::rewriteEquality(theory, equality);
- if (normalized.getKind() != kind::CONST_BOOLEAN || !normalized.getConst<bool>()) {
- // Notify client
- d_sharedNotify.notify(normalized, equality, theory);
- }
+ // As you were
+ return true;
}
-
-// term was just part of an assertion that makes it shared for theories
-// Let's mark that the set theories has now been notified
-// In addition, we make sure the equivalence class containing term knows a
-// representative for each theory in theories.
-// Finally, if the EC already knows a rep for a theory that was just notified, we
-// have to tell the theory that these two terms are equal.
void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) {
// Find out if there are any new theories that were notified about this term
@@ -232,87 +156,46 @@ void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) {
if (newlyNotified == 0) {
return;
}
-
+
Debug("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term << ")" << endl;
// First update the set of notified theories for this term
d_alreadyNotifiedMap[term] = Theory::setUnion(newlyNotified, alreadyNotified);
- // Now get the representative of the equivalence class and find out which theories it represents
- TNode rep = d_equalityEngine.getRepresentative(term);
- if (rep != term) {
- alreadyNotified = 0;
- theoriesFind = d_alreadyNotifiedMap.find(rep);
- if (theoriesFind != d_alreadyNotifiedMap.end()) {
- alreadyNotified = (*theoriesFind).second;
- }
- }
-
- // For each theory that is newly notified
- for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) {
- if (Theory::setContains(theory, newlyNotified)) {
-
- Debug("shared-terms-database") << "SharedTermsDatabase::markNotified: processing theory " << theory << endl;
-
- if (Theory::setContains(theory, alreadyNotified)) {
- // rep represents this theory already, need to assert that term = rep
- Assert(rep != term);
- assertEq(rep.eqNode(term), theory);
- }
- else {
- // Get the list of terms representing theories for this EC
- TermToNotifyList::iterator it = d_termToNotifyList.find(rep);
- if (it == d_termToNotifyList.end()) {
- // No need to do anything - no list associated with this EC
- Assert(term == rep);
- }
- else {
- NotifyList* pnl = (*it).second;
- Assert(pnl != NULL);
-
- // Check if this theory is already represented
- NotifyList::iterator nit = pnl->find(theory);
- if (nit != pnl->end()) {
- // Already have a representative for this theory, assert term equal to it
- assertEq((*nit).second.eqNode(term), theory);
- }
- else {
- // if term == rep, no need to do anything, as term will represent the theory via alreadyNotifiedMap
- if (term != rep) {
- // No term in this EC represents this theory, so add term as a new representative
- Debug("shared-terms-database") << "SharedTermsDatabase::markNotified: adding " << term << " to representative " << rep << " for theory " << theory << endl;
- (*pnl)[theory] = term;
- }
- }
- }
- }
- }
+ // Mark the shared terms in the equality engine
+ theory::TheoryId currentTheory;
+ while ((currentTheory = Theory::setPop(newlyNotified)) != THEORY_LAST) {
+ d_equalityEngine.addTriggerTerm(term, currentTheory);
}
+
+ // Check for any conflits
+ checkForConflict();
}
-
-bool SharedTermsDatabase::areEqual(TNode a, TNode b) {
+bool SharedTermsDatabase::areEqual(TNode a, TNode b) const {
return d_equalityEngine.areEqual(a,b);
}
-
-bool SharedTermsDatabase::areDisequal(TNode a, TNode b) {
+bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const {
return d_equalityEngine.areDisequal(a,b,false);
}
-void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason)
+void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode reason)
{
- bool negated = literal.getKind() == kind::NOT;
- TNode atom = negated ? literal[0] : literal;
- if (negated) {
- Assert(!d_equalityEngine.areDisequal(atom[0], atom[1],false));
- d_equalityEngine.assertEquality(atom, false, reason);
- // !!! need to send this out
- }
- else {
- Assert(!d_equalityEngine.areEqual(atom[0], atom[1]));
- d_equalityEngine.assertEquality(atom, true, reason);
+ Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl;
+ // Add it to the equality engine
+ d_equalityEngine.assertEquality(equality, polarity, reason);
+ // Check for conflict
+ checkForConflict();
+}
+
+bool SharedTermsDatabase::propagateEquality(TNode equality, bool polarity) {
+ if (polarity) {
+ d_theoryEngine->propagate(equality, THEORY_BUILTIN);
+ } else {
+ d_theoryEngine->propagate(equality.notNode(), THEORY_BUILTIN);
}
+ return true;
}
static Node mkAnd(const std::vector<TNode>& conjunctions) {
@@ -335,18 +218,35 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) {
}
return conjunction;
-}/* mkAnd() */
+}
+void SharedTermsDatabase::checkForConflict() {
+ if (d_inConflict) {
+ d_inConflict = false;
+ std::vector<TNode> assumptions;
+ d_equalityEngine.explainEquality(d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions);
+ Node conflict = mkAnd(assumptions);
+ d_theoryEngine->conflict(conflict, THEORY_BUILTIN);
+ d_conflictLHS = d_conflictRHS = Node::null();
+ }
+}
-Node SharedTermsDatabase::explain(TNode literal)
-{
- std::vector<TNode> assumptions;
- if (literal.getKind() == kind::NOT) {
- Assert(literal[0].getKind() == kind::EQUAL);
- d_equalityEngine.explainEquality(literal[0][0], literal[0][1], false, assumptions);
+bool SharedTermsDatabase::isKnown(TNode literal) const {
+ bool polarity = literal.getKind() != kind::NOT;
+ TNode equality = polarity ? literal : literal[0];
+ if (polarity) {
+ return d_equalityEngine.areEqual(equality[0], equality[1]);
} else {
- Assert(literal.getKind() == kind::EQUAL);
- d_equalityEngine.explainEquality(literal[0], literal[1], true, assumptions);
+ return d_equalityEngine.areDisequal(equality[0], equality[1], false);
}
- return mkAnd(assumptions);
}
+
+Node SharedTermsDatabase::explain(TNode literal) const {
+ bool polarity = literal.getKind() != kind::NOT;
+ TNode atom = polarity ? literal : literal[0];
+ Assert(atom.getKind() == kind::EQUAL);
+ std::vector<TNode> assumptions;
+ d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+ return mkAnd(assumptions);
+}
+
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index c044097ff..1a38d7332 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -18,12 +18,14 @@
#include "expr/node.h"
#include "theory/theory.h"
-#include "context/context.h"
-#include "util/stats.h"
#include "theory/uf/equality_engine.h"
+#include "util/stats.h"
+#include "context/cdhashset.h"
namespace CVC4 {
+class TheoryEngine;
+
class SharedTermsDatabase : public context::ContextNotifyObj {
public:
@@ -54,51 +56,20 @@ private:
/** Context-dependent size of the d_addedSharedTerms list */
context::CDO<unsigned> d_addedSharedTermsSize;
- typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
-
/** A map from atoms and subterms to the theories that use it */
+ typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
SharedTermsTheoriesMap d_termsToTheories;
- typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
-
/** Map from term to theories that have already been notified about the shared term */
+ typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
AlreadyNotifiedMap d_alreadyNotifiedMap;
-public:
-
- /** Class for notifications about new shared term equalities */
- class SharedTermsNotifyClass {
- public:
- SharedTermsNotifyClass() {}
- virtual ~SharedTermsNotifyClass() {}
- virtual void notify(TNode literal, TNode original, theory::TheoryId theory) = 0;
- };
+ /** The registered equalities for propagation */
+ typedef context::CDHashSet<TNode, TNodeHashFunction> RegisteredEqualitiesSet;
+ RegisteredEqualitiesSet d_registeredEqualities;
private:
- // Instance of class to send shared term notifications to
- SharedTermsNotifyClass& d_sharedNotify;
-
- // Type for list of theory, node pairs: theory is theory to be notified,
- // node is the representative for this equivalence class known to the
- // theory that will be notified
- typedef context::CDHashMap<theory::TheoryId, TNode, __gnu_cxx::hash<unsigned> > NotifyList;
- typedef context::CDHashMap<TNode, NotifyList*, TNodeHashFunction> TermToNotifyList;
-
- // Map from terms (only valid for reps) to their notify lists
- // Note that theory, term pairs only need to be in the notify list if the
- // representative term is not a valid shared term for the theory.
- TermToNotifyList d_termToNotifyList;
-
- // List of allocated NotifyList* objects
- std::vector<NotifyList*> d_allocatedNL;
-
- // Total number of allocated NotifyList* objects
- unsigned d_allocatedNLSize;
-
- // Size of portion of d_allocatedNL that is currently in use
- context::CDO<unsigned> d_allocatedNLNext;
-
/** This method removes all the un-necessary stuff from the maps */
void backtrack();
@@ -108,7 +79,7 @@ private:
public:
EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
bool eqNotifyTriggerEquality(TNode equality, bool value) {
- Unreachable();
+ d_sharedTerms.propagateEquality(equality, value);
return true;
}
@@ -118,14 +89,12 @@ private:
}
bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) {
- if (value) {
- d_sharedTerms.mergeSharedTerms(t1, t2);
- }
- return true;
+ return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
}
bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
- return true;
+ d_sharedTerms.conflict(t1, t2, true);
+ return false;
}
};
@@ -135,24 +104,83 @@ private:
/** Equality engine */
theory::eq::EqualityEngine d_equalityEngine;
- /** Attach a new notify list to an equivalence class representative */
- NotifyList* getNewNotifyList();
+ /**
+ * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with
+ * the theory. Returns false if there is a direct conflict (via rewrite for example).
+ */
+ bool propagateSharedEquality(theory::TheoryId theory, TNode a, TNode b, bool value);
+
+ /**
+ * Called from the equality engine when a trigger equality is deduced.
+ */
+ bool propagateEquality(TNode equality, bool polarity);
+
+ /** Theory engine */
+ TheoryEngine* d_theoryEngine;
+
+ /** Are we in conflict */
+ context::CDO<bool> d_inConflict;
+
+ /** Conflicting terms, if any */
+ Node d_conflictLHS, d_conflictRHS;
+
+ /** Polarity of the conflict */
+ bool d_conflictPolarity;
+
+ /** Called by the equality engine notify to mark the conflict */
+ void conflict(TNode lhs, TNode rhs, bool polarity) {
+ if (!d_inConflict) {
+ // Only remember it if we're not already in conflict
+ d_inConflict = true;
+ d_conflictLHS = lhs;
+ d_conflictRHS = rhs;
+ d_conflictPolarity = polarity;
+ }
+ }
- /** Method called by equalityEngine when a becomes equal to b */
- void mergeSharedTerms(TNode a, TNode b);
+ /**
+ * Should be called before any public non-const method in order to
+ * enqueue the conflict to the theory engine.
+ */
+ void checkForConflict();
public:
- SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context);
+ SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);
~SharedTermsDatabase() throw(AssertionException);
/**
+ * Asserts the equality to the shared terms database,
+ */
+ void assertEquality(TNode equality, bool polarity, TNode reason);
+
+ /**
+ * Return whether the equality is alreday known to the engine
+ */
+ bool isKnown(TNode literal) const;
+
+ /**
+ * Returns an explanation of the propagation that came from the database.
+ */
+ Node explain(TNode literal) const;
+
+ /**
+ * Add an equality to propagate.
+ */
+ void addEqualityToPropagate(TNode equality);
+
+ /**
* Add a shared term to the database. The shared term is a subterm of the atom and
* should be associated with the given theory.
*/
void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories);
/**
+ * Mark that the given theories have been notified of the given shared term.
+ */
+ void markNotified(TNode term, theory::Theory::Set theories);
+
+ /**
* Returns true if the atom contains any shared terms, false otherwise.
*/
bool hasSharedTerms(TNode atom) const;
@@ -176,26 +204,32 @@ public:
* Get the theories that share the term and have been notified already.
*/
theory::Theory::Set getNotifiedTheories(TNode term) const;
-
- // Notify theory about a new equality between shared terms
- void assertEq(TNode equality, theory::TheoryId theory);
-
+
/**
- * Mark that the given theories have been notified of the given shared term.
+ * Returns true if the term is currently registered as shared with some theory.
*/
- void markNotified(TNode term, theory::Theory::Set theories);
-
bool isShared(TNode term) const {
- return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
+ return term.isConst() || d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
}
- bool areEqual(TNode a, TNode b);
-
- bool areDisequal(TNode a, TNode b);
+ /**
+ * Returns true if the literal is an (dis-)equality with both sides registered as shared with
+ * some theory.
+ */
+ bool isSharedEquality(TNode literal) const {
+ TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
+ return atom.getKind() == kind::EQUAL && isShared(atom[0]) && isShared(atom[1]);
+ }
- void processSharedLiteral(TNode literal, TNode reason);
+ /**
+ * Returns true if the shared terms a and b are known to be equal.
+ */
+ bool areEqual(TNode a, TNode b) const;
- Node explain(TNode literal);
+ /**
+ * Retursn true if the shared terms a and b are known to be dis-equal.
+ */
+ bool areDisequal(TNode a, TNode b) const;
protected:
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)
{
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index bc9f4c889..ed95149b3 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -46,16 +46,19 @@
namespace CVC4 {
-// In terms of abstraction, this is below (and provides services to)
-// PropEngine.
-
+/**
+ * A pair of a theory and a node. This is used to mark the flow of
+ * propagations between theories.
+ */
struct NodeTheoryPair {
Node node;
theory::TheoryId theory;
- NodeTheoryPair(TNode node, theory::TheoryId theory)
- : node(node), theory(theory) {}
+ size_t timestamp;
+ NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp)
+ : node(node), theory(theory), timestamp(timestamp) {}
NodeTheoryPair()
: theory(theory::THEORY_LAST) {}
+ // Comparison doesn't take into account the timestamp
bool operator == (const NodeTheoryPair& pair) const {
return node == pair.node && theory == pair.theory;
}
@@ -63,6 +66,7 @@ struct NodeTheoryPair {
struct NodeTheoryPairHashFunction {
NodeHashFunction hashFunction;
+ // Hash doesn't take into account the timestamp
size_t operator()(const NodeTheoryPair& pair) const {
return hashFunction(pair.node)*0x9e3779b9 + pair.theory;
}
@@ -75,6 +79,9 @@ struct NodeTheoryPairHashFunction {
* CVC4.
*/
class TheoryEngine {
+
+ /** Shared terms database can use the internals notify the theories */
+ friend class SharedTermsDatabase;
/** Associated PropEngine engine */
prop::PropEngine* d_propEngine;
@@ -103,21 +110,6 @@ class TheoryEngine {
*/
const LogicInfo& d_logicInfo;
- // NotifyClass: template helper class for Shared Terms Database
- class NotifyClass :public SharedTermsDatabase::SharedTermsNotifyClass {
- TheoryEngine& d_theoryEngine;
- public:
- NotifyClass(TheoryEngine& engine): d_theoryEngine(engine) {}
- ~NotifyClass() {}
-
- void notify(TNode literal, TNode original, theory::TheoryId theory) {
- d_theoryEngine.propagateSharedLiteral(literal, original, theory);
- }
- };
-
- // Instance of NotifyClass
- NotifyClass d_notify;
-
/**
* The database of shared terms.
*/
@@ -221,11 +213,11 @@ class TheoryEngine {
d_engine->conflict(conflictNode, d_theory);
}
- void propagate(TNode literal) throw(AssertionException) {
+ bool propagate(TNode literal) throw(AssertionException) {
Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
++ d_statistics.propagations;
d_engine->d_outputChannelUsed = true;
- d_engine->propagate(literal, d_theory);
+ return d_engine->propagate(literal, d_theory);
}
void propagateAsDecision(TNode literal) throw(AssertionException) {
@@ -263,28 +255,11 @@ class TheoryEngine {
context::CDO<bool> d_inConflict;
/**
- * Explain the equality literals and push all the explaining literals
- * into the builder. All the non-equality literals are pushed to the
- * builder.
- */
- void explainEqualities(theory::TheoryId theoryId, TNode literals, NodeBuilder<>& builder);
-
- /**
- * Same as above, but just for single equalities.
- */
- void explainEquality(theory::TheoryId theoryId, TNode eqLiteral, NodeBuilder<>& builder);
-
- /**
* Called by the theories to notify of a conflict.
*/
void conflict(TNode conflict, theory::TheoryId theoryId);
/**
- * Called by shared terms database to notify of a conflict.
- */
- void sharedConflict(TNode conflict);
-
- /**
* Debugging flag to ensure that shutdown() is called before the
* destructor.
*/
@@ -310,63 +285,16 @@ class TheoryEngine {
d_propEngine->spendResource();
}
- struct SharedLiteral {
- /**
- * The node/theory pair for the assertion. THEORY_LAST indicates this is a SAT
- * literal and should be sent to the SAT solver
- */
- NodeTheoryPair toAssert;
- /** This is the node that we will use to explain it */
- Node toExplain;
-
- SharedLiteral(TNode assertion, TNode original, theory::TheoryId receivingTheory)
- : toAssert(assertion, receivingTheory),
- toExplain(original)
- { }
- };
-
- /**
- * Map from nodes to theories.
- */
- typedef context::CDHashMap<Node, theory::TheoryId, NodeHashFunction> SharedLiteralsInMap;
-
/**
- * All shared literals asserted to theory engine.
- * Maps from literal to the theory that sent the literal (THEORY_LAST means sent from SAT).
+ * Mapping of propagations from recievers to senders.
*/
- SharedLiteralsInMap d_sharedLiteralsIn;
-
- /**
- * Map from literals asserted by theory engine to literal that can explain
- */
- typedef context::CDHashMap<NodeTheoryPair, Node, NodeTheoryPairHashFunction> AssertedLiteralsOutMap;
-
- /**
- * All literals asserted to theories from theory engine.
- * Maps from literal/theory pair to literal that can explain this assertion.
- */
- AssertedLiteralsOutMap d_assertedLiteralsOut;
-
- /**
- * Shared literals queud up to be asserted to the individual theories.
- */
- std::vector<SharedLiteral> d_propagatedSharedLiterals;
-
- void propagateSharedLiteral(TNode literal, TNode original, theory::TheoryId theory)
- {
- if (literal.getKind() == kind::CONST_BOOLEAN) {
- Assert(!literal.getConst<bool>());
- sharedConflict(original);
- }
- else {
- d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory));
- }
- }
+ typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> PropagationMap;
+ PropagationMap d_propagationMap;
/**
- * Assert the shared literals that are queued up to the theories.
+ * Timestamp of propagations
*/
- void outputSharedLiterals();
+ context::CDO<size_t> d_propagationMapTimestamp;
/**
* Literals that are propagated by the theory. Note that these are TNodes.
@@ -395,8 +323,9 @@ class TheoryEngine {
/**
* Called by the output channel to propagate literals and facts
+ * @return false if immediate conflict
*/
- void propagate(TNode literal, theory::TheoryId theory);
+ bool propagate(TNode literal, theory::TheoryId theory);
/**
* Internal method to call the propagation routines and collect the
@@ -427,55 +356,8 @@ class TheoryEngine {
/**
* Adds a new lemma, returning its status.
*/
- theory::LemmaStatus lemma(TNode node, bool negated, bool removable) {
- if(Dump.isOn("t-lemmas")) {
- Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
- << QueryCommand(node.toExpr());
- }
-
- // Share with other portfolio threads
- if(Options::current()->lemmaOutputChannel != NULL) {
- Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr());
- }
-
- // 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);
- }
-
- // 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.
-
- // assert to decision engine
- if(!removable)
- d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap);
-
- // 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());
- }
-
+ theory::LemmaStatus lemma(TNode node, bool negated, bool removable);
+
/** Time spent in theory combination */
TimerStat d_combineTheoriesTime;
@@ -535,6 +417,45 @@ private:
*/
bool d_inPreregister;
+ /**
+ * Did the theories get any new facts since the last time we called
+ * check()
+ */
+ context::CDO<bool> d_factsAsserted;
+
+ /**
+ * 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);
+
+ /**
+ * Marks a theory propagation from a theory to a theory where a
+ * theory could be the THEORY_SAT_SOLVER for literals coming from
+ * or being propagated to the SAT solver. If the receiving theory
+ * already recieved the literal, the method returns false, otherwise
+ * it returns true.
+ *
+ * @param assertion the normalized assertion being sent
+ * @param originalAssertion the actual assertion that was sent
+ * @param toTheoryId the theory that is on the receiving end
+ * @param fromTheoryId the theory that sent the assertino
+ * @return true if a new assertion, false if theory already got it
+ */
+ bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId);
+
+ /**
+ * Computes the explanation by travarsing the propagation graph and
+ * asking relevant theories to explain the propagations. Initially
+ * the explanation vector should contain only the element (node, theory)
+ * where the node is the one to be explained, and the theory is the
+ * theory that sent the literal.
+ */
+ void getExplanation(std::vector<NodeTheoryPair>& explanationVector);
+
public:
/**
@@ -657,40 +578,14 @@ public:
bool properPropagation(TNode lit) const;
bool properExplanation(TNode node, TNode expl) const;
- enum ExplainTaskKind {
- // Literal sent out from the theory engine
- SHARED_LITERAL_OUT,
- // Explanation produced by a theory
- THEORY_EXPLANATION,
- // Explanation produced by the shared terms database
- SHARED_DATABASE_EXPLANATION
- };
-
- struct ExplainTask {
- Node node;
- ExplainTaskKind kind;
- theory::TheoryId theory;
- ExplainTask(Node n, ExplainTaskKind k, theory::TheoryId tid = theory::THEORY_LAST) :
- node(n), kind(k), theory(tid) {}
- bool operator == (const ExplainTask& other) const {
- return node == other.node && kind == other.kind && theory == other.theory;
- }
- };
-
- struct ExplainTaskHashFunction {
- size_t operator () (const ExplainTask& task) const {
- size_t hash = 0;
- hash = 0x9e3779b9 + NodeHashFunction().operator()(task.node);
- hash ^= 0x9e3779b9 + task.kind + (hash << 6) + (hash >> 2);
- hash ^= 0x9e3779b9 + task.theory + (hash << 6) + (hash >> 2);
- return hash;
- }
- };
-
+ /**
+ * Returns an explanation of the node propagated to the SAT solver.
+ */
Node getExplanation(TNode node);
- Node explain(ExplainTask toExplain);
-
+ /**
+ * Returns the value of the given node.
+ */
Node getValue(TNode node);
/**
@@ -732,6 +627,9 @@ private:
/** Prints the assertions to the debug stream */
void printAssertions(const char* tag);
+ /** Dump the assertions to the dump */
+ void dumpAssertions(const char* tag);
+
/** For preprocessing pass simplifying ITEs */
ITESimplifier d_iteSimplifier;
@@ -739,6 +637,7 @@ private:
UnconstrainedSimplifier d_unconstrainedSimp;
public:
+
Node ppSimpITE(TNode assertion);
void ppUnconstrainedSimp(std::vector<Node>& assertions);
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index aaf47425b..bf1370090 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -78,9 +78,10 @@ public:
push(CONFLICT, n);
}
- void propagate(TNode n)
+ bool propagate(TNode n)
throw(AssertionException) {
push(PROPAGATE, n);
+ return true;
}
void propagateAsDecision(TNode n)
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 5093e5a7b..4cd54a2bf 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -62,14 +62,14 @@ void EqualityEngine::init() {
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
+ d_triggerDatabaseAllocatedSize = 100000;
+ d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
+
addTerm(d_true);
addTerm(d_false);
d_trueId = getNodeId(d_true);
d_falseId = getNodeId(d_false);
-
- d_triggerDatabaseAllocatedSize = 100000;
- d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
}
EqualityEngine::~EqualityEngine() throw(AssertionException) {
@@ -114,7 +114,8 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c
}
void EqualityEngine::enqueue(const MergeCandidate& candidate) {
- d_propagationQueue.push(candidate);
+ Debug("equality") << "EqualityEngine::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl;
+ d_propagationQueue.push(candidate);
}
EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality) {
@@ -144,7 +145,15 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId
if (isEquality && d_isConstant[t1ClassId] && d_isConstant[t2ClassId]) {
if (t1ClassId != t2ClassId) {
Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl;
+ Assert(d_nodes[funId].getKind() == kind::EQUAL);
enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+ // Also enqueue the symmetric one
+ TNode eq = d_nodes[funId];
+ Node symmetricEq = eq[1].eqNode(eq[0]);
+ if (hasTerm(symmetricEq)) {
+ EqualityNodeId symmFunId = getNodeId(symmetricEq);
+ enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+ }
}
}
} else {
@@ -154,8 +163,8 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId
}
// Add to the use lists
- d_equalityNodes[t1ClassId].usedIn<USE_LIST_FUNCTIONS>(funId, d_useListNodes);
- d_equalityNodes[t2ClassId].usedIn<USE_LIST_FUNCTIONS>(funId, d_useListNodes);
+ d_equalityNodes[t1].usedIn(funId, d_useListNodes);
+ d_equalityNodes[t2].usedIn(funId, d_useListNodes);
// Return the new id
Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl;
@@ -238,6 +247,20 @@ void EqualityEngine::addTerm(TNode t) {
// We set this here as this only applies to actual terms, not the
// intermediate application terms
d_isBoolean[result] = true;
+ } else if (t.isConst()) {
+ // Non-Boolean constants are trigger terms for all tags
+ EqualityNodeId tId = getNodeId(t);
+ d_newSetTags = 0;
+ d_newSetTriggersSize = THEORY_LAST;
+ for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) {
+ d_newSetTags = Theory::setInsert(currentTheory, d_newSetTags);
+ d_newSetTriggers[currentTheory] = tId;
+ }
+ // Add it to the list for backtracking
+ d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id));
+ d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
+ // Mark the the new set as a trigger
+ d_nodeIndividualTrigger[tId] = newTriggerTermSet();
}
propagate();
@@ -319,15 +342,20 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
assertEqualityInternal(eq, d_false, reason);
propagate();
assertEqualityInternal(eq[1].eqNode(eq[0]), d_false, reason);
- propagate();
+ propagate();
if (d_done) {
return;
}
- // If we are adding a disequality, notify of the shared term representatives
+ // If both have constant representatives, we don't notify anyone
EqualityNodeId a = getNodeId(eq[0]);
EqualityNodeId b = getNodeId(eq[1]);
+ if (isConstant(a) && isConstant(b)) {
+ return;
+ }
+
+ // If we are adding a disequality, notify of the shared term representatives
EqualityNodeId eqId = getNodeId(eq);
TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[a];
TriggerTermSetRef bTriggerRef = d_nodeIndividualTrigger[b];
@@ -356,6 +384,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
d_deducedDisequalityReasons.push_back(EqualityPair(bSharedId, b));
d_deducedDisequalityReasons.push_back(EqualityPair(eqId, d_falseId));
storePropagatedDisequality(d_nodes[aSharedId], d_nodes[bSharedId], 3);
+
// We notify even if the it's already been sent (they are not
// disequal at assertion, and we need to notify for each tag)
if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) {
@@ -383,7 +412,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
Assert(triggersFired.empty());
-
+
++ d_stats.mergesCount;
EqualityNodeId class1Id = class1.getFind();
@@ -391,6 +420,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
// Check for constant merges
bool isConstant = d_isConstant[class1Id];
+ Assert(isConstant || !d_isConstant[class2Id]);
// Update class2 representative information
Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl;
@@ -438,13 +468,13 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl;
// Go through the uselist and check for congruences
- UseListNodeId currentUseId = currentNode.getUseList<USE_LIST_FUNCTIONS>();
+ UseListNodeId currentUseId = currentNode.getUseList();
while (currentUseId != null_uselist_id) {
// Get the node of the use list
UseListNode& useNode = d_useListNodes[currentUseId];
// Get the function application
EqualityNodeId funId = useNode.getApplicationId();
- Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl;
+ Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl;
const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
// Check if there is an application with find arguments
EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
@@ -460,11 +490,16 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
// There is no representative, so we can add one, we remove this when backtracking
storeApplicationLookup(funNormalized, funId);
// Now, if we're constant and it's an equality, check if the other guy is also a constant
- if (isConstant && funNormalized.isEquality) {
- if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) {
- // both constants
- if (funNormalized.a != funNormalized.b) {
- enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+ if (funNormalized.isEquality) {
+ if (d_isConstant[aNormalized] && d_isConstant[bNormalized] && aNormalized != bNormalized) {
+ Assert(d_nodes[funId].getKind() == kind::EQUAL);
+ enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+ // Also enqueue the symmetric one
+ TNode eq = d_nodes[funId];
+ Node symmetricEq = eq[1].eqNode(eq[0]);
+ if (hasTerm(symmetricEq)) {
+ EqualityNodeId symmFunId = getNodeId(symmetricEq);
+ enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
}
}
}
@@ -482,6 +517,17 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
// Now merge the lists
class1.merge<true>(class2);
+ // Notify of the constants merge
+ bool constantMerge = false;
+ if (isConstant && d_isConstant[class2Id]) {
+ constantMerge = true;
+ if (d_performNotify) {
+ if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) {
+ return false;
+ }
+ }
+ }
+
// Go through the triggers and store the dis-equalities
unsigned i = 0, j = 0;
for (; i < triggersFired.size();) {
@@ -543,7 +589,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
// copy tag1
EqualityNodeId tag1id = d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++];
// since they are both tagged notify of merge
- if (d_performNotify) {
+ if (d_performNotify && !constantMerge) {
EqualityNodeId tag2id = class2triggers.triggers[i2++];
if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) {
return false;
@@ -566,15 +612,6 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
}
}
- // Notify of the constants merge
- if (isConstant && d_isConstant[class2Id]) {
- if (d_performNotify) {
- if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) {
- return false;
- }
- }
- }
-
// Everything fine
return true;
}
@@ -680,12 +717,12 @@ void EqualityEngine::backtrack() {
Debug("equality") << "EqualityEngine::backtrack(): removing node " << d_nodes[i] << std::endl;
d_nodeIds.erase(d_nodes[i]);
- const FunctionApplication& app = d_applications[i].normalized;
+ const FunctionApplication& app = d_applications[i].original;
if (app.isApplication()) {
// Remove b from use-list
- getEqualityNode(app.b).removeTopFromUseList<USE_LIST_FUNCTIONS>(d_useListNodes);
+ getEqualityNode(app.b).removeTopFromUseList(d_useListNodes);
// Remove a from use-list
- getEqualityNode(app.a).removeTopFromUseList<USE_LIST_FUNCTIONS>(d_useListNodes);
+ getEqualityNode(app.a).removeTopFromUseList(d_useListNodes);
}
}
@@ -818,8 +855,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
// Go through the equality edges of this node
EqualityEdgeId currentEdge = d_equalityGraph[currentNode];
- Debug("equality") << "EqualityEngine::getExplanation(): edgesId = " << currentEdge << std::endl;
- Debug("equality") << "EqualityEngine::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl;
+ if (Debug.isOn("equality")) {
+ Debug("equality") << "EqualityEngine::getExplanation(): edgesId = " << currentEdge << std::endl;
+ Debug("equality") << "EqualityEngine::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl;
+ }
while (currentEdge != null_edge) {
// Get the edge
@@ -871,8 +910,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
Debug("equality") << push;
// Explain why a is a constant
+ Assert(isConstant(eq.a));
getExplanation(eq.a, getEqualityNode(eq.a).getFind(), equalities);
// Explain why b is a constant
+ Assert(isConstant(eq.b));
getExplanation(eq.b, getEqualityNode(eq.b).getFind(), equalities);
Debug("equality") << pop;
@@ -1062,7 +1103,7 @@ void EqualityEngine::propagate() {
// Depending on the merge preference (such as size, or being a constant), merge them
std::vector<TriggerId> triggers;
- if (node2.getSize() > node1.getSize() || d_isConstant[t2classId]) {
+ if ((node2.getSize() > node1.getSize() && !d_isConstant[t1classId]) || d_isConstant[t2classId]) {
Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
d_assertedEqualities.push_back(Equality(t2classId, t1classId));
if (!merge(node2, node1, triggers)) {
@@ -1222,7 +1263,7 @@ size_t EqualityEngine::getSize(TNode t)
void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
{
- Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
+ Debug("equality::trigger") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
Assert(tag != THEORY_LAST);
if (d_done) {
@@ -1243,12 +1284,71 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
// If the term already is in the equivalence class that a tagged representative, just notify
if (d_performNotify) {
EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag);
- if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) {
+ if (eqNodeId != triggerId && !d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) {
d_done = true;
}
}
} else {
+ // Check for disequalities by going through the equivalence class looking for equalities in the
+ // uselists that have been asserted to false. All the representatives appearing on the other
+ // side of such disequalities, that have the tag on, are put in a set.
+ std::set<EqualityNodeId> disequalSet;
+ EqualityNodeId currentId = classId;
+ do {
+ // Current node
+ EqualityNode& currentNode = getEqualityNode(currentId);
+ // Go through the uselist and look for disequalities
+ UseListNodeId currentUseId = currentNode.getUseList();
+ while (!d_done && currentUseId != null_uselist_id) {
+ // Get the normalized equality
+ UseListNode& useNode = d_useListNodes[currentUseId];
+ EqualityNodeId funId = useNode.getApplicationId();
+ const FunctionApplication& fun = d_applications[useNode.getApplicationId()].original;
+ // Check for asserted disequalities
+ if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) {
+ // Get the other equality member
+ EqualityNodeId toCompare = fun.b;
+ if (toCompare == currentId) {
+ toCompare = fun.a;
+ }
+ // Representative of the other member
+ EqualityNodeId toCompareRep = getEqualityNode(toCompare).getFind();
+ Assert(toCompareRep != classId);
+ // Get the trigger set
+ TriggerTermSetRef toCompareTriggerSetRef = d_nodeIndividualTrigger[toCompareRep];
+ // Only notify if we're not both constants
+ if ((!d_isConstant[classId] || !d_isConstant[toCompareRep]) && toCompareTriggerSetRef != null_set_id) {
+ TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef);
+ if (Theory::setContains(tag, toCompareTriggerSet.tags)) {
+ // Get the tag representative
+ EqualityNodeId tagRep = toCompareTriggerSet.getTrigger(tag);
+ // Propagate the disequality if not already done
+ if (!disequalSet.count(tagRep) && d_performNotify) {
+ // Mark as propagated
+ disequalSet.insert(tagRep);
+ // Store the propagation
+ d_deducedDisequalityReasons.push_back(EqualityPair(eqNodeId, currentId));
+ d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep));
+ d_deducedDisequalityReasons.push_back(EqualityPair(funId, d_falseId));
+ storePropagatedDisequality(t, d_nodes[tagRep], 3);
+ // We don't check if it's been propagated already, as we need one per tag
+ if (d_performNotify) {
+ if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[tagRep], false)) {
+ d_done = true;
+ }
+ }
+ }
+ }
+ }
+ }
+ // Go to the next one in the use list
+ currentUseId = useNode.getNext();
+ }
+ // Next in equivalence class
+ currentId = currentNode.getNext();
+ } while (!d_done && currentId != classId);
+
// Setup the data for the new set
if (triggerSetRef != null_set_id) {
// Get the existing set
@@ -1322,7 +1422,7 @@ void EqualityEngine::getUseListTerms(TNode t, std::set<TNode>& output) {
// Get the current node
EqualityNode& currentNode = getEqualityNode(currentId);
// Go through the use-list
- UseListNodeId currentUseId = currentNode.getUseList<USE_LIST_FUNCTIONS>();
+ UseListNodeId currentUseId = currentNode.getUseList();
while (currentUseId != null_uselist_id) {
// Get the node of the use list
UseListNode& useNode = d_useListNodes[currentUseId];
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 5ff8ee4dc..f40c79df3 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -345,6 +345,13 @@ private:
std::vector<bool> d_isConstant;
/**
+ * Returns true if it's a constant
+ */
+ bool isConstant(EqualityNodeId id) const {
+ return d_isConstant[getEqualityNode(id).getFind()];
+ }
+
+ /**
* Map from ids to wheather they are Boolean.
*/
std::vector<bool> d_isBoolean;
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 0baf70fcf..056ee0b84 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -94,8 +94,9 @@ struct MergeCandidate {
EqualityNodeId t1Id, t2Id;
MergeReasonType type;
TNode reason;
- MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason):
- t1Id(x), t2Id(y), type(type), reason(reason) {}
+ MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason)
+ : t1Id(x), t2Id(y), type(type), reason(reason)
+ {}
};
/**
@@ -145,15 +146,6 @@ public:
}
};
-/** Main types of uselists */
-enum UseListType {
- /** Use list of functions where the term appears in */
- USE_LIST_FUNCTIONS,
- /** Use list of asserted disequalities */
- USE_LIST_DISEQUALITIES
-};
-
-
/**
* Main class for representing nodes in the equivalence class. The
* nodes are a circular list, with the representative carrying the
@@ -178,9 +170,6 @@ private:
/** The use list of this node */
UseListNodeId d_useList;
- /** The list of asserted disequalities that this node appears in */
- UseListNodeId d_diseqList;
-
public:
/**
@@ -191,15 +180,13 @@ public:
, d_findId(nodeId)
, d_nextId(nodeId)
, d_useList(null_uselist_id)
- , d_diseqList(null_uselist_id)
{}
/**
* Returns the requested uselist.
*/
- template<UseListType type>
UseListNodeId getUseList() const {
- return type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList;
+ return d_useList;
}
/**
@@ -244,22 +231,20 @@ public:
* Note that this node is used in a function application funId, or
* a negatively asserted equality (dis-equality) with funId.
*/
- template<UseListType type, typename memory_class>
+ template<typename memory_class>
void usedIn(EqualityNodeId funId, memory_class& memory) {
- UseListNodeId& useList = type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList;
UseListNodeId newUseId = memory.size();
- memory.push_back(UseListNode(funId, useList));
- useList = newUseId;
+ memory.push_back(UseListNode(funId, d_useList));
+ d_useList = newUseId;
}
/**
* For backtracking: remove the first element from the uselist and pop the memory.
*/
- template<UseListType type, typename memory_class>
+ template<typename memory_class>
void removeTopFromUseList(memory_class& memory) {
- UseListNodeId& useList = type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList;
- Assert ((int) useList == (int)memory.size() - 1);
- useList = memory.back().getNext();
+ Assert ((int) d_useList == (int)memory.size() - 1);
+ d_useList = memory.back().getNext();
memory.pop_back();
}
};
@@ -288,7 +273,7 @@ struct FunctionApplication {
FunctionApplication(bool isEquality = false, EqualityNodeId a = null_id, EqualityNodeId b = null_id)
: isEquality(isEquality), a(a), b(b) {}
bool operator == (const FunctionApplication& other) const {
- return a == other.a && b == other.b;
+ return isEquality == other.isEquality && a == other.a && b == other.b;
}
bool isApplication() const {
return a != null_id && b != null_id;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index ae8bdc8da..7583f8ee7 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -70,16 +70,6 @@ void TheoryUF::check(Effort level) {
Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
- // If the assertion doesn't have a literal, it's a shared equality, so we set it up
- if (!assertion.isPreregistered) {
- Debug("uf") << "TheoryUF::check(): shared equality, setting up " << fact << std::endl;
- if (fact.getKind() == kind::NOT) {
- preRegisterTerm(fact[0]);
- } else {
- preRegisterTerm(fact);
- }
- }
-
// Do the work
bool polarity = fact.getKind() != kind::NOT;
TNode atom = polarity ? fact : fact[0];
@@ -90,31 +80,8 @@ void TheoryUF::check(Effort level) {
}
}
- // If in conflict, output the conflict
- if (d_conflict) {
- Debug("uf") << "TheoryUF::check(): conflict " << d_conflictNode << std::endl;
- d_out->conflict(d_conflictNode);
- }
-
- // Otherwise we propagate in order to detect a weird conflict like
- // p, x = y
- // p -> f(x) != f(y) -- f(x) = f(y) gets added to the propagation list at preregistration time
- // but when f(x) != f(y) is deduced by the sat solver, so it's asserted, and we don't detect the conflict
- // until we go through the propagation list
- propagate(level);
}/* TheoryUF::check() */
-void TheoryUF::propagate(Effort level) {
- Debug("uf") << "TheoryUF::propagate()" << std::endl;
- if (!d_conflict) {
- for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
- TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
- Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl;
- d_out->propagate(literal);
- }
- }
-}/* TheoryUF::propagate(Effort) */
-
void TheoryUF::preRegisterTerm(TNode node) {
Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
@@ -143,37 +110,18 @@ void TheoryUF::preRegisterTerm(TNode node) {
}/* TheoryUF::preRegisterTerm() */
bool TheoryUF::propagate(TNode literal) {
- Debug("uf") << "TheoryUF::propagate(" << literal << ")" << std::endl;
-
+ Debug("uf::propagate") << "TheoryUF::propagate(" << literal << ")" << std::endl;
// If already in conflict, no more propagation
if (d_conflict) {
- Debug("uf") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
+ Debug("uf::propagate") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
return false;
}
-
- // See if the literal has been asserted already
- Node normalized = Rewriter::rewrite(literal);
-
- // If asserted and is false, we're done or in conflict
- // Note that even trivial equalities have a SAT value (i.e. 1 = 2 -> false)
- bool satValue = false;
- if (d_valuation.hasSatValue(normalized, satValue) && !satValue) {
- Debug("uf") << "TheoryUF::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
- std::vector<TNode> assumptions;
- Node negatedLiteral;
- negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
- assumptions.push_back(negatedLiteral);
- explain(literal, assumptions);
- d_conflictNode = mkAnd(assumptions);
- d_conflict = true;
- return false;
+ // Propagate out
+ bool ok = d_out->propagate(literal);
+ if (!ok) {
+ d_conflict = true;
}
-
- // Nothing, just enqueue it for propagation and mark it as asserted already
- Debug("uf") << "TheoryUF::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
- d_literalsToPropagate.push_back(literal);
-
- return true;
+ return ok;
}/* TheoryUF::propagate(TNode) */
void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
@@ -437,3 +385,13 @@ void TheoryUF::computeCareGraph() {
}
}
}/* TheoryUF::computeCareGraph() */
+
+void TheoryUF::conflict(TNode a, TNode b) {
+ if (Theory::theoryOf(a) == theory::THEORY_BOOL) {
+ d_conflictNode = explain(a.iffNode(b));
+ } else {
+ d_conflictNode = explain(a.eqNode(b));
+ }
+ d_out->conflict(d_conflictNode);
+ d_conflict = true;
+}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 1dfcb86f0..0d35d57d8 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -55,7 +55,7 @@ public:
}
bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
- Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+ Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
return d_uf.propagate(predicate);
} else {
@@ -64,7 +64,7 @@ public:
}
bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
- Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << std::endl;
+ Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
if (value) {
return d_uf.propagate(t1.eqNode(t2));
} else {
@@ -73,12 +73,9 @@ public:
}
bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
- Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
- if (Theory::theoryOf(t1) == THEORY_BOOL) {
- return d_uf.propagate(t1.iffNode(t2));
- } else {
- return d_uf.propagate(t1.eqNode(t2));
- }
+ Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+ d_uf.conflict(t1, t2);
+ return false;
}
};
@@ -119,13 +116,15 @@ private:
/** Symmetry analyzer */
SymmetryBreaker d_symb;
+ /** Conflict when merging two constants */
+ void conflict(TNode a, TNode b);
+
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
void check(Effort);
- void propagate(Effort);
void preRegisterTerm(TNode term);
Node explain(TNode n);
@@ -135,6 +134,8 @@ public:
void addSharedTerm(TNode n);
void computeCareGraph();
+ void propagate(Effort effort) {}
+
EqualityStatus getEqualityStatus(TNode a, TNode b);
std::string identify() const {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback