Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/node_visitor.h	Lines:	33	33	100.0 %
Date:	2021-05-22	Branches:	89	178	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Dejan Jovanovic, Andrew Reynolds, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * A simple visitor for nodes.
 */

#pragma once

#include <vector>

#include "cvc5_private.h"
#include "expr/node.h"

namespace cvc5 {

/**
 * Traverses the nodes reverse-topologically (children before parents),
 * calling the visitor in order.
 */
template<typename Visitor>
class NodeVisitor {

  /** For re-entry checking */
  static thread_local bool s_inRun;

  /**
   * Guard against NodeVisitor<> being re-entrant.
   */
  template <class T>
  class GuardReentry {
    T& d_guard;
  public:
    GuardReentry(T& guard)
    : d_guard(guard) {
      Assert(!d_guard);
      d_guard = true;
    }
    ~GuardReentry() {
      Assert(d_guard);
      d_guard = false;
    }
  };/* class NodeVisitor<>::GuardReentry */

public:

  /**
   * Element of the stack.
   */
  struct stack_element {
    /** The node to be visited */
    TNode d_node;
    /** The parent of the node */
    TNode d_parent;
    /** Have the children been queued up for visitation */
    bool d_childrenAdded;
    stack_element(TNode node, TNode parent)
        : d_node(node), d_parent(parent), d_childrenAdded(false)
    {
    }
  };/* struct preprocess_stack_element */

  /**
   * Performs the traversal.
   */
  static typename Visitor::return_type run(Visitor& visitor, TNode node) {

    GuardReentry<bool> guard(s_inRun);

    // Notify of a start
    visitor.start(node);

    // Do a reverse-topological sort of the subexpressions
    std::vector<stack_element> toVisit;
    toVisit.push_back(stack_element(node, node));
    while (!toVisit.empty()) {
      stack_element& stackHead = toVisit.back();
      // The current node we are processing
      TNode current = stackHead.d_node;
      TNode parent = stackHead.d_parent;

      if (visitor.alreadyVisited(current, parent)) {
        // If already visited, we're done
        toVisit.pop_back();
      }
      else if (stackHead.d_childrenAdded)
      {
        // Call the visitor
        visitor.visit(current, parent);
        // Done with this node, remove from the stack
        toVisit.pop_back();
      }
      else
      {
        // Mark that we have added the children
        stackHead.d_childrenAdded = true;
        // We need to add the children
        for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
          TNode childNode = *child_it;
          if (!visitor.alreadyVisited(childNode, current)) {
            toVisit.push_back(stack_element(childNode, current));
          }
        }
      }
    }

    // Notify that we're done
    return visitor.done(node);
  }

};/* class NodeVisitor<> */

template <typename Visitor>
thread_local bool NodeVisitor<Visitor>::s_inRun = false;

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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