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

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