Move node algorithms to separate file (#2311)

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