From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 8 Apr 2022 21:17:29 +0000 (-0500)
Subject: Do not allow unresolved sorts in smt2 (#8587)
X-Git-Tag: cvc5-1.0.1~281
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5e8e2d12c80bfe13ddd41ad355b348cf97eb8191;p=cvc5.git

Do not allow unresolved sorts in smt2 (#8587)

This simplifies the smt2 parser so that we never parse "inlined" unresolved sorts. This infrastructure was used for accomodating the ad-hoc datatype syntax from SMT-LIB <=2.5, and SyGuS 1.0.

We now assume that sorts are fully declared wherever we parse them.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index edde6489e..6882223fa 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -255,7 +255,7 @@ command [std::unique_ptr<cvc5::Command>* cmd]
         sorts.push_back(PARSER_STATE->mkSort(*i));
       }
     }
-    sortSymbol[t,CHECK_DECLARED]
+    sortSymbol[t]
     { PARSER_STATE->popScope();
       // Do NOT call mkSort, since that creates a new sort!
       // This name is not its own distinct sort, it's an alias.
@@ -267,7 +267,7 @@ command [std::unique_ptr<cvc5::Command>* cmd]
     symbol[name,CHECK_NONE,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(name); }
     LPAREN_TOK sortList[sorts] RPAREN_TOK
-    sortSymbol[t,CHECK_DECLARED]
+    sortSymbol[t]
     { Trace("parser") << "declare fun: '" << name << "'" << std::endl;
       if( !sorts.empty() ) {
         t = PARSER_STATE->mkFlatFunctionType(sorts, t);
@@ -294,7 +294,7 @@ command [std::unique_ptr<cvc5::Command>* cmd]
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(name); }
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
-    sortSymbol[t,CHECK_DECLARED]
+    sortSymbol[t]
     { /* add variables to parser state before parsing term */
       Trace("parser") << "define fun: '" << name << "'" << std::endl;
       if( sortedVarNames.size() > 0 ) {
@@ -514,7 +514,7 @@ sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
     DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(name); }
-    sortSymbol[t,CHECK_DECLARED]
+    sortSymbol[t]
     {
       cvc5::Term var = SOLVER->declareSygusVar(name, t);
       PARSER_STATE->defineVar(name, var);
@@ -527,7 +527,7 @@ sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
     { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
-    ( sortSymbol[range,CHECK_DECLARED] )?
+    ( sortSymbol[range] )?
     {
       PARSER_STATE->pushScope();
       sygusVars = PARSER_STATE->bindBoundVars(sortedVarNames);
@@ -631,7 +631,7 @@ sygusGrammar[cvc5::Grammar*& ret,
   // 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] (
+    sortSymbol[t] (
       // SyGuS version 1.0 expects a grammar ((Start Int ( ...
       // SyGuS version 2.0 expects a predeclaration ((Start Int) ...
       LPAREN_TOK
@@ -675,7 +675,7 @@ sygusGrammar[cvc5::Grammar*& ret,
   LPAREN_TOK
   (
     LPAREN_TOK
-    symbol[name, CHECK_DECLARED, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED]
+    symbol[name, CHECK_DECLARED, SYM_VARIABLE] sortSymbol[t]
     {
       // check that it matches sortedVarNames
       if (sortedVarNames[dtProcessed].first != name)
@@ -701,11 +701,11 @@ sygusGrammar[cvc5::Grammar*& ret,
         // add term as constructor to datatype
         ret->addRule(ntSyms[dtProcessed], e);
       }
-      | LPAREN_TOK SYGUS_CONSTANT_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
+      | LPAREN_TOK SYGUS_CONSTANT_TOK sortSymbol[t] RPAREN_TOK {
         // allow constants in datatype for ntSyms[dtProcessed]
         ret->addAnyConstant(ntSyms[dtProcessed]);
       }
-      | LPAREN_TOK SYGUS_VARIABLE_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
+      | LPAREN_TOK SYGUS_VARIABLE_TOK sortSymbol[t] RPAREN_TOK {
         // add variable constructors to datatype
         ret->addAnyVariable(ntSyms[dtProcessed]);
       }
@@ -774,7 +774,7 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd]
   : DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_NONE,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(name); }
-    sortSymbol[t,CHECK_DECLARED]
+    sortSymbol[t]
     { // allow overloading here
       if( PARSER_STATE->sygus() )
       {
@@ -815,7 +815,7 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd]
     symbol[fname,CHECK_NONE,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(fname); }
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
-    sortSymbol[t,CHECK_DECLARED]
+    sortSymbol[t]
     {
       func =
           PARSER_STATE->bindDefineFunRec(fname, sortedVarNames, t, flattenVars);
@@ -836,7 +836,7 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd]
       symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
       { PARSER_STATE->checkUserSymbol(fname); }
       LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
-      sortSymbol[t,CHECK_DECLARED]
+      sortSymbol[t]
       {
         flattenVars.clear();
         func = PARSER_STATE->bindDefineFunRec(
@@ -979,7 +979,7 @@ extendedCommand[std::unique_ptr<cvc5::Command>* cmd]
     DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(name); }
-    sortSymbol[t,CHECK_DECLARED]
+    sortSymbol[t]
     term[e, e2]
     {
       // declare the name down here (while parsing term, signature
@@ -1028,14 +1028,14 @@ extendedCommand[std::unique_ptr<cvc5::Command>* cmd]
       cmd->reset(new GetInterpolantNextCommand);
     }
   | DECLARE_HEAP LPAREN_TOK
-    sortSymbol[t, CHECK_DECLARED]
-    sortSymbol[s, CHECK_DECLARED]
+    sortSymbol[t]
+    sortSymbol[s]
     { cmd->reset(new DeclareHeapCommand(t, s)); }
     RPAREN_TOK
   | DECLARE_POOL { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_NONE,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(name); }
-    sortSymbol[t,CHECK_DECLARED]
+    sortSymbol[t]
     LPAREN_TOK
     ( term[e, e2]
       { terms.push_back( e ); }
@@ -1574,13 +1574,13 @@ qualIdentifier[cvc5::ParseOp& p]
 }
 : identifier[p]
   | LPAREN_TOK AS_TOK
-    ( CONST_TOK sortSymbol[type, CHECK_DECLARED]
+    ( CONST_TOK sortSymbol[type]
       {
         p.d_kind = cvc5::CONST_ARRAY;
         PARSER_STATE->parseOpApplyTypeAscription(p, type);
       }
     | identifier[p]
-      sortSymbol[type, CHECK_DECLARED]
+      sortSymbol[type]
       {
         PARSER_STATE->parseOpApplyTypeAscription(p, type);
       }
@@ -1720,7 +1720,7 @@ termAtomic[cvc5::Term& atomTerm]
         std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
         atomTerm = PARSER_STATE->mkCharConstant(hexStr);
       }
-    | FMF_CARD_TOK sortSymbol[t,CHECK_DECLARED] INTEGER_LITERAL
+    | FMF_CARD_TOK sortSymbol[t] INTEGER_LITERAL
       {
         uint32_t ubound = AntlrInput::tokenToUnsigned($INTEGER_LITERAL);
         atomTerm = SOLVER->mkCardinalityConstraint(t, ubound);
@@ -1910,14 +1910,14 @@ sortList[std::vector<cvc5::Sort>& sorts]
 @declarations {
   cvc5::Sort t;
 }
-  : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
+  : ( sortSymbol[t] { sorts.push_back(t); } )*
   ;
 
 nonemptySortList[std::vector<cvc5::Sort>& sorts]
 @declarations {
   cvc5::Sort t;
 }
-  : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
+  : ( sortSymbol[t] { sorts.push_back(t); } )+
   ;
 
 /**
@@ -1930,7 +1930,7 @@ sortedVarList[std::vector<std::pair<std::string, cvc5::Sort> >& sortedVars]
   cvc5::Sort t;
 }
   : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
-      sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
+      sortSymbol[t] RPAREN_TOK
       { sortedVars.push_back(make_pair(name, t)); }
     )*
   ;
@@ -1959,7 +1959,7 @@ sortName[std::string& name, cvc5::parser::DeclarationCheck check]
   : symbol[name,check,SYM_SORT]
   ;
 
-sortSymbol[cvc5::Sort& t, cvc5::parser::DeclarationCheck check]
+sortSymbol[cvc5::Sort& t]
 @declarations {
   std::string name;
   std::vector<cvc5::Sort> args;
@@ -1968,11 +1968,7 @@ sortSymbol[cvc5::Sort& t, cvc5::parser::DeclarationCheck check]
 }
   : sortName[name,CHECK_NONE]
     {
-      if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) {
-        t = PARSER_STATE->getSort(name);
-      } else {
-        t = PARSER_STATE->mkUnresolvedType(name);
-      }
+      t = PARSER_STATE->getSort(name);
     }
   | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;})
     symbol[name,CHECK_NONE,SYM_SORT]
@@ -2048,22 +2044,8 @@ sortSymbol[cvc5::Sort& t, cvc5::parser::DeclarationCheck check]
           t = SOLVER->mkSequenceSort( args[0] );
         } else if (name == "Tuple" && !PARSER_STATE->strictModeEnabled()) {
           t = SOLVER->mkTupleSort(args);
-        } else if(check == CHECK_DECLARED ||
-                  PARSER_STATE->isDeclared(name, SYM_SORT)) {
-          t = PARSER_STATE->getSort(name, args);
         } else {
-          // make unresolved type
-          if(args.empty()) {
-            t = PARSER_STATE->mkUnresolvedType(name);
-            Trace("parser-param") << "param: make unres type " << name
-                                  << std::endl;
-          } else {
-            t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args);
-            t = t.instantiate( args );
-            Trace("parser-param")
-                << "param: make unres param type " << name << " " << args.size()
-                << " " << PARSER_STATE->getArity( name ) << std::endl;
-          }
+          t = PARSER_STATE->getSort(name, args);
         }
       }
     ) RPAREN_TOK
@@ -2182,7 +2164,7 @@ selector[cvc5::DatatypeConstructorDecl& ctor]
   std::string id;
   cvc5::Sort t, t2;
 }
-  : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE]
+  : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t]
     { 
       ctor.addSelector(id, t);
       Trace("parser-idt") << "selector: " << id.c_str()