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

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2b686441ab37e755716290c44cd30d1ace5ef381..25d3bf35a4390c60c42172d011de58e53e09eea5 100644 (file)
--- 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 30437a76e07aeee053f08faa6ed951a56d41b266..343d4d1f1f0f813b712f89fbdd63842bd40e21ed 100644 (file)
--- 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 da3fb65540969e78726d2bfd3e5d677a281f9f2b..3a5a07f1ca659f7a51bf0b4b6b72e73721898911 100644 (file)
--- 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 36033db0bb7369d8fec3d063bbc4386fba2c52c5..e41959da29534d7a4f35fb02ea7d5b954a187dda 100644 (file)
--- 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.

diff --git a/test/regress/regress0/aufbv/bug338.smt2 b/test/regress/regress0/aufbv/bug338.smt2
new file mode 100644 (file)
index 0000000..b245228
--- /dev/null
+++ b/test/regress/regress0/aufbv/bug338.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_AUFBV)
+(declare-sort U 0)
+(declare-sort Index 0)
+(declare-sort Element 0)
+(declare-fun memory_0 () (Array (_ BitVec 32) (_ BitVec 8)))
+(set-info :status sat)
+
+(set-info :notes "RewriteRule <ExtractBitwise>; expect unsat")
+
+(assert (not (= ((_ extract 7 0) (bvor (_ bv65536 32) (concat (_ bv0 25) ((_ extract 7 1) (select memory_0 (_ bv1 32)))) (concat (_ bv0 24) (select memory_0 (_ bv1 32))))) (bvor ((_ extract 7 0) (_ bv65536 32)) ((_ extract 7 0) (concat (_ bv0 25) ((_ extract 7 1) (select memory_0 (_ bv1 32)))))))))
+(check-sat)
+
+
+(exit)