GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_traversal.h Lines: 5 5 100.0 %
Date: 2021-03-22 Branches: 4 8 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_traversal.h
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 "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__NODE_TRAVERSAL_H
18
#define CVC4__EXPR__NODE_TRAVERSAL_H
19
20
#include <iterator>
21
#include <unordered_map>
22
#include <vector>
23
24
#include "expr/node.h"
25
26
namespace CVC4 {
27
28
/**
29
 * Enum that represents an order in which nodes are visited.
30
 */
31
enum class VisitOrder
32
{
33
  PREORDER,
34
  POSTORDER
35
};
36
37
// Iterator for traversing a node in pre-/post-order
38
// It does DAG-traversal, so indentical sub-nodes will be visited once only.
39
class NodeDfsIterator
40
{
41
 public:
42
  // STL type definitions for an iterator
43
  using value_type = TNode;
44
  using pointer = TNode*;
45
  using reference = TNode&;
46
  using iterator_category = std::forward_iterator_tag;
47
  using difference_type = std::ptrdiff_t;
48
49
  // Construct a traversal iterator beginning at `n`
50
  NodeDfsIterator(TNode n, VisitOrder order, std::function<bool(TNode)> skipIf);
51
  // Construct an end-of-traversal iterator
52
  NodeDfsIterator(VisitOrder order);
53
54
  // Move/copy construction and assignment. Destructor.
55
40
  NodeDfsIterator(NodeDfsIterator&&) = default;
56
  NodeDfsIterator& operator=(NodeDfsIterator&&) = default;
57
96
  NodeDfsIterator(NodeDfsIterator&) = default;
58
  NodeDfsIterator& operator=(NodeDfsIterator&) = default;
59
1964
  ~NodeDfsIterator() = default;
60
61
  // Preincrement
62
  NodeDfsIterator& operator++();
63
  // Postincrement
64
  NodeDfsIterator operator++(int);
65
  // Dereference
66
  reference operator*();
67
  // Equals
68
  // It is not constant, because an unitilized node must be initialized before
69
  // comparison
70
  bool operator==(NodeDfsIterator&);
71
  // Not equals
72
  // It is not constant, because an unitilized node must be initialized before
73
  // comparison
74
  bool operator!=(NodeDfsIterator&);
75
76
 private:
77
  // While we're not at an appropriate visit (see d_postorder), advance.
78
  // In each step:
79
  //   * enqueue children of a not-yet-pre-visited node (and mark it
80
  //     previsited)
81
  //   * pop a not-yet-post-visited node (and mark it post-visited)
82
  //   * pop an already post-visited node.
83
  // After calling this, `d_current` will be changed to the next node, if there
84
  // is another node in the traversal.
85
  void advanceToNextVisit();
86
87
  // If this iterator hasn't been dereferenced or incremented yet, advance to
88
  // first visit.
89
  // Necessary because we are lazy and don't find our first visit node at
90
  // construction time.
91
  void initializeIfUninitialized();
92
93
  // Stack of nodes to visit.
94
  std::vector<TNode> d_stack;
95
96
  // Whether (and how) we've visited a node.
97
  // Absent if we haven't visited it.
98
  // Set to `false` if we've already pre-visited it (enqueued its children).
99
  // Set to `true` if we've also already post-visited it.
100
  std::unordered_map<TNode, bool, TNodeHashFunction> d_visited;
101
102
  // The visit order that this iterator is using
103
  VisitOrder d_order;
104
105
  // Current referent node. A valid node to visit if non-null.
106
  // Null after construction (but before first access) and at the end.
107
  TNode d_current;
108
109
  // When to omit a node and its descendants from the traversal
110
  std::function<bool(TNode)> d_skipIf;
111
};
112
113
// Node wrapper that is iterable in DAG pre-/post-order
114
class NodeDfsIterable
115
{
116
 public:
117
  /**
118
   * Creates a new node wrapper that can be used to iterate over the children
119
   * of a node in pre-/post-order.
120
   *
121
   * @param n The node the iterate
122
   * @param order The order in which the children are visited.
123
   * @param skipIf Function that determines whether a given node and its
124
   *               descendants should be skipped or not.
125
   */
126
  NodeDfsIterable(
127
      TNode n,
128
      VisitOrder order = VisitOrder::POSTORDER,
129
90
      std::function<bool(TNode)> skipIf = [](TNode) { return false; });
130
131
  // Move/copy construction and assignment. Destructor.
132
  NodeDfsIterable(NodeDfsIterable&&) = default;
133
  NodeDfsIterable& operator=(NodeDfsIterable&&) = default;
134
  NodeDfsIterable(NodeDfsIterable&) = default;
135
  NodeDfsIterable& operator=(NodeDfsIterable&) = default;
136
914
  ~NodeDfsIterable() = default;
137
138
  NodeDfsIterator begin() const;
139
  NodeDfsIterator end() const;
140
141
 private:
142
  TNode d_node;
143
  VisitOrder d_order;
144
  std::function<bool(TNode)> d_skipIf;
145
};
146
147
}  // namespace CVC4
148
149
#endif  // CVC4__EXPR__NODE_TRAVERSAL_H