summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r--src/parser/smt2/smt2.cpp118
1 files changed, 112 insertions, 6 deletions
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<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() ){
@@ -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<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;
@@ -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<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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback