diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 221 |
1 files changed, 141 insertions, 80 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a72b0ac6e..7a681f327 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -21,6 +21,7 @@ #include "parser/parser.h" #include "parser/smt1/smt1.h" #include "parser/smt2/smt2_input.h" +#include "printer/sygus_print_callback.h" #include "smt/command.h" #include "util/bitvector.h" @@ -926,23 +927,15 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) { Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; - std::vector<std::string> df_name; - std::vector<CVC4::Expr> df_op; - std::vector< std::vector<Expr> > df_let_args; - std::vector< Expr > df_let_body; - //dt.mkSygusConstructors( ops, cnames, cargs, sygus_to_builtin, - // d_sygus_let_func_to_vars, d_sygus_let_func_to_body, d_sygus_let_func_to_num_input_vars, - // df_name, df_op, df_let_args, df_let_body ); Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; - for( int i=0; i<(int)cnames.size(); i++ ){ + for (unsigned i = 0, size = cnames.size(); i < size; i++) + { bool is_dup = false; bool is_dup_op = false; - Expr let_body; - std::vector< Expr > let_args; - unsigned let_num_input_args = 0; - for( int j=0; j<i; j++ ){ + for (unsigned j = 0; j < i; j++) + { if( ops[i]==ops[j] ){ is_dup_op = true; if( cargs[i].size()==cargs[j].size() ){ @@ -959,60 +952,122 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, } } } + Debug("parser-sygus") << "SYGUS CONS " << i << " : "; if( is_dup ){ - Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << " at " << i << std::endl; + Debug("parser-sygus") << "--> Duplicate gterm : " << ops[i] << std::endl; ops.erase( ops.begin() + i, ops.begin() + i + 1 ); cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 ); cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 ); i--; - }else if( is_dup_op ){ - Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] << " at " << i << std::endl; - //make into define-fun - std::vector<CVC4::Type> fsorts; - for( unsigned j=0; j<cargs[i].size(); j++ ){ - Type bt = sygus_to_builtin[cargs[i][j]]; - std::stringstream ss; - ss << dt.getName() << "_x_" << i << "_" << j; - Expr v = mkBoundVar(ss.str(), bt); - let_args.push_back( v ); - fsorts.push_back( bt ); - Debug("parser-sygus") << ": var " << i << " " << v << " with type " << bt << " from " << cargs[i][j] << std::endl; + } + else + { + std::shared_ptr<SygusPrintCallback> spc; + if (is_dup_op) + { + Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] + << std::endl; + // make into define-fun + std::vector<Type> ltypes; + for (unsigned j = 0, size = cargs[i].size(); j < size; j++) + { + ltypes.push_back(sygus_to_builtin[cargs[i][j]]); + } + std::vector<Expr> largs; + Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs); + + // make the let_body + std::vector<Expr> children; + if (ops[i].getKind() != kind::BUILTIN) + { + children.push_back(ops[i]); + } + children.insert(children.end(), largs.begin(), largs.end()); + Kind sk = ops[i].getKind() != kind::BUILTIN + ? kind::APPLY + : getExprManager()->operatorToKind(ops[i]); + Expr body = getExprManager()->mkExpr(sk, children); + // replace by lambda + ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); + Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; + // callback prints as the expression + spc = std::make_shared<printer::SygusExprPrintCallback>(body, largs); } - //make the let_body - std::vector< Expr > children; - if( ops[i].getKind() != kind::BUILTIN ){ - children.push_back( ops[i] ); + else + { + std::map<Expr, Expr>::iterator it = + d_sygus_let_func_to_body.find(ops[i]); + if (it != d_sygus_let_func_to_body.end()) + { + Debug("parser-sygus") << "--> Let expression " << ops[i] << std::endl; + Expr let_body = it->second; + std::vector<Expr> let_args = d_sygus_let_func_to_vars[ops[i]]; + unsigned let_num_input_args = + d_sygus_let_func_to_num_input_vars[ops[i]]; + // the operator is just the body for the arguments + std::vector<Type> ltypes; + for (unsigned j = 0, size = let_args.size(); j < size; j++) + { + ltypes.push_back(let_args[j].getType()); + } + std::vector<Expr> largs; + Expr lbvl = makeSygusBoundVarList(dt, i, ltypes, largs); + Expr sbody = let_body.substitute(let_args, largs); + ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, sbody); + Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; + // callback prints as a let expression + spc = std::make_shared<printer::SygusLetExprPrintCallback>( + let_body, let_args, let_num_input_args); + } + else if (ops[i].getType().isBitVector() && ops[i].isConst()) + { + Debug("parser-sygus") << "--> Bit-vector constant " << ops[i] << " (" + << cnames[i] << ")" << std::endl; + // Since there are multiple output formats for bit-vectors and + // we are required by sygus standards to print in the exact input + // format given by the user, we use a print callback to custom print + // the given name. + spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]); + } + else if (isDefinedFunction(ops[i])) + { + Debug("parser-sygus") << "--> Defined function " << ops[i] + << std::endl; + // turn f into (lammbda (x) (f x)) + // in a degenerate case, ops[i] may be a defined constant, + // in which case we do not replace by a lambda. + if (ops[i].getType().isFunction()) + { + std::vector<Type> ftypes = + static_cast<FunctionType>(ops[i].getType()).getArgTypes(); + std::vector<Expr> largs; + Expr lbvl = makeSygusBoundVarList(dt, i, ftypes, largs); + largs.insert(largs.begin(), ops[i]); + Expr body = getExprManager()->mkExpr(kind::APPLY, largs); + ops[i] = getExprManager()->mkExpr(kind::LAMBDA, lbvl, body); + Debug("parser-sygus") << " ...replace op : " << ops[i] + << std::endl; + } + else + { + ops[i] = getExprManager()->mkExpr(kind::APPLY, ops[i]); + Debug("parser-sygus") << " ...replace op : " << ops[i] + << std::endl; + } + // keep a callback to say it should be printed with the defined name + spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]); + } + else + { + Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl; + } } - children.insert( children.end(), let_args.begin(), let_args.end() ); - Kind sk = ops[i].getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(ops[i]); - Debug("parser-sygus") << ": replace " << ops[i] << " " << ops[i].getKind() << " " << sk << std::endl; - let_body = getExprManager()->mkExpr( sk, children ); - Debug("parser-sygus") << ": new body of function is " << let_body << std::endl; - - Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType()); - Debug("parser-sygus") << ": function type is " << ft << std::endl; + // must rename to avoid duplication std::stringstream ss; - ss << dt.getName() << "_df_" << i; - //replace operator and name - ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); + ss << dt.getName() << "_" << i << "_" << cnames[i]; cnames[i] = ss.str(); - // indicate we need a define function - df_name.push_back( ss.str() ); - df_op.push_back( ops[i] ); - df_let_args.push_back( let_args ); - df_let_body.push_back( let_body ); - - //d_sygus_defined_funs.push_back( ops[i] ); - //preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) ); - dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, 0 ); - }else{ - std::map< CVC4::Expr, CVC4::Expr >::iterator it = d_sygus_let_func_to_body.find( ops[i] ); - if( it!=d_sygus_let_func_to_body.end() ){ - let_body = it->second; - let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() ); - let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]]; - } - dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args ); + // add the sygus constructor + dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc); } } @@ -1030,28 +1085,25 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, //identity element Type bt = dt.getSygusType(); Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl; + std::stringstream ss; - ss << t << "_x_id"; - Expr let_body = mkBoundVar(ss.str(), bt); - std::vector< Expr > let_args; - let_args.push_back( let_body ); - //make the identity function - Type ft = getExprManager()->mkFunctionType(bt, bt); - std::stringstream ssid; - ssid << unresolved_gterm_sym[i] << "_id"; - Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); - // indicate we need a define function - df_name.push_back( ssid.str() ); - df_op.push_back( id_op ); - df_let_args.push_back( let_args ); - df_let_body.push_back( let_body ); - - //d_sygus_defined_funs.push_back( id_op ); - //preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) ); + ss << t << "_x"; + Expr var = mkBoundVar(ss.str(), bt); + std::vector<Expr> lchildren; + lchildren.push_back( + getExprManager()->mkExpr(kind::BOUND_VAR_LIST, var)); + lchildren.push_back(var); + Expr id_op = getExprManager()->mkExpr(kind::LAMBDA, lchildren); + + // empty sygus callback (should not be printed) + std::shared_ptr<SygusPrintCallback> sepc = + std::make_shared<printer::SygusEmptyPrintCallback>(); + //make the sygus argument list std::vector< Type > id_carg; id_carg.push_back( t ); - dt.addSygusConstructor( id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 ); + dt.addSygusConstructor(id_op, unresolved_gterm_sym[i], id_carg, sepc); + //add to operators ops.push_back( id_op ); } @@ -1060,12 +1112,21 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, } } } - - - for( unsigned i=0; i<df_name.size(); i++ ){ - d_sygus_defined_funs.push_back( df_op[i] ); - preemptCommand( new DefineFunctionCommand(df_name[i], df_op[i], df_let_args[i], df_let_body[i]) ); +} + +Expr Smt2::makeSygusBoundVarList(Datatype& dt, + unsigned i, + const std::vector<Type>& ltypes, + std::vector<Expr>& lvars) +{ + for (unsigned j = 0, size = ltypes.size(); j < size; j++) + { + std::stringstream ss; + ss << dt.getName() << "_x_" << i << "_" << j; + Expr v = mkBoundVar(ss.str(), ltypes[j]); + lvars.push_back(v); } + return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars); } const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) { |