Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Alex Ozdemir
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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::internal {
22 : : namespace test {
23 : :
24 : : class TestUtilBlackBitVector : public TestInternal
25 : : {
26 : : protected:
27 : 10 : void SetUp() override
28 : : {
29 : 10 : d_zero = BitVector(4);
30 : 10 : d_one = BitVector::mkOne(4);
31 : 10 : d_two = BitVector("0010", 2);
32 : 10 : d_neg_one = BitVector(4, Integer(-1));
33 : 10 : d_ones = BitVector::mkOnes(4);
34 : 10 : }
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 : 2 : TEST_F(TestUtilBlackBitVector, string_constructor)
44 : : {
45 : 2 : BitVector b1("0101", 2);
46 [ - + ]: 1 : 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 : 2 : BitVector b2("000001", 2);
52 [ - + ]: 1 : 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 : 2 : BitVector b3("7f", 16);
58 [ - + ]: 1 : 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 : 2 : BitVector b4("01a", 16);
64 [ - + ]: 1 : 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 : 1 : ASSERT_DEATH(BitVector("-4", 10), "num\\[0\\] != '-'");
70 : 1 : ASSERT_DEATH(BitVector("-0010", 2), "num\\[0\\] != '-'");
71 : 1 : ASSERT_DEATH(BitVector("-3210", 4), "base == 2");
72 [ - + ]: 1 : ASSERT_EQ(3, BitVector("4", 10).getSize());
73 : : }
74 : :
75 : 2 : 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 [ - + ]: 1 : 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 [ - + ]: 1 : ASSERT_EQ(d_zero.hash(), (d_one - d_one).hash());
85 [ - + ]: 1 : ASSERT_NE(d_neg_one.hash(), d_zero.hash());
86 : : }
87 : :
88 : 2 : TEST_F(TestUtilBlackBitVector, setBit_getBit)
89 : : {
90 : 1 : BitVector ones(d_one);
91 [ - + ]: 1 : ASSERT_EQ(ones.setBit(1, true).setBit(2, true).setBit(3, true), d_ones);
92 : :
93 : 1 : BitVector zero(d_ones);
94 [ - + ]: 1 : ASSERT_EQ(
95 : : zero.setBit(0, false).setBit(1, false).setBit(2, false).setBit(3, false),
96 : : d_zero);
97 : :
98 : 1 : ones = d_ones;
99 [ - + ]: 1 : ASSERT_EQ(ones.setBit(0, false).setBit(0, true), d_ones);
100 : :
101 : 1 : BitVector not_one(d_ones);
102 [ - + ]: 2 : ASSERT_EQ(not_one.setBit(0, false), ~BitVector::mkOne(d_one.getSize()));
103 : :
104 [ - + ]: 1 : ASSERT_TRUE(d_ones.isBitSet(3));
105 [ - + ]: 1 : ASSERT_FALSE(d_two.isBitSet(3));
106 : :
107 [ - + ]: 2 : ASSERT_EQ(d_one.getValue(), Integer(1));
108 [ - + ]: 1 : ASSERT_EQ(d_zero.isPow2(), 0);
109 [ - + ]: 1 : ASSERT_EQ(d_one.isPow2(), 1);
110 [ - + ]: 1 : ASSERT_EQ(d_two.isPow2(), 2);
111 [ - + ]: 1 : ASSERT_EQ(d_ones.isPow2(), 0);
112 : : }
113 : :
114 : 2 : TEST_F(TestUtilBlackBitVector, concat_extract)
115 : : {
116 : 1 : 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 : 1 : ASSERT_DEATH(b.extract(4, 7), "low <= high");
120 : 1 : ASSERT_DEATH(b.extract(8, 3), "high < d_size");
121 [ - + ]: 2 : ASSERT_EQ(b.concat(BitVector()), b);
122 : : }
123 : :
124 : 2 : TEST_F(TestUtilBlackBitVector, comparisons)
125 : : {
126 [ - + ]: 1 : ASSERT_NE(d_zero, d_one);
127 [ - + ]: 1 : ASSERT_TRUE(d_neg_one > d_zero);
128 [ - + ]: 1 : ASSERT_TRUE(d_neg_one >= d_zero);
129 [ - + ]: 1 : ASSERT_TRUE(d_neg_one >= d_neg_one);
130 [ - + ]: 1 : ASSERT_TRUE(d_neg_one == d_neg_one);
131 [ - + ]: 1 : ASSERT_TRUE(d_zero.unsignedLessThan(d_neg_one));
132 [ - + ]: 1 : ASSERT_TRUE(d_zero.unsignedLessThanEq(d_neg_one));
133 [ - + ]: 1 : ASSERT_TRUE(d_zero.unsignedLessThanEq(d_zero));
134 [ - + ]: 1 : ASSERT_TRUE(d_zero < d_neg_one);
135 [ - + ]: 1 : ASSERT_TRUE(d_zero <= d_neg_one);
136 [ - + ]: 1 : ASSERT_TRUE(d_zero <= d_zero);
137 [ - + ]: 1 : ASSERT_TRUE(d_neg_one.signedLessThan(d_zero));
138 [ - + ]: 1 : ASSERT_TRUE(d_neg_one.signedLessThanEq(d_zero));
139 [ - + ]: 1 : ASSERT_TRUE(d_neg_one.signedLessThanEq(d_neg_one));
140 : :
141 : 1 : BitVector b = d_neg_one.concat(d_neg_one);
142 : 1 : ASSERT_DEATH(b.unsignedLessThan(d_neg_one), "d_size == y.d_size");
143 : 1 : ASSERT_DEATH(d_neg_one.unsignedLessThanEq(b), "d_size == y.d_size");
144 : 1 : ASSERT_DEATH(b.signedLessThan(d_neg_one), "d_size == y.d_size");
145 : 1 : ASSERT_DEATH(d_neg_one.signedLessThanEq(b), "d_size == y.d_size");
146 : : }
147 : :
148 : 2 : 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 : 2 : 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 : 1 : BitVector b = d_neg_one.concat(d_neg_one);
171 : 1 : ASSERT_DEATH(b + d_neg_one, "a.getSize\\(\\) == b.getSize\\(\\)");
172 : 1 : ASSERT_DEATH(d_neg_one * b, "a.getSize\\(\\) == b.getSize\\(\\)");
173 : 1 : ASSERT_DEATH(b.unsignedDivTotal(d_neg_one), "d_size == y\\.d_size");
174 : 1 : ASSERT_DEATH(d_neg_one.unsignedRemTotal(b), "d_size == y\\.d_size");
175 : : }
176 : :
177 : 2 : 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 : 2 : 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 : 2 : 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 : : } // namespace cvc5::internal
|
