Fixed bug 338:

   - fixed buggy rewrite rules assuming certain nodes only had 2 children
   - added support for bv-rewrite dump
   - fixed smt2_printer for bv constants
  

2 files changed, 34 insertions, 12 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 30437a76e..343d4d1f1 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -24,6 +24,7 @@
 #include "context/context.h"
 #include "util/stats.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "expr/command.h"
 #include <sstream>
 
 namespace CVC4 {
@@ -345,6 +346,23 @@ public:
       Assert(checkApplies || applies(node));
       //++ s_statistics->d_ruleApplications;
       Node result = apply(node);
+      if (result != node) {
+        if(Dump.isOn("bv-rewrites")) {
+          std::ostringstream os;
+          os << "RewriteRule <"<<rule<<">; expect unsat";
+
+          Node condition;
+          if (result.getType().isBoolean()) {
+            condition = node.iffNode(result).notNode();
+          } else {
+            condition = node.eqNode(result).notNode();
+          }
+
+          Dump("bv-rewrites")
+            << CommentCommand(os.str())
+            << CheckSatCommand(condition.toExpr());
+        }
+      }
       BVDebug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
       return result;
     } else {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index da3fb6554..3a5a07f1c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -46,10 +46,12 @@ Node RewriteRule<ExtractBitwise>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl;
   unsigned high = utils::getExtractHigh(node);
   unsigned low = utils::getExtractLow(node);
-  Node a = utils::mkExtract(node[0][0], high, low);
-  Node b = utils::mkExtract(node[0][1], high, low);
+  std::vector<Node> children; 
+  for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
+    children.push_back(utils::mkExtract(node[0][i], high, low)); 
+  }
   Kind kind = node[0].getKind(); 
-  return utils::mkNode(kind, a, b);
+  return utils::mkSortedNode(kind, children);
 }
 
 /**
@@ -92,11 +94,12 @@ Node RewriteRule<ExtractArith>::apply(Node node) {
   unsigned low = utils::getExtractLow(node);
   Assert (low == 0); 
   unsigned high = utils::getExtractHigh(node);
-  Node a = utils::mkExtract(node[0][0], high, low);
-  Node b = utils::mkExtract(node[0][1], high, low);
-  
+  std::vector<Node> children;
+  for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
+    children.push_back(utils::mkExtract(node[0][i], high, low)); 
+  }
   Kind kind = node[0].getKind(); 
-  return utils::mkNode(kind, a, b); 
+  return utils::mkNode(kind, children); 
   
 }
 
@@ -119,13 +122,14 @@ Node RewriteRule<ExtractArith2>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" << std::endl;
   unsigned low = utils::getExtractLow(node);
   unsigned high = utils::getExtractHigh(node);
-  Node a = utils::mkExtract(node[0][0], high, 0);
-  Node b = utils::mkExtract(node[0][1], high, 0);
-  
+  std::vector<Node> children;
+  for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
+    children.push_back(utils::mkExtract(node[0][i], high, 0)); 
+  }
   Kind kind = node[0].getKind(); 
-  Node a_op_b = utils::mkNode(kind, a, b); 
+  Node op_children = utils::mkSortedNode(kind, children); 
   
-  return utils::mkExtract(a_op_b, high, low); 
+  return utils::mkExtract(op_children, high, low); 
 }
 
 template<> inline