src/theory/uf/equality_engine_iterator.cpp

   1 /*********************                                                        */
   2 /*! \file equality_engine_iterator.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 Implementation of iterator class for equality engine
  13  **/
  14
  15 #include "theory/uf/equality_engine_iterator.h"
  16
  17 #include "theory/uf/equality_engine.h"
  18
  19 namespace CVC4 {
  20 namespace theory {
  21 namespace eq {
  22
  23 EqClassesIterator::EqClassesIterator() : d_ee(nullptr), d_it(0) {}
  24
  25 EqClassesIterator::EqClassesIterator(const eq::EqualityEngine* ee) : d_ee(ee)
  26 {
  27   Assert(d_ee->consistent());
  28   d_it = 0;
  29   // Go to the first non-internal node that is it's own representative
  30   if (d_it < d_ee->d_nodesCount
  31       && (d_ee->d_isInternal[d_it]
  32           || d_ee->getEqualityNode(d_it).getFind() != d_it))
  33   {
  34     ++d_it;
  35   }
  36 }
  37
  38 Node EqClassesIterator::operator*() const { return d_ee->d_nodes[d_it]; }
  39
  40 bool EqClassesIterator::operator==(const EqClassesIterator& i) const
  41 {
  42   return d_ee == i.d_ee && d_it == i.d_it;
  43 }
  44
  45 bool EqClassesIterator::operator!=(const EqClassesIterator& i) const
  46 {
  47   return !(*this == i);
  48 }
  49
  50 EqClassesIterator& EqClassesIterator::operator++()
  51 {
  52   ++d_it;
  53   while (d_it < d_ee->d_nodesCount
  54          && (d_ee->d_isInternal[d_it]
  55              || d_ee->getEqualityNode(d_it).getFind() != d_it))
  56   {
  57     ++d_it;
  58   }
  59   return *this;
  60 }
  61
  62 EqClassesIterator EqClassesIterator::operator++(int)
  63 {
  64   EqClassesIterator i = *this;
  65   ++*this;
  66   return i;
  67 }
  68
  69 bool EqClassesIterator::isFinished() const
  70 {
  71   return d_it >= d_ee->d_nodesCount;
  72 }
  73
  74 EqClassIterator::EqClassIterator()
  75     : d_ee(nullptr), d_start(null_id), d_current(null_id)
  76 {
  77 }
  78
  79 EqClassIterator::EqClassIterator(Node eqc, const eq::EqualityEngine* ee)
  80     : d_ee(ee)
  81 {
  82   Assert(d_ee->consistent());
  83   d_current = d_start = d_ee->getNodeId(eqc);
  84   Assert(d_start == d_ee->getEqualityNode(d_start).getFind());
  85   Assert(!d_ee->d_isInternal[d_start]);
  86 }
  87
  88 Node EqClassIterator::operator*() const { return d_ee->d_nodes[d_current]; }
  89
  90 bool EqClassIterator::operator==(const EqClassIterator& i) const
  91 {
  92   return d_ee == i.d_ee && d_current == i.d_current;
  93 }
  94
  95 bool EqClassIterator::operator!=(const EqClassIterator& i) const
  96 {
  97   return !(*this == i);
  98 }
  99
 100 EqClassIterator& EqClassIterator::operator++()
 101 {
 102   Assert(!isFinished());
 103
 104   Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
 105   Assert(!d_ee->d_isInternal[d_current]);
 106
 107   // Find the next one
 108   do
 109   {
 110     d_current = d_ee->getEqualityNode(d_current).getNext();
 111   } while (d_ee->d_isInternal[d_current]);
 112
 113   Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
 114   Assert(!d_ee->d_isInternal[d_current]);
 115
 116   if (d_current == d_start)
 117   {
 118     // we end when we have cycled back to the original representative
 119     d_current = null_id;
 120   }
 121   return *this;
 122 }
 123
 124 EqClassIterator EqClassIterator::operator++(int)
 125 {
 126   EqClassIterator i = *this;
 127   ++*this;
 128   return i;
 129 }
 130
 131 bool EqClassIterator::isFinished() const { return d_current == null_id; }
 132
 133 }  // namespace eq
 134 }  // Namespace theory
 135 }  // Namespace CVC4