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
  

4 files changed, 44 insertions, 17 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2b686441a..25d3bf35a 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -85,11 +85,15 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     case kind::CONST_BITVECTOR: {
       const BitVector& bv = n.getConst<BitVector>();
       const Integer& x = bv.getValue();
-      out << "#b";
       unsigned n = bv.getSize();
-      while(n-- > 0) {
-        out << (x.testBit(n) ? '1' : '0');
-      }
+      out << "(_ ";
+      out << "bv" << x <<" " << n; 
+      out << ")"; 
+      // //out << "#b";
+
+      // while(n-- > 0) {
+      //   out << (x.testBit(n) ? '1' : '0');
+      // }
       break;
     }
     case kind::CONST_BOOLEAN:
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
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 36033db0b..e41959da2 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -619,7 +619,8 @@ throw(OptionException) {
         } else if(!strcmp(optarg, "clauses")) {
         } else if(!strcmp(optarg, "t-conflicts") ||
                   !strcmp(optarg, "t-lemmas") ||
-                  !strcmp(optarg, "t-explanations")) {
+                  !strcmp(optarg, "t-explanations") ||
+                  !strcmp(optarg, "bv-rewrites")) {
           // These are "non-state-dumping" modes.  If state (SAT decisions,
           // propagations, etc.) is dumped, it will interfere with the validity
           // of these generated queries.