diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-16 17:29:30 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-16 17:29:53 -0400 |
commit | eb49fadc8cb3e8b8d865279ca532ee58efd77ffe (patch) | |
tree | 9b2b9c3cc336abda606e0e951b3418afc223a313 /src/theory/bv | |
parent | 839920ac29df9cf5a8a231a3d66250a102821472 (diff) |
Minor bugfixes to model-building
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 23 |
2 files changed, 27 insertions, 6 deletions
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 a5368d2c9..9f3d12415 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -198,8 +198,9 @@ Node RewriteRule<EvalNeg>::apply(TNode node) { } template<> inline bool RewriteRule<EvalUdiv>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && - utils::isBVGroundTerm(node)); + return (utils::isBVGroundTerm(node) && + (node.getKind() == kind::BITVECTOR_UDIV_TOTAL || + (node.getKind() == kind::BITVECTOR_UDIV && node[1].isConst()))); } template<> inline @@ -213,8 +214,9 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) { } template<> inline bool RewriteRule<EvalUrem>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && - utils::isBVGroundTerm(node)); + return (utils::isBVGroundTerm(node) && + (node.getKind() == kind::BITVECTOR_UREM_TOTAL || + (node.getKind() == kind::BITVECTOR_UREM && node[1].isConst()))); } template<> inline diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 534347c4a..f698ec83d 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -394,6 +394,25 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) { return RewriteResponse(REWRITE_DONE, resultNode); } +RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool prerewrite){ + Node resultNode = node; + + if(node[1].isConst() && node[1].getConst<BitVector>().getValue() != 0) { + return RewriteUdivTotal(node, prerewrite); + } + + return RewriteResponse(REWRITE_DONE, resultNode); +} + +RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool prerewrite){ + Node resultNode = node; + + if(node[1].isConst() && node[1].getConst<BitVector>().getValue() != 0) { + return RewriteUremTotal(node, prerewrite); + } + + return RewriteResponse(REWRITE_DONE, resultNode); +} RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){ Node resultNode = node; @@ -605,8 +624,8 @@ 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; |