1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Dejan Jovanovic, Andrew Reynolds, Morgan Deters |
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_H |
22 |
|
#define CVC5__THEORY__UF__EQUALITY_ENGINE_H |
23 |
|
|
24 |
|
#include <deque> |
25 |
|
#include <queue> |
26 |
|
#include <unordered_map> |
27 |
|
#include <vector> |
28 |
|
|
29 |
|
#include "context/cdhashmap.h" |
30 |
|
#include "context/cdo.h" |
31 |
|
#include "expr/kind_map.h" |
32 |
|
#include "expr/node.h" |
33 |
|
#include "theory/theory_id.h" |
34 |
|
#include "theory/uf/equality_engine_iterator.h" |
35 |
|
#include "theory/uf/equality_engine_notify.h" |
36 |
|
#include "theory/uf/equality_engine_types.h" |
37 |
|
#include "util/statistics_stats.h" |
38 |
|
|
39 |
|
namespace cvc5 { |
40 |
|
namespace theory { |
41 |
|
namespace eq { |
42 |
|
|
43 |
|
class EqClassesIterator; |
44 |
|
class EqClassIterator; |
45 |
|
class EqProof; |
46 |
|
|
47 |
|
/** |
48 |
|
* Class for keeping an incremental congruence closure over a set of terms. It provides |
49 |
|
* notifications via an EqualityEngineNotify object. |
50 |
|
*/ |
51 |
|
class EqualityEngine : public context::ContextNotifyObj { |
52 |
|
|
53 |
|
friend class EqClassesIterator; |
54 |
|
friend class EqClassIterator; |
55 |
|
|
56 |
|
/** Default implementation of the notification object */ |
57 |
|
static EqualityEngineNotifyNone s_notifyNone; |
58 |
|
|
59 |
|
/** |
60 |
|
* Master equality engine that gets all the equality information from |
61 |
|
* this one, or null if none. |
62 |
|
*/ |
63 |
|
EqualityEngine* d_masterEqualityEngine; |
64 |
|
|
65 |
|
public: |
66 |
|
/** |
67 |
|
* Initialize the equality engine, given the notification class. |
68 |
|
* |
69 |
|
* @param constantTriggers Whether we treat constants as trigger terms |
70 |
|
* @param anyTermTriggers Whether we use any terms as triggers |
71 |
|
*/ |
72 |
|
EqualityEngine(EqualityEngineNotify& notify, |
73 |
|
context::Context* context, |
74 |
|
std::string name, |
75 |
|
bool constantTriggers, |
76 |
|
bool anyTermTriggers = true); |
77 |
|
|
78 |
|
/** |
79 |
|
* Initialize the equality engine with no notification class. |
80 |
|
*/ |
81 |
|
EqualityEngine(context::Context* context, |
82 |
|
std::string name, |
83 |
|
bool constantsAreTriggers, |
84 |
|
bool anyTermTriggers = true); |
85 |
|
|
86 |
|
/** |
87 |
|
* Just a destructor. |
88 |
|
*/ |
89 |
|
virtual ~EqualityEngine(); |
90 |
|
|
91 |
|
/** |
92 |
|
* Set the master equality engine for this one. Master engine will get copies |
93 |
|
* of all the terms and equalities from this engine. |
94 |
|
*/ |
95 |
|
void setMasterEqualityEngine(EqualityEngine* master); |
96 |
|
|
97 |
|
/** Print the equivalence classes for debugging */ |
98 |
|
std::string debugPrintEqc() const; |
99 |
|
|
100 |
|
/** Statistics about the equality engine instance */ |
101 |
|
struct Statistics |
102 |
|
{ |
103 |
|
/** Total number of merges */ |
104 |
|
IntStat d_mergesCount; |
105 |
|
/** Number of terms managed by the system */ |
106 |
|
IntStat d_termsCount; |
107 |
|
/** Number of function terms managed by the system */ |
108 |
|
IntStat d_functionTermsCount; |
109 |
|
/** Number of constant terms managed by the system */ |
110 |
|
IntStat d_constantTermsCount; |
111 |
|
|
112 |
|
Statistics(const std::string& name); |
113 |
|
};/* struct EqualityEngine::statistics */ |
114 |
|
|
115 |
|
private: |
116 |
|
|
117 |
|
/** The context we are using */ |
118 |
|
context::Context* d_context; |
119 |
|
|
120 |
|
/** If we are done, we don't except any new assertions */ |
121 |
|
context::CDO<bool> d_done; |
122 |
|
|
123 |
|
/** Whether to notify or not (temporarily disabled on equality checks) */ |
124 |
|
bool d_performNotify; |
125 |
|
|
126 |
|
/** The class to notify when a representative changes for a term */ |
127 |
|
EqualityEngineNotify& d_notify; |
128 |
|
|
129 |
|
/** The map of kinds to be treated as function applications */ |
130 |
|
KindMap d_congruenceKinds; |
131 |
|
|
132 |
|
/** The map of kinds to be treated as interpreted function applications (for evaluation of constants) */ |
133 |
|
KindMap d_congruenceKindsInterpreted; |
134 |
|
|
135 |
|
/** The map of kinds with operators to be considered external (for higher-order) */ |
136 |
|
KindMap d_congruenceKindsExtOperators; |
137 |
|
|
138 |
|
/** Map from nodes to their ids */ |
139 |
|
std::unordered_map<TNode, EqualityNodeId> d_nodeIds; |
140 |
|
|
141 |
|
/** Map from function applications to their ids */ |
142 |
|
typedef std::unordered_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap; |
143 |
|
|
144 |
|
/** |
145 |
|
* A map from a pair (a', b') to a function application f(a, b), where a' and b' are the current representatives |
146 |
|
* of a and b. |
147 |
|
*/ |
148 |
|
ApplicationIdsMap d_applicationLookup; |
149 |
|
|
150 |
|
/** Application lookups in order, so that we can backtrack. */ |
151 |
|
std::vector<FunctionApplication> d_applicationLookups; |
152 |
|
|
153 |
|
/** Number of application lookups, for backtracking. */ |
154 |
|
context::CDO<DefaultSizeType> d_applicationLookupsCount; |
155 |
|
|
156 |
|
/** |
157 |
|
* Store the application lookup, with enough information to backtrack |
158 |
|
*/ |
159 |
|
void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId); |
160 |
|
|
161 |
|
/** Map from ids to the nodes (these need to be nodes as we pick up the operators) */ |
162 |
|
std::vector<Node> d_nodes; |
163 |
|
|
164 |
|
/** A context-dependents count of nodes */ |
165 |
|
context::CDO<DefaultSizeType> d_nodesCount; |
166 |
|
|
167 |
|
/** Map from ids to the applications */ |
168 |
|
std::vector<FunctionApplicationPair> d_applications; |
169 |
|
|
170 |
|
/** Map from ids to the equality nodes */ |
171 |
|
std::vector<EqualityNode> d_equalityNodes; |
172 |
|
|
173 |
|
/** Number of asserted equalities we have so far */ |
174 |
|
context::CDO<DefaultSizeType> d_assertedEqualitiesCount; |
175 |
|
|
176 |
|
/** Memory for the use-list nodes */ |
177 |
|
std::vector<UseListNode> d_useListNodes; |
178 |
|
|
179 |
|
/** |
180 |
|
* We keep a list of asserted equalities. Not among original terms, but |
181 |
|
* among the class representatives. |
182 |
|
*/ |
183 |
|
struct Equality { |
184 |
|
/** Left hand side of the equality */ |
185 |
|
EqualityNodeId d_lhs; |
186 |
|
/** Right hand side of the equality */ |
187 |
|
EqualityNodeId d_rhs; |
188 |
|
/** Equality constructor */ |
189 |
22081093 |
Equality(EqualityNodeId l = null_id, EqualityNodeId r = null_id) |
190 |
22081093 |
: d_lhs(l), d_rhs(r) |
191 |
|
{ |
192 |
22081093 |
} |
193 |
|
};/* struct EqualityEngine::Equality */ |
194 |
|
|
195 |
|
/** The ids of the classes we have merged */ |
196 |
|
std::vector<Equality> d_assertedEqualities; |
197 |
|
|
198 |
|
/** The reasons for the equalities */ |
199 |
|
|
200 |
|
/** |
201 |
|
* An edge in the equality graph. This graph is an undirected graph (both edges added) |
202 |
|
* containing the actual asserted equalities. |
203 |
|
*/ |
204 |
140023996 |
class EqualityEdge { |
205 |
|
|
206 |
|
// The id of the RHS of this equality |
207 |
|
EqualityNodeId d_nodeId; |
208 |
|
// The next edge |
209 |
|
EqualityEdgeId d_nextId; |
210 |
|
// Type of reason for this equality |
211 |
|
unsigned d_mergeType; |
212 |
|
// Reason of this equality |
213 |
|
TNode d_reason; |
214 |
|
|
215 |
|
public: |
216 |
|
|
217 |
|
EqualityEdge(): |
218 |
|
d_nodeId(null_edge), d_nextId(null_edge), d_mergeType(MERGED_THROUGH_CONGRUENCE) {} |
219 |
|
|
220 |
44162186 |
EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, unsigned type, TNode reason): |
221 |
44162186 |
d_nodeId(nodeId), d_nextId(nextId), d_mergeType(type), d_reason(reason) {} |
222 |
|
|
223 |
|
/** Returns the id of the next edge */ |
224 |
74326774 |
EqualityEdgeId getNext() const { return d_nextId; } |
225 |
|
|
226 |
|
/** Returns the id of the target edge node */ |
227 |
144757493 |
EqualityNodeId getNodeId() const { return d_nodeId; } |
228 |
|
|
229 |
|
/** The reason of this edge */ |
230 |
4340178 |
unsigned getReasonType() const { return d_mergeType; } |
231 |
|
|
232 |
|
/** The reason of this edge */ |
233 |
4340178 |
TNode getReason() const { return d_reason; } |
234 |
|
};/* class EqualityEngine::EqualityEdge */ |
235 |
|
|
236 |
|
/** |
237 |
|
* All the equality edges (twice as many as the number of asserted equalities. If an equality |
238 |
|
* t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hence, having the index |
239 |
|
* of one of the edges you can reconstruct the original equality. |
240 |
|
*/ |
241 |
|
std::vector<EqualityEdge> d_equalityEdges; |
242 |
|
|
243 |
|
/** |
244 |
|
* Returns the string representation of the edges. |
245 |
|
*/ |
246 |
|
std::string edgesToString(EqualityEdgeId edgeId) const; |
247 |
|
|
248 |
|
/** |
249 |
|
* Map from a node to its first edge in the equality graph. Edges are added to the front of the |
250 |
|
* list which makes the insertion/backtracking easy. |
251 |
|
*/ |
252 |
|
std::vector<EqualityEdgeId> d_equalityGraph; |
253 |
|
|
254 |
|
/** Add an edge to the equality graph */ |
255 |
|
void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason); |
256 |
|
|
257 |
|
/** Returns the equality node of the given node */ |
258 |
|
EqualityNode& getEqualityNode(TNode node); |
259 |
|
|
260 |
|
/** Returns the equality node of the given node */ |
261 |
|
const EqualityNode& getEqualityNode(TNode node) const; |
262 |
|
|
263 |
|
/** Returns the equality node of the given node */ |
264 |
|
EqualityNode& getEqualityNode(EqualityNodeId nodeId); |
265 |
|
|
266 |
|
/** Returns the equality node of the given node */ |
267 |
|
const EqualityNode& getEqualityNode(EqualityNodeId nodeId) const; |
268 |
|
|
269 |
|
/** Returns the id of the node */ |
270 |
|
EqualityNodeId getNodeId(TNode node) const; |
271 |
|
|
272 |
|
/** |
273 |
|
* Merge the class2 into class1 |
274 |
|
* @return true if ok, false if to break out |
275 |
|
*/ |
276 |
|
bool merge(EqualityNode& class1, EqualityNode& class2, std::vector<TriggerId>& triggers); |
277 |
|
|
278 |
|
/** Undo the merge of class2 into class1 */ |
279 |
|
void undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id); |
280 |
|
|
281 |
|
/** Backtrack the information if necessary */ |
282 |
|
void backtrack(); |
283 |
|
|
284 |
|
/** |
285 |
|
* Trigger that will be updated |
286 |
|
*/ |
287 |
|
struct Trigger { |
288 |
|
/** The current class id of the LHS of the trigger */ |
289 |
|
EqualityNodeId d_classId; |
290 |
|
/** Next trigger for class */ |
291 |
|
TriggerId d_nextTrigger; |
292 |
|
|
293 |
3458436 |
Trigger(EqualityNodeId classId = null_id, |
294 |
|
TriggerId nextTrigger = null_trigger) |
295 |
3458436 |
: d_classId(classId), d_nextTrigger(nextTrigger) |
296 |
|
{ |
297 |
3458436 |
} |
298 |
|
};/* struct EqualityEngine::Trigger */ |
299 |
|
|
300 |
|
/** |
301 |
|
* Vector of triggers. Triggers come in pairs for an |
302 |
|
* equality trigger (t1, t2): one at position 2k for t1, and one at position 2k + 1 for t2. When |
303 |
|
* updating triggers we always know where the other one is (^1). |
304 |
|
*/ |
305 |
|
std::vector<Trigger> d_equalityTriggers; |
306 |
|
|
307 |
|
/** |
308 |
|
* Vector of original equalities of the triggers. |
309 |
|
*/ |
310 |
|
std::vector<TriggerInfo> d_equalityTriggersOriginal; |
311 |
|
|
312 |
|
/** |
313 |
|
* Context dependent count of triggers |
314 |
|
*/ |
315 |
|
context::CDO<DefaultSizeType> d_equalityTriggersCount; |
316 |
|
|
317 |
|
/** |
318 |
|
* Trigger lists per node. The begin id changes as we merge, but the end always points to |
319 |
|
* the actual end of the triggers for this node. |
320 |
|
*/ |
321 |
|
std::vector<TriggerId> d_nodeTriggers; |
322 |
|
|
323 |
|
/** |
324 |
|
* Map from ids to whether they are constants (constants are always |
325 |
|
* representatives of their class. |
326 |
|
*/ |
327 |
|
std::vector<bool> d_isConstant; |
328 |
|
|
329 |
|
/** |
330 |
|
* Map from ids of proper terms, to the number of non-constant direct subterms. If we update an interpreted |
331 |
|
* application to a constant, we can decrease this value. If we hit 0, we can evaluate the term. |
332 |
|
* |
333 |
|
*/ |
334 |
|
std::vector<unsigned> d_subtermsToEvaluate; |
335 |
|
|
336 |
|
/** |
337 |
|
* For nodes that we need to postpone evaluation. |
338 |
|
*/ |
339 |
|
std::queue<EqualityNodeId> d_evaluationQueue; |
340 |
|
|
341 |
|
/** |
342 |
|
* Evaluate all terms in the evaluation queue. |
343 |
|
*/ |
344 |
|
void processEvaluationQueue(); |
345 |
|
|
346 |
|
/** Vector of nodes that evaluate. */ |
347 |
|
std::vector<EqualityNodeId> d_subtermEvaluates; |
348 |
|
|
349 |
|
/** Size of the nodes that evaluate vector. */ |
350 |
|
context::CDO<unsigned> d_subtermEvaluatesSize; |
351 |
|
|
352 |
|
/** Set the node evaluate flag */ |
353 |
|
void subtermEvaluates(EqualityNodeId id); |
354 |
|
|
355 |
|
/** |
356 |
|
* Returns the evaluation of the term when all (direct) children are replaced with |
357 |
|
* the constant representatives. |
358 |
|
*/ |
359 |
|
Node evaluateTerm(TNode node); |
360 |
|
|
361 |
|
/** |
362 |
|
* Returns true if it's a constant |
363 |
|
*/ |
364 |
261948 |
bool isConstant(EqualityNodeId id) const { |
365 |
261948 |
return d_isConstant[getEqualityNode(id).getFind()]; |
366 |
|
} |
367 |
|
|
368 |
|
/** |
369 |
|
* Map from ids to whether they are Boolean. |
370 |
|
*/ |
371 |
|
std::vector<bool> d_isEquality; |
372 |
|
|
373 |
|
/** |
374 |
|
* Map from ids to whether the nods is internal. An internal node is a node |
375 |
|
* that corresponds to a partially currified node, for example. |
376 |
|
*/ |
377 |
|
std::vector<bool> d_isInternal; |
378 |
|
|
379 |
|
/** |
380 |
|
* Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId. |
381 |
|
*/ |
382 |
|
void addTriggerToList(EqualityNodeId nodeId, TriggerId triggerId); |
383 |
|
|
384 |
|
/** Statistics */ |
385 |
|
Statistics d_stats; |
386 |
|
|
387 |
|
/** Add a new function application node to the database, i.e APP t1 t2 */ |
388 |
|
EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, FunctionApplicationType type); |
389 |
|
|
390 |
|
/** Add a new node to the database */ |
391 |
|
EqualityNodeId newNode(TNode t); |
392 |
|
|
393 |
|
/** Propagation queue */ |
394 |
|
std::deque<MergeCandidate> d_propagationQueue; |
395 |
|
|
396 |
|
/** Enqueue to the propagation queue */ |
397 |
|
void enqueue(const MergeCandidate& candidate, bool back = true); |
398 |
|
|
399 |
|
/** Do the propagation */ |
400 |
|
void propagate(); |
401 |
|
|
402 |
|
/** Are we in propagate */ |
403 |
|
bool d_inPropagate; |
404 |
|
|
405 |
|
/** Proof-new specific construction of equality conclusions for EqProofs |
406 |
|
* |
407 |
|
* Given two equality node ids, build an equality between the nodes they |
408 |
|
* correspond to and add it as a conclusion to the given EqProof. |
409 |
|
* |
410 |
|
* The equality is only built if the nodes the ids correspond to are not |
411 |
|
* internal nodes in the equality engine, i.e., they correspond to full |
412 |
|
* applications of the respective kinds. Since the equality engine also |
413 |
|
* applies congruence over n-ary kinds, internal nodes, i.e., partial |
414 |
|
* applications, may still correspond to "full applications" in the |
415 |
|
* first-order sense. Therefore this method also checks, in the case of n-ary |
416 |
|
* congruence kinds, if an equality between "full applications" can be built. |
417 |
|
*/ |
418 |
|
void buildEqConclusion(EqualityNodeId id1, |
419 |
|
EqualityNodeId id2, |
420 |
|
EqProof* eqp) const; |
421 |
|
|
422 |
|
/** |
423 |
|
* Get an explanation of the equality t1 = t2. Returns the asserted equalities |
424 |
|
* that imply t1 = t2. Returns TNodes as the assertion equalities should be |
425 |
|
* hashed somewhere else. |
426 |
|
* |
427 |
|
* This call refers to terms t1 and t2 by their ids t1Id and t2Id. |
428 |
|
* |
429 |
|
* If eqp is non-null, then this method populates eqp's information and |
430 |
|
* children such that it is a proof of t1 = t2. |
431 |
|
* |
432 |
|
* We cache results of this call in cache, where cache[t1Id][t2Id] stores |
433 |
|
* a proof of t1 = t2. |
434 |
|
*/ |
435 |
|
void getExplanation( |
436 |
|
EqualityEdgeId t1Id, |
437 |
|
EqualityNodeId t2Id, |
438 |
|
std::vector<TNode>& equalities, |
439 |
|
std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>& cache, |
440 |
|
EqProof* eqp) const; |
441 |
|
|
442 |
|
/** |
443 |
|
* Print the equality graph. |
444 |
|
*/ |
445 |
|
void debugPrintGraph() const; |
446 |
|
|
447 |
|
/** The true node */ |
448 |
|
Node d_true; |
449 |
|
/** True node id */ |
450 |
|
EqualityNodeId d_trueId; |
451 |
|
|
452 |
|
/** The false node */ |
453 |
|
Node d_false; |
454 |
|
/** False node id */ |
455 |
|
EqualityNodeId d_falseId; |
456 |
|
|
457 |
|
/** |
458 |
|
* Adds an equality of terms t1 and t2 to the database. |
459 |
|
*/ |
460 |
|
void assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); |
461 |
|
|
462 |
|
/** |
463 |
|
* Adds a trigger equality to the database with the trigger node and polarity for notification. |
464 |
|
*/ |
465 |
|
void addTriggerEqualityInternal(TNode t1, TNode t2, TNode trigger, bool polarity); |
466 |
|
|
467 |
|
/** |
468 |
|
* This method gets called on backtracks from the context manager. |
469 |
|
*/ |
470 |
28244989 |
void contextNotifyPop() override { backtrack(); } |
471 |
|
|
472 |
|
/** |
473 |
|
* Constructor initialization stuff. |
474 |
|
*/ |
475 |
|
void init(); |
476 |
|
|
477 |
|
/** Set of trigger terms */ |
478 |
|
struct TriggerTermSet { |
479 |
|
/** Set of theories in this set */ |
480 |
|
TheoryIdSet d_tags; |
481 |
|
/** The trigger terms */ |
482 |
|
EqualityNodeId d_triggers[0]; |
483 |
|
/** Returns the theory tags */ |
484 |
|
TheoryIdSet hasTrigger(TheoryId tag) const; |
485 |
|
/** Returns a trigger by tag */ |
486 |
|
EqualityNodeId getTrigger(TheoryId tag) const; |
487 |
|
};/* struct EqualityEngine::TriggerTermSet */ |
488 |
|
|
489 |
|
/** Are the constants triggers */ |
490 |
|
bool d_constantsAreTriggers; |
491 |
|
/** |
492 |
|
* Are any terms triggers? If this is false, then all trigger terms are |
493 |
|
* ignored (e.g. this means that addTriggerTerm is equivalent to addTerm). |
494 |
|
*/ |
495 |
|
bool d_anyTermsAreTriggers; |
496 |
|
|
497 |
|
/** The information about trigger terms is stored in this easily maintained memory. */ |
498 |
|
char* d_triggerDatabase; |
499 |
|
|
500 |
|
/** Allocated size of the trigger term database */ |
501 |
|
DefaultSizeType d_triggerDatabaseAllocatedSize; |
502 |
|
|
503 |
|
/** Reference for the trigger terms set */ |
504 |
|
typedef DefaultSizeType TriggerTermSetRef; |
505 |
|
|
506 |
|
/** Null reference */ |
507 |
|
static const TriggerTermSetRef null_set_id = (TriggerTermSetRef)(-1); |
508 |
|
|
509 |
|
/** Create new trigger term set based on the internally set information */ |
510 |
|
TriggerTermSetRef newTriggerTermSet(TheoryIdSet newSetTags, |
511 |
|
EqualityNodeId* newSetTriggers, |
512 |
|
unsigned newSetTriggersSize); |
513 |
|
|
514 |
|
/** Get the trigger set give a reference */ |
515 |
62095176 |
TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) { |
516 |
62095176 |
Assert(ref < d_triggerDatabaseSize); |
517 |
62095176 |
return *(reinterpret_cast<TriggerTermSet*>(d_triggerDatabase + ref)); |
518 |
|
} |
519 |
|
|
520 |
|
/** Get the trigger set give a reference */ |
521 |
8515614 |
const TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) const { |
522 |
8515614 |
Assert(ref < d_triggerDatabaseSize); |
523 |
8515614 |
return *(reinterpret_cast<const TriggerTermSet*>(d_triggerDatabase + ref)); |
524 |
|
} |
525 |
|
|
526 |
|
/** Used part of the trigger term database */ |
527 |
|
context::CDO<DefaultSizeType> d_triggerDatabaseSize; |
528 |
|
|
529 |
|
struct TriggerSetUpdate { |
530 |
|
EqualityNodeId d_classId; |
531 |
|
TriggerTermSetRef d_oldValue; |
532 |
4485611 |
TriggerSetUpdate(EqualityNodeId classId = null_id, |
533 |
|
TriggerTermSetRef oldValue = null_set_id) |
534 |
4485611 |
: d_classId(classId), d_oldValue(oldValue) |
535 |
|
{ |
536 |
4485611 |
} |
537 |
|
};/* struct EqualityEngine::TriggerSetUpdate */ |
538 |
|
|
539 |
|
/** |
540 |
|
* List of trigger updates for backtracking. |
541 |
|
*/ |
542 |
|
std::vector<TriggerSetUpdate> d_triggerTermSetUpdates; |
543 |
|
|
544 |
|
/** |
545 |
|
* Size of the individual triggers list. |
546 |
|
*/ |
547 |
|
context::CDO<unsigned> d_triggerTermSetUpdatesSize; |
548 |
|
|
549 |
|
/** |
550 |
|
* Map from ids to the individual trigger set representatives. |
551 |
|
*/ |
552 |
|
std::vector<TriggerTermSetRef> d_nodeIndividualTrigger; |
553 |
|
|
554 |
|
typedef std::unordered_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap; |
555 |
|
|
556 |
|
/** |
557 |
|
* A map from pairs of disequal terms, to the reason why we deduced they are disequal. |
558 |
|
*/ |
559 |
|
DisequalityReasonsMap d_disequalityReasonsMap; |
560 |
|
|
561 |
|
/** |
562 |
|
* A list of all the disequalities we deduced. |
563 |
|
*/ |
564 |
|
std::vector<EqualityPair> d_deducedDisequalities; |
565 |
|
|
566 |
|
/** |
567 |
|
* Context dependent size of the deduced disequalities |
568 |
|
*/ |
569 |
|
context::CDO<size_t> d_deducedDisequalitiesSize; |
570 |
|
|
571 |
|
/** |
572 |
|
* For each disequality deduced, we add the pairs of equivalences needed to explain it. |
573 |
|
*/ |
574 |
|
std::vector<EqualityPair> d_deducedDisequalityReasons; |
575 |
|
|
576 |
|
/** |
577 |
|
* Size of the memory for disequality reasons. |
578 |
|
*/ |
579 |
|
context::CDO<size_t> d_deducedDisequalityReasonsSize; |
580 |
|
|
581 |
|
/** |
582 |
|
* Map from equalities to the tags that have received the notification. |
583 |
|
*/ |
584 |
|
typedef context:: |
585 |
|
CDHashMap<EqualityPair, TheoryIdSet, EqualityPairHashFunction> |
586 |
|
PropagatedDisequalitiesMap; |
587 |
|
PropagatedDisequalitiesMap d_propagatedDisequalities; |
588 |
|
|
589 |
|
/** |
590 |
|
* Has this equality been propagated to anyone. |
591 |
|
*/ |
592 |
|
bool hasPropagatedDisequality(EqualityNodeId lhsId, EqualityNodeId rhsId) const; |
593 |
|
|
594 |
|
/** |
595 |
|
* Has this equality been propagated to the tag owner. |
596 |
|
*/ |
597 |
|
bool hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) const; |
598 |
|
|
599 |
|
/** |
600 |
|
* Stores a propagated disequality for explanation purposes and remembers the reasons. The |
601 |
|
* reasons should be pushed on the reasons vector. |
602 |
|
*/ |
603 |
|
void storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId); |
604 |
|
|
605 |
|
/** |
606 |
|
* An equality tagged with a set of tags. |
607 |
|
*/ |
608 |
|
struct TaggedEquality { |
609 |
|
/** Id of the equality */ |
610 |
|
EqualityNodeId d_equalityId; |
611 |
|
/** TriggerSet reference for the class of one of the sides */ |
612 |
|
TriggerTermSetRef d_triggerSetRef; |
613 |
|
/** Is trigger equivalent to the lhs (rhs otherwise) */ |
614 |
|
bool d_lhs; |
615 |
|
|
616 |
839939 |
TaggedEquality(EqualityNodeId equalityId = null_id, |
617 |
|
TriggerTermSetRef triggerSetRef = null_set_id, |
618 |
|
bool lhs = true) |
619 |
839939 |
: d_equalityId(equalityId), d_triggerSetRef(triggerSetRef), d_lhs(lhs) |
620 |
|
{ |
621 |
839939 |
} |
622 |
|
}; |
623 |
|
|
624 |
|
/** A map from equivalence class id's to tagged equalities */ |
625 |
|
typedef std::vector<TaggedEquality> TaggedEqualitiesSet; |
626 |
|
|
627 |
|
/** |
628 |
|
* Returns a set of equalities that have been asserted false where one side of the equality |
629 |
|
* belongs to the given equivalence class. The equalities are restricted to the ones where |
630 |
|
* one side of the equality is in the tags set, but the other one isn't. Each returned |
631 |
|
* dis-equality is associated with the tags that are the subset of the input tags, such that |
632 |
|
* exactly one side of the equality is not in the set yet. |
633 |
|
* |
634 |
|
* @param classId the equivalence class to search |
635 |
|
* @param inputTags the tags to filter the equalities |
636 |
|
* @param out the output equalities, as described above |
637 |
|
*/ |
638 |
|
void getDisequalities(bool allowConstants, |
639 |
|
EqualityNodeId classId, |
640 |
|
TheoryIdSet inputTags, |
641 |
|
TaggedEqualitiesSet& out); |
642 |
|
|
643 |
|
/** |
644 |
|
* Propagates the remembered disequalities with given tags the original triggers for those tags, |
645 |
|
* and the set of disequalities produced by above. |
646 |
|
*/ |
647 |
|
bool propagateTriggerTermDisequalities( |
648 |
|
TheoryIdSet tags, |
649 |
|
TriggerTermSetRef triggerSetRef, |
650 |
|
const TaggedEqualitiesSet& disequalitiesToNotify); |
651 |
|
|
652 |
|
/** Name of the equality engine */ |
653 |
|
std::string d_name; |
654 |
|
|
655 |
|
/** The internal addTerm */ |
656 |
|
void addTermInternal(TNode t, bool isOperator = false); |
657 |
|
/** |
658 |
|
* Adds a notify trigger for equality. When equality becomes true |
659 |
|
* eqNotifyTriggerPredicate will be called with value = true, and when |
660 |
|
* equality becomes false eqNotifyTriggerPredicate will be called with value = |
661 |
|
* false. |
662 |
|
*/ |
663 |
|
void addTriggerEquality(TNode equality); |
664 |
|
|
665 |
|
public: |
666 |
|
/** |
667 |
|
* Adds a term to the term database. |
668 |
|
*/ |
669 |
2174986 |
void addTerm(TNode t) { |
670 |
2174986 |
addTermInternal(t, false); |
671 |
2174986 |
} |
672 |
|
|
673 |
|
/** |
674 |
|
* Add a kind to treat as function applications. |
675 |
|
* When extOperator is true, this equality engine will treat the operators of this kind |
676 |
|
* as "external" e.g. not internal nodes (see d_isInternal). This means that we will |
677 |
|
* consider equivalence classes containing the operators of such terms, and "hasTerm" will |
678 |
|
* return true. |
679 |
|
*/ |
680 |
|
void addFunctionKind(Kind fun, bool interpreted = false, bool extOperator = false); |
681 |
|
|
682 |
|
/** |
683 |
|
* Returns true if this kind is used for congruence closure. |
684 |
|
*/ |
685 |
599926 |
bool isFunctionKind(Kind fun) const { return d_congruenceKinds.test(fun); } |
686 |
|
|
687 |
|
/** |
688 |
|
* Returns true if this kind is used for congruence closure + evaluation of constants. |
689 |
|
*/ |
690 |
680905 |
bool isInterpretedFunctionKind(Kind fun) const |
691 |
|
{ |
692 |
680905 |
return d_congruenceKindsInterpreted.test(fun); |
693 |
|
} |
694 |
|
|
695 |
|
/** |
696 |
|
* Returns true if this kind has an operator that is considered external (e.g. not internal). |
697 |
|
*/ |
698 |
680905 |
bool isExternalOperatorKind(Kind fun) const |
699 |
|
{ |
700 |
680905 |
return d_congruenceKindsExtOperators.test(fun); |
701 |
|
} |
702 |
|
|
703 |
|
/** |
704 |
|
* Check whether the node is already in the database. |
705 |
|
*/ |
706 |
|
bool hasTerm(TNode t) const; |
707 |
|
|
708 |
|
/** |
709 |
|
* Adds a predicate p with given polarity. The predicate asserted |
710 |
|
* should be in the congruence closure kinds (otherwise it's |
711 |
|
* useless). |
712 |
|
* |
713 |
|
* @param p the (non-negated) predicate |
714 |
|
* @param polarity true if asserting the predicate, false if |
715 |
|
* asserting the negated predicate |
716 |
|
* @param reason the reason to keep for building explanations |
717 |
|
* @return true if a new fact was asserted, false if this call was a no-op. |
718 |
|
*/ |
719 |
|
bool assertPredicate(TNode p, |
720 |
|
bool polarity, |
721 |
|
TNode reason, |
722 |
|
unsigned pid = MERGED_THROUGH_EQUALITY); |
723 |
|
|
724 |
|
/** |
725 |
|
* Adds an equality eq with the given polarity to the database. |
726 |
|
* |
727 |
|
* @param eq the (non-negated) equality |
728 |
|
* @param polarity true if asserting the equality, false if |
729 |
|
* asserting the negated equality |
730 |
|
* @param reason the reason to keep for building explanations |
731 |
|
* @return true if a new fact was asserted, false if this call was a no-op. |
732 |
|
*/ |
733 |
|
bool assertEquality(TNode eq, |
734 |
|
bool polarity, |
735 |
|
TNode reason, |
736 |
|
unsigned pid = MERGED_THROUGH_EQUALITY); |
737 |
|
|
738 |
|
/** |
739 |
|
* Returns the current representative of the term t. |
740 |
|
*/ |
741 |
|
TNode getRepresentative(TNode t) const; |
742 |
|
|
743 |
|
/** |
744 |
|
* Add all the terms where the given term appears as a first child |
745 |
|
* (directly or implicitly). |
746 |
|
*/ |
747 |
|
void getUseListTerms(TNode t, std::set<TNode>& output); |
748 |
|
|
749 |
|
/** |
750 |
|
* Get an explanation of the equality t1 = t2 being true or false. |
751 |
|
* Returns the reasons (added when asserting) that imply it |
752 |
|
* in the assertions vector. |
753 |
|
*/ |
754 |
|
void explainEquality(TNode t1, TNode t2, bool polarity, |
755 |
|
std::vector<TNode>& assertions, |
756 |
|
EqProof* eqp = nullptr) const; |
757 |
|
|
758 |
|
/** |
759 |
|
* Get an explanation of the predicate being true or false. |
760 |
|
* Returns the reasons (added when asserting) that imply imply it |
761 |
|
* in the assertions vector. |
762 |
|
*/ |
763 |
|
void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, |
764 |
|
EqProof* eqp = nullptr) const; |
765 |
|
|
766 |
|
//--------------------------- standard safe explanation methods |
767 |
|
/** |
768 |
|
* Explain literal, add its explanation to assumptions. This method does not |
769 |
|
* add duplicates to assumptions. It requires that the literal |
770 |
|
* holds in this class. If lit is a disequality, it |
771 |
|
* moreover ensures this class is ready to explain it via areDisequal with |
772 |
|
* ensureProof = true. |
773 |
|
*/ |
774 |
|
void explainLit(TNode lit, std::vector<TNode>& assumptions); |
775 |
|
/** |
776 |
|
* Explain literal, return the explanation as a conjunction. This method |
777 |
|
* relies on the above method. |
778 |
|
*/ |
779 |
|
Node mkExplainLit(TNode lit); |
780 |
|
//--------------------------- end standard safe explanation methods |
781 |
|
|
782 |
|
/** |
783 |
|
* Add term to the set of trigger terms with a corresponding tag. The notify class will get |
784 |
|
* notified when two trigger terms with the same tag become equal or dis-equal. The notification |
785 |
|
* will not happen on all the terms, but only on the ones that are represent the class. Note that |
786 |
|
* a term can be added more than once with different tags, and each tag appearance will merit |
787 |
|
* it's own notification. |
788 |
|
* |
789 |
|
* @param t the trigger term |
790 |
|
* @param theoryTag tag for this trigger (do NOT use THEORY_LAST) |
791 |
|
*/ |
792 |
|
void addTriggerTerm(TNode t, TheoryId theoryTag); |
793 |
|
|
794 |
|
/** |
795 |
|
* Returns true if t is a trigger term or in the same equivalence |
796 |
|
* class as some other trigger term. |
797 |
|
*/ |
798 |
|
bool isTriggerTerm(TNode t, TheoryId theoryTag) const; |
799 |
|
|
800 |
|
/** |
801 |
|
* Returns the representative trigger term of the given term. |
802 |
|
* |
803 |
|
* @param t the term to check where isTriggerTerm(t) should be true |
804 |
|
*/ |
805 |
|
TNode getTriggerTermRepresentative(TNode t, TheoryId theoryTag) const; |
806 |
|
|
807 |
|
/** |
808 |
|
* Adds a notify trigger for the predicate p, where notice that p can be |
809 |
|
* an equality. When the predicate becomes true, eqNotifyTriggerPredicate will |
810 |
|
* be called with value = true, and when predicate becomes false |
811 |
|
* eqNotifyTriggerPredicate will be called with value = false. |
812 |
|
* |
813 |
|
* Notice that if p is an equality, then we use a separate method for |
814 |
|
* determining when to call eqNotifyTriggerPredicate. |
815 |
|
*/ |
816 |
|
void addTriggerPredicate(TNode predicate); |
817 |
|
|
818 |
|
/** |
819 |
|
* Returns true if the two terms are equal. Requires both terms to |
820 |
|
* be in the database. |
821 |
|
*/ |
822 |
|
bool areEqual(TNode t1, TNode t2) const; |
823 |
|
|
824 |
|
/** |
825 |
|
* Check whether the two term are dis-equal. Requires both terms to |
826 |
|
* be in the database. |
827 |
|
*/ |
828 |
|
bool areDisequal(TNode t1, TNode t2, bool ensureProof) const; |
829 |
|
|
830 |
|
/** |
831 |
|
* Return the number of nodes in the equivalence class containing t |
832 |
|
* Adds t if not already there. |
833 |
|
*/ |
834 |
|
size_t getSize(TNode t); |
835 |
|
|
836 |
|
/** |
837 |
|
* Returns true if the engine is in a consistent state. |
838 |
|
*/ |
839 |
6930941 |
bool consistent() const { return !d_done; } |
840 |
|
|
841 |
|
/** Identify this equality engine (for debugging, etc..) */ |
842 |
|
std::string identify() const; |
843 |
|
}; |
844 |
|
|
845 |
|
} // Namespace eq |
846 |
|
} // Namespace theory |
847 |
|
} // namespace cvc5 |
848 |
|
|
849 |
|
#endif |