From: Morgan Deters Date: Tue, 16 Jul 2013 21:29:30 +0000 (-0400) Subject: Minor bugfixes to model-building X-Git-Tag: cvc5-1.0.0~7287^2~63 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eb49fadc8cb3e8b8d865279ca532ee58efd77ffe;p=cvc5.git Minor bugfixes to model-building --- 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::apply(TNode node) { } template<> inline bool RewriteRule::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::apply(TNode node) { } template<> inline bool RewriteRule::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().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().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; diff --git a/src/theory/model.cpp b/src/theory/model.cpp index b10c85cfe..75187b7bd 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -53,6 +53,8 @@ Node TheoryModel::getValue( TNode n ) const{ Node nn = d_substitutions.apply( n ); //get value in model nn = getModelValue( nn ); + //normalize + nn = Rewriter::rewrite(nn); Assert(nn.isConst() || nn.getKind() == kind::LAMBDA); return nn; }