From: Andres Notzli <andres.noetzli@gmail.com>
Date: Wed, 30 Nov 2016 01:30:54 +0000 (-0800)
Subject: Remove wrong `ExtractMultLeadingBit` rule
X-Git-Tag: cvc5-1.0.0~5959^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=05c7d36e7a4844ac1c8a14035776fbba6e00704b;p=cvc5.git

Remove wrong `ExtractMultLeadingBit` rule

The rule `ExtractMultLeadingBit` estimated the number of leading zeros
wrong: when there were ones in the leading constant parts of the
factors, it was using the length of the non-zero part instead of the
length of the zero part. This commit includes an example for which the
previous version of the rule would cause a wrong answer.
---

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index d84a07780..6ef591760 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -802,7 +802,7 @@ bool RewriteRule<ExtractMultLeadingBit>::applies(TNode node) {
     return false;
   unsigned low = utils::getExtractLow(node);
   node = node[0];
-  
+
   if (node.getKind() != kind::BITVECTOR_MULT ||
       node.getNumChildren() != 2 ||
       utils::getSize(node) <= 64)
@@ -818,15 +818,14 @@ bool RewriteRule<ExtractMultLeadingBit>::applies(TNode node) {
   // count number of leading zeroes
   const Integer& int1 = node[0][0].getConst<BitVector>().toInteger();
   const Integer& int2 = node[1][0].getConst<BitVector>().toInteger();
-  unsigned zeroes1 = int1.isZero()? utils::getSize(node[0][0]) :
-                                    int1.length();
-
-  unsigned zeroes2 = int2.isZero()? utils::getSize(node[1][0]) :
-                                    int2.length();
+  size_t int1_size = utils::getSize(node[0][0]);
+  size_t int2_size = utils::getSize(node[1][0]);
+  unsigned zeroes1 = int1.isZero() ? int1_size : int1_size - int1.length();
+  unsigned zeroes2 = int2.isZero() ? int2_size : int2_size - int2.length();
 
   // first k bits are not zero in the result
   unsigned k = 2 * n - (zeroes1 + zeroes2);
-  
+
   if (k > low)
     return false; 
 
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index b3c7250ff..2caaea799 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -112,7 +112,8 @@ CVC_TESTS = bvsimple.cvc sizecheck.cvc
 BUG_TESTS = \
 	bug260a.smt \
 	bug260b.smt \
-	bug440.smt
+	bug440.smt \
+	bug_extract_mult_leading_bit.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 b/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2
new file mode 100644
index 000000000..8e3728587
--- /dev/null
+++ b/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-fun x1 () (_ BitVec 15))
+(declare-fun x2 () (_ BitVec 15))
+(assert (not (= ((_ extract 64 60) (bvmul (concat #b00000000000000000000000000000000000000000000000000 x1) (concat #b10000000000000000000000000000000000000000000000000 x2))) #b00000)))
+(check-sat)
+(exit)