From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 23 Mar 2020 18:30:48 +0000 (-0500)
Subject: Throw exception for non-well-founded unimplemented SyGuS types. (#4125)
X-Git-Tag: cvc5-1.0.0~3454
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd515b59583cba1afed8fbb583f8012a214feaad;p=cvc5.git

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 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<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)