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