Check free variables in assertions (#1737)

7 files changed, 112 insertions, 24 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.
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 2c26c824f..ae9d304f1 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -429,6 +429,17 @@ command [std::unique_ptr<CVC4::Command>* cmd]
         csen->setMuted(true);
         PARSER_STATE->preemptCommand(csen);
       }
+      // if sygus, check whether it has a free variable
+      // this is because, due to the sygus format, one can write assertions
+      // that have free function variables in them
+      if (PARSER_STATE->sygus())
+      {
+        if (expr.hasFreeVariable())
+        {
+          PARSER_STATE->parseError("Assertion has free variable. Perhaps you "
+                                   "meant constraint instead of assert?");
+        }
+      }
     }
   | /* check-sat */
     CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index 890b7fcd3..0a0dac4ba 100644
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -250,37 +250,28 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs,
         // now must check if it has other bound variables
         std::vector<Node> bvs;
         TermUtil::getBoundVars(cr, bvs);
-        if (bvs.size() > d_si_vars.size())
+        // bound variables must be contained in the single invocation variables
+        for (const Node& bv : bvs)
         {
-          // getBoundVars also collects functions in the rare case that we are
-          // synthesizing a function with 0 arguments
-          // take these into account below.
-          unsigned n_const_synth_fun = 0;
-          for (unsigned j = 0; j < bvs.size(); j++)
+          if (std::find(d_si_vars.begin(), d_si_vars.end(), bv)
+              == d_si_vars.end())
           {
-            if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bvs[j])
-                != d_input_funcs.end())
+            // getBoundVars also collects functions in the rare case that we are
+            // synthesizing a function with 0 arguments, take this into account
+            // here.
+            if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bv)
+                == d_input_funcs.end())
             {
-              n_const_synth_fun++;
+              Trace("si-prt")
+                  << "...not ground single invocation." << std::endl;
+              ngroundSingleInvocation = true;
+              singleInvocation = false;
             }
           }
-          if (bvs.size() - n_const_synth_fun > d_si_vars.size())
-          {
-            Trace("si-prt") << "...not ground single invocation." << std::endl;
-            ngroundSingleInvocation = true;
-            singleInvocation = false;
-          }
-          else
-          {
-            Trace("si-prt") << "...ground single invocation : success, after "
-                               "removing 0-arg synth functions."
-                            << std::endl;
-          }
         }
-        else
+        if (singleInvocation)
         {
-          Trace("si-prt") << "...ground single invocation : success."
-                          << std::endl;
+          Trace("si-prt") << "...ground single invocation" << std::endl;
         }
       }
       else
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f3489f5ad..de71a8b5e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -393,6 +393,8 @@ void TheoryEngine::preRegister(TNode preprocessed) {
         d_sharedTerms.addEqualityToPropagate(preprocessed);
       }
 
+      // the atom should not have free variables
+      Assert(!preprocessed.hasFreeVar());
       // Pre-register the terms in the atom
       Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
       theories = Theory::setRemove(THEORY_BOOL, theories);