From 1ce0650dcf8ce30424b546deb540974cc510c215 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Wed, 9 May 2012 21:25:17 +0000 Subject: * 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 --- src/theory/bv/theory_bv.cpp | 90 ++++++++++++++------------------------------- 1 file changed, 27 insertions(+), 63 deletions(-) (limited to 'src/theory/bv/theory_bv.cpp') 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 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 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 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 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& 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; } -- cgit v1.2.3