diff options
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 170 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 9 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 657 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 68 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database_sygus.cpp | 46 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database_sygus.h | 24 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/cegar1.sy | 23 |
8 files changed, 351 insertions, 649 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 9ee79af1f..38247c84c 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -117,21 +117,29 @@ void CegConjecture::collectConstants( Node n, std::map< TypeNode, std::vector< N } } + void CegConjecture::assign( Node q ) { Assert( d_quant.isNull() ); Assert( q.getKind()==FORALL ); Trace("cegqi") << "CegConjecture : assign : " << q << std::endl; d_assert_quant = q; + + //register with single invocation if applicable + if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){ + d_ceg_si->initialize( d_assert_quant ); + } + + // convert to deep embedding and finalize single invocation here + // now, construct the grammar + Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl; std::map< TypeNode, std::vector< Node > > extra_cons; - Trace("cegqi") << "CegConjecture : collect constants..." << std::endl; if( options::sygusAddConstGrammar() ){ - std::map< Node, bool > cvisited; - collectConstants( q[1], extra_cons, cvisited ); - } - - Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl; - //convert to deep embedding + std::map< Node, bool > visited; + collectConstants( q[1], extra_cons, visited ); + } + bool has_ites = true; + bool is_syntax_restricted = false; std::vector< Node > qchildren; std::map< Node, Node > visited; std::map< Node, Node > synth_fun_vars; @@ -144,19 +152,43 @@ void CegConjecture::assign( Node q ) { // sfvl may be null for constant synthesis functions Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl; TypeNode tn; + std::stringstream ss; + ss << sf; if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){ tn = v.getType(); }else{ // make the default grammar - std::stringstream ss; - ss << sf; tn = d_qe->getTermDatabaseSygus()->mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons ); } + // if there is a template for this argument, make a sygus type on top of it + Node templ = d_ceg_si->getTemplate( sf ); + if( !templ.isNull() ){ + Node templ_arg = d_ceg_si->getTemplateArg( sf ); + Assert( !templ_arg.isNull() ); + if( Trace.isOn("cegqi-debug") ){ + Trace("cegqi-debug") << "Template for " << sf << " is : " << templ << " with arg " << templ_arg << std::endl; + Trace("cegqi-debug") << " embed this template as a grammar..." << std::endl; + } + tn = d_qe->getTermDatabaseSygus()->mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() ); + } d_qe->getTermDatabaseSygus()->registerSygusType( tn ); + // check grammar restrictions + if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){ + if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){ + has_ites = false; + } + } + Assert( tn.isDatatype() ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( dt.isSygus() ); + if( !dt.getSygusAllowAll() ){ + is_syntax_restricted = true; + } + // ev is the first-order variable corresponding to this synth fun - std::stringstream ss; - ss << "f" << sf; - Node ev = NodeManager::currentNM()->mkBoundVar( ss.str(), tn ); + std::stringstream ssf; + ssf << "f" << sf; + Node ev = NodeManager::currentNM()->mkBoundVar( ssf.str(), tn ); ebvl.push_back( ev ); synth_fun_vars[sf] = ev; Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl; @@ -168,19 +200,13 @@ void CegConjecture::assign( Node q ) { } q = NodeManager::currentNM()->mkNode( kind::FORALL, qchildren ); Trace("cegqi") << "CegConjecture : converted to embedding : " << q << std::endl; + d_quant = q; - //register with single invocation if applicable - if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInvMode()!=CEGQI_SI_MODE_NONE ){ - d_ceg_si->initialize( 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; - Assert( q.getKind()==kind::FORALL ); - } + // we now finalize the single invocation module, based on the syntax restrictions + if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){ + d_ceg_si->finishInit( is_syntax_restricted, has_ites ); } - d_quant = q; Assert( d_candidates.empty() ); std::vector< Node > vars; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ @@ -278,54 +304,22 @@ bool CegConjecture::isSingleInvocation() const { return d_ceg_si->isSingleInvocation(); } -bool CegConjecture::isFullySingleInvocation() { - return d_ceg_si->isFullySingleInvocation(); -} - bool CegConjecture::needsCheck( std::vector< Node >& lem ) { if( isSingleInvocation() && !d_ceg_si->needsCheck() ){ return false; }else{ bool value; - if( !isSingleInvocation() || isFullySingleInvocation() ){ - Assert( !getGuard().isNull() ); - // non or fully single invocation : look at guard only - if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) { - if( !value ){ - Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl; - return false; - } - }else{ - Assert( false ); + Assert( !getGuard().isNull() ); + // non or fully single invocation : look at guard only + if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) { + if( !value ){ + Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl; + return false; } }else{ - // not fully single invocation : infeasible if overall specification is infeasible - Assert( !d_ceg_si->d_full_guard.isNull() ); - if( d_qe->getValuation().hasSatValue( d_ceg_si->d_full_guard, value ) ) { - if( !value ){ - Trace("cegqi-nsi") << "NSI : found full specification is infeasible." << std::endl; - return false; - }else{ - Assert( !d_ceg_si->d_si_guard.isNull() ); - if( d_qe->getValuation().hasSatValue( d_ceg_si->d_si_guard, value ) ) { - if( !value ){ - if( !d_ceg_si->d_single_inv_exp.isNull() ){ - //this should happen infrequently : only if cegqi determines infeasibility of a false candidate before E-matching does - Trace("cegqi-nsi") << "NSI : current single invocation lemma was infeasible, block assignment upon which conjecture was based." << std::endl; - Node l = NodeManager::currentNM()->mkNode( OR, d_ceg_si->d_full_guard.negate(), d_ceg_si->d_single_inv_exp ); - lem.push_back( l ); - d_ceg_si->initializeNextSiConjecture(); - } - return false; - } - }else{ - Assert( false ); - } - } - }else{ - Assert( false ); - } + Assert( false ); } + return true; } } @@ -672,15 +666,8 @@ void CegInstantiation::assertNode( Node n ) { Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) { if( d_conj->isAssigned() ){ std::vector< Node > req_dec; - const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv(); - if( ! ceg_si->d_full_guard.isNull() ){ - req_dec.push_back( ceg_si->d_full_guard ); - } - //must decide ns guard before s guard - if( !ceg_si->d_ns_guard.isNull() ){ - req_dec.push_back( ceg_si->d_ns_guard ); - } req_dec.push_back( d_conj->getGuard() ); + // other decision requests should ask the conjecture for( unsigned i=0; i<req_dec.size(); i++ ){ bool value; if( !d_quantEngine->getValuation().hasSatValue( req_dec[i], value ) ) { @@ -942,49 +929,6 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { for( unsigned j=0; j<svl.getNumChildren(); j++ ){ subs.push_back( Node::fromExpr( svl[j] ) ); } - //bool templIsPost = false; - const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv(); - Node templ = ceg_si->getTemplate( prog ); - /* - if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ - const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv(); - if(ceg_si->d_trans_pre.find( prog ) != ceg_si->d_trans_pre.end()){ - templ = ceg_si->getTransPre(prog); - templIsPost = false; - } - }else if(options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST){ - const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv(); - if(ceg_si->d_trans_post.find(prog) != ceg_si->d_trans_post.end()){ - templ = ceg_si->getTransPost(prog); - templIsPost = true; - } - } - */ - Trace("cegqi-inv") << "Template is " << templ << std::endl; - if( !templ.isNull() ){ - TNode templa = ceg_si->getTemplateArg( prog ); - Assert( !templa.isNull() ); - std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog); - std::vector< Node > vars; - vars.insert( vars.end(), templ_vars.begin(), templ_vars.end() ); - Node vl = Node::fromExpr( dt.getSygusVarList() ); - Assert(vars.size() == subs.size()); - if( Trace.isOn("cegqi-inv-debug") ){ - for( unsigned j=0; j<vars.size(); j++ ){ - Trace("cegqi-inv-debug") << " subs : " << vars[j] << " -> " << subs[j] << std::endl; - } - } - //apply the substitution to the template - templ = templ.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus(); - sol = sygusDb->sygusToBuiltin( sol, sol.getType() ); - Trace("cegqi-inv") << "Builtin version of solution is : " - << sol << ", type : " << sol.getType() - << std::endl; - //sol = NodeManager::currentNM()->mkNode( templIsPost ? AND : OR, sol, templ ); - TNode tsol = sol; - sol = templ.substitute( templa, tsol ); - } if( sol==sygus_sol ){ sol = sygus_sol; status = 1; diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index c5c865ff9..fd34fc028 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -47,6 +47,7 @@ private: /** refinement lemmas */ std::vector< Node > d_refinement_lemmas; std::vector< Node > d_refinement_lemmas_base; +private: /** get embedding */ Node convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited ); /** collect constants */ @@ -79,8 +80,8 @@ public: bool needsRefinement(); void getCandidateList( std::vector< Node >& clist, bool forceOrig = false ); - bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values, - std::vector< Node >& lems ); + bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, + std::vector< Node >& candidate_values, std::vector< Node >& lems ); void doCegConjectureSingleInvCheck(std::vector< Node >& lems); void doCegConjectureCheck(std::vector< Node >& lems, std::vector< Node >& model_values); @@ -96,10 +97,6 @@ public: return d_ceg_si->reconstructToSyntax(s, stn, reconstructed, rconsSygus); } - std::vector<Node>& getProgTempVars(Node prog) { - return d_ceg_si->d_prog_templ_vars[prog]; - } - void recordInstantiation( std::vector< Node >& vs ) { Assert( vs.size()==d_candidates.size() ); for( unsigned i=0; i<vs.size(); i++ ){ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index f25d42284..2fa993b97 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -50,11 +50,11 @@ CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe, d_parent(p), d_sip(new SingleInvocationPartition), d_sol(new CegConjectureSingleInvSol(qe)), - d_ei(NULL), d_cosi(new CegqiOutputSingleInv(this)), d_cinst(NULL), d_c_inst_match_trie(NULL), - d_has_ites(true) { + d_has_ites(true), + d_single_invocation(false) { // third and fourth arguments set to (false,false) until we have solution // reconstruction for delta and infinity d_cinst = new CegInstantiator(d_qe, d_cosi, false, false); @@ -62,10 +62,6 @@ CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe, if (options::incrementalSolving()) { d_c_inst_match_trie = new inst::CDInstMatchTrie(qe->getUserContext()); } - - if (options::cegqiSingleInvPartial()) { - d_ei = new CegEntailmentInfer(qe, d_sip); - } } CegConjectureSingleInv::~CegConjectureSingleInv() { @@ -74,9 +70,6 @@ CegConjectureSingleInv::~CegConjectureSingleInv() { } delete d_cinst; delete d_cosi; - if (d_ei) { - delete d_ei; - } delete d_sol; // (new CegConjectureSingleInvSol(qe)), delete d_sip; // d_sip(new SingleInvocationPartition), } @@ -123,216 +116,150 @@ void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems } void CegConjectureSingleInv::initialize( Node q ) { + // can only register one quantified formula with this Assert( d_quant.isNull() ); - Assert( options::cegqiSingleInvMode()!=CEGQI_SI_MODE_NONE ); - //initialize data d_quant = q; - //process - Trace("cegqi-si") << "Initialize cegqi-si for " << q << std::endl; - // conj -> conj* - std::map< Node, std::vector< Node > > children; - // conj X prog -> inv* - std::map< Node, std::map< Node, std::vector< Node > > > prog_invoke; + // infer single invocation-ness std::vector< Node > progs; - std::map< Node, std::map< Node, bool > > contains; - bool is_syntax_restricted = false; + std::map< Node, std::vector< Node > > prog_vars; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - progs.push_back( q[0][i] ); - //check whether all types have ITE - TypeNode tn = q[0][i].getType(); - d_qe->getTermDatabaseSygus()->registerSygusType( tn ); - if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){ - if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){ - d_has_ites = false; - } - } - Assert( tn.isDatatype() ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Assert( dt.isSygus() ); - if( !dt.getSygusAllowAll() ){ - is_syntax_restricted = true; + Node v = q[0][i]; + Node sf = v.getAttribute(SygusSynthFunAttribute()); + progs.push_back( sf ); + Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute()); + for( unsigned j=0; j<sfvl.getNumChildren(); j++ ){ + prog_vars[sf].push_back( sfvl[j] ); } } - //abort if not aggressive - bool singleInvocation = true; - if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_USE && is_syntax_restricted ){ - singleInvocation = false; - Trace("cegqi-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl; - }else{ - Node qq = q[1]; + // compute single invocation partition + if( options::cegqiSingleInvMode()!=CEGQI_SI_MODE_NONE ){ + Node qq; if( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ){ qq = q[1][0][1]; }else{ - qq = TermDb::simpleNegate( qq ); + qq = TermDb::simpleNegate( q[1] ); } - //remove the deep embedding - std::map< Node, Node > visited; - std::vector< TypeNode > types; + //process the single invocation-ness of the property + d_sip->init( progs, qq ); + Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl; + d_sip->debugPrint( "cegqi-si" ); + + //map from program to bound variables std::vector< Node > order_vars; std::map< Node, Node > single_inv_app_map; - int type_valid = 0; - qq = removeDeepEmbedding( qq, progs, types, type_valid, visited ); - Trace("cegqi-si-debug") << "- Remove deep embedding, got : " << qq << ", type valid = " << type_valid << std::endl; - if( type_valid==0 ){ - std::vector< Node > prog_funcs; - for( unsigned j=0; j<progs.size(); j++ ){ - std::map< Node, Node >::iterator itns = d_nsi_op_map.find( progs[j] ); - if( itns != d_nsi_op_map.end() ){ - prog_funcs.push_back( itns->second ); - } - } - - //process the single invocation-ness of the property - d_sip->init( prog_funcs, qq ); - Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl; - d_sip->debugPrint( "cegqi-si" ); - //map from program to bound variables - for( unsigned j=0; j<progs.size(); j++ ){ - Node prog = progs[j]; - std::map< Node, Node >::iterator it_nsi = d_nsi_op_map.find( prog ); - if( it_nsi!=d_nsi_op_map.end() ){ - Node op = it_nsi->second; - std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( op ); - if( it_fov!=d_sip->d_func_fo_var.end() ){ - Node pv = it_fov->second; - Assert( d_sip->d_func_inv.find( op )!=d_sip->d_func_inv.end() ); - Node inv = d_sip->d_func_inv[op]; - single_inv_app_map[prog] = inv; - Trace("cegqi-si") << " " << pv << ", " << inv << " is associated with program " << prog << std::endl; - d_prog_to_sol_index[prog] = order_vars.size(); - order_vars.push_back( pv ); - }else{ - Trace("cegqi-si") << " " << prog << " has no fo var." << std::endl; - } - }else{ - //does not mention the function - Trace("cegqi-si") << " " << prog << " is not mentioned." << std::endl; - } + for( unsigned j=0; j<progs.size(); j++ ){ + Node prog = progs[j]; + std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( prog ); + if( it_fov!=d_sip->d_func_fo_var.end() ){ + Node pv = it_fov->second; + Assert( d_sip->d_func_inv.find( prog )!=d_sip->d_func_inv.end() ); + Node inv = d_sip->d_func_inv[prog]; + single_inv_app_map[prog] = inv; + Trace("cegqi-si") << " " << pv << ", " << inv << " is associated with program " << prog << std::endl; + d_prog_to_sol_index[prog] = order_vars.size(); + order_vars.push_back( pv ); + }else{ + Trace("cegqi-si") << " " << prog << " has no fo var." << std::endl; } - //reorder the variables - Assert( d_sip->d_func_vars.size()==order_vars.size() ); - d_sip->d_func_vars.clear(); - d_sip->d_func_vars.insert( d_sip->d_func_vars.begin(), order_vars.begin(), order_vars.end() ); - - //check if it is single invocation - if( !d_sip->d_conjuncts[1].empty() ){ - singleInvocation = false; - if( options::cegqiSingleInvPartial() ){ - //this enables partially single invocation techniques - d_nsingle_inv = d_sip->getNonSingleInvocation(); - d_nsingle_inv = TermDb::simpleNegate( d_nsingle_inv ); - d_full_inv = d_sip->getFullSpecification(); - d_full_inv = TermDb::simpleNegate( d_full_inv ); - singleInvocation = true; - }else if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ - //if we are doing invariant templates, then construct the template - Trace("cegqi-si") << "- Do transition inference..." << std::endl; - d_ti[q].process( qq ); - Trace("cegqi-inv") << std::endl; - std::map< Node, Node > prog_templ; - if( !d_ti[q].d_func.isNull() ){ - // map the program back via non-single invocation map - Assert( d_nsi_op_map_to_prog.find( d_ti[q].d_func )!=d_nsi_op_map_to_prog.end() ); - Node prog = d_nsi_op_map_to_prog[d_ti[q].d_func]; - Assert( d_prog_templ_vars[prog].empty() ); - d_prog_templ_vars[prog].insert( d_prog_templ_vars[prog].end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end() ); - d_trans_pre[prog] = d_ti[q].getComponent( 1 ); - d_trans_post[prog] = d_ti[q].getComponent( -1 ); - Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; - Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; - Node invariant = single_inv_app_map[prog]; - invariant = invariant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); - Trace("cegqi-inv") << " invariant : " << invariant << std::endl; - - //construct template - d_templ_arg[prog] = NodeManager::currentNM()->mkSkolem( "I", invariant.getType() ); - if( options::sygusInvAutoUnfold() ){ - if( d_ti[q].isComplete() ){ - Trace("cegqi-inv-auto-unfold") << "Automatic deterministic unfolding... " << std::endl; - // auto-unfold - DetTrace dt; - int init_dt = d_ti[q].initializeTrace( dt ); - if( init_dt==0 ){ - Trace("cegqi-inv-auto-unfold") << " Init : "; + } + //reorder the variables + Assert( d_sip->d_func_vars.size()==order_vars.size() ); + d_sip->d_func_vars.clear(); + d_sip->d_func_vars.insert( d_sip->d_func_vars.begin(), order_vars.begin(), order_vars.end() ); + + + //check if it is single invocation + if( !d_sip->d_conjuncts[1].empty() ){ + if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ + //if we are doing invariant templates, then construct the template + Trace("cegqi-si") << "- Do transition inference..." << std::endl; + d_ti[q].process( qq ); + Trace("cegqi-inv") << std::endl; + if( !d_ti[q].d_func.isNull() ){ + // map the program back via non-single invocation map + Node prog = d_ti[q].d_func; + std::vector< Node > prog_templ_vars; + prog_templ_vars.insert( prog_templ_vars.end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end() ); + d_trans_pre[prog] = d_ti[q].getComponent( 1 ); + d_trans_post[prog] = d_ti[q].getComponent( -1 ); + Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; + Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; + Node invariant = single_inv_app_map[prog]; + invariant = invariant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), prog_templ_vars.begin(), prog_templ_vars.end() ); + Trace("cegqi-inv") << " invariant : " << invariant << std::endl; + + //construct template argument + d_templ_arg[prog] = NodeManager::currentNM()->mkSkolem( "I", invariant.getType() ); + + //construct template + Node templ; + if( options::sygusInvAutoUnfold() ){ + if( d_ti[q].isComplete() ){ + Trace("cegqi-inv-auto-unfold") << "Automatic deterministic unfolding... " << std::endl; + // auto-unfold + DetTrace dt; + int init_dt = d_ti[q].initializeTrace( dt ); + if( init_dt==0 ){ + Trace("cegqi-inv-auto-unfold") << " Init : "; + dt.print("cegqi-inv-auto-unfold"); + Trace("cegqi-inv-auto-unfold") << std::endl; + unsigned counter = 0; + unsigned status = 0; + while( counter<100 && status==0 ){ + status = d_ti[q].incrementTrace( dt ); + counter++; + Trace("cegqi-inv-auto-unfold") << " #" << counter << " : "; dt.print("cegqi-inv-auto-unfold"); - Trace("cegqi-inv-auto-unfold") << std::endl; - unsigned counter = 0; - unsigned status = 0; - while( counter<100 && status==0 ){ - status = d_ti[q].incrementTrace( dt ); - counter++; - Trace("cegqi-inv-auto-unfold") << " #" << counter << " : "; - dt.print("cegqi-inv-auto-unfold"); - Trace("cegqi-inv-auto-unfold") << "...status = " << status << std::endl; - } - if( status==1 ){ - // we have a trivial invariant - d_templ[prog] = d_ti[q].constructFormulaTrace( dt ); - Trace("cegqi-inv") << "By finite deterministic terminating trace, a solution invariant is : " << std::endl; - Trace("cegqi-inv") << " " << d_templ[prog] << std::endl; - // FIXME : this should be uncessary - d_templ[prog] = NodeManager::currentNM()->mkNode( AND, d_templ[prog], d_templ_arg[prog] ); - } - }else{ - Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl; + Trace("cegqi-inv-auto-unfold") << "...status = " << status << std::endl; + } + if( status==1 ){ + // we have a trivial invariant + templ = d_ti[q].constructFormulaTrace( dt ); + Trace("cegqi-inv") << "By finite deterministic terminating trace, a solution invariant is : " << std::endl; + Trace("cegqi-inv") << " " << templ << std::endl; + // FIXME : this should be unnecessary + templ = NodeManager::currentNM()->mkNode( AND, templ, d_templ_arg[prog] ); } - } - } - if( d_templ[prog].isNull() ){ - if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ - //d_templ[prog] = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] ); - d_templ[prog] = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], d_templ_arg[prog] ); }else{ - Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ); - //d_templ[prog] = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) ); - d_templ[prog] = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], d_templ_arg[prog] ); + Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl; } } - TNode iv = d_templ_arg[prog]; - TNode is = invariant; - Node templ = d_templ[prog].substitute( iv, is ); - visited.clear(); - templ = addDeepEmbedding( templ, visited ); - Trace("cegqi-inv") << " template : " << templ << std::endl; - prog_templ[prog] = templ; - } - Node bd = d_sip->d_conjuncts[2].size()==1 ? d_sip->d_conjuncts[2][0] : NodeManager::currentNM()->mkNode( AND, d_sip->d_conjuncts[2] ); - visited.clear(); - bd = addDeepEmbedding( bd, visited ); - Trace("cegqi-inv") << " body : " << bd << std::endl; - bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars ); - Trace("cegqi-inv-debug") << " templ-subs body : " << bd << std::endl; - //make inner existential - std::vector< Node > new_var_bv; - for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){ - std::stringstream ss; - ss << "ss_" << j; - new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() ) ); } - bd = bd.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), new_var_bv.begin(), new_var_bv.end() ); - Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ); - for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){ - new_var_bv.push_back( q[1][0][0][j] ); - } - if( !new_var_bv.empty() ){ - Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_var_bv ); - bd = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ).negate(); + if( templ.isNull() ){ + if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ + //d_templ[prog] = 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], d_templ_arg[prog] ); + }else{ + Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ); + //d_templ[prog] = 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], d_templ_arg[prog] ); + } } - //make outer universal - bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd ); - bd = Rewriter::rewrite( bd ); - Trace("cegqi-inv") << " rtempl-subs body : " << bd << std::endl; - d_quant = bd; + Trace("cegqi-inv") << " template (pre-substitution) : " << templ << std::endl; + Assert( !templ.isNull() ); + // subsitute the template arguments + templ = templ.substitute( prog_templ_vars.begin(), prog_templ_vars.end(), prog_vars[prog].begin(), prog_vars[prog].end() ); + Trace("cegqi-inv") << " template : " << templ << std::endl; + d_templ[prog] = templ; } - }else{ - //we are fully single invocation } }else{ - Trace("cegqi-si") << "...property is not single invocation, involves functions with different argument sorts." << std::endl; - singleInvocation = false; + //we are fully single invocation + d_single_invocation = true; } } - if( singleInvocation ){ +} + +void CegConjectureSingleInv::finishInit( bool syntaxRestricted, bool hasItes ) { + d_has_ites = hasItes; + // do not do single invocation if grammar is restricted and CEGQI_SI_MODE_ALL is not enabled + if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_USE && d_single_invocation && syntaxRestricted ){ + d_single_invocation = false; + Trace("cegqi-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl; + } + + // we now have determined whether we will do single invocation techniques + if( d_single_invocation ){ d_single_inv = d_sip->getSingleInvocation(); d_single_inv = TermDb::simpleNegate( d_single_inv ); if( !d_sip->d_func_vars.empty() ){ @@ -344,258 +271,79 @@ void CegConjectureSingleInv::initialize( Node q ) { Node v = NodeManager::currentNM()->mkSkolem( "a", d_sip->d_si_vars[i].getType(), "single invocation arg" ); d_single_inv_arg_sk.push_back( v ); } - d_single_inv = d_single_inv.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() ); + d_single_inv = d_single_inv.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), + d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() ); Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv << std::endl; if( options::cbqiPreRegInst() && d_single_inv.getKind()==FORALL ){ //just invoke the presolve now d_cinst->presolve( d_single_inv ); } - if( !isFullySingleInvocation() ){ - //initialize information as next single invocation conjecture - initializeNextSiConjecture(); - Trace("cegqi-si") << "Non-single invocation formula is : " << d_nsingle_inv << std::endl; - Trace("cegqi-si") << "Full specification is : " << d_full_inv << std::endl; - //add full specification lemma : will use for testing infeasibility/deriving entailments - d_full_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GF", NodeManager::currentNM()->booleanType() ) ); - d_full_guard = d_qe->getValuation().ensureLiteral( d_full_guard ); - AlwaysAssert( !d_full_guard.isNull() ); - d_qe->getOutputChannel().requirePhase( d_full_guard, true ); - Node fbvl; - if( !d_sip->d_all_vars.empty() ){ - fbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, d_sip->d_all_vars ); - } - //should construct this conjunction directly since miniscoping is disabled - std::vector< Node > flem_c; - for( unsigned i=0; i<d_sip->d_conjuncts[2].size(); i++ ){ - Node flemi = d_sip->d_conjuncts[2][i]; - if( !fbvl.isNull() ){ - flemi = NodeManager::currentNM()->mkNode( FORALL, fbvl, flemi ); - } - flem_c.push_back( flemi ); - } - Node flem = flem_c.empty() ? d_qe->getTermDatabase()->d_true : ( flem_c.size()==1 ? flem_c[0] : NodeManager::currentNM()->mkNode( AND, flem_c ) ); - flem = NodeManager::currentNM()->mkNode( OR, d_full_guard.negate(), flem ); - flem = Rewriter::rewrite( flem ); - Trace("cegqi-lemma") << "Cegqi::Lemma : full specification " << flem << std::endl; - d_qe->getOutputChannel().lemma( flem ); - } }else{ + d_single_inv = Node::null(); Trace("cegqi-si") << "Formula is not single invocation." << std::endl; if( options::cegqiSingleInvAbort() ){ Notice() << "Property is not single invocation." << std::endl; - exit( 0 ); + exit( 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; - } -} - -Node CegConjectureSingleInv::removeDeepEmbedding( Node n, std::vector< Node >& progs, std::vector< TypeNode >& types, int& type_valid, - std::map< Node, Node >& visited ) { - std::map< Node, Node >::iterator itv = visited.find( n ); - if( itv!=visited.end() ){ - return itv->second; - }else{ - std::vector< Node > children; - bool childChanged = false; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node ni = removeDeepEmbedding( n[i], progs, types, type_valid, visited ); - childChanged = childChanged || n[i]!=ni; - children.push_back( ni ); - } - Node ret; - if( n.getKind()==APPLY_UF ){ - Assert( n.getNumChildren()>0 ); - if( std::find( progs.begin(), progs.end(), n[0] )!=progs.end() ){ - std::map< Node, Node >::iterator it = d_nsi_op_map.find( n[0] ); - Node op; - if( it==d_nsi_op_map.end() ){ - bool checkTypes = !types.empty(); - std::vector< TypeNode > argTypes; - for( unsigned j=1; j<n.getNumChildren(); j++ ){ - TypeNode tn = n[j].getType(); - argTypes.push_back( tn ); - if( checkTypes ){ - if( j>=types.size()+1 || tn!=types[j-1] ){ - type_valid = -1; - } - }else{ - types.push_back( tn ); - } - } - TypeNode ft = argTypes.empty() ? n.getType() : NodeManager::currentNM()->mkFunctionType( argTypes, n.getType() ); - std::stringstream ss2; - ss2 << "O_" << n[0]; - op = NodeManager::currentNM()->mkSkolem( ss2.str(), ft, "was created for non-single invocation reasoning" ); - d_prog_to_eval_op[n[0]] = n.getOperator(); - d_nsi_op_map[n[0]] = op; - d_nsi_op_map_to_prog[op] = n[0]; - Trace("cegqi-si-debug2") << "Make operator " << op << " for " << n[0] << std::endl; - }else{ - op = it->second; - } - children[0] = d_nsi_op_map[n[0]]; - ret = children.size()>1 ? NodeManager::currentNM()->mkNode( APPLY_UF, children ) : children[0]; - } - } - if( ret.isNull() ){ - ret = n; - if( childChanged ){ - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.insert( children.begin(), n.getOperator() ); - } - ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - } - visited[n] = ret; - return ret; - } -} - -Node CegConjectureSingleInv::addDeepEmbedding( Node n, std::map< Node, Node >& visited ) { - std::map< Node, Node >::iterator itv = visited.find( n ); - if( itv!=visited.end() ){ - return itv->second; - }else{ - std::vector< Node > children; - bool childChanged = false; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node ni = addDeepEmbedding( n[i], visited ); - childChanged = childChanged || n[i]!=ni; - children.push_back( ni ); - } - Node ret; - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - std::map< Node, Node >::iterator it = d_nsi_op_map_to_prog.find( op ); - if( it!=d_nsi_op_map_to_prog.end() ){ - Node prog = it->second; - children.insert( children.begin(), prog ); - Assert( d_prog_to_eval_op.find( prog )!=d_prog_to_eval_op.end() ); - children.insert( children.begin(), d_prog_to_eval_op[prog] ); - ret = NodeManager::currentNM()->mkNode( APPLY_UF, children ); - } - } - if( ret.isNull() ){ - ret = n; - if( childChanged ){ - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.insert( children.begin(), n.getOperator() ); - } - ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - } - visited[n] = ret; - return ret; - } -} - -void CegConjectureSingleInv::initializeNextSiConjecture() { - Trace("cegqi-nsi") << "NSI : initialize next candidate conjecture..." << std::endl; - if( d_single_inv.isNull() ){ - if( d_ei->getEntailedConjecture( d_single_inv, d_single_inv_exp ) ){ - Trace("cegqi-nsi") << "NSI : got : " << d_single_inv << std::endl; - Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl; - }else{ - Trace("cegqi-nsi") << "NSI : failed to construct next conjecture." << std::endl; - Notice() << "Incomplete due to --cegqi-si-partial." << std::endl; - exit( 10 ); - } - }else{ - //initial call - Trace("cegqi-nsi") << "NSI : have : " << d_single_inv << std::endl; - Assert( d_single_inv_exp.isNull() ); - } - - d_si_guard = Node::null(); - d_ns_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GS", NodeManager::currentNM()->booleanType() ) ); - d_ns_guard = d_qe->getValuation().ensureLiteral( d_ns_guard ); - AlwaysAssert( !d_ns_guard.isNull() ); - d_qe->getOutputChannel().requirePhase( d_ns_guard, true ); - d_lemmas_produced.clear(); - if( options::incrementalSolving() ){ - delete d_c_inst_match_trie; - d_c_inst_match_trie = new inst::CDInstMatchTrie( d_qe->getUserContext() ); - }else{ - d_inst_match_trie.clear(); - } - Trace("cegqi-nsi") << "NSI : initialize next candidate conjecture, ns guard = " << d_ns_guard << std::endl; - Trace("cegqi-nsi") << "NSI : conjecture is " << d_single_inv << std::endl; -} - bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){ + Assert( d_single_inv_sk.size()==subs.size() ); + Trace("cegqi-si-inst-debug") << "CegConjectureSingleInv::doAddInstantiation, #vars = "; + Trace("cegqi-si-inst-debug") << d_single_inv_sk.size() << "..." << std::endl; std::stringstream siss; if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){ siss << " * single invocation: " << std::endl; for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){ Assert( d_sip->d_fo_var_to_func.find( d_single_inv[0][j] )!=d_sip->d_fo_var_to_func.end() ); Node op = d_sip->d_fo_var_to_func[d_single_inv[0][j]]; - Assert( d_nsi_op_map_to_prog.find( op )!=d_nsi_op_map_to_prog.end() ); - Node prog = d_nsi_op_map_to_prog[op]; + Node prog = op; siss << " * " << prog; siss << " (" << d_single_inv_sk[j] << ")"; siss << " -> " << subs[j] << std::endl; } } - bool alreadyExists; - if( options::incrementalSolving() ){ - alreadyExists = !d_c_inst_match_trie->addInstMatch( d_qe, d_single_inv, subs, d_qe->getUserContext() ); - }else{ - alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs ); - } Trace("cegqi-si-inst-debug") << siss.str(); - Trace("cegqi-si-inst-debug") << " * success = " << !alreadyExists << std::endl; - if( alreadyExists ){ - return false; + + bool alreadyExists; + Node lem; + if( subs.empty() ){ + Assert( d_single_inv.getKind()!=FORALL ); + alreadyExists = false; + lem = d_single_inv; }else{ - Trace("cegqi-engine") << siss.str() << std::endl; - Assert( d_single_inv_var.size()==subs.size() ); - Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); - if( d_qe->getTermDatabase()->containsVtsTerm( lem ) ){ - Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl; - lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem ); + Assert( d_single_inv.getKind()==FORALL ); + if( options::incrementalSolving() ){ + alreadyExists = !d_c_inst_match_trie->addInstMatch( d_qe, d_single_inv, subs, d_qe->getUserContext() ); + }else{ + alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs ); } - Trace("cegqi-engine-debug") << "Rewrite..." << std::endl; - lem = Rewriter::rewrite( lem ); - Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; - if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){ - d_curr_lemmas.push_back( lem ); - d_lemmas_produced.push_back( lem ); - d_inst.push_back( std::vector< Node >() ); - d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() ); + Trace("cegqi-si-inst-debug") << " * success = " << !alreadyExists << std::endl; + //Trace("cegqi-si-inst-debug") << siss.str(); + //Trace("cegqi-si-inst-debug") << " * success = " << !alreadyExists << std::endl; + if( alreadyExists ){ + return false; + }else{ + Trace("cegqi-engine") << siss.str() << std::endl; + Assert( d_single_inv_var.size()==subs.size() ); + lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); + if( d_qe->getTermDatabase()->containsVtsTerm( lem ) ){ + Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl; + lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem ); + } } - return true; } + Trace("cegqi-engine-debug") << "Rewrite..." << std::endl; + lem = Rewriter::rewrite( lem ); + Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; + if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){ + d_curr_lemmas.push_back( lem ); + d_lemmas_produced.push_back( lem ); + d_inst.push_back( std::vector< Node >() ); + d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() ); + } + return true; } bool CegConjectureSingleInv::isEligibleForInstantiation( Node n ) { @@ -610,84 +358,14 @@ bool CegConjectureSingleInv::addLemma( Node n ) { bool CegConjectureSingleInv::check( std::vector< Node >& lems ) { if( !d_single_inv.isNull() ) { Trace("cegqi-si-debug") << "CegConjectureSingleInv::check..." << std::endl; - if( !d_ns_guard.isNull() ){ - //if partially single invocation, check if we have constructed a candidate by refutation - bool value; - if( d_qe->getValuation().hasSatValue( d_ns_guard, value ) ) { - if( !value ){ - //construct candidate solution - Trace("cegqi-nsi") << "NSI : refuted current candidate conjecture, construct corresponding solution..." << std::endl; - d_ns_guard = Node::null(); - - std::map< Node, Node > lams; - for( unsigned i=0; i<d_quant[0].getNumChildren(); i++ ){ - Node prog = d_quant[0][i]; - int rcons; - Node sol = getSolution( i, prog.getType(), rcons, false ); - Trace("cegqi-nsi") << " solution for " << prog << " : " << sol << std::endl; - //make corresponding lambda - std::map< Node, Node >::iterator it_nso = d_nsi_op_map.find( prog ); - if( it_nso!=d_nsi_op_map.end() ){ - lams[it_nso->second] = sol; - }else{ - Assert( false ); - } - } - - //now, we will check if this candidate solution satisfies the non-single-invocation portion of the specification - Node inst = d_sip->getSpecificationInst( 1, lams ); - Trace("cegqi-nsi") << "NSI : specification instantiation : " << inst << std::endl; - inst = TermDb::simpleNegate( inst ); - std::vector< Node > subs; - for( unsigned i=0; i<d_sip->d_all_vars.size(); i++ ){ - subs.push_back( NodeManager::currentNM()->mkSkolem( "kv", d_sip->d_all_vars[i].getType(), "created for verifying nsi" ) ); - } - Assert( d_sip->d_all_vars.size()==subs.size() ); - inst = inst.substitute( d_sip->d_all_vars.begin(), d_sip->d_all_vars.end(), subs.begin(), subs.end() ); - Trace("cegqi-nsi") << "NSI : verification : " << inst << std::endl; - Trace("cegqi-lemma") << "Cegqi::Lemma : verification lemma : " << inst << std::endl; - d_qe->addLemma( inst ); - /* - Node finst = d_sip->getFullSpecification(); - finst = finst.substitute( d_sip->d_all_vars.begin(), d_sip->d_all_vars.end(), subs.begin(), subs.end() ); - Trace("cegqi-nsi") << "NSI : check refinement : " << finst << std::endl; - Node finst_lem = NodeManager::currentNM()->mkNode( OR, d_full_guard.negate(), finst ); - Trace("cegqi-lemma") << "Cegqi::Lemma : verification, refinement lemma : " << inst << std::endl; - d_qe->addLemma( finst_lem ); - */ - Trace("cegqi-si-debug") << "CegConjectureSingleInv::check returned verification lemma (nsi)..." << std::endl; - return true; - }else{ - //currently trying to construct candidate by refutation (by d_cinst->check below) - } - }else{ - //should be assigned a SAT value - Assert( false ); - } - }else if( !isFullySingleInvocation() ){ - //create next candidate conjecture - Assert( d_ei!=NULL ); - //construct d_single_inv - d_single_inv = Node::null(); - initializeNextSiConjecture(); - Trace("cegqi-si-debug") << "CegConjectureSingleInv::check initialized next si conjecture..." << std::endl; - return true; - } Trace("cegqi-si-debug") << "CegConjectureSingleInv::check consulting ceg instantiation..." << std::endl; d_curr_lemmas.clear(); Assert( d_cinst!=NULL ); //call check for instantiator d_cinst->check(); + Trace("cegqi-si-debug") << "...returned " << d_curr_lemmas.size() << " lemmas " << std::endl; //add lemmas - //add guard if not fully single invocation - if( !isFullySingleInvocation() ){ - Assert( !d_ns_guard.isNull() ); - for( unsigned i=0; i<d_curr_lemmas.size(); i++ ){ - lems.push_back( NodeManager::currentNM()->mkNode( OR, d_ns_guard.negate(), d_curr_lemmas[i] ) ); - } - }else{ - lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() ); - } + lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() ); return !lems.empty(); }else{ // not single invocation @@ -769,10 +447,11 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Assert( !d_lemmas_produced.empty() ); const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); Node varList = Node::fromExpr( dt.getSygusVarList() ); - Node prog = d_quant[0][sol_index]; + Node prog = d_quant[0][sol_index].getAttribute(SygusSynthFunAttribute()); std::vector< Node > vars; Node s; if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){ + Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl; s = d_qe->getTermDatabase()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 ); }else{ Trace("csi-sol") << "Get solution for " << prog << ", with skolems : "; diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index e22d5fb53..ad0f4f595 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -95,19 +95,17 @@ public: Node constructFormulaTrace( DetTrace& dt ); }; - +// this class infers whether a conjecture is single invocation (Reynolds et al CAV 2015), and sets up the +// counterexample-guided quantifier instantiation utility (d_cinst), and methods for solution +// reconstruction (d_sol). +// It also has more advanced techniques for: +// (1) partitioning a conjecture into single invocation / non-single invocation portions for invariant synthesis, +// (2) inferring whether the conjecture corresponds to a deterministic transistion system (by utility d_ti). +// For these techniques, we may generate a template (d_templ) which specifies a restricted +// solution space. We may in turn embed this template as a SyGuS grammar. class CegConjectureSingleInv { private: friend class CegqiOutputSingleInv; - // for recognizing templates for invariant synthesis - Node substituteInvariantTemplates( - Node n, std::map<Node, Node>& prog_templ, - std::map<Node, std::vector<Node> >& prog_templ_vars); - // partially single invocation - Node removeDeepEmbedding( Node n, std::vector< Node >& progs, - std::vector< TypeNode >& types, int& type_valid, - std::map< Node, Node >& visited ); - Node addDeepEmbedding( Node n, std::map< Node, Node >& visited ); //presolve void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ); @@ -119,16 +117,18 @@ class CegConjectureSingleInv { Node constructSolution(std::vector<unsigned>& indices, unsigned i, unsigned index, std::map<Node, Node>& weak_imp); Node postProcessSolution(Node n); - private: QuantifiersEngine* d_qe; CegConjecture* d_parent; + // single invocation inference utility SingleInvocationPartition* d_sip; + // transition inference module for each function to synthesize std::map< Node, TransitionInference > d_ti; + // solution reconstruction CegConjectureSingleInvSol* d_sol; - CegEntailmentInfer* d_ei; - // the instantiator + // the instantiator's output channel CegqiOutputSingleInv* d_cosi; + // the instantiator CegInstantiator* d_cinst; // list of skolems for each argument of programs @@ -148,6 +148,7 @@ class CegConjectureSingleInv { Node d_orig_solution; Node d_solution; Node d_sygus_solution; + // whether the grammar for our solution allows ITEs, this tells us when reconstruction is infeasible bool d_has_ites; public: @@ -166,34 +167,29 @@ class CegConjectureSingleInv { public: CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ); ~CegConjectureSingleInv(); - // original conjecture + // conjecture Node d_quant; + // are we single invocation? + bool d_single_invocation; // single invocation portion of quantified formula Node d_single_inv; Node d_si_guard; - // non-single invocation portion of quantified formula - Node d_nsingle_inv; - Node d_ns_guard; - // full version quantified formula - Node d_full_inv; - Node d_full_guard; - //explanation for current single invocation conjecture - Node d_single_inv_exp; // 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; + // the template for each function to synthesize std::map< Node, Node > d_templ; + // the template argument for each function to synthesize (occurs in exactly one position of its template) std::map< Node, Node > d_templ_arg; - //the non-single invocation portion of the quantified formula - std::map< Node, Node > d_nsi_op_map; - std::map< Node, Node > d_nsi_op_map_to_prog; - std::map< Node, Node > d_prog_to_eval_op; public: //get the single invocation lemma(s) void getInitialSingleInvLemma( std::vector< Node >& lems ); - //initialize + // initialize this class for synthesis conjecture q void initialize( Node q ); + // finish initialize, sets up final decisions about whether to use single invocation techniques + // syntaxRestricted is whether the syntax for solutions for the initialized conjecture is restricted + // hasItes is whether the syntax for solutions for the initialized conjecture allows ITEs + void finishInit( bool syntaxRestricted, bool hasItes ); //check bool check( std::vector< Node >& lems ); //get solution @@ -205,16 +201,10 @@ class CegConjectureSingleInv { bool hasITEs() { return d_has_ites; } // is single invocation bool isSingleInvocation() const { return !d_single_inv.isNull(); } - // is single invocation - bool isFullySingleInvocation() const { - return !d_single_inv.isNull() && d_nsingle_inv.isNull(); - } //needs check bool needsCheck(); /** preregister conjecture */ void preregisterConjecture( Node q ); - //initialize next candidate si conjecture (if not fully single invocation) - void initializeNextSiConjecture(); Node getTransPre(Node prog) const { std::map<Node, Node>::const_iterator location = d_trans_pre.find(prog); @@ -225,6 +215,7 @@ class CegConjectureSingleInv { std::map<Node, Node>::const_iterator location = d_trans_post.find(prog); return location->second; } + // get template for program prog. This returns a term of the form t[x] where x is the template argument (see below) Node getTemplate(Node prog) const { std::map<Node, Node>::const_iterator tmpl = d_templ.find(prog); if( tmpl!=d_templ.end() ){ @@ -233,6 +224,8 @@ class CegConjectureSingleInv { return Node::null(); } } + // get the template argument for program prog. + // This is a variable which indicates the position of the function/predicate to synthesize. Node getTemplateArg(Node prog) const { std::map<Node, Node>::const_iterator tmpla = d_templ_arg.find(prog); if( tmpla != d_templ_arg.end() ){ @@ -241,12 +234,11 @@ class CegConjectureSingleInv { return Node::null(); } } - }; -// partitions any formulas given to it into single invocation/non-single -// invocation only processes functions having argument types exactly matching -// "d_arg_types", and all invocations are in the same order across all +// A utility to group formulas into single invocation/non-single +// invocation parts. Only processes functions having argument types exactly matching +// "d_arg_types", and all invocations are in the same order across all // functions class SingleInvocationPartition { private: diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index 0a48b8834..a0af545e1 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -3003,6 +3003,52 @@ TypeNode TermDbSygus::mkSygusDefaultType( TypeNode range, Node bvl, const std::s return TypeNode::fromType( types[0] ); } +TypeNode TermDbSygus::mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, + const std::string& fun, unsigned& tcount ) { + if( templ==templ_arg ){ + //Assert( templ_arg.getType()==sygusToBuiltinType( templ_arg_sygus_type ) ); + return templ_arg_sygus_type; + }else{ + tcount++; + std::set<Type> unres; + std::vector< CVC4::Datatype > datatypes; + std::stringstream ssd; + ssd << fun << "_templ_" << tcount; + std::string dbname = ssd.str(); + datatypes.push_back(Datatype(dbname)); + Node op; + std::vector< Type > argTypes; + if( templ.getNumChildren()==0 ){ + // TODO : can short circuit to this case when !TermDb::containsTerm( templ, templ_arg ) + op = templ; + }else{ + Assert( templ.hasOperator() ); + op = templ.getOperator(); + // make constructor taking arguments types from children + for( unsigned i=0; i<templ.getNumChildren(); i++ ){ + //recursion depth bound by the depth of SyGuS template expressions (low) + TypeNode tnc = mkSygusTemplateTypeRec( templ[i], templ_arg, templ_arg_sygus_type, bvl, fun, tcount ); + argTypes.push_back( tnc.toType() ); + } + } + std::stringstream ssdc; + ssdc << fun << "_templ_cons_" << tcount; + std::string cname = ssdc.str(); + // we have a single sygus constructor that encodes the template + datatypes.back().addSygusConstructor( op.toExpr(), cname, argTypes ); + datatypes.back().setSygus( templ.getType().toType(), bvl.toExpr(), true, true ); + std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres); + Assert( types.size()==1 ); + return TypeNode::fromType( types[0] ); + } +} + +TypeNode TermDbSygus::mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, + const std::string& fun ) { + unsigned tcount = 0; + return mkSygusTemplateTypeRec( templ, templ_arg, templ_arg_sygus_type, bvl, fun, tcount ); +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h index 70f27dbaa..0ddfbaa75 100644 --- a/src/theory/quantifiers/term_database_sygus.h +++ b/src/theory/quantifiers/term_database_sygus.h @@ -296,18 +296,38 @@ private: public: Node extendedRewrite( Node n ); -// for default grammar construction +// for grammar construction private: + // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction) TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres); + // make the builtin constants for type type that should be included in a sygus grammar void mkSygusConstantsForType( TypeNode type, std::vector<CVC4::Node>& ops ); + // collect the list of types that depend on type range void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ); - void mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons, std::vector< CVC4::Datatype >& datatypes, std::set<Type>& unres ); + // helper function for function mkSygusDefaultGrammar below + // collects a set of mutually recursive datatypes "datatypes" corresponding to encoding type "range" to SyGuS + // unres is used for the resulting call to mkMutualDatatypeTypes + void mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons, + std::vector< CVC4::Datatype >& datatypes, std::set<Type>& unres ); + // helper function for mkSygusTemplateType + TypeNode mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, + const std::string& fun, unsigned& tcount ); public: + // make the default sygus datatype type corresponding to builtin type range + // bvl is the set of free variables to include in the grammar + // fun is for naming + // extra_cons is a set of extra constant symbols to include in the grammar TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons ); + // make the default sygus datatype type corresponding to builtin type range TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun ){ std::map< TypeNode, std::vector< Node > > extra_cons; return mkSygusDefaultType( range, bvl, fun, extra_cons ); } + // make the sygus datatype type that encodes the solution space (lambda templ_arg. templ[templ_arg]) where templ_arg + // has syntactic restrictions encoded by sygus type templ_arg_sygus_type + // bvl is the set of free variables to include in the frammar + // fun is for naming + TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun ); }; }/* CVC4::theory::quantifiers namespace */ diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index c22f64b93..01f3be1a1 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -62,7 +62,8 @@ TESTS = commutative.sy \ General_plus10.sy \ qe.sy \ cggmp.sy \ - parse-bv-let.sy + parse-bv-let.sy \ + cegar1.sy # sygus tests currently taking too long for make regress diff --git a/test/regress/regress0/sygus/cegar1.sy b/test/regress/regress0/sygus/cegar1.sy new file mode 100644 index 000000000..dd7f73e27 --- /dev/null +++ b/test/regress/regress0/sygus/cegar1.sy @@ -0,0 +1,23 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth +(set-logic LIA) + +(synth-inv inv-f ((x Int) (y Int))) + +(declare-primed-var x Int) +(declare-primed-var y Int) + +(define-fun pre-f ((x Int) (y Int)) Bool +(and (and (>= x 0) +(and (<= x 2) +(<= y 2))) (>= y 0))) + +(define-fun trans-f ((x Int) (y Int) (x! Int) (y! Int)) Bool +(and (= x! (+ x 2)) (= y! (+ y 2)))) + +(define-fun post-f ((x Int) (y Int)) Bool +(not (and (= x 4) (= y 0)))) + +(inv-constraint inv-f pre-f trans-f post-f) + +(check-synth) |