From 679011435a1200ed97148d6daae130b48254c0e2 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 28 Mar 2017 16:21:12 -0500 Subject: [PATCH] Minor refactoring sygus. --- .../quantifiers/ce_guided_instantiation.cpp | 635 +++++++++--------- .../quantifiers/ce_guided_instantiation.h | 12 +- 2 files changed, 331 insertions(+), 316 deletions(-) diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index aa3b9c0de..08d705fa8 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -34,7 +34,6 @@ namespace quantifiers { CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_curr_lit( c, 0 ) { d_refine_count = 0; - d_incomplete_candidate_values = false; d_ceg_si = new CegConjectureSingleInv( qe, this ); } @@ -408,7 +407,7 @@ void CegConjecture::doCegConjectureSingleInvCheck(std::vector< Node >& lems) { } bool CegConjecture::needsRefinement() { - return !d_ce_sk.empty() || d_incomplete_candidate_values; + return !d_ce_sk.empty(); } void CegConjecture::getConditionalCandidateList( std::vector< Node >& clist, Node curr, bool reqAdd ){ @@ -517,7 +516,6 @@ void CegConjecture::doCegConjectureCheck(std::vector< Node >& lems, std::vector< std::vector< Node > c_model_values; Trace("cegqi-check") << "CegConjuncture : check, build candidates..." << std::endl; if( constructCandidates( clist, model_values, c_model_values ) ){ - d_incomplete_candidate_values = false; Assert( c_model_values.size()==d_candidates.size() ); if( Trace.isOn("cegqi-check") ){ Trace("cegqi-check") << "CegConjuncture : check candidate : " << std::endl; @@ -535,6 +533,7 @@ void CegConjecture::doCegConjectureCheck(std::vector< Node >& lems, std::vector< //check whether we will run CEGIS on inner skolem variables bool sk_refine = ( !isGround() || d_refine_count==0 || hasActiveConditionalNode ); if( sk_refine ){ + Assert( d_ce_sk.empty() ); d_ce_sk.push_back( std::vector< Node >() ); } std::vector< Node > ic; @@ -565,7 +564,6 @@ void CegConjecture::doCegConjectureCheck(std::vector< Node >& lems, std::vector< lems.push_back( lem ); recordInstantiation( c_model_values ); }else{ - d_incomplete_candidate_values = true; Assert( false ); } } @@ -691,13 +689,67 @@ Node CegConjecture::purifyConditionalEvaluations( Node n, std::map< Node, Node > void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ Assert( lems.empty() ); + Assert( d_ce_sk.size()==1 ); + + //first, make skolem substitution + Trace("cegqi-refine") << "doCegConjectureRefine : construct skolem substitution..." << std::endl; + std::vector< Node > sk_vars; + std::vector< Node > sk_subs; + //collect the substitution over all disjuncts + for( unsigned k=0; kgetTermDatabase()->d_skolem_constants[ce_q].size() ); + std::vector< Node > model_values; + getModelValues( d_qe->getTermDatabase()->d_skolem_constants[ce_q], model_values ); + sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() ); + sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() ); + }else{ + if( !d_inner_vars_disj[k].empty() ){ + //denegrate case : quantified disjunct was trivially true and does not need to be refined + //add trivial substitution (in case we need substitution for previous cex's) + for( unsigned i=0; i csol_active; std::map< Node, std::vector< Node > > csol_ccond_nodes; - std::map< Node, std::map< Node, bool > > csol_cpol; - std::vector< Node > csol_vals; + std::map< Node, std::map< Node, bool > > csol_cpol; if( options::sygusUnifCondSol() ){ + //previous non-ground conditional refinement lemmas must satisfy the current point + if( !isGround() ){ + Trace("cegqi-refine") << "doCegConjectureRefine : check for new refinements of previous lemmas..." << std::endl; + for( unsigned i=0; i subs; + for( unsigned ii=0; iimkSkolem( "y", d_refinement_lemmas_aux_vars[i][ii].getType(), + "purification variable for non-ground sygus conditional solution" ) ); + } + prev_lem = prev_lem.substitute( d_refinement_lemmas_aux_vars[i].begin(), d_refinement_lemmas_aux_vars[i].end(), subs.begin(), subs.end() ); + prev_lem = Rewriter::rewrite( prev_lem ); + Trace("sygus-unif") << "...previous conditional refinement lemma with new counterexample : " << prev_lem << std::endl; + lems.push_back( prev_lem ); + } + } + if( !lems.empty() ){ + Trace("cegqi-refine") << "...added lemmas, abort further refinement." << std::endl; + d_ce_sk.clear(); + return; + } + } + Trace("cegqi-refine") << "doCegConjectureRefine : conditional solution refinement, expand active conditional nodes" << std::endl; std::vector< Node > new_active_measure_sum; - Trace("sygus-unif") << "Conditional solution refinement, expand active conditional nodes" << std::endl; for( unsigned i=0; i& lems ){ new_active_measure_sum.push_back( acfv ); } csol_active[v] = ac; - csol_vals.push_back( d_cinfo[ac].d_csol_var[d_cinfo[ac].d_csol_status] ); } } if( !is_active_conditional ){ @@ -750,7 +801,6 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ } d_cinfo[ac].d_csol_status = 2; } - csol_vals.push_back( ac ); } if( !csol_ccond_nodes[v].empty() ){ Trace("sygus-unif") << "...it is nested under " << csol_ccond_nodes[v].size() << " other conditionals" << std::endl; @@ -762,14 +812,13 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ Node mclem = NodeManager::currentNM()->mkNode( kind::LEQ, mcsum, d_active_measure_term ); Trace("cegqi-lemma") << "Cegqi::Lemma : Measure component lemma : " << mclem << std::endl; d_qe->getOutputChannel().lemma( mclem ); -/* + /* for( unsigned i=0; imkNode( kind::LEQ, new_active_measure_sum[i], d_active_measure_term ); Trace("cegqi-lemma") << "Cegqi::Lemma : Measure component lemma : " << mclem << std::endl; d_qe->getOutputChannel().lemma( mclem ); } - */ - /* + Node new_active_measure = NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ); new_active_measure_sum.push_back( new_active_measure ); Node namlem = NodeManager::currentNM()->mkNode( kind::GEQ, new_active_measure, NodeManager::currentNM()->mkConst(Rational(0))); @@ -781,40 +830,32 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ */ } } - Trace("cegqi-refine") << "Refine " << d_ce_sk.size() << " points." << std::endl; + //for conditional evaluation std::map< Node, Node > psubs_visited; std::map< Node, Node > psubs; - //skolem substitution - std::vector< Node > sk_vars; - std::vector< Node > sk_subs; - for( unsigned j=0; j lem_c; - Assert( d_ce_sk[j].size()==d_base_disj.size() ); - std::vector< Node > inst_cond_c; - for( unsigned k=0; k lem_c; + Assert( d_ce_sk[0].size()==d_base_disj.size() ); + std::vector< Node > inst_cond_c; + Trace("cegqi-refine") << "doCegConjectureRefine : Construct refinement lemma..." << std::endl; + for( unsigned k=0; k& lems ){ }else{ //standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification } - //collect the substitution over all disjuncts - if( !ce_q.isNull() ){ - Assert( !d_inner_vars_disj[k].empty() ); - Assert( d_inner_vars_disj[k].size()==d_qe->getTermDatabase()->d_skolem_constants[ce_q].size() ); - std::vector< Node > model_values; - if( getModelValues( d_qe->getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){ - sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() ); - sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() ); - }else{ - success = false; - break; - } + lem_c.push_back( c_disj ); + } + } + Assert( sk_vars.size()==sk_subs.size() ); + //add conditional correctness assumptions + std::vector< Node > psubs_cond_ant; + std::vector< Node > psubs_cond_conc; + std::map< Node, std::vector< Node > > psubs_apply; + std::vector< Node > paux_vars; + if( options::sygusUnifCondSol() ){ + Trace("cegqi-refine") << "doCegConjectureRefine : add conditional assumptions for " << psubs.size() << " evaluations..." << std::endl; + for( std::map< Node, Node >::iterator itp = psubs.begin(); itp != psubs.end(); ++itp ){ + Assert( csol_active.find( itp->first[0] )!=csol_active.end() ); + paux_vars.push_back( itp->second ); + std::vector< Node > args; + for( unsigned a=1; afirst.getNumChildren(); a++ ){ + args.push_back( itp->first[a] ); } - //add to the lemma - if( !c_disj.isNull() ){ - lem_c.push_back( c_disj ); + Node ac = csol_active[itp->first[0]]; + Assert( d_cinfo.find( ac )!=d_cinfo.end() ); + Node c = d_cinfo[ac].d_csol_cond; + psubs_apply[ c ].push_back( itp->first ); + Trace("sygus-unif") << " process assumption " << itp->first << " == " << itp->second << ", with current condition " << c; + Trace("sygus-unif") << ", and " << csol_ccond_nodes[itp->first[0]].size() << " context conditionals." << std::endl; + std::vector< Node> assm; + if( !c.isNull() ){ + assm.push_back( mkConditional( ac, args, true ) ); } - } - if( success ){ - if( options::sygusUnifCondSol() ){ - Assert( d_candidates.size()==csol_vals.size() ); - //substitute the actual return values - sk_vars.insert( sk_vars.end(), d_candidates.begin(), d_candidates.end() ); - sk_subs.insert( sk_subs.end(), csol_vals.begin(), csol_vals.end() ); + for( unsigned j=0; jfirst[0]].size(); j++ ){ + Node acc = csol_ccond_nodes[itp->first[0]][j]; + bool pol = ( d_cinfo[acc].d_csol_status==1 ); + assm.push_back( mkConditional( acc, args, pol ) ); } - Assert( sk_vars.size()==sk_subs.size() ); - Trace("sygus-unif") << "Add conditional assumptions for " << psubs.size() << " evaluations." << std::endl; - //add conditional correctness assumptions - std::vector< Node > psubs_cond_ant; - std::vector< Node > psubs_cond_conc; - std::map< Node, std::vector< Node > > psubs_apply; - std::vector< Node > paux_vars; - for( std::map< Node, Node >::iterator itp = psubs.begin(); itp != psubs.end(); ++itp ){ - Assert( csol_active.find( itp->first[0] )!=csol_active.end() ); - paux_vars.push_back( itp->second ); - std::vector< Node > args; - for( unsigned a=1; afirst.getNumChildren(); a++ ){ - args.push_back( itp->first[a] ); - } - Node ac = csol_active[itp->first[0]]; - Assert( d_cinfo.find( ac )!=d_cinfo.end() ); - Node c = d_cinfo[ac].d_csol_cond; - psubs_apply[ c ].push_back( itp->first ); - Trace("sygus-unif") << " process assumption " << itp->first << " == " << itp->second << ", with current condition " << c; - Trace("sygus-unif") << ", and " << csol_ccond_nodes[itp->first[0]].size() << " context conditionals." << std::endl; - std::vector< Node> assm; - if( !c.isNull() ){ - assm.push_back( mkConditional( ac, args, true ) ); - } - for( unsigned j=0; jfirst[0]].size(); j++ ){ - Node acc = csol_ccond_nodes[itp->first[0]][j]; - bool pol = ( d_cinfo[acc].d_csol_status==1 ); - assm.push_back( mkConditional( acc, args, pol ) ); + Assert( !assm.empty() ); + Node c_ant = assm.size()==1 ? assm[0] : NodeManager::currentNM()->mkNode( kind::AND, assm ); + psubs_cond_ant.push_back( c_ant ); + // make the evaluation node + Node eret = mkConditionalNode( ac, args, d_cinfo[ac].d_csol_status+1 ); + Node c_conc = eret.eqNode( itp->second ); + psubs_cond_conc.push_back( c_conc ); + Trace("sygus-unif") << " ...made conditional correctness assumption : " << c_ant << " => " << c_conc << std::endl; + } + }else{ + Assert( psubs.empty() ); + } + + Node base_lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ); + + if( options::sygusUnifCondSol() ){ + Trace("sygus-unif-debug") << "We have base lemma : " << base_lem << std::endl; + //progress lemmas + Trace("cegqi-refine") << "doCegConjectureRefine : add progress lemmas..." << std::endl; + std::map< Node, bool > cprocessed; + for( std::map< Node, Node >::iterator itc = csol_active.begin(); itc !=csol_active.end(); ++itc ){ + Node x = itc->first; + Node ac = itc->second; + Assert( d_cinfo.find( ac )!=d_cinfo.end() ); + Node c = d_cinfo[ac].d_csol_cond; + if( !c.isNull() ){ + Trace("sygus-unif") << " process conditional " << c << " for " << x << ", which was applied " << psubs_apply[c].size() << " times." << std::endl; + //make the progress point + Assert( x.getType().isDatatype() ); + const Datatype& dx = ((DatatypeType)x.getType().toType()).getDatatype(); + Node sbvl = Node::fromExpr( dx.getSygusVarList() ); + std::vector< Node > prgr_pt; + for( unsigned a=0; amkSkolem( "kp", sbvl[a].getType(), "progress point for sygus conditional" ) ); } - Assert( !assm.empty() ); - Node c_ant = assm.size()==1 ? assm[0] : NodeManager::currentNM()->mkNode( kind::AND, assm ); - c_ant = c_ant.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); - psubs_cond_ant.push_back( c_ant ); - Node c_conc = itp->first.eqNode( itp->second ); - c_conc = c_conc.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); - psubs_cond_conc.push_back( c_conc ); - Trace("sygus-unif") << " ...made conditional correctness assumption : " << c_ant << " => " << c_conc << std::endl; - } - - Node base_lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ); - - if( options::sygusUnifCondSol() ){ - Trace("sygus-unif") << "We have base lemma : " << base_lem << std::endl; - //progress lemmas - Trace("sygus-unif") << "Now add progress assertions..." << std::endl; - std::map< Node, bool > cprocessed; - for( std::map< Node, Node >::iterator itc = csol_active.begin(); itc !=csol_active.end(); ++itc ){ - Node x = itc->first; - Node ac = itc->second; - Assert( d_cinfo.find( ac )!=d_cinfo.end() ); - Node c = d_cinfo[ac].d_csol_cond; - if( !c.isNull() ){ - Trace("sygus-unif") << " process conditional " << c << " for " << x << ", which was applied " << psubs_apply[c].size() << " times." << std::endl; - //make the progress point - Assert( x.getType().isDatatype() ); - const Datatype& dx = ((DatatypeType)x.getType().toType()).getDatatype(); - Node sbvl = Node::fromExpr( dx.getSygusVarList() ); - std::vector< Node > prgr_pt; - for( unsigned a=0; amkSkolem( "kp", sbvl[a].getType(), "progress point for sygus conditional" ) ); + Node pdlem; + if( !psubs_apply[c].empty() ){ + std::vector< Node > prgr_domain_d; + for( unsigned j=0; j prgr_domain; + for( unsigned a=1; a prgr_domain_d; - for( unsigned j=0; j prgr_domain; - for( unsigned a=1; amkNode( AND, prgr_domain ); - prgr_domain_d.push_back( pdc ); - } - } - if( !prgr_domain_d.empty() ){ - //the progress point is in the domain of some function application - pdlem = prgr_domain_d.size()==1 ? prgr_domain_d[0] : NodeManager::currentNM()->mkNode( OR, prgr_domain_d ); - pdlem = pdlem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); - Trace("sygus-unif") << "Progress domain point lemma is " << pdlem << std::endl; - lems.push_back( pdlem ); - } + if( !prgr_domain.empty() ){ + //the point is in the domain of this function application + Node pdc = prgr_domain.size()==1 ? prgr_domain[0] : NodeManager::currentNM()->mkNode( AND, prgr_domain ); + prgr_domain_d.push_back( pdc ); } - //the condition holds for the point, if this is an active condition - Node cplem = mkConditional( ac, prgr_pt ); - if( !csol_ccond_nodes[x].empty() ){ - std::vector< Node > prgr_conj; - prgr_conj.push_back( cplem ); - // ...and not for its context - for( unsigned j=0; jmkNode( kind::AND, prgr_conj ); - } - Assert( !d_cinfo[x].d_csol_progress_guard.isNull() ); - cplem = NodeManager::currentNM()->mkNode( kind::OR, d_cinfo[x].d_csol_progress_guard.negate(), cplem ); - Trace("sygus-unif") << "Progress lemma is " << cplem << std::endl; - lems.push_back( cplem ); } - } - /* - if( !prgr_conj.empty() ){ - Node prgr_lem = prgr_conj.size()==1 ? prgr_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, prgr_conj ); - prgr_lem = prgr_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); - prgr_lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), prgr_lem ); - Trace("sygus-unif") << "Progress lemma is " << prgr_lem << std::endl; - lems.push_back( prgr_lem ); - } - */ - - //previous non-ground conditional refinement lemmas must satisfy the current point - if( !isGround() ){ - for( unsigned i=0; i subs; - for( unsigned ii=0; iimkSkolem( "y", d_refinement_lemmas_aux_vars[i][ii].getType(), - "purification variable for non-ground sygus conditional solution" ) ); - } - prev_lem = prev_lem.substitute( d_refinement_lemmas_aux_vars[i].begin(), d_refinement_lemmas_aux_vars[i].end(), subs.begin(), subs.end() ); - prev_lem = Rewriter::rewrite( prev_lem ); - Trace("sygus-unif") << "...previous conditional refinement lemma with new counterexample : " << prev_lem << std::endl; - lems.push_back( prev_lem ); + if( !prgr_domain_d.empty() ){ + //the progress point is in the domain of some function application + pdlem = prgr_domain_d.size()==1 ? prgr_domain_d[0] : NodeManager::currentNM()->mkNode( OR, prgr_domain_d ); + pdlem = pdlem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + Trace("sygus-unif") << "Progress domain point lemma is " << pdlem << std::endl; + lems.push_back( pdlem ); } } - } - - //make the base lemma - base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); - base_lem = Rewriter::rewrite( base_lem ); - d_refinement_lemmas_base.push_back( base_lem ); - - Node lem = base_lem; - - if( options::sygusUnifCondSol() ){ - d_refinement_lemmas_ceval_ant.push_back( psubs_cond_ant ); - d_refinement_lemmas_ceval_conc.push_back( psubs_cond_conc ); - //add the conditional evaluation - if( !psubs_cond_ant.empty() ){ - std::vector< Node > children; - children.push_back( base_lem ); - for( unsigned i=0; imkNode( kind::OR, psubs_cond_ant[i].negate(), psubs_cond_conc[i] ) ); + //the condition holds for the point, if this is an active condition + Node cplem = mkConditional( ac, prgr_pt ); + if( !csol_ccond_nodes[x].empty() ){ + std::vector< Node > prgr_conj; + prgr_conj.push_back( cplem ); + // ...and not for its context + for( unsigned j=0; jmkNode( AND, children ); + cplem = NodeManager::currentNM()->mkNode( kind::AND, prgr_conj ); } + Assert( !d_cinfo[x].d_csol_progress_guard.isNull() ); + cplem = NodeManager::currentNM()->mkNode( kind::OR, d_cinfo[x].d_csol_progress_guard.negate(), cplem ); + Trace("sygus-unif") << "Progress lemma is " << cplem << std::endl; + lems.push_back( cplem ); + } + } + /* + if( !prgr_conj.empty() ){ + Node prgr_lem = prgr_conj.size()==1 ? prgr_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, prgr_conj ); + prgr_lem = prgr_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + prgr_lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), prgr_lem ); + Trace("sygus-unif") << "Progress lemma is " << prgr_lem << std::endl; + lems.push_back( prgr_lem ); + } + */ + } + + Trace("cegqi-refine") << "doCegConjectureRefine : construct and finalize lemmas..." << std::endl; + + Node lem = base_lem; + + base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + base_lem = Rewriter::rewrite( base_lem ); + d_refinement_lemmas_base.push_back( base_lem ); + + if( options::sygusUnifCondSol() ){ + //add the conditional evaluation + if( !psubs_cond_ant.empty() ){ + std::vector< Node > children; + children.push_back( base_lem ); + std::vector< Node > pav; + std::vector< Node > pcv; + for( unsigned i=0; imkNode( kind::OR, psubs_cond_ant[i].negate(), psubs_cond_conc[i] ) ); + Node pa = psubs_cond_ant[i].substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + pav.push_back( pa ); + Node pc = psubs_cond_conc[i].substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + pcv.push_back( pc ); } + d_refinement_lemmas_ceval_ant.push_back( pav ); + d_refinement_lemmas_ceval_conc.push_back( pcv ); + lem = NodeManager::currentNM()->mkNode( AND, children ); + } + } - lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem ); + lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem ); + + if( options::sygusUnifCondSol() ){ + if( !isGround() ){ + //store the non-ground version of the lemma lem = Rewriter::rewrite( lem ); - lems.push_back( lem ); - - d_refinement_lemmas.push_back( lem ); + d_refinement_lemmas_ngr.push_back( lem ); d_refinement_lemmas_aux_vars.push_back( paux_vars ); } } + + lem = lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + lem = Rewriter::rewrite( lem ); + d_refinement_lemmas.push_back( lem ); + lems.push_back( lem ); + d_ce_sk.clear(); - d_incomplete_candidate_values = false; } void CegConjecture::preregisterConjecture( Node q ) { d_ceg_si->preregisterConjecture( q ); } -bool CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) { - bool success = true; +void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) { Trace("cegqi-engine") << " * Value is : "; for( unsigned i=0; i& n, std::vector< Node >& TermDbSygus::printSygusTerm( ss, nv, lvs ); Trace("cegqi-engine") << ss.str() << " "; } - if( nv.isNull() ){ - Trace("cegqi-warn") << "WARNING: failed getModelValues." << std::endl; - success = false; - } + Assert( !nv.isNull() ); } Trace("cegqi-engine") << std::endl; - return success; } Node CegConjecture::getModelValue( Node n ) { @@ -1327,120 +1341,121 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { std::vector< Node > clist; conj->getCandidateList( clist ); std::vector< Node > model_values; - if( conj->getModelValues( clist, model_values ) ){ - if( options::sygusDirectEval() ){ - bool addedEvalLemmas = false; - if( options::sygusCRefEval() ){ - Trace("cegqi-debug") << "Do cref evaluation..." << std::endl; - // see if any refinement lemma is refuted by evaluation - std::vector< Node > cre_lems; - getCRefEvaluationLemmas( conj, clist, model_values, cre_lems ); - if( !cre_lems.empty() ){ - Trace("cegqi-engine") << " *** Do conjecture refinement evaluation..." << std::endl; - for( unsigned j=0; jaddLemma( lem ) ){ - addedEvalLemmas = true; - } - } - if( addedEvalLemmas ){ - return; - } - } - } - Trace("cegqi-debug") << "Do direct evaluation..." << std::endl; - std::vector< Node > eager_terms; - std::vector< Node > eager_vals; - std::vector< Node > eager_exps; - for( unsigned j=0; j " << model_values[j] << std::endl; - d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_terms, eager_vals, eager_exps ); - } - Trace("cegqi-debug") << "...produced " << eager_terms.size() << " eager evaluation lemmas." << std::endl; - if( !eager_terms.empty() ){ - Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl; - for( unsigned j=0; jmkNode( kind::OR, eager_exps[j].negate(), eager_terms[j].eqNode( eager_vals[j] ) ); - if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){ - //FIXME: hack to incorporate hacks from BV for division by zero - lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem ); - } - Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl; + conj->getModelValues( clist, model_values ); + if( options::sygusDirectEval() ){ + bool addedEvalLemmas = false; + if( options::sygusCRefEval() ){ + Trace("cegqi-debug") << "Do cref evaluation..." << std::endl; + // see if any refinement lemma is refuted by evaluation + std::vector< Node > cre_lems; + getCRefEvaluationLemmas( conj, clist, model_values, cre_lems ); + if( !cre_lems.empty() ){ + Trace("cegqi-engine") << " *** Do conjecture refinement evaluation..." << std::endl; + for( unsigned j=0; jaddLemma( lem ) ){ addedEvalLemmas = true; } } - } - if( addedEvalLemmas ){ - return; + if( addedEvalLemmas ){ + return; + } } } - //check if we must apply fairness lemmas - if( conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){ - Trace("cegqi-debug") << "Get measure lemmas..." << std::endl; - std::vector< Node > lems; - for( unsigned j=0; j " << model_values[j] << std::endl; - getMeasureLemmas( clist[j], model_values[j], lems ); - } - Trace("cegqi-debug") << "...produced " << lems.size() << " measure lemmas." << std::endl; - if( !lems.empty() ){ - Trace("cegqi-engine") << " *** Do measure refinement..." << std::endl; - for( unsigned j=0; jaddLemma( lems[j] ); + Trace("cegqi-debug") << "Do direct evaluation..." << std::endl; + std::vector< Node > eager_terms; + std::vector< Node > eager_vals; + std::vector< Node > eager_exps; + for( unsigned j=0; j " << model_values[j] << std::endl; + d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_terms, eager_vals, eager_exps ); + } + Trace("cegqi-debug") << "...produced " << eager_terms.size() << " eager evaluation lemmas." << std::endl; + if( !eager_terms.empty() ){ + Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl; + for( unsigned j=0; jmkNode( kind::OR, eager_exps[j].negate(), eager_terms[j].eqNode( eager_vals[j] ) ); + if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){ + //FIXME: hack to incorporate hacks from BV for division by zero + lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem ); + } + Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl; + if( d_quantEngine->addLemma( lem ) ){ + addedEvalLemmas = true; } - Trace("cegqi-engine") << " ...refine size." << std::endl; - return; } } - - Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; - std::vector< Node > cclems; - conj->doCegConjectureCheck( cclems, model_values ); - bool addedLemma = false; - for( unsigned i=0; i visited_n; - lem = getEagerUnfold( lem, visited_n ); - } - Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem << std::endl; - if( d_quantEngine->addLemma( lem ) ){ - ++(d_statistics.d_cegqi_lemmas_ce); - addedLemma = true; - }else{ - //this may happen if we eagerly unfold, simplify to true - if( !options::sygusDirectEval() ){ - Trace("cegqi-warn") << " ...FAILED to add candidate!" << std::endl; - }else{ - Trace("cegqi-engine-debug") << " ...FAILED to add candidate!" << std::endl; - } + if( addedEvalLemmas ){ + return; + } + } + //check if we must apply fairness lemmas + if( conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){ + Trace("cegqi-debug") << "Get measure lemmas..." << std::endl; + std::vector< Node > lems; + for( unsigned j=0; j " << model_values[j] << std::endl; + getMeasureLemmas( clist[j], model_values[j], lems ); + } + Trace("cegqi-debug") << "...produced " << lems.size() << " measure lemmas." << std::endl; + if( !lems.empty() ){ + Trace("cegqi-engine") << " *** Do measure refinement..." << std::endl; + for( unsigned j=0; jaddLemma( lems[j] ); } + Trace("cegqi-engine") << " ...refine size." << std::endl; + return; + } + } + + Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; + std::vector< Node > cclems; + conj->doCegConjectureCheck( cclems, model_values ); + bool addedLemma = false; + for( unsigned i=0; i visited_n; + lem = getEagerUnfold( lem, visited_n ); } - if( addedLemma ){ - Trace("cegqi-engine") << " ...check for counterexample." << std::endl; + Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem << std::endl; + if( d_quantEngine->addLemma( lem ) ){ + ++(d_statistics.d_cegqi_lemmas_ce); + addedLemma = true; }else{ - if( conj->needsRefinement() ){ - //immediately go to refine candidate - checkCegConjecture( conj ); - return; + //this may happen if we eagerly unfold, simplify to true + if( !options::sygusDirectEval() ){ + Trace("cegqi-warn") << " ...FAILED to add candidate!" << std::endl; + }else{ + Trace("cegqi-engine-debug") << " ...FAILED to add candidate!" << std::endl; } - } + } } + if( addedLemma ){ + Trace("cegqi-engine") << " ...check for counterexample." << std::endl; + }else{ + if( conj->needsRefinement() ){ + //immediately go to refine candidate + checkCegConjecture( conj ); + return; + } + } }else{ Assert( aq==q ); std::vector< Node > model_terms; std::vector< Node > clist; conj->getCandidateList( clist, true ); Assert( clist.size()==q[0].getNumChildren() ); - if( conj->getModelValues( clist, model_terms ) ){ + conj->getModelValues( clist, model_terms ); + if( d_quantEngine->addInstantiation( q, model_terms ) ){ conj->recordInstantiation( model_terms ); - d_quantEngine->addInstantiation( q, model_terms ); + }else{ + Assert( false ); } } }else{ diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 358e4ea21..9eef7f070 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -50,13 +50,15 @@ private: Node d_active_measure_term; /** refinement lemmas */ std::vector< Node > d_refinement_lemmas; - std::vector< std::vector< Node > > d_refinement_lemmas_aux_vars; std::vector< Node > d_refinement_lemmas_base; - std::vector< std::vector< Node > > d_refinement_lemmas_ceval_ant; - std::vector< std::vector< Node > > d_refinement_lemmas_ceval_conc; //std::vector< Node > d_refinement_lemmas_cprogress; //std::vector< std::vector< Node > > d_refinement_lemmas_cprogress_pts; private: //for condition solutions + std::vector< std::vector< Node > > d_refinement_lemmas_aux_vars; + std::vector< std::vector< Node > > d_refinement_lemmas_ceval_ant; + std::vector< std::vector< Node > > d_refinement_lemmas_ceval_conc; + std::vector< Node > d_refinement_lemmas_ngr; //non-ground version + std::map< Node, bool > d_refinement_lemmas_reproc; /** get candidate list recursively for conditional solutions */ void getConditionalCandidateList( std::vector< Node >& clist, Node curr, bool reqAdd ); Node constructConditionalCandidate( std::map< Node, Node >& cmv, Node curr ); @@ -104,8 +106,6 @@ public: int d_measure_term_size; /** refine count */ unsigned d_refine_count; - /** incomplete candidate values */ - bool d_incomplete_candidate_values; const CegConjectureSingleInv* getCegConjectureSingleInv() const { return d_ceg_si; @@ -183,7 +183,7 @@ public: /** is assigned */ bool isAssigned() { return !d_quant.isNull(); } /** get model values */ - bool getModelValues( std::vector< Node >& n, std::vector< Node >& v ); + void getModelValues( std::vector< Node >& n, std::vector< Node >& v ); /** get model value */ Node getModelValue( Node n ); /** get number of refinement lemmas */ -- 2.30.2