Move node visitor class from smt_util/ to expr/ (#4110)

Done by:

Running rg 'smt_util/node_visitor' -l | xargs sed -i 's/smt_util\/node_visitor/expr\/node_visitor/' in src to change the #includes
Moving the file
Changing src/expr/CMakeLists.txt and src/CMakeLists.txt
clang-format, omitting node_visitor.h.
In reference to discussion, here.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index bb2b9596035be8d3beb96ffb3214927a53fc44a8..dfdfb0a473fa92c43363aa73c8de377646d71718 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -249,7 +249,6 @@ libcvc4_add_sources(
   smt_util/boolean_simplification.h
   smt_util/nary_builder.cpp
   smt_util/nary_builder.h
-  smt_util/node_visitor.h
   theory/arith/approx_simplex.cpp
   theory/arith/approx_simplex.h
   theory/arith/arith_ite_utils.cpp

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 8357102b0f4bae540bccb966268eccabf10de19e..d1faa8ffb74bb5d4ae276de82a41acfafa8dba1a 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -31,6 +31,7 @@ libcvc4_add_sources(
   node_trie.h
   node_value.cpp
   node_value.h
+  node_visitor.h
   symbol_table.cpp
   symbol_table.h
   term_canonize.cpp

diff --git a/src/expr/node_visitor.h b/src/expr/node_visitor.h
new file mode 100644 (file)
index 0000000..47ed6ef
--- /dev/null
+++ b/src/expr/node_visitor.h
@@ -0,0 +1,126 @@
+/*********************                                                        */
+/*! \file node_visitor.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Dejan Jovanovic, Morgan Deters, Liana Hadarean
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief A simple visitor for nodes
+ **
+ ** A simple visitor for nodes.
+ **/
+
+#pragma once
+
+#include "cvc4_private.h"
+
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+
+/**
+ * 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;
+
+}/* CVC4 namespace */

diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index de9504503d3940e60ca047f331d387ca52cdebb8..5b10f66449b71ba4a1041c3fd8dd041ebbaf02a1 100644 (file)
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -22,8 +22,8 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "expr/node_visitor.h"
 #include "smt/smt_statistics_registry.h"
-#include "smt_util/node_visitor.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index c59d8f32845cf4c1c11fdd3d13324e09cfc8399b..2e32e9c121e0190e0b9eb1530e481453831b387c 100644 (file)
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -20,12 +20,12 @@
 #include <typeinfo>
 #include <vector>
 
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "expr/node_manager_attributes.h" // for VarNameAttr
-#include "options/language.h" // for LANG_AST
+#include "expr/expr.h"                     // for ExprSetDepth etc..
+#include "expr/node_manager_attributes.h"  // for VarNameAttr
+#include "expr/node_visitor.h"
+#include "options/language.h"  // for LANG_AST
 #include "printer/dagification_visitor.h"
 #include "smt/command.h"
-#include "smt_util/node_visitor.h"
 #include "theory/substitutions.h"
 
 using namespace std;

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 79a8904cdf65f0e3ef7ca518f0cf087b8917b66c..cad3c464007731535778d34df9f37835382a7120 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -27,12 +27,12 @@
 #include "expr/dtype.h"
 #include "expr/expr.h"                     // for ExprSetDepth etc..
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
-#include "options/language.h"              // for LANG_AST
+#include "expr/node_visitor.h"
+#include "options/language.h"  // for LANG_AST
 #include "options/smt_options.h"
 #include "printer/dagification_visitor.h"
 #include "smt/command.h"
 #include "smt/smt_engine.h"
-#include "smt_util/node_visitor.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory_model.h"

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index ed4d3f5dc0f3a2e1e22bffceff634f70d6a9047e..541827f8999253e899ae6ca32f54753a54761890 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -23,6 +23,7 @@
 
 #include "expr/dtype.h"
 #include "expr/node_manager_attributes.h"
+#include "expr/node_visitor.h"
 #include "options/bv_options.h"
 #include "options/language.h"
 #include "options/printer_options.h"
@@ -30,7 +31,6 @@
 #include "printer/dagification_visitor.h"
 #include "smt/smt_engine.h"
 #include "smt_util/boolean_simplification.h"
-#include "smt_util/node_visitor.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/substitutions.h"

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 33f284bf8928efadd59dd9b207495f0eb19ff14c..14556708bb12f2b1b86a5304971e29edeb11ab71 100644 (file)
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -19,6 +19,7 @@
 
 #include "base/check.h"
 #include "context/context.h"
+#include "expr/node_visitor.h"
 #include "options/bv_options.h"
 #include "options/proof_options.h"
 #include "proof/clause_id.h"
@@ -31,7 +32,6 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
-#include "smt_util/node_visitor.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/output_channel.h"
 #include "theory/term_registration_visitor.h"

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index e746a6315c38283136e94d3fac6510416720377c..f4a762cb0e1a67452a266cffadc89d92c3ceeaaa 100644 (file)
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -18,6 +18,7 @@
 
 #include "base/check.h"
 #include "context/context.h"
+#include "expr/node_visitor.h"
 #include "options/bv_options.h"
 #include "options/proof_options.h"
 #include "proof/arith_proof.h"
@@ -35,7 +36,6 @@
 #include "prop/sat_solver_types.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
-#include "smt_util/node_visitor.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/output_channel.h"

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3f8160ce9695b3078701fe487dd4db0703150e30..4b232669656e280bbdc45dffc7e5aacc4dc09a87 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -49,6 +49,7 @@
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
 #include "expr/node_self_iterator.h"
+#include "expr/node_visitor.h"
 #include "options/arith_options.h"
 #include "options/arrays_options.h"
 #include "options/base_options.h"
@@ -90,7 +91,6 @@
 #include "smt/update_ostream.h"
 #include "smt_util/boolean_simplification.h"
 #include "smt_util/nary_builder.h"
-#include "smt_util/node_visitor.h"
 #include "theory/booleans/circuit_propagator.h"
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/logic_info.h"

diff --git a/src/smt_util/node_visitor.h b/src/smt_util/node_visitor.h
deleted file mode 100644 (file)
index 47ed6ef..0000000
--- a/src/smt_util/node_visitor.h
+++ /dev/null
@@ -1,126 +0,0 @@
-/*********************                                                        */
-/*! \file node_visitor.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Dejan Jovanovic, Morgan Deters, Liana Hadarean
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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.\endverbatim
- **
- ** \brief A simple visitor for nodes
- **
- ** A simple visitor for nodes.
- **/
-
-#pragma once
-
-#include "cvc4_private.h"
-
-#include <vector>
-
-#include "expr/node.h"
-
-namespace CVC4 {
-
-/**
- * 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;
-
-}/* CVC4 namespace */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 60ad00fc5b0f8653219a85db3a342e50f1b5010b..32a80a418b6b343cae7aaff2320f0aa40c51dc61 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -25,6 +25,7 @@
 #include "expr/node.h"
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
+#include "expr/node_visitor.h"
 #include "options/bv_options.h"
 #include "options/options.h"
 #include "options/proof_options.h"
@@ -37,7 +38,6 @@
 #include "proof/theory_proof.h"
 #include "smt/logic_exception.h"
 #include "smt/term_formula_removal.h"
-#include "smt_util/node_visitor.h"
 #include "theory/arith/arith_ite_utils.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/care_graph.h"