From 55050d2a3dff2d0428171c51d0ac54626d579d3a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 17 Aug 2018 12:37:19 -0500 Subject: Split sygus grammar to its own ANTLR grammar (#2307) --- src/parser/smt2/Smt2.g | 279 ++++++++++++++++++++++++++++--------------------- 1 file changed, 157 insertions(+), 122 deletions(-) (limited to 'src/parser') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 9bcac27ca..6491856a5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -603,24 +603,14 @@ sygusCommand [std::unique_ptr* cmd] Expr expr, expr2; Type t, range; std::vector terms; - std::vector sorts; std::vector sygus_vars; std::vector > sortedVarNames; SExpr sexpr; std::unique_ptr seq; - std::vector< std::vector< CVC4::SygusGTerm > > sgts; - std::vector< CVC4::Datatype > datatypes; - std::vector< std::vector > ops; - std::vector< std::vector< std::string > > cnames; - std::vector< std::vector< std::vector< CVC4::Type > > > cargs; - std::vector< bool > allow_const; - std::vector< std::vector< std::string > > unresolved_gterm_sym; - bool read_syntax = false; Type sygus_ret; - std::map< CVC4::Type, CVC4::Type > sygus_to_builtin; - std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr; int startIndex = -1; Expr synth_fun; + Type sygus_type; } : /* declare-var */ DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -676,124 +666,31 @@ sygusCommand [std::unique_ptr* cmd] sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); - terms.push_back( v ); sygus_vars.push_back( v ); } Expr bvl; - if( !terms.empty() ){ - bvl = MK_EXPR(kind::BOUND_VAR_LIST, terms); + if (!sygus_vars.empty()) + { + bvl = MK_EXPR(kind::BOUND_VAR_LIST, sygus_vars); } - terms.clear(); - terms.push_back(bvl); // associate this variable list with the synth fun std::vector< Expr > attr_val_bvl; attr_val_bvl.push_back( bvl ); Command* cattr_bvl = new SetUserAttributeCommand("sygus-synth-fun-var-list", synth_fun, attr_val_bvl); cattr_bvl->setMuted(true); PARSER_STATE->preemptCommand(cattr_bvl); + // set the sygus type to be range by default, which is overwritten below + // if a grammar is provided + sygus_type = range; } - ( LPAREN_TOK - ( LPAREN_TOK - symbol[name,CHECK_NONE,SYM_VARIABLE] - sortSymbol[t,CHECK_DECLARED] - { std::stringstream ss; - ss << fun << "_" << name; - if( name=="Start" ){ - startIndex = datatypes.size(); - } - std::string dname = ss.str(); - sgts.push_back( std::vector< CVC4::SygusGTerm >() ); - sgts.back().push_back( CVC4::SygusGTerm() ); - PARSER_STATE->pushSygusDatatypeDef( - t, dname, datatypes, sorts, ops, cnames, cargs, allow_const, - unresolved_gterm_sym); - Type unres_t; - if(!PARSER_STATE->isUnresolvedType(dname)) { - // if not unresolved, must be undeclared - Debug("parser-sygus") << "Make unresolved type : " << dname - << std::endl; - PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); - unres_t = PARSER_STATE->mkUnresolvedType(dname); - }else{ - Debug("parser-sygus") << "Get sort : " << dname << std::endl; - unres_t = PARSER_STATE->getSort(dname); - } - sygus_to_builtin[unres_t] = t; - Debug("parser-sygus") << "--- Read sygus grammar " << name - << " under function " << fun << "..." - << std::endl - << " type to resolve " << unres_t << std::endl - << " builtin type " << t << std::endl; - } - // Note the official spec for NTDef is missing the ( parens ) - // but they are necessary to parse SyGuS examples - LPAREN_TOK ( sygusGTerm[ sgts.back().back(), fun] - { sgts.back().push_back( CVC4::SygusGTerm() ); } )+ - RPAREN_TOK { sgts.back().pop_back(); } - RPAREN_TOK - )+ - RPAREN_TOK { read_syntax = true; } + ( + // optionally, read the sygus grammar + sygusGrammar[sygus_type, sygus_vars, fun] )? { // the sygus sym type specifies the required grammar for synth_fun, expressed as a type - Type sygus_sym_type; - if( !read_syntax ){ - sygus_sym_type = range; - PARSER_STATE->popScope(); - }else{ - Debug("parser-sygus") << "--- Process " << sgts.size() - << " sygus gterms..." << std::endl; - for( unsigned i=0; iprocessSygusGTerm( - sgts[i][j], i, datatypes, sorts, ops, cnames, cargs, - allow_const, unresolved_gterm_sym, sygus_vars, sygus_to_builtin, - sygus_to_builtin_expr, sub_ret ); - } - } - //swap index if necessary - Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl; - for( unsigned i=0; iparseError("Internal error : could not infer " - "builtin sort for nested gterm."); - } - datatypes[i].setSygus( sorts[i], terms[0], allow_const[i], false ); - PARSER_STATE->mkSygusDatatype( - datatypes[i], ops[i], cnames[i], cargs[i], - unresolved_gterm_sym[i], sygus_to_builtin ); - } - PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, ops); - //only care about datatypes/sorts/ops past here - PARSER_STATE->popScope(); - Debug("parser-sygus") << "--- Make " << datatypes.size() - << " mutual datatypes..." << std::endl; - for( unsigned i=0; i datatypeTypes = - PARSER_STATE->mkMutualDatatypeTypes(datatypes); - Command * cdd = new DatatypeDeclarationCommand(datatypeTypes); - // we set this command muted since there should only be one success printed - cdd->setMuted(true); - seq->addCommand(cdd); - if( sorts[0]!=range ){ - PARSER_STATE->parseError(std::string("Bad return type in grammar for " - "SyGuS function ") + fun); - } - sygus_sym_type = datatypeTypes[0]; - } - + PARSER_STATE->popScope(); // store a dummy variable which stands for second-order quantification, linked to synth fun by an attribute - PARSER_STATE->addSygusFunSymbol( sygus_sym_type, synth_fun ); + PARSER_STATE->addSygusFunSymbol(sygus_type, synth_fun); cmd->reset(seq.release()); } | /* constraint */ @@ -900,15 +797,153 @@ sygusCommand [std::unique_ptr* cmd] cmd->reset(new CheckSynthCommand(body)); } | command[cmd] - // /* error handling */ - // | (~(CHECK_SYNTH_TOK))=> token=. - // { std::string id = AntlrInput::tokenText($token); - // std::stringstream ss; - // ss << "Not a recognized SyGuS command: `" << id << "'"; - // PARSER_STATE->parseError(ss.str()); - // } ; +/** Reads a sygus grammar + * + * The resulting sygus datatype encoding the grammar is stored in ret. + * The argument sygus_vars indicates the sygus bound variable list, which is + * the argument list of the function-to-synthesize (or null if the grammar + * has bound variables). + * The argument fun is a unique identifier to avoid naming clashes for the + * datatypes constructed by this call. + */ +sygusGrammar[CVC4::Type & ret, + std::vector& sygus_vars, + std::string& fun] @declarations +{ + Type t; + std::string name; + unsigned startIndex = 0; + std::vector> sgts; + std::vector datatypes; + std::vector sorts; + std::vector> ops; + std::vector> cnames; + std::vector>> cargs; + std::vector allow_const; + std::vector> unresolved_gterm_sym; + std::map sygus_to_builtin; + std::map sygus_to_builtin_expr; +} + : LPAREN_TOK { PARSER_STATE->pushScope(); } + (LPAREN_TOK + symbol[name, CHECK_NONE, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED] { + std::stringstream ss; + ss << fun << "_" << name; + if (name == "Start") + { + startIndex = datatypes.size(); + } + std::string dname = ss.str(); + sgts.push_back(std::vector()); + sgts.back().push_back(CVC4::SygusGTerm()); + PARSER_STATE->pushSygusDatatypeDef(t, + dname, + datatypes, + sorts, + ops, + cnames, + cargs, + allow_const, + unresolved_gterm_sym); + Type unres_t; + if (!PARSER_STATE->isUnresolvedType(dname)) + { + // if not unresolved, must be undeclared + Debug("parser-sygus") << "Make unresolved type : " << dname + << std::endl; + PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); + unres_t = PARSER_STATE->mkUnresolvedType(dname); + } + else + { + Debug("parser-sygus") << "Get sort : " << dname << std::endl; + unres_t = PARSER_STATE->getSort(dname); + } + sygus_to_builtin[unres_t] = t; + Debug("parser-sygus") << "--- Read sygus grammar " << name + << " under function " << fun << "..." + << std::endl + << " type to resolve " << unres_t << std::endl + << " builtin type " << t << std::endl; + } + // Note the official spec for NTDef is missing the ( parens ) + // but they are necessary to parse SyGuS examples + LPAREN_TOK(sygusGTerm[sgts.back().back(), fun] { + sgts.back().push_back(CVC4::SygusGTerm()); + }) + + RPAREN_TOK { sgts.back().pop_back(); } RPAREN_TOK) + + RPAREN_TOK + { + unsigned numSTerms = sgts.size(); + Debug("parser-sygus") << "--- Process " << numSTerms << " sygus gterms..." + << std::endl; + for (unsigned i = 0; i < numSTerms; i++) + { + for (unsigned j = 0, size = sgts[i].size(); j < size; j++) + { + Type sub_ret; + PARSER_STATE->processSygusGTerm(sgts[i][j], + i, + datatypes, + sorts, + ops, + cnames, + cargs, + allow_const, + unresolved_gterm_sym, + sygus_vars, + sygus_to_builtin, + sygus_to_builtin_expr, + sub_ret); + } + } + // swap index if necessary + Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl; + unsigned ndatatypes = datatypes.size(); + for (unsigned i = 0; i < ndatatypes; i++) + { + Debug("parser-sygus") << "..." << datatypes[i].getName() + << " has builtin sort " << sorts[i] << std::endl; + } + Expr bvl; + if (!sygus_vars.empty()) + { + bvl = MK_EXPR(kind::BOUND_VAR_LIST, sygus_vars); + } + for (unsigned i = 0; i < ndatatypes; i++) + { + Debug("parser-sygus") << "...make " << datatypes[i].getName() + << " with builtin sort " << sorts[i] << std::endl; + if (sorts[i].isNull()) + { + PARSER_STATE->parseError( + "Internal error : could not infer " + "builtin sort for nested gterm."); + } + datatypes[i].setSygus(sorts[i], bvl, allow_const[i], false); + PARSER_STATE->mkSygusDatatype(datatypes[i], + ops[i], + cnames[i], + cargs[i], + unresolved_gterm_sym[i], + sygus_to_builtin); + } + PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, ops); + PARSER_STATE->popScope(); + Debug("parser-sygus") << "--- Make " << ndatatypes + << " mutual datatypes..." << std::endl; + for (unsigned i = 0; i < ndatatypes; i++) + { + Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName() + << std::endl; + } + std::vector datatypeTypes = + PARSER_STATE->mkMutualDatatypeTypes(datatypes); + ret = datatypeTypes[0]; + }; + // SyGuS grammar term. // // fun is the name of the synth-fun this grammar term is for. -- cgit v1.2.3