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