From 2cf12a56cb9c5eb539d50a39b2764a292d6fd13f Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Tue, 13 Nov 2012 04:49:34 +0000 Subject: added support for division by zero for bit-vector division operators --- src/theory/bv/bitblast_strategies.cpp | 8 ++++---- src/theory/bv/bitblaster.cpp | 22 +++++++++++++++++----- src/theory/bv/bv_subtheory_eq.cpp | 16 +++++++++++++--- src/theory/bv/bv_subtheory_eq.h | 2 ++ src/theory/bv/kinds | 6 ++++++ .../theory_bv_rewrite_rules_constant_evaluation.h | 4 ++-- .../bv/theory_bv_rewrite_rules_simplification.h | 12 ++++++------ src/theory/bv/theory_bv_rewriter.cpp | 11 +++++++---- src/theory/bv/theory_bv_rewriter.h | 4 +++- 9 files changed, 60 insertions(+), 25 deletions(-) (limited to 'src/theory/bv') diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index d2fbb432b..fbf9a45ee 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -640,7 +640,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0); + Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0); Bits a, b; bb->bbTerm(node[0], a); @@ -650,13 +650,13 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { uDivModRec(a, b, q, r, getSize(node)); // cache the remainder in case we need it later - Node remainder = mkNode(kind::BITVECTOR_UREM, node[0], node[1]); + Node remainder = mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1]); bb->cacheTermDef(remainder, r); } void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0); + Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0); Bits a, b; bb->bbTerm(node[0], a); @@ -666,7 +666,7 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { uDivModRec(a, b, q, rem, getSize(node)); // cache the quotient in case we need it later - Node quotient = mkNode(kind::BITVECTOR_UDIV, node[0], node[1]); + Node quotient = mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]); bb->cacheTermDef(quotient, q); } diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 41d98326e..aca81e176 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -214,6 +214,13 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) { */ bool Bitblaster::solve(bool quick_solve) { + if (Trace.isOn("bitvector")) { + Trace("bitvector") << "Bitblaster::solve() asserted atoms "; + context::CDList::const_iterator it = d_assertedAtoms.begin(); + for (; it != d_assertedAtoms.end(); ++it) { + Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; + } + } BVDebug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; return SAT_VALUE_TRUE == d_satSolver->solve(); } @@ -280,11 +287,13 @@ void Bitblaster::initTermBBStrategies() { d_termBBStrategies [ kind::BITVECTOR_PLUS ] = DefaultPlusBB; d_termBBStrategies [ kind::BITVECTOR_SUB ] = DefaultSubBB; d_termBBStrategies [ kind::BITVECTOR_NEG ] = DefaultNegBB; - d_termBBStrategies [ kind::BITVECTOR_UDIV ] = DefaultUdivBB; - d_termBBStrategies [ kind::BITVECTOR_UREM ] = DefaultUremBB; - d_termBBStrategies [ kind::BITVECTOR_SDIV ] = DefaultSdivBB; - d_termBBStrategies [ kind::BITVECTOR_SREM ] = DefaultSremBB; - d_termBBStrategies [ kind::BITVECTOR_SMOD ] = DefaultSmodBB; + d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ] = DefaultUdivBB; + d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ] = DefaultUremBB; + d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy; d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB; d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB; d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB; @@ -429,6 +438,9 @@ void Bitblaster::collectModelInfo(TheoryModel* m) { TNode var = *it; if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { Node const_value = getVarValue(var); + Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; m->assertEquality(var, const_value, true); } } diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp index 17f3acdd1..e809a2566 100644 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -28,7 +28,8 @@ using namespace CVC4::theory::bv::utils; EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), d_notify(*this), - d_equalityEngine(d_notify, c, "theory::bv::TheoryBV") + d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), + d_assertions(c) { if (d_useEqualityEngine) { @@ -87,14 +88,16 @@ void EqualitySolver::explain(TNode literal, std::vector& assumptions) { } bool EqualitySolver::addAssertions(const std::vector& assertions, Theory::Effort e) { - BVDebug("bitvector::equality") << "EqualitySolver::addAssertions \n"; + Trace("bitvector::equality") << "EqualitySolver::addAssertions \n"; Assert (!d_bv->inConflict()); for (unsigned i = 0; i < assertions.size(); ++i) { TNode fact = assertions[i]; - + // Notify the equality engine if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_EQUALITY) ) { + Trace("bitvector::equality") << " (assert " << fact << ")\n"; + d_assertions.push_back(fact); bool negated = fact.getKind() == kind::NOT; TNode predicate = negated ? fact[0] : fact; if (predicate.getKind() == kind::EQUAL) { @@ -164,5 +167,12 @@ void EqualitySolver::conflict(TNode a, TNode b) { } void EqualitySolver::collectModelInfo(TheoryModel* m) { + if (Debug.isOn("bitvector-model")) { + context::CDList::const_iterator it = d_assertions.begin(); + for (; it!= d_assertions.end(); ++it) { + Debug("bitvector-model") << "EqualitySolver::collectModelInfo (assert " + << *it << ")\n"; + } + } m->assertEqualityEngine(&d_equalityEngine); } diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h index 91ad1599b..64fe12706 100644 --- a/src/theory/bv/bv_subtheory_eq.h +++ b/src/theory/bv/bv_subtheory_eq.h @@ -58,6 +58,8 @@ class EqualitySolver : public SubtheorySolver { /** Store a conflict from merging two constants */ void conflict(TNode a, TNode b); + /** FIXME: for debugging purposes only */ + context::CDList d_assertions; public: EqualitySolver(context::Context* c, TheoryBV* bv); diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 9dc2e66bb..2faa12437 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -54,6 +54,10 @@ operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating divisio operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division" operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)" operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)" +# total division kinds +operator BITVECTOR_UDIV_TOTAL 2 "bit-vector total unsigned division, truncating towards 0 (undefined if divisor is 0)" +operator BITVECTOR_UREM_TOTAL 2 "bit-vector total unsigned remainder from truncating division (undefined if divisor is 0)" + operator BITVECTOR_SHL 2 "bit-vector left shift" operator BITVECTOR_LSHR 2 "bit-vector logical shift right" operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right" @@ -135,6 +139,8 @@ typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_UDIV_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_UREM_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index d7d7c9670..8b080d104 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -198,7 +198,7 @@ Node RewriteRule::apply(TNode node) { } template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV && + return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && utils::isBVGroundTerm(node)); } @@ -213,7 +213,7 @@ Node RewriteRule::apply(TNode node) { } template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM && + return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && utils::isBVGroundTerm(node)); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index a2fd9ee19..23cd8381d 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -752,7 +752,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV && + return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && utils::isPow2Const(node[1])); } @@ -776,7 +776,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV && + return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && node[1] == utils::mkConst(utils::getSize(node), 1)); } @@ -794,7 +794,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV && + return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && node[0] == node[1]); } @@ -812,7 +812,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM && + return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && utils::isPow2Const(node[1])); } @@ -837,7 +837,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM && + return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && node[1] == utils::mkConst(utils::getSize(node), 1)); } @@ -855,7 +855,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM && + return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && node[0] == node[1]); } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index a8941aac2..1335f8f4a 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -365,7 +365,8 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool preregister){ + +RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool preregister){ Node resultNode = node; if(RewriteRule::applies(node)) { @@ -382,7 +383,7 @@ RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool preregister){ return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool preregister) { Node resultNode = node; if(RewriteRule::applies(node)) { @@ -575,8 +576,10 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_PLUS ] = RewritePlus; d_rewriteTable [ kind::BITVECTOR_SUB ] = RewriteSub; d_rewriteTable [ kind::BITVECTOR_NEG ] = RewriteNeg; - d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv; - d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem; + // d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv; + // d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem; + d_rewriteTable [ kind::BITVECTOR_UDIV_TOTAL ] = RewriteUdivTotal; + d_rewriteTable [ kind::BITVECTOR_UREM_TOTAL ] = RewriteUremTotal; d_rewriteTable [ kind::BITVECTOR_SMOD ] = RewriteSmod; d_rewriteTable [ kind::BITVECTOR_SDIV ] = RewriteSdiv; d_rewriteTable [ kind::BITVECTOR_SREM ] = RewriteSrem; diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index c50a3bbe0..59a2f90f6 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -39,7 +39,7 @@ class TheoryBVRewriter { static void initializeRewrites(); - static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false); + static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false); static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false); static RewriteResponse RewriteSlt(TNode node, bool prerewrite = false); static RewriteResponse RewriteUle(TNode node, bool prerewrite = false); @@ -63,6 +63,8 @@ class TheoryBVRewriter { static RewriteResponse RewriteNeg(TNode node, bool prerewrite = false); static RewriteResponse RewriteUdiv(TNode node, bool prerewrite = false); static RewriteResponse RewriteUrem(TNode node, bool prerewrite = false); + static RewriteResponse RewriteUdivTotal(TNode node, bool prerewrite = false); + static RewriteResponse RewriteUremTotal(TNode node, bool prerewrite = false); static RewriteResponse RewriteSmod(TNode node, bool prerewrite = false); static RewriteResponse RewriteSdiv(TNode node, bool prerewrite = false); static RewriteResponse RewriteSrem(TNode node, bool prerewrite = false); -- cgit v1.2.3