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.

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index bfb6c0f3973686ac2472ae63c0cb682941e8a31b..d33c72ede3d986ec76a9b4d3a4ed932e8ee230b6 100644 (file)
--- 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<TypeNode> 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<TypeNode> cargsIte;
+    cargsIte.push_back(unres_bt);
+    cargsIte.push_back(unres_t);
+    cargsIte.push_back(unres_t);
+    sdts[i].addConstructor(k, cargsIte);
   }
   std::map<TypeNode, unsigned>::iterator itgat;
   // initialize the datatypes (except for the last one, reserved for Bool)