diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-03-30 06:33:33 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-30 13:33:33 +0000 |
commit | e5bf082fde4c8b3c10448cbf3cb962739df9cf66 (patch) | |
tree | 1f5690a300a3558355915411b61ec617f8e1a54e | |
parent | c7a8c32825af7dceb6cee631523a480a5b2cc6ba (diff) |
Give a better error when sygus grammar rules contain free variables. (#6199)
-rw-r--r-- | src/api/cvc4cpp.cpp | 29 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 8 | ||||
-rw-r--r-- | test/unit/api/grammar_black.cpp | 2 |
3 files changed, 39 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.*/ 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); |