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