diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 107 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 6 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 476 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 60 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_match.h | 1 |
5 files changed, 362 insertions, 288 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 44b353ae5..f11153f5f 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -29,7 +29,7 @@ using namespace std; namespace CVC4 { -CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){ +CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_curr_lit( c, 0 ){ d_refine_count = 0; d_ceg_si = new CegConjectureSingleInv( qe, this ); } @@ -51,10 +51,10 @@ void CegConjecture::assign( Node 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; + Trace("cegqi") << "Base quantified formula is : " << q << std::endl; //construct base instantiation d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, d_candidates ) ); - Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; + Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; if( d_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; @@ -91,7 +91,7 @@ void CegConjecture::initializeGuard( QuantifiersEngine * qe ){ qe->getOutputChannel().lemma( lem ); }else if( d_ceg_si ){ std::vector< Node > lems; - d_ceg_si->getSingleInvLemma( d_guard, lems ); + d_ceg_si->getInitialSingleInvLemma( d_guard, lems ); for( unsigned i=0; i<lems.size(); i++ ){ Trace("cegqi-lemma") << "Add single invocation lemma " << i << " : " << lems[i] << std::endl; qe->getOutputChannel().lemma( lems[i] ); @@ -146,8 +146,12 @@ bool CegConjecture::isSingleInvocation() { return d_ceg_si->isSingleInvocation(); } +bool CegConjecture::isFullySingleInvocation() { + return d_ceg_si->isFullySingleInvocation(); +} + bool CegConjecture::needsCheck() { - return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() ); + return !isSingleInvocation() || d_ceg_si->needsCheck(); } void CegConjecture::preregisterConjecture( Node q ) { @@ -171,8 +175,21 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){ Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl; Trace("cegqi-engine-debug") << std::endl; - Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl; - if( d_conj->needsCheck() ){ + bool active = false; + bool feasible = false; + bool value; + if( d_quantEngine->getValuation().hasSatValue( d_conj->d_assert_quant, value ) ) { + active = value; + }else{ + Trace("cegqi-engine-debug") << "...no value for quantified formula." << std::endl; + } + if( d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) { + feasible = value; + }else{ + Trace("cegqi-engine-debug") << "...no value for guard." << std::endl; + } + Trace("cegqi-engine-debug") << "Current conjecture status : active : " << active << " feasible : " << feasible << std::endl; + if( active && feasible && d_conj->needsCheck() ){ checkCegConjecture( d_conj ); } Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl; @@ -217,34 +234,28 @@ void CegInstantiation::registerQuantifier( Node q ) { } void CegInstantiation::assertNode( Node n ) { - Trace("cegqi-debug") << "Cegqi : Assert : " << n << std::endl; - bool pol = n.getKind()!=NOT; - Node lit = n.getKind()==NOT ? n[0] : n; - if( lit==d_conj->d_guard ){ - //d_guard_assertions[lit] = pol; - d_conj->d_infeasible = !pol; - } - if( lit==d_conj->d_assert_quant ){ - d_conj->d_active = true; - } } Node CegInstantiation::getNextDecisionRequest() { //enforce fairness if( d_conj->isAssigned() ){ d_conj->initializeGuard( d_quantEngine ); - bool value; - if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) { - //if( d_conj->d_guard_split.isNull() ){ - // Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard ); - // d_quantEngine->getOutputChannel().lemma( lem ); - //} - Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl; - return d_conj->d_guard; + std::vector< Node > req_dec; + req_dec.push_back( d_conj->d_guard ); + if( d_conj->d_ceg_si && !d_conj->d_ceg_si->d_ns_guard.isNull() ){ + req_dec.push_back( d_conj->d_ceg_si->d_ns_guard ); + } + for( unsigned i=0; i<req_dec.size(); i++ ){ + bool value; + if( !d_quantEngine->getValuation().hasSatValue( req_dec[i], value ) ) { + Trace("cegqi-debug") << "CEGQI : Decide next on : " << req_dec[i] << "..." << std::endl; + return req_dec[i]; + } } if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); + bool value; if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { if( !value ){ d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 ); @@ -511,7 +522,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { //if( !(Trace.isOn("cegqi-stats")) ){ // out << "Solution:" << std::endl; //} - for( unsigned i=0; i<d_conj->d_candidates.size(); i++ ){ + for( unsigned i=0; i<d_conj->d_quant[0].getNumChildren(); i++ ){ Node prog = d_conj->d_quant[0][i]; std::stringstream ss; ss << prog; @@ -527,34 +538,50 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { if( d_last_inst_si ){ Assert( d_conj->d_ceg_si ); sol = d_conj->d_ceg_si->getSolution( i, tn, status ); + sol = sol.getKind()==LAMBDA ? sol[1] : sol; }else{ if( !d_conj->d_candidate_inst[i].empty() ){ sol = d_conj->d_candidate_inst[i].back(); //check if this was based on a template, if so, we must do reconstruction if( d_conj->d_assert_quant!=d_conj->d_quant ){ + Node sygus_sol = sol; 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(), + if( d_conj->d_ceg_si->d_trans_pre.find( prog )!=d_conj->d_ceg_si->d_trans_pre.end() ){ + Assert( d_conj->d_ceg_si->d_prog_templ_vars[prog].size()==subs.size() ); + 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( AND, sol, post ); + sol = getTermDatabase()->getTermDatabaseSygus()->sygusToBuiltin( sol, sol.getType() ); + Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() << std::endl; + sol = NodeManager::currentNM()->mkNode( OR, sol, pre ); + } + }else if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ){ + if( d_conj->d_ceg_si->d_trans_post.find( prog )!=d_conj->d_ceg_si->d_trans_post.end() ){ + Assert( d_conj->d_ceg_si->d_prog_templ_vars[prog].size()==subs.size() ); + 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 = getTermDatabase()->getTermDatabaseSygus()->sygusToBuiltin( sol, sol.getType() ); + Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() << std::endl; + sol = NodeManager::currentNM()->mkNode( AND, sol, post ); + } + } + if( sol==sygus_sol ){ + sol = sygus_sol; + status = 1; + }else{ + 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 ); + sol = sol.getKind()==LAMBDA ? sol[1] : sol; } - 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; } diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 8aa2e2c26..82c57b3d8 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -33,10 +33,6 @@ private: QuantifiersEngine * d_qe; public: CegConjecture( QuantifiersEngine * qe, context::Context* c ); - /** is conjecture active */ - context::CDO< bool > d_active; - /** is conjecture infeasible */ - context::CDO< bool > d_infeasible; /** quantified formula asserted */ Node d_assert_quant; /** quantified formula (after processing) */ @@ -87,6 +83,8 @@ public: //for fairness CegqiFairMode getCegqiFairMode(); /** is single invocation */ bool isSingleInvocation(); + /** is single invocation */ + bool isFullySingleInvocation(); /** needs check */ bool needsCheck(); /** preregister conjecture */ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 542fb652d..c9f71b76a 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -57,11 +57,11 @@ CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConje d_cinst = new CegInstantiator( qe, cosi, false, false ); d_sol = new CegConjectureSingleInvSol( qe ); - + d_sip = new SingleInvocationPartition; } -void CegConjectureSingleInv::getSingleInvLemma( Node guard, std::vector< Node >& lems ) { +void CegConjectureSingleInv::getInitialSingleInvLemma( Node guard, std::vector< Node >& lems ) { if( !d_single_inv.isNull() ) { d_single_inv_var.clear(); d_single_inv_sk.clear(); @@ -122,6 +122,7 @@ void CegConjectureSingleInv::initialize( Node q ) { std::map< Node, Node > visited; std::vector< TypeNode > types; 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; @@ -141,11 +142,9 @@ void CegConjectureSingleInv::initialize( Node q ) { 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; - d_single_inv_map[prog] = pv; - d_single_inv_map_to_prog[pv] = prog; Assert( d_sip->d_func_inv.find( op )!=d_sip->d_func_inv.end() ); Node inv = d_sip->d_func_inv[op]; - d_single_inv_app_map[prog] = inv; + 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 ); @@ -154,57 +153,72 @@ void CegConjectureSingleInv::initialize( Node q ) { //does not mention the function } } + //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 we are doing invariant templates, then construct the template - if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ + if( options::cegqiSingleInvPartial() ){ + /* TODO : 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 std::map< Node, bool > has_inv; std::map< Node, std::vector< Node > > inv_pre_post[2]; for( unsigned i=0; i<d_sip->d_conjuncts[2].size(); i++ ){ std::vector< Node > disjuncts; Node func; int pol = -1; - Trace("cegqi-si-inv") << "INV process " << d_sip->d_conjuncts[2][i] << std::endl; + Trace("cegqi-inv") << "INV process " << d_sip->d_conjuncts[2][i] << std::endl; d_sip->extractInvariant( d_sip->d_conjuncts[2][i], func, pol, disjuncts ); if( pol>=0 ){ Assert( d_nsi_op_map_to_prog.find( func )!=d_nsi_op_map_to_prog.end() ); Node prog = d_nsi_op_map_to_prog[func]; - Trace("cegqi-si-inv") << "..." << ( pol==0 ? "pre" : "post" ) << "-condition for " << prog << "." << std::endl; + Trace("cegqi-inv") << "..." << ( pol==0 ? "pre" : "post" ) << "-condition for " << prog << "." << std::endl; Node c = disjuncts.empty() ? d_qe->getTermDatabase()->d_false : ( disjuncts.size()==1 ? disjuncts[0] : NodeManager::currentNM()->mkNode( OR, disjuncts ) ); c = pol==0 ? TermDb::simpleNegate( c ) : c; - Trace("cegqi-si-inv-debug") << "...extracted : " << c << std::endl; + Trace("cegqi-inv-debug") << "...extracted : " << c << std::endl; inv_pre_post[pol][prog].push_back( c ); has_inv[prog] = true; }else{ - Trace("cegqi-si-inv") << "...no status." << std::endl; + Trace("cegqi-inv") << "...no status." << std::endl; } } - Trace("cegqi-si-inv") << "Constructing invariant templates..." << std::endl; + Trace("cegqi-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 : "; + Trace("cegqi-inv") << "...for " << prog << "..." << std::endl; + Trace("cegqi-inv") << " args : "; for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){ - Node v = NodeManager::currentNM()->mkBoundVar( d_sip->d_si_vars[j].getType() ); + std::stringstream ss; + ss << "i_" << j; + Node v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() ); d_prog_templ_vars[prog].push_back( v ); - Trace("cegqi-si-inv") << v << " "; + Trace("cegqi-inv") << v << " "; } - Trace("cegqi-si-inv") << std::endl; + Trace("cegqi-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( d_sip->d_si_vars.begin(), d_sip->d_si_vars.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( 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-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]; + 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-si-inv") << " invariant : " << invariant << std::endl; + Trace("cegqi-inv") << " invariant : " << invariant << std::endl; //construct template Node templ; if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ @@ -217,19 +231,21 @@ void CegConjectureSingleInv::initialize( Node q ) { } visited.clear(); templ = addDeepEmbedding( templ, visited ); - Trace("cegqi-si-inv") << " template : " << templ << std::endl; + 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-si-inv") << " body : " << bd << std::endl; + Trace("cegqi-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; + 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++ ){ - new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( d_sip->d_si_vars[j].getType() ) ); + 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 ); @@ -243,7 +259,7 @@ void CegConjectureSingleInv::initialize( Node q ) { //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; + Trace("cegqi-inv") << " rtempl-subs body : " << bd << std::endl; d_quant = bd; } }else{ @@ -253,14 +269,11 @@ void CegConjectureSingleInv::initialize( Node q ) { Trace("cegqi-si") << "...property is not single invocation, involves functions with different argument sorts." << std::endl; singleInvocation = false; } - if( options::cegqiSingleInvPartial() ){ - //TODO: set up outer loop - } if( singleInvocation ){ d_single_inv = d_sip->getSingleInvocation(); d_single_inv = TermDb::simpleNegate( d_single_inv ); - if( !order_vars.empty() ){ - Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, order_vars ); + if( !d_sip->d_func_vars.empty() ){ + Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, d_sip->d_func_vars ); d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv ); } //now, introduce the skolems @@ -274,6 +287,12 @@ void CegConjectureSingleInv::initialize( Node q ) { //just invoke the presolve now d_cinst->presolve( d_single_inv ); } + if( !d_nsingle_inv.isNull() ){ + //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; + } }else{ Trace("cegqi-si") << "Formula is not single invocation." << std::endl; if( options::cegqiSingleInvAbort() ){ @@ -283,84 +302,6 @@ void CegConjectureSingleInv::initialize( Node q ) { } } -bool CegConjectureSingleInv::doVariableElimination( Node v, std::vector< Node >& conjuncts ) { - //all conjuncts containing v must contain a literal v != s for some s - // if so, do DER on all such conjuncts - TNode s; - for( unsigned i=0; i<conjuncts.size(); i++ ){ - int status = 0; - if( getVariableEliminationTerm( true, true, v, conjuncts[i], s, status ) ){ - Trace("cegqi-si-debug") << "Substitute " << s << " for " << v << " in " << conjuncts[i] << std::endl; - Assert( !s.isNull() ); - conjuncts[i] = conjuncts[i].substitute( v, s ); - }else{ - if( status==1 ){ - Trace("cegqi-si-debug") << "Conjunct " << conjuncts[i] << " contains " << v << " but not in disequality." << std::endl; - return false; - }else{ - Trace("cegqi-si-debug") << "Conjunct does not contain " << v << "." << std::endl; - } - } - } - return true; -} - -bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol, Node v, Node n, TNode& s, int& status ) { - if( hasPol ){ - if( n.getKind()==NOT ){ - return getVariableEliminationTerm( !pol, true, v, n[0], s, status ); - }else if( pol && ( n.getKind()==EQUAL || n.getKind()==IFF ) ){ - Node ss = QuantArith::solveEqualityFor( n, v ); - if( !ss.isNull() ){ - if( s.isNull() ){ - s = ss; - } - return ss==s; - } - }else if( ( n.getKind()==OR && !pol ) || ( n.getKind()==AND && pol ) ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( getVariableEliminationTerm( pol, true, v, n[i], s, status ) ){ - return true; - } - } - return false; - } - } - if( n==v ){ - status = 1; - }else{ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - getVariableEliminationTerm( pol, false, v, n[i], s, status ); - } - } - 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] ); @@ -493,67 +434,20 @@ Node CegConjectureSingleInv::addDeepEmbedding( Node n, std::map< Node, Node >& v } } -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 ) { - 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 ) ){ - return false; - } - } - }else if( pol && n.getKind()==NOT && n[0].getKind()==FORALL ){ - if( !p.isNull() ){ - //do not allow nested quantifiers - return false; - } - analyzeSygusConjunct( n[0][0], n[0][1], children, prog_invoke, progs, contains, false ); - }else{ - if( pol ){ - n = TermDb::simpleNegate( n ); - } - Trace("cegqi-si") << "Sygus conjunct : " << n << std::endl; - children[p].push_back( n ); - for( unsigned i=0; i<progs.size(); i++ ){ - prog_invoke[n][progs[i]].clear(); - } - bool success = analyzeSygusTerm( n, prog_invoke[n], contains[n] ); - for( unsigned i=0; i<progs.size(); i++ ){ - std::map< Node, std::vector< Node > >::iterator it = prog_invoke[n].find( progs[i] ); - Trace("cegqi-si") << " Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl; - for( unsigned j=0; j<it->second.size(); j++ ){ - Trace("cegqi-si") << " " << it->second[j] << std::endl; - } - } - return success; - } - return true; -} - -bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains ) { - if( n.getNumChildren()>0 ){ - if( n.getKind()==FORALL ){ - //do not allow nested quantifiers - return false; - } - //look at first argument in evaluator - Node p = n[0]; - std::map< Node, std::vector< Node > >::iterator it = prog_invoke.find( p ); - if( it!=prog_invoke.end() ){ - if( std::find( it->second.begin(), it->second.end(), n )==it->second.end() ){ - it->second.push_back( n ); - } - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( !analyzeSygusTerm( n[i], prog_invoke, contains ) ){ - return false; - } - } +void CegConjectureSingleInv::initializeNextSiConjecture() { + 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{ - //record this conjunct contains n - contains[n] = true; + d_inst_match_trie.clear(); } - return true; + Trace("cegqi-nsi") << "NSI : initialize next candidate conjecture, guard = " << d_ns_guard << std::endl; + Trace("cegqi-nsi") << "NSI : conjecture is " << d_single_inv << std::endl; } bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){ @@ -561,8 +455,11 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){ 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++ ){ - Node v = d_single_inv_map_to_prog[d_single_inv[0][j]]; - siss << " * " << v; + 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]; + siss << " * " << prog; siss << " (" << d_single_inv_sk[j] << ")"; siss << " -> " << subs[j] << std::endl; } @@ -584,6 +481,10 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){ Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl; lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem ); } + //add guard if not fully single invocation + if( !isFullySingleInvocation() ){ + lem = NodeManager::currentNM()->mkNode( OR, d_ns_guard.negate(), lem ); + } Trace("cegqi-engine-debug") << "Rewrite..." << std::endl; lem = Rewriter::rewrite( lem ); Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; @@ -608,6 +509,54 @@ bool CegConjectureSingleInv::addLemma( Node n ) { void CegConjectureSingleInv::check( std::vector< Node >& lems ) { if( !d_single_inv.isNull() ) { + 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" ) ); + } + inst = inst.substitute( d_sip->d_all_vars.begin(), d_sip->d_all_vars.end(), subs.begin(), subs.end() ); + Trace("cegqi-nsi") << "NSI : verification lemma : " << inst << std::endl; + lems.push_back( inst ); + return; + }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 + Trace("cegqi-nsi") << "NSI : create next candidate conjecture..." << std::endl; + exit( 10 ); + } d_curr_lemmas.clear(); //call check for instantiator d_cinst->check(); @@ -681,20 +630,19 @@ Node CegConjectureSingleInv::postProcessSolution( Node n ){ } -Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){ +Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus ){ Assert( d_sol!=NULL ); 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]; std::vector< Node > vars; - bool success = true; - Trace("csi-sol") << "Get solution for " << prog << ", with skolems : "; + Node s; if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){ - success = false; + s = d_qe->getTermDatabase()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 ); }else{ + Trace("csi-sol") << "Get solution for " << prog << ", with skolems : "; sol_index = d_prog_to_sol_index[prog]; - d_varList.clear(); d_sol->d_varList.clear(); Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() ); for( unsigned i=0; i<d_single_inv_arg_sk.size(); i++ ){ @@ -706,15 +654,11 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& }else{ vars.push_back( d_single_inv_arg_sk[i] ); } - d_varList.push_back( varList[i] ); d_sol->d_varList.push_back( varList[i] ); } - } - Trace("csi-sol") << std::endl; + Trace("csi-sol") << std::endl; - //construct the solution - Node s; - if( success ){ + //construct the solution Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl; Assert( d_lemmas_produced.size()==d_inst.size() ); std::vector< unsigned > indices; @@ -730,27 +674,24 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& std::sort( indices.begin(), indices.end(), ssii ); Trace("csi-sol") << "Construct solution" << std::endl; s = constructSolution( indices, sol_index, 0 ); - s = s.substitute( vars.begin(), vars.end(), d_varList.begin(), d_varList.end() ); - d_orig_solution = s; - }else{ - //function is unconstrained : make ground term of correct sort - s = d_qe->getTermDatabase()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 ); + s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() ); } + d_orig_solution = s; //simplify the solution 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 ); + return reconstructToSyntax( s, stn, reconstructed, rconsSygus ); } -Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed ) { +Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus ) { d_solution = s; const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); //reconstruct the solution into sygus if necessary reconstructed = 0; - if( options::cegqiSingleInvReconstruct() && !dt.getSygusAllowAll() && !stn.isNull() ){ + if( options::cegqiSingleInvReconstruct() && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus ){ d_sol->preregisterConjecture( d_orig_conjecture ); d_sygus_solution = d_sol->reconstructSolution( s, stn, reconstructed ); if( reconstructed==1 ){ @@ -760,7 +701,7 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec Trace("csi-sol") << "Post-process solution..." << std::endl; Node prev = d_solution; d_solution = postProcessSolution( d_solution ); - if( prev!=d_solution ){ + if( prev!=d_solution ){ Trace("csi-sol") << "Solution (after post process) : " << d_solution << std::endl; } } @@ -792,10 +733,18 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec } Trace("cegqi-stats") << std::endl; } + Node sol; if( reconstructed==1 ){ - return d_sygus_solution; + sol = d_sygus_solution; }else{ - return d_solution; + sol = d_solution; + } + //make into lambda + if( !dt.getSygusVarList().isNull() ){ + Node varList = Node::fromExpr( dt.getSygusVarList() ); + return NodeManager::currentNM()->mkNode( LAMBDA, varList, sol ); + }else{ + return sol; } } @@ -817,7 +766,9 @@ void SingleInvocationPartition::init( std::vector< TypeNode >& typs ){ Assert( d_si_vars.empty() ); d_arg_types.insert( d_arg_types.end(), typs.begin(), typs.end() ); for( unsigned j=0; j<d_arg_types.size(); j++ ){ - Node si_v = NodeManager::currentNM()->mkBoundVar( d_arg_types[j] ); + std::stringstream ss; + ss << "s_" << j; + Node si_v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_arg_types[j] ); d_si_vars.push_back( si_v ); } } @@ -836,7 +787,9 @@ void SingleInvocationPartition::process( Node n ) { Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl; //do DER on conjunct Node cr = TermDb::getQuantSimplify( conj[i] ); - Trace("si-prt-debug") << "...rewritten to " << cr << std::endl; + if( cr!=conj[i] ){ + Trace("si-prt-debug") << "...rewritten to " << cr << std::endl; + } std::map< Node, bool > visited; // functions to arguments std::vector< Node > args; @@ -885,13 +838,36 @@ void SingleInvocationPartition::process( Node n ) { }else{ Trace("si-prt") << "...not single invocation." << std::endl; singleInvocation = false; + //rename bound variables with maximal overlap with si_vars + std::vector< Node > bvs; + TermDb::getBoundVars( cr, bvs ); + std::vector< Node > terms; + std::vector< Node > subs; + for( unsigned j=0; j<bvs.size(); j++ ){ + TypeNode tn = bvs[j].getType(); + Trace("si-prt-debug") << "Fit bound var #" << j << " : " << bvs[j] << " with si." << std::endl; + for( unsigned k=0; k<d_si_vars.size(); k++ ){ + if( tn==d_arg_types[k] ){ + if( std::find( subs.begin(), subs.end(), d_si_vars[k] )==subs.end() ){ + terms.push_back( bvs[j] ); + subs.push_back( d_si_vars[k] ); + Trace("si-prt-debug") << " ...use " << d_si_vars[k] << std::endl; + break; + } + } + } + } + cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); } - Trace("si-prt") << "..... got si=" << singleInvocation << ", result : " << cr << std::endl; + cr = Rewriter::rewrite( cr ); + Trace("si-prt") << ".....got si=" << singleInvocation << ", result : " << cr << std::endl; d_conjuncts[2].push_back( cr ); + TermDb::getBoundVars( cr, d_all_vars ); if( singleInvocation ){ //replace with single invocation formulation cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end() ); - Trace("si-prt") << "..... si version=" << cr << std::endl; + cr = Rewriter::rewrite( cr ); + Trace("si-prt") << ".....si version=" << cr << std::endl; d_conjuncts[0].push_back( cr ); }else{ d_conjuncts[1].push_back( cr ); @@ -923,7 +899,7 @@ bool SingleInvocationPartition::collectConjuncts( Node n, bool pol, std::vector< return true; } -bool SingleInvocationPartition::processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args, +bool SingleInvocationPartition::processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args, std::vector< Node >& terms, std::vector< Node >& subs ) { std::map< Node, bool >::iterator it = visited.find( n ); if( it!=visited.end() ){ @@ -950,7 +926,7 @@ bool SingleInvocationPartition::processConjunct( Node n, std::map< Node, bool >& //arguments must be the same as those already recorded for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( args[i]!=n[i] ){ - Trace("si-prt-debug") << "... bad invocation : " << n << " at arg " << i << "." << std::endl; + Trace("si-prt-debug") << "...bad invocation : " << n << " at arg " << i << "." << std::endl; ret = false; break; } @@ -1008,29 +984,101 @@ bool SingleInvocationPartition::isAntiSkolemizableType( Node f ) { } Node SingleInvocationPartition::getConjunct( int index ) { - return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst( true ) : + return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst( true ) : ( d_conjuncts[index].size()==1 ? d_conjuncts[index][0] : NodeManager::currentNM()->mkNode( AND, d_conjuncts[index] ) ); } -void SingleInvocationPartition::extractInvariant( Node n, Node& func, int& pol, std::vector< Node >& disjuncts ) { - if( n.getKind()==OR ){ +Node SingleInvocationPartition::getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited ) { + std::map< Node, Node >::iterator it = visited.find( n ); + if( it!=visited.end() ){ + return it->second; + }else{ + bool childChanged = false; + std::vector< Node > children; for( unsigned i=0; i<n.getNumChildren(); i++ ){ - extractInvariant( n[i], func, pol, disjuncts ); + Node nn = getSpecificationInst( n[i], lam, visited ); + children.push_back( nn ); + childChanged = childChanged || ( nn!=n[i] ); } - }else{ - bool lit_pol = n.getKind()!=NOT; - Node lit = n.getKind()==NOT ? n[0] : n; - std::map< Node, Node >::iterator it = d_inv_to_func.find( lit ); - if( it!=d_inv_to_func.end() ){ - if( pol==-1 ){ - pol = lit_pol ? 0 : 1; - func = it->second; - }else{ - //mixing multiple invariants - pol = -2; + Node ret; + if( n.getKind()==APPLY_UF ){ + std::map< Node, Node >::iterator itl = lam.find( n.getOperator() ); + if( itl!=lam.end() ){ + Assert( itl->second[0].getNumChildren()==children.size() ); + std::vector< Node > terms; + std::vector< Node > subs; + for( unsigned i=0; i<itl->second[0].getNumChildren(); i++ ){ + terms.push_back( itl->second[0][i] ); + subs.push_back( children[i] ); + } + ret = itl->second[1].substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + ret = Rewriter::rewrite( ret ); + } + } + 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 ); + } + } + return ret; + } +} + +Node SingleInvocationPartition::getSpecificationInst( int index, std::map< Node, Node >& lam ) { + Node conj = getConjunct( index ); + std::map< Node, Node > visited; + return getSpecificationInst( conj, lam, visited ); +} + +void SingleInvocationPartition::extractInvariant( Node n, Node& func, int& pol, std::vector< Node >& disjuncts ) { + std::map< Node, bool > visited; + extractInvariant2( n, func, pol, disjuncts, true, visited ); +} + +void SingleInvocationPartition::extractInvariant2( Node n, Node& func, int& pol, std::vector< Node >& disjuncts, bool hasPol, std::map< Node, bool >& visited ) { + if( visited.find( n )==visited.end() && pol!=-2 ){ + Trace("cegqi-inv-debug2") << "Extract : " << n << " " << hasPol << ", pol = " << pol << std::endl; + visited[n] = true; + if( n.getKind()==OR && hasPol ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + extractInvariant2( n[i], func, pol, disjuncts, true, visited ); } }else{ - disjuncts.push_back( n ); + if( hasPol ){ + bool lit_pol = n.getKind()!=NOT; + Node lit = n.getKind()==NOT ? n[0] : n; + std::map< Node, Node >::iterator it = d_inv_to_func.find( lit ); + if( it!=d_inv_to_func.end() ){ + if( pol==-1 ){ + pol = lit_pol ? 0 : 1; + func = it->second; + }else{ + //mixing multiple invariants + pol = -2; + } + return; + }else{ + disjuncts.push_back( n ); + } + } + //if another part mentions UF or a free variable, then fail + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( d_funcs.find( op )!=d_funcs.end() ){ + pol = -2; + return; + } + }else if( n.getKind()==BOUND_VARIABLE && std::find( d_si_vars.begin(), d_si_vars.end(), n )==d_si_vars.end() ){ + pol = -2; + return; + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + extractInvariant2( n[i], func, pol, disjuncts, false, visited ); + } } } } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index e6853b4f3..f058cf196 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -54,20 +54,13 @@ private: CegConjectureSingleInvSol * d_sol; //the instantiator CegInstantiator * d_cinst; - //for recognizing when conjecture is single invocation - bool analyzeSygusConjunct( Node n, Node p, 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 ); - bool analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains ); - 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 ); // 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 ); + //initialize next candidate si conjecture + void initializeNextSiConjecture(); //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 ); @@ -75,11 +68,6 @@ private: Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ); Node postProcessSolution( Node n ); private: - //map from programs to variables in single invocation property - std::map< Node, Node > d_single_inv_map; - std::map< Node, Node > d_single_inv_map_to_prog; - //map from programs to evaluator term representing the above variable - std::map< Node, Node > d_single_inv_app_map; //list of skolems for each argument of programs std::vector< Node > d_single_inv_arg_sk; //list of variables/skolems for each program @@ -94,7 +82,6 @@ private: //original conjecture Node d_orig_conjecture; // solution - std::vector< Node > d_varList; Node d_orig_solution; Node d_solution; Node d_sygus_solution; @@ -115,8 +102,14 @@ public: CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ); // original conjecture Node d_quant; - // single invocation version of quantified formula + // single invocation portion of quantified formula Node d_single_inv; + // non-single invocation portion of quantified formula + Node d_nsingle_inv; + // full version quantified formula + Node d_full_inv; + // current guard + Node d_ns_guard; // transition relation version per program std::map< Node, Node > d_trans_pre; std::map< Node, Node > d_trans_post; @@ -127,19 +120,21 @@ public: std::map< Node, Node > d_prog_to_eval_op; public: //get the single invocation lemma(s) - void getSingleInvLemma( Node guard, std::vector< Node >& lems ); + void getInitialSingleInvLemma( Node guard, std::vector< Node >& lems ); //initialize void initialize( Node q ); //check void check( std::vector< Node >& lems ); //get solution - Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ); + Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus = true ); //reconstruct to syntax - Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed ); + Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus = true ); // has ites bool hasITEs() { return d_has_ites; } // is single invocation bool isSingleInvocation() { return !d_single_inv.isNull(); } + // is single invocation + bool isFullySingleInvocation() { return d_nsingle_inv.isNull(); } //needs check bool needsCheck(); /** preregister conjecture */ @@ -147,40 +142,45 @@ public: }; // partitions any formulas given to it into single invocation/non-single invocation -// only processes functions having argument types exactly matching "d_arg_types", +// 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: bool collectConjuncts( Node n, bool pol, std::vector< Node >& conj ); - bool processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args, + bool processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args, std::vector< Node >& terms, std::vector< Node >& subs ); - std::map< Node, Node > d_inv_to_func; - std::map< Node, Node > d_fo_var_to_func; + Node getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited ); + void extractInvariant2( Node n, Node& func, int& pol, std::vector< Node >& disjuncts, bool hasPol, std::map< Node, bool >& visited ); public: void init( std::vector< TypeNode >& typs ); //inputs void process( Node n ); std::vector< TypeNode > d_arg_types; - + //outputs (everything is with bound var) std::map< Node, bool > d_funcs; std::map< Node, Node > d_func_inv; + std::map< Node, Node > d_inv_to_func; std::map< Node, Node > d_func_fo_var; - std::vector< Node > d_func_vars; - std::vector< Node > d_si_vars; + std::map< Node, Node > d_fo_var_to_func; + std::vector< Node > d_func_vars; //the first-order variables corresponding to all functions + std::vector< Node > d_si_vars; //the arguments that we based the anti-skolemization on + std::vector< Node > d_all_vars; //every free variable of conjuncts[2] // si, nsi, all std::vector< Node > d_conjuncts[3]; - + bool isAntiSkolemizableType( Node f ); - + Node getConjunct( int index ); Node getSingleInvocation() { return getConjunct( 0 ); } Node getNonSingleInvocation() { return getConjunct( 1 ); } Node getFullSpecification() { return getConjunct( 2 ); } - + + Node getSpecificationInst( int index, std::map< Node, Node >& lam ); + void extractInvariant( Node n, Node& func, int& pol, std::vector< Node >& disjuncts ); - + void debugPrint( const char * c ); }; diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index d66d331e5..f1c1c952a 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -131,6 +131,7 @@ public: std::vector< TNode > terms; print( out, q, terms ); } + void clear() { d_data.clear(); } };/* class InstMatchTrie */ /** trie for InstMatch objects */ |