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 | |
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.
39 files changed, 498 insertions, 187 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 653eaca8f..b9e951f7b 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -213,9 +213,13 @@ int runCvc4(int argc, char* argv[], Options& opts) { } // if doing sygus, turn on CEGQI by default - if(opts[options::inputLanguage] == language::input::LANG_SYGUS && - !opts.wasSetByUser(options::ceGuidedInst)) { - opts.set(options::ceGuidedInst, true); + if(opts[options::inputLanguage] == language::input::LANG_SYGUS ){ + if( !opts.wasSetByUser(options::ceGuidedInst)) { + opts.set(options::ceGuidedInst, true); + } + if( !opts.wasSetByUser(options::dumpSynth)) { + opts.set(options::dumpSynth, true); + } } // Determine which messages to show based on smtcomp_mode and verbosity @@ -572,7 +576,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { // make sure out and err streams are flushed too *opts[options::out] << flush; *opts[options::err] << flush; - + #ifdef CVC4_DEBUG if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) { _exit(returnValue); 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, diff --git a/src/smt/options b/src/smt/options index 077acc6e9..7c725e508 100644 --- a/src/smt/options +++ b/src/smt/options @@ -37,7 +37,7 @@ option dumpProofs --dump-proofs bool :default false :link --proof output proofs after every UNSAT/VALID response option dumpInstantiations --dump-instantiations bool :default false output instantiations of quantified formulas after every UNSAT/VALID response -option dumpSynth --dump-synth bool :default false +option dumpSynth --dump-synth bool :read-write :default false output solution for synthesis conjectures after every UNSAT/VALID response option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 921583ed2..fa145813c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1465,6 +1465,13 @@ void SmtEngine::setDefaults() { if( !options::dtForceAssignment.wasSetByUser() ){ options::dtForceAssignment.set( true ); } + //try to remove ITEs from quantified formulas + if( !options::iteDtTesterSplitQuant.wasSetByUser() ){ + options::iteDtTesterSplitQuant.set( true ); + } + if( !options::iteLiftQuant.wasSetByUser() ){ + options::iteLiftQuant.set( quantifiers::ITE_LIFT_QUANT_MODE_ALL ); + } } if( options::intWfInduction() ){ if( !options::purifyTriggers.wasSetByUser() ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 045407bf0..e10ba0fef 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -37,14 +37,25 @@ CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_in void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { Assert( d_quant.isNull() ); Assert( q.getKind()==FORALL ); + d_assert_quant = q; + //register with single invocation if applicable + if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){ + d_ceg_si->initialize( qe, q ); + if( q!=d_ceg_si->d_quant ){ + //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant ); + //may have rewritten quantified formula (for invariant synthesis) + q = d_ceg_si->d_quant; + } + } d_quant = q; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) ); } + Trace("cegqi") << "Base quantified fm is : " << q << std::endl; //construct base instantiation d_base_inst = Rewriter::rewrite( qe->getInstantiation( q, d_candidates ) ); Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; - if( qe->getTermDatabase()->isQAttrSygus( q ) ){ + if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){ CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj ); Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; //store the inner variables for each disjunct @@ -59,10 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } } d_syntax_guided = true; - if( options::cegqiSingleInv() ){ - d_ceg_si->initialize( qe, q ); - } - }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){ + }else if( qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){ d_syntax_guided = false; }else{ Assert( false ); @@ -211,7 +219,7 @@ void CegInstantiation::assertNode( Node n ) { //d_guard_assertions[lit] = pol; d_conj->d_infeasible = !pol; } - if( lit==d_conj->d_quant ){ + if( lit==d_conj->d_assert_quant ){ d_conj->d_active = true; } } @@ -229,7 +237,7 @@ Node CegInstantiation::getNextDecisionRequest() { Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl; return d_conj->d_guard; } - + if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { @@ -251,6 +259,7 @@ Node CegInstantiation::getNextDecisionRequest() { void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Node q = conj->d_quant; + Node aq = conj->d_assert_quant; Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl; Trace("cegqi-engine-debug") << " * Candidate program/output symbol : "; for( unsigned i=0; i<conj->d_candidates.size(); i++ ){ @@ -263,7 +272,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( conj->d_ce_sk.empty() ){ Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; - if( getTermDatabase()->isQAttrSygus( q ) ){ + if( conj->d_syntax_guided ){ if( conj->d_ceg_si ){ std::vector< Node > lems; conj->d_ceg_si->check( lems ); @@ -303,7 +312,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { conj->d_ce_sk.push_back( std::vector< Node >() ); } std::vector< Node > ic; - ic.push_back( q.negate() ); + ic.push_back( aq.negate() ); std::vector< Node > d; collectDisjuncts( inst, d ); Assert( d.size()==conj->d_base_disj.size() ); @@ -334,7 +343,8 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Trace("cegqi-engine") << " ...find counterexample." << std::endl; } - }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ + }else{ + Assert( aq==q ); std::vector< Node > model_terms; if( getModelValues( conj, conj->d_candidates, model_terms ) ){ d_quantEngine->addInstantiation( q, model_terms, false ); @@ -497,11 +507,12 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { // out << "Solution:" << std::endl; //} for( unsigned i=0; i<d_conj->d_candidates.size(); i++ ){ + Node prog = d_conj->d_quant[0][i]; std::stringstream ss; - ss << d_conj->d_quant[0][i]; + ss << prog; std::string f(ss.str()); f.erase(f.begin()); - TypeNode tn = d_conj->d_quant[0][i].getType(); + TypeNode tn = prog.getType(); Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Assert( dt.isSygus() ); @@ -514,7 +525,34 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { }else{ if( !d_conj->d_candidate_inst[i].empty() ){ sol = d_conj->d_candidate_inst[i].back(); - status = 1; + //check if this was based on a template, if so, we must do reconstruction + if( d_conj->d_assert_quant!=d_conj->d_quant ){ + Trace("cegqi-inv") << "Sygus version of solution is : " << sol << ", type : " << sol.getType() << std::endl; + sol = getTermDatabase()->getTermDatabaseSygus()->sygusToBuiltin( sol, sol.getType() ); + Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() << std::endl; + std::vector< Node > subs; + Expr svl = dt.getSygusVarList(); + for( unsigned j=0; j<svl.getNumChildren(); j++ ){ + subs.push_back( Node::fromExpr( svl[j] ) ); + } + if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ + Node pre = d_conj->d_ceg_si->d_trans_pre[prog]; + pre = pre.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(), + subs.begin(), subs.end() ); + sol = NodeManager::currentNM()->mkNode( OR, sol, pre ); + }else if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ){ + Node post = d_conj->d_ceg_si->d_trans_post[prog]; + post = post.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(), + subs.begin(), subs.end() ); + sol = NodeManager::currentNM()->mkNode( AND, sol, post ); + } + Trace("cegqi-inv-debug") << "With template : " << sol << std::endl; + sol = Rewriter::rewrite( sol ); + Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl; + sol = d_conj->d_ceg_si->reconstructToSyntax( sol, tn, status ); + }else{ + status = 1; + } } } if( !(Trace.isOn("cegqi-stats")) ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 5f393626c..af3a19d62 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -35,7 +35,9 @@ public: context::CDO< bool > d_active; /** is conjecture infeasible */ context::CDO< bool > d_infeasible; - /** quantified formula */ + /** quantified formula asserted */ + Node d_assert_quant; + /** quantified formula (after processing) */ Node d_quant; /** guard */ Node d_guard; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index b7bbf8a93..ef2e3005e 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -810,6 +810,7 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { } //collect information about conjunctions bool singleInvocation = false; + bool invExtractPrePost = false; if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){ singleInvocation = true; //try to phrase as single invocation property @@ -826,7 +827,6 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ if( it2->second.size()>1 ){ singleInvocation = false; - break; }else if( it2->second.size()==1 ){ Node prog = it2->first; Node inv = it2->second[0]; @@ -840,15 +840,26 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { single_invoke_args[prog][k-1].push_back( arg ); } } + if( inv.getType().isBoolean() ){ + //conjunct defines pre and/or post conditions + if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ + invExtractPrePost = true; + } + } } } } } } - if( singleInvocation ){ + if( singleInvocation || invExtractPrePost ){ + //no value in extracting pre/post if we are single invocation + if( singleInvocation ){ + invExtractPrePost = false; + } Trace("cegqi-si") << "Property is single invocation with : " << std::endl; std::vector< Node > pbvs; std::vector< Node > new_vars; + std::map< Node, std::vector< Node > > prog_vars; std::map< Node, std::vector< Node > > new_assumptions; for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){ Assert( !it->second.empty() ); @@ -868,12 +879,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { Assert( !single_invoke_args[prog][k-1].empty() ); if( single_invoke_args[prog][k-1].size()==1 && single_invoke_args[prog][k-1][0].getKind()==BOUND_VARIABLE ){ invc.push_back( single_invoke_args[prog][k-1][0] ); + prog_vars[prog].push_back( single_invoke_args[prog][k-1][0] ); }else{ //introduce fresh variable, assign all Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" ); new_vars.push_back( v ); invc.push_back( v ); d_single_inv_arg_sk.push_back( v ); + prog_vars[prog].push_back( v ); for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){ Node arg = single_invoke_args[prog][k-1][i]; @@ -897,7 +910,6 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { } //construct the single invocation version of the property Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl; - //std::vector< Node > si_conj; Node pbvl; if( !pbvs.empty() ){ pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); @@ -906,6 +918,8 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { //should hold since we prevent miniscoping Assert( d_single_inv.isNull() ); std::vector< Node > conjuncts; + std::vector< Node > conjuncts_si_progs; + std::vector< Node > conjuncts_si_invokes; for( unsigned i=0; i<it->second.size(); i++ ){ Node c = it->second[i]; std::vector< Node > disj; @@ -917,17 +931,32 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { if( itp!=prog_invoke.end() ){ std::vector< Node > terms; std::vector< Node > subs; + std::vector< Node > progs; for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ - if( !it2->second.empty() ){ + if( it2->second.size()==1 ){ Node prog = it2->first; Node inv = it2->second[0]; Assert( it2->second.size()==1 ); terms.push_back( inv ); subs.push_back( d_single_inv_map[prog] ); + progs.push_back( prog ); Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl; } } - cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + if( singleInvocation ){ + cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + }else{ + cr = c; + if( invExtractPrePost ){ + if( terms.size()==1 ){ + conjuncts_si_progs.push_back( progs[0] ); + conjuncts_si_invokes.push_back( terms[0] ); + }else if( terms.size()>1 ){ + //abort when mixing multiple invariants? TODO + invExtractPrePost = false; + } + } + } }else{ cr = c; } @@ -941,6 +970,10 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ); curr = TermDb::simpleNegate( curr ); Trace("cegqi-si") << " " << curr; + if( invExtractPrePost && conjuncts.size()==conjuncts_si_progs.size() ){ + conjuncts_si_progs.push_back( Node::null() ); + conjuncts_si_invokes.push_back( Node::null() ); + } conjuncts.push_back( curr ); if( !it->first.isNull() ){ Trace("cegqi-si-debug") << " under " << it->first; @@ -948,75 +981,163 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { Trace("cegqi-si") << std::endl; } Assert( !conjuncts.empty() ); - //make the skolems for the existential - if( !it->first.isNull() ){ - std::vector< Node > vars; - std::vector< Node > sks; - for( unsigned j=0; j<it->first.getNumChildren(); j++ ){ - std::stringstream ss; - ss << "a_" << it->first[j]; - Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" ); - vars.push_back( it->first[j] ); - sks.push_back( v ); + //CASE 1 : rewrite based on a template for invariants + if( invExtractPrePost ){ + //for invariant synthesis + std::map< Node, bool > has_inv; + std::map< Node, std::vector< Node > > inv_pre_post[2]; + for( unsigned c=0; c<conjuncts.size(); c++ ){ + Node inv = conjuncts_si_invokes[c]; + Node prog = conjuncts_si_progs[c]; + Trace("cegqi-si-inv-debug") << "Conjunct #" << c << ": " << conjuncts[c] << std::endl; + if( !prog.isNull() ){ + Trace("cegqi-si-inv-debug") << "...has program " << prog << " invoked once: " << inv << std::endl; + std::vector< Node > curr_disj; + //find the polarity of the invocation : this determines pre vs. post + int pol = extractInvariantPolarity( conjuncts[c], inv, curr_disj, true ); + Trace("cegqi-si-inv-debug") << "...polarity is " << pol << std::endl; + if( ( pol==1 && !curr_disj.empty() ) || pol==0 ){ + //conjunct is part of pre/post condition : will add to template of invariant + Node nc = curr_disj.empty() ? NodeManager::currentNM()->mkConst( true ) : + ( curr_disj.size()==1 ? curr_disj[0] : NodeManager::currentNM()->mkNode( AND, curr_disj ) ); + nc = pol==0 ? nc : TermDb::simpleNegate( nc ); + Trace("cegqi-si-inv-debug") << " -> " << nc << " is " << ( pol==0 ? "pre" : "post" ) << "condition of invariant " << prog << "." << std::endl; + inv_pre_post[pol][prog].push_back( nc ); + has_inv[prog] = true; + } + } } - //substitute conjunctions - for( unsigned i=0; i<conjuncts.size(); i++ ){ - conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + Trace("cegqi-si-inv") << "Constructing invariant templates..." << std::endl; + //now, contruct the template for the invariant(s) + std::map< Node, Node > prog_templ; + for( std::map< Node, bool >::iterator iti = has_inv.begin(); iti != has_inv.end(); ++iti ){ + Node prog = iti->first; + Trace("cegqi-si-inv") << "...for " << prog << "..." << std::endl; + Trace("cegqi-si-inv") << " args : "; + for( unsigned j=0; j<prog_vars[prog].size(); j++ ){ + Node v = NodeManager::currentNM()->mkBoundVar( prog_vars[prog][j].getType() ); + d_prog_templ_vars[prog].push_back( v ); + Trace("cegqi-si-inv") << v << " "; + } + Trace("cegqi-si-inv") << std::endl; + Node pre = inv_pre_post[0][prog].empty() ? NodeManager::currentNM()->mkConst( false ) : + ( inv_pre_post[0][prog].size()==1 ? inv_pre_post[0][prog][0] : NodeManager::currentNM()->mkNode( OR, inv_pre_post[0][prog] ) ); + d_trans_pre[prog] = pre.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); + Node post = inv_pre_post[1][prog].empty() ? NodeManager::currentNM()->mkConst( true ) : + ( inv_pre_post[1][prog].size()==1 ? inv_pre_post[1][prog][0] : NodeManager::currentNM()->mkNode( AND, inv_pre_post[1][prog] ) ); + d_trans_post[prog] = post.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); + Trace("cegqi-si-inv") << " precondition : " << d_trans_pre[prog] << std::endl; + Trace("cegqi-si-inv") << " postcondition : " << d_trans_post[prog] << std::endl; + Node invariant = d_single_inv_app_map[prog]; + invariant = invariant.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); + Trace("cegqi-si-inv") << " invariant : " << invariant << std::endl; + //construct template + Node templ; + if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ + //templ = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] ); + templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ); + }else{ + Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ); + //templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) ); + templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ); + } + Trace("cegqi-si-inv") << " template : " << templ << std::endl; + prog_templ[prog] = templ; } - d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() ); - //substitute single invocation applications - for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ - Node n = itam->second; - d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); + Trace("cegqi-si-inv") << " body : " << bd << std::endl; + bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars ); + Trace("cegqi-si-inv-debug") << " templ-subs body : " << bd << std::endl; + //make inner existential + std::vector< Node > new_var_bv; + for( unsigned j=0; j<new_vars.size(); j++ ){ + new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( new_vars[j].getType() ) ); } - } - //ensure that this is a ground property - for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ - Node n = itam->second; - //check if all variables are arguments of this - std::vector< Node > n_args; - for( unsigned i=1; i<n.getNumChildren(); i++ ){ - n_args.push_back( n[i] ); + bd = bd.substitute( new_vars.begin(), new_vars.end(), new_var_bv.begin(), new_var_bv.end() ); + for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){ + new_var_bv.push_back( q[1][0][0][j] ); } - for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){ - if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){ - Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl; - //try to do variable elimination on d_single_inv_arg_sk[i] - if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){ - Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl; - d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 ); - i--; - }else{ - singleInvocation = false; - //exit( 57 ); + if( !new_var_bv.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_var_bv ); + bd = NodeManager::currentNM()->mkNode( FORALL, bvl, TermDb::simpleNegate( bd ) ).negate(); + } + //make outer universal + bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd ); + bd = Rewriter::rewrite( bd ); + Trace("cegqi-si-inv") << " rtempl-subs body : " << bd << std::endl; + d_quant = bd; + //CASE 2 : rewrite based on single invocation + }else{ + //make the skolems for the existential + if( !it->first.isNull() ){ + std::vector< Node > vars; + std::vector< Node > sks; + for( unsigned j=0; j<it->first.getNumChildren(); j++ ){ + std::stringstream ss; + ss << "a_" << it->first[j]; + Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" ); + vars.push_back( it->first[j] ); + sks.push_back( v ); + } + //substitute conjunctions + for( unsigned i=0; i<conjuncts.size(); i++ ){ + conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + } + d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() ); + //substitute single invocation applications + for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ + Node n = itam->second; + d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + } + } + //ensure that this is a ground property + for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ + Node n = itam->second; + //check if all variables are arguments of this + std::vector< Node > n_args; + for( unsigned i=1; i<n.getNumChildren(); i++ ){ + n_args.push_back( n[i] ); + } + for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){ + if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){ + Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl; + //try to do variable elimination on d_single_inv_arg_sk[i] + if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){ + Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl; + d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 ); + i--; + }else{ + singleInvocation = false; + //exit( 57 ); + } + break; } - break; } } - } - if( singleInvocation ){ - Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); - if( pbvl.isNull() ){ - d_single_inv = bd; - }else{ - d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); - } - Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; - /* - if( options::eMatching() && options::eMatching.wasSetByUser() ){ - Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv ); - std::vector< Node > patTerms; - std::vector< Node > exclude; - inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude ); - if( !patTerms.empty() ){ - Trace("cegqi-si-em") << "Triggers : " << std::endl; - for( unsigned i=0; i<patTerms.size(); i++ ){ - Trace("cegqi-si-em") << " " << patTerms[i] << std::endl; + if( singleInvocation ){ + Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); + if( pbvl.isNull() ){ + d_single_inv = bd; + }else{ + d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + } + Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; + /* + if( options::eMatching() && options::eMatching.wasSetByUser() ){ + Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv ); + std::vector< Node > patTerms; + std::vector< Node > exclude; + inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude ); + if( !patTerms.empty() ){ + Trace("cegqi-si-em") << "Triggers : " << std::endl; + for( unsigned i=0; i<patTerms.size(); i++ ){ + Trace("cegqi-si-em") << " " << patTerms[i] << std::endl; + } } } + */ } - */ } } } @@ -1146,9 +1267,66 @@ bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol, return false; } +int CegConjectureSingleInv::extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol ) { + if( n.getKind()==NOT ){ + return extractInvariantPolarity( n[0], inv, curr_disj, !pol ); + }else if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){ + int curr_pol = -1; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + int eipc = extractInvariantPolarity( n[i], inv, curr_disj, pol ); + if( eipc!=-1 ){ + if( curr_pol==-1 ){ + curr_pol = eipc; + }else{ + return -1; + } + }else{ + curr_disj.push_back( pol ? n[i] : TermDb::simpleNegate( n[i] ) ); + } + } + return curr_pol; + }else if( n==inv ){ + return pol ? 1 : 0; + }else{ + return -1; + } +} + +Node CegConjectureSingleInv::substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ) { + if( n.getKind()==APPLY_UF && n.getNumChildren()>0 ){ + std::map< Node, Node >::iterator it = prog_templ.find( n[0] ); + if( it!=prog_templ.end() ){ + std::vector< Node > children; + for( unsigned i=1; i<n.getNumChildren(); i++ ){ + children.push_back( n[i] ); + } + std::map< Node, std::vector< Node > >::iterator itv = prog_templ_vars.find( n[0] ); + Assert( itv!=prog_templ_vars.end() ); + Assert( children.size()==itv->second.size() ); + Node newc = it->second.substitute( itv->second.begin(), itv->second.end(), children.begin(), children.end() ); + return newc; + } + } + bool childChanged = false; + std::vector< Node > children; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nn = substituteInvariantTemplates( n[i], prog_templ, prog_templ_vars ); + children.push_back( nn ); + childChanged = childChanged || ( nn!=n[i] ); + } + if( childChanged ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), n.getOperator() ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + return n; + } +} + bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children, - std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, - std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) { + std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, + std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) { if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){ @@ -1371,7 +1549,12 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl; s = d_sol->simplifySolution( s, stn ); Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl; + return reconstructToSyntax( s, stn, reconstructed ); +} + +Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed ) { d_solution = s; + const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); //reconstruct the solution into sygus if necessary reconstructed = 0; @@ -1429,4 +1612,5 @@ bool CegConjectureSingleInv::needsCheck() { return true; } + }
\ No newline at end of file diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index f8e3879ac..f0d00b61c 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -111,6 +111,9 @@ private: bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ); bool doVariableElimination( Node v, std::vector< Node >& conjuncts ); bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status ); + //for recognizing templates for invariant synthesis + int extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol ); + Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ); //presolve void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ); void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); @@ -141,7 +144,7 @@ private: public: //lemmas produced std::vector< Node > d_lemmas_produced; - std::vector< std::vector< Node > > d_inst; + std::vector< std::vector< Node > > d_inst; private: std::vector< Node > d_curr_lemmas; //add instantiation @@ -156,6 +159,10 @@ public: Node d_quant; // single invocation version of quant Node d_single_inv; + // transition relation version per program + std::map< Node, Node > d_trans_pre; + std::map< Node, Node > d_trans_post; + std::map< Node, std::vector< Node > > d_prog_templ_vars; public: //get the single invocation lemma Node getSingleInvLemma( Node guard ); @@ -165,6 +172,8 @@ public: void check( std::vector< Node >& lems ); //get solution Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ); + //reconstruct to syntax + Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed ); // has ites bool hasITEs() { return d_has_ites; } // is single invocation diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 97ad3e8ea..af2d88e94 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -152,6 +152,15 @@ typedef enum { ITE_LIFT_QUANT_MODE_ALL, } IteLiftQuantMode; +typedef enum { + /** synthesize I( x ) */ + SYGUS_INV_TEMPL_MODE_NONE, + /** synthesize ( pre( x ) V I( x ) ) */ + SYGUS_INV_TEMPL_MODE_PRE, + /** synthesize ( post( x ) ^ I( x ) ) */ + SYGUS_INV_TEMPL_MODE_POST, +} SygusInvTemplMode; + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index ab0526471..5cb9062e4 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -32,7 +32,7 @@ option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuan ite lifting mode for quantified formulas option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true split variables occurring as conditions of ITE in quantifiers -option iteDtTesterSplitQuant --ite-dtt-split-quant bool :default false +option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false split ites with dt testers as conditions # Whether to CNF quantifier bodies # option cnfQuant --cnf-quant bool :default false @@ -240,6 +240,9 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true generalize based on content in global search space narrowing +option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h" + template mode for sygus invariant synthesis + # approach applied to general quantified formulas option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index c518813a0..4d2276621 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -217,6 +217,19 @@ none \n\ + Lift if-then-else in quantified formulas. \n\ \n\ "; +static const std::string sygusInvTemplHelp = "\ +Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ +\n\ +none \n\ ++ Synthesize invariant directly.\n\ +\n\ +pre \n\ ++ Synthesize invariant based on weakening of precondition .\n\ +\n\ +post \n\ ++ Synthesize invariant based on strengthening of postcondition. \n\ +\n\ +"; inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { @@ -443,6 +456,22 @@ inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string } } +inline SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "none" ) { + return SYGUS_INV_TEMPL_MODE_NONE; + } else if(optarg == "pre") { + return SYGUS_INV_TEMPL_MODE_PRE; + } else if(optarg == "post") { + return SYGUS_INV_TEMPL_MODE_POST; + } else if(optarg == "help") { + puts(sygusInvTemplHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --sygus-inv-templ: `") + + optarg + "'. Try --sygus-inv-templ help."); + } +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index fa0e211b3..c6115195d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -781,6 +781,7 @@ Node TermDb::getCounterexampleLiteral( Node f ){ } Node TermDb::getInstConstantNode( Node n, Node f ){ + Assert( d_inst_constants.find( f )!=d_inst_constants.end() ); return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]); } @@ -1754,6 +1755,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n ); if( it==d_sygus_to_builtin[tn].end() ){ + Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl; Assert( n.getKind()==APPLY_CONSTRUCTOR ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); unsigned i = Datatype::indexOf( n.getOperator().toExpr() ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ccbbd5bd5..54f2a16fe 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -754,6 +754,7 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){ } Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) { + d_term_db->makeInstantiationConstantsFor( f ); return getInstantiation( f, d_term_db->d_inst_constants[f], terms ); } diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy index 5d8cd8752..56a30b210 100644 --- a/test/regress/regress0/sygus/array_search_2.sy +++ b/test/regress/regress0/sygus/array_search_2.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy index 48b5c8a4d..f6c0320e2 100644 --- a/test/regress/regress0/sygus/array_sum_2_5.sy +++ b/test/regress/regress0/sygus/array_sum_2_5.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy index 15567b0a8..46dbd2981 100644 --- a/test/regress/regress0/sygus/commutative.sy +++ b/test/regress/regress0/sygus/commutative.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index 0d753bdf1..428cb2adc 100644 --- a/test/regress/regress0/sygus/const-var-test.sy +++ b/test/regress/regress0/sygus/const-var-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy index ddc12a6a9..0059f6947 100644 --- a/test/regress/regress0/sygus/constant.sy +++ b/test/regress/regress0/sygus/constant.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy index dbf415986..e5448d626 100644 --- a/test/regress/regress0/sygus/dup-op.sy +++ b/test/regress/regress0/sygus/dup-op.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-cegqi-si +; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ Con Con) (+ Start Start) x)) diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy index 52a72c07d..cd129385e 100644 --- a/test/regress/regress0/sygus/enum-test.sy +++ b/test/regress/regress0/sygus/enum-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (define-sort D (Enum (a b))) (define-fun f ((x D)) Int (ite (= x D::a) 3 7)) diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy index a58bc2f64..2e6c6ef81 100644 --- a/test/regress/regress0/sygus/hd-01-d1-prog.sy +++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic BV) @@ -8,12 +8,12 @@ (synth-fun f ((x (BitVec 32))) (BitVec 32) ((Start (BitVec 32) ((bvand Start Start) (bvsub Start Start) - (bvor Start Start) - (bvadd Start Start) - (bvxor Start Start) + (bvor Start Start) + (bvadd Start Start) + (bvxor Start Start) x - #x00000000 - #xFFFFFFFF + #x00000000 + #xFFFFFFFF #x00000001)))) (declare-var x (BitVec 32)) diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy index 6e1610337..b07be0e98 100644 --- a/test/regress/regress0/sygus/icfp_28_10.sy +++ b/test/regress/regress0/sygus/icfp_28_10.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic BV) @@ -14,14 +14,14 @@ (Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) (shl1 Start) - (shr1 Start) - (shr4 Start) - (shr16 Start) - (bvand Start Start) - (bvor Start Start) - (bvxor Start Start) - (bvadd Start Start) - (if0 Start Start Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) )) ) ) diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy index dda8e0ed5..aafbbd987 100644 --- a/test/regress/regress0/sygus/inv-example.sy +++ b/test/regress/regress0/sygus/inv-example.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) (declare-primed-var x Int) diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index 046d074d9..4bae90b00 100644 --- a/test/regress/regress0/sygus/let-ringer.sy +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (define-fun g ((x Int)) Int (ite (= x 1) 15 19)) (synth-fun f ((x Int)) Int diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy index daca906a2..71cd27e8f 100644 --- a/test/regress/regress0/sygus/let-simp.sy +++ b/test/regress/regress0/sygus/let-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int ((Start Int (x diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy index 4fc515353..dec4594d7 100644 --- a/test/regress/regress0/sygus/max.sy +++ b/test/regress/regress0/sygus/max.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy index 24d49ee4e..6d185ba3f 100644 --- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy +++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy @@ -1,13 +1,13 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun addExpr1 ((x Int) (y Int)) Int ((Start Int (x y - 0 - 1 + 0 + 1 (+ Start Start) (- Start Start) )) @@ -16,8 +16,8 @@ (synth-fun addExpr2 ((x Int) (y Int)) Int ((Start Int (x y - 0 - 1 + 0 + 1 (+ Start Start) (- Start Start) )) diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy index bd7c79e3e..9065a1025 100644 --- a/test/regress/regress0/sygus/nflat-fwd-3.sy +++ b/test/regress/regress0/sygus/nflat-fwd-3.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ (+ Con Con) Con) x)) diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy index 0f9d46215..d211d475b 100644 --- a/test/regress/regress0/sygus/nflat-fwd.sy +++ b/test/regress/regress0/sygus/nflat-fwd.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x)) diff --git a/test/regress/regress0/sygus/no-flat-simp.sy b/test/regress/regress0/sygus/no-flat-simp.sy index 81f90e2aa..cb284b180 100755 --- a/test/regress/regress0/sygus/no-flat-simp.sy +++ b/test/regress/regress0/sygus/no-flat-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy index cc3855ad1..4b3fa22e6 100644 --- a/test/regress/regress0/sygus/no-syntax-test-bool.sy +++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy index 21788426c..86b60638b 100644 --- a/test/regress/regress0/sygus/no-syntax-test-no-si.sy +++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy index 95f9b7c11..b95f31aa7 100644 --- a/test/regress/regress0/sygus/no-syntax-test.sy +++ b/test/regress/regress0/sygus/no-syntax-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy index c4fbd1c17..03d180634 100644 --- a/test/regress/regress0/sygus/parity-AIG-d0.sy +++ b/test/regress/regress0/sygus/parity-AIG-d0.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic BV) (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy index a8da13742..1545f86cd 100644 --- a/test/regress/regress0/sygus/tl-type.sy +++ b/test/regress/regress0/sygus/tl-type.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-cegqi-si +; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int (Term (+ Start Start))) diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy index 24b0f2c09..7f84ce06c 100644 --- a/test/regress/regress0/sygus/twolets1.sy +++ b/test/regress/regress0/sygus/twolets1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) ;; f1 is x plus 2 ;; f2 is 2x plus 5 @@ -7,27 +7,27 @@ (define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z)) (synth-fun f1 ((x Int)) Int - ( - (Start Int ( - (let0 Intx CInt CInt) - ) - ) - (Intx Int (x)) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - - ) + ( + (Start Int ( + (let0 Intx CInt CInt) + ) + ) + (Intx Int (x)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) ) (synth-fun f2 ((x Int)) Int - ( - (Start Int (x - (let0 Intx Start CInt) - ) - ) + ( + (Start Int (x + (let0 Intx Start CInt) + ) + ) (Intx Int (x)) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) + ) ) diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy index c1066277e..91bab5ece 100644 --- a/test/regress/regress0/sygus/twolets2-orig.sy +++ b/test/regress/regress0/sygus/twolets2-orig.sy @@ -1,25 +1,25 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f1 ((x Int)) Int - ( - (Start Int ( - (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z)) - ) - ) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + ( + (Start Int ( + (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) + ) ) (synth-fun f2 ((x Int)) Int - ( - (Start Int (x - (let ((y Int Start) (z Int CInt)) (+ (+ y x) z)) - ) - ) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + ( + (Start Int (x + (let ((y Int Start) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) + ) ) (declare-var x1 Int) (declare-var x2 Int) diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy index b020c0bee..9886f6a7b 100644 --- a/test/regress/regress0/sygus/uminus_one.sy +++ b/test/regress/regress0/sygus/uminus_one.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((- 1))))) (declare-var x Int) diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy index dc39efd84..7c9d6c601 100644 --- a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy +++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun inv ((x Int)) Bool |