From ba3a69d7915292ddb649bdb8b4830623b337818c Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Wed, 18 Mar 2020 14:30:30 -0700 Subject: [PATCH] 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. --- src/CMakeLists.txt | 1 - src/expr/CMakeLists.txt | 1 + src/{smt_util => expr}/node_visitor.h | 0 src/preprocessing/passes/bv_to_bool.cpp | 2 +- src/printer/ast/ast_printer.cpp | 8 ++++---- src/printer/cvc/cvc_printer.cpp | 4 ++-- src/printer/smt2/smt2_printer.cpp | 2 +- src/proof/proof_manager.cpp | 2 +- src/proof/theory_proof.cpp | 2 +- src/smt/smt_engine.cpp | 2 +- src/theory/theory_engine.cpp | 2 +- 11 files changed, 13 insertions(+), 13 deletions(-) rename src/{smt_util => expr}/node_visitor.h (100%) 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 similarity index 100% rename from src/smt_util/node_visitor.h rename to 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 #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 #include -#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" -- 2.30.2