Give a better error when sygus grammar rules contain free variables. (#6199)

2 files changed, 37 insertions, 0 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f33095a4b..e8b190003 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -45,6 +45,7 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node.h"
+#include "expr/node_algorithm.h"
 #include "expr/node_manager.h"
 #include "expr/sequence.h"
 #include "expr/type_node.h"
@@ -3659,6 +3660,9 @@ void Grammar::addRule(const Term& ntSymbol, const Term& rule)
          "predeclaration";
   CVC4_API_CHECK(ntSymbol.d_node->getType() == rule.d_node->getType())
       << "Expected ntSymbol and rule to have the same sort";
+  CVC4_API_ARG_CHECK_EXPECTED(!containsFreeVariables(rule), rule)
+      << "a term whose free variables are limited to synthFun/synthInv "
+         "parameters and non-terminal symbols of the grammar";
   //////// all checks before this line
   d_ntsToTerms[ntSymbol].push_back(rule);
   ////////
@@ -3676,6 +3680,13 @@ void Grammar::addRules(const Term& ntSymbol, const std::vector<Term>& rules)
       d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
       << "ntSymbol to be one of the non-terminal symbols given in the "
          "predeclaration";
+  for (size_t i = 0, n = rules.size(); i < n; ++i)
+  {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        !containsFreeVariables(rules[i]), rules[i], rules, i)
+        << "a term whose free variables are limited to synthFun/synthInv "
+           "parameters and non-terminal symbols of the grammar";
+  }
   //////// all checks before this line
   d_ntsToTerms[ntSymbol].insert(
       d_ntsToTerms[ntSymbol].cend(), rules.cbegin(), rules.cend());
@@ -3988,6 +3999,24 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt,
   CVC4_API_TRY_CATCH_END;
 }
 
+bool Grammar::containsFreeVariables(const Term& rule) const
+{
+  std::unordered_set<TNode, TNodeHashFunction> scope;
+
+  for (const Term& sygusVar : d_sygusVars)
+  {
+    scope.emplace(*sygusVar.d_node);
+  }
+
+  for (const Term& ntsymbol : d_ntSyms)
+  {
+    scope.emplace(*ntsymbol.d_node);
+  }
+
+  std::unordered_set<Node, NodeHashFunction> fvs;
+  return expr::getFreeVariablesScope(*rule.d_node, fvs, scope, false);
+}
+
 std::ostream& operator<<(std::ostream& out, const Grammar& grammar)
 {
   return out << grammar.toString();
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index a176744ef..5a8f62983 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2250,6 +2250,14 @@ class CVC4_EXPORT Grammar
    */
   void addSygusConstructorVariables(DatatypeDecl& dt, const Sort& sort) const;
 
+  /**
+   * Check if <rule> contains variables that are neither parameters of
+   * the corresponding synthFun/synthInv nor non-terminals.
+   * @param rule the non-terminal allowed to be any constant
+   * @return <true> if <rule> contains free variables and <false> otherwise
+   */
+  bool containsFreeVariables(const Term& rule) const;
+
   /** The solver that created this grammar. */
   const Solver* d_solver;
   /** Input variables to the corresponding function/invariant to synthesize.*/