1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Black box testing of cvc5::BitVector. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include <sstream> |
17 |
|
|
18 |
|
#include "test.h" |
19 |
|
#include "util/bitvector.h" |
20 |
|
|
21 |
|
namespace cvc5 { |
22 |
|
namespace test { |
23 |
|
|
24 |
40 |
class TestUtilBlackBitVector : public TestInternal |
25 |
|
{ |
26 |
|
protected: |
27 |
20 |
void SetUp() override |
28 |
|
{ |
29 |
20 |
d_zero = BitVector(4); |
30 |
20 |
d_one = BitVector::mkOne(4); |
31 |
20 |
d_two = BitVector("0010", 2); |
32 |
20 |
d_neg_one = BitVector(4, Integer(-1)); |
33 |
20 |
d_ones = BitVector::mkOnes(4); |
34 |
20 |
} |
35 |
|
|
36 |
|
BitVector d_zero; |
37 |
|
BitVector d_one; |
38 |
|
BitVector d_two; |
39 |
|
BitVector d_neg_one; |
40 |
|
BitVector d_ones; |
41 |
|
}; |
42 |
|
|
43 |
19 |
TEST_F(TestUtilBlackBitVector, string_constructor) |
44 |
|
{ |
45 |
4 |
BitVector b1("0101", 2); |
46 |
2 |
ASSERT_EQ(4u, b1.getSize()); |
47 |
2 |
ASSERT_EQ("0101", b1.toString()); |
48 |
2 |
ASSERT_EQ("5", b1.toString(10)); |
49 |
2 |
ASSERT_EQ("5", b1.toString(16)); |
50 |
|
|
51 |
4 |
BitVector b2("000001", 2); |
52 |
2 |
ASSERT_EQ(6u, b2.getSize()); |
53 |
2 |
ASSERT_EQ("000001", b2.toString()); |
54 |
2 |
ASSERT_EQ("1", b2.toString(10)); |
55 |
2 |
ASSERT_EQ("1", b2.toString(16)); |
56 |
|
|
57 |
4 |
BitVector b3("7f", 16); |
58 |
2 |
ASSERT_EQ(8u, b3.getSize()); |
59 |
2 |
ASSERT_EQ("01111111", b3.toString()); |
60 |
2 |
ASSERT_EQ("127", b3.toString(10)); |
61 |
2 |
ASSERT_EQ("7f", b3.toString(16)); |
62 |
|
|
63 |
4 |
BitVector b4("01a", 16); |
64 |
2 |
ASSERT_EQ(12u, b4.getSize()); |
65 |
2 |
ASSERT_EQ("000000011010", b4.toString()); |
66 |
2 |
ASSERT_EQ("26", b4.toString(10)); |
67 |
2 |
ASSERT_EQ("1a", b4.toString(16)); |
68 |
|
|
69 |
4 |
ASSERT_THROW(BitVector("-4", 10), IllegalArgumentException); |
70 |
4 |
ASSERT_THROW(BitVector("-0010", 2), IllegalArgumentException); |
71 |
4 |
ASSERT_THROW(BitVector("-3210", 4), IllegalArgumentException); |
72 |
2 |
ASSERT_EQ(3, BitVector("4", 10).getSize()); |
73 |
|
} |
74 |
|
|
75 |
19 |
TEST_F(TestUtilBlackBitVector, conversions) |
76 |
|
{ |
77 |
2 |
ASSERT_EQ(d_two.toSignedInteger(), Integer(2)); |
78 |
2 |
ASSERT_EQ(d_neg_one.toString(), "1111"); |
79 |
2 |
ASSERT_EQ(d_neg_one.getValue(), Integer(15)); |
80 |
2 |
ASSERT_EQ(d_neg_one.getSize(), 4); |
81 |
2 |
ASSERT_EQ(d_neg_one.toInteger(), Integer(15)); |
82 |
2 |
ASSERT_EQ(d_neg_one.toSignedInteger(), Integer(-1)); |
83 |
|
|
84 |
2 |
ASSERT_EQ(d_zero.hash(), (d_one - d_one).hash()); |
85 |
2 |
ASSERT_NE(d_neg_one.hash(), d_zero.hash()); |
86 |
|
} |
87 |
|
|
88 |
19 |
TEST_F(TestUtilBlackBitVector, setBit_getBit) |
89 |
|
{ |
90 |
4 |
BitVector ones(d_one); |
91 |
2 |
ASSERT_EQ(ones.setBit(1, true).setBit(2, true).setBit(3, true), d_ones); |
92 |
|
|
93 |
4 |
BitVector zero(d_ones); |
94 |
2 |
ASSERT_EQ( |
95 |
|
zero.setBit(0, false).setBit(1, false).setBit(2, false).setBit(3, false), |
96 |
2 |
d_zero); |
97 |
|
|
98 |
2 |
ones = d_ones; |
99 |
2 |
ASSERT_EQ(ones.setBit(0, false).setBit(0, true), d_ones); |
100 |
|
|
101 |
4 |
BitVector not_one(d_ones); |
102 |
2 |
ASSERT_EQ(not_one.setBit(0, false), ~BitVector::mkOne(d_one.getSize())); |
103 |
|
|
104 |
2 |
ASSERT_TRUE(d_ones.isBitSet(3)); |
105 |
2 |
ASSERT_FALSE(d_two.isBitSet(3)); |
106 |
|
|
107 |
2 |
ASSERT_EQ(d_one.getValue(), Integer(1)); |
108 |
2 |
ASSERT_EQ(d_zero.isPow2(), 0); |
109 |
2 |
ASSERT_EQ(d_one.isPow2(), 1); |
110 |
2 |
ASSERT_EQ(d_two.isPow2(), 2); |
111 |
2 |
ASSERT_EQ(d_ones.isPow2(), 0); |
112 |
|
} |
113 |
|
|
114 |
19 |
TEST_F(TestUtilBlackBitVector, concat_extract) |
115 |
|
{ |
116 |
4 |
BitVector b = d_one.concat(d_zero); |
117 |
2 |
ASSERT_EQ(b.toString(), "00010000"); |
118 |
2 |
ASSERT_EQ(b.extract(7, 4), d_one); |
119 |
4 |
ASSERT_THROW(b.extract(4, 7), IllegalArgumentException); |
120 |
4 |
ASSERT_THROW(b.extract(8, 3), IllegalArgumentException); |
121 |
2 |
ASSERT_EQ(b.concat(BitVector()), b); |
122 |
|
} |
123 |
|
|
124 |
19 |
TEST_F(TestUtilBlackBitVector, comparisons) |
125 |
|
{ |
126 |
2 |
ASSERT_NE(d_zero, d_one); |
127 |
2 |
ASSERT_TRUE(d_neg_one > d_zero); |
128 |
2 |
ASSERT_TRUE(d_neg_one >= d_zero); |
129 |
2 |
ASSERT_TRUE(d_neg_one >= d_neg_one); |
130 |
2 |
ASSERT_TRUE(d_neg_one == d_neg_one); |
131 |
2 |
ASSERT_TRUE(d_zero.unsignedLessThan(d_neg_one)); |
132 |
2 |
ASSERT_TRUE(d_zero.unsignedLessThanEq(d_neg_one)); |
133 |
2 |
ASSERT_TRUE(d_zero.unsignedLessThanEq(d_zero)); |
134 |
2 |
ASSERT_TRUE(d_zero < d_neg_one); |
135 |
2 |
ASSERT_TRUE(d_zero <= d_neg_one); |
136 |
2 |
ASSERT_TRUE(d_zero <= d_zero); |
137 |
2 |
ASSERT_TRUE(d_neg_one.signedLessThan(d_zero)); |
138 |
2 |
ASSERT_TRUE(d_neg_one.signedLessThanEq(d_zero)); |
139 |
2 |
ASSERT_TRUE(d_neg_one.signedLessThanEq(d_neg_one)); |
140 |
|
|
141 |
4 |
BitVector b = d_neg_one.concat(d_neg_one); |
142 |
4 |
ASSERT_THROW(b.unsignedLessThan(d_neg_one), IllegalArgumentException); |
143 |
4 |
ASSERT_THROW(d_neg_one.unsignedLessThanEq(b), IllegalArgumentException); |
144 |
4 |
ASSERT_THROW(b.signedLessThan(d_neg_one), IllegalArgumentException); |
145 |
4 |
ASSERT_THROW(d_neg_one.signedLessThanEq(b), IllegalArgumentException); |
146 |
|
} |
147 |
|
|
148 |
19 |
TEST_F(TestUtilBlackBitVector, bitwise_operators) |
149 |
|
{ |
150 |
2 |
ASSERT_EQ((d_one ^ d_neg_one).toString(), "1110"); |
151 |
2 |
ASSERT_EQ((d_two | d_one).toString(), "0011"); |
152 |
2 |
ASSERT_EQ((d_neg_one & d_two).toString(), "0010"); |
153 |
2 |
ASSERT_EQ((~d_two).toString(), "1101"); |
154 |
|
} |
155 |
|
|
156 |
19 |
TEST_F(TestUtilBlackBitVector, arithmetic) |
157 |
|
{ |
158 |
2 |
ASSERT_EQ(d_neg_one + d_one, d_zero); |
159 |
2 |
ASSERT_EQ((d_neg_one - d_one).getValue(), Integer(14)); |
160 |
2 |
ASSERT_EQ((-d_neg_one).getValue(), Integer(1)); |
161 |
|
|
162 |
2 |
ASSERT_EQ((d_two * (d_two + d_one)).getValue(), Integer(6)); |
163 |
|
|
164 |
2 |
ASSERT_EQ(d_two.unsignedDivTotal(d_zero), d_neg_one); |
165 |
2 |
ASSERT_EQ(d_neg_one.unsignedDivTotal(d_two).getValue(), Integer(7)); |
166 |
|
|
167 |
2 |
ASSERT_EQ(d_two.unsignedRemTotal(d_zero), d_two); |
168 |
2 |
ASSERT_EQ(d_neg_one.unsignedRemTotal(d_two), d_one); |
169 |
|
|
170 |
4 |
BitVector b = d_neg_one.concat(d_neg_one); |
171 |
4 |
ASSERT_THROW(b + d_neg_one, IllegalArgumentException); |
172 |
4 |
ASSERT_THROW(d_neg_one * b, IllegalArgumentException); |
173 |
4 |
ASSERT_THROW(b.unsignedDivTotal(d_neg_one), IllegalArgumentException); |
174 |
4 |
ASSERT_THROW(d_neg_one.unsignedRemTotal(b), IllegalArgumentException); |
175 |
|
} |
176 |
|
|
177 |
19 |
TEST_F(TestUtilBlackBitVector, extend_operators) |
178 |
|
{ |
179 |
2 |
ASSERT_EQ(d_one.zeroExtend(4), d_zero.concat(d_one)); |
180 |
2 |
ASSERT_EQ(d_one.zeroExtend(0), d_one); |
181 |
2 |
ASSERT_EQ(d_neg_one.signExtend(4), d_neg_one.concat(d_neg_one)); |
182 |
2 |
ASSERT_EQ(d_one.signExtend(4), d_zero.concat(d_one)); |
183 |
2 |
ASSERT_EQ(d_one.signExtend(0), d_one); |
184 |
|
} |
185 |
|
|
186 |
19 |
TEST_F(TestUtilBlackBitVector, shift_operators) |
187 |
|
{ |
188 |
2 |
ASSERT_EQ(d_one.leftShift(d_one), d_two); |
189 |
2 |
ASSERT_EQ(d_one.leftShift(d_neg_one), d_zero); |
190 |
2 |
ASSERT_EQ(d_one.leftShift(d_zero), d_one); |
191 |
|
|
192 |
2 |
ASSERT_EQ(d_two.logicalRightShift(d_one), d_one); |
193 |
2 |
ASSERT_EQ(d_two.logicalRightShift(d_neg_one), d_zero); |
194 |
|
|
195 |
2 |
ASSERT_EQ(d_two.arithRightShift(d_one), d_one); |
196 |
2 |
ASSERT_EQ(d_neg_one.arithRightShift(d_one), d_neg_one); |
197 |
2 |
ASSERT_EQ(d_neg_one.arithRightShift(d_neg_one), d_neg_one); |
198 |
2 |
ASSERT_EQ(d_two.arithRightShift(d_neg_one), d_zero); |
199 |
|
} |
200 |
|
|
201 |
19 |
TEST_F(TestUtilBlackBitVector, static_helpers) |
202 |
|
{ |
203 |
2 |
ASSERT_EQ(BitVector::mkZero(4), d_zero); |
204 |
2 |
ASSERT_EQ(BitVector::mkOne(4), d_one); |
205 |
2 |
ASSERT_EQ(BitVector::mkOnes(4), d_neg_one); |
206 |
2 |
ASSERT_EQ(BitVector::mkMinSigned(4).toSignedInteger(), Integer(-8)); |
207 |
2 |
ASSERT_EQ(BitVector::mkMaxSigned(4).toSignedInteger(), Integer(7)); |
208 |
|
} |
209 |
|
} // namespace test |
210 |
33 |
} // namespace cvc5 |