diff options
author | lianah <lianahady@gmail.com> | 2013-04-25 18:43:12 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-25 18:43:12 -0400 |
commit | c2cf8201afa6b44a5d3103cf8938eccb69cec590 (patch) | |
tree | f50f20fd6f24a9cc796d64f0b20efb9487483a0f /src/theory/bv | |
parent | 12f48b0a11207ddbd34b2b2b88362250e9692ac2 (diff) |
added bvule, bvsle operator elimination rulesl; added bvurem lemma generation
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bv_to_bool.cpp | 19 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 29 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 5 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 16 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 18 |
6 files changed, 78 insertions, 17 deletions
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 8084a7282..7bec805ef 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -44,8 +44,11 @@ void BvToBoolVisitor::start(TNode node) {} void BvToBoolVisitor::storeBvToBool(TNode bv_term, TNode bool_term) { Assert (bv_term.getType().isBitVector() && - bv_term.getType().getBitVectorSize() == 1); - Assert (bool_term.getType().isBoolean() && d_bvToBoolMap.find(bv_term) == d_bvToBoolMap.end()); + bv_term.getType().getBitVectorSize() == 1 && + bool_term.getType().isBoolean() && bv_term != Node() && bool_term != Node()); + if (d_bvToBoolMap.find(bv_term) != d_bvToBoolMap.end()) { + Assert (d_bvToBoolMap[bv_term] == bool_term); + } d_bvToBoolMap[bv_term] = bool_term; } @@ -75,9 +78,10 @@ bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) { return true; } - Kind kind = node.getKind(); if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1) return false; + + Kind kind = node.getKind(); if (kind == kind::CONST_BITVECTOR) { return true; @@ -95,6 +99,10 @@ bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) { } return true; } + if (kind == kind::VARIABLE) { + storeBvToBool(node, utils::mkNode(kind::EQUAL, node, utils::mkConst(BitVector(1, 1u)))); + return true; + } return false; } @@ -226,7 +234,8 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) { check(current, parent); if (isConvertibleBvAtom(current)) { - result = convertBvAtom(current); + result = convertBvAtom(current); + addToCache(current, result); } else if (isConvertibleBvTerm(current)) { result = convertBvTerm(current); } else { @@ -244,10 +253,10 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) { } result = builder; } + addToCache(current, result); } Assert (result != Node()); Debug("bv-to-bool") << " =>" << result <<"\n"; - addToCache(current, result); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 7cb06ca15..bd7d4c70b 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -43,6 +43,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_subtheories(), d_subtheoryMap(), d_statistics(), + d_lemmasAdded(c, false), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), @@ -122,6 +123,28 @@ void TheoryBV::sendConflict() { } } +void TheoryBV::checkForLemma(TNode fact) { + if (fact.getKind() == kind::EQUAL) { + if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) { + TNode urem = fact[0]; + TNode result = fact[1]; + TNode divisor = urem[1]; + Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor); + Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div); + lemma(split); + } + if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) { + TNode urem = fact[1]; + TNode result = fact[0]; + TNode divisor = urem[1]; + Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor); + Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div); + lemma(split); + } + } +} + + void TheoryBV::check(Effort e) { Trace("bitvector") <<"TheoryBV::check (" << e << ")\n"; @@ -141,8 +164,14 @@ void TheoryBV::check(Effort e) return; } + if (Theory::fullEffort(e)) { + Trace("bitvector-fulleffort") << "TheoryBV::fullEffort \n"; + printFacts( Trace("bitvector-fulleffort") ); + } + while (!done()) { TNode fact = get().assertion; + checkForLemma(fact); for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->assertFact(fact); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 8b184f972..827b6e878 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -84,6 +84,8 @@ private: Statistics d_statistics; + context::CDO<bool> d_lemmasAdded; + // Are we in conflict? context::CDO<bool> d_conflict; @@ -96,6 +98,8 @@ private: /** Index of the next literal to propagate */ context::CDO<unsigned> d_literalsToPropagateIndex; + + /** * Keeps a map from nodes to the subtheory that propagated it so that we can explain it * properly. @@ -146,7 +150,9 @@ private: void sendConflict(); - void lemma(TNode node) { d_out->lemma(node); } + void lemma(TNode node) { d_out->lemma(node); d_lemmasAdded = true; } + + void checkForLemma(TNode node); friend class Bitblaster; friend class BitblastSolver; diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index cff85b92b..d362fa603 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -152,7 +152,7 @@ enum RewriteRuleId { AndSimplify, OrSimplify, XorSimplify, - + UleEliminate, // rules to simplify bitblasting BBPlusNeg }; @@ -269,7 +269,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case BBPlusNeg : out << "BBPlusNeg"; return out; case UltOne : out << "UltOne"; return out; case SltZero : out << "SltZero"; return out; - case ZeroUlt : out << "ZeroUlt"; return out; + case ZeroUlt : out << "ZeroUlt"; return out; + case UleEliminate : out << "UleEliminate"; return out; default: Unreachable(); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index b466aceae..a63721de1 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -85,6 +85,7 @@ Node RewriteRule<SgeEliminate>::apply(TNode node) { return result; } + template <> bool RewriteRule<SltEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLT); @@ -136,6 +137,21 @@ Node RewriteRule<SleEliminate>::apply(TNode node) { return utils::mkNode(kind::NOT, b_slt_a); } +template <> +bool RewriteRule<UleEliminate>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULE); +} + +template <> +Node RewriteRule<UleEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<UleEliminate>(" << node << ")" << std::endl; + + TNode a = node[0]; + TNode b = node[1]; + Node b_ult_a = utils::mkNode(kind::BITVECTOR_ULT, b, a); + return utils::mkNode(kind::NOT, b_ult_a); +} + template <> bool RewriteRule<CompEliminate>::applies(TNode node) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 07499d01a..f6d138f5d 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -75,10 +75,10 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<EvalUlt>, // if both arguments are constants evaluates - RewriteRule<UltZero>, + RewriteRule<UltZero> // a < 0 rewrites to false - RewriteRule<UltOne>, - RewriteRule<ZeroUlt> + // RewriteRule<UltOne>, + // RewriteRule<ZeroUlt> >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); @@ -86,8 +86,8 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy - < RewriteRule < EvalSlt >, - RewriteRule < SltZero > + < RewriteRule < EvalSlt > + // RewriteRule < SltZero > >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); @@ -106,18 +106,18 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){ RewriteRule<UleMax>, RewriteRule<ZeroUle>, RewriteRule<UleZero>, - RewriteRule<UleSelf> + RewriteRule<UleSelf>, + RewriteRule<UleEliminate> >::apply(node); return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); } RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy - < RewriteRule <EvalSle>, + < RewriteRule <EvalSle>, RewriteRule <SleEliminate> >::apply(node); - - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode); } RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){ |