From: Alex Ozdemir Date: Wed, 18 Mar 2020 21:30:30 +0000 (-0700) Subject: Move node visitor class from smt_util/ to expr/ (#4110) X-Git-Tag: cvc5-1.0.0~3480 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ba3a69d7915292ddb649bdb8b4830623b337818c;p=cvc5.git 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 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/expr/node_visitor.h b/src/expr/node_visitor.h new file mode 100644 index 000000000..47ed6eff8 --- /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 + +#include "expr/node.h" + +namespace CVC4 { + +/** + * Traverses the nodes reverse-topologically (children before parents), + * calling the visitor in order. + */ +template +class NodeVisitor { + + /** For re-entry checking */ + static thread_local bool s_inRun; + + /** + * Guard against NodeVisitor<> being re-entrant. + */ + template + 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 guard(s_inRun); + + // Notify of a start + visitor.start(node); + + // Do a reverse-topological sort of the subexpressions + std::vector 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 +thread_local bool NodeVisitor::s_inRun = false; + +}/* CVC4 namespace */ 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/smt_util/node_visitor.h b/src/smt_util/node_visitor.h deleted file mode 100644 index 47ed6eff8..000000000 --- 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 - -#include "expr/node.h" - -namespace CVC4 { - -/** - * Traverses the nodes reverse-topologically (children before parents), - * calling the visitor in order. - */ -template -class NodeVisitor { - - /** For re-entry checking */ - static thread_local bool s_inRun; - - /** - * Guard against NodeVisitor<> being re-entrant. - */ - template - 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 guard(s_inRun); - - // Notify of a start - visitor.start(node); - - // Do a reverse-topological sort of the subexpressions - std::vector 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 -thread_local bool NodeVisitor::s_inRun = false; - -}/* CVC4 namespace */ 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"