diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-16 16:46:05 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-16 18:46:05 -0500 |
commit | 7fc04bf78c6c20f3711d14425469eef2e0c2cd60 (patch) | |
tree | d9f2e91a52406edf66967faccad550631cd9e4a5 /src/expr | |
parent | 4e62cdade61514f268b96e78e2f82ad12dfcad07 (diff) |
Move node algorithms to separate file (#2311)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 2 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 7 | ||||
-rw-r--r-- | src/expr/node.cpp | 98 | ||||
-rw-r--r-- | src/expr/node.h | 53 | ||||
-rw-r--r-- | src/expr/node_algorithm.cpp | 170 | ||||
-rw-r--r-- | src/expr/node_algorithm.h | 59 |
6 files changed, 235 insertions, 154 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index bf4ad9acd..f8f9dbd11 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -37,6 +37,8 @@ libexpr_la_SOURCES = \ matcher.h \ node.cpp \ node.h \ + node_algorithm.cpp \ + node_algorithm.h \ node_builder.h \ node_manager.cpp \ node_manager.h \ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 3a0d31b2d..3c867e442 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -21,10 +21,11 @@ #include <vector> #include "base/cvc4_assert.h" -#include "expr/node.h" #include "expr/expr_manager_scope.h" -#include "expr/variable_type_map.h" +#include "expr/node.h" +#include "expr/node_algorithm.h" #include "expr/node_manager_attributes.h" +#include "expr/variable_type_map.h" ${includes} @@ -537,7 +538,7 @@ bool Expr::hasFreeVariable() const { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - return d_node->hasFreeVar(); + return expr::hasFreeVar(*d_node); } void Expr::toStream(std::ostream& out, int depth, bool types, size_t dag, diff --git a/src/expr/node.cpp b/src/expr/node.cpp index fdb1e4d90..b983c81f5 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -73,13 +73,8 @@ UnknownTypeException::UnknownTypeException(TNode n) /** Is this node constant? (and has that been computed yet?) */ struct IsConstTag { }; struct IsConstComputedTag { }; -struct HasBoundVarTag { }; -struct HasBoundVarComputedTag { }; typedef expr::Attribute<IsConstTag, bool> IsConstAttr; typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr; -/** Attribute true for expressions with bound variables in them */ -typedef expr::Attribute<HasBoundVarTag, bool> HasBoundVarAttr; -typedef expr::Attribute<HasBoundVarComputedTag, bool> HasBoundVarComputedAttr; template <bool ref_count> bool NodeTemplate<ref_count>::isConst() const { @@ -114,100 +109,7 @@ bool NodeTemplate<ref_count>::isConst() const { } } -template <bool ref_count> -bool NodeTemplate<ref_count>::hasBoundVar() { - assertTNodeNotExpired(); - if(! getAttribute(HasBoundVarComputedAttr())) { - bool hasBv = false; - if(getKind() == kind::BOUND_VARIABLE) { - hasBv = true; - } else { - for(iterator i = begin(); i != end() && !hasBv; ++i) { - hasBv = (*i).hasBoundVar(); - } - } - if (!hasBv && hasOperator()) { - hasBv = getOperator().hasBoundVar(); - } - setAttribute(HasBoundVarAttr(), hasBv); - setAttribute(HasBoundVarComputedAttr(), true); - Debug("bva") << *this << " has bva : " << getAttribute(HasBoundVarAttr()) << std::endl; - return hasBv; - } - return getAttribute(HasBoundVarAttr()); -} - -template <bool ref_count> -bool NodeTemplate<ref_count>::hasFreeVar() -{ - assertTNodeNotExpired(); - std::unordered_set<TNode, TNodeHashFunction> bound_var; - std::unordered_map<TNode, bool, TNodeHashFunction> visited; - std::vector<TNode> visit; - TNode cur; - visit.push_back(*this); - do - { - cur = visit.back(); - visit.pop_back(); - // can skip if it doesn't have a bound variable - if (!cur.hasBoundVar()) - { - continue; - } - Kind k = cur.getKind(); - bool isQuant = k == kind::FORALL || k == kind::EXISTS || k == kind::LAMBDA - || k == kind::CHOICE; - std::unordered_map<TNode, bool, TNodeHashFunction>::iterator itv = - visited.find(cur); - if (itv == visited.end()) - { - if (k == kind::BOUND_VARIABLE) - { - if (bound_var.find(cur) == bound_var.end()) - { - return true; - } - } - else if (isQuant) - { - for (const TNode& cn : cur[0]) - { - // should not shadow - Assert(bound_var.find(cn) == bound_var.end()); - bound_var.insert(cn); - } - visit.push_back(cur); - } - // must visit quantifiers again to clean up below - visited[cur] = !isQuant; - if (cur.hasOperator()) - { - visit.push_back(cur.getOperator()); - } - for (const TNode& cn : cur) - { - visit.push_back(cn); - } - } - else if (!itv->second) - { - Assert(isQuant); - for (const TNode& cn : cur[0]) - { - bound_var.erase(cn); - } - visited[cur] = true; - } - } while (!visit.empty()); - return false; -} - template bool NodeTemplate<true>::isConst() const; template bool NodeTemplate<false>::isConst() const; -template bool NodeTemplate<true>::hasBoundVar(); -template bool NodeTemplate<false>::hasBoundVar(); -template bool NodeTemplate<true>::hasFreeVar(); -template bool NodeTemplate<false>::hasFreeVar(); }/* CVC4 namespace */ diff --git a/src/expr/node.h b/src/expr/node.h index 92794ffe2..4b12c7ece 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -428,18 +428,6 @@ public: // bool containsDecision(); // is "atomic" // bool properlyContainsDecision(); // maybe not atomic but all children are - /** - * Returns true iff this node contains a bound variable. This bound - * variable may or may not be free. - * @return true iff this node contains a bound variable. - */ - bool hasBoundVar(); - - /** - * Returns true iff this node contains a free variable. - * @return true iff this node contains a free variable. - */ - bool hasFreeVar(); /** * Convert this Node into an Expr using the currently-in-scope @@ -889,11 +877,6 @@ public: */ inline void printAst(std::ostream& out, int indent = 0) const; - /** - * Check if the node has a subterm t. - */ - inline bool hasSubterm(NodeTemplate<false> t, bool strict = false) const; - template <bool ref_count2> NodeTemplate<true> eqNode(const NodeTemplate<ref_count2>& right) const; @@ -1524,42 +1507,6 @@ inline Node NodeTemplate<true>::fromExpr(const Expr& e) { return NodeManager::fromExpr(e); } -template<bool ref_count> -bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) const { - typedef std::unordered_set<TNode, TNodeHashFunction> node_set; - - if (!strict && *this == t) { - return true; - } - - node_set visited; - std::vector<TNode> toProcess; - - toProcess.push_back(*this); - - for (unsigned i = 0; i < toProcess.size(); ++ i) { - TNode current = toProcess[i]; - if (current.hasOperator() && current.getOperator() == t) - { - return true; - } - for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) { - TNode child = current[j]; - if (child == t) { - return true; - } - if (visited.find(child) != visited.end()) { - continue; - } else { - visited.insert(child); - toProcess.push_back(child); - } - } - } - - return false; -} - #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp new file mode 100644 index 000000000..5443a3a2a --- /dev/null +++ b/src/expr/node_algorithm.cpp @@ -0,0 +1,170 @@ +/********************* */ +/*! \file node_algorithm.cpp + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Common algorithms on nodes + ** + ** This file implements common algorithms applied to nodes, such as checking if + ** a node contains a free or a bound variable. + **/ + +#include "expr/node_algorithm.h" + +#include "expr/attribute.h" + +namespace CVC4 { +namespace expr { + +bool hasSubterm(TNode n, TNode t, bool strict) +{ + if (!strict && n == t) + { + return true; + } + + std::unordered_set<TNode, TNodeHashFunction> visited; + std::vector<TNode> toProcess; + + toProcess.push_back(n); + + for (unsigned i = 0; i < toProcess.size(); ++i) + { + TNode current = toProcess[i]; + if (current.hasOperator() && current.getOperator() == t) + { + return true; + } + for (unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++j) + { + TNode child = current[j]; + if (child == t) + { + return true; + } + if (visited.find(child) != visited.end()) + { + continue; + } + else + { + visited.insert(child); + toProcess.push_back(child); + } + } + } + + return false; +} + +struct HasBoundVarTag +{ +}; +struct HasBoundVarComputedTag +{ +}; +/** Attribute true for expressions with bound variables in them */ +typedef expr::Attribute<HasBoundVarTag, bool> HasBoundVarAttr; +typedef expr::Attribute<HasBoundVarComputedTag, bool> HasBoundVarComputedAttr; + +bool hasBoundVar(TNode n) +{ + if (!n.getAttribute(HasBoundVarComputedAttr())) + { + bool hasBv = false; + if (n.getKind() == kind::BOUND_VARIABLE) + { + hasBv = true; + } + else + { + for (auto i = n.begin(); i != n.end() && !hasBv; ++i) + { + hasBv = hasBoundVar(*i); + } + } + if (!hasBv && n.hasOperator()) + { + hasBv = hasBoundVar(n.getOperator()); + } + n.setAttribute(HasBoundVarAttr(), hasBv); + n.setAttribute(HasBoundVarComputedAttr(), true); + Debug("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttr()) + << std::endl; + return hasBv; + } + return n.getAttribute(HasBoundVarAttr()); +} + +bool hasFreeVar(TNode n) +{ + std::unordered_set<TNode, TNodeHashFunction> bound_var; + std::unordered_map<TNode, bool, TNodeHashFunction> visited; + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + // can skip if it doesn't have a bound variable + if (!hasBoundVar(cur)) + { + continue; + } + Kind k = cur.getKind(); + bool isQuant = k == kind::FORALL || k == kind::EXISTS || k == kind::LAMBDA + || k == kind::CHOICE; + std::unordered_map<TNode, bool, TNodeHashFunction>::iterator itv = + visited.find(cur); + if (itv == visited.end()) + { + if (k == kind::BOUND_VARIABLE) + { + if (bound_var.find(cur) == bound_var.end()) + { + return true; + } + } + else if (isQuant) + { + for (const TNode& cn : cur[0]) + { + // should not shadow + Assert(bound_var.find(cn) == bound_var.end()); + bound_var.insert(cn); + } + visit.push_back(cur); + } + // must visit quantifiers again to clean up below + visited[cur] = !isQuant; + if (cur.hasOperator()) + { + visit.push_back(cur.getOperator()); + } + for (const TNode& cn : cur) + { + visit.push_back(cn); + } + } + else if (!itv->second) + { + Assert(isQuant); + for (const TNode& cn : cur[0]) + { + bound_var.erase(cn); + } + visited[cur] = true; + } + } while (!visit.empty()); + return false; +} + +} // namespace expr +} // namespace CVC4 diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h new file mode 100644 index 000000000..61e81c4c2 --- /dev/null +++ b/src/expr/node_algorithm.h @@ -0,0 +1,59 @@ +/********************* */ +/*! \file node_algorithm.h + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Common algorithms on nodes + ** + ** This file implements common algorithms applied to nodes, such as checking if + ** a node contains a free or a bound variable. This file should generally only + ** be included in source files. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__EXPR__NODE_ALGORITHM_H +#define __CVC4__EXPR__NODE_ALGORITHM_H + +#include <unordered_map> +#include <vector> + +#include "expr/node.h" + +namespace CVC4 { +namespace expr { + +/** + * Check if the node n has a subterm t. + * @param n The node to search in + * @param t The subterm to search for + * @param strict If true, a term is not considered to be a subterm of itself + * @return true iff t is a subterm in n + */ +bool hasSubterm(TNode n, TNode t, bool strict = false); + +/** + * Returns true iff the node n contains a bound variable. This bound + * variable may or may not be free. + * @param n The node under investigation + * @return true iff this node contains a bound variable + */ +bool hasBoundVar(TNode n); + +/** + * Returns true iff the node n contains a free variable. + * @param n The node under investigation + * @return true iff this node contains a free variable. + */ +bool hasFreeVar(TNode n); + +} // namespace expr +} // namespace CVC4 + +#endif |