GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_traversal.cpp Lines: 60 60 100.0 %
Date: 2021-03-23 Branches: 53 105 50.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_traversal.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Alex Ozdemir, Andres Noetzli
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 Iterators for traversing nodes.
13
 **/
14
15
#include "node_traversal.h"
16
17
#include <functional>
18
19
namespace CVC4 {
20
21
914
NodeDfsIterator::NodeDfsIterator(TNode n,
22
                                 VisitOrder order,
23
914
                                 std::function<bool(TNode)> skipIf)
24
    : d_stack{n},
25
      d_visited(),
26
      d_order(order),
27
      d_current(TNode()),
28
914
      d_skipIf(skipIf)
29
{
30
914
}
31
32
914
NodeDfsIterator::NodeDfsIterator(VisitOrder order)
33
    : d_stack(),
34
      d_visited(),
35
      d_order(order),
36
      d_current(TNode()),
37
914
      d_skipIf([](TNode) { return false; })
38
{
39
914
}
40
41
1877
NodeDfsIterator& NodeDfsIterator::operator++()
42
{
43
  // If we were just constructed, advance to first visit, **before**
44
  // advancing past it to the next visit (below).
45
1877
  initializeIfUninitialized();
46
47
  // Advance to the next visit
48
1877
  advanceToNextVisit();
49
1877
  return *this;
50
}
51
52
12
NodeDfsIterator NodeDfsIterator::operator++(int)
53
{
54
12
  NodeDfsIterator copyOfOld(*this);
55
12
  ++*this;
56
12
  return copyOfOld;
57
}
58
59
1879
TNode& NodeDfsIterator::operator*()
60
{
61
  // If we were just constructed, advance to first visit
62
1879
  initializeIfUninitialized();
63
1879
  Assert(!d_current.isNull());
64
65
1879
  return d_current;
66
}
67
68
2779
bool NodeDfsIterator::operator==(NodeDfsIterator& other)
69
{
70
  // Unitialize this node, and the other, before comparing.
71
2779
  initializeIfUninitialized();
72
2779
  other.initializeIfUninitialized();
73
  // The stack and current node uniquely represent traversal state. We need not
74
  // use the scheduled node set.
75
  //
76
  // Users should not compare iterators for traversals of different nodes, or
77
  // traversals with different skipIfs.
78
2779
  Assert(d_order == other.d_order);
79
2779
  return d_stack == other.d_stack && d_current == other.d_current;
80
}
81
82
2757
bool NodeDfsIterator::operator!=(NodeDfsIterator& other)
83
{
84
2757
  return !(*this == other);
85
}
86
87
8988
void NodeDfsIterator::advanceToNextVisit()
88
{
89
  // While a node is enqueued and we're not at the right visit type
90
11940
  while (!d_stack.empty())
91
  {
92
6945
    TNode back = d_stack.back();
93
4835
    auto visitEntry = d_visited.find(back);
94
4835
    if (visitEntry == d_visited.end())
95
    {
96
      // if we haven't pre-visited this node, pre-visit it
97
3571
      if (d_skipIf(back))
98
      {
99
        // actually, skip it if the skip predicate says so...
100
842
        d_stack.pop_back();
101
842
        continue;
102
      }
103
1887
      d_visited[back] = false;
104
1887
      d_current = back;
105
      // Use integer underflow to reverse-iterate
106
3931
      for (size_t n = back.getNumChildren(), i = n - 1; i < n; --i)
107
      {
108
2044
        d_stack.push_back(back[i]);
109
      }
110
1887
      if (d_order == VisitOrder::PREORDER)
111
      {
112
48
        return;
113
      }
114
    }
115
2106
    else if (d_order == VisitOrder::PREORDER || visitEntry->second)
116
    {
117
      // if we're previsiting or we've already post-visited this node: skip it
118
271
      d_stack.pop_back();
119
    }
120
    else
121
    {
122
      // otherwise, this is a post-visit
123
1835
      visitEntry->second = true;
124
1835
      d_current = back;
125
1835
      d_stack.pop_back();
126
1835
      return;
127
    }
128
  }
129
  // We're at the end of the traversal: nullify the current node to agree
130
  // with the "end" iterator.
131
4153
  d_current = TNode();
132
}
133
134
9314
void NodeDfsIterator::initializeIfUninitialized()
135
{
136
9314
  if (d_current.isNull())
137
  {
138
4159
    advanceToNextVisit();
139
  }
140
9314
}
141
142
914
NodeDfsIterable::NodeDfsIterable(TNode n,
143
                                 VisitOrder order,
144
914
                                 std::function<bool(TNode)> skipIf)
145
914
    : d_node(n), d_order(order), d_skipIf(skipIf)
146
{
147
914
}
148
149
914
NodeDfsIterator NodeDfsIterable::begin() const
150
{
151
914
  return NodeDfsIterator(d_node, d_order, d_skipIf);
152
}
153
154
914
NodeDfsIterator NodeDfsIterable::end() const
155
{
156
914
  return NodeDfsIterator(d_order);
157
}
158
159
26685
}  // namespace CVC4