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 : : * White box testing of cvc5::internal::expr::attr::AttrHash<>
11 : : */
12 : :
13 : : #include <stdint.h>
14 : :
15 : : #include <array>
16 : : #include <cstdint>
17 : : #include <utility>
18 : :
19 : : #include "expr/attribute.h"
20 : : #include "test_node.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace test {
24 : : // fixtures
25 : : class AttrHashFixture : public TestInternal
26 : : {
27 : : public:
28 : 3 : AttrHashFixture()
29 : 6 : : d_nodeManager{std::make_unique<NodeManager>()},
30 : 3 : d_booleanType{d_nodeManager->booleanType()}
31 : : {
32 : 3 : }
33 : :
34 : : protected:
35 : : template <typename V>
36 : : using Hash = expr::attr::AttrHash<V>;
37 : :
38 : : std::unique_ptr<NodeManager> d_nodeManager;
39 : : TypeNode d_booleanType;
40 : : };
41 : :
42 : 4 : TEST_F(AttrHashFixture, basic)
43 : : {
44 : 2 : Node nA = d_nodeManager->mkVar("A", d_booleanType);
45 : 2 : Node nB = d_nodeManager->mkVar("B", d_booleanType);
46 : 2 : Node nC = d_nodeManager->mkVar("C", d_booleanType);
47 : 2 : Node nD = d_nodeManager->mkVar("D", d_booleanType);
48 : :
49 : : // a constant hash will always be empty (only default constructor)
50 : 1 : const Hash<int> emptyHash;
51 [ - + ]: 1 : EXPECT_EQ(std::distance(emptyHash.begin(), emptyHash.end()),
52 : 1 : 0u); // const iterators
53 [ - + ]: 1 : EXPECT_EQ(emptyHash.size(), 0u);
54 : :
55 : : // add elements using operator[] and varying NodeValue*
56 : 2 : Hash<int> hash1;
57 : 1 : hash1[std::make_pair(0u, nA.d_nv)] = 0;
58 : 1 : hash1[std::make_pair(0u, nB.d_nv)] = 1;
59 : 1 : hash1[std::make_pair(0u, nC.d_nv)] = 2;
60 : :
61 [ - + ]: 1 : EXPECT_EQ(hash1.size(), 3u);
62 [ - + ]: 1 : EXPECT_EQ(std::distance(hash1.begin(), hash1.end()), 3u); // non-const
63 : :
64 : : // check const iterators on non-empty hash
65 : 1 : auto const_size_of = [](Hash<int> const& h) {
66 : 1 : return std::distance(h.begin(), h.end());
67 : : };
68 [ - + ]: 1 : EXPECT_EQ(const_size_of(hash1), 3u);
69 : :
70 : : // make sure the expected values are present
71 [ - + ]: 1 : EXPECT_NE(hash1.find(std::make_pair(0u, nA.d_nv)), hash1.end());
72 [ - + ]: 1 : EXPECT_NE(hash1.find(std::make_pair(0u, nB.d_nv)), hash1.end());
73 [ - + ]: 1 : EXPECT_NE(hash1.find(std::make_pair(0u, nC.d_nv)), hash1.end());
74 : :
75 : : // add elements using "insert", varying Id
76 : 2 : Hash<int> hash2;
77 : : std::array<typename Hash<int>::iterator::value_type, 3> new_elements{
78 : 1 : std::make_pair(std::make_pair(uint64_t{42}, nA.d_nv), 1),
79 : 1 : std::make_pair(std::make_pair(uint64_t{43}, nA.d_nv), 2),
80 : 1 : std::make_pair(std::make_pair(uint64_t{44}, nA.d_nv), 3)};
81 : 1 : hash2.insert(new_elements.begin(), new_elements.end());
82 [ - + ]: 1 : EXPECT_EQ(hash2.size(), 3u);
83 [ - + ]: 1 : EXPECT_EQ(std::distance(hash2.begin(), hash2.end()), 3u);
84 : :
85 : : // are they there?
86 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{42}, nA.d_nv)), hash2.end());
87 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{43}, nA.d_nv)), hash2.end());
88 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{44}, nA.d_nv)), hash2.end());
89 : :
90 : : // erase by iterator
91 : : auto next_after_erase =
92 : 1 : hash2.erase(hash2.find(std::make_pair(uint64_t{43}, nA.d_nv)));
93 : : // entry is gone
94 [ - + ]: 1 : EXPECT_EQ(hash2.find(std::make_pair(uint64_t{43}, nA.d_nv)), hash2.end());
95 : : // the returned "next" iterator makes sense
96 [ + - ][ + - ]: 1 : EXPECT_TRUE((next_after_erase == hash2.end())
[ + - ][ - + ]
97 : : || ((*next_after_erase)
98 : : == std::make_pair(std::make_pair(uint64_t{42}, nA.d_nv), 1))
99 : : || ((*next_after_erase)
100 : 1 : == std::make_pair(std::make_pair(uint64_t{44}, nA.d_nv), 3)));
101 : :
102 : : // erase by NodeValue*
103 : 1 : hash1.eraseBy(nC.d_nv);
104 [ - + ]: 1 : EXPECT_EQ(hash1.find(std::make_pair(0u, nC.d_nv)), hash1.end());
105 [ - + ]: 1 : EXPECT_EQ(hash1.size(), std::size_t{2});
106 [ - + ]: 1 : EXPECT_EQ(std::distance(hash1.begin(), hash1.end()), std::size_t{2});
107 [ - + ]: 1 : EXPECT_NE(hash1.find(std::make_pair(0u, nA.d_nv)), hash1.end());
108 [ - + ]: 1 : EXPECT_NE(hash1.find(std::make_pair(0u, nB.d_nv)), hash1.end());
109 : :
110 : : // clear
111 : 1 : hash1.clear();
112 [ - + ]: 1 : EXPECT_EQ(hash1.size(), 0ul);
113 : :
114 : : // swap
115 : 1 : std::swap(hash1, hash2);
116 [ - + ]: 1 : EXPECT_EQ(hash2.size(), 0ul);
117 [ - + ]: 1 : EXPECT_EQ(hash1.size(), 2ul);
118 [ - + ]: 1 : EXPECT_NE(hash1.find(std::make_pair(uint64_t{42}, nA.d_nv)), hash1.end());
119 [ - + ]: 1 : EXPECT_NE(hash1.find(std::make_pair(uint64_t{44}, nA.d_nv)), hash1.end());
120 : 1 : }
121 : :
122 : 4 : TEST_F(AttrHashFixture, empty_levels)
123 : : {
124 : : // removing the last element from an L2 map
125 : : // (thus causing an empty L2) changes
126 : : // nothing about the operation of the hash overall
127 : :
128 : 2 : Node nA = d_nodeManager->mkVar("A", d_booleanType);
129 : 2 : Node nB = d_nodeManager->mkVar("B", d_booleanType);
130 : 2 : Node nC = d_nodeManager->mkVar("C", d_booleanType);
131 : 2 : Node nD = d_nodeManager->mkVar("D", d_booleanType);
132 : :
133 : : std::array<typename Hash<int>::iterator::value_type, 2> new_elements{
134 : 1 : std::make_pair(std::make_pair(uint64_t{42}, nA.d_nv), 1),
135 : 1 : std::make_pair(std::make_pair(uint64_t{43}, nA.d_nv), 2)};
136 : :
137 : 1 : Hash<int> hash1;
138 : 1 : hash1.insert(new_elements.begin(), new_elements.end());
139 [ - + ]: 1 : EXPECT_EQ(hash1.size(), std::size_t{2});
140 : 1 : auto it = hash1.erase(hash1.begin());
141 [ + - ][ + - ]: 1 : EXPECT_TRUE((it == hash1.end()) || (it == hash1.begin()));
[ - + ]
142 [ - + ]: 1 : EXPECT_EQ(hash1.find((*hash1.begin()).first), hash1.begin());
143 [ - + ]: 1 : EXPECT_EQ(hash1.size(), std::size_t{1});
144 : :
145 : : // delete the last element
146 : 1 : hash1.erase(hash1.begin());
147 [ - + ]: 1 : EXPECT_EQ(hash1.size(), 0ul);
148 : :
149 : : // create several L2 maps in a fresh hash
150 : : std::array<typename Hash<int>::iterator::value_type, 8> new_elements2{
151 : 1 : std::make_pair(std::make_pair(uint64_t{11}, nD.d_nv), 3),
152 : 1 : std::make_pair(std::make_pair(uint64_t{12}, nA.d_nv), 3),
153 : 1 : std::make_pair(std::make_pair(uint64_t{13}, nB.d_nv), 2),
154 : 1 : std::make_pair(std::make_pair(uint64_t{14}, nA.d_nv), 4),
155 : 1 : std::make_pair(std::make_pair(uint64_t{15}, nB.d_nv), 2),
156 : 1 : std::make_pair(std::make_pair(uint64_t{16}, nC.d_nv), 5),
157 : 1 : std::make_pair(std::make_pair(uint64_t{17}, nD.d_nv), 6),
158 : 1 : std::make_pair(std::make_pair(uint64_t{18}, nC.d_nv), 7)};
159 : :
160 : 2 : Hash<int> hash2;
161 : 1 : hash2.insert(new_elements2.begin(), new_elements2.end());
162 [ - + ]: 1 : EXPECT_EQ(hash2.size(), std::size_t{8});
163 : :
164 : : // remove the two node B attributes one at a time
165 : 1 : hash2.erase(hash2.find(std::make_pair(uint64_t{13}, nB.d_nv)));
166 [ - + ]: 1 : EXPECT_EQ(hash2.find(std::make_pair(uint64_t{13}, nB.d_nv)), hash2.end());
167 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{15}, nB.d_nv)), hash2.end());
168 [ - + ]: 1 : EXPECT_EQ(hash2[std::make_pair(uint64_t{15}, nB.d_nv)], 2);
169 [ - + ]: 1 : EXPECT_EQ(hash2.size(), std::size_t{7});
170 [ - + ]: 1 : EXPECT_EQ(std::distance(hash2.begin(), hash2.end()), std::size_t{7});
171 : :
172 : 1 : hash2.erase(hash2.find(std::make_pair(uint64_t{15}, nB.d_nv)));
173 [ - + ]: 1 : EXPECT_EQ(hash2.find(std::make_pair(uint64_t{15}, nB.d_nv)), hash2.end());
174 : :
175 : : // validate remaining entries
176 [ - + ]: 1 : EXPECT_EQ(hash2.size(), std::size_t{6});
177 [ - + ]: 1 : EXPECT_EQ(std::distance(hash2.begin(), hash2.end()), std::size_t{6});
178 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{11}, nD.d_nv)), hash2.end());
179 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{12}, nA.d_nv)), hash2.end());
180 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{14}, nA.d_nv)), hash2.end());
181 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{16}, nC.d_nv)), hash2.end());
182 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{17}, nD.d_nv)), hash2.end());
183 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{18}, nC.d_nv)), hash2.end());
184 [ - + ]: 1 : EXPECT_EQ(hash2[std::make_pair(uint64_t{11}, nD.d_nv)], 3);
185 [ - + ]: 1 : EXPECT_EQ(hash2[std::make_pair(uint64_t{12}, nA.d_nv)], 3);
186 [ - + ]: 1 : EXPECT_EQ(hash2[std::make_pair(uint64_t{14}, nA.d_nv)], 4);
187 [ - + ]: 1 : EXPECT_EQ(hash2[std::make_pair(uint64_t{16}, nC.d_nv)], 5);
188 [ - + ]: 1 : EXPECT_EQ(hash2[std::make_pair(uint64_t{17}, nD.d_nv)], 6);
189 [ - + ]: 1 : EXPECT_EQ(hash2[std::make_pair(uint64_t{18}, nC.d_nv)], 7);
190 : :
191 : : // now delete one full NodeValue*'s worth (one L2 map) and reverify
192 : 1 : hash2.eraseBy(nA.d_nv);
193 [ - + ]: 1 : EXPECT_EQ(hash2.size(), std::size_t{4});
194 [ - + ]: 1 : EXPECT_EQ(std::distance(hash2.begin(), hash2.end()), std::size_t{4});
195 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{11}, nD.d_nv)), hash2.end());
196 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{16}, nC.d_nv)), hash2.end());
197 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{17}, nD.d_nv)), hash2.end());
198 [ - + ]: 1 : EXPECT_NE(hash2.find(std::make_pair(uint64_t{18}, nC.d_nv)), hash2.end());
199 [ - + ]: 1 : EXPECT_EQ(hash2[std::make_pair(uint64_t{11}, nD.d_nv)], 3);
200 [ - + ]: 1 : EXPECT_EQ(hash2[std::make_pair(uint64_t{16}, nC.d_nv)], 5);
201 [ - + ]: 1 : EXPECT_EQ(hash2[std::make_pair(uint64_t{17}, nD.d_nv)], 6);
202 [ - + ]: 1 : EXPECT_EQ(hash2[std::make_pair(uint64_t{18}, nC.d_nv)], 7);
203 : 1 : }
204 : :
205 : 4 : TEST_F(AttrHashFixture, repeated_inserts)
206 : : {
207 : : // when we insert with an existing key, the value is not updated,
208 : : // but it is when we use operator[]
209 : :
210 : 2 : Node nA = d_nodeManager->mkVar("A", d_booleanType);
211 : 2 : Node nB = d_nodeManager->mkVar("B", d_booleanType);
212 : 2 : Node nC = d_nodeManager->mkVar("C", d_booleanType);
213 : :
214 : : std::array<typename Hash<int>::iterator::value_type, 5> initial_elements{
215 : 1 : std::make_pair(std::make_pair(uint64_t{42}, nA.d_nv), 2),
216 : 1 : std::make_pair(std::make_pair(uint64_t{43}, nA.d_nv), 1),
217 : 1 : std::make_pair(std::make_pair(uint64_t{42}, nB.d_nv), 4),
218 : 1 : std::make_pair(std::make_pair(uint64_t{43}, nB.d_nv), 5),
219 : 1 : std::make_pair(std::make_pair(uint64_t{42}, nC.d_nv), 2)};
220 : :
221 : 1 : Hash<int> hash;
222 : 1 : hash.insert(initial_elements.begin(), initial_elements.end());
223 : :
224 : : // attempt to change two entries using insert
225 : : std::array<typename Hash<int>::iterator::value_type, 2> new_elements{
226 : 1 : std::make_pair(std::make_pair(uint64_t{42}, nA.d_nv), 6),
227 : 1 : std::make_pair(std::make_pair(uint64_t{42}, nC.d_nv), 8)};
228 : 1 : hash.insert(new_elements.begin(), new_elements.end());
229 : :
230 : : // entries should be unchanged (insert doesn't alter existing entries)
231 [ - + ]: 1 : EXPECT_EQ(hash.size(), std::size_t{5});
232 [ - + ]: 1 : EXPECT_EQ(hash[std::make_pair(uint64_t{42}, nA.d_nv)], 2);
233 [ - + ]: 1 : EXPECT_EQ(hash[std::make_pair(uint64_t{42}, nC.d_nv)], 2);
234 [ - + ]: 1 : EXPECT_EQ(*hash.find(std::make_pair(uint64_t{42}, nA.d_nv)),
235 : 1 : std::make_pair(std::make_pair(uint64_t{42}, nA.d_nv), 2));
236 [ - + ]: 1 : EXPECT_EQ(*hash.find(std::make_pair(uint64_t{42}, nC.d_nv)),
237 : 1 : std::make_pair(std::make_pair(uint64_t{42}, nC.d_nv), 2));
238 : :
239 : : // change two entries using operator[]
240 : 1 : hash[std::make_pair(uint64_t{42}, nB.d_nv)] = 10;
241 : 1 : hash[std::make_pair(uint64_t{42}, nC.d_nv)] = 12;
242 : :
243 : : // entries should be changed this time
244 [ - + ]: 1 : EXPECT_EQ(hash[std::make_pair(uint64_t{42}, nB.d_nv)], 10);
245 [ - + ]: 1 : EXPECT_EQ(hash[std::make_pair(uint64_t{42}, nC.d_nv)], 12);
246 [ - + ]: 1 : EXPECT_EQ(*hash.find(std::make_pair(uint64_t{42}, nB.d_nv)),
247 : 1 : std::make_pair(std::make_pair(uint64_t{42}, nB.d_nv), 10));
248 [ - + ]: 1 : EXPECT_EQ(*hash.find(std::make_pair(uint64_t{42}, nC.d_nv)),
249 : 1 : std::make_pair(std::make_pair(uint64_t{42}, nC.d_nv), 12));
250 : 1 : }
251 : :
252 : : } // namespace test
253 : : } // namespace cvc5::internal
|
