Fix bugs in getFreeVariables (#5601)

Did not consider scopes properly, which would fail to say that formulas with escaped variables (both bound and unbound) in formula had free variables.

2 files changed, 48 insertions, 25 deletions

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index f41bef37b..2439e28b6 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -328,8 +328,16 @@ 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;
+  std::unordered_set<TNode, TNodeHashFunction> scope;
+  return getFreeVariablesScope(n, fvs, scope, computeFv);
+}
+
+bool getFreeVariablesScope(TNode n,
+                           std::unordered_set<Node, NodeHashFunction>& fvs,
+                           std::unordered_set<TNode, TNodeHashFunction>& scope,
+                           bool computeFv)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(n);
@@ -342,15 +350,14 @@ bool getFreeVariables(TNode n,
     {
       continue;
     }
-    Kind k = cur.getKind();
-    bool isQuant = cur.isClosure();
-    std::unordered_map<TNode, bool, TNodeHashFunction>::iterator itv =
+    std::unordered_set<TNode, TNodeHashFunction>::iterator itv =
         visited.find(cur);
     if (itv == visited.end())
     {
-      if (k == kind::BOUND_VARIABLE)
+      visited.insert(cur);
+      if (cur.getKind() == kind::BOUND_VARIABLE)
       {
-        if (bound_var.find(cur) == bound_var.end())
+        if (scope.find(cur) == scope.end())
         {
           if (computeFv)
           {
@@ -362,32 +369,34 @@ bool getFreeVariables(TNode n,
           }
         }
       }
-      else if (isQuant)
+      else if (cur.isClosure())
       {
+        // add to scope
         for (const TNode& cn : cur[0])
         {
           // should not shadow
-          Assert(bound_var.find(cn) == bound_var.end());
-          bound_var.insert(cn);
+          Assert(scope.find(cn) == scope.end());
+          scope.insert(cn);
+        }
+        // must make recursive call to use separate cache
+        if (getFreeVariablesScope(cur[1], fvs, scope, computeFv) && !computeFv)
+        {
+          return true;
+        }
+        // cleanup
+        for (const TNode& cn : cur[0])
+        {
+          scope.erase(cn);
         }
-        visit.push_back(cur);
-      }
-      // must visit quantifiers again to clean up below
-      visited[cur] = !isQuant;
-      if (cur.hasOperator())
-      {
-        visit.push_back(cur.getOperator());
       }
-      visit.insert(visit.end(), cur.begin(), cur.end());
-    }
-    else if (!itv->second)
-    {
-      Assert(isQuant);
-      for (const TNode& cn : cur[0])
+      else
       {
-        bound_var.erase(cn);
+        if (cur.hasOperator())
+        {
+          visit.push_back(cur.getOperator());
+        }
+        visit.insert(visit.end(), cur.begin(), cur.end());
       }
-      visited[cur] = true;
     }
   } while (!visit.empty());
 
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 7b6dd4f8c..f5d9f6516 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -105,6 +105,20 @@ bool hasClosure(Node n);
 bool getFreeVariables(TNode n,
                       std::unordered_set<Node, NodeHashFunction>& fvs,
                       bool computeFv = true);
+/**
+ * Get the free variables in n, that is, the subterms of n of kind
+ * BOUND_VARIABLE that are not bound in n or occur in scope, adds these to fvs.
+ * @param n The node under investigation
+ * @param fvs The set which free variables are added to
+ * @param scope The scope we are considering.
+ * @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 getFreeVariablesScope(TNode n,
+                           std::unordered_set<Node, NodeHashFunction>& fvs,
+                           std::unordered_set<TNode, TNodeHashFunction>& scope,
+                           bool computeFv = true);
 
 /**
  * Get all variables in n.