diff options
author | Andres Notzli <andres.noetzli@gmail.com> | 2016-11-29 17:30:54 -0800 |
---|---|---|
committer | Andres Notzli <andres.noetzli@gmail.com> | 2016-11-30 15:33:35 -0800 |
commit | 05c7d36e7a4844ac1c8a14035776fbba6e00704b (patch) | |
tree | 1c9a5919a9ce461f64b9f8b7c26c26cf54c1b4d3 /src | |
parent | bc2378517a2f4100ba614cd44b3aa047089c82c8 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 13 |
1 files changed, 6 insertions, 7 deletions
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; |