diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
commit | d01d291be3213368985f28d0072905c4f033d5ff (patch) | |
tree | 8524a2b6a00c012221ecca9266c3ab9fb11989ed /src/theory/bv | |
parent | 889853e225687dfef36b15ca1dccf74682e0fd66 (diff) |
merge from arrays-clark branch
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_sat.cpp | 9 | ||||
-rw-r--r-- | src/theory/bv/bv_sat.h | 5 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 315 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 69 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 23 |
7 files changed, 386 insertions, 40 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index edaf8c154..b579122e5 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -338,7 +338,7 @@ void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) { } void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) { - Assert (node.getKind() == kind::VARIABLE); + // Assert (node.getKind() == kind::VARIABLE); Assert(bits.size() == 0); for (unsigned i = 0; i < utils::getSize(node); ++i) { diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp index f5c43688a..2f4ac1324 100644 --- a/src/theory/bv/bv_sat.cpp +++ b/src/theory/bv/bv_sat.cpp @@ -83,6 +83,9 @@ void Bitblaster::bbAtom(TNode node) { return; } + // make sure it is marked as an atom + addAtom(node); + BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numAtoms; // the bitblasted definition of the atom @@ -298,12 +301,14 @@ void Bitblaster::initAtomBBStrategies() { } void Bitblaster::initTermBBStrategies() { + // Changed this to DefaultVarBB because any foreign kind should be treated as a variable + // TODO: check this is OK for (int i = 0 ; i < kind::LAST_KIND; ++i ) { - d_termBBStrategies[i] = UndefinedTermBBStrategy; + d_termBBStrategies[i] = DefaultVarBB; } /// setting default bb strategies for terms: - d_termBBStrategies [ kind::VARIABLE ] = DefaultVarBB; + // d_termBBStrategies [ kind::VARIABLE ] = DefaultVarBB; d_termBBStrategies [ kind::CONST_BITVECTOR ] = DefaultConstBB; d_termBBStrategies [ kind::BITVECTOR_NOT ] = DefaultNotBB; d_termBBStrategies [ kind::BITVECTOR_CONCAT ] = DefaultConcatBB; diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index 647e4fe9f..2422da0b7 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -82,7 +82,9 @@ class Bitblaster { currently asserted by the DPLL SAT solver. */ /// helper methods + public: bool hasBBAtom(TNode node); + private: bool hasBBTerm(TNode node); void getBBTerm(TNode node, Bits& bits); @@ -101,6 +103,7 @@ class Bitblaster { Node bbOptimize(TNode node); void bbAtom(TNode node); + void addAtom(TNode atom); // division is bitblasted in terms of constraints // so it needs to use private bitblaster interface void bbUdiv(TNode node, Bits& bits); @@ -116,7 +119,7 @@ public: bool solve(bool quick_solve = false); void bitblast(TNode node); void getConflict(std::vector<TNode>& conflict); - void addAtom(TNode atom); + bool getPropagations(std::vector<TNode>& propagations); void explainPropagation(TNode atom, std::vector<Node>& explanation); private: diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 429e5ff19..a3f4364ba 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -20,8 +20,8 @@ #include "theory/bv/theory_bv.h" #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; @@ -31,16 +31,67 @@ using namespace CVC4::context; using namespace std; using namespace CVC4::theory::bv::utils; + +const bool d_useEqualityEngine = true; +const bool d_useSatPropagation = true; + + TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : Theory(THEORY_BV, c, u, out, valuation), d_context(c), d_assertions(c), d_bitblaster(new Bitblaster(c) ), d_statistics(), - d_alreadyPropagatedSet(c) - { + d_alreadyPropagatedSet(c), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), + d_conflict(c, false), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_toBitBlast(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); + + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); + + } } + TheoryBV::~TheoryBV() { delete d_bitblaster; } @@ -68,32 +119,99 @@ void TheoryBV::preRegisterTerm(TNode node) { node.getKind() == kind::BITVECTOR_SLT || node.getKind() == kind::BITVECTOR_SLE) { d_bitblaster->bitblast(node); - d_bitblaster->addAtom(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()); + break; + default: + d_equalityEngine.addTerm(node); + break; + } + } + } -void TheoryBV::check(Effort e) { - BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; +void TheoryBV::check(Effort e) +{ + BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl; - while (!done()) { - TNode assertion = get(); - // make sure we do not assert things we propagated - if (!hasBeenPropagated(assertion)) { - BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n"; - bool ok = d_bitblaster->assertToSat(assertion, true); + while (!done() && !d_conflict) { + Assertion assertion = get(); + TNode fact = assertion.assertion; + + BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; + + // If the assertion doesn't have a literal, it's a shared equality + bool shared = !assertion.isPreregistered; + Assert(!d_useEqualityEngine || !shared || + ((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])))); + + // Notify the Equality Engine + switch (fact.getKind()) { + case kind::EQUAL: + if (d_useEqualityEngine) { + d_equalityEngine.addEquality(fact[0], fact[1], fact); + } + if (shared && !d_bitblaster->hasBBAtom(fact)) { + d_bitblaster->bitblast(fact); + } + break; + case kind::NOT: + if (fact[0].getKind() == kind::EQUAL) { + // Assert the dis-equality + if (d_useEqualityEngine) { + d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact); + } + if (shared && !d_bitblaster->hasBBAtom(fact[0])) { + d_bitblaster->bitblast(fact[0]); + } + } else { + if (d_useEqualityEngine) { + d_equalityEngine.addPredicate(fact[0], false, fact); + } + break; + } + break; + default: + if (d_useEqualityEngine) { + d_equalityEngine.addPredicate(fact, true, fact); + } + break; + } + + // make sure we do not assert things we propagated + if (!d_conflict && d_alreadyPropagatedSet.count(fact) == 0) { + bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation); if (!ok) { std::vector<TNode> conflictAtoms; d_bitblaster->getConflict(conflictAtoms); d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size()); - Node conflict = mkConjunction(conflictAtoms); - d_out->conflict(conflict); - BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n "; - return; + d_conflict = true; + d_conflictNode = mkConjunction(conflictAtoms); + break; } } } + // If in conflict, output the conflict + if (d_conflict) { + Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl; + d_out->conflict(d_conflictNode); + return; + } + if (e == EFFORT_FULL) { + + Assert(done() && !d_conflict); BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; // in standard effort we only do boolean constraint propagation bool ok = d_bitblaster->solve(false); @@ -127,12 +245,36 @@ Node TheoryBV::getValue(TNode n) { } } -bool TheoryBV::hasBeenPropagated(TNode node) { - return d_alreadyPropagatedSet.count(node); -} void TheoryBV::propagate(Effort e) { - BVDebug("bitvector") << "TheoryBV::propagate() \n"; + BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate()" << std::endl; + + if (d_conflict) { + return; + } + + // get new propagations from the equality engine + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { + TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; + BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl; + bool satValue; + Node normalized = Rewriter::rewrite(literal); + if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { + d_out->propagate(literal); + } else { + Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; + 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; + return; + } + } // get new propagations from the sat solver std::vector<TNode> propagations; @@ -142,6 +284,10 @@ void TheoryBV::propagate(Effort e) { for (unsigned i = 0; i < propagations.size(); ++ i) { TNode node = propagations[i]; BVDebug("bitvector") << "TheoryBV::propagate " << node <<" \n"; + if (!d_valuation.isSatLiteral(node)) { + // TODO: maybe propagate shared terms too? + continue; + } if (d_valuation.getSatValue(node) == Node::null()) { vector<Node> explanation; d_bitblaster->explainPropagation(node, explanation); @@ -162,21 +308,21 @@ void TheoryBV::propagate(Effort e) { } -Node TheoryBV::explain(TNode n) { - BVDebug("bitvector") << "TheoryBV::explain node " << n <<"\n"; - std::vector<Node> explanation; - d_bitblaster->explainPropagation(n, explanation); - Node exp; +// Node TheoryBV::explain(TNode n) { +// BVDebug("bitvector") << "TheoryBV::explain node " << n <<"\n"; +// std::vector<Node> explanation; +// d_bitblaster->explainPropagation(n, explanation); +// Node exp; - if (explanation.size() == 0) { - return utils::mkTrue(); - } +// if (explanation.size() == 0) { +// return utils::mkTrue(); +// } - exp = utils::mkAnd(explanation); +// exp = utils::mkAnd(explanation); - BVDebug("bitvector") << "TheoryBV::explain with " << exp <<"\n"; - return exp; -} +// BVDebug("bitvector") << "TheoryBV::explain with " << exp <<"\n"; +// return exp; +// } Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { switch(in.getKind()) { @@ -203,3 +349,108 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu } return PP_ASSERT_STATUS_UNSOLVED; } + + +bool TheoryBV::propagate(TNode literal) +{ + Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl; + + // If already in conflict, no more propagation + if (d_conflict) { + Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl; + 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 might be in conflict + if (isAsserted) { + if (!satValue) { + Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; + std::vector<TNode> assumptions; + Node negatedLiteral; + 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; + 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!) + } + + // Nothing, just enqueue it for propagation and mark it as asserted already + Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl; + d_literalsToPropagate.push_back(literal); + + return true; +}/* TheoryBV::propagate(TNode) */ + + +void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) { + 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(); + } + d_equalityEngine.explainEquality(lhs, rhs, assumptions); +} + + +Node TheoryBV::explain(TNode node) { + BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; + std::vector<TNode> assumptions; + explain(node, assumptions); + return mkAnd(assumptions); +} + + +void TheoryBV::addSharedTerm(TNode t) { + Debug("bitvector::sharing") << spaces(getContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; + if (d_useEqualityEngine) { + d_equalityEngine.addTriggerTerm(t); + } +} + + +EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) +{ + if (d_useEqualityEngine) { + if (d_equalityEngine.areEqual(a, b)) { + // The terms are implied to be equal + return EQUALITY_TRUE; + } + if (d_equalityEngine.areDisequal(a, b)) { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; + } + } + return EQUALITY_UNKNOWN; +} + diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index d147c8bb5..940eaef56 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -27,6 +27,8 @@ #include "context/cdhashset.h" #include "theory/bv/theory_bv_utils.h" #include "util/stats.h" +#include "theory/uf/equality_engine.h" +#include "context/cdqueue.h" namespace BVMinisat { class SimpSolver; @@ -40,6 +42,12 @@ namespace bv { /// forward declarations class Bitblaster; +static inline std::string spaces(int level) +{ + std::string indentStr(level, ' '); + return indentStr; +} + class TheoryBV : public Theory { @@ -54,11 +62,11 @@ 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; - bool hasBeenPropagated(TNode node); public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); @@ -70,8 +78,6 @@ public: void check(Effort e); - void propagate(Effort e); - Node explain(TNode n); Node getValue(TNode n); @@ -93,6 +99,61 @@ private: Statistics d_statistics; + // Added by Clark + // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module + class NotifyClass { + TheoryBV& d_bv; + public: + NotifyClass(TheoryBV& uf): d_bv(uf) {} + + bool notify(TNode propagation) { + Debug("bitvector") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; + // Just forward to bv + return d_bv.propagate(propagation); + } + + void notify(TNode t1, TNode t2) { + Debug("arrays") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; + // Propagate equality between shared terms + Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); + d_bv.propagate(t1.eqNode(t2)); + } + }; + + /** The notify class for d_equalityEngine */ + NotifyClass d_notify; + + /** Equaltity engine */ + uf::EqualityEngine<NotifyClass> d_equalityEngine; + + // Are we in conflict? + context::CDO<bool> d_conflict; + + /** The conflict node */ + Node d_conflictNode; + + /** Literals to propagate */ + context::CDList<Node> d_literalsToPropagate; + + /** Index of the next literal to propagate */ + context::CDO<unsigned> d_literalsToPropagateIndex; + + context::CDQueue<Node> d_toBitBlast; + + /** Should be called to propagate the literal. */ + bool propagate(TNode literal); + + /** Explain why this literal is true by adding assumptions */ + void explain(TNode literal, std::vector<TNode>& assumptions); + + void addSharedTerm(TNode t); + + EqualityStatus getEqualityStatus(TNode a, TNode b); + +public: + + void propagate(Effort e); + };/* class TheoryBV */ }/* CVC4::theory::bv namespace */ diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index cf8310e5a..530949de2 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -866,6 +866,9 @@ Node RewriteRule<UremPow2>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl; TNode a = node[0]; unsigned power = utils::isPow2Const(node[1]) - 1; + if (power == 0) { + return utils::mkConst(utils::getSize(node), 0); + } Node extract = utils::mkExtract(a, power - 1, 0); Node zeros = utils::mkConst(utils::getSize(node) - power, 0); return utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract); diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 8b5dd0499..38547ad99 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -344,6 +344,29 @@ inline Node mkConjunction(const std::vector<TNode>& nodes) { } +inline Node mkAnd(const std::vector<TNode>& conjunctions) { + Assert(conjunctions.size() > 0); + + std::set<TNode> all; + all.insert(conjunctions.begin(), conjunctions.end()); + + if (all.size() == 1) { + // All the same, or just one + return conjunctions[0]; + } + + 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 conjunction; +}/* mkAnd() */ + + // Turn a set into a string inline std::string setToString(const std::set<TNode>& nodeSet) { std::stringstream out; |