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.

11 files changed, 13 insertions, 13 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index bb2b95960..dfdfb0a47 100644
--- 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 8357102b0..d1faa8ffb 100644
--- 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/smt_util/node_visitor.h b/src/expr/node_visitor.h
index 47ed6eff8..47ed6eff8 100644
--- a/src/smt_util/node_visitor.h
+++ b/src/expr/node_visitor.h
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index de9504503..5b10f6644 100644
--- 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 c59d8f328..2e32e9c12 100644
--- 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 79a8904cd..cad3c4640 100644
--- 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 ed4d3f5dc..541827f89 100644
--- 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 33f284bf8..14556708b 100644
--- 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 e746a6315..f4a762cb0 100644
--- 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 3f8160ce9..4b2326696 100644
--- 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/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 60ad00fc5..32a80a418 100644
--- 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"