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 |
|
|
70 |
19 |
TEST_F(TestUtilBlackBitVector, conversions) |
71 |
|
{ |
72 |
2 |
ASSERT_EQ(d_two.toSignedInteger(), Integer(2)); |
73 |
2 |
ASSERT_EQ(d_neg_one.toString(), "1111"); |
74 |
2 |
ASSERT_EQ(d_neg_one.getValue(), Integer(15)); |
75 |
2 |
ASSERT_EQ(d_neg_one.getSize(), 4); |
76 |
2 |
ASSERT_EQ(d_neg_one.toInteger(), Integer(15)); |
77 |
2 |
ASSERT_EQ(d_neg_one.toSignedInteger(), Integer(-1)); |
78 |
|
|
79 |
2 |
ASSERT_EQ(d_zero.hash(), (d_one - d_one).hash()); |
80 |
2 |
ASSERT_NE(d_neg_one.hash(), d_zero.hash()); |
81 |
|
} |
82 |
|
|
83 |
19 |
TEST_F(TestUtilBlackBitVector, setBit_getBit) |
84 |
|
{ |
85 |
4 |
BitVector ones(d_one); |
86 |
2 |
ASSERT_EQ(ones.setBit(1, true).setBit(2, true).setBit(3, true), d_ones); |
87 |
|
|
88 |
4 |
BitVector zero(d_ones); |
89 |
2 |
ASSERT_EQ( |
90 |
|
zero.setBit(0, false).setBit(1, false).setBit(2, false).setBit(3, false), |
91 |
2 |
d_zero); |
92 |
|
|
93 |
2 |
ones = d_ones; |
94 |
2 |
ASSERT_EQ(ones.setBit(0, false).setBit(0, true), d_ones); |
95 |
|
|
96 |
4 |
BitVector not_one(d_ones); |
97 |
2 |
ASSERT_EQ(not_one.setBit(0, false), ~BitVector::mkOne(d_one.getSize())); |
98 |
|
|
99 |
2 |
ASSERT_TRUE(d_ones.isBitSet(3)); |
100 |
2 |
ASSERT_FALSE(d_two.isBitSet(3)); |
101 |
|
|
102 |
2 |
ASSERT_EQ(d_one.getValue(), Integer(1)); |
103 |
2 |
ASSERT_EQ(d_zero.isPow2(), 0); |
104 |
2 |
ASSERT_EQ(d_one.isPow2(), 1); |
105 |
2 |
ASSERT_EQ(d_two.isPow2(), 2); |
106 |
2 |
ASSERT_EQ(d_ones.isPow2(), 0); |
107 |
|
} |
108 |
|
|
109 |
19 |
TEST_F(TestUtilBlackBitVector, concat_extract) |
110 |
|
{ |
111 |
4 |
BitVector b = d_one.concat(d_zero); |
112 |
2 |
ASSERT_EQ(b.toString(), "00010000"); |
113 |
2 |
ASSERT_EQ(b.extract(7, 4), d_one); |
114 |
4 |
ASSERT_THROW(b.extract(4, 7), IllegalArgumentException); |
115 |
4 |
ASSERT_THROW(b.extract(8, 3), IllegalArgumentException); |
116 |
2 |
ASSERT_EQ(b.concat(BitVector()), b); |
117 |
|
} |
118 |
|
|
119 |
19 |
TEST_F(TestUtilBlackBitVector, comparisons) |
120 |
|
{ |
121 |
2 |
ASSERT_NE(d_zero, d_one); |
122 |
2 |
ASSERT_TRUE(d_neg_one > d_zero); |
123 |
2 |
ASSERT_TRUE(d_neg_one >= d_zero); |
124 |
2 |
ASSERT_TRUE(d_neg_one >= d_neg_one); |
125 |
2 |
ASSERT_TRUE(d_neg_one == d_neg_one); |
126 |
2 |
ASSERT_TRUE(d_zero.unsignedLessThan(d_neg_one)); |
127 |
2 |
ASSERT_TRUE(d_zero.unsignedLessThanEq(d_neg_one)); |
128 |
2 |
ASSERT_TRUE(d_zero.unsignedLessThanEq(d_zero)); |
129 |
2 |
ASSERT_TRUE(d_zero < d_neg_one); |
130 |
2 |
ASSERT_TRUE(d_zero <= d_neg_one); |
131 |
2 |
ASSERT_TRUE(d_zero <= d_zero); |
132 |
2 |
ASSERT_TRUE(d_neg_one.signedLessThan(d_zero)); |
133 |
2 |
ASSERT_TRUE(d_neg_one.signedLessThanEq(d_zero)); |
134 |
2 |
ASSERT_TRUE(d_neg_one.signedLessThanEq(d_neg_one)); |
135 |
|
|
136 |
4 |
BitVector b = d_neg_one.concat(d_neg_one); |
137 |
4 |
ASSERT_THROW(b.unsignedLessThan(d_neg_one), IllegalArgumentException); |
138 |
4 |
ASSERT_THROW(d_neg_one.unsignedLessThanEq(b), IllegalArgumentException); |
139 |
4 |
ASSERT_THROW(b.signedLessThan(d_neg_one), IllegalArgumentException); |
140 |
4 |
ASSERT_THROW(d_neg_one.signedLessThanEq(b), IllegalArgumentException); |
141 |
|
} |
142 |
|
|
143 |
19 |
TEST_F(TestUtilBlackBitVector, bitwise_operators) |
144 |
|
{ |
145 |
2 |
ASSERT_EQ((d_one ^ d_neg_one).toString(), "1110"); |
146 |
2 |
ASSERT_EQ((d_two | d_one).toString(), "0011"); |
147 |
2 |
ASSERT_EQ((d_neg_one & d_two).toString(), "0010"); |
148 |
2 |
ASSERT_EQ((~d_two).toString(), "1101"); |
149 |
|
} |
150 |
|
|
151 |
19 |
TEST_F(TestUtilBlackBitVector, arithmetic) |
152 |
|
{ |
153 |
2 |
ASSERT_EQ(d_neg_one + d_one, d_zero); |
154 |
2 |
ASSERT_EQ((d_neg_one - d_one).getValue(), Integer(14)); |
155 |
2 |
ASSERT_EQ((-d_neg_one).getValue(), Integer(1)); |
156 |
|
|
157 |
2 |
ASSERT_EQ((d_two * (d_two + d_one)).getValue(), Integer(6)); |
158 |
|
|
159 |
2 |
ASSERT_EQ(d_two.unsignedDivTotal(d_zero), d_neg_one); |
160 |
2 |
ASSERT_EQ(d_neg_one.unsignedDivTotal(d_two).getValue(), Integer(7)); |
161 |
|
|
162 |
2 |
ASSERT_EQ(d_two.unsignedRemTotal(d_zero), d_two); |
163 |
2 |
ASSERT_EQ(d_neg_one.unsignedRemTotal(d_two), d_one); |
164 |
|
|
165 |
4 |
BitVector b = d_neg_one.concat(d_neg_one); |
166 |
4 |
ASSERT_THROW(b + d_neg_one, IllegalArgumentException); |
167 |
4 |
ASSERT_THROW(d_neg_one * b, IllegalArgumentException); |
168 |
4 |
ASSERT_THROW(b.unsignedDivTotal(d_neg_one), IllegalArgumentException); |
169 |
4 |
ASSERT_THROW(d_neg_one.unsignedRemTotal(b), IllegalArgumentException); |
170 |
|
} |
171 |
|
|
172 |
19 |
TEST_F(TestUtilBlackBitVector, extend_operators) |
173 |
|
{ |
174 |
2 |
ASSERT_EQ(d_one.zeroExtend(4), d_zero.concat(d_one)); |
175 |
2 |
ASSERT_EQ(d_one.zeroExtend(0), d_one); |
176 |
2 |
ASSERT_EQ(d_neg_one.signExtend(4), d_neg_one.concat(d_neg_one)); |
177 |
2 |
ASSERT_EQ(d_one.signExtend(4), d_zero.concat(d_one)); |
178 |
2 |
ASSERT_EQ(d_one.signExtend(0), d_one); |
179 |
|
} |
180 |
|
|
181 |
19 |
TEST_F(TestUtilBlackBitVector, shift_operators) |
182 |
|
{ |
183 |
2 |
ASSERT_EQ(d_one.leftShift(d_one), d_two); |
184 |
2 |
ASSERT_EQ(d_one.leftShift(d_neg_one), d_zero); |
185 |
2 |
ASSERT_EQ(d_one.leftShift(d_zero), d_one); |
186 |
|
|
187 |
2 |
ASSERT_EQ(d_two.logicalRightShift(d_one), d_one); |
188 |
2 |
ASSERT_EQ(d_two.logicalRightShift(d_neg_one), d_zero); |
189 |
|
|
190 |
2 |
ASSERT_EQ(d_two.arithRightShift(d_one), d_one); |
191 |
2 |
ASSERT_EQ(d_neg_one.arithRightShift(d_one), d_neg_one); |
192 |
2 |
ASSERT_EQ(d_neg_one.arithRightShift(d_neg_one), d_neg_one); |
193 |
2 |
ASSERT_EQ(d_two.arithRightShift(d_neg_one), d_zero); |
194 |
|
} |
195 |
|
|
196 |
19 |
TEST_F(TestUtilBlackBitVector, static_helpers) |
197 |
|
{ |
198 |
2 |
ASSERT_EQ(BitVector::mkZero(4), d_zero); |
199 |
2 |
ASSERT_EQ(BitVector::mkOne(4), d_one); |
200 |
2 |
ASSERT_EQ(BitVector::mkOnes(4), d_neg_one); |
201 |
2 |
ASSERT_EQ(BitVector::mkMinSigned(4).toSignedInteger(), Integer(-8)); |
202 |
2 |
ASSERT_EQ(BitVector::mkMaxSigned(4).toSignedInteger(), Integer(7)); |
203 |
|
} |
204 |
|
} // namespace test |
205 |
33 |
} // namespace cvc5 |