Merge branch 'master' into warn_spaceswarn_spaces

1 files changed, 64 insertions, 0 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index b41014f9c..cb61362c5 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -137,9 +137,73 @@ bool NodeTemplate<ref_count>::hasBoundVar() {
   return getAttribute(HasBoundVarAttr());
 }
 
+template <bool ref_count>
+bool NodeTemplate<ref_count>::hasFreeVar()
+{
+  assertTNodeNotExpired();
+  std::unordered_set<TNode, TNodeHashFunction> bound_var;
+  std::unordered_map<TNode, bool, TNodeHashFunction> visited;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(*this);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    // can skip if it doesn't have a bound variable
+    if (!cur.hasBoundVar())
+    {
+      continue;
+    }
+    Kind k = cur.getKind();
+    bool isQuant = k == kind::FORALL || k == kind::EXISTS || k == kind::LAMBDA
+                   || k == kind::CHOICE;
+    std::unordered_map<TNode, bool, TNodeHashFunction>::iterator itv =
+        visited.find(cur);
+    if (itv == visited.end())
+    {
+      if (k == kind::BOUND_VARIABLE)
+      {
+        if (bound_var.find(cur) == bound_var.end())
+        {
+          return true;
+        }
+      }
+      else if (isQuant)
+      {
+        for (const TNode& cn : cur[0])
+        {
+          // should not shadow
+          Assert(bound_var.find(cn) == bound_var.end());
+          bound_var.insert(cn);
+        }
+        visit.push_back(cur);
+      }
+      // must visit quantifiers again to clean up below
+      visited[cur] = !isQuant;
+      for (const TNode& cn : cur)
+      {
+        visit.push_back(cn);
+      }
+    }
+    else if (!itv->second)
+    {
+      Assert(isQuant);
+      for (const TNode& cn : cur[0])
+      {
+        bound_var.erase(cn);
+      }
+      visited[cur] = true;
+    }
+  } while (!visit.empty());
+  return false;
+}
+
 template bool NodeTemplate<true>::isConst() const;
 template bool NodeTemplate<false>::isConst() const;
 template bool NodeTemplate<true>::hasBoundVar();
 template bool NodeTemplate<false>::hasBoundVar();
+template bool NodeTemplate<true>::hasFreeVar();
+template bool NodeTemplate<false>::hasFreeVar();
 
 }/* CVC4 namespace */