Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Morgan Deters, Clark Barrett, Andrew Reynolds
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Contains additional classes to store context dependent information
14 : : * for each term of type array.
15 : : */
16 : :
17 : : #include "theory/arrays/array_info.h"
18 : :
19 : : #include "util/statistics_registry.h"
20 : :
21 : : namespace cvc5::internal {
22 : : namespace theory {
23 : : namespace arrays {
24 : :
25 : 53993 : Info::Info(context::Context* c)
26 : 0 : : isNonLinear(c, false),
27 : 0 : rIntro1Applied(c, false),
28 : 53993 : modelRep(c, TNode()),
29 : 53993 : constArr(c, TNode()),
30 : 53993 : weakEquivPointer(c, TNode()),
31 : 53993 : weakEquivIndex(c, TNode()),
32 : 53993 : weakEquivSecondary(c, TNode()),
33 : 323958 : weakEquivSecondaryReason(c, TNode())
34 : : {
35 : 53993 : indices = new(true)CTNodeList(c);
36 : 53993 : stores = new(true)CTNodeList(c);
37 : 53993 : in_stores = new(true)CTNodeList(c);
38 : 53993 : }
39 : :
40 : 53737 : Info::~Info() {
41 : 53737 : indices->deleteSelf();
42 : 53737 : stores->deleteSelf();
43 : 53737 : in_stores->deleteSelf();
44 : 53737 : }
45 : :
46 : 49876 : ArrayInfo::ArrayInfo(StatisticsRegistry& sr,
47 : : context::Context* c,
48 : 49876 : std::string statisticsPrefix)
49 : : : ct(c),
50 : : info_map(),
51 : 49876 : d_mergeInfoTimer(sr.registerTimer(statisticsPrefix + "mergeInfoTimer")),
52 : : d_avgIndexListLength(
53 : 49876 : sr.registerAverage(statisticsPrefix + "avgIndexListLength")),
54 : : d_avgStoresListLength(
55 : 49876 : sr.registerAverage(statisticsPrefix + "avgStoresListLength")),
56 : : d_avgInStoresListLength(
57 : 49876 : sr.registerAverage(statisticsPrefix + "avgInStoresListLength")),
58 : 49876 : d_listsCount(sr.registerInt(statisticsPrefix + "listsCount")),
59 : 49876 : d_callsMergeInfo(sr.registerInt(statisticsPrefix + "callsMergeInfo")),
60 : 49876 : d_maxList(sr.registerInt(statisticsPrefix + "maxList")),
61 : : d_tableSize(sr.registerSize<CNodeInfoMap>(
62 : 99752 : statisticsPrefix + "infoTableSize", info_map))
63 : : {
64 : 49876 : emptyList = new(true) CTNodeList(ct);
65 : 49876 : emptyInfo = new Info(ct);
66 : 49876 : }
67 : :
68 : 49620 : ArrayInfo::~ArrayInfo() {
69 : 49620 : CNodeInfoMap::iterator it = info_map.begin();
70 [ + + ]: 53737 : for (; it != info_map.end(); ++it)
71 : : {
72 [ + - ]: 4117 : if((*it).second!= emptyInfo) {
73 [ + - ]: 4117 : delete (*it).second;
74 : : }
75 : : }
76 : 49620 : emptyList->deleteSelf();
77 [ + - ]: 49620 : delete emptyInfo;
78 : 49620 : }
79 : :
80 : 34593 : bool inList(const CTNodeList* l, const TNode el) {
81 : 34593 : CTNodeList::const_iterator it = l->begin();
82 [ + + ]: 192719 : for (; it != l->end(); ++it)
83 : : {
84 [ + + ]: 162002 : if(*it == el)
85 : 3876 : return true;
86 : : }
87 : 30717 : return false;
88 : : }
89 : :
90 : 609 : void printList (CTNodeList* list) {
91 : 609 : CTNodeList::const_iterator it = list->begin();
92 [ + - ]: 609 : Trace("arrays-info")<<" [ ";
93 [ + + ]: 1007 : for (; it != list->end(); ++it)
94 : : {
95 [ + - ]: 398 : Trace("arrays-info")<<(*it)<<" ";
96 : : }
97 [ + - ]: 609 : Trace("arrays-info")<<"] \n";
98 : 609 : }
99 : :
100 : 20601 : void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{
101 : 41202 : std::set<TNode> temp;
102 : 20601 : CTNodeList::const_iterator it;
103 [ + + ]: 67071 : for (it = la->begin(); it != la->end(); ++it)
104 : : {
105 : 46470 : temp.insert((*it));
106 : : }
107 : :
108 [ + + ]: 53518 : for (it = lb->begin(); it != lb->end(); ++it)
109 : : {
110 [ + + ]: 32917 : if(temp.count(*it) == 0) {
111 : 13295 : la->push_back(*it);
112 : : }
113 : : }
114 : 20601 : }
115 : :
116 : 34692 : void ArrayInfo::addIndex(const Node a, const TNode i) {
117 [ - + ][ - + ]: 34692 : Assert(a.getType().isArray());
[ - - ]
118 [ - + ][ - + ]: 34692 : Assert(!i.getType().isArray()); // temporary for flat arrays
[ - - ]
119 : :
120 [ + - ]: 34692 : Trace("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n";
121 : : CTNodeList* temp_indices;
122 : : Info* temp_info;
123 : :
124 : 34692 : CNodeInfoMap::iterator it = info_map.find(a);
125 [ + + ]: 34692 : if(it == info_map.end()) {
126 : 3334 : temp_info = new Info(ct);
127 : 3334 : temp_indices = temp_info->indices;
128 : 3334 : temp_indices->push_back(i);
129 : 3334 : info_map[a] = temp_info;
130 : : } else {
131 : 31358 : temp_indices = (*it).second->indices;
132 [ + + ]: 31358 : if (! inList(temp_indices, i)) {
133 : 27482 : temp_indices->push_back(i);
134 : : }
135 : : }
136 [ - + ]: 34692 : if(TraceIsOn("arrays-ind")) {
137 : 0 : printList((*(info_map.find(a))).second->indices);
138 : : }
139 : :
140 : 34692 : }
141 : :
142 : 1885 : void ArrayInfo::addStore(const Node a, const TNode st){
143 [ - + ][ - + ]: 1885 : Assert(a.getType().isArray());
[ - - ]
144 [ - + ][ - + ]: 1885 : Assert(st.getKind() == Kind::STORE); // temporary for flat arrays
[ - - ]
145 : :
146 : : CTNodeList* temp_store;
147 : : Info* temp_info;
148 : :
149 : 1885 : CNodeInfoMap::iterator it = info_map.find(a);
150 [ - + ]: 1885 : if(it == info_map.end()) {
151 : 0 : temp_info = new Info(ct);
152 : 0 : temp_store = temp_info->stores;
153 : 0 : temp_store->push_back(st);
154 : 0 : info_map[a]=temp_info;
155 : : } else {
156 : 1885 : temp_store = (*it).second->stores;
157 [ + - ]: 1885 : if(! inList(temp_store, st)) {
158 : 1885 : temp_store->push_back(st);
159 : : }
160 : : }
161 : 1885 : };
162 : :
163 : :
164 : 1885 : void ArrayInfo::addInStore(const TNode a, const TNode b){
165 [ + - ]: 1885 : Trace("arrays-addinstore")<<"Arrays::addInStore "<<a<<" ~ "<<b<<"\n";
166 [ - + ][ - + ]: 1885 : Assert(a.getType().isArray());
[ - - ]
167 [ - + ][ - + ]: 1885 : Assert(b.getType().isArray());
[ - - ]
168 : :
169 : : CTNodeList* temp_inst;
170 : : Info* temp_info;
171 : :
172 : 1885 : CNodeInfoMap::iterator it = info_map.find(a);
173 [ + + ]: 1885 : if(it == info_map.end()) {
174 : 535 : temp_info = new Info(ct);
175 : 535 : temp_inst = temp_info->in_stores;
176 : 535 : temp_inst->push_back(b);
177 : 535 : info_map[a] = temp_info;
178 : : } else {
179 : 1350 : temp_inst = (*it).second->in_stores;
180 [ + - ]: 1350 : if(! inList(temp_inst, b)) {
181 : 1350 : temp_inst->push_back(b);
182 : : }
183 : : }
184 : 1885 : };
185 : :
186 : :
187 : 2867 : void ArrayInfo::setNonLinear(const TNode a) {
188 [ - + ][ - + ]: 2867 : Assert(a.getType().isArray());
[ - - ]
189 : : Info* temp_info;
190 : 2867 : CNodeInfoMap::iterator it = info_map.find(a);
191 [ + + ]: 2867 : if(it == info_map.end()) {
192 : 6 : temp_info = new Info(ct);
193 : 6 : temp_info->isNonLinear = true;
194 : 6 : info_map[a] = temp_info;
195 : : } else {
196 : 2861 : (*it).second->isNonLinear = true;
197 : : }
198 : :
199 : 2867 : }
200 : :
201 : 0 : void ArrayInfo::setRIntro1Applied(const TNode a) {
202 : 0 : Assert(a.getType().isArray());
203 : : Info* temp_info;
204 : 0 : CNodeInfoMap::iterator it = info_map.find(a);
205 [ - - ]: 0 : if(it == info_map.end()) {
206 : 0 : temp_info = new Info(ct);
207 : 0 : temp_info->rIntro1Applied = true;
208 : 0 : info_map[a] = temp_info;
209 : : } else {
210 : 0 : (*it).second->rIntro1Applied = true;
211 : : }
212 : :
213 : 0 : }
214 : :
215 : 1885 : void ArrayInfo::setModelRep(const TNode a, const TNode b) {
216 [ - + ][ - + ]: 1885 : Assert(a.getType().isArray());
[ - - ]
217 : : Info* temp_info;
218 : 1885 : CNodeInfoMap::iterator it = info_map.find(a);
219 [ - + ]: 1885 : if(it == info_map.end()) {
220 : 0 : temp_info = new Info(ct);
221 : 0 : temp_info->modelRep = b;
222 : 0 : info_map[a] = temp_info;
223 : : } else {
224 : 1885 : (*it).second->modelRep = b;
225 : : }
226 : :
227 : 1885 : }
228 : :
229 : 43 : void ArrayInfo::setConstArr(const TNode a, const TNode constArr) {
230 [ - + ][ - + ]: 43 : Assert(a.getType().isArray());
[ - - ]
231 : : Info* temp_info;
232 : 43 : CNodeInfoMap::iterator it = info_map.find(a);
233 [ + + ]: 43 : if(it == info_map.end()) {
234 : 39 : temp_info = new Info(ct);
235 : 39 : temp_info->constArr = constArr;
236 : 39 : info_map[a] = temp_info;
237 : : } else {
238 : 4 : (*it).second->constArr = constArr;
239 : : }
240 : 43 : }
241 : :
242 : 0 : void ArrayInfo::setWeakEquivPointer(const TNode a, const TNode pointer) {
243 : 0 : Assert(a.getType().isArray());
244 : : Info* temp_info;
245 : 0 : CNodeInfoMap::iterator it = info_map.find(a);
246 [ - - ]: 0 : if(it == info_map.end()) {
247 : 0 : temp_info = new Info(ct);
248 : 0 : temp_info->weakEquivPointer = pointer;
249 : 0 : info_map[a] = temp_info;
250 : : } else {
251 : 0 : (*it).second->weakEquivPointer = pointer;
252 : : }
253 : 0 : }
254 : :
255 : 0 : void ArrayInfo::setWeakEquivIndex(const TNode a, const TNode index) {
256 : 0 : Assert(a.getType().isArray());
257 : : Info* temp_info;
258 : 0 : CNodeInfoMap::iterator it = info_map.find(a);
259 [ - - ]: 0 : if(it == info_map.end()) {
260 : 0 : temp_info = new Info(ct);
261 : 0 : temp_info->weakEquivIndex = index;
262 : 0 : info_map[a] = temp_info;
263 : : } else {
264 : 0 : (*it).second->weakEquivIndex = index;
265 : : }
266 : 0 : }
267 : :
268 : 0 : void ArrayInfo::setWeakEquivSecondary(const TNode a, const TNode secondary) {
269 : 0 : Assert(a.getType().isArray());
270 : : Info* temp_info;
271 : 0 : CNodeInfoMap::iterator it = info_map.find(a);
272 [ - - ]: 0 : if(it == info_map.end()) {
273 : 0 : temp_info = new Info(ct);
274 : 0 : temp_info->weakEquivSecondary = secondary;
275 : 0 : info_map[a] = temp_info;
276 : : } else {
277 : 0 : (*it).second->weakEquivSecondary = secondary;
278 : : }
279 : 0 : }
280 : :
281 : 0 : void ArrayInfo::setWeakEquivSecondaryReason(const TNode a, const TNode reason) {
282 : 0 : Assert(a.getType().isArray());
283 : : Info* temp_info;
284 : 0 : CNodeInfoMap::iterator it = info_map.find(a);
285 [ - - ]: 0 : if(it == info_map.end()) {
286 : 0 : temp_info = new Info(ct);
287 : 0 : temp_info->weakEquivSecondaryReason = reason;
288 : 0 : info_map[a] = temp_info;
289 : : } else {
290 : 0 : (*it).second->weakEquivSecondaryReason = reason;
291 : : }
292 : 0 : }
293 : :
294 : : /**
295 : : * Returns the information associated with TNode a
296 : : */
297 : :
298 : 0 : const Info* ArrayInfo::getInfo(const TNode a) const{
299 : 0 : CNodeInfoMap::const_iterator it = info_map.find(a);
300 : :
301 [ - - ]: 0 : if(it!= info_map.end()) {
302 : 0 : return (*it).second;
303 : : }
304 : 0 : return emptyInfo;
305 : : }
306 : :
307 : 56144 : const bool ArrayInfo::isNonLinear(const TNode a) const
308 : : {
309 : 56144 : CNodeInfoMap::const_iterator it = info_map.find(a);
310 : :
311 [ + + ]: 56144 : if(it!= info_map.end()) {
312 : 54385 : return (*it).second->isNonLinear;
313 : : }
314 : 1759 : return false;
315 : : }
316 : :
317 : 0 : const bool ArrayInfo::rIntro1Applied(const TNode a) const
318 : : {
319 : 0 : CNodeInfoMap::const_iterator it = info_map.find(a);
320 : :
321 [ - - ]: 0 : if(it!= info_map.end()) {
322 : 0 : return (*it).second->rIntro1Applied;
323 : : }
324 : 0 : return false;
325 : : }
326 : :
327 : 0 : const TNode ArrayInfo::getModelRep(const TNode a) const
328 : : {
329 : 0 : CNodeInfoMap::const_iterator it = info_map.find(a);
330 : :
331 [ - - ]: 0 : if(it!= info_map.end()) {
332 : 0 : return (*it).second->modelRep;
333 : : }
334 : 0 : return TNode();
335 : : }
336 : :
337 : 65098 : const TNode ArrayInfo::getConstArr(const TNode a) const
338 : : {
339 : 65098 : CNodeInfoMap::const_iterator it = info_map.find(a);
340 : :
341 [ + + ]: 65098 : if(it!= info_map.end()) {
342 : 62860 : return (*it).second->constArr;
343 : : }
344 : 2238 : return TNode();
345 : : }
346 : :
347 : 0 : const TNode ArrayInfo::getWeakEquivPointer(const TNode a) const
348 : : {
349 : 0 : CNodeInfoMap::const_iterator it = info_map.find(a);
350 : :
351 [ - - ]: 0 : if(it!= info_map.end()) {
352 : 0 : return (*it).second->weakEquivPointer;
353 : : }
354 : 0 : return TNode();
355 : : }
356 : :
357 : 0 : const TNode ArrayInfo::getWeakEquivIndex(const TNode a) const
358 : : {
359 : 0 : CNodeInfoMap::const_iterator it = info_map.find(a);
360 : :
361 [ - - ]: 0 : if(it!= info_map.end()) {
362 : 0 : return (*it).second->weakEquivIndex;
363 : : }
364 : 0 : return TNode();
365 : : }
366 : :
367 : 0 : const TNode ArrayInfo::getWeakEquivSecondary(const TNode a) const
368 : : {
369 : 0 : CNodeInfoMap::const_iterator it = info_map.find(a);
370 : :
371 [ - - ]: 0 : if(it!= info_map.end()) {
372 : 0 : return (*it).second->weakEquivSecondary;
373 : : }
374 : 0 : return TNode();
375 : : }
376 : :
377 : 0 : const TNode ArrayInfo::getWeakEquivSecondaryReason(const TNode a) const
378 : : {
379 : 0 : CNodeInfoMap::const_iterator it = info_map.find(a);
380 : :
381 [ - - ]: 0 : if(it!= info_map.end()) {
382 : 0 : return (*it).second->weakEquivSecondaryReason;
383 : : }
384 : 0 : return TNode();
385 : : }
386 : :
387 : 18528 : const CTNodeList* ArrayInfo::getIndices(const TNode a) const{
388 : 18528 : CNodeInfoMap::const_iterator it = info_map.find(a);
389 [ + + ]: 18528 : if(it!= info_map.end()) {
390 : 17409 : return (*it).second->indices;
391 : : }
392 : 1119 : return emptyList;
393 : : }
394 : :
395 : 63699 : const CTNodeList* ArrayInfo::getStores(const TNode a) const{
396 : 63699 : CNodeInfoMap::const_iterator it = info_map.find(a);
397 [ + + ]: 63699 : if(it!= info_map.end()) {
398 : 61706 : return (*it).second->stores;
399 : : }
400 : 1993 : return emptyList;
401 : : }
402 : :
403 : 57356 : const CTNodeList* ArrayInfo::getInStores(const TNode a) const{
404 : 57356 : CNodeInfoMap::const_iterator it = info_map.find(a);
405 [ + + ]: 57356 : if(it!= info_map.end()) {
406 : 56237 : return (*it).second->in_stores;
407 : : }
408 : 1119 : return emptyList;
409 : : }
410 : :
411 : :
412 : 7600 : void ArrayInfo::mergeInfo(const TNode a, const TNode b){
413 : : // can't have assertion that find(b) = a !
414 : 7600 : TimerStat::CodeTimer codeTimer(d_mergeInfoTimer);
415 : 7600 : ++d_callsMergeInfo;
416 : :
417 [ + - ]: 7600 : Trace("arrays-mergei")<<"Arrays::mergeInfo merging "<<a<<"\n";
418 [ + - ]: 7600 : Trace("arrays-mergei")<<" and "<<b<<"\n";
419 : :
420 : 7600 : CNodeInfoMap::iterator ita = info_map.find(a);
421 : 7600 : CNodeInfoMap::iterator itb = info_map.find(b);
422 : :
423 [ + + ]: 7600 : if(ita != info_map.end()) {
424 [ + - ]: 7214 : Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<a<<"\n";
425 [ - + ]: 7214 : if(TraceIsOn("arrays-mergei"))
426 : 0 : (*ita).second->print();
427 : :
428 [ + + ]: 7214 : if(itb != info_map.end()) {
429 [ + - ]: 6664 : Trace("arrays-mergei")<<"Arrays::mergeInfo info "<<b<<"\n";
430 [ - + ]: 6664 : if(TraceIsOn("arrays-mergei"))
431 : 0 : (*itb).second->print();
432 : :
433 : 6664 : CTNodeList* lista_i = (*ita).second->indices;
434 : 6664 : CTNodeList* lista_st = (*ita).second->stores;
435 : 6664 : CTNodeList* lista_inst = (*ita).second->in_stores;
436 : :
437 : :
438 : 6664 : CTNodeList* listb_i = (*itb).second->indices;
439 : 6664 : CTNodeList* listb_st = (*itb).second->stores;
440 : 6664 : CTNodeList* listb_inst = (*itb).second->in_stores;
441 : :
442 : 6664 : mergeLists(lista_i, listb_i);
443 : 6664 : mergeLists(lista_st, listb_st);
444 : 6664 : mergeLists(lista_inst, listb_inst);
445 : :
446 : : /* sketchy stats */
447 : :
448 : : //FIXME
449 : 6664 : int s = 0;//lista_i->size();
450 : 6664 : d_maxList.maxAssign(s);
451 : :
452 : :
453 [ - + ]: 6664 : if(s!= 0) {
454 : 0 : d_avgIndexListLength << s;
455 : 0 : ++d_listsCount;
456 : : }
457 : 6664 : s = lista_st->size();
458 : 6664 : d_maxList.maxAssign(s);
459 [ + + ]: 6664 : if(s!= 0) {
460 : 4482 : d_avgStoresListLength << s;
461 : 4482 : ++d_listsCount;
462 : : }
463 : :
464 : 6664 : s = lista_inst->size();
465 : 6664 : d_maxList.maxAssign(s);
466 [ + + ]: 6664 : if(s!=0) {
467 : 3645 : d_avgInStoresListLength << s;
468 : 3645 : ++d_listsCount;
469 : : }
470 : :
471 : : /* end sketchy stats */
472 : :
473 : : }
474 : :
475 : : } else {
476 [ + - ]: 386 : Trace("arrays-mergei")<<" First element has no info \n";
477 [ + + ]: 386 : if(itb != info_map.end()) {
478 [ + - ]: 203 : Trace("arrays-mergei")<<" adding second element's info \n";
479 : 203 : (*itb).second->print();
480 : :
481 : 203 : CTNodeList* listb_i = (*itb).second->indices;
482 : 203 : CTNodeList* listb_st = (*itb).second->stores;
483 : 203 : CTNodeList* listb_inst = (*itb).second->in_stores;
484 : :
485 : 203 : Info* temp_info = new Info(ct);
486 : :
487 : 203 : mergeLists(temp_info->indices, listb_i);
488 : 203 : mergeLists(temp_info->stores, listb_st);
489 : 203 : mergeLists(temp_info->in_stores, listb_inst);
490 : 203 : info_map[a] = temp_info;
491 : :
492 : : } else {
493 [ + - ]: 183 : Trace("arrays-mergei")<<" Second element has no info \n";
494 : : }
495 : :
496 : : }
497 [ + - ]: 7600 : Trace("arrays-mergei")<<"Arrays::mergeInfo done \n";
498 : :
499 : 7600 : }
500 : :
501 : : } // namespace arrays
502 : : } // namespace theory
503 : : } // namespace cvc5::internal
|
