summaryrefslogtreecommitdiff
path: root/src/expr/node_algorithm.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/node_algorithm.h')
-rw-r--r--src/expr/node_algorithm.h8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 656f162ae..727f5ba75 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -73,6 +73,14 @@ bool getFreeVariables(TNode n,
bool computeFv = true);
/**
+ * Get all variables in n.
+ * @param n The node under investigation
+ * @param vs The set which free variables are added to
+ * @return true iff this node contains a free variable.
+ */
+bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs);
+
+/**
* For term n, this function collects the symbols that occur as a subterms
* of n. A symbol is a variable that does not have kind BOUND_VARIABLE.
* @param n The node under investigation
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback