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 a5368d2c9ca7f729897867f1ffe629fd5a0b6700..9f3d12415dc96d98bd3b7708e32473ccee75dace 100644 (file)
--- 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 534347c4ae7e8ce907f842d4eaec0e894c248991..f698ec83df6af2e487707ffb7efddc35f01dbaa6 100644 (file)
--- 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;

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index b10c85cfe82d292807bdcdb778f97cdc67fdd2e5..75187b7bd3312e2cc720e3b0ec3a89ab2841541f 100644 (file)
--- 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;
 }