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