Parse error for SyGuS version 1.0 vs 2.0 (#4057)

This adds a useful error message that recognizes a divergence in the expected input format (version 1 vs. version 2), which will be useful when we switch to SyGuS version 2 by default. This warning message is already potentially useful for users who are using --lang=sygus2.

1 files changed, 32 insertions, 1 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d01fd7a05..ec1eae7da 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -943,7 +943,38 @@ sygusGrammar[CVC4::api::Sort & ret,
 }
   :
   // predeclaration
-  LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
+  LPAREN_TOK
+  // We read a sorted variable list here in a custom way that throws an
+  // error to recognize if the user is using the (deprecated) version 1.0
+  // sygus syntax.
+  ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
+    sortSymbol[t,CHECK_DECLARED] (
+      // SyGuS version 1.0 expects a grammar ((Start Int ( ...
+      // SyGuS version 2.0 expects a predeclaration ((Start Int) ...
+      LPAREN_TOK
+      {
+        std::stringstream sse;
+        if (sortedVarNames.empty())
+        {
+          sse << "The expected SyGuS language is version 2.0, whereas the "
+              << "input appears to be SyGuS version 1.0 format. The version "
+              << "2.0 format requires a predeclaration of the non-terminal "
+              << "symbols of the grammar to be given prior to the definition "
+              << "of the grammar. See https://sygus.org/language/ for details "
+              << "and examples. CVC4 versions past 1.8 do not support SyGuS "
+              << "version 1.0.";
+        }
+        else
+        {
+          // an unknown syntax error
+          sse << "Unexpected syntax for SyGuS predeclaration.";
+        }
+        PARSER_STATE->parseError(sse.str().c_str());
+      }
+    | RPAREN_TOK )
+    { sortedVarNames.push_back(make_pair(name, t)); }
+  )*
+  RPAREN_TOK
   {
     // non-terminal symbols in the pre-declaration are locally scoped
     PARSER_STATE->pushScope(true);