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