Add getFreeVariables method to node algorithm (#2852)

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 3905ad5c9cf8e81acb5d7780b508e670dacfaf6a..6923efec279ac8174d2336e822a3443ed2384aa0 100644 (file)
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -158,6 +158,14 @@ bool hasBoundVar(TNode n)
 }
 
 bool hasFreeVar(TNode n)
+{
+  std::unordered_set<Node, NodeHashFunction> fvs;
+  return getFreeVariables(n, fvs, false);
+}
+
+bool getFreeVariables(TNode n,
+                      std::unordered_set<Node, NodeHashFunction>& fvs,
+                      bool computeFv)
 {
   std::unordered_set<TNode, TNodeHashFunction> bound_var;
   std::unordered_map<TNode, bool, TNodeHashFunction> visited;
@@ -184,7 +192,14 @@ bool hasFreeVar(TNode n)
       {
         if (bound_var.find(cur) == bound_var.end())
         {
-          return true;
+          if (computeFv)
+          {
+            fvs.insert(cur);
+          }
+          else
+          {
+            return true;
+          }
         }
       }
       else if (isQuant)
@@ -218,7 +233,8 @@ bool hasFreeVar(TNode n)
       visited[cur] = true;
     }
   } while (!visit.empty());
-  return false;
+
+  return !fvs.empty();
 }
 
 void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms)

diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index d825d7f57def283858ca3d189040c65e5fce6afe..bf2cb5877c689b50ab1d13b098b5e07c90572c5f 100644 (file)
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -59,6 +59,19 @@ bool hasBoundVar(TNode n);
  */
 bool hasFreeVar(TNode n);
 
+/**
+ * Get the free variables in n, that is, the subterms of n of kind
+ * BOUND_VARIABLE that are not bound in n, adds these to fvs.
+ * @param n The node under investigation
+ * @param fvs The set which free variables are added to
+ * @param computeFv If this flag is false, then we only return true/false and
+ * do not add to fvs.
+ * @return true iff this node contains a free variable.
+ */
+bool getFreeVariables(TNode n,
+                      std::unordered_set<Node, NodeHashFunction>& fvs,
+                      bool computeFv = true);
+
 /**
  * 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.