From 6417016a38e24b09bc062a4bd4b0a5945fbcc0ec Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 10 Jun 2015 11:26:51 +0200 Subject: [PATCH] Parse support for sygus LetGTerm. --- src/parser/smt2/Smt2.g | 98 ++++++++++++------- src/parser/smt2/smt2.cpp | 118 +++++++++++++++++++++-- src/parser/smt2/smt2.h | 20 +++- src/theory/quantifiers/term_database.cpp | 2 + 4 files changed, 198 insertions(+), 40 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 45630d2cd..54938a686 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -498,9 +498,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::vector< std::vector< std::vector< CVC4::Type > > > cargs; bool allow_const = false; bool read_syntax = false; - int sygus_dt_index; + int sygus_dt_index = 0; Type sygus_ret; std::map< CVC4::Type, CVC4::Type > sygus_to_builtin; + std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] @@ -620,7 +621,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] } // Note the official spec for NTDef is missing the ( parens ) // but they are necessary to parse SyGuS examples - LPAREN_TOK sygusGTerm[sygus_dt_index, datatypes, sorts, fun, ops, cnames, cargs, sygus_vars, sygus_to_builtin, allow_const, sygus_ret, -1]+ RPAREN_TOK + LPAREN_TOK sygusGTerm[sygus_dt_index, datatypes, sorts, fun, ops, cnames, cargs, sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, allow_const, sygus_ret, -1]+ RPAREN_TOK RPAREN_TOK { Debug("parser-sygus") << "Making sygus datatypes..." << std::endl; for( unsigned i=sygus_dt_index; imkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars ); } PARSER_STATE->popScope(); - Debug("parser-sygus") << "Make mutual datatypes..." << std::endl; + Debug("parser-sygus") << "Make " << datatypes.size() << " mutual datatypes..." << std::endl; + for( unsigned i=0; i datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes); seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes)); @@ -735,7 +739,9 @@ sygusGTerm[int index, std::vector< std::vector >& ops, std::vector< std::vector >& cnames, std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector& sygus_vars, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, bool& allow_const, CVC4::Type& ret, int gtermType] + std::vector& sygus_vars, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, + bool& allow_const, CVC4::Type& ret, int gtermType] @declarations { std::string name; Kind k; @@ -745,12 +751,17 @@ sygusGTerm[int index, std::string sname; // 0 builtin operator, 1 defined operator, 2 any constant, 3 any variable, 4 ignore, 5 let, -1 none int sub_gtermType = -1; - bool sub_allow_const; + bool sub_allow_const = false; Type sub_ret; - int sub_dt_index; + int sub_dt_index = -1; std::string sub_dname; Type null_type; + Expr null_expr; std::vector< Expr > let_vars; + int let_start_index = -1; + int let_end_index = -1; + int let_end_arg_index = -1; + Expr let_func; } : LPAREN_TOK ( builtinOp[k] @@ -759,31 +770,41 @@ sygusGTerm[int index, if( k==CVC4::kind::BITVECTOR_UDIV ){ k = CVC4::kind::BITVECTOR_UDIV_TOTAL; } - ops[index].push_back(EXPR_MANAGER->operatorOf(k)); name = kind::kindToString(k); sub_gtermType = 0; + ops[index].push_back(EXPR_MANAGER->operatorOf(k)); + cnames[index].push_back( name ); } - /* TODO - | LET_TOK { sub_gtermType = 5; } - LPAREN_TOK { PARSER_STATE->pushScope(true); } - ( LPAREN_TOK + | LET_TOK LPAREN_TOK { + name = std::string("let"); + sub_gtermType = 5; + ops[index].push_back( null_expr ); + cnames[index].push_back( name ); + cargs[index].push_back( std::vector< CVC4::Type >() ); + PARSER_STATE->pushScope(true); + let_start_index = datatypes.size(); + } + ( LPAREN_TOK symbol[sname,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] { - Expr v = PARSER_STATE->mkVar(sname,t); + Expr v = PARSER_STATE->mkBoundVar(sname,t); let_vars.push_back( v ); std::stringstream ss; - ss << datatypes[index].getName() << "_let_arg_" << let_vars.size(); + ss << datatypes[index].getName() << "_let_var_" << let_vars.size(); sub_dname = ss.str(); PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs ); sub_dt_index = datatypes.size()-1; sub_ret = null_type; } - sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,sygus_vars,sygus_to_builtin,sub_allow_const,sub_ret,sub_gtermType] { + sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_allow_const,sub_ret,sub_gtermType] { Debug("parser-sygus") << "Process argument #" << let_vars.size() << "..." << std::endl; - Type t = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, sygus_to_builtin, sub_ret ); + Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); + cargs[index].back().push_back(tt); + } + RPAREN_TOK )+ RPAREN_TOK { + let_end_index = datatypes.size(); + let_end_arg_index = cargs[index].back().size(); } - RPAREN_TOK )+ RPAREN_TOK - */ | SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED] { sub_gtermType = 2; allow_const = true;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; } | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] @@ -800,8 +821,9 @@ sygusGTerm[int index, if( k==CVC4::kind::BITVECTOR_UDIV ){ k = CVC4::kind::BITVECTOR_UDIV_TOTAL; } - ops[index].push_back(EXPR_MANAGER->operatorOf(k)); name = kind::kindToString(k); + ops[index].push_back(EXPR_MANAGER->operatorOf(k)); + cnames[index].push_back( name ); sub_gtermType = 0; }else{ // what is this sygus term trying to accomplish here, if the @@ -813,17 +835,17 @@ sygusGTerm[int index, PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); } ops[index].push_back( PARSER_STATE->getVariable(name) ); + cnames[index].push_back( name ); sub_gtermType = 1; } } ) - { if( sub_gtermType<=1 ){ - cnames[index].push_back( name ); - } - cargs[index].push_back( std::vector< CVC4::Type >() ); - Debug("parser-sygus") << "Read arguments under " << name << ", gtermType = " << sub_gtermType << std::endl; - if( !ops[index].empty() ){ - Debug("parser-sygus") << "Operator " << ops[index].back() << std::endl; + { Debug("parser-sygus") << "Read arguments under " << name << ", gtermType = " << sub_gtermType << std::endl; + if( sub_gtermType!=5 ){ + cargs[index].push_back( std::vector< CVC4::Type >() ); + if( !ops[index].empty() ){ + Debug("parser-sygus") << "Operator " << ops[index].back() << std::endl; + } } //add datatype definition for argument count++; @@ -834,10 +856,9 @@ sygusGTerm[int index, sub_dt_index = datatypes.size()-1; sub_ret = null_type; } - ( //symbol[sname,CHECK_NONE,SYM_VARIABLE] - sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,sygus_vars,sygus_to_builtin,sub_allow_const,sub_ret,sub_gtermType] + ( sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_allow_const,sub_ret,sub_gtermType] { Debug("parser-sygus") << "Process argument #" << count << "..." << std::endl; - Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, sygus_to_builtin, sub_ret ); + Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); cargs[index].back().push_back(tt); //add next datatype definition for argument count++; @@ -883,6 +904,19 @@ sygusGTerm[int index, }else if( sub_gtermType==4 ){ //local variable, TODO? } + }else if( sub_gtermType==5 ){ + if( (cargs[index].back().size()-let_end_arg_index)!=1 ){ + PARSER_STATE->parseError(std::string("Must provide single body for let Sygus constructor.")); + } + PARSER_STATE->processSygusLetConstructor( let_vars, index, let_start_index, datatypes, sorts, ops, cnames, cargs, + sygus_vars, sygus_to_builtin, sygus_to_builtin_expr ); + PARSER_STATE->popScope(); + //remove datatypes defining body + //while( (int)datatypes.size()>let_end_index ){ + // Debug("parser-sygus") << "Removing let body datatype " << datatypes[datatypes.size()-1].getName() << std::endl; + // PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs ); + //} + //Debug("parser-sygus") << "Done let body datatypes" << std::endl; }else{ if( cargs[index].back().empty() ){ PARSER_STATE->parseError(std::string("Must provide argument for Sygus constructor.")); @@ -925,11 +959,9 @@ sygusGTerm[int index, cargs[index].push_back( std::vector< CVC4::Type >() ); }else{ //prepend function name to base sorts when reading an operator - if( gtermType<=1 ){ - std::stringstream ss; - ss << fun << "_" << name; - name = ss.str(); - } + std::stringstream ss; + ss << fun << "_" << name; + name = ss.str(); if( PARSER_STATE->isDeclared(name, SYM_SORT) ){ Debug("parser-sygus") << "Sygus grammar " << fun << " : nested sort " << name << std::endl; ret = PARSER_STATE->getSort(name); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 6e5e57355..101e26746 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -649,7 +649,8 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st std::vector< std::vector >& ops, std::vector< std::vector >& cnames, std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, Type sub_ret ) { + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, + std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) { Type t = sub_ret; Debug("parser-sygus") << "Argument is "; if( t.isNull() ){ @@ -662,24 +663,36 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st } Expr sop = ops[sub_dt_index][0]; Type curr_t; - if( sop.getKind() != kind::BUILTIN && sop.isConst() ){ + if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || sop.getNumChildren()==0 ) ){ curr_t = sop.getType(); - Debug("parser-sygus") << ": it is constant with type " << sop.getType() << std::endl; + Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << std::endl; + sygus_to_builtin_expr[t] = sop; + d_sygus_bound_var_type[sop] = t; }else{ std::vector< Expr > children; if( sop.getKind() != kind::BUILTIN ){ children.push_back( sop ); } for( unsigned i=0; i::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] ); + if( it==sygus_to_builtin_expr.end() ){ + Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]]; + Debug("parser-sygus") << ": type elem " << i << " " << cargs[sub_dt_index][0][i] << " " << bt << std::endl; + std::stringstream ss; + ss << t << "_x_" << i; + Expr bv = mkBoundVar(ss.str(), bt); + children.push_back( bv ); + d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i]; + }else{ + children.push_back( it->second ); + } } Kind sk = sop.getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(sop); Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl; Expr e = getExprManager()->mkExpr( sk, children ); Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl; curr_t = e.getType(); + sygus_to_builtin_expr[t] = e; } sorts[sub_dt_index] = curr_t; sygus_to_builtin[t] = curr_t; @@ -693,6 +706,99 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st return t; } +void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, + int index, int start_index, + std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Type>& sorts, + std::vector< std::vector >& ops, + std::vector< std::vector >& cnames, + std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector& sygus_vars, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, + std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ) { + std::vector< CVC4::Expr > let_define_args; + Expr let_body; + int dindex = cargs[index].size()-1; + Debug("parser-sygus") << "Process let constructor for datatype " << datatypes[index].getName() << ", #subtypes = " << cargs[index][dindex].size() << std::endl; + for( unsigned i=0; i::iterator it = sygus_to_builtin_expr.find( cargs[index][dindex][i] ); + if( it!=sygus_to_builtin_expr.end() ){ + let_body = it->second; + }else{ + std::stringstream ss; + ss << datatypes[index].getName() << "_body"; + let_body = mkBoundVar(ss.str(), sygus_to_builtin[cargs[index][dindex][i]]); + d_sygus_bound_var_type[let_body] = cargs[index][dindex][i]; + } + } + } + Debug("parser-sygus") << std::endl; + Debug("parser-sygus") << "Body is " << let_body << std::endl; + Debug("parser-sygus") << "# let vars = " << let_vars.size() << std::endl; + for( unsigned i=0; i fsorts; + for( unsigned i=0; imkFunctionType(fsorts, let_body.getType()); + std::stringstream ss; + ss << datatypes[index].getName() << "_let"; + Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); + preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) ); + + ops[index].pop_back(); + ops[index].push_back( let_func ); + cnames[index].pop_back(); + cnames[index].push_back(ss.str()); + + //TODO : mark function as let constructor + d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_vars.begin(), let_vars.end() ); + d_sygus_let_func_to_body[let_func] = let_body; +} + + +void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ) { + if( e.getKind()==kind::BOUND_VARIABLE ){ + if( std::find( builtinArgs.begin(), builtinArgs.end(), e )==builtinArgs.end() ){ + builtinArgs.push_back( e ); + sygusArgs.push_back( d_sygus_bound_var_type[e] ); + if( d_sygus_bound_var_type[e].isNull() ){ + std::stringstream ss; + ss << "While constructing body of let gterm, can't map " << e << " to sygus type." << std::endl; + parseError(ss.str()); + } + } + }else{ + for( unsigned i=0; i >& ops, std::vector< std::vector >& cnames, std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, Type sub_ret ); + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, + std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ); + void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, + int index, int start_index, + std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Type>& sorts, + std::vector< std::vector >& ops, + std::vector< std::vector >& cnames, + std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector& sygus_vars, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, + std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ); + + void addSygusFun(const std::string& fun, Expr eval) { d_sygusFuns.push_back(std::make_pair(fun, eval)); } @@ -285,6 +298,11 @@ public: } private: + std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type; + std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars; + std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body; + + void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ); void addArithmeticOperators(); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 1082bed23..d57f52b35 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1612,6 +1612,7 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn ) { Node TermDbSygus::getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ) { return n; + /* TODO? if( n.getKind()==SKOLEM ){ std::map< Node, Node >::iterator its = subs.find( n ); if( its!=subs.end() ){ @@ -1644,6 +1645,7 @@ Node TermDbSygus::getSygusNormalized( Node n, std::map< TypeNode, int >& var_cou } return n; } + */ } Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm, bool do_post_norm ) { -- 2.30.2