Check free variables in assertions (#1737)

4 files changed, 84 insertions, 0 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 010b36e94..f812be5a3 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -530,6 +530,13 @@ bool Expr::isConst() const {
   return d_node->isConst();
 }
 
+bool Expr::hasFreeVariable() const
+{
+  ExprManagerScope ems(*this);
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->hasFreeVar();
+}
+
 void Expr::toStream(std::ostream& out, int depth, bool types, size_t dag,
                     OutputLanguage language) const {
   ExprManagerScope ems(*this);
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index cb4534c08..3a27fca25 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -526,6 +526,13 @@ public:
    */
   bool isConst() const;
 
+  /**
+   * Check if this expression contains a free variable.
+   *
+   * @return true if this node contains a free variable.
+   */
+  bool hasFreeVariable() const;
+
   /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
    *
    * It has been decided for now to hold off on implementations of
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 */
diff --git a/src/expr/node.h b/src/expr/node.h
index e1b979570..14630bae1 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -436,6 +436,12 @@ public:
   bool hasBoundVar();
 
   /**
+   * Returns true iff this node contains a free variable.
+   * @return true iff this node contains a free variable.
+   */
+  bool hasFreeVar();
+
+  /**
    * Convert this Node into an Expr using the currently-in-scope
    * manager.  Essentially this is like an "operator Expr()" but we
    * don't want it to compete with implicit conversions between e.g.