Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2

7 files changed, 99 insertions, 16 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 82f4779c6..8cbf99ae9 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -30,12 +30,15 @@ namespace bv {
 
 template<> inline
 bool RewriteRule<EvalAnd>::applies(TNode node) {
+  Unreachable();
   return (node.getKind() == kind::BITVECTOR_AND &&
+          node.getNumChildren() == 2 &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
 Node RewriteRule<EvalAnd>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -46,12 +49,15 @@ Node RewriteRule<EvalAnd>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<EvalOr>::applies(TNode node) {
+  Unreachable();
   return (node.getKind() == kind::BITVECTOR_OR &&
+          node.getNumChildren() == 2 &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
 Node RewriteRule<EvalOr>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -62,12 +68,15 @@ Node RewriteRule<EvalOr>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<EvalXor>::applies(TNode node) {
+  Unreachable();
   return (node.getKind() == kind::BITVECTOR_XOR &&
+          node.getNumChildren() == 2 &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
 Node RewriteRule<EvalXor>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -101,7 +110,7 @@ template<> inline
 Node RewriteRule<EvalNot>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
-  BitVector res = ~ a;  
+  BitVector res = ~ a;
   return utils::mkConst(res);
 }
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index d2cc7e05f..506570ed2 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -221,7 +221,8 @@ Node RewriteRule<RotateRightEliminate>::apply(TNode node) {
 
 template<>
 bool RewriteRule<NandEliminate>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_NAND);
+  return (node.getKind() == kind::BITVECTOR_NAND &&
+          node.getNumChildren() == 2);
 }
 
 template<>
@@ -236,7 +237,8 @@ Node RewriteRule<NandEliminate>::apply(TNode node) {
 
 template<>
 bool RewriteRule<NorEliminate>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_NOR);
+  return (node.getKind() == kind::BITVECTOR_NOR &&
+          node.getNumChildren() == 2);
 }
 
 template<>
@@ -251,7 +253,8 @@ Node RewriteRule<NorEliminate>::apply(TNode node) {
 
 template<>
 bool RewriteRule<XnorEliminate>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_XNOR);
+  return (node.getKind() == kind::BITVECTOR_XNOR &&
+          node.getNumChildren() == 2);
 }
 
 template<>
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 8e14980a7..272b56ae9 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -152,13 +152,16 @@ Node RewriteRule<AshrByConst>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<BitwiseIdemp>::applies(TNode node) {
+  Unreachable();
   return ((node.getKind() == kind::BITVECTOR_AND ||
            node.getKind() == kind::BITVECTOR_OR) &&
+          node.getNumChildren() == 2 &&
           node[0] == node[1]);
 }
 
 template<> inline
 Node RewriteRule<BitwiseIdemp>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
   return node[0]; 
 }
@@ -171,14 +174,17 @@ Node RewriteRule<BitwiseIdemp>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<AndZero>::applies(TNode node) {
+  Unreachable();
   unsigned size = utils::getSize(node); 
   return (node.getKind() == kind::BITVECTOR_AND  &&
+          node.getNumChildren() == 2 &&
           (node[0] == utils::mkConst(size, 0) ||
            node[1] == utils::mkConst(size, 0)));
 }
 
 template<> inline
 Node RewriteRule<AndZero>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
 }
@@ -191,15 +197,18 @@ Node RewriteRule<AndZero>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<AndOne>::applies(TNode node) {
+  Unreachable();
   unsigned size = utils::getSize(node);
   Node ones = utils::mkOnes(size); 
   return (node.getKind() == kind::BITVECTOR_AND  &&
+          node.getNumChildren() == 2 &&
           (node[0] == ones ||
            node[1] == ones));
 }
 
 template<> inline
 Node RewriteRule<AndOne>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
   unsigned size = utils::getSize(node);
   
@@ -219,14 +228,17 @@ Node RewriteRule<AndOne>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<OrZero>::applies(TNode node) {
+  Unreachable();
   unsigned size = utils::getSize(node); 
   return (node.getKind() == kind::BITVECTOR_OR  &&
+          node.getNumChildren() == 2 &&
           (node[0] == utils::mkConst(size, 0) ||
            node[1] == utils::mkConst(size, 0)));
 }
 
 template<> inline
 Node RewriteRule<OrZero>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
   
   unsigned size = utils::getSize(node); 
@@ -246,15 +258,18 @@ Node RewriteRule<OrZero>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<OrOne>::applies(TNode node) {
+  Unreachable();
   unsigned size = utils::getSize(node);
   Node ones = utils::mkOnes(size); 
   return (node.getKind() == kind::BITVECTOR_OR  &&
+          node.getNumChildren() == 2 &&
           (node[0] == ones ||
            node[1] == ones));
 }
 
 template<> inline
 Node RewriteRule<OrOne>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
   return utils::mkOnes(utils::getSize(node)); 
 }
@@ -268,12 +283,15 @@ Node RewriteRule<OrOne>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<XorDuplicate>::applies(TNode node) {
+  Unreachable();
   return (node.getKind() == kind::BITVECTOR_XOR &&
+          node.getNumChildren() == 2 &&
           node[0] == node[1]);
 }
 
 template<> inline
 Node RewriteRule<XorDuplicate>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
   return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); 
 }
@@ -367,13 +385,16 @@ Node RewriteRule<XorZero>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<BitwiseNotAnd>::applies(TNode node) {
+  Unreachable();
   return (node.getKind() == kind::BITVECTOR_AND &&
+          node.getNumChildren() == 2 &&
           ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
            (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0]))); 
 }
 
 template<> inline
 Node RewriteRule<BitwiseNotAnd>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
   return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); 
 }
@@ -386,13 +407,16 @@ Node RewriteRule<BitwiseNotAnd>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<BitwiseNotOr>::applies(TNode node) {
+  Unreachable();
   return (node.getKind() == kind::BITVECTOR_OR &&
+          node.getNumChildren() == 2 &&
           ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
            (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0]))); 
 }
 
 template<> inline
 Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
   uint32_t size = utils::getSize(node);
   Integer ones = Integer(1).multiplyByPow2(size) - 1; 
@@ -407,13 +431,16 @@ Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<XorNot>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_XOR &&
+  Unreachable();
+  if (node.getKind() == kind::BITVECTOR_XOR &&
+      node.getNumChildren() == 2 &&
           node[0].getKind() == kind::BITVECTOR_NOT &&
           node[1].getKind() == kind::BITVECTOR_NOT); 
 }
 
 template<> inline
 Node RewriteRule<XorNot>::apply(TNode node) {
+  Unreachable();
   BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
   Node a = node[0][0];
   Node b = node[1][0]; 
@@ -434,11 +461,14 @@ bool RewriteRule<NotXor>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<NotXor>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
-  Node a = node[0][0];
-  Node b = node[0][1];
-  Node nota = utils::mkNode(kind::BITVECTOR_NOT, a); 
-  return utils::mkSortedNode(kind::BITVECTOR_XOR, nota, b); 
+  BVDebug("bv-rewrite") << "RewriteRule<NotXor>(" << node << ")" << std::endl;
+  std::vector<Node> children;
+  TNode::iterator child_it = node[0].begin();
+  children.push_back(utils::mkNode(kind::BITVECTOR_NOT, *child_it));
+  for(++child_it; child_it != node[0].end(); ++child_it) {
+    children.push_back(*child_it);
+  }
+  return utils::mkSortedNode(kind::BITVECTOR_XOR, children);
 }
 
 /**
diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am
index 41bb5db5b..482c06ac7 100644
--- a/test/regress/regress0/aufbv/Makefile.am
+++ b/test/regress/regress0/aufbv/Makefile.am
@@ -22,9 +22,10 @@ TESTS =	\
 	wchains010ue.delta02.smt \
 	dubreva005ue.delta01.smt \
 	fuzz00.smt \
+	fuzz01.smt \
 	fuzz01.delta01.smt \
 	fuzz02.delta01.smt \
-	fuzz02.smt \  
+	fuzz02.smt \
 	fuzz03.delta01.smt \
 	fuzz03.smt \
 	fuzz04.delta01.smt \
@@ -37,11 +38,9 @@ TESTS =	\
 	fuzz08.smt \
 	fuzz09.smt \
 	fuzz10.smt \
-	fifo32bc06k08.delta01.smt
+	fifo32bc06k08.delta01.smt \
+	rewrite_bug.smt
 
-# failing
-#	fuzz01.smt \
-#
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/aufbv/rewrite_bug.smt b/test/regress/regress0/aufbv/rewrite_bug.smt
new file mode 100644
index 000000000..c0906ba0d
--- /dev/null
+++ b/test/regress/regress0/aufbv/rewrite_bug.smt
@@ -0,0 +1,28 @@
+(benchmark B_
+:logic QF_AUFBV
+:extrafuns ((a Array[32:8]))
+:status sat
+:formula
+(flet ($n1 true)
+(let (?n2 bv0[8])
+(let (?n3 (sign_extend[24] ?n2))
+(let (?n4 bv1[32])
+(let (?n5 bv1[8])
+(let (?n6 (store a ?n4 ?n5))
+(let (?n7 bv0[32])
+(let (?n8 (select a ?n4))
+(let (?n9 (sign_extend[24] ?n8))
+(let (?n10 (extract[7:0] ?n9))
+(let (?n11 (store ?n6 ?n7 ?n10))
+(let (?n12 (select ?n11 ?n4))
+(let (?n13 (store ?n11 ?n4 ?n12))
+(let (?n14 (select ?n13 ?n7))
+(let (?n15 (sign_extend[24] ?n14))
+(flet ($n16 (bvslt ?n3 ?n15))
+(flet ($n17 (not $n16))
+(let (?n18 (select ?n13 ?n4))
+(let (?n19 (sign_extend[24] ?n18))
+(flet ($n20 (bvslt ?n7 ?n19))
+(flet ($n21 (and $n1 $n1 $n1 $n1 $n17 $n20))
+$n21
+))))))))))))))))))))))
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index a21c772b1..937a886f6 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -81,7 +81,8 @@ SMT_TESTS = \
 	fuzz40.delta01.smt \
 	fuzz40.smt \
 	fuzz41.smt \
-	calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt
+	calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt \
+	smtcompbug.smt
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS =
diff --git a/test/regress/regress0/bv/smtcompbug.smt b/test/regress/regress0/bv/smtcompbug.smt
new file mode 100644
index 000000000..7efe3015c
--- /dev/null
+++ b/test/regress/regress0/bv/smtcompbug.smt
@@ -0,0 +1,13 @@
+(benchmark B_
+  :status sat
+  :category { unknown }
+  :logic QF_BV
+  :extrafuns ((x781 BitVec[32]))
+  :extrafuns ((x803 BitVec[8]))
+  :extrafuns ((x804 BitVec[8]))
+  :extrafuns ((x791 BitVec[8]))
+  :formula (and
+(= x804 (bvxor (bvxor (extract[7:0] (bvadd bv1[32] x781)) x791) x803))
+(= (bvnot (extract[0:0] x804)) bv0[1])
+(= x781 bv0[32]))
+)