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 provides
51 : : * 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 : 275789 : 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 : 1296898 : bool isInterpretedFunctionKind(Kind fun) const
152 : : {
153 : 1296898 : 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 : 1296898 : bool isExternalOperatorKind(Kind fun) const
160 : : {
161 : 1296898 : 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 : 5069914 : 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 : 17781472 : 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 evaluation of constants) */
300 : : KindMap d_congruenceKindsInterpreted;
301 : :
302 : : /** The map of kinds with operators to be considered external (for higher-order) */
303 : : KindMap d_congruenceKindsExtOperators;
304 : :
305 : : /** Map from nodes to their ids */
306 : : std::unordered_map<TNode, EqualityNodeId> d_nodeIds;
307 : :
308 : : /** Map from function applications to their ids */
309 : : typedef std::unordered_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap;
310 : :
311 : : /**
312 : : * A map from a pair (a', b') to a function application f(a, b), where a' and b' are the current representatives
313 : : * of a and b.
314 : : */
315 : : ApplicationIdsMap d_applicationLookup;
316 : :
317 : : /** Application lookups in order, so that we can backtrack. */
318 : : std::vector<FunctionApplication> d_applicationLookups;
319 : :
320 : : /** Number of application lookups, for backtracking. */
321 : : context::CDO<DefaultSizeType> d_applicationLookupsCount;
322 : :
323 : : /**
324 : : * Return the number of nodes in the equivalence class containing t
325 : : * Adds t if not already there.
326 : : */
327 : : size_t getSize(TNode t);
328 : : /**
329 : : * Store the application lookup, with enough information to backtrack
330 : : */
331 : : void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId);
332 : :
333 : : /** notify trigger term equality */
334 : 12761516 : bool notifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
335 : : {
336 : : // since we will be generating an equality, we orient t1/t2 in the standard
337 : : // equality order used by the rewriter for most theories.
338 [ + + ]: 12761516 : if (t1 > t2)
339 : : {
340 : 2689470 : return d_notify->eqNotifyTriggerTermEquality(tag, t2, t1, value);
341 : : }
342 : 10072046 : return d_notify->eqNotifyTriggerTermEquality(tag, t1, t2, value);
343 : : }
344 : :
345 : : /** Map from ids to the nodes (these need to be nodes as we pick up the operators) */
346 : : std::vector<Node> d_nodes;
347 : :
348 : : /** A context-dependents count of nodes */
349 : : context::CDO<DefaultSizeType> d_nodesCount;
350 : :
351 : : /** Map from ids to the applications */
352 : : std::vector<FunctionApplicationPair> d_applications;
353 : :
354 : : /** Map from ids to the equality nodes */
355 : : std::vector<EqualityNode> d_equalityNodes;
356 : :
357 : : /** Number of asserted equalities we have so far */
358 : : context::CDO<DefaultSizeType> d_assertedEqualitiesCount;
359 : :
360 : : /** Memory for the use-list nodes */
361 : : std::vector<UseListNode> d_useListNodes;
362 : :
363 : : /**
364 : : * We keep a list of asserted equalities. Not among original terms, but
365 : : * among the class representatives.
366 : : */
367 : : struct Equality {
368 : : /** Left hand side of the equality */
369 : : EqualityNodeId d_lhs;
370 : : /** Right hand side of the equality */
371 : : EqualityNodeId d_rhs;
372 : : /** Equality constructor */
373 : 61170241 : Equality(EqualityNodeId l = null_id, EqualityNodeId r = null_id)
374 : 61170241 : : d_lhs(l), d_rhs(r)
375 : : {
376 : 61170241 : }
377 : : };/* struct EqualityEngine::Equality */
378 : :
379 : : /** The ids of the classes we have merged */
380 : : std::vector<Equality> d_assertedEqualities;
381 : :
382 : : /** The reasons for the equalities */
383 : :
384 : : /**
385 : : * An edge in the equality graph. This graph is an undirected graph (both edges added)
386 : : * containing the actual asserted equalities.
387 : : */
388 : : class EqualityEdge {
389 : :
390 : : // The id of the RHS of this equality
391 : : EqualityNodeId d_nodeId;
392 : : // The next edge
393 : : EqualityEdgeId d_nextId;
394 : : // Type of reason for this equality
395 : : unsigned d_mergeType;
396 : : // Reason of this equality
397 : : TNode d_reason;
398 : :
399 : : public:
400 : :
401 : 0 : EqualityEdge():
402 : 0 : d_nodeId(null_edge), d_nextId(null_edge), d_mergeType(MERGED_THROUGH_CONGRUENCE) {}
403 : :
404 : 122340482 : EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, unsigned type, TNode reason):
405 : 122340482 : d_nodeId(nodeId), d_nextId(nextId), d_mergeType(type), d_reason(reason) {}
406 : :
407 : : /** Returns the id of the next edge */
408 : 179179562 : EqualityEdgeId getNext() const { return d_nextId; }
409 : :
410 : : /** Returns the id of the target edge node */
411 : 215349554 : EqualityNodeId getNodeId() const { return d_nodeId; }
412 : :
413 : : /** The reason of this edge */
414 : 9826921 : unsigned getReasonType() const { return d_mergeType; }
415 : :
416 : : /** The reason of this edge */
417 : 9826921 : TNode getReason() const { return d_reason; }
418 : : };/* class EqualityEngine::EqualityEdge */
419 : :
420 : : /**
421 : : * All the equality edges (twice as many as the number of asserted equalities. If an equality
422 : : * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hence, having the index
423 : : * of one of the edges you can reconstruct the original equality.
424 : : */
425 : : std::vector<EqualityEdge> d_equalityEdges;
426 : :
427 : : /**
428 : : * Returns the string representation of the edges.
429 : : */
430 : : std::string edgesToString(EqualityEdgeId edgeId) const;
431 : :
432 : : /**
433 : : * Map from a node to its first edge in the equality graph. Edges are added to the front of the
434 : : * list which makes the insertion/backtracking easy.
435 : : */
436 : : std::vector<EqualityEdgeId> d_equalityGraph;
437 : :
438 : : /** Add an edge to the equality graph */
439 : : void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason);
440 : :
441 : : /** Returns the equality node of the given node */
442 : : EqualityNode& getEqualityNode(TNode node);
443 : :
444 : : /** Returns the equality node of the given node */
445 : : const EqualityNode& getEqualityNode(TNode node) const;
446 : :
447 : : /** Returns the equality node of the given node */
448 : : EqualityNode& getEqualityNode(EqualityNodeId nodeId);
449 : :
450 : : /** Returns the equality node of the given node */
451 : : const EqualityNode& getEqualityNode(EqualityNodeId nodeId) const;
452 : :
453 : : /** Returns the id of the node */
454 : : EqualityNodeId getNodeId(TNode node) const;
455 : :
456 : : /**
457 : : * Merge the class2 into class1
458 : : * @return true if ok, false if to break out
459 : : */
460 : : bool merge(EqualityNode& class1, EqualityNode& class2, std::vector<TriggerId>& triggers);
461 : :
462 : : /** Undo the merge of class2 into class1 */
463 : : void undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id);
464 : :
465 : : /** Backtrack the information if necessary */
466 : : void backtrack();
467 : :
468 : : /**
469 : : * Trigger that will be updated
470 : : */
471 : : struct Trigger {
472 : : /** The current class id of the LHS of the trigger */
473 : : EqualityNodeId d_classId;
474 : : /** Next trigger for class */
475 : : TriggerId d_nextTrigger;
476 : :
477 : 6826436 : Trigger(EqualityNodeId classId = null_id,
478 : : TriggerId nextTrigger = null_trigger)
479 : 6826436 : : d_classId(classId), d_nextTrigger(nextTrigger)
480 : : {
481 : 6826436 : }
482 : : };/* struct EqualityEngine::Trigger */
483 : :
484 : : /**
485 : : * Vector of triggers. Triggers come in pairs for an
486 : : * equality trigger (t1, t2): one at position 2k for t1, and one at position 2k + 1 for t2. When
487 : : * updating triggers we always know where the other one is (^1).
488 : : */
489 : : std::vector<Trigger> d_equalityTriggers;
490 : :
491 : : /**
492 : : * Vector of original equalities of the triggers.
493 : : */
494 : : std::vector<TriggerInfo> d_equalityTriggersOriginal;
495 : :
496 : : /**
497 : : * Context dependent count of triggers
498 : : */
499 : : context::CDO<DefaultSizeType> d_equalityTriggersCount;
500 : :
501 : : /**
502 : : * Trigger lists per node. The begin id changes as we merge, but the end always points to
503 : : * the actual end of the triggers for this node.
504 : : */
505 : : std::vector<TriggerId> d_nodeTriggers;
506 : :
507 : : /**
508 : : * Map from ids to whether they are constants (constants are always
509 : : * representatives of their class.
510 : : */
511 : : std::vector<bool> d_isConstant;
512 : :
513 : : /**
514 : : * Map from ids of proper terms, to the number of non-constant direct subterms. If we update an interpreted
515 : : * application to a constant, we can decrease this value. If we hit 0, we can evaluate the term.
516 : : *
517 : : */
518 : : std::vector<unsigned> d_subtermsToEvaluate;
519 : :
520 : : /**
521 : : * For nodes that we need to postpone evaluation.
522 : : */
523 : : std::queue<EqualityNodeId> d_evaluationQueue;
524 : :
525 : : /**
526 : : * Evaluate all terms in the evaluation queue.
527 : : */
528 : : void processEvaluationQueue();
529 : :
530 : : /** Vector of nodes that evaluate. */
531 : : std::vector<EqualityNodeId> d_subtermEvaluates;
532 : :
533 : : /** Size of the nodes that evaluate vector. */
534 : : context::CDO<unsigned> d_subtermEvaluatesSize;
535 : :
536 : : /** Set the node evaluate flag */
537 : : void subtermEvaluates(EqualityNodeId id);
538 : :
539 : : /**
540 : : * Returns the evaluation of the term when all (direct) children are replaced with
541 : : * the constant representatives.
542 : : */
543 : : Node evaluateTerm(TNode node);
544 : :
545 : : /**
546 : : * Returns true if it's a constant
547 : : */
548 : 374841 : bool isConstant(EqualityNodeId id) const {
549 : 374841 : return d_isConstant[getEqualityNode(id).getFind()];
550 : : }
551 : :
552 : : /**
553 : : * Map from ids to whether they are Boolean.
554 : : */
555 : : std::vector<bool> d_isEquality;
556 : :
557 : : /**
558 : : * Map from ids to whether the nods is internal. An internal node is a node
559 : : * that corresponds to a partially currified node, for example.
560 : : */
561 : : std::vector<bool> d_isInternal;
562 : :
563 : : /**
564 : : * Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId.
565 : : */
566 : : void addTriggerToList(EqualityNodeId nodeId, TriggerId triggerId);
567 : :
568 : : /** Statistics */
569 : : Statistics d_stats;
570 : :
571 : : /** Add a new function application node to the database, i.e APP t1 t2 */
572 : : EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, FunctionApplicationType type);
573 : :
574 : : /** Add a new node to the database */
575 : : EqualityNodeId newNode(TNode t);
576 : :
577 : : /** Propagation queue */
578 : : std::deque<MergeCandidate> d_propagationQueue;
579 : :
580 : : /** Enqueue to the propagation queue */
581 : : void enqueue(const MergeCandidate& candidate, bool back = true);
582 : :
583 : : /** Do the propagation */
584 : : void propagate();
585 : :
586 : : /** Are we in propagate */
587 : : bool d_inPropagate;
588 : :
589 : : /** Construction of equality conclusions for EqProofs
590 : : *
591 : : * Given two equality node ids, build an equality between the nodes they
592 : : * correspond to and add it as a conclusion to the given EqProof.
593 : : *
594 : : * The equality is only built if the nodes the ids correspond to are not
595 : : * internal nodes in the equality engine, i.e., they correspond to full
596 : : * applications of the respective kinds. Since the equality engine also
597 : : * applies congruence over n-ary kinds, internal nodes, i.e., partial
598 : : * applications, may still correspond to "full applications" in the
599 : : * first-order sense. Therefore this method also checks, in the case of n-ary
600 : : * congruence kinds, if an equality between "full applications" can be built.
601 : : */
602 : : void buildEqConclusion(EqualityNodeId id1,
603 : : EqualityNodeId id2,
604 : : EqProof* eqp) const;
605 : :
606 : : /**
607 : : * Get an explanation of the equality t1 = t2. Returns the asserted equalities
608 : : * that imply t1 = t2. Returns TNodes as the assertion equalities should be
609 : : * hashed somewhere else.
610 : : *
611 : : * This call refers to terms t1 and t2 by their ids t1Id and t2Id.
612 : : *
613 : : * If eqp is non-null, then this method populates eqp's information and
614 : : * children such that it is a proof of t1 = t2.
615 : : *
616 : : * We cache results of this call in cache, where cache[t1Id][t2Id] stores
617 : : * a proof of t1 = t2.
618 : : */
619 : : void getExplanation(
620 : : EqualityEdgeId t1Id,
621 : : EqualityNodeId t2Id,
622 : : std::vector<TNode>& equalities,
623 : : std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>& cache,
624 : : EqProof* eqp) const;
625 : :
626 : : /**
627 : : * Print the equality graph.
628 : : */
629 : : void debugPrintGraph() const;
630 : :
631 : : /** The true node */
632 : : Node d_true;
633 : : /** True node id */
634 : : EqualityNodeId d_trueId;
635 : :
636 : : /** The false node */
637 : : Node d_false;
638 : : /** False node id */
639 : : EqualityNodeId d_falseId;
640 : :
641 : : /**
642 : : * Adds an equality of terms t1 and t2 to the database.
643 : : */
644 : : void assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
645 : :
646 : : /**
647 : : * Adds a trigger equality to the database with the trigger node and polarity for notification.
648 : : */
649 : : void addTriggerEqualityInternal(TNode t1, TNode t2, TNode trigger, bool polarity);
650 : :
651 : : /**
652 : : * This method gets called on backtracks from the context manager.
653 : : */
654 : 116901085 : void contextNotifyPop() override { backtrack(); }
655 : :
656 : : /**
657 : : * Constructor initialization stuff.
658 : : */
659 : : void init();
660 : :
661 : : /** Set of trigger terms */
662 : : struct TriggerTermSet {
663 : : /** Set of theories in this set */
664 : : TheoryIdSet d_tags;
665 : : /** The trigger terms */
666 : : EqualityNodeId d_triggers[0];
667 : : /** Returns the theory tags */
668 : : TheoryIdSet hasTrigger(TheoryId tag) const;
669 : : /** Returns a trigger by tag */
670 : : EqualityNodeId getTrigger(TheoryId tag) const;
671 : : };/* struct EqualityEngine::TriggerTermSet */
672 : :
673 : : /** Are the constants triggers */
674 : : bool d_constantsAreTriggers;
675 : : /**
676 : : * Are any terms triggers? If this is false, then all trigger terms are
677 : : * ignored (e.g. this means that addTriggerTerm is equivalent to addTerm).
678 : : */
679 : : bool d_anyTermsAreTriggers;
680 : :
681 : : /** The information about trigger terms is stored in this easily maintained memory. */
682 : : char* d_triggerDatabase;
683 : :
684 : : /** Allocated size of the trigger term database */
685 : : DefaultSizeType d_triggerDatabaseAllocatedSize;
686 : :
687 : : /** Reference for the trigger terms set */
688 : : typedef DefaultSizeType TriggerTermSetRef;
689 : :
690 : : /** Null reference */
691 : : static const TriggerTermSetRef null_set_id = (TriggerTermSetRef)(-1);
692 : :
693 : : /** Create new trigger term set based on the internally set information */
694 : : TriggerTermSetRef newTriggerTermSet(TheoryIdSet newSetTags,
695 : : EqualityNodeId* newSetTriggers,
696 : : unsigned newSetTriggersSize);
697 : :
698 : : /** Get the trigger set give a reference */
699 : 164635004 : TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) {
700 [ - + ][ - + ]: 164635004 : Assert(ref < d_triggerDatabaseSize);
[ - - ]
701 : 164635004 : return *(reinterpret_cast<TriggerTermSet*>(d_triggerDatabase + ref));
702 : : }
703 : :
704 : : /** Get the trigger set give a reference */
705 : 15874880 : const TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) const {
706 [ - + ][ - + ]: 15874880 : Assert(ref < d_triggerDatabaseSize);
[ - - ]
707 : 15874880 : return *(reinterpret_cast<const TriggerTermSet*>(d_triggerDatabase + ref));
708 : : }
709 : :
710 : : /** Used part of the trigger term database */
711 : : context::CDO<DefaultSizeType> d_triggerDatabaseSize;
712 : :
713 : : struct TriggerSetUpdate {
714 : : EqualityNodeId d_classId;
715 : : TriggerTermSetRef d_oldValue;
716 : 10782325 : TriggerSetUpdate(EqualityNodeId classId = null_id,
717 : : TriggerTermSetRef oldValue = null_set_id)
718 : 10782325 : : d_classId(classId), d_oldValue(oldValue)
719 : : {
720 : 10782325 : }
721 : : };/* struct EqualityEngine::TriggerSetUpdate */
722 : :
723 : : /**
724 : : * List of trigger updates for backtracking.
725 : : */
726 : : std::vector<TriggerSetUpdate> d_triggerTermSetUpdates;
727 : :
728 : : /**
729 : : * Size of the individual triggers list.
730 : : */
731 : : context::CDO<unsigned> d_triggerTermSetUpdatesSize;
732 : :
733 : : /**
734 : : * Map from ids to the individual trigger set representatives.
735 : : */
736 : : std::vector<TriggerTermSetRef> d_nodeIndividualTrigger;
737 : :
738 : : typedef std::unordered_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap;
739 : :
740 : : /**
741 : : * A map from pairs of disequal terms, to the reason why we deduced they are disequal.
742 : : */
743 : : DisequalityReasonsMap d_disequalityReasonsMap;
744 : :
745 : : /**
746 : : * A list of all the disequalities we deduced.
747 : : */
748 : : std::vector<EqualityPair> d_deducedDisequalities;
749 : :
750 : : /**
751 : : * Context dependent size of the deduced disequalities
752 : : */
753 : : context::CDO<size_t> d_deducedDisequalitiesSize;
754 : :
755 : : /**
756 : : * For each disequality deduced, we add the pairs of equivalences needed to explain it.
757 : : */
758 : : std::vector<EqualityPair> d_deducedDisequalityReasons;
759 : :
760 : : /**
761 : : * Size of the memory for disequality reasons.
762 : : */
763 : : context::CDO<size_t> d_deducedDisequalityReasonsSize;
764 : :
765 : : /**
766 : : * Map from equalities to the tags that have received the notification.
767 : : */
768 : : typedef context::
769 : : CDHashMap<EqualityPair, TheoryIdSet, EqualityPairHashFunction>
770 : : PropagatedDisequalitiesMap;
771 : : PropagatedDisequalitiesMap d_propagatedDisequalities;
772 : :
773 : : /**
774 : : * Has this equality been propagated to anyone.
775 : : */
776 : : bool hasPropagatedDisequality(EqualityNodeId lhsId, EqualityNodeId rhsId) const;
777 : :
778 : : /**
779 : : * Has this equality been propagated to the tag owner.
780 : : */
781 : : bool hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) const;
782 : :
783 : : /**
784 : : * Stores a propagated disequality for explanation purposes and remembers the reasons. The
785 : : * reasons should be pushed on the reasons vector.
786 : : */
787 : : void storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId);
788 : :
789 : : /**
790 : : * An equality tagged with a set of tags.
791 : : */
792 : : struct TaggedEquality {
793 : : /** Id of the equality */
794 : : EqualityNodeId d_equalityId;
795 : : /** TriggerSet reference for the class of one of the sides */
796 : : TriggerTermSetRef d_triggerSetRef;
797 : : /** Is trigger equivalent to the lhs (rhs otherwise) */
798 : : bool d_lhs;
799 : :
800 : 1679486 : TaggedEquality(EqualityNodeId equalityId = null_id,
801 : : TriggerTermSetRef triggerSetRef = null_set_id,
802 : : bool lhs = true)
803 : 1679486 : : d_equalityId(equalityId), d_triggerSetRef(triggerSetRef), d_lhs(lhs)
804 : : {
805 : 1679486 : }
806 : : };
807 : :
808 : : /** A map from equivalence class id's to tagged equalities */
809 : : typedef std::vector<TaggedEquality> TaggedEqualitiesSet;
810 : :
811 : : /**
812 : : * Returns a set of equalities that have been asserted false where one side of the equality
813 : : * belongs to the given equivalence class. The equalities are restricted to the ones where
814 : : * one side of the equality is in the tags set, but the other one isn't. Each returned
815 : : * dis-equality is associated with the tags that are the subset of the input tags, such that
816 : : * exactly one side of the equality is not in the set yet.
817 : : *
818 : : * @param classId the equivalence class to search
819 : : * @param inputTags the tags to filter the equalities
820 : : * @param out the output equalities, as described above
821 : : */
822 : : void getDisequalities(bool allowConstants,
823 : : EqualityNodeId classId,
824 : : TheoryIdSet inputTags,
825 : : TaggedEqualitiesSet& out);
826 : :
827 : : /**
828 : : * Propagates the remembered disequalities with given tags the original triggers for those tags,
829 : : * and the set of disequalities produced by above.
830 : : */
831 : : bool propagateTriggerTermDisequalities(
832 : : TheoryIdSet tags,
833 : : TriggerTermSetRef triggerSetRef,
834 : : const TaggedEqualitiesSet& disequalitiesToNotify);
835 : :
836 : : /** Name of the equality engine */
837 : : std::string d_name;
838 : :
839 : : /** The internal addTerm */
840 : : void addTermInternal(TNode t, bool isOperator = false);
841 : : /**
842 : : * Adds a notify trigger for equality. When equality becomes true
843 : : * eqNotifyTriggerPredicate will be called with value = true, and when
844 : : * equality becomes false eqNotifyTriggerPredicate will be called with value =
845 : : * false.
846 : : */
847 : : void addTriggerEquality(TNode equality);
848 : : };
849 : :
850 : : } // Namespace eq
851 : : } // Namespace theory
852 : : } // namespace cvc5::internal
853 : :
854 : : #endif
|
