From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 30 Mar 2021 13:33:33 +0000 (-0700)
Subject: Give a better error when sygus grammar rules contain free variables. (#6199)
X-Git-Tag: cvc5-1.0.0~2012
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e5bf082fde4c8b3c10448cbf3cb962739df9cf66;p=cvc5.git

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

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.*/
diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp
index cabc3e249..c816fa5a3 100644
--- a/test/unit/api/grammar_black.cpp
+++ b/test/unit/api/grammar_black.cpp
@@ -44,6 +44,7 @@ TEST_F(TestApiBlackGrammar, addRule)
   ASSERT_THROW(g.addRule(start, nullTerm), CVC4ApiException);
   ASSERT_THROW(g.addRule(nts, d_solver.mkBoolean(false)), CVC4ApiException);
   ASSERT_THROW(g.addRule(start, d_solver.mkInteger(0)), CVC4ApiException);
+  ASSERT_THROW(g.addRule(start, nts), CVC4ApiException);
 
   d_solver.synthFun("f", {}, boolean, g);
 
@@ -68,6 +69,7 @@ TEST_F(TestApiBlackGrammar, addRules)
   ASSERT_THROW(g.addRules(start, {nullTerm}), CVC4ApiException);
   ASSERT_THROW(g.addRules(nts, {d_solver.mkBoolean(false)}), CVC4ApiException);
   ASSERT_THROW(g.addRules(start, {d_solver.mkInteger(0)}), CVC4ApiException);
+  ASSERT_THROW(g.addRules(start, {nts}), CVC4ApiException);
 
   d_solver.synthFun("f", {}, boolean, g);