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::context::CDMap<>.
11 : : */
12 : :
13 : : #include <map>
14 : :
15 : : #include "base/check.h"
16 : : #include "context/cdhashmap.h"
17 : : #include "context/cdlist.h"
18 : : #include "test_context.h"
19 : :
20 : : namespace cvc5::internal {
21 : : namespace test {
22 : :
23 : : using cvc5::context::CDHashMap;
24 : : using cvc5::context::Context;
25 : :
26 : : class TestContextBlackCDHashMap : public TestContext
27 : : {
28 : : protected:
29 : : /** Returns the elements in a CDHashMap. */
30 : 26 : static std::map<int32_t, int32_t> get_elements(
31 : : const CDHashMap<int32_t, int32_t>& map)
32 : : {
33 : 52 : return std::map<int32_t, int32_t>{map.begin(), map.end()};
34 : : }
35 : :
36 : : /**
37 : : * Returns true if the elements in map are the same as expected.
38 : : * NOTE: This is mostly to help the type checker for matching expected within
39 : : * a ASSERT_*.
40 : : */
41 : 26 : static bool elements_are(const CDHashMap<int32_t, int32_t>& map,
42 : : const std::map<int32_t, int32_t>& expected)
43 : : {
44 : 26 : return get_elements(map) == expected;
45 : : }
46 : : };
47 : :
48 : 4 : TEST_F(TestContextBlackCDHashMap, simple_sequence)
49 : : {
50 : 1 : CDHashMap<int32_t, int32_t> map(d_context.get());
51 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {}));
52 : :
53 : 1 : map.insert(3, 4);
54 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}}));
55 : :
56 : : {
57 : 1 : d_context->push();
58 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}}));
59 : :
60 : 1 : map.insert(5, 6);
61 : 1 : map.insert(9, 8);
62 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
63 : :
64 : : {
65 : 1 : d_context->push();
66 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
67 : :
68 : 1 : map.insert(1, 2);
69 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
70 : :
71 : : {
72 : 1 : d_context->push();
73 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
74 : :
75 : 1 : map.insert(1, 45);
76 : :
77 [ - + ]: 1 : ASSERT_TRUE(
78 [ + - ]: 1 : elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}}));
79 : 1 : map.insert(23, 324);
80 : :
81 [ - + ]: 1 : ASSERT_TRUE(
82 [ + - ]: 1 : elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 324}}));
83 : 1 : d_context->pop();
84 : : }
85 : :
86 [ - + ]: 1 : ASSERT_TRUE(
87 [ + - ]: 1 : elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
88 : 1 : d_context->pop();
89 : : }
90 : :
91 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
92 : 1 : d_context->pop();
93 : : }
94 : :
95 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}}));
96 [ + - ]: 1 : }
97 : :
98 : 4 : TEST_F(TestContextBlackCDHashMap, simple_sequence_fewer_finds)
99 : : {
100 : : // no intervening find() in this one (under the theory that this could trigger
101 : : // a bug)
102 : 1 : CDHashMap<int, int> map(d_context.get());
103 : 1 : map.insert(3, 4);
104 : :
105 : : {
106 : 1 : d_context->push();
107 : :
108 : 1 : map.insert(5, 6);
109 : 1 : map.insert(9, 8);
110 : :
111 : : {
112 : 1 : d_context->push();
113 : :
114 : 1 : map.insert(1, 2);
115 : :
116 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
117 : : {
118 : 1 : d_context->push();
119 : 1 : d_context->pop();
120 : : }
121 : :
122 : 1 : d_context->pop();
123 : : }
124 : :
125 : 1 : d_context->pop();
126 : : }
127 [ + - ]: 1 : }
128 : :
129 : 4 : TEST_F(TestContextBlackCDHashMap, insert_at_context_level_zero)
130 : : {
131 : 1 : CDHashMap<int, int> map(d_context.get());
132 : :
133 : 1 : map.insert(3, 4);
134 : :
135 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}}));
136 : : {
137 : 1 : d_context->push();
138 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}}));
139 : :
140 : 1 : map.insert(5, 6);
141 : 1 : map.insert(9, 8);
142 : :
143 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
144 : :
145 : : {
146 : 1 : d_context->push();
147 : :
148 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
149 : :
150 : 1 : map.insert(1, 2);
151 : :
152 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
153 : :
154 [ - + ]: 1 : ASSERT_TRUE(
155 [ + - ]: 1 : elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
156 : :
157 : 1 : map.insert(23, 472);
158 : :
159 [ - + ]: 1 : ASSERT_TRUE(
160 [ + - ]: 1 : elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
161 : : {
162 : 1 : d_context->push();
163 : :
164 [ - + ]: 1 : ASSERT_TRUE(
165 [ + - ]: 1 : elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
166 : :
167 : 1 : map.insert(23, 1024);
168 : :
169 [ - + ]: 1 : ASSERT_TRUE(
170 [ + - ]: 1 : elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 1024}}));
171 : 1 : d_context->pop();
172 : : }
173 [ - + ]: 1 : ASSERT_TRUE(
174 [ + - ]: 1 : elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
175 : 1 : d_context->pop();
176 : : }
177 : :
178 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
179 : :
180 : 1 : map.insert(23, 477);
181 : :
182 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 477}}));
183 : 1 : d_context->pop();
184 : : }
185 : :
186 [ - + ][ + - ]: 1 : ASSERT_TRUE(elements_are(map, {{3, 4}}));
187 [ + - ]: 1 : }
188 : : } // namespace test
189 : : } // namespace cvc5::internal
|
