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]
}
// 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; i<datatypes.size(); i++ ){
PARSER_STATE->mkSygusDefaultGrammar( 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<datatypes.size(); i++ ){
+ Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName() << std::endl;
+ }
seq = new CommandSequence();
std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes);
seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
std::vector< std::vector<CVC4::Expr> >& ops,
std::vector< std::vector<std::string> >& cnames,
std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
- std::vector<CVC4::Expr>& sygus_vars, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, bool& allow_const, CVC4::Type& ret, int gtermType]
+ std::vector<CVC4::Expr>& 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;
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]
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]
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
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++;
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++;
}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."));
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);
std::vector< std::vector<CVC4::Expr> >& ops,
std::vector< std::vector<std::string> >& 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() ){
}
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<cargs[sub_dt_index][0].size(); i++ ){
- 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;
- children.push_back( mkVar("x", bt) );
+ std::map< CVC4::Type, CVC4::Expr >::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;
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<CVC4::Expr> >& ops,
+ std::vector< std::vector<std::string> >& cnames,
+ std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
+ std::vector<CVC4::Expr>& 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<cargs[index][dindex].size(); i++ ){
+ Debug("parser-sygus") << " " << i << " : " << cargs[index][dindex][i] << std::endl;
+ if( i+1==cargs[index][dindex].size() ){
+ std::map< CVC4::Type, CVC4::Expr >::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<let_vars.size(); i++ ){
+ Debug("parser-sygus") << " let var " << i << " : " << let_vars[i] << " " << let_vars[i].getType() << std::endl;
+ let_define_args.push_back( let_vars[i] );
+ }
+ Debug("parser-sygus") << "index = " << index << ", start index = " << start_index << ", #Current datatypes = " << datatypes.size() << std::endl;
+ for( unsigned i=start_index; i<datatypes.size(); i++ ){
+ Debug("parser-sygus") << " datatype " << i << " : " << datatypes[i].getName() << ", #cons = " << cargs[i].size() << std::endl;
+ if( !cargs[i].empty() ){
+ Debug("parser-sygus") << " operator 0 is " << ops[i][0] << std::endl;
+ Debug("parser-sygus") << " cons 0 has " << cargs[i][0].size() << " sub fields." << std::endl;
+ for( unsigned j=0; j<cargs[i][0].size(); j++ ){
+ Type bt = sygus_to_builtin[cargs[i][0][j]];
+ Debug("parser-sygus") << " cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl;
+ }
+ }
+ }
+ //last argument is the return, pop
+ cargs[index][dindex].pop_back();
+ collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );
+
+ Debug("parser-sygus") << "Make define-fun with " << cargs[index][dindex].size() << " arguments..." << std::endl;
+ std::vector<CVC4::Type> fsorts;
+ for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
+ Debug("parser-sygus") << " " << i << " : " << let_define_args[i] << " " << let_define_args[i].getType() << " " << cargs[index][dindex][i] << std::endl;
+ fsorts.push_back(let_define_args[i].getType());
+ }
+
+ Type ft = getExprManager()->mkFunctionType(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<e.getNumChildren(); i++ ){
+ collectSygusLetArgs( e[i], sygusArgs, builtinArgs );
+ }
+ }
+}
+
void Smt2::defineSygusFuns() {
// only define each one once
projects / cvc5.git / commitdiff