From dd515b59583cba1afed8fbb583f8012a214feaad Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Mar 2020 13:30:48 -0500 Subject: Throw exception for non-well-founded unimplemented SyGuS types. (#4125) Fixes #3931. Currently we print a warning for unimplemented types when constructing default SyGuS grammars. We should additionally throw an exception when the unimplemented type would lead to a non-well-founded datatype. --- .../quantifiers/sygus/sygus_grammar_cons.cpp | 28 +++++++++++++++------- 1 file changed, 20 insertions(+), 8 deletions(-) (limited to 'src/theory/quantifiers') diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index bfb6c0f39..d33c72ede 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -682,14 +682,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( sdts[i].addConstructor(consts[j], ss.str(), cargsEmpty); } } - // ITE - Kind k = ITE; - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - std::vector cargsIte; - cargsIte.push_back(unres_bt); - cargsIte.push_back(unres_t); - cargsIte.push_back(unres_t); - sdts[i].addConstructor(k, cargsIte); if (types[i].isReal()) { @@ -898,6 +890,26 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( << "Warning: No implementation for default Sygus grammar of type " << types[i] << std::endl; } + + if (sdts[i].d_sdt.getNumConstructors() == 0) + { + // if there are no constructors yet by this point, we cannot make + // datatype, which can happen e.g. for unimplemented types + // that have no variables in the argument list of the + // function-to-synthesize. + std::stringstream ss; + ss << "Cannot make default grammar for " << types[i]; + throw LogicException(ss.str()); + } + + // always add ITE + Kind k = ITE; + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + std::vector cargsIte; + cargsIte.push_back(unres_bt); + cargsIte.push_back(unres_t); + cargsIte.push_back(unres_t); + sdts[i].addConstructor(k, cargsIte); } std::map::iterator itgat; // initialize the datatypes (except for the last one, reserved for Bool) -- cgit v1.2.3