GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/equality_engine_types.h Lines: 61 81 75.3 %
Date: 2021-03-22 Branches: 11 34 32.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file equality_engine_types.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Andrew Reynolds, Haniel Barbosa
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H
21
#define CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H
22
23
#include <string>
24
#include <iostream>
25
#include <sstream>
26
27
#include "util/hash.h"
28
29
namespace CVC4 {
30
namespace theory {
31
namespace eq {
32
33
/** Default type for the size of the sizes (size_t replacement) */
34
typedef uint32_t DefaultSizeType;
35
36
/** Id of the node */
37
typedef DefaultSizeType EqualityNodeId;
38
39
/** Id of the use list */
40
typedef DefaultSizeType UseListNodeId;
41
42
/** The trigger ids */
43
typedef DefaultSizeType TriggerId;
44
45
/** The equality edge ids */
46
typedef DefaultSizeType EqualityEdgeId;
47
48
/** The null node */
49
static const EqualityNodeId null_id = (EqualityNodeId)(-1);
50
51
/** The null use list node */
52
static const EqualityNodeId null_uselist_id = (EqualityNodeId)(-1);
53
54
/** The null trigger */
55
static const TriggerId null_trigger = (TriggerId)(-1);
56
57
/** The null edge id */
58
static const EqualityEdgeId null_edge = (EqualityEdgeId)(-1);
59
60
/**
61
 * A reason for a merge. Either an equality x = y, a merge of two
62
 * function applications f(x1, x2), f(y1, y2) due to congruence,
63
 * or a merge of an equality to false due to both sides being
64
 * (different) constants.
65
 */
66
enum MergeReasonType
67
{
68
  /** Terms were merged due to congruence */
69
  MERGED_THROUGH_CONGRUENCE,
70
  /** Terms were merged due to an assumption */
71
  MERGED_THROUGH_EQUALITY,
72
  /** Terms were merged due to reflexivity */
73
  MERGED_THROUGH_REFLEXIVITY,
74
  /** Terms were merged due to theory reasoning */
75
  MERGED_THROUGH_CONSTANTS,
76
  /** Terms were merged due to transitivity */
77
  MERGED_THROUGH_TRANS,
78
};
79
80
inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
81
  switch (reason) {
82
  case MERGED_THROUGH_CONGRUENCE:
83
    out << "congruence";
84
    break;
85
  case MERGED_THROUGH_EQUALITY:
86
    out << "pure equality";
87
    break;
88
  case MERGED_THROUGH_REFLEXIVITY:
89
    out << "reflexivity";
90
    break;
91
  case MERGED_THROUGH_CONSTANTS: out << "theory constants"; break;
92
  case MERGED_THROUGH_TRANS:
93
    out << "transitivity";
94
    break;
95
  default:
96
    out << "[theory]";
97
    break;
98
  }
99
  return out;
100
}
101
102
/**
103
 * A candidate for merging two equivalence classes, with the necessary
104
 * additional information.
105
 */
106
170133433
struct MergeCandidate {
107
  EqualityNodeId d_t1Id, d_t2Id;
108
  unsigned d_type;
109
  TNode d_reason;
110
35670723
  MergeCandidate(EqualityNodeId x,
111
                 EqualityNodeId y,
112
                 unsigned type,
113
                 TNode reason)
114
35670723
      : d_t1Id(x), d_t2Id(y), d_type(type), d_reason(reason)
115
35670723
  {}
116
};
117
118
/**
119
 * Just an index into the reasons array, and the number of merges to consume.
120
 */
121
struct DisequalityReasonRef {
122
  DefaultSizeType d_mergesStart;
123
  DefaultSizeType d_mergesEnd;
124
22113387
  DisequalityReasonRef(DefaultSizeType mergesStart = 0,
125
                       DefaultSizeType mergesEnd = 0)
126
22113387
      : d_mergesStart(mergesStart), d_mergesEnd(mergesEnd)
127
  {
128
22113387
  }
129
};
130
131
/**
132
 * We maintain uselist where a node appears in, and this is the node
133
 * of such a list.
134
 */
135
class UseListNode {
136
137
private:
138
139
  /** The id of the application node where this representative is at */
140
  EqualityNodeId d_applicationId;
141
142
  /** The next one in the class */
143
  UseListNodeId d_nextUseListNodeId;
144
145
public:
146
147
  /**
148
   * Creates a new node, which is in a list of it's own.
149
   */
150
5803926
  UseListNode(EqualityNodeId nodeId = null_id, UseListNodeId nextId = null_uselist_id)
151
5803926
  : d_applicationId(nodeId), d_nextUseListNodeId(nextId) {}
152
153
  /**
154
   * Returns the next node in the circular list.
155
   */
156
64109007
  UseListNodeId getNext() const {
157
64109007
    return d_nextUseListNodeId;
158
  }
159
160
  /**
161
   * Returns the id of the function application.
162
   */
163
116621434
  EqualityNodeId getApplicationId() const {
164
116621434
    return d_applicationId;
165
  }
166
};
167
168
/**
169
 * Main class for representing nodes in the equivalence class. The
170
 * nodes are a circular list, with the representative carrying the
171
 * size. Each individual node carries with itself the uselist of
172
 * function applications it appears in and the list of asserted
173
 * disequalities it belongs to. In order to get these lists one must
174
 * traverse the entire class and pick up all the individual lists.
175
 */
176
class EqualityNode {
177
178
private:
179
180
  /** The size of this equivalence class (if it's a representative) */
181
  DefaultSizeType d_size;
182
183
  /** The id (in the eq-manager) of the representative equality node */
184
  EqualityNodeId d_findId;
185
186
  /** The next equality node in this class */
187
  EqualityNodeId d_nextId;
188
189
  /** The use list of this node */
190
  UseListNodeId d_useList;
191
192
public:
193
194
  /**
195
   * Creates a new node, which is in a list of it's own.
196
   */
197
7641898
  EqualityNode(EqualityNodeId nodeId = null_id)
198
7641898
  : d_size(1)
199
  , d_findId(nodeId)
200
  , d_nextId(nodeId)
201
7641898
  , d_useList(null_uselist_id)
202
7641898
  {}
203
204
  /**
205
   * Returns the requested uselist.
206
   */
207
41099677
  UseListNodeId getUseList() const {
208
41099677
    return d_useList;
209
  }
210
211
  /**
212
   * Returns the next node in the class circular list.
213
   */
214
127803285
  EqualityNodeId getNext() const {
215
127803285
    return d_nextId;
216
  }
217
218
  /**
219
   * Returns the size of this equivalence class (only valid if this is the representative).
220
   */
221
13276654
  DefaultSizeType getSize() const {
222
13276654
    return d_size;
223
  }
224
225
  /**
226
   * Merges the two lists. If add size is true the size of this node is increased by the size of
227
   * the other node, otherwise the size is decreased by the size of the other node.
228
   */
229
  template<bool addSize>
230
51598409
  void merge(EqualityNode& other) {
231
51598409
    EqualityNodeId tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp;
232
    if (addSize) {
233
25800132
      d_size += other.d_size;
234
    } else {
235
25798277
      d_size -= other.d_size;
236
    }
237
51598409
  }
238
239
  /**
240
   * Returns the class representative.
241
   */
242
979225399
  EqualityNodeId getFind() const { return d_findId; }
243
244
  /**
245
   * Set the class representative.
246
   */
247
66895258
  void setFind(EqualityNodeId findId) { d_findId = findId; }
248
249
  /**
250
   * Note that this node is used in a function application funId, or
251
   * a negatively asserted equality (dis-equality) with funId.
252
   */
253
  template<typename memory_class>
254
5803926
  void usedIn(EqualityNodeId funId, memory_class& memory) {
255
5803926
    UseListNodeId newUseId = memory.size();
256
5803926
    memory.push_back(UseListNode(funId, d_useList));
257
5803926
    d_useList = newUseId;
258
5803926
  }
259
260
  /**
261
   * For backtracking: remove the first element from the uselist and pop the memory.
262
   */
263
  template<typename memory_class>
264
5798290
  void removeTopFromUseList(memory_class& memory) {
265
5798290
    Assert((int)d_useList == (int)memory.size() - 1);
266
5798290
    d_useList = memory.back().getNext();
267
5798290
    memory.pop_back();
268
5798290
  }
269
};
270
271
/** A pair of ids */
272
typedef std::pair<EqualityNodeId, EqualityNodeId> EqualityPair;
273
using EqualityPairHashFunction =
274
    PairHashFunction<EqualityNodeId, EqualityNodeId>;
275
276
enum FunctionApplicationType {
277
  /** This application is an equality a = b */
278
  APP_EQUALITY,
279
  /** This is a part of an uninterpreted application f(t1, ...., tn) */
280
  APP_UNINTERPRETED,
281
  /** This is a part of an interpreted application f(t1, ..., tn) */
282
  APP_INTERPRETED
283
};
284
285
/**
286
 * Represents the function APPLY a b. If isEquality is true then it
287
 * represents the predicate (a = b). Note that since one can not
288
 * construct the equality over function terms, the equality and hash
289
 * function below are still well defined.
290
 */
291
struct FunctionApplication {
292
  /** Type of application */
293
  FunctionApplicationType d_type;
294
  /** The actual application elements */
295
  EqualityNodeId d_a, d_b;
296
297
  /** Construct an application */
298
67969118
  FunctionApplication(FunctionApplicationType type = APP_EQUALITY,
299
                      EqualityNodeId a = null_id,
300
                      EqualityNodeId b = null_id)
301
67969118
      : d_type(type), d_a(a), d_b(b)
302
  {
303
67969118
  }
304
305
  /** Equality of two applications */
306
49105767
  bool operator == (const FunctionApplication& other) const {
307
49105767
    return d_type == other.d_type && d_a == other.d_a && d_b == other.d_b;
308
  }
309
310
  /** Is this a null application */
311
7375107
  bool isNull() const { return d_a == null_id || d_b == null_id; }
312
313
  /** Is this an equality */
314
33837029
  bool isEquality() const { return d_type == APP_EQUALITY; }
315
316
  /** Is this an interpreted application (equality is special, i.e. not interpreted) */
317
38823003
  bool isInterpreted() const { return d_type == APP_INTERPRETED; }
318
};
319
320
struct FunctionApplicationHashFunction {
321
100575205
  size_t operator () (const FunctionApplication& app) const {
322
100575205
    size_t hash = 0;
323
100575205
    hash = 0x9e3779b9 + app.d_a;
324
100575205
    hash ^= 0x9e3779b9 + app.d_b + (hash << 6) + (hash >> 2);
325
100575205
    return hash;
326
  }
327
};
328
329
/**
330
 * At time of addition a function application can already normalize to something, so
331
 * we keep both the original, and the normalized version.
332
 */
333
struct FunctionApplicationPair {
334
  FunctionApplication d_original;
335
  FunctionApplication d_normalized;
336
7641898
  FunctionApplicationPair() {}
337
2901963
  FunctionApplicationPair(const FunctionApplication& original,
338
                          const FunctionApplication& normalized)
339
2901963
      : d_original(original), d_normalized(normalized)
340
  {
341
2901963
  }
342
  bool isNull() const { return d_original.isNull(); }
343
};
344
345
/**
346
 * Information about the added triggers.
347
 */
348
15567992
struct TriggerInfo {
349
  /** The trigger itself */
350
  Node d_trigger;
351
  /** Polarity of the trigger */
352
  bool d_polarity;
353
  TriggerInfo() : d_polarity(false) {}
354
3229984
  TriggerInfo(Node trigger, bool polarity)
355
3229984
      : d_trigger(trigger), d_polarity(polarity)
356
  {
357
3229984
  }
358
};
359
360
} // namespace eq
361
} // namespace theory
362
} // namespace CVC4
363
364
#endif /* CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H */