diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-09 21:25:17 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-09 21:25:17 +0000 |
commit | 1ce0650dcf8ce30424b546deb540974cc510c215 (patch) | |
tree | 74a9985463234fc9adfed2de209c134ed7da359b /src/theory/bv | |
parent | 690fb2843d9845e405fee54eb2d8023eebbd5b72 (diff) |
* simplifying equality engine interface
* notifications are now through the interface subclass instead of a template
* notifications include constants being merged
* changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed
* sat solver now has explicit methods to make true and false constants
* 0-level literals are removed from explanations of propagations
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 90 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 46 |
2 files changed, 60 insertions, 76 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index c9d58574e..4076a7ee0 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -21,7 +21,6 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/valuation.h" #include "theory/bv/bv_sat.h" -#include "theory/uf/equality_engine_impl.h" using namespace CVC4; using namespace CVC4::theory; @@ -52,18 +51,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_toBitBlast(c), d_propagatedBy(c) { - d_true = utils::mkTrue(); - d_false = utils::mkFalse(); - if (d_useEqualityEngine) { - d_equalityEngine.addTerm(d_true); - d_equalityEngine.addTerm(d_false); - d_equalityEngine.addTriggerEquality(d_true, d_false, d_false); - - // add disequality between 0 and 1 bits - d_equalityEngine.addDisequality(utils::mkConst(BitVector((unsigned)1, (unsigned)0)), - utils::mkConst(BitVector((unsigned)1, (unsigned)1)), - d_true); // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT); @@ -137,11 +125,8 @@ void TheoryBV::preRegisterTerm(TNode node) { if (d_useEqualityEngine) { switch (node.getKind()) { case kind::EQUAL: - // Add the terms - d_equalityEngine.addTerm(node); // Add the trigger for equality - d_equalityEngine.addTriggerEquality(node[0], node[1], node); - d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode()); + d_equalityEngine.addTriggerEquality(node); break; default: d_equalityEngine.addTerm(node); @@ -185,15 +170,15 @@ void TheoryBV::check(Effort e) if (predicate.getKind() == kind::EQUAL) { if (negated) { // dis-equality - d_equalityEngine.addDisequality(predicate[0], predicate[1], fact); + d_equalityEngine.assertEquality(predicate, false, fact); } else { // equality - d_equalityEngine.addEquality(predicate[0], predicate[1], fact); + d_equalityEngine.assertEquality(predicate, true, fact); } } else { // Adding predicate if the congruence over it is turned on if (d_equalityEngine.isFunctionKind(predicate.getKind())) { - d_equalityEngine.addPredicate(predicate, !negated, fact); + d_equalityEngine.assertPredicate(predicate, !negated, fact); } } } @@ -279,16 +264,16 @@ void TheoryBV::propagate(Effort e) { bool satValue; if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { // check if we already propagated the negation - Node neg_literal = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal); - if (d_alreadyPropagatedSet.find(neg_literal) != d_alreadyPropagatedSet.end()) { + Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal); + if (d_alreadyPropagatedSet.find(negLiteral) != d_alreadyPropagatedSet.end()) { Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; // we are in conflict std::vector<TNode> assumptions; explain(literal, assumptions); - explain(neg_literal, assumptions); + explain(negLiteral, assumptions); d_conflictNode = mkAnd(assumptions); d_conflict = true; - return; + return; } BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): " << literal << std::endl; @@ -299,10 +284,8 @@ void TheoryBV::propagate(Effort e) { Node negatedLiteral; std::vector<TNode> assumptions; - if (normalized != d_false) { negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); assumptions.push_back(negatedLiteral); - } explain(literal, assumptions); d_conflictNode = mkAnd(assumptions); d_conflict = true; @@ -352,8 +335,6 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) // If propagated already, just skip PropagatedMap::const_iterator find = d_propagatedBy.find(literal); if (find != d_propagatedBy.end()) { - //unsigned theories = (*find).second | (unsigned) subtheory; - //d_propagatedBy[literal] = theories; return true; } else { d_propagatedBy[literal] = subtheory; @@ -362,56 +343,37 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) // See if the literal has been asserted already bool satValue = false; bool hasSatValue = d_valuation.hasSatValue(literal, satValue); - // If asserted, we might be in conflict + // If asserted, we might be in conflict if (hasSatValue && !satValue) { - Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl; - std::vector<TNode> assumptions; - Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); - assumptions.push_back(negatedLiteral); - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - return false; + Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl; + std::vector<TNode> assumptions; + Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); + assumptions.push_back(negatedLiteral); + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + return false; } // Nothing, just enqueue it for propagation and mark it as asserted already Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => enqueuing for propagation" << std::endl; d_literalsToPropagate.push_back(literal); + // No conflict return true; }/* TheoryBV::propagate(TNode) */ void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) { - if (propagatedBy(literal, SUB_EQUALITY)) { - TNode lhs, rhs; - switch (literal.getKind()) { - case kind::EQUAL: - lhs = literal[0]; - rhs = literal[1]; - break; - case kind::NOT: - if (literal[0].getKind() == kind::EQUAL) { - // Disequalities - d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); - return; - } else { - // Predicates - lhs = literal[0]; - rhs = d_false; - break; - } - case kind::CONST_BOOLEAN: - // we get to explain true = false, since we set false to be the trigger of this - lhs = d_true; - rhs = d_false; - break; - default: - Unreachable(); + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + if (atom.getKind() == kind::EQUAL) { + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + } else { + d_equalityEngine.explainPredicate(atom, polarity, assumptions); } - d_equalityEngine.explainEquality(lhs, rhs, assumptions); } else { Assert(propagatedBy(literal, SUB_BITBLASTER)); d_bitblaster->explain(literal, assumptions); @@ -430,7 +392,9 @@ Node TheoryBV::explain(TNode node) { return utils::mkTrue(); } // return the explanation - return mkAnd(assumptions); + Node explanation = mkAnd(assumptions); + Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl; + return explanation; } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 0ced179ec..e46d052f8 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -61,8 +61,6 @@ private: /** Bitblaster */ Bitblaster* d_bitblaster; - Node d_true; - Node d_false; /** Context dependent set of atoms we already propagated */ context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet; @@ -99,22 +97,44 @@ private: // Added by Clark // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module - class NotifyClass { + class NotifyClass : public eq::EqualityEngineNotify { + TheoryBV& d_bv; + public: + NotifyClass(TheoryBV& uf): d_bv(uf) {} - bool notify(TNode propagation) { - Debug("bitvector") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; - // Just forward to bv - return d_bv.storePropagation(propagation, SUB_EQUALITY); + bool eqNotifyTriggerEquality(TNode equality, bool value) { + Debug("bitvector") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; + if (value) { + return d_bv.storePropagation(equality, SUB_EQUALITY); + } else { + return d_bv.storePropagation(equality.notNode(), SUB_EQUALITY); + } + } + + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + Debug("bitvector") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl; + if (value) { + return d_bv.storePropagation(predicate, SUB_EQUALITY); + } else { + return d_bv.storePropagation(predicate, SUB_EQUALITY); + } + } + + bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) { + Debug("bitvector") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl; + if (value) { + return d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY); + } else { + return d_bv.storePropagation(t1.eqNode(t2).notNode(), SUB_EQUALITY); + } } - void notify(TNode t1, TNode t2) { - Debug("arrays") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; - // Propagate equality between shared terms - Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); - d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY); + bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { + Debug("bitvector") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; + return d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY); } }; @@ -122,7 +142,7 @@ private: NotifyClass d_notify; /** Equaltity engine */ - uf::EqualityEngine<NotifyClass> d_equalityEngine; + eq::EqualityEngine d_equalityEngine; // Are we in conflict? context::CDO<bool> d_conflict; |