1 files changed, 59 insertions, 0 deletions
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