diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-25 16:40:54 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-25 16:40:54 +0200 |
commit | c0079b3110a81f2ff993b7f86782266380dd102e (patch) | |
tree | c39d61ecc3857ebe5af75bd41ef7c11353e0824a /src/parser | |
parent | 7dcb635088e73b508dbe00ae7fe08dae99968416 (diff) |
Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/post conditions. Dump synth by default in sygus, update regressions. Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 79 |
1 files changed, 51 insertions, 28 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b8c4793d4..9ee6d24b4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -517,7 +517,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin startIndex = -1; Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl; std::map< CVC4::Type, CVC4::Type > sygus_to_builtin; - + std::vector< Type > types; for( unsigned i=0; i<sygus_vars.size(); i++ ){ Type t = sygus_vars[i].getType(); @@ -525,13 +525,13 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin types.push_back( t ); } } - + //name of boolean sort std::stringstream ssb; ssb << fun << "_Bool"; std::string dbname = ssb.str(); Type unres_bt = mkUnresolvedType(ssb.str()); - + std::vector< Type > unres_types; for( unsigned i=0; i<types.size(); i++ ){ std::stringstream ss; @@ -700,7 +700,7 @@ void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& o // This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1) // This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms. -void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, +void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, @@ -708,14 +708,37 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, std::vector< bool >& allow_const, std::vector< std::vector< std::string > >& unresolved_gterm_sym, - 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>& sygus_vars, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, CVC4::Type& ret, bool isNested ){ if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){ Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index << std::endl; - //convert to UMINUS if one child of - + Kind oldKind; + Kind newKind = kind::UNDEFINED_KIND; + //convert to UMINUS if one child of MINUS if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){ - sgt.d_expr = getExprManager()->operatorOf(kind::UMINUS); + oldKind = kind::MINUS; + newKind = kind::UMINUS; + } + //convert to IFF if boolean EQUAL + if( sgt.d_expr==getExprManager()->operatorOf(kind::EQUAL) ){ + Type ctn = sgt.d_children[0].d_type; + std::map< CVC4::Type, CVC4::Type >::iterator it = sygus_to_builtin.find( ctn ); + if( it != sygus_to_builtin.end() && it->second.isBoolean() ){ + oldKind = kind::EQUAL; + newKind = kind::IFF; + } + } + if( newKind!=kind::UNDEFINED_KIND ){ + Expr newExpr = getExprManager()->operatorOf(newKind); + Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl; + sgt.d_expr = newExpr; + std::string oldName = kind::kindToString(oldKind); + std::string newName = kind::kindToString(newKind); + size_t pos = 0; + if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){ + sgt.d_name.replace(pos, oldName.length(), newName); + } } ops[index].push_back( sgt.d_expr ); cnames[index].push_back( sgt.d_name ); @@ -730,16 +753,16 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, int sub_dt_index = datatypes.size()-1; //process child Type sub_ret; - processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, + processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true ); //process the nested gterm (either pop the last datatype, or flatten the argument) - Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, + Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); cargs[index].back().push_back(tt); } //if let, must create operator if( sgt.d_gterm_type==SygusGTerm::gterm_let ){ - processSygusLetConstructor( sgt.d_let_vars, index, datatypes, sorts, ops, cnames, cargs, + processSygusLetConstructor( sgt.d_let_vars, index, datatypes, sorts, ops, cnames, cargs, sygus_vars, sygus_to_builtin, sygus_to_builtin_expr ); } }else if( sgt.d_gterm_type==SygusGTerm::gterm_constant ){ @@ -790,7 +813,7 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, unresolved_gterm_sym[index].push_back(sgt.d_name); } }else if( sgt.d_gterm_type==SygusGTerm::gterm_ignore ){ - + } } @@ -828,7 +851,7 @@ bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes, unresolved_gterm_sym.pop_back(); return true; } - + Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, @@ -836,7 +859,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st 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::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 "; @@ -907,13 +930,13 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st } void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, - int index, + int 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::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; @@ -953,30 +976,30 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, 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 ); - + 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()); - + //mark function as let constructor d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_define_args.begin(), let_define_args.end() ); d_sygus_let_func_to_body[let_func] = let_body; @@ -997,12 +1020,12 @@ void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusAr } }else{ for( unsigned i=0; i<e.getNumChildren(); i++ ){ - collectSygusLetArgs( e[i], sygusArgs, builtinArgs ); - } + collectSygusLetArgs( e[i], sygusArgs, builtinArgs ); + } } } -void Smt2::setSygusStartIndex( std::string& fun, int startIndex, +void Smt2::setSygusStartIndex( std::string& fun, int startIndex, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops ) { @@ -1093,7 +1116,7 @@ void Smt2::defineSygusFuns() { void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs, - std::vector<std::string>& unresolved_gterm_sym, + std::vector<std::string>& unresolved_gterm_sym, 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; @@ -1149,7 +1172,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, 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; std::stringstream ss; @@ -1206,7 +1229,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, } } } - + } void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, |