Add unit tests for BitVector, minor BV rewrite fix (#1622)

This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low.

3 files changed, 167 insertions, 27 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index d91067d1e..a4be19253 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1303,10 +1303,13 @@ inline bool RewriteRule<ZeroExtendUltConst>::applies(TNode node) {
       t = node[1][0];
       c = node[0];
     }
-    BitVector bv_c = c.getConst<BitVector>();
-    BitVector bv_max =
-        BitVector(utils::getSize(c)).setBit(utils::getSize(t) - 1);
 
+    if (utils::getSize(t) == utils::getSize(c))
+    {
+      return false;
+    }
+
+    BitVector bv_c = c.getConst<BitVector>();
     BitVector c_hi = c.getConst<BitVector>().extract(utils::getSize(c) - 1,
                                                      utils::getSize(t));
     BitVector zero = BitVector(c_hi.getSize(), Integer(0));
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index 2d94be875..549c94dc9 100644
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -90,6 +90,8 @@ BitVector BitVector::concat(const BitVector& other) const
 
 BitVector BitVector::extract(unsigned high, unsigned low) const
 {
+  CheckArgument(high < d_size, high);
+  CheckArgument(low <= high, low);
   return BitVector(high - low + 1,
                    d_value.extractBitRange(high - low + 1, low));
 }
diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h
index 254abc905..98d148185 100644
--- a/test/unit/util/bitvector_black.h
+++ b/test/unit/util/bitvector_black.h
@@ -26,30 +26,165 @@ class BitVectorBlack : public CxxTest::TestSuite {
 
 
 public:
+ void setUp()
+ {
+   zero = BitVector(4);
+   one = zero.setBit(0);
+   two = BitVector("0010", 2);
+   negOne = BitVector(4, Integer(-1));
+ }
 
-  void testStringConstructor() {
-    BitVector b1("0101",2);
-    TS_ASSERT_EQUALS( 4u, b1.getSize() );
-    TS_ASSERT_EQUALS( "0101", b1.toString() );
-    TS_ASSERT_EQUALS( "5", b1.toString(10) );
-    TS_ASSERT_EQUALS( "5", b1.toString(16) );
-
-    BitVector b2("000001", 2);
-    TS_ASSERT_EQUALS( 6u, b2.getSize() );
-    TS_ASSERT_EQUALS( "000001", b2.toString() );
-    TS_ASSERT_EQUALS( "1", b2.toString(10) );
-    TS_ASSERT_EQUALS( "1", b2.toString(16) );
-
-    BitVector b3("7f", 16);
-    TS_ASSERT_EQUALS( 8u, b3.getSize() );
-    TS_ASSERT_EQUALS( "01111111", b3.toString() );
-    TS_ASSERT_EQUALS( "127", b3.toString(10) );
-    TS_ASSERT_EQUALS( "7f", b3.toString(16) );
-
-    BitVector b4("01a", 16);
-    TS_ASSERT_EQUALS( 12u, b4.getSize() );
-    TS_ASSERT_EQUALS( "000000011010", b4.toString() );
-    TS_ASSERT_EQUALS( "26", b4.toString(10) );
-    TS_ASSERT_EQUALS( "1a", b4.toString(16) );
+ void testStringConstructor()
+ {
+   BitVector b1("0101", 2);
+   TS_ASSERT_EQUALS(4u, b1.getSize());
+   TS_ASSERT_EQUALS("0101", b1.toString());
+   TS_ASSERT_EQUALS("5", b1.toString(10));
+   TS_ASSERT_EQUALS("5", b1.toString(16));
+
+   BitVector b2("000001", 2);
+   TS_ASSERT_EQUALS(6u, b2.getSize());
+   TS_ASSERT_EQUALS("000001", b2.toString());
+   TS_ASSERT_EQUALS("1", b2.toString(10));
+   TS_ASSERT_EQUALS("1", b2.toString(16));
+
+   BitVector b3("7f", 16);
+   TS_ASSERT_EQUALS(8u, b3.getSize());
+   TS_ASSERT_EQUALS("01111111", b3.toString());
+   TS_ASSERT_EQUALS("127", b3.toString(10));
+   TS_ASSERT_EQUALS("7f", b3.toString(16));
+
+   BitVector b4("01a", 16);
+   TS_ASSERT_EQUALS(12u, b4.getSize());
+   TS_ASSERT_EQUALS("000000011010", b4.toString());
+   TS_ASSERT_EQUALS("26", b4.toString(10));
+   TS_ASSERT_EQUALS("1a", b4.toString(16));
+  }
+
+  void testConversions()
+  {
+    TS_ASSERT_EQUALS(two.toSignedInteger(), Integer(2));
+    TS_ASSERT_EQUALS(negOne.toString(), "1111");
+    TS_ASSERT_EQUALS(negOne.getValue(), Integer(15));
+    TS_ASSERT_EQUALS(negOne.getSize(), 4);
+    TS_ASSERT_EQUALS(negOne.toInteger(), Integer(15));
+    TS_ASSERT_EQUALS(negOne.toSignedInteger(), Integer(-1));
+
+    TS_ASSERT_EQUALS(zero.hash(), (one - one).hash());
+    TS_ASSERT_DIFFERS(negOne.hash(), zero.hash());
+  }
+
+  void testSetGetBit()
+  {
+    TS_ASSERT_EQUALS(one.setBit(1).setBit(2).setBit(3), negOne);
+
+    TS_ASSERT(negOne.isBitSet(3));
+    TS_ASSERT(!two.isBitSet(3));
+
+    TS_ASSERT_EQUALS(one.getValue(), Integer(1));
+    TS_ASSERT_EQUALS(zero.isPow2(), 0);
+    TS_ASSERT_EQUALS(one.isPow2(), 1);
+    TS_ASSERT_EQUALS(two.isPow2(), 2);
+    TS_ASSERT_EQUALS(negOne.isPow2(), 0);
+  }
+
+  void testConcatExtract()
+  {
+    BitVector b = one.concat(zero);
+    TS_ASSERT_EQUALS(b.toString(), "00010000");
+    TS_ASSERT_EQUALS(b.extract(7, 4), one);
+    TS_ASSERT_THROWS(b.extract(4, 7), IllegalArgumentException);
+    TS_ASSERT_THROWS(b.extract(8, 3), IllegalArgumentException);
+    TS_ASSERT_EQUALS(b.concat(BitVector()), b);
+  }
+
+  void testComparisons()
+  {
+    TS_ASSERT_DIFFERS(zero, one);
+    TS_ASSERT(negOne > zero);
+    TS_ASSERT(negOne >= zero);
+    TS_ASSERT(negOne >= negOne);
+    TS_ASSERT(negOne == negOne);
+    TS_ASSERT(zero.unsignedLessThan(negOne));
+    TS_ASSERT(zero.unsignedLessThanEq(negOne));
+    TS_ASSERT(zero.unsignedLessThanEq(zero));
+    TS_ASSERT(zero < negOne);
+    TS_ASSERT(zero <= negOne);
+    TS_ASSERT(zero <= zero);
+    TS_ASSERT(negOne.signedLessThan(zero));
+    TS_ASSERT(negOne.signedLessThanEq(zero));
+    TS_ASSERT(negOne.signedLessThanEq(negOne));
+
+    BitVector b = negOne.concat(negOne);
+    TS_ASSERT_THROWS(b.unsignedLessThan(negOne), IllegalArgumentException);
+    TS_ASSERT_THROWS(negOne.unsignedLessThanEq(b), IllegalArgumentException);
+    TS_ASSERT_THROWS(b.signedLessThan(negOne), IllegalArgumentException);
+    TS_ASSERT_THROWS(negOne.signedLessThanEq(b), IllegalArgumentException);
+  }
+
+  void testBitwiseOps()
+  {
+    TS_ASSERT_EQUALS((one ^ negOne).toString(), "1110");
+    TS_ASSERT_EQUALS((two | one).toString(), "0011");
+    TS_ASSERT_EQUALS((negOne & two).toString(), "0010");
+    TS_ASSERT_EQUALS((~two).toString(), "1101");
+  }
+
+  void testArithmetic()
+  {
+    TS_ASSERT_EQUALS(negOne + one, zero);
+    TS_ASSERT_EQUALS((negOne - one).getValue(), Integer(14));
+    TS_ASSERT_EQUALS((-negOne).getValue(), Integer(1));
+
+    TS_ASSERT_EQUALS((two * (two + one)).getValue(), Integer(6));
+
+    TS_ASSERT_EQUALS(two.unsignedDivTotal(zero), negOne);
+    TS_ASSERT_EQUALS(negOne.unsignedDivTotal(two).getValue(), Integer(7));
+
+    TS_ASSERT_EQUALS(two.unsignedRemTotal(zero), two);
+    TS_ASSERT_EQUALS(negOne.unsignedRemTotal(two), one);
+
+    BitVector b = negOne.concat(negOne);
+    TS_ASSERT_THROWS(b + negOne, IllegalArgumentException);
+    TS_ASSERT_THROWS(negOne * b, IllegalArgumentException);
+    TS_ASSERT_THROWS(b.unsignedDivTotal(negOne), IllegalArgumentException);
+    TS_ASSERT_THROWS(negOne.unsignedRemTotal(b), IllegalArgumentException);
+  }
+
+  void testExtendOps()
+  {
+    TS_ASSERT_EQUALS(one.zeroExtend(4), zero.concat(one));
+    TS_ASSERT_EQUALS(one.zeroExtend(0), one);
+    TS_ASSERT_EQUALS(negOne.signExtend(4), negOne.concat(negOne));
+    TS_ASSERT_EQUALS(one.signExtend(4), zero.concat(one));
+    TS_ASSERT_EQUALS(one.signExtend(0), one);
+  }
+
+  void testShifts()
+  {
+    TS_ASSERT_EQUALS(one.leftShift(one), two);
+    TS_ASSERT_EQUALS(one.leftShift(negOne), zero);
+    TS_ASSERT_EQUALS(one.leftShift(zero), one);
+
+    TS_ASSERT_EQUALS(two.logicalRightShift(one), one);
+    TS_ASSERT_EQUALS(two.logicalRightShift(negOne), zero);
+
+    TS_ASSERT_EQUALS(two.arithRightShift(one), one);
+    TS_ASSERT_EQUALS(negOne.arithRightShift(one), negOne);
+    TS_ASSERT_EQUALS(negOne.arithRightShift(negOne), negOne);
+    TS_ASSERT_EQUALS(two.arithRightShift(negOne), zero);
+  }
+
+  void testStaticHelpers()
+  {
+    TS_ASSERT_EQUALS(BitVector::mkOnes(4), negOne);
+    TS_ASSERT_EQUALS(BitVector::mkMinSigned(4).toSignedInteger(), Integer(-8));
+    TS_ASSERT_EQUALS(BitVector::mkMaxSigned(4).toSignedInteger(), Integer(7));
   }
+
+ private:
+  BitVector zero;
+  BitVector one;
+  BitVector two;
+  BitVector negOne;
 };