Avoid cases of empty sygus grammars (#3301)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9a8232df9a7b50f7916737e0d4080b0e1e05a7e5..e838398baba698177e07f10b0c798d3efedbdeee 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1096,13 +1096,13 @@ sygusGrammar[CVC4::Type & ret,
         PARSER_STATE->addSygusConstructorVariables(
             datatypes[dtProcessed], sygusVars, t);
       }
-    )*
+    )+
     RPAREN_TOK
     RPAREN_TOK
     {
       dtProcessed++;
     }
-  )*
+  )+
   RPAREN_TOK
   {
     if (dtProcessed != sortedVarNames.size())
@@ -1122,6 +1122,30 @@ sygusGrammar[CVC4::Type & ret,
       bool aci = allowConst.find(i)!=allowConst.end();
       Type btt = sortedVarNames[i].second;
       datatypes[i].setSygus(btt, bvl, aci, false);
+      Trace("parser-sygus2") << "- " << datatypes[i].getName()
+                             << ", #cons= " << datatypes[i].getNumConstructors()
+                             << ", aci= " << aci << std::endl;
+      // We can be in a case where the only rule specified was (Variable T)
+      // and there are no variables of type T, in which case this is a bogus
+      // grammar. This results in the error below.
+      // We can also be in a case where the only rule specified was
+      // (Constant T), in which case we have not yet added a constructor. We
+      // ensure an arbitrary constant is added in this case.
+      if (datatypes[i].getNumConstructors() == 0)
+      {
+        if (aci)
+        {
+          Expr c = btt.mkGroundTerm();
+          PARSER_STATE->addSygusConstructorTerm(datatypes[i], c, ntsToUnres);
+        }
+        else
+        {
+          std::stringstream se;
+          se << "Grouped rule listing for " << datatypes[i].getName()
+             << " produced an empty rule list.";
+          PARSER_STATE->parseError(se.str());
+        }
+      }
     }
     // pop scope from the pre-declaration
     PARSER_STATE->popScope();

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d5ce552e6d9ac9c71b5ce7b576217f1ecefaebdd..b47d22492c324e2847841766577219af1ae16c5f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1698,6 +1698,7 @@ set(regress_1_tests
   regress1/sygus/nia-max-square-ns.sy
   regress1/sygus/no-flat-simp.sy
   regress1/sygus/no-mention.sy
+  regress1/sygus/only-const-grammar.sy
   regress1/sygus/parity-si-rcons.sy
   regress1/sygus/pbe_multi.sy
   regress1/sygus/phone-1-long.sy

diff --git a/test/regress/regress1/sygus/only-const-grammar.sy b/test/regress/regress1/sygus/only-const-grammar.sy
new file mode 100644 (file)
index 0000000..25effd1
--- /dev/null
+++ b/test/regress/regress1/sygus/only-const-grammar.sy
@@ -0,0 +1,20 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Int
+  ((Start Int) (CInt Int))
+  (
+    (Start Int ((+ x CInt)))
+    (CInt Int ((Constant Int)))
+  )
+)
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (f 0 0) 2))
+
+(constraint (= (f 1 1) 3))
+
+(check-synth)