1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 parray.cpp
7
8 Abstract:
9
10 Test persistent arrays.
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2011-02-23.
15
16 Revision History:
17
18 --*/
19 #include "util/parray.h"
20 #include "util/small_object_allocator.h"
21 #include "ast/ast.h"
22
23 template<bool PRESERVE_ROOTS>
24 struct int_parray_config {
25 typedef int value;
26 typedef dummy_value_manager<int> value_manager;
27 typedef small_object_allocator allocator;
28 static const bool ref_count = false;
29 static const bool preserve_roots = PRESERVE_ROOTS;
30 static const unsigned max_trail_sz = 8;
31 static const unsigned factor = 2;
32 };
33
34
35 template<bool PRESERVE_ROOTS>
tst1()36 static void tst1() {
37 typedef parray_manager<int_parray_config<PRESERVE_ROOTS> > int_parray_manager;
38 typedef typename int_parray_manager::ref int_array;
39
40 dummy_value_manager<int> vm;
41 small_object_allocator a;
42 int_parray_manager m(vm, a);
43
44 int_array a1;
45 int_array a2;
46 int_array a3;
47
48 m.mk(a1);
49 ENSURE(m.size(a1) == 0);
50 m.push_back(a1, 10, a2);
51 TRACE("parray",
52 m.display_info(tout, a1); tout << "\n";
53 m.display_info(tout, a2); tout << "\n";);
54 ENSURE(m.size(a1) == 0);
55 ENSURE(m.size(a2) == 1);
56 m.push_back(a1, 20, a1);
57 m.push_back(a1, 30, a1);
58 TRACE("parray",
59 m.display_info(tout, a1); tout << "\n";
60 m.display_info(tout, a2); tout << "\n";);
61 ENSURE(m.get(a1, 0) == 20);
62 ENSURE(m.get(a1, 1) == 30);
63 ENSURE(m.get(a2, 0) == 10);
64 ENSURE(m.size(a1) == 2);
65 ENSURE(m.size(a2) == 1);
66 ENSURE(m.size(a3) == 0);
67 m.push_back(a2, 100, a3);
68 ENSURE(m.size(a3) == 2);
69 ENSURE(m.get(a3, 0) == 10);
70 ENSURE(m.get(a3, 1) == 100);
71 TRACE("parray",
72 m.display_info(tout, a1); tout << "\n";
73 m.display_info(tout, a2); tout << "\n";
74 m.display_info(tout, a3); tout << "\n";);
75 m.push_back(a2, 50);
76 ENSURE(m.get(a2, 0) == 10);
77 ENSURE(m.get(a2, 1) == 50);
78 ENSURE(m.size(a2) == 2);
79 TRACE("parray",
80 m.display_info(tout, a1); tout << "\n";
81 m.display_info(tout, a2); tout << "\n";
82 m.display_info(tout, a3); tout << "\n";);
83 m.del(a1);
84 m.del(a2);
85 m.del(a3);
86 }
87
88 template<bool PRESERVE_ROOTS>
tst2()89 static void tst2() {
90 typedef parray_manager<int_parray_config<PRESERVE_ROOTS> > int_parray_manager;
91 typedef typename int_parray_manager::ref int_array;
92
93 TRACE("parray", tout << "tst2\n";);
94 dummy_value_manager<int> vm;
95 small_object_allocator a;
96 int_parray_manager m(vm, a);
97
98 int_array a1;
99 int_array a2;
100
101 for (unsigned i = 0; i < 100; i++)
102 m.push_back(a1, i);
103 ENSURE(m.size(a1) == 100);
104 m.push_back(a1, 100, a2);
105 for (unsigned i = 0; i < 10; i++)
106 m.push_back(a2, i+101);
107 TRACE("parray",
108 m.display_info(tout, a1); tout << "\n";
109 m.display_info(tout, a2); tout << "\n";);
110 ENSURE(m.get(a1, 0) == 0);
111 TRACE("parray",
112 m.display_info(tout, a1); tout << "\n";
113 m.display_info(tout, a2); tout << "\n";);
114 for (unsigned i = 0; i < m.size(a1); i++) {
115 ENSURE(static_cast<unsigned>(m.get(a1, i)) == i);
116 }
117 for (unsigned i = 0; i < m.size(a2); i++) {
118 ENSURE(static_cast<unsigned>(m.get(a2, i)) == i);
119 }
120 TRACE("parray",
121 m.display_info(tout, a1); tout << "\n";
122 m.display_info(tout, a2); tout << "\n";);
123 m.unshare(a1);
124 TRACE("parray",
125 m.display_info(tout, a1); tout << "\n";
126 m.display_info(tout, a2); tout << "\n";);
127 m.del(a1);
128 m.del(a2);
129 }
130
131 template<bool PRESERVE_ROOTS>
tst3()132 static void tst3() {
133 typedef parray_manager<int_parray_config<PRESERVE_ROOTS> > int_parray_manager;
134 typedef typename int_parray_manager::ref int_array;
135
136 TRACE("parray", tout << "tst3\n";);
137 dummy_value_manager<int> vm;
138 small_object_allocator a;
139 int_parray_manager m(vm, a);
140
141 int_array a1;
142 int_array a2;
143 int_array a3;
144 int_array a4;
145
146 for (unsigned i = 0; i < 20; i++)
147 m.push_back(a1, i);
148 ENSURE(m.size(a1) == 20);
149 m.set(a1, 0, 1, a2);
150 for (unsigned i = 1; i < 20; i++) {
151 if (i == 6) {
152 m.copy(a2, a3);
153 m.pop_back(a3);
154 m.pop_back(a3);
155 m.push_back(a3, 40);
156 }
157 m.set(a2, i, i+1);
158 }
159 m.pop_back(a2, a4);
160 m.pop_back(a4);
161 m.push_back(a4, 30);
162
163 for (unsigned i = 0; i < 20; i++) {
164 ENSURE(static_cast<unsigned>(m.get(a2, i)) == i+1);
165 }
166 TRACE("parray",
167 m.display_info(tout, a1); tout << "\n";
168 m.display_info(tout, a2); tout << "\n";
169 m.display_info(tout, a3); tout << "\n";
170 m.display_info(tout, a4); tout << "\n";
171 );
172 ENSURE(m.get(a1, 10) == 10);
173 TRACE("parray",
174 tout << "after rerooting...\n";
175 m.display_info(tout, a1); tout << "\n";
176 m.display_info(tout, a2); tout << "\n";
177 m.display_info(tout, a3); tout << "\n";
178 m.display_info(tout, a4); tout << "\n";
179 );
180 ENSURE(m.size(a1) == 20);
181 ENSURE(m.size(a2) == 20);
182 ENSURE(m.size(a3) == 19);
183 ENSURE(m.size(a4) == 19);
184 for (unsigned i = 0; i < 20; i++) {
185 ENSURE(static_cast<unsigned>(m.get(a1, i)) == i);
186 ENSURE(static_cast<unsigned>(m.get(a2, i)) == i+1);
187 ENSURE(i >= 18 || static_cast<unsigned>(m.get(a4, i)) == i+1);
188 ENSURE(i >= 6 || static_cast<unsigned>(m.get(a3, i)) == i+1);
189 ENSURE(!(6 <= i && i <= 17) || static_cast<unsigned>(m.get(a3, i)) == i);
190 }
191 ENSURE(m.get(a4, 18) == 30);
192 ENSURE(m.get(a3, 18) == 40);
193 TRACE("parray",
194 tout << "after many gets...\n";
195 m.display_info(tout, a1); tout << "\n";
196 m.display_info(tout, a2); tout << "\n";
197 m.display_info(tout, a3); tout << "\n";
198 m.display_info(tout, a4); tout << "\n";
199 );
200 m.unshare(a1);
201 TRACE("parray",
202 tout << "after unshare...\n";
203 m.display_info(tout, a1); tout << "\n";
204 m.display_info(tout, a2); tout << "\n";
205 m.display_info(tout, a3); tout << "\n";
206 m.display_info(tout, a4); tout << "\n";
207 );
208 m.reroot(a4);
209 TRACE("parray",
210 tout << "after reroot...\n";
211 m.display_info(tout, a1); tout << "\n";
212 m.display_info(tout, a2); tout << "\n";
213 m.display_info(tout, a3); tout << "\n";
214 m.display_info(tout, a4); tout << "\n";
215 );
216 m.unshare(a2);
217 TRACE("parray",
218 tout << "after second unshare...\n";
219 m.display_info(tout, a1); tout << "\n";
220 m.display_info(tout, a2); tout << "\n";
221 m.display_info(tout, a3); tout << "\n";
222 m.display_info(tout, a4); tout << "\n";
223 );
224 m.del(a1);
225 m.del(a2);
226 m.del(a3);
227 m.del(a4);
228 }
229
230 #if 0
231 // Moved to ast.cpp
232 struct expr_array_config {
233 typedef expr * value;
234 typedef ast_manager value_manager;
235 typedef small_object_allocator allocator;
236 static const bool ref_count = true;
237 static const bool preserve_roots = true;
238 static const unsigned max_trail_sz = 8;
239 static const unsigned factor = 2;
240 };
241
242 typedef parray_manager<expr_array_config> expr_array_manager;
243 typedef expr_array_manager::ref expr_array;
244
245 static void tst4() {
246 TRACE("parray", tout << "tst4\n";);
247 ast_manager m;
248 expr_array_manager m2(m, m.get_allocator());
249
250 expr_array a1;
251 expr_array a2;
252
253 expr * v0 = m.mk_var(0, m.mk_bool_sort());
254 expr * v1 = m.mk_var(1, m.mk_bool_sort());
255 expr * v2 = m.mk_var(2, m.mk_bool_sort());
256 expr * v3 = m.mk_var(3, m.mk_bool_sort());
257
258 m2.push_back(a1, v0);
259 m2.push_back(a1, v1);
260 m2.push_back(a1, v2, a2);
261 m2.push_back(a1, v3);
262 m2.push_back(a2, v2);
263 m2.pop_back(a1);
264 TRACE("parray",
265 m2.display_info(tout, a1); tout << "\n";
266 m2.display_info(tout, a2); tout << "\n";
267 );
268 m2.reroot(a1);
269 TRACE("parray",
270 m2.display_info(tout, a1); tout << "\n";
271 m2.display_info(tout, a2); tout << "\n";
272 );
273 m2.del(a1);
274 m2.del(a2);
275 }
276 #endif
277
tst5()278 static void tst5() {
279 ast_manager m;
280 expr_array a1;
281 expr_array a2;
282
283 m.mk(a1);
284 for (unsigned i = 0; i < 100; i++) {
285 m.push_back(a1, m.mk_var(i, m.mk_bool_sort()));
286 }
287
288 unsigned long long mem = memory::get_max_used_memory();
289 std::cout << "max. heap size: " << static_cast<double>(mem)/static_cast<double>(1024*1024) << " Mbytes\n";
290
291 m.copy(a1, a2);
292
293 for (unsigned i = 0; i < 1000000; i++) {
294 m.set(a1, i % 100, m.mk_var(rand() % 100, m.mk_bool_sort()));
295 }
296
297 mem = memory::get_max_used_memory();
298 std::cout << "max. heap size: " << static_cast<double>(mem)/static_cast<double>(1024*1024) << " Mbytes\n";
299
300 m.del(a2);
301 m.del(a1);
302 }
303
tst_parray()304 void tst_parray() {
305 // enable_trace("parray_mem");
306 tst1<true>();
307 tst2<true>();
308 tst3<true>();
309 tst1<false>();
310 tst2<false>();
311 tst3<false>();
312 // tst4();
313 tst5();
314 }
315