GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arrays/array_info.cpp Lines: 212 311 68.2 %
Date: 2021-03-23 Branches: 300 978 30.7 %

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