From 5e8e2d12c80bfe13ddd41ad355b348cf97eb8191 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 8 Apr 2022 16:17:29 -0500 Subject: [PATCH] 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. --- src/parser/smt2/Smt2.g | 70 ++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 44 deletions(-) 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* 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* 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* 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 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 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* 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* 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* 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* 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* 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& sorts] @declarations { cvc5::Sort t; } - : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )* + : ( sortSymbol[t] { sorts.push_back(t); } )* ; nonemptySortList[std::vector& 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 >& 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 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() -- 2.30.2