From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Mar 2019 20:13:55 +0000 (-0500)
Subject:  Add getFreeVariables method to node algorithm (#2852)
X-Git-Tag: cvc5-1.0.0~4245
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7247f321dc8d319c5079b31d450c09029506274a;p=cvc5.git

 Add getFreeVariables method to node algorithm (#2852)
---

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 3905ad5c9..6923efec2 100644
--- 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 d825d7f57..bf2cb5877 100644
--- 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.