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