GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_visitor.h Lines: 33 33 100.0 %
Date: 2021-03-23 Branches: 89 178 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_visitor.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Andrew Reynolds, Morgan Deters
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 A simple visitor for nodes
13
 **
14
 ** A simple visitor for nodes.
15
 **/
16
17
#pragma once
18
19
#include "cvc4_private.h"
20
21
#include <vector>
22
23
#include "expr/node.h"
24
25
namespace CVC4 {
26
27
/**
28
 * Traverses the nodes reverse-topologically (children before parents),
29
 * calling the visitor in order.
30
 */
31
template<typename Visitor>
32
class NodeVisitor {
33
34
  /** For re-entry checking */
35
  static thread_local bool s_inRun;
36
37
  /**
38
   * Guard against NodeVisitor<> being re-entrant.
39
   */
40
  template <class T>
41
  class GuardReentry {
42
    T& d_guard;
43
  public:
44
894605
    GuardReentry(T& guard)
45
894605
    : d_guard(guard) {
46
894605
      Assert(!d_guard);
47
894605
      d_guard = true;
48
894605
    }
49
894605
    ~GuardReentry() {
50
894605
      Assert(d_guard);
51
894605
      d_guard = false;
52
894605
    }
53
  };/* class NodeVisitor<>::GuardReentry */
54
55
public:
56
57
  /**
58
   * Element of the stack.
59
   */
60
24226284
  struct stack_element {
61
    /** The node to be visited */
62
    TNode d_node;
63
    /** The parent of the node */
64
    TNode d_parent;
65
    /** Have the children been queued up for visitation */
66
    bool d_childrenAdded;
67
5034102
    stack_element(TNode node, TNode parent)
68
5034102
        : d_node(node), d_parent(parent), d_childrenAdded(false)
69
    {
70
5034102
    }
71
  };/* struct preprocess_stack_element */
72
73
  /**
74
   * Performs the traversal.
75
   */
76
894605
  static typename Visitor::return_type run(Visitor& visitor, TNode node) {
77
78
1789210
    GuardReentry<bool> guard(s_inRun);
79
80
    // Notify of a start
81
894605
    visitor.start(node);
82
83
    // Do a reverse-topological sort of the subexpressions
84
1789210
    std::vector<stack_element> toVisit;
85
894605
    toVisit.push_back(stack_element(node, node));
86
20409833
    while (!toVisit.empty()) {
87
9757618
      stack_element& stackHead = toVisit.back();
88
      // The current node we are processing
89
19515236
      TNode current = stackHead.d_node;
90
19515236
      TNode parent = stackHead.d_parent;
91
92
9757618
      if (visitor.alreadyVisited(current, parent)) {
93
        // If already visited, we're done
94
310585
        toVisit.pop_back();
95
      }
96
9447033
      else if (stackHead.d_childrenAdded)
97
      {
98
        // Call the visitor
99
4723520
        visitor.visit(current, parent);
100
        // Done with this node, remove from the stack
101
4723512
        toVisit.pop_back();
102
      }
103
      else
104
      {
105
        // Mark that we have added the children
106
4723517
        stackHead.d_childrenAdded = true;
107
        // We need to add the children
108
9786829
        for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
109
10126624
          TNode childNode = *child_it;
110
5063312
          if (!visitor.alreadyVisited(childNode, current)) {
111
4139497
            toVisit.push_back(stack_element(childNode, current));
112
          }
113
        }
114
      }
115
    }
116
117
    // Notify that we're done
118
1789202
    return visitor.done(node);
119
  }
120
121
};/* class NodeVisitor<> */
122
123
template <typename Visitor>
124
thread_local bool NodeVisitor<Visitor>::s_inRun = false;
125
126
}/* CVC4 namespace */