GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arrays/array_info.h Lines: 14 14 100.0 %
Date: 2021-03-23 Branches: 22 56 39.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file array_info.h
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
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__ARRAYS__ARRAY_INFO_H
19
#define CVC4__THEORY__ARRAYS__ARRAY_INFO_H
20
21
#include <tuple>
22
#include <unordered_map>
23
24
#include "context/backtrackable.h"
25
#include "context/cdlist.h"
26
#include "expr/node.h"
27
#include "util/statistics_registry.h"
28
#include "util/stats_timer.h"
29
30
namespace CVC4 {
31
namespace theory {
32
namespace arrays {
33
34
typedef context::CDList<TNode> CTNodeList;
35
using RowLemmaType = std::tuple<TNode, TNode, TNode, TNode>;
36
37
struct RowLemmaTypeHashFunction {
38
90000
  size_t operator()(const RowLemmaType& q) const {
39
180000
    TNode n1, n2, n3, n4;
40
90000
    std::tie(n1, n2, n3, n4) = q;
41
90000
    return (size_t) (n1.getId()*0x9e3779b9 + n2.getId()*0x30000059 +
42
180000
        n3.getId()*0x60000005 + n4.getId()*0x07FFFFFF);
43
44
  }
45
};/* struct RowLemmaTypeHashFunction */
46
47
void printList (CTNodeList* list);
48
void printList( List<TNode>* list);
49
50
bool inList(const CTNodeList* l, const TNode el);
51
52
/**
53
 * Small class encapsulating the information
54
 * in the map. It's a class and not a struct to
55
 * call the destructor.
56
 */
57
58
class Info {
59
public:
60
  context::CDO<bool> isNonLinear;
61
  context::CDO<bool> rIntro1Applied;
62
  context::CDO<TNode> modelRep;
63
  context::CDO<TNode> constArr;
64
  context::CDO<TNode> weakEquivPointer;
65
  context::CDO<TNode> weakEquivIndex;
66
  context::CDO<TNode> weakEquivSecondary;
67
  context::CDO<TNode> weakEquivSecondaryReason;
68
  CTNodeList* indices;
69
  CTNodeList* stores;
70
  CTNodeList* in_stores;
71
72
  Info(context::Context* c, Backtracker<TNode>* bck);
73
  ~Info();
74
75
  /**
76
   * prints the information
77
   */
78
125
  void print() const {
79
125
    Assert(indices != NULL && stores != NULL && in_stores != NULL);
80
125
    Trace("arrays-info")<<"  indices   ";
81
125
    printList(indices);
82
125
    Trace("arrays-info")<<"  stores ";
83
125
    printList(stores);
84
125
    Trace("arrays-info")<<"  in_stores ";
85
125
    printList(in_stores);
86
125
  }
87
};/* class Info */
88
89
90
typedef std::unordered_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
91
92
/**
93
 * Class keeping track of the following information for canonical
94
 * representatives of type array [a] :
95
 *    indices at which it is being read (all i for which there is a
96
 *            term of the form SELECT a i)
97
 *    all store terms in the congruence class
98
 *    stores in which it appears (terms of the form STORE a _ _ )
99
 *
100
 */
101
class ArrayInfo {
102
private:
103
  context::Context* ct;
104
  Backtracker<TNode>* bck;
105
  CNodeInfoMap info_map;
106
107
  CTNodeList* emptyList;
108
109
  /* == STATISTICS == */
110
111
  /** time spent in preregisterTerm() */
112
  TimerStat d_mergeInfoTimer;
113
  AverageStat d_avgIndexListLength;
114
  AverageStat d_avgStoresListLength;
115
  AverageStat d_avgInStoresListLength;
116
  IntStat d_listsCount;
117
  IntStat d_callsMergeInfo;
118
  IntStat d_maxList;
119
  SizeStat<CNodeInfoMap > d_tableSize;
120
121
  /**
122
   * checks if a certain element is in the list l
123
   * FIXME: better way to check for duplicates?
124
   */
125
126
  /**
127
   * helper method that merges two lists into the first
128
   * without adding duplicates
129
   */
130
  void mergeLists(CTNodeList* la, const CTNodeList* lb) const;
131
132
public:
133
  const Info* emptyInfo;
134
/*
135
  ArrayInfo(): ct(NULl), info
136
    d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
137
    d_avgIndexListLength("theory::arrays::avgIndexListLength"),
138
    d_avgStoresListLength("theory::arrays::avgStoresListLength"),
139
    d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
140
    d_listsCount("theory::arrays::listsCount",0),
141
    d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
142
    d_maxList("theory::arrays::maxList",0),
143
    d_tableSize("theory::arrays::infoTableSize", info_map) {
144
  currentStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
145
  currentStatisticsRegistry()->registerStat(&d_avgIndexListLength);
146
  currentStatisticsRegistry()->registerStat(&d_avgStoresListLength);
147
  currentStatisticsRegistry()->registerStat(&d_avgInStoresListLength);
148
  currentStatisticsRegistry()->registerStat(&d_listsCount);
149
  currentStatisticsRegistry()->registerStat(&d_callsMergeInfo);
150
  currentStatisticsRegistry()->registerStat(&d_maxList);
151
  currentStatisticsRegistry()->registerStat(&d_tableSize);
152
  }*/
153
154
  ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix = "");
155
156
  ~ArrayInfo();
157
158
  /**
159
   * adds the node a to the map if it does not exist
160
   * and it initializes the info. checks for duplicate i's
161
   */
162
  void addIndex(const Node a, const TNode i);
163
  void addStore(const Node a, const TNode st);
164
  void addInStore(const TNode a, const TNode st);
165
166
  void setNonLinear(const TNode a);
167
  void setRIntro1Applied(const TNode a);
168
  void setModelRep(const TNode a, const TNode rep);
169
170
  void setConstArr(const TNode a, const TNode constArr);
171
  void setWeakEquivPointer(const TNode a, const TNode pointer);
172
  void setWeakEquivIndex(const TNode a, const TNode index);
173
  void setWeakEquivSecondary(const TNode a, const TNode secondary);
174
  void setWeakEquivSecondaryReason(const TNode a, const TNode reason);
175
  /**
176
   * Returns the information associated with TNode a
177
   */
178
179
  const Info* getInfo(const TNode a) const;
180
181
  const bool isNonLinear(const TNode a) const;
182
183
  const bool rIntro1Applied(const TNode a) const;
184
185
  const TNode getModelRep(const TNode a) const;
186
187
  const TNode getConstArr(const TNode a) const;
188
  const TNode getWeakEquivPointer(const TNode a) const;
189
  const TNode getWeakEquivIndex(const TNode a) const;
190
  const TNode getWeakEquivSecondary(const TNode a) const;
191
  const TNode getWeakEquivSecondaryReason(const TNode a) const;
192
193
  const CTNodeList* getIndices(const TNode a) const;
194
195
  const CTNodeList* getStores(const TNode a) const;
196
197
  const CTNodeList* getInStores(const TNode a) const;
198
199
  /**
200
   * merges the information of  nodes a and b
201
   * the nodes do not have to actually be in the map.
202
   * pre-condition
203
   *  a should be the canonical representative of b
204
   */
205
  void mergeInfo(const TNode a, const TNode b);
206
};/* class ArrayInfo */
207
208
}/* CVC4::theory::arrays namespace */
209
}/* CVC4::theory namespace */
210
}/* CVC4 namespace */
211
212
#endif /* CVC4__THEORY__ARRAYS__ARRAY_INFO_H */