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