Move node algorithms to separate file (#2311)

32 files changed, 523 insertions, 316 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
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index ade34d127..2e18899a2 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -17,6 +17,7 @@
 
 #include <vector>
 
+#include "expr/node_algorithm.h"
 #include "options/proof_options.h"
 #include "proof/proof_manager.h"
 
@@ -85,7 +86,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
   Node newAssertion;
   if(node.getKind() == kind::ITE) {
     // If an ITE, replace it
-    if (!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar()))
+    if (!nodeType.isBoolean() && (!inQuant || !expr::hasBoundVar(node)))
     {
       skolem = getSkolemForNode(node);
       if (skolem.isNull())
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index ed68df89c..4bfc1a4f9 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -19,6 +19,7 @@
 
 #include "base/output.h"
 #include "expr/expr.h"
+#include "expr/node_algorithm.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_static_learner.h"
@@ -107,9 +108,11 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
 
   switch(n.getKind()){
   case ITE:
-    if(n.hasBoundVar()) {
+    if (expr::hasBoundVar(n))
+    {
       // Unsafe with non-ground ITEs; do nothing
-      Debug("arith::static") << "(potentially) non-ground ITE, ignoring..." << endl;
+      Debug("arith::static")
+          << "(potentially) non-ground ITE, ignoring..." << endl;
       break;
     }
 
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 30debf6d7..f4e9f9d6b 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -20,6 +20,7 @@
 #include <cmath>
 #include <set>
 
+#include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
@@ -1199,7 +1200,7 @@ bool NonlinearExtension::solveEqualitySimple(Node eq)
         {
           Assert(!slv.isNull());
           // currently do not support substitution-with-coefficients
-          if (veqc.isNull() && !slv.hasSubterm(uv))
+          if (veqc.isNull() && !expr::hasSubterm(slv, uv))
           {
             Trace("nl-ext-cm")
                 << "check-model-subs : " << uv << " -> " << slv << std::endl;
@@ -1454,7 +1455,7 @@ bool NonlinearExtension::simpleCheckModelLit(Node lit)
     // is it a valid variable?
     std::map<Node, std::pair<Node, Node> >::iterator bit =
         d_check_model_bounds.find(v);
-    if (!invalid_vsum.hasSubterm(v) && bit != d_check_model_bounds.end())
+    if (!expr::hasSubterm(invalid_vsum, v) && bit != d_check_model_bounds.end())
     {
       std::map<Node, Node>::iterator it = v_a.find(v);
       if (it != v_a.end())
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 6db246b8b..968970049 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -32,6 +32,7 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node.h"
+#include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
 #include "options/arith_options.h"
 #include "options/smt_options.h"  // for incrementalSolving()
@@ -1354,24 +1355,37 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o
       // Add the substitution if not recursive
       Assert(elim == Rewriter::rewrite(elim));
 
-
-      if(right.size() > options::ppAssertMaxSubSize()){
-        Debug("simplify") << "TheoryArithPrivate::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl;
+      if (right.size() > options::ppAssertMaxSubSize())
+      {
+        Debug("simplify")
+            << "TheoryArithPrivate::solve(): did not substitute due to the "
+               "right hand side containing too many terms: "
+            << minVar << ":" << elim << endl;
         Debug("simplify") << right.size() << endl;
-      }else if(elim.hasSubterm(minVar)){
-        Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl;
-
-      }else if (!minVar.getType().isInteger() || right.isIntegral()) {
-        Assert(!elim.hasSubterm(minVar));
+      }
+      else if (expr::hasSubterm(elim, minVar))
+      {
+        Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute "
+                             "due to recursive pattern with sharing: "
+                          << minVar << ":" << elim << endl;
+      }
+      else if (!minVar.getType().isInteger() || right.isIntegral())
+      {
+        Assert(!expr::hasSubterm(elim, minVar));
         // cannot eliminate integers here unless we know the resulting
         // substitution is integral
-        Debug("simplify") << "TheoryArithPrivate::solve(): substitution " << minVar << " |-> " << elim << endl;
+        Debug("simplify") << "TheoryArithPrivate::solve(): substitution "
+                          << minVar << " |-> " << elim << endl;
 
         outSubstitutions.addSubstitution(minVar, elim);
         return Theory::PP_ASSERT_STATUS_SOLVED;
-      } else {
-        Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
-
+      }
+      else
+      {
+        Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute "
+                             "b/c it's integer: "
+                          << minVar << ":" << minVar.getType() << " |-> "
+                          << elim << ":" << elim.getType() << endl;
       }
     }
   }
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9af564a05..4407d45d8 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -20,6 +20,7 @@
 #include <memory>
 
 #include "expr/kind.h"
+#include "expr/node_algorithm.h"
 #include "options/arrays_options.h"
 #include "options/smt_options.h"
 #include "proof/array_proof.h"
@@ -342,11 +343,15 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs
     {
       d_ppFacts.push_back(in);
       d_ppEqualityEngine.assertEquality(in, true, in);
-      if (in[0].isVar() && !in[1].hasSubterm(in[0]) && (in[1].getType()).isSubtypeOf(in[0].getType()) ){
+      if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
+          && (in[1].getType()).isSubtypeOf(in[0].getType()))
+      {
         outSubstitutions.addSubstitution(in[0], in[1]);
         return PP_ASSERT_STATUS_SOLVED;
       }
-      if (in[1].isVar() && !in[0].hasSubterm(in[1]) && (in[0].getType()).isSubtypeOf(in[1].getType())){
+      if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])
+          && (in[0].getType()).isSubtypeOf(in[1].getType()))
+      {
         outSubstitutions.addSubstitution(in[1], in[0]);
         return PP_ASSERT_STATUS_SOLVED;
       }
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index aa87b65ba..d04b71ee1 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -15,12 +15,14 @@
  **/
 
 #include "theory/booleans/circuit_propagator.h"
-#include "util/utility.h"
 
 #include <stack>
 #include <vector>
 #include <algorithm>
 
+#include "expr/node_algorithm.h"
+#include "util/utility.h"
+
 using namespace std;
 
 namespace CVC4 {
@@ -208,7 +210,7 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) {
   for(; parent_it != parent_it_end && !d_conflict; ++ parent_it) {
     // The current parent of the child
     TNode parent = *parent_it;
-    Assert(parent.hasSubterm(child));
+    Assert(expr::hasSubterm(parent, child));
 
     // Forward rules
     switch(parent.getKind()) {
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index da28b1ffd..4c14ec177 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -19,6 +19,7 @@
 #include "theory/builtin/theory_builtin_rewriter.h"
 
 #include "expr/chain.h"
+#include "expr/node_algorithm.h"
 
 using namespace std;
 
@@ -88,7 +89,7 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) {
         Trace("builtin-rewrite") << "  array rep : " << anode << ", constant = " << anode.isConst() << std::endl;
         Assert( anode.isConst()==retNode.isConst() );
         Assert( retNode.getType()==node.getType() );
-        Assert(node.hasFreeVar() == retNode.hasFreeVar());
+        Assert(expr::hasFreeVar(node) == expr::hasFreeVar(retNode));
         return RewriteResponse(REWRITE_DONE, retNode);
       } 
     }else{
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 8ea474ad7..0150264fd 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -15,6 +15,9 @@
  **/
 #include "theory/bv/bv_subtheory_algebraic.h"
 
+#include <unordered_set>
+
+#include "expr/node_algorithm.h"
 #include "options/bv_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
@@ -23,8 +26,6 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
 
-#include <unordered_set>
-
 using namespace CVC4::context;
 using namespace CVC4::prop;
 using namespace CVC4::theory::bv::utils;
@@ -490,11 +491,13 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
   TNode left = fact[0];
   TNode right = fact[1];
 
-  if (left.isVar() && !right.hasSubterm(left)) {
-    bool changed  = subst.addSubstitution(left, right, reason);
+  if (left.isVar() && !expr::hasSubterm(right, left))
+  {
+    bool changed = subst.addSubstitution(left, right, reason);
     return changed;
   }
-  if (right.isVar() && !left.hasSubterm(right)) {
+  if (right.isVar() && !expr::hasSubterm(left, right))
+  {
     bool changed = subst.addSubstitution(right, left, reason);
     return changed;
   }
@@ -507,7 +510,8 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
       return false;
 
     // simplify xor with same variable on both sides
-    if (right.hasSubterm(var)) {
+    if (expr::hasSubterm(right, var))
+    {
       std::vector<Node> right_children;
       for (unsigned i = 0; i < right.getNumChildren(); ++i) {
         if (right[i] != var)
@@ -548,9 +552,10 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
   }
 
   // (a xor t = a) <=> (t = 0)
-  if (left.getKind() == kind::BITVECTOR_XOR &&
-      right.getMetaKind() == kind::metakind::VARIABLE &&
-      left.hasSubterm(right)) {
+  if (left.getKind() == kind::BITVECTOR_XOR
+      && right.getMetaKind() == kind::metakind::VARIABLE
+      && expr::hasSubterm(left, right))
+  {
     TNode var = right;
     Node new_left = nm->mkNode(kind::BITVECTOR_XOR, var, left);
     Node zero = utils::mkConst(utils::getSize(var), 0u);
@@ -559,9 +564,10 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
     return changed;
   }
 
-  if (right.getKind() == kind::BITVECTOR_XOR &&
-      left.getMetaKind() == kind::metakind::VARIABLE &&
-      right.hasSubterm(left)) {
+  if (right.getKind() == kind::BITVECTOR_XOR
+      && left.getMetaKind() == kind::metakind::VARIABLE
+      && expr::hasSubterm(right, left))
+  {
     TNode var = left;
     Node new_right = nm->mkNode(kind::BITVECTOR_XOR, var, right);
     Node zero = utils::mkConst(utils::getSize(var), 0u);
@@ -584,9 +590,10 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
   return false;
 }
 
-bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in) {
-  if (node.getMetaKind() == kind::metakind::VARIABLE &&
-      !in.hasSubterm(node))
+bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in)
+{
+  if (node.getMetaKind() == kind::metakind::VARIABLE
+      && !expr::hasSubterm(in, node))
     return true;
   return false;
 }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 9ecbbc99c..541b77fe6 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/bv/theory_bv.h"
 
+#include "expr/node_algorithm.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
@@ -670,13 +671,13 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
   {
     case kind::EQUAL:
     {
-      if (in[0].isVar() && !in[1].hasSubterm(in[0]))
+      if (in[0].isVar() && !expr::hasSubterm(in[1], in[0]))
       {
         ++(d_statistics.d_solveSubstitutions);
         outSubstitutions.addSubstitution(in[0], in[1]);
         return PP_ASSERT_STATUS_SOLVED;
       }
-      if (in[1].isVar() && !in[0].hasSubterm(in[1]))
+      if (in[1].isVar() && !expr::hasSubterm(in[0], in[1]))
       {
         ++(d_statistics.d_solveSubstitutions);
         outSubstitutions.addSubstitution(in[1], in[0]);
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index a02bf305f..1293f8311 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -22,9 +22,10 @@
 #include <unordered_map>
 #include <unordered_set>
 
-#include "theory/rewriter.h"
+#include "expr/node_algorithm.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
@@ -601,11 +602,13 @@ inline Node RewriteRule<ConcatToMult>::apply(TNode node)
   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, factor, coef);
 }
 
-template<> inline
-bool RewriteRule<SolveEq>::applies(TNode node) {
-  if (node.getKind() != kind::EQUAL ||
-      (node[0].isVar() && !node[1].hasSubterm(node[0])) ||
-      (node[1].isVar() && !node[0].hasSubterm(node[1]))) {
+template <>
+inline bool RewriteRule<SolveEq>::applies(TNode node)
+{
+  if (node.getKind() != kind::EQUAL
+      || (node[0].isVar() && !expr::hasSubterm(node[1], node[0]))
+      || (node[1].isVar() && !expr::hasSubterm(node[0], node[1])))
+  {
     return false;
   }
   return true;
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index f1235d185..4ea006d54 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/cegqi/ceg_arith_instantiator.h"
 
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/partial_model.h"
@@ -851,7 +852,7 @@ int ArithInstantiator::solve_arith(CegInstantiator* ci,
         << pv << " " << atom.getKind() << " " << val << std::endl;
   }
   // when not pure LIA/LRA, we must check whether the lhs contains pv
-  if (val.hasSubterm(pv))
+  if (expr::hasSubterm(val, pv))
   {
     Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl;
     return 0;
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
index 3a0db0273..e56d5f5db 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
 
+#include "expr/node_algorithm.h"
+
 using namespace std;
 using namespace CVC4::kind;
 using namespace CVC4::context;
@@ -170,7 +172,7 @@ Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb)
   if (!ret.isNull())
   {
     // ensure does not contain v
-    if (ret.hasSubterm(v))
+    if (expr::hasSubterm(ret, v))
     {
       ret = Node::null();
     }
diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
index 9f12f8b23..3535b57b7 100644
--- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/cegqi/ceg_epr_instantiator.h"
 
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/term_database.h"
@@ -145,7 +146,7 @@ void EprInstantiator::computeMatchScore(CegInstantiator* ci,
                                         Node eqc,
                                         std::map<Node, int>& match_score)
 {
-  if (!inst::Trigger::isAtomicTrigger(catom) || !catom.hasSubterm(pv))
+  if (!inst::Trigger::isAtomicTrigger(catom) || !expr::hasSubterm(catom, pv))
   {
     return;
   }
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 1abd1d4e1..2a17f1e36 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
 #include "theory/quantifiers/cegqi/ceg_epr_instantiator.h"
 
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "smt/term_formula_removal.h"
 #include "theory/arith/arith_msum.h"
@@ -1214,7 +1215,7 @@ void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq
     {
       Node nn = n[i == 0 ? 1 : 0];
       std::map<Node, std::vector<Node> >::iterator it = teq.find(n[i]);
-      if (it != teq.end() && !nn.hasFreeVar()
+      if (it != teq.end() && !expr::hasFreeVar(nn)
           && std::find(it->second.begin(), it->second.end(), nn)
                  == it->second.end())
       {
@@ -1268,7 +1269,7 @@ void CegInstantiator::presolve( Node q ) {
       Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
       lem = NodeManager::currentNM()->mkNode( OR, g, lem );
       Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
-      Assert(!lem.hasFreeVar());
+      Assert(!expr::hasFreeVar(lem));
       d_qe->getOutputChannel().lemma( lem, false, true );
     }
   }
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index 615968704..c281e81ca 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -13,6 +13,7 @@
  **/
 #include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
 
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "smt/term_formula_removal.h"
 #include "theory/arith/partial_model.h"
@@ -662,7 +663,7 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
         }
       }
       //only legal if current quantified formula contains n
-      return d_curr_quant.hasSubterm(n);
+      return expr::hasSubterm(d_curr_quant, n);
     }
   }else{
     return true;
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 1fce68de0..3615ef6f4 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/ematching/trigger.h"
 
+#include "expr/node_algorithm.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"
 #include "theory/quantifiers/ematching/ho_trigger.h"
@@ -305,10 +306,12 @@ bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
     }
   }else if( isUsableAtomicTrigger( n1, q ) ){
     if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
-        && !n1.hasSubterm(n2))
+        && !expr::hasSubterm(n1, n2))
     {
       return true;
-    }else if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){
+    }
+    else if (!quantifiers::TermUtil::hasInstConstAttr(n2))
+    {
       return true;
     }
   }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index fd98aa208..f0789a503 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/quantifiers/fmf/bounded_integers.h"
 
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -436,17 +437,23 @@ void BoundedIntegers::checkOwnership(Node f)
                                << bound_lit_map[2][v] << std::endl;
           }
         }else if( it->second==BOUND_FIXED_SET ){
-          setBoundedVar( f, v, BOUND_FIXED_SET );
+          setBoundedVar(f, v, BOUND_FIXED_SET);
           setBoundVar = true;
-          for( unsigned i=0; i<bound_fixed_set[v].size(); i++ ){
+          for (unsigned i = 0; i < bound_fixed_set[v].size(); i++)
+          {
             Node t = bound_fixed_set[v][i];
-            if( t.hasBoundVar() ){
-              d_fixed_set_ngr_range[f][v].push_back( t ); 
-            }else{
-              d_fixed_set_gr_range[f][v].push_back( t ); 
+            if (expr::hasBoundVar(t))
+            {
+              d_fixed_set_ngr_range[f][v].push_back(t);
             }
-          } 
-          Trace("bound-int") << "Variable " << v << " is bound because of disequality conjunction " << bound_lit_map[3][v] << std::endl;
+            else
+            {
+              d_fixed_set_gr_range[f][v].push_back(t);
+            }
+          }
+          Trace("bound-int") << "Variable " << v
+                             << " is bound because of disequality conjunction "
+                             << bound_lit_map[3][v] << std::endl;
         }
         if( setBoundVar ){
           success = true;
@@ -543,9 +550,11 @@ void BoundedIntegers::checkOwnership(Node f)
         Node r = itr->second;
         Assert( !r.isNull() );
         bool isProxy = false;
-        if( r.hasBoundVar() ){
-          //introduce a new bound
-          Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" );
+        if (expr::hasBoundVar(r))
+        {
+          // introduce a new bound
+          Node new_range = NodeManager::currentNM()->mkSkolem(
+              "bir", r.getType(), "bound for term");
           d_nground_range[f][v] = r;
           d_range[f][v] = new_range;
           r = new_range;
@@ -645,13 +654,21 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
   return;
 }
 
-bool BoundedIntegers::isGroundRange( Node q, Node v ) {
-  if( isBoundVar(q,v) ){
-    if( d_bound_type[q][v]==BOUND_INT_RANGE ){
-      return !getLowerBound(q,v).hasBoundVar() && !getUpperBound(q,v).hasBoundVar();
-    }else if( d_bound_type[q][v]==BOUND_SET_MEMBER ){
-      return !d_setm_range[q][v].hasBoundVar();
-    }else if( d_bound_type[q][v]==BOUND_FIXED_SET ){
+bool BoundedIntegers::isGroundRange(Node q, Node v)
+{
+  if (isBoundVar(q, v))
+  {
+    if (d_bound_type[q][v] == BOUND_INT_RANGE)
+    {
+      return !expr::hasBoundVar(getLowerBound(q, v))
+             && !expr::hasBoundVar(getUpperBound(q, v));
+    }
+    else if (d_bound_type[q][v] == BOUND_SET_MEMBER)
+    {
+      return !expr::hasBoundVar(d_setm_range[q][v]);
+    }
+    else if (d_bound_type[q][v] == BOUND_FIXED_SET)
+    {
       return !d_fixed_set_ngr_range[q][v].empty();
     }
   }
@@ -684,7 +701,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
     return sr;
   }
   Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
-  Assert(!sr.hasFreeVar());
+  Assert(!expr::hasFreeVar(sr));
   Node sro = sr;
   sr = d_quantEngine->getModel()->getValue(sr);
   // if non-constant, then sr does not occur in the model, we fail
@@ -915,4 +932,3 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
     return true;
   }
 }
-
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 3b2a650ab..3006a07bf 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -17,14 +17,15 @@
 
 #include <vector>
 
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
@@ -179,23 +180,34 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
     registerNode( n[1], hasPol, pol, true );
   }else{
     if( !MatchGen::isHandledBoolConnective( n ) ){
-      if( n.hasBoundVar() ){
-        //literals
-        if( n.getKind()==EQUAL ){
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            flatten( n[i], beneathQuant );
+      if (expr::hasBoundVar(n))
+      {
+        // literals
+        if (n.getKind() == EQUAL)
+        {
+          for (unsigned i = 0; i < n.getNumChildren(); i++)
+          {
+            flatten(n[i], beneathQuant);
           }
-        }else if( MatchGen::isHandledUfTerm( n ) ){
-          flatten( n, beneathQuant );
-        }else if( n.getKind()==ITE ){
-          for( unsigned i=1; i<=2; i++ ){
-            flatten( n[i], beneathQuant );
+        }
+        else if (MatchGen::isHandledUfTerm(n))
+        {
+          flatten(n, beneathQuant);
+        }
+        else if (n.getKind() == ITE)
+        {
+          for (unsigned i = 1; i <= 2; i++)
+          {
+            flatten(n[i], beneathQuant);
           }
-          registerNode( n[0], false, pol, beneathQuant );
-        }else if( options::qcfTConstraint() ){
-          //a theory-specific predicate
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            flatten( n[i], beneathQuant );
+          registerNode(n[0], false, pol, beneathQuant);
+        }
+        else if (options::qcfTConstraint())
+        {
+          // a theory-specific predicate
+          for (unsigned i = 0; i < n.getNumChildren(); i++)
+          {
+            flatten(n[i], beneathQuant);
           }
         }
       }
@@ -215,7 +227,8 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
 
 void QuantInfo::flatten( Node n, bool beneathQuant ) {
   Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
-  if( n.hasBoundVar() ){
+  if (expr::hasBoundVar(n))
+  {
     if( n.getKind()==BOUND_VARIABLE ){
       d_inMatchConstraint[n] = true;
     }
@@ -982,7 +995,8 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
       }
     }
   }else{
-    if( n.hasBoundVar() ){
+    if (expr::hasBoundVar(n))
+    {
       d_type_not = false;
       d_n = n;
       if( d_n.getKind()==NOT ){
@@ -1012,21 +1026,28 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
           Assert( d_n.getType().isBoolean() );
           d_type = typ_bool_var;
         }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){
-          for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
-            if( d_n[i].hasBoundVar() ){
-              if( !qi->isVar( d_n[i] ) ){
-                Trace("qcf-qregister-debug")  << "ERROR : not var " << d_n[i] << std::endl;
+          for (unsigned i = 0; i < d_n.getNumChildren(); i++)
+          {
+            if (expr::hasBoundVar(d_n[i]))
+            {
+              if (!qi->isVar(d_n[i]))
+              {
+                Trace("qcf-qregister-debug")
+                    << "ERROR : not var " << d_n[i] << std::endl;
               }
-              Assert( qi->isVar( d_n[i] ) );
-              if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){
-                d_qni_var_num[i+1] = qi->d_var_num[d_n[i]];
+              Assert(qi->isVar(d_n[i]));
+              if (d_n.getKind() != EQUAL && qi->isVar(d_n[i]))
+              {
+                d_qni_var_num[i + 1] = qi->d_var_num[d_n[i]];
               }
-            }else{
+            }
+            else
+            {
               d_qni_gterm[i] = d_n[i];
-              qi->setGroundSubterm( d_n[i] );
+              qi->setGroundSubterm(d_n[i]);
             }
           }
-          d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint;
+          d_type = d_n.getKind() == EQUAL ? typ_eq : typ_tconstraint;
           Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;
         }
       }
@@ -1180,12 +1201,17 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
       }
     }
   }else if( d_type==typ_eq ){
-    for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
-      if( !d_n[i].hasBoundVar() ){
-        TNode t = p->getTermDatabase()->getEntailedTerm( d_n[i] );
-        if( t.isNull() ){
+    for (unsigned i = 0; i < d_n.getNumChildren(); i++)
+    {
+      if (!expr::hasBoundVar(d_n[i]))
+      {
+        TNode t = p->getTermDatabase()->getEntailedTerm(d_n[i]);
+        if (t.isNull())
+        {
           d_ground_eval[i] = d_n[i];
-        }else{
+        }
+        else
+        {
           d_ground_eval[i] = t;
         }
       }
@@ -1772,7 +1798,8 @@ Node MatchGen::getMatchOperator( QuantConflictFind * p, Node n ) {
 }
 
 bool MatchGen::isHandled( TNode n ) {
-  if( n.getKind()!=BOUND_VARIABLE && n.hasBoundVar() ){
+  if (n.getKind() != BOUND_VARIABLE && expr::hasBoundVar(n))
+  {
     if( !isHandledBoolConnective( n ) && !isHandledUfTerm( n ) && n.getKind()!=EQUAL && n.getKind()!=ITE ){
       return false;
     }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 4799de09d..37451b776 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -14,14 +14,15 @@
 
 #include "theory/quantifiers/quantifiers_rewriter.h"
 
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/bv_inverter.h"
+#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -774,9 +775,11 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){
       }
     }
   }else if( n.getKind()==EQUAL ){
-    for( unsigned i=0; i<2; i++ ){
-      if( n[i].getKind()==BOUND_VARIABLE ){
-        if (!n[1 - i].hasSubterm(n[i]))
+    for (unsigned i = 0; i < 2; i++)
+    {
+      if (n[i].getKind() == BOUND_VARIABLE)
+      {
+        if (!expr::hasSubterm(n[1 - i], n[i]))
         {
           return true;
         }
@@ -874,8 +877,9 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){
   return body;
 }
 
-bool QuantifiersRewriter::isVariableElim( Node v, Node s ) {
-  return !s.hasSubterm(v) && s.getType().isSubtypeOf(v.getType());
+bool QuantifiersRewriter::isVariableElim(Node v, Node s)
+{
+  return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType());
 }
 
 void QuantifiersRewriter::isVariableBoundElig( Node n, std::map< Node, int >& exclude, std::map< Node, std::map< int, bool > >& visited, bool hasPol, bool pol, 
@@ -1112,7 +1116,7 @@ bool QuantifiersRewriter::computeVariableElimLit(
       Trace("var-elim-quant")
           << "Variable eliminate based on bit-vector inversion : " << var
           << " -> " << slv << std::endl;
-      Assert(!slv.hasSubterm(var));
+      Assert(!expr::hasSubterm(slv, var));
       Assert(slv.getType().isSubtypeOf(var.getType()));
       vars.push_back(var);
       subs.push_back(slv);
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 6a7eb8197..5f5a84a6b 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -14,6 +14,7 @@
  **/
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
@@ -726,12 +727,14 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st
       // check if it is a variable equality
       TNode v;
       Node s;
-      for( unsigned r=0; r<2; r++ ){
-        if( std::find( vars.begin(), vars.end(), slit[r] )!=vars.end() ){
-          if (!slit[1 - r].hasSubterm(slit[r]))
+      for (unsigned r = 0; r < 2; r++)
+      {
+        if (std::find(vars.begin(), vars.end(), slit[r]) != vars.end())
+        {
+          if (!expr::hasSubterm(slit[1 - r], slit[r]))
           {
             v = slit[r];
-            s = slit[1-r];
+            s = slit[1 - r];
             break;
           }
         }
@@ -741,13 +744,18 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st
         std::map< Node, Node > msum;
         if (ArithMSum::getMonomialSumLit(slit, msum))
         {
-          for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
-            if( std::find( vars.begin(), vars.end(), itm->first )!=vars.end() ){  
+          for (std::map<Node, Node>::iterator itm = msum.begin();
+               itm != msum.end();
+               ++itm)
+          {
+            if (std::find(vars.begin(), vars.end(), itm->first) != vars.end())
+            {
               Node veq_c;
               Node val;
               int ires =
                   ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL);
-              if (ires != 0 && veq_c.isNull() && !val.hasSubterm(itm->first))
+              if (ires != 0 && veq_c.isNull()
+                  && !expr::hasSubterm(val, itm->first))
               {
                 v = itm->first;
                 s = val;
@@ -859,7 +867,8 @@ void TransitionInference::process( Node n ) {
         }else{
           res = NodeManager::currentNM()->mkNode( kind::OR, disjuncts );
         }
-        if( !res.hasBoundVar() ){
+        if (!expr::hasBoundVar(res))
+        {
           Trace("cegqi-inv") << "*** inferred " << ( comp_num==1 ? "pre" : ( comp_num==-1 ? "post" : "trans" ) ) << "-condition : " << res << std::endl;
           d_com[comp_num].d_conjuncts.push_back( res );
           if( !const_var.empty() ){
@@ -1076,4 +1085,3 @@ Node TransitionInference::constructFormulaTrace( DetTrace& dt ) {
 }
   
 } //namespace CVC4
-
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 44835cc26..2ee120211 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -15,15 +15,16 @@
 #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
 
 #include "expr/datatype.h"
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
-#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
+#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
+#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
@@ -294,11 +295,12 @@ bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >&
       Assert( std::find( vars.begin(), vars.end(), eq[r] )==vars.end() );
       if( std::find( new_vars.begin(), new_vars.end(), eq[r] )==new_vars.end() ){
         Node eqro = eq[r==0 ? 1 : 0 ];
-        if (!eqro.hasSubterm(eq[r]))
+        if (!expr::hasSubterm(eqro, eq[r]))
         {
-          Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl;
-          new_vars.push_back( eq[r] );
-          new_subs.push_back( eqro );
+          Trace("csi-simp-debug")
+              << "---equality " << eq[r] << " = " << eqro << std::endl;
+          new_vars.push_back(eq[r]);
+          new_subs.push_back(eqro);
           return true;
         }
       }
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index cf06dfa45..7d91e9812 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/term_util.h"
 
 #include "expr/datatype.h"
+#include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
@@ -582,7 +583,7 @@ Node TermUtil::rewriteVtsSymbols( Node n ) {
     //rewriting infinity always takes precedence over rewriting delta
     for( unsigned r=0; r<2; r++ ){
       Node inf = getVtsInfinityIndex( r, false, false );
-      if (!inf.isNull() && n.hasSubterm(inf))
+      if (!inf.isNull() && expr::hasSubterm(n, inf))
       {
         if( rew_vts_inf.isNull() ){
           rew_vts_inf = inf;
@@ -595,16 +596,17 @@ Node TermUtil::rewriteVtsSymbols( Node n ) {
           subs_lhs.push_back( rew_vts_inf );
           n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
           n = Rewriter::rewrite( n );
-          //may have cancelled
-          if (!n.hasSubterm(rew_vts_inf))
+          // may have cancelled
+          if (!expr::hasSubterm(n, rew_vts_inf))
           {
             rew_vts_inf = Node::null();
           }
         }
       }
     }
-    if( rew_vts_inf.isNull() ){
-      if (!d_vts_delta.isNull() && n.hasSubterm(d_vts_delta))
+    if (rew_vts_inf.isNull())
+    {
+      if (!d_vts_delta.isNull() && expr::hasSubterm(n, d_vts_delta))
       {
         rew_delta = true;
       }
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 49954c111..9346970d1 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -18,13 +18,14 @@
 #include "theory/sets/theory_sets_private.h"
 
 #include "expr/emptyset.h"
+#include "expr/node_algorithm.h"
 #include "options/sets_options.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/sets/theory_sets.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/sets/normal_form.h"
+#include "theory/sets/theory_sets.h"
 #include "theory/theory_model.h"
 #include "util/result.h"
-#include "theory/quantifiers/term_database.h"
 
 #define AJR_IMPLEMENTATION
 
@@ -2200,28 +2201,37 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou
   
   //this is based off of Theory::ppAssert
   Node var;
-  if (in.getKind() == kind::EQUAL) {
-    if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
-        (in[1].getType()).isSubtypeOf(in[0].getType()) ){
-      if( !in[0].getType().isSet() || !options::setsExt() ){
+  if (in.getKind() == kind::EQUAL)
+  {
+    if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
+        && (in[1].getType()).isSubtypeOf(in[0].getType()))
+    {
+      if (!in[0].getType().isSet() || !options::setsExt())
+      {
         outSubstitutions.addSubstitution(in[0], in[1]);
         var = in[0];
         status = Theory::PP_ASSERT_STATUS_SOLVED;
       }
-    }else if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
-        (in[0].getType()).isSubtypeOf(in[1].getType())){
-      if( !in[1].getType().isSet() || !options::setsExt() ){
+    }
+    else if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])
+             && (in[0].getType()).isSubtypeOf(in[1].getType()))
+    {
+      if (!in[1].getType().isSet() || !options::setsExt())
+      {
         outSubstitutions.addSubstitution(in[1], in[0]);
         var = in[1];
         status = Theory::PP_ASSERT_STATUS_SOLVED;
       }
-    }else if (in[0].isConst() && in[1].isConst()) {
-      if (in[0] != in[1]) {
+    }
+    else if (in[0].isConst() && in[1].isConst())
+    {
+      if (in[0] != in[1])
+      {
         status = Theory::PP_ASSERT_STATUS_CONFLICT;
       }
     }
   }
-  
+
   if( status==Theory::PP_ASSERT_STATUS_SOLVED ){
     Trace("sets-var-elim") << "Sets : ppAssert variable eliminated : " << in << ", var = " << var << std::endl;
     /*
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 2585d1ee3..036bb4ada 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "theory/substitutions.h"
+#include "expr/node_algorithm.h"
 #include "theory/rewriter.h"
 
 using namespace std;
@@ -209,15 +210,18 @@ void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateC
   }
 }
 
-
-static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
-static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
+static bool check(TNode node,
+                  const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
+static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions)
+{
   SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
   SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end();
   Debug("substitution") << "checking " << node << endl;
-  for (; it != it_end; ++ it) {
+  for (; it != it_end; ++it)
+  {
     Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << endl;
-    if (node.hasSubterm((*it).first)) {
+    if (expr::hasSubterm(node, (*it).first))
+    {
       Debug("substitution") << "-- FAIL" << endl;
       return false;
     }
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 311776693..eedf0ff52 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -22,6 +22,7 @@
 #include <string>
 
 #include "base/cvc4_assert.h"
+#include "expr/node_algorithm.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/ext_theory.h"
 #include "theory/quantifiers_engine.h"
@@ -283,27 +284,31 @@ void Theory::computeRelevantTerms(set<Node>& termSet,
   }
 }
 
-
 Theory::PPAssertStatus Theory::ppAssert(TNode in,
                                         SubstitutionMap& outSubstitutions)
 {
-  if (in.getKind() == kind::EQUAL) {
+  if (in.getKind() == kind::EQUAL)
+  {
     // (and (= x t) phi) can be replaced by phi[x/t] if
     // 1) x is a variable
     // 2) x is not in the term t
     // 3) x : T and t : S, then S <: T
-    if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
-        (in[1].getType()).isSubtypeOf(in[0].getType()) ){
+    if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
+        && (in[1].getType()).isSubtypeOf(in[0].getType()))
+    {
       outSubstitutions.addSubstitution(in[0], in[1]);
       return PP_ASSERT_STATUS_SOLVED;
     }
-    if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
-        (in[0].getType()).isSubtypeOf(in[1].getType())){
+    if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])
+        && (in[0].getType()).isSubtypeOf(in[1].getType()))
+    {
       outSubstitutions.addSubstitution(in[1], in[0]);
       return PP_ASSERT_STATUS_SOLVED;
     }
-    if (in[0].isConst() && in[1].isConst()) {
-      if (in[0] != in[1]) {
+    if (in[0].isConst() && in[1].isConst())
+    {
+      if (in[0] != in[1])
+      {
         return PP_ASSERT_STATUS_CONFLICT;
       }
     }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4aed35e75..cedeb640f 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -22,6 +22,7 @@
 #include "decision/decision_engine.h"
 #include "expr/attribute.h"
 #include "expr/node.h"
+#include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
 #include "options/bv_options.h"
 #include "options/options.h"
@@ -31,8 +32,8 @@
 #include "proof/lemma_proof.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
-#include "smt/term_formula_removal.h"
 #include "smt/logic_exception.h"
+#include "smt/term_formula_removal.h"
 #include "smt_util/lemma_output_channel.h"
 #include "smt_util/node_visitor.h"
 #include "theory/arith/arith_ite_utils.h"
@@ -396,7 +397,7 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       // the atom should not have free variables
       Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
                       << std::endl;
-      Assert(!preprocessed.hasFreeVar());
+      Assert(!expr::hasFreeVar(preprocessed));
       // Pre-register the terms in the atom
       Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
       theories = Theory::setRemove(THEORY_BOOL, theories);