Expr expr, expr2;
Type t, range;
std::vector<Expr> terms;
- std::vector<Type> sorts;
std::vector<Expr> sygus_vars;
std::vector<std::pair<std::string, Type> > sortedVarNames;
SExpr sexpr;
std::unique_ptr<CVC4::CommandSequence> seq;
- std::vector< std::vector< CVC4::SygusGTerm > > sgts;
- std::vector< CVC4::Datatype > datatypes;
- std::vector< std::vector<Expr> > 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(); }
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; i<sgts.size(); i++ ){
- for( unsigned j=0; j<sgts[i].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;
- for( unsigned i=0; i<datatypes.size(); i++ ){
- Debug("parser-sygus") << "..." << datatypes[i].getName()
- << " has builtin sort " << sorts[i]
- << std::endl;
- }
- for( unsigned i=0; i<datatypes.size(); 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], 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<datatypes.size(); i++ ){
- Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName() << std::endl;
- }
- std::vector<DatatypeType> 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 */
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<CVC4::Expr>& sygus_vars,
+ std::string& fun] @declarations
+{
+ Type t;
+ std::string name;
+ unsigned startIndex = 0;
+ std::vector<std::vector<CVC4::SygusGTerm>> sgts;
+ std::vector<CVC4::Datatype> datatypes;
+ std::vector<Type> sorts;
+ std::vector<std::vector<Expr>> 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;
+ std::map<CVC4::Type, CVC4::Type> sygus_to_builtin;
+ std::map<CVC4::Type, CVC4::Expr> 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<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
+ {
+ 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<DatatypeType> datatypeTypes =
+ PARSER_STATE->mkMutualDatatypeTypes(datatypes);
+ ret = datatypeTypes[0];
+ };
+
// SyGuS grammar term.
//
// fun is the name of the synth-fun this grammar term is for.
projects / cvc5.git / commitdiff