From: lianah Date: Thu, 25 Apr 2013 22:43:12 +0000 (-0400) Subject: added bvule, bvsle operator elimination rulesl; added bvurem lemma generation X-Git-Tag: cvc5-1.0.0~7297 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=94dc66d4cb4061a80bffe1ec72d2ab98e44dd626;p=cvc5.git added bvule, bvsle operator elimination rulesl; added bvurem lemma generation --- diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 6bbe4bb3e..ab25fa6cb 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -106,6 +106,7 @@ SatValue BVMinisatSatSolver::solve(){ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; + ++d_statistics.d_statCallsToSolve; if(resource == 0) { d_minisat->budgetOff(); } else { 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 326eab36a..953f9b3e5 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), @@ -125,6 +126,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"; @@ -144,8 +167,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 481493e13..22e3d0507 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -85,6 +85,8 @@ private: Statistics d_statistics; + context::CDO d_lemmasAdded; + // Are we in conflict? context::CDO d_conflict; @@ -97,6 +99,8 @@ private: /** Index of the next literal to propagate */ context::CDO d_literalsToPropagateIndex; + + /** * Keeps a map from nodes to the subtheory that propagated it so that we can explain it * properly. @@ -147,7 +151,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::apply(TNode node) { return result; } + template <> bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLT); @@ -136,6 +137,21 @@ Node RewriteRule::apply(TNode node) { return utils::mkNode(kind::NOT, b_slt_a); } +template <> +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULE); +} + +template <> +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << 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::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, // if both arguments are constants evaluates - RewriteRule, + RewriteRule // a < 0 rewrites to false - RewriteRule, - RewriteRule + // RewriteRule, + // RewriteRule >::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, RewriteRule, RewriteRule, - RewriteRule + RewriteRule, + RewriteRule >::apply(node); return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); } RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy - < RewriteRule , + < RewriteRule , RewriteRule >::apply(node); - - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode); } RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){