src/theory/bv/equality_engine.h

   1 #include "cvc4_private.h"
   2
   3 #pragma once
   4
   5 #include <vector>
   6 #include <ext/hash_map>
   7
   8 #include "expr/node.h"
   9 #include "context/cdo.h"
  10 #include "util/output.h"
  11
  12 namespace CVC4 {
  13 namespace theory {
  14 namespace bv {
  15
  16 struct BitSizeTraits {
  17
  18   /** The null id */
  19   static const size_t id_null; // Defined in the cpp file (GCC bug)
  20   /** The null trigger id */
  21   static const size_t trigger_id_null;
  22
  23   /** Number of bits we use for the id */
  24   static const size_t id_bits   = 24;
  25   /** Number of bits we use for the size the equivalence class */
  26   static const size_t size_bits = 16;
  27   /** Number of bits we use for the trigger id */
  28   static const size_t trigger_id_bits = 24;
  29
  30 };
  31
  32 class EqualityNode {
  33
  34 public:
  35
  36   /** The size of this equivalence class (if it's a representative) */
  37   size_t d_size   : BitSizeTraits::size_bits;
  38
  39   /** The id (in the eq-manager) of the representative equality node */
  40   size_t d_findId : BitSizeTraits::id_bits;
  41
  42   /** The next equality node in this class */
  43   size_t d_nextId : BitSizeTraits::id_bits;
  44
  45 public:
  46
  47   /**
  48    * Creates a new node, which is in a list of it's own.
  49    */
  50   EqualityNode(size_t nodeId = BitSizeTraits::id_null)
  51   : d_size(1), d_findId(nodeId), d_nextId(nodeId) {}
  52
  53   /** Initialize the equality node */
  54   inline void init(size_t nodeId) {
  55     d_size = 1;
  56     d_findId = d_nextId = nodeId;
  57   }
  58
  59   /**
  60    * Returns the next node in the class circural list.
  61    */
  62   inline size_t getNext() const {
  63     return d_nextId;
  64   }
  65
  66   /**
  67    * Returns the size of this equivalence class (only valid if this is the representative).
  68    */
  69   inline size_t getSize() const {
  70     return d_size;
  71   }
  72
  73   /**
  74    * Merges the two lists. If add size is true the size of this node is increased by the size of
  75    * the other node, otherwise the size is decreased by the size of the other node.
  76    */
  77   template<bool addSize>
  78   inline void merge(EqualityNode& other) {
  79     size_t tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp;
  80     if (addSize) {
  81       d_size += other.d_size;
  82     } else {
  83       d_size -= other.d_size;
  84     }
  85   }
  86
  87   /**
  88    * Returns the class representative.
  89    */
  90   inline size_t getFind() const { return d_findId; }
  91
  92   /**
  93    * Set the class representative.
  94    */
  95   inline void setFind(size_t findId) { d_findId = findId; }
  96
  97 };
  98
  99
 100 template <typename OwnerClass, typename NotifyClass>
 101 class EqualityEngine {
 102
 103   /** The class to notify when a representative changes for a term */
 104   NotifyClass d_notify;
 105
 106   /** Map from nodes to their ids */
 107   __gnu_cxx::hash_map<TNode, size_t, TNodeHashFunction> d_nodeIds;
 108
 109   /** Map from ids to the nodes */
 110   std::vector<Node> d_nodes;
 111
 112   /** Map from ids to the equality nodes */
 113   std::vector<EqualityNode> d_equalityNodes;
 114
 115   /** Number of asserted equalities we have so far */
 116   context::CDO<size_t> d_assertedEqualitiesCount;
 117
 118   /**
 119    * We keep a list of asserted equalities. Not among original terms, but
 120    * among the class representatives.
 121    */
 122   struct Equality {
 123     /** Left hand side of the equality */
 124     size_t lhs : BitSizeTraits::id_bits;
 125     /** Right hand side of the equality */
 126     size_t rhs : BitSizeTraits::id_bits;
 127     /** Equality constructor */
 128     Equality(size_t lhs = BitSizeTraits::id_null, size_t rhs = BitSizeTraits::id_null)
 129     : lhs(lhs), rhs(rhs) {}
 130   };
 131
 132   /** The ids of the classes we have merged */
 133   std::vector<Equality> d_assertedEqualities;
 134
 135   /**
 136    * An edge in the equality graph. This graph is an undirected graph (both edges added)
 137    * containing the actual asserted equalities.
 138    */
 139   class EqualityEdge {
 140
 141     // The id of the RHS of this equality
 142     size_t d_nodeId : BitSizeTraits::id_bits;
 143     // The next edge
 144     size_t d_nextId : BitSizeTraits::id_bits;
 145
 146   public:
 147
 148     EqualityEdge(size_t nodeId = BitSizeTraits::id_null, size_t nextId = BitSizeTraits::id_null)
 149     : d_nodeId(nodeId), d_nextId(nextId) {}
 150
 151     /** Returns the id of the next edge */
 152     inline size_t getNext() const { return d_nextId; }
 153
 154     /** Returns the id of the target edge node */
 155     inline size_t getNodeId() const { return d_nodeId; }
 156   };
 157
 158   /**
 159    * All the equality edges (twice as many as the number of asserted equalities. If an equality
 160    * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hance, having the index
 161    * of one of the edges you can reconstruct the original equality.
 162    */
 163   std::vector<EqualityEdge> d_equalityEdges;
 164
 165   /**
 166    * Map from a node to it's first edge in the equality graph. Edges are added to the front of the
 167    * list which makes the insertion/backtracking easy.
 168    */
 169   std::vector<size_t> d_equalityGraph;
 170
 171   /** Add an edge to the equality graph */
 172   inline void addGraphEdge(size_t t1, size_t t2);
 173
 174   /** Returns the equality node of the given node */
 175   inline EqualityNode& getEqualityNode(TNode node);
 176
 177   /** Returns the equality node of the given node */
 178   inline EqualityNode& getEqualityNode(size_t nodeId);
 179
 180   /** Returns the id of the node */
 181   inline size_t getNodeId(TNode node) const;
 182
 183   /** Merge the class2 into class1 */
 184   void merge(EqualityNode& class1, EqualityNode& class2, std::vector<size_t>& triggers);
 185
 186   /** Undo the mereg of class2 into class1 */
 187   void undoMerge(EqualityNode& class1, EqualityNode& class2, size_t class2Id);
 188
 189   /** Backtrack the information if necessary */
 190   void backtrack();
 191
 192   /**
 193    * Data used in the BFS search through the equality graph.
 194    */
 195   struct BfsData {
 196     // The current node
 197     size_t nodeId : BitSizeTraits::id_bits;
 198     // The index of the edge we traversed
 199     size_t edgeId : BitSizeTraits::id_bits;
 200     // Index in the queue of the previous node. Shouldn't be too much of them, at most the size
 201     // of the biggest equivalence class
 202     size_t previousIndex : BitSizeTraits::size_bits;
 203
 204     BfsData(size_t nodeId = BitSizeTraits::id_null, size_t edgeId = BitSizeTraits::id_null, size_t prev = 0)
 205     : nodeId(nodeId), edgeId(edgeId), previousIndex(prev) {}
 206   };
 207
 208   /**
 209    * Trigger that will be updated
 210    */
 211   struct Trigger {
 212     /** The current class id of the LHS of the trigger */
 213     size_t classId : BitSizeTraits::id_bits;
 214     /** Next trigger for class 1 */
 215     size_t nextTrigger : BitSizeTraits::id_bits;
 216
 217     Trigger(size_t classId, size_t nextTrigger)
 218     : classId(classId), nextTrigger(nextTrigger) {}
 219   };
 220
 221   /**
 222    * Vector of triggers (persistent and not-backtrackable). Triggers come in pairs for an
 223    * equality trigger (t1, t2): one at position 2k for t1, and one at position 2k + 1 for t2. When
 224    * updating triggers we always know where the other one is (^1).
 225    */
 226   std::vector<Trigger> d_equalityTriggers;
 227
 228   /**
 229    * Trigger lists per node. The begin id changes as we merge, but the end always points to
 230    * the acutal end of the triggers for this node.
 231    */
 232   std::vector<size_t> d_nodeTriggers;
 233
 234   /**
 235    * Adds the trigger with triggerId to the begining of the trigger list of the node with id nodeId.
 236    */
 237   inline void addTriggerToList(size_t nodeId, size_t triggerId);
 238
 239 public:
 240
 241   /**
 242    * Initialize the equalty engine, given the owning class. This will initialize the notifier with
 243    * the owner information.
 244    */
 245   EqualityEngine(OwnerClass& owner, context::Context* context)
 246   : d_notify(owner), d_assertedEqualitiesCount(context, 0) {
 247     Debug("equality") << "EqualityEdge::EqualityEdge(): id_null = " << BitSizeTraits::id_null <<
 248         ", trigger_id_null = " << BitSizeTraits::trigger_id_null << std::endl;
 249   }
 250
 251   /**
 252    * Adds a term to the term database. Returns the internal id of the term.
 253    */
 254   size_t addTerm(TNode t);
 255
 256   /**
 257    * Check whether the node is already in the database.
 258    */
 259   inline bool hasTerm(TNode t) const;
 260
 261   /**
 262    * Adds an equality t1 = t2 to the database. Returns false if any of the triggers failed.
 263    */
 264   bool addEquality(TNode t1, TNode t2);
 265
 266   /**
 267    * Returns the representative of the term t.
 268    */
 269   inline TNode getRepresentative(TNode t) const;
 270
 271   /**
 272    * Returns true if the two nodes are in the same class.
 273    */
 274   inline bool areEqual(TNode t1, TNode t2) const;
 275
 276   /**
 277    * Get an explanation of the equality t1 = t2. Returns the asserted equalities that
 278    * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
 279    * else. TODO: mark the phantom equalities (skolems).
 280    */
 281   void getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const;
 282
 283   /**
 284    * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with
 285    * (t1, t2).
 286    */
 287   size_t addTrigger(TNode t1, TNode t2);
 288
 289 };
 290
 291 template <typename OwnerClass, typename NotifyClass>
 292 size_t EqualityEngine<OwnerClass, NotifyClass>::addTerm(TNode t) {
 293
 294   Debug("equality") << "EqualityEngine::addTerm(" << t << ")" << std::endl;
 295
 296   // If term already added, retrurn it's id
 297   if (hasTerm(t)) return getNodeId(t);
 298
 299   // Register the new id of the term
 300   size_t newId = d_nodes.size();
 301   d_nodeIds[t] = newId;
 302   // Add the node to it's position
 303   d_nodes.push_back(t);
 304   // Add the trigger list for this node
 305   d_nodeTriggers.push_back(BitSizeTraits::trigger_id_null);
 306   // Add it to the equality graph
 307   d_equalityGraph.push_back(BitSizeTraits::id_null);
 308   // Add the equality node to the nodes
 309   if (d_equalityNodes.size() <= newId) {
 310     d_equalityNodes.resize(newId + 100);
 311   }
 312   d_equalityNodes[newId].init(newId);
 313   // Return the id of the term
 314   return newId;
 315 }
 316
 317 template <typename OwnerClass, typename NotifyClass>
 318 bool EqualityEngine<OwnerClass, NotifyClass>::hasTerm(TNode t) const {
 319   return d_nodeIds.find(t) != d_nodeIds.end();
 320 }
 321
 322 template <typename OwnerClass, typename NotifyClass>
 323 size_t EqualityEngine<OwnerClass, NotifyClass>::getNodeId(TNode node) const {
 324   Assert(hasTerm(node));
 325   return (*d_nodeIds.find(node)).second;
 326 }
 327
 328 template <typename OwnerClass, typename NotifyClass>
 329 EqualityNode& EqualityEngine<OwnerClass, NotifyClass>::getEqualityNode(TNode t) {
 330   return getEqualityNode(getNodeId(t));
 331 }
 332
 333 template <typename OwnerClass, typename NotifyClass>
 334 EqualityNode& EqualityEngine<OwnerClass, NotifyClass>::getEqualityNode(size_t nodeId) {
 335   Assert(nodeId < d_equalityNodes.size());
 336   return d_equalityNodes[nodeId];
 337 }
 338
 339 template <typename OwnerClass, typename NotifyClass>
 340 bool EqualityEngine<OwnerClass, NotifyClass>::addEquality(TNode t1, TNode t2) {
 341
 342   Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
 343
 344   // Backtrack if necessary
 345   backtrack();
 346
 347   // Add the terms if they are not already in the database
 348   size_t t1Id = getNodeId(t1);
 349   size_t t2Id = getNodeId(t2);
 350
 351   // Get the representatives
 352   size_t t1classId = getEqualityNode(t1Id).getFind();
 353   size_t t2classId = getEqualityNode(t2Id).getFind();
 354
 355   // If already the same, we're done
 356   if (t1classId == t2classId) return true;
 357
 358   // Get the nodes of the representatives
 359   EqualityNode& node1 = getEqualityNode(t1classId);
 360   EqualityNode& node2 = getEqualityNode(t2classId);
 361
 362   Assert(node1.getFind() == t1classId);
 363   Assert(node2.getFind() == t2classId);
 364
 365   // Depending on the size, merge them
 366   std::vector<size_t> triggers;
 367   if (node1.getSize() < node2.getSize()) {
 368     merge(node2, node1, triggers);
 369     d_assertedEqualities.push_back(Equality(t2classId, t1classId));
 370   } else {
 371     merge(node1, node2, triggers);
 372     d_assertedEqualities.push_back(Equality(t1classId, t2classId));
 373   }
 374
 375   // Add the actuall equality to the equality graph
 376   addGraphEdge(t1Id, t2Id);
 377
 378   // One more equality added
 379   d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
 380
 381   Assert(2*d_assertedEqualities.size() == d_equalityEdges.size());
 382   Assert(d_assertedEqualities.size() == d_assertedEqualitiesCount);
 383
 384   // Notify the triggers
 385   for (size_t i = 0, i_end = triggers.size(); i < i_end; ++ i) {
 386     // Notify the trigger and exit if it fails
 387     if (!d_notify(triggers[i])) return false;
 388   }
 389
 390   return true;
 391 }
 392
 393 template <typename OwnerClass, typename NotifyClass>
 394 TNode EqualityEngine<OwnerClass, NotifyClass>::getRepresentative(TNode t) const {
 395
 396   Debug("equality") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl;
 397
 398   Assert(hasTerm(t));
 399
 400   // Both following commands are semantically const
 401   const_cast<EqualityEngine*>(this)->backtrack();
 402   size_t representativeId = const_cast<EqualityEngine*>(this)->getEqualityNode(t).getFind();
 403
 404   Debug("equality") << "EqualityEngine::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl;
 405
 406   return d_nodes[representativeId];
 407 }
 408
 409 template <typename OwnerClass, typename NotifyClass>
 410 bool EqualityEngine<OwnerClass, NotifyClass>::areEqual(TNode t1, TNode t2) const {
 411   Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ")" << std::endl;
 412
 413   Assert(hasTerm(t1));
 414   Assert(hasTerm(t2));
 415
 416   // Both following commands are semantically const
 417   const_cast<EqualityEngine*>(this)->backtrack();
 418   size_t rep1 = const_cast<EqualityEngine*>(this)->getEqualityNode(t1).getFind();
 419   size_t rep2 = const_cast<EqualityEngine*>(this)->getEqualityNode(t2).getFind();
 420
 421   Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl;
 422
 423   return rep1 == rep2;
 424 }
 425
 426 template <typename OwnerClass, typename NotifyClass>
 427 void EqualityEngine<OwnerClass, NotifyClass>::merge(EqualityNode& class1, EqualityNode& class2, std::vector<size_t>& triggers) {
 428
 429   Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
 430
 431   Assert(triggers.empty());
 432
 433   size_t class1Id = class1.getFind();
 434   size_t class2Id = class2.getFind();
 435
 436   // Update class2 representative information
 437   size_t currentId = class2Id;
 438   do {
 439     // Get the current node
 440     EqualityNode& currentNode = getEqualityNode(currentId);
 441
 442     // Update it's find to class1 id
 443     currentNode.setFind(class1Id);
 444
 445     // Go through the triggers and inform if necessary
 446     size_t currentTrigger = d_nodeTriggers[currentId];
 447     while (currentTrigger != BitSizeTraits::trigger_id_null) {
 448       Trigger& trigger = d_equalityTriggers[currentTrigger];
 449       Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1];
 450
 451       // If the two are not already in the same class
 452       if (otherTrigger.classId != trigger.classId) {
 453         trigger.classId = class1Id;
 454         // If they became the same, call the trigger
 455         if (otherTrigger.classId == class1Id) {
 456           // Id of the real trigger is half the internal one
 457           triggers.push_back(currentTrigger >> 1);
 458         }
 459       }
 460
 461       // Go to the next trigger
 462       currentTrigger = trigger.nextTrigger;
 463     }
 464
 465     // Move to the next node
 466     currentId = currentNode.getNext();
 467
 468   } while (currentId != class2Id);
 469
 470   // Now merge the lists
 471   class1.merge<true>(class2);
 472 }
 473
 474 template <typename OwnerClass, typename NotifyClass>
 475 void EqualityEngine<OwnerClass, NotifyClass>::undoMerge(EqualityNode& class1, EqualityNode& class2, size_t class2Id) {
 476
 477   Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl;
 478
 479   // Now unmerge the lists (same as merge)
 480   class1.merge<false>(class2);
 481
 482   // Update class2 representative information
 483   size_t currentId = class2Id;
 484   do {
 485     // Get the current node
 486     EqualityNode& currentNode = getEqualityNode(currentId);
 487
 488     // Update it's find to class1 id
 489     currentNode.setFind(class2Id);
 490
 491     // Go through the trigger list (if any) and undo the class
 492     size_t currentTrigger = d_nodeTriggers[currentId];
 493     while (currentTrigger != BitSizeTraits::trigger_id_null) {
 494       Trigger& trigger = d_equalityTriggers[currentTrigger];
 495       trigger.classId = class2Id;
 496       currentTrigger = trigger.nextTrigger;
 497     }
 498
 499     // Move to the next node
 500     currentId = currentNode.getNext();
 501
 502   } while (currentId != class2Id);
 503
 504 }
 505
 506 template <typename OwnerClass, typename NotifyClass>
 507 void EqualityEngine<OwnerClass, NotifyClass>::backtrack() {
 508
 509   // If we need to backtrack then do it
 510   if (d_assertedEqualitiesCount < d_assertedEqualities.size()) {
 511
 512     Debug("equality") << "EqualityEngine::backtrack(): nodes" << std::endl;
 513
 514     for (int i = (int)d_assertedEqualities.size() - 1, i_end = (int)d_assertedEqualitiesCount; i >= i_end; --i) {
 515       // Get the ids of the merged classes
 516       Equality& eq = d_assertedEqualities[i];
 517       // Undo the merge
 518       undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs);
 519     }
 520
 521     d_assertedEqualities.resize(d_assertedEqualitiesCount);
 522
 523     Debug("equality") << "EqualityEngine::backtrack(): edges" << std::endl;
 524
 525     for (int i = (int)d_equalityEdges.size() - 2, i_end = (int)(2*d_assertedEqualitiesCount); i >= i_end; i -= 2) {
 526       EqualityEdge& edge1 = d_equalityEdges[i];
 527       EqualityEdge& edge2 = d_equalityEdges[i | 1];
 528       d_equalityGraph[edge2.getNodeId()] = edge1.getNext();
 529       d_equalityGraph[edge1.getNodeId()] = edge2.getNext();
 530     }
 531
 532     d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
 533   }
 534
 535 }
 536
 537 template <typename OwnerClass, typename NotifyClass>
 538 void EqualityEngine<OwnerClass, NotifyClass>::addGraphEdge(size_t t1, size_t t2) {
 539   Debug("equality") << "EqualityEngine::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << ")" << std::endl;
 540   size_t edge = d_equalityEdges.size();
 541   d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1]));
 542   d_equalityEdges.push_back(EqualityEdge(t1, d_equalityGraph[t2]));
 543   d_equalityGraph[t1] = edge;
 544   d_equalityGraph[t2] = edge | 1;
 545 }
 546
 547 template <typename OwnerClass, typename NotifyClass>
 548 void EqualityEngine<OwnerClass, NotifyClass>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
 549   Assert(equalities.empty());
 550   Assert(t1 != t2);
 551   Assert(getRepresentative(t1) == getRepresentative(t2));
 552
 553   Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl;
 554
 555   const_cast<EqualityEngine*>(this)->backtrack();
 556
 557   // Queue for the BFS containing nodes
 558   std::vector<BfsData> bfsQueue;
 559
 560   // The id's of the nodes
 561   size_t t1Id = getNodeId(t1);
 562   size_t t2Id = getNodeId(t2);
 563
 564   // Find a path from t1 to t2 in the graph (BFS)
 565   bfsQueue.push_back(BfsData(t1Id, BitSizeTraits::id_null, 0));
 566   size_t currentIndex = 0;
 567   while (true) {
 568     // There should always be a path, and every node can be visited only once (tree)
 569     Assert(currentIndex < bfsQueue.size());
 570
 571     // The next node to visit
 572     BfsData& current = bfsQueue[currentIndex];
 573     size_t currentNode = current.nodeId;
 574
 575     Debug("equality") << "EqualityEngine::getExplanation(): currentNode =  " << d_nodes[currentNode] << std::endl;
 576
 577     // Go through the equality edges of this node
 578     size_t currentEdge = d_equalityGraph[currentNode];
 579
 580     while (currentEdge != BitSizeTraits::id_null) {
 581       // Get the edge
 582       const EqualityEdge& edge = d_equalityEdges[currentEdge];
 583
 584       // If not just the backwards edge
 585       if ((currentEdge | 1u) != (current.edgeId | 1u)) {
 586
 587         Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
 588
 589         // Did we find the path
 590         if (edge.getNodeId() == t2Id) {
 591
 592           Debug("equality") << "EqualityEngine::getExplanation(): path found: " << std::endl;
 593
 594           // Reconstruct the path
 595           do {
 596             // Get the left and right hand side from the edge
 597             size_t firstEdge = (currentEdge >> 1) << 1;
 598             size_t secondEdge = (currentEdge | 1);
 599             TNode lhs = d_nodes[d_equalityEdges[secondEdge].getNodeId()];
 600             TNode rhs = d_nodes[d_equalityEdges[firstEdge].getNodeId()];
 601             // Add the actual equality to the vector
 602             equalities.push_back(lhs.eqNode(rhs));
 603
 604             Debug("equality") << "EqualityEngine::getExplanation(): adding: " << lhs.eqNode(rhs) << std::endl;
 605
 606             // Go to the previous
 607             currentEdge = bfsQueue[currentIndex].edgeId;
 608             currentIndex = bfsQueue[currentIndex].previousIndex;
 609         } while (currentEdge != BitSizeTraits::id_null);
 610
 611         // Done
 612         return;
 613       }
 614
 615       // Push to the visitation queue if it's not the backward edge
 616         bfsQueue.push_back(BfsData(edge.getNodeId(), currentEdge, currentIndex));
 617       }
 618
 619       // Go to the next edge
 620       currentEdge = edge.getNext();
 621     }
 622
 623     // Go to the next node to visit
 624     ++ currentIndex;
 625   }
 626 }
 627
 628 template <typename OwnerClass, typename NotifyClass>
 629 size_t EqualityEngine<OwnerClass, NotifyClass>::addTrigger(TNode t1, TNode t2) {
 630
 631   Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ")" << std::endl;
 632
 633   Assert(hasTerm(t1));
 634   Assert(hasTerm(t2));
 635
 636   // Get the information about t1
 637   size_t t1Id = getNodeId(t1);
 638   size_t t1TriggerId = d_nodeTriggers[t1Id];
 639   size_t t1classId = getEqualityNode(t1Id).getFind();
 640
 641   // Get the information about t2
 642   size_t t2Id = getNodeId(t2);
 643   size_t t2TriggerId = d_nodeTriggers[t2Id];
 644   size_t t2classId = getEqualityNode(t2Id).getFind();
 645
 646   // Create the triggers
 647   size_t t1NewTriggerId = d_equalityTriggers.size();
 648   size_t t2NewTriggerId = t1NewTriggerId | 1;
 649   d_equalityTriggers.push_back(Trigger(t1classId, t1TriggerId));
 650   d_equalityTriggers.push_back(Trigger(t2classId, t2TriggerId));
 651
 652   // Add the trigger to the trigger graph
 653   d_nodeTriggers[t1Id] = t1NewTriggerId;
 654   d_nodeTriggers[t2Id] = t2NewTriggerId;
 655
 656   Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => " << t1NewTriggerId / 2 << std::endl;
 657
 658   // Return the global id of the trigger
 659   return t1NewTriggerId / 2;
 660 }
 661
 662 } // Namespace bv
 663 } // Namespace theory
 664 } // Namespace CVC4
 665