GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/equality_engine.h Lines: 37 39 94.9 %
Date: 2021-03-23 Branches: 5 34 14.7 %

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