From eb49fadc8cb3e8b8d865279ca532ee58efd77ffe Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 16 Jul 2013 17:29:30 -0400
Subject: [PATCH] Minor bugfixes to model-building

---
 ...ory_bv_rewrite_rules_constant_evaluation.h | 10 ++++----
 src/theory/bv/theory_bv_rewriter.cpp          | 23 +++++++++++++++++--
 src/theory/model.cpp                          |  2 ++
 3 files changed, 29 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;
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;
 }
-- 
2.30.2