diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-22 08:52:42 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-22 09:00:56 -0500 |
commit | 620ebbaf88f07abc36399499cfa6dfef8c3369d9 (patch) | |
tree | fe18fdae38b0fcd64ea9d3014a3dd7846b6c7202 /src/theory/quantifiers | |
parent | 18d2fd549d5058a6ea3ee782568bbc3ce00189ea (diff) |
Work on new approach for sygus involving conditional solutions. Refactoring of sygus solver. Bug fix for sygus solution reconstruction.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 938 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 112 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv_sol.cpp | 2 |
4 files changed, 822 insertions, 236 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 9903f14aa..999c554b5 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -32,9 +32,9 @@ namespace quantifiers { CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c ) - : d_qe( qe ), d_curr_lit( c, 0 ) -{ + : d_qe( qe ), d_curr_lit( c, 0 ) { d_refine_count = 0; + d_incomplete_candidate_values = false; d_ceg_si = new CegConjectureSingleInv( qe, this ); } @@ -71,6 +71,7 @@ void CegConjecture::assign( Node q ) { Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; //store the inner variables for each disjunct for( unsigned j=0; j<d_base_disj.size(); j++ ){ + Trace("cegqi") << " " << j << " : " << d_base_disj[j] << std::endl; d_inner_vars_disj.push_back( std::vector< Node >() ); //if the disjunct is an existential, store it if( d_base_disj[j].getKind()==NOT && d_base_disj[j][0].getKind()==FORALL ){ @@ -80,6 +81,12 @@ void CegConjecture::assign( Node q ) { } } } + if( options::cegqiUnifCondSol() ){ + // for each variable, determine whether we can do conditional counterexamples + for( unsigned i=0; i<d_candidates.size(); i++ ){ + registerCandidateConditional( d_candidates[i] ); + } + } d_syntax_guided = true; }else if( d_qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){ d_syntax_guided = false; @@ -88,25 +95,64 @@ void CegConjecture::assign( Node q ) { } } -void CegConjecture::initializeGuard( QuantifiersEngine * qe ){ +void CegConjecture::registerCandidateConditional( Node v ) { + TypeNode tn = v.getType(); + bool type_valid = false; + if( tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); + if( dt.isSygus() ){ + type_valid = true; + for( unsigned j=0; j<dt.getNumConstructors(); j++ ){ + Node op = Node::fromExpr( dt[j].getSygusOp() ); + if( op.getKind() == kind::BUILTIN ){ + Kind sk = NodeManager::operatorToKind( op ); + if( sk==kind::ITE ){ + // we can do unification + d_cinfo[v].d_csol_op = Node::fromExpr( dt[j].getConstructor() ); + Trace("cegqi") << "Can do synthesis unification for variable " << v << ", based on operator " << d_cinfo[v].d_csol_op << std::endl; + Assert( dt[j].getNumArgs()==3 ); + for( unsigned k=0; k<3; k++ ){ + Type t = dt[j][k].getRangeType(); + if( k==0 ){ + d_cinfo[v].d_csol_cond = NodeManager::currentNM()->mkSkolem( "c", TypeNode::fromType( t ) ); + }else{ + d_cinfo[v].d_csol_var[k-1] = NodeManager::currentNM()->mkSkolem( "e", TypeNode::fromType( t ) ); + } + } + break; + } + } + } + } + } + //mark active + if( d_cinfo[v].d_csol_cond.isNull() ){ + d_cinfo[v].d_csol_status = 0; + } + if( !type_valid ){ + Assert( false ); + } +} + +void CegConjecture::initializeGuard(){ if( isAssigned() ){ if( !d_syntax_guided ){ if( d_nsg_guard.isNull() ){ d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); - d_nsg_guard = qe->getValuation().ensureLiteral( d_nsg_guard ); + d_nsg_guard = d_qe->getValuation().ensureLiteral( d_nsg_guard ); AlwaysAssert( !d_nsg_guard.isNull() ); - qe->getOutputChannel().requirePhase( d_nsg_guard, true ); + d_qe->getOutputChannel().requirePhase( d_nsg_guard, true ); //add immediate lemma Node lem = NodeManager::currentNM()->mkNode( OR, d_nsg_guard.negate(), d_base_inst.negate() ); Trace("cegqi-lemma") << "Cegqi::Lemma : non-syntax-guided : " << lem << std::endl; - qe->getOutputChannel().lemma( lem ); + d_qe->getOutputChannel().lemma( lem ); } }else if( d_ceg_si->d_si_guard.isNull() ){ std::vector< Node > lems; d_ceg_si->getInitialSingleInvLemma( lems ); for( unsigned i=0; i<lems.size(); i++ ){ Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl; - qe->getOutputChannel().lemma( lems[i] ); + d_qe->getOutputChannel().lemma( lems[i] ); if( Trace.isOn("cegqi-debug") ){ Node rlem = Rewriter::rewrite( lems[i] ); Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl; @@ -117,7 +163,25 @@ void CegConjecture::initializeGuard( QuantifiersEngine * qe ){ } } -Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { +void CegConjecture::setMeasureTerm( Node mt ){ + d_measure_term = mt; + d_active_measure_term = mt; +} + +Node CegConjecture::getMeasureTermFactor( Node v ) { + Node ret; + if( getCegqiFairMode()==CEGQI_FAIR_DT_SIZE ){ + if( v.getType().isDatatype() ){ + ret = NodeManager::currentNM()->mkNode( DT_SIZE, v ); + } + } + //TODO + Assert( ret.isNull() || ret.getType().isInteger() ); + return ret; +} + + +Node CegConjecture::getFairnessLiteral( int i ) { if( d_measure_term.isNull() ){ return Node::null(); }else{ @@ -131,8 +195,8 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() ); Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness split : " << lem << std::endl; - qe->getOutputChannel().lemma( lem ); - qe->getOutputChannel().requirePhase( lit, true ); + d_qe->getOutputChannel().lemma( lem ); + d_qe->getOutputChannel().requirePhase( lit, true ); if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED ){ //implies height bounds on each candidate variable @@ -146,7 +210,7 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { } Node hlem = NodeManager::currentNM()->mkNode( OR, lit.negate(), lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ) ); Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness expansion (pred) : " << hlem << std::endl; - qe->getOutputChannel().lemma( hlem ); + d_qe->getOutputChannel().lemma( hlem ); } return lit; }else{ @@ -219,10 +283,563 @@ bool CegConjecture::needsCheck( std::vector< Node >& lem ) { } } + +void CegConjecture::doCegConjectureSingleInvCheck(std::vector< Node >& lems) { + if( d_ceg_si!=NULL ){ + d_ceg_si->check(lems); + } +} + +bool CegConjecture::needsRefinement() { + return !d_ce_sk.empty() || d_incomplete_candidate_values; +} + +void CegConjecture::getConditionalCandidateList( std::vector< Node >& clist, Node curr, bool reqAdd ){ + Assert( options::cegqiUnifCondSol() ); + std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr ); + if( it!=d_cinfo.end() ){ + if( !it->second.d_csol_cond.isNull() ){ + if( it->second.d_csol_status!=-1 ){ + Assert( it->second.d_csol_status==0 || it->second.d_csol_status==1 ); + //interested in model value for condition and branched variables + clist.push_back( it->second.d_csol_cond ); + //assume_flat_ITEs + clist.push_back( it->second.d_csol_var[it->second.d_csol_status] ); + //conditionally get the other branch + getConditionalCandidateList( clist, it->second.d_csol_var[1-it->second.d_csol_status], false ); + return; + }else{ + //otherwise, yet to explore branch + if( !reqAdd ){ + // if we are not top-level, we can ignore this (it won't be part of solution) + return; + } + } + }else{ + // a standard variable not handlable by unification + } + clist.push_back( curr ); + } +} + +void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) { + if( options::cegqiUnifCondSol() && !forceOrig ){ + for( unsigned i=0; i<d_candidates.size(); i++ ){ + getConditionalCandidateList( clist, d_candidates[i], true ); + } + }else{ + clist.insert( clist.end(), d_candidates.begin(), d_candidates.end() ); + } +} + +Node CegConjecture::constructConditionalCandidate( std::map< Node, Node >& cmv, Node curr ) { + Assert( options::cegqiUnifCondSol() ); + std::map< Node, Node >::iterator itc = cmv.find( curr ); + if( itc!=cmv.end() ){ + return itc->second; + }else{ + std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr ); + if( it!=d_cinfo.end() ){ + if( !it->second.d_csol_cond.isNull() ){ + if( it->second.d_csol_status!=-1 ){ + Assert( it->second.d_csol_status==0 || it->second.d_csol_status==1 ); + Node v_curr = constructConditionalCandidate( cmv, it->second.d_csol_var[it->second.d_csol_status] ); + Node v_next = constructConditionalCandidate( cmv, it->second.d_csol_var[1-it->second.d_csol_status] ); + if( v_next.isNull() ){ + // try taking current branch as a leaf + return v_curr; + }else{ + Node v_cond = constructConditionalCandidate( cmv, it->second.d_csol_cond ); + std::vector< Node > args; + args.push_back( it->second.d_csol_op ); + args.push_back( v_cond ); + args.push_back( it->second.d_csol_status==0 ? v_curr : v_next ); + args.push_back( it->second.d_csol_status==0 ? v_next : v_curr ); + return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, args ); + } + } + } + } + } + return Node::null(); +} + +bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values ) { + Assert( clist.size()==model_values.size() ); + if( options::cegqiUnifCondSol() ){ + std::map< Node, Node > cmv; + for( unsigned i=0; i<clist.size(); i++ ){ + cmv[ clist[i] ] = model_values[i]; + } + for( unsigned i=0; i<d_candidates.size(); i++ ){ + Node n = constructConditionalCandidate( cmv, d_candidates[i] ); + Trace("cegqi-candidate") << "...constructed conditional candidate " << n << " for " << d_candidates[i] << std::endl; + candidate_values.push_back( n ); + if( n.isNull() ){ + return false; + } + } + }else{ + Assert( model_values.size()==d_candidates.size() ); + candidate_values.insert( candidate_values.end(), model_values.begin(), model_values.end() ); + } + return true; +} + +void CegConjecture::doCegConjectureCheck(std::vector< Node >& lems, std::vector< Node >& model_values) { + std::vector< Node > clist; + getCandidateList( clist ); + 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; + for( unsigned i=0; i<c_model_values.size(); i++ ){ + Trace("cegqi-check") << " " << i << " : " << d_candidates[i] << " -> " << c_model_values[i] << std::endl; + } + } + //must get a counterexample to the value of the current candidate + Node inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() ); + bool hasActiveConditionalNode = false; + if( options::cegqiUnifCondSol() ){ + //TODO + hasActiveConditionalNode = true; + } + //check whether we will run CEGIS on inner skolem variables + bool sk_refine = ( !isGround() || d_refine_count==0 || hasActiveConditionalNode ); + if( sk_refine ){ + d_ce_sk.push_back( std::vector< Node >() ); + } + std::vector< Node > ic; + ic.push_back( d_assert_quant.negate() ); + std::vector< Node > d; + CegInstantiation::collectDisjuncts( inst, d ); + Assert( d.size()==d_base_disj.size() ); + //immediately skolemize inner existentials + for( unsigned i=0; i<d.size(); i++ ){ + Node dr = Rewriter::rewrite( d[i] ); + if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){ + ic.push_back( d_qe->getTermDatabase()->getSkolemizedBody( dr[0] ).negate() ); + if( sk_refine ){ + d_ce_sk.back().push_back( dr[0] ); + } + }else{ + ic.push_back( dr ); + if( sk_refine ){ + d_ce_sk.back().push_back( Node::null() ); + } + if( !d_inner_vars_disj[i].empty() ){ + Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl; + } + } + } + Node lem = NodeManager::currentNM()->mkNode( OR, ic ); + lem = Rewriter::rewrite( lem ); + lems.push_back( lem ); + recordInstantiation( c_model_values ); + }else{ + d_incomplete_candidate_values = true; + Assert( false ); + } +} + +Node CegConjecture::getActiveConditional( Node curr ) { + Assert( options::cegqiUnifCondSol() ); + std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr ); + Assert( it!=d_cinfo.end() ); + if( !it->second.d_csol_cond.isNull() ){ + if( it->second.d_csol_status==-1 ){ + //yet to branch, this is the one + return curr; + }else{ + Assert( it->second.d_csol_status==0 || it->second.d_csol_status==1 ); + return getActiveConditional( it->second.d_csol_var[1-it->second.d_csol_status] ); + } + }else{ + //not a conditional + return curr; + } +} + +void CegConjecture::getContextConditionals( Node curr, Node x, std::vector< Node >& conds, std::vector< Node >& rets, std::map< Node, bool >& cpols ) { + if( curr!=x ){ + std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr ); + if( !it->second.d_csol_cond.isNull() ){ + if( it->second.d_csol_status!=-1 ){ + conds.push_back( it->second.d_csol_cond ); + rets.push_back( it->second.d_csol_var[it->second.d_csol_status] ); + cpols[it->second.d_csol_cond] = ( it->second.d_csol_status==1 ); + getContextConditionals( it->second.d_csol_var[1-it->second.d_csol_status], x, conds, rets, cpols ); + } + } + } +} + +Node CegConjecture::mkConditional( Node c, std::vector< Node >& args, bool pol ) { + Assert( !c.isNull() ); + std::vector< Node > condc; + //get evaluator + Assert( c.getType().isDatatype() ); + const Datatype& cd = ((DatatypeType)c.getType().toType()).getDatatype(); + Assert( cd.isSygus() ); + condc.push_back( Node::fromExpr( cd.getSygusEvaluationFunc() ) ); + condc.push_back( c ); + for( unsigned a=0; a<args.size(); a++ ){ + condc.push_back( args[a] ); + } + Node ret = NodeManager::currentNM()->mkNode( kind::APPLY_UF, condc ); + if( !pol ){ + ret = ret.negate(); + } + return ret; +} + + +Node CegConjecture::purifyConditionalEvaluations( Node n, std::map< Node, Node >& csol_cond, std::map< Node, Node >& psubs, std::map< Node, Node >& visited ){ + std::map< Node, Node >::iterator itv = visited.find( n ); + if( itv!=visited.end() ){ + return itv->second; + }else{ + Node ret; + if( n.getKind()==APPLY_UF ){ + std::map< Node, Node >::iterator itc = csol_cond.find( n[0] ); + if( itc!=csol_cond.end() ){ + //purify it with a variable + ret = NodeManager::currentNM()->mkSkolem( "y", n.getType(), "purification variable for sygus conditional solution" ); + psubs[n] = ret; + } + } + if( ret.isNull() ){ + ret = n; + if( n.getNumChildren()>0 ){ + std::vector< Node > children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + bool childChanged = false; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = purifyConditionalEvaluations( n[i], csol_cond, psubs, visited ); + childChanged = childChanged || nc!=n[i]; + children.push_back( nc ); + } + if( childChanged ){ + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + } + visited[n] = ret; + return ret; + } +} + +void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){ + Assert( lems.empty() ); + std::map< Node, Node > csol_cond; + std::map< Node, std::vector< Node > > csol_ccond; + std::map< Node, std::vector< Node > > csol_ccond_ret; + std::map< Node, std::map< Node, bool > > csol_cpol; + std::vector< Node > csol_vals; + if( options::cegqiUnifCondSol() ){ + std::vector< Node > new_active_measure_sum; + Trace("cegqi-unif") << "Conditional solution refinement, expand active conditional nodes" << std::endl; + for( unsigned i=0; i<d_candidates.size(); i++ ){ + Node v = d_candidates[i]; + Node ac = getActiveConditional( v ); + Assert( !ac.isNull() ); + //compute the contextual conditions + getContextConditionals( v, ac, csol_ccond[v], csol_ccond_ret[v], csol_cpol[v] ); + if( !csol_ccond[v].empty() ){ + //it will be conditionally evaluated, this is a placeholder + csol_cond[v] = Node::null(); + } + //if it is a conditional + if( !d_cinfo[ac].d_csol_cond.isNull() ){ + //activate + Trace("cegqi-unif") << "****** For " << v << ", expanding an active conditional node : " << ac << std::endl; + d_cinfo[ac].d_csol_status = 0; //TODO + Trace("cegqi-unif") << "...expanded to " << d_cinfo[ac].d_csol_op << "( "; + Trace("cegqi-unif") << d_cinfo[ac].d_csol_cond << ", " << d_cinfo[ac].d_csol_var[0] << ", "; + Trace("cegqi-unif") << d_cinfo[ac].d_csol_var[1] << " )" << std::endl; + registerCandidateConditional( d_cinfo[ac].d_csol_var[1-d_cinfo[ac].d_csol_status] ); + //add to measure sum + Node acfc = getMeasureTermFactor( d_cinfo[ac].d_csol_cond ); + if( !acfc.isNull() ){ + new_active_measure_sum.push_back( acfc ); + } + Node acfv = getMeasureTermFactor( d_cinfo[ac].d_csol_var[d_cinfo[ac].d_csol_status] ); + if( !acfv.isNull() ){ + new_active_measure_sum.push_back( acfv ); + } + csol_cond[v] = d_cinfo[ac].d_csol_cond; + csol_vals.push_back( d_cinfo[ac].d_csol_var[d_cinfo[ac].d_csol_status] ); + }else{ + Trace("cegqi-unif") << "* For " << v << ", its active node " << ac << " is not a conditional node." << std::endl; + //if we have not already included this in the measure, do so + if( d_cinfo[ac].d_csol_status==0 ){ + Node acf = getMeasureTermFactor( ac ); + if( !acf.isNull() ){ + new_active_measure_sum.push_back( acf ); + } + d_cinfo[ac].d_csol_status = 1; + } + csol_vals.push_back( ac ); + } + if( !csol_ccond[v].empty() ){ + Trace("cegqi-unif") << "...it is nested under " << csol_ccond[v].size() << " other conditionals" << std::endl; + } + } + // must add to active measure + if( !new_active_measure_sum.empty() ){ + 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))); + Node ramlem = d_active_measure_term.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, new_active_measure_sum ) ); + namlem = NodeManager::currentNM()->mkNode( kind::AND, ramlem, namlem ); + Trace("cegqi-lemma") << "Cegqi::Lemma : Measure expansion : " << namlem << std::endl; + d_qe->getOutputChannel().lemma( namlem ); + d_active_measure_term = new_active_measure; + } + } + 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<d_ce_sk.size(); j++ ){ + bool success = true; + std::vector< Node > lem_c; + Assert( d_ce_sk[j].size()==d_base_disj.size() ); + std::vector< Node > inst_cond_c; + for( unsigned k=0; k<d_ce_sk[j].size(); k++ ){ + Node ce_q = d_ce_sk[j][k]; + Trace("cegqi-refine") << " For counterexample point " << j << ", disjunct " << k << " : " << ce_q << " " << d_base_disj[k] << std::endl; + Node c_disj; + if( !ce_q.isNull() ){ + Assert( d_base_disj[k].getKind()==kind::NOT && d_base_disj[k][0].getKind()==kind::FORALL ); + c_disj = d_base_disj[k][0][1]; + }else{ + if( d_inner_vars_disj[k].empty() ){ + c_disj = d_base_disj[k].negate(); + }else{ + //denegrate case : quantified disjunct was trivially true and does not need to be refined + Trace("cegqi-refine") << "*** skip " << d_base_disj[k] << std::endl; + //add trivial substitution (in case we need substitution for previous cex's) + for( unsigned i=0; i<d_inner_vars_disj[k].size(); i++ ){ + sk_vars.push_back( d_inner_vars_disj[k][i] ); + sk_subs.push_back( getModelValue( d_inner_vars_disj[k][i] ) ); // will return dummy value + } + } + } + //compute the body, inst_cond + if( options::cegqiUnifCondSol() && !c_disj.isNull() ){ + Trace("cegqi-unif") << "Process " << c_disj << std::endl; + c_disj = purifyConditionalEvaluations( c_disj, csol_cond, psubs, psubs_visited ); + Trace("cegqi-unif") << "Purified to : " << c_disj << std::endl; + Trace("cegqi-unif") << "...now with " << psubs.size() << " definitions." << std::endl; + }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; + } + } + //add to the lemma + if( !c_disj.isNull() ){ + lem_c.push_back( c_disj ); + } + } + if( success ){ + Trace("cegqi-unif") << "Add conditional assumptions for " << psubs.size() << " evaluations." << std::endl; + //add conditional correctness assumptions + std::map< Node, Node > psubs_condc; + 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_cond.find( itp->first[0] )!=csol_cond.end() ); + paux_vars.push_back( itp->second ); + std::vector< Node > args; + for( unsigned a=1; a<itp->first.getNumChildren(); a++ ){ + args.push_back( itp->first[a] ); + } + Node c = csol_cond[itp->first[0]]; + psubs_apply[ c ].push_back( itp->first ); + Trace("cegqi-unif") << " process assumption " << itp->first << " == " << itp->second << ", with current condition " << c; + Trace("cegqi-unif") << ", and " << csol_ccond[itp->first[0]].size() << " context conditionals." << std::endl; + std::vector< Node> assm; + if( !c.isNull() ){ + assm.push_back( mkConditional( c, args ) ); + } + for( unsigned j=0; j<csol_ccond[itp->first[0]].size(); j++ ){ + Node cc = csol_ccond[itp->first[0]][j]; + assm.push_back( mkConditional( cc, args, csol_cpol[itp->first[0]][cc] ) ); + } + Assert( !assm.empty() ); + Node condn = assm.size()==1 ? assm[0] : NodeManager::currentNM()->mkNode( kind::AND, assm ); + Node cond = NodeManager::currentNM()->mkNode( kind::IMPLIES, condn, itp->first.eqNode( itp->second ) ); + psubs_condc[itp->first] = cond; + Trace("cegqi-unif") << " ...made conditional correctness assumption : " << cond << std::endl; + } + for( std::map< Node, Node >::iterator itp = psubs_condc.begin(); itp != psubs_condc.end(); ++itp ){ + lem_c.push_back( itp->second ); + } + + Node lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ); + //substitute the actual return values + if( options::cegqiUnifCondSol() ){ + Assert( d_candidates.size()==csol_vals.size() ); + lem = lem.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() ); + } + + //previous non-ground conditional refinement lemmas must satisfy the current point + for( unsigned i=0; i<d_refinement_lemmas.size(); i++ ){ + Node prev_lem = d_refinement_lemmas[i]; + prev_lem = prev_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + //do auxiliary variable substitution + std::vector< Node > subs; + for( unsigned ii=0; ii<d_refinement_lemmas_aux_vars[i].size(); ii++ ){ + subs.push_back( NodeManager::currentNM()->mkSkolem( "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 ); + prev_lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), prev_lem ); + Trace("cegqi-unif") << "...previous conditional refinement lemma with new counterexample : " << prev_lem << std::endl; + lems.push_back( prev_lem ); + } + if( !isGround() && !csol_cond.empty() ){ + Trace("cegqi-unif") << "Lemma " << lem << " is a non-ground conditional refinement lemma, store it for future instantiation." << std::endl; + d_refinement_lemmas.push_back( lem ); + d_refinement_lemmas_aux_vars.push_back( paux_vars ); + } + + if( options::cegqiUnifCondSol() ){ + Trace("cegqi-unif") << "We have lemma : " << lem << std::endl; + Trace("cegqi-unif") << "Now add progress assertions..." << std::endl; + std::vector< Node > prgr_conj; + std::map< Node, bool > cprocessed; + for( std::map< Node, Node >::iterator itc = csol_cond.begin(); itc !=csol_cond.end(); ++itc ){ + Node x = itc->first; + Node c = itc->second; + if( !c.isNull() ){ + Trace("cegqi-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; a<sbvl.getNumChildren(); a++ ){ + prgr_pt.push_back( NodeManager::currentNM()->mkSkolem( "kp", sbvl[a].getType(), "progress point for sygus conditional" ) ); + } + if( !psubs_apply[c].empty() ){ + std::vector< Node > prgr_domain_d; + for( unsigned j=0; j<psubs_apply[c].size(); j++ ){ + std::vector< Node > prgr_domain; + for( unsigned a=1; a<psubs_apply[c][j].getNumChildren(); a++ ){ + Assert( a<=prgr_pt.size() ); + prgr_domain.push_back( prgr_pt[a-1].eqNode( psubs_apply[c][j][a] ) ); + } + 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 ); + } + } + if( !prgr_domain_d.empty() ){ + //the progress point is in the domain of some function application + Node pdlem = prgr_domain_d.size()==1 ? prgr_domain_d[0] : NodeManager::currentNM()->mkNode( OR, prgr_domain_d ); + prgr_conj.push_back( pdlem ); + } + } + //the condition holds for the point + prgr_conj.push_back( mkConditional( c, prgr_pt ) ); + // ...and not for its context, if this return point is different from them + //for( unsigned j=0; j<csol_ccond[x].size(); j++ ){ + // Node cc = csol_ccond[x][j]; + // prgr_conj.push_back( mkConditional( cc, prgr_pt, csol_cpol[x][cc] ) ); + //} + //FIXME + } + } + 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( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() ); + Trace("cegqi-unif") << "Progress lemma is " << prgr_lem << std::endl; + lem = NodeManager::currentNM()->mkNode( kind::AND, lem, prgr_lem ); + } + //make in terms of new values + Assert( csol_vals.size()==d_candidates.size() ); + Trace("cegqi-unif") << "Now rewrite in terms of new evaluation branches...got " << lem << std::endl; + } + //apply the substitution + Assert( sk_vars.size()==sk_subs.size() ); + lem = lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem ); + lem = Rewriter::rewrite( 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; + Trace("cegqi-engine") << " * Value is : "; + for( unsigned i=0; i<n.size(); i++ ){ + Node nv = getModelValue( n[i] ); + v.push_back( nv ); + if( Trace.isOn("cegqi-engine") ){ + TypeNode tn = nv.getType(); + Trace("cegqi-engine") << n[i] << " -> "; + std::stringstream ss; + std::vector< Node > lvs; + TermDbSygus::printSygusTerm( ss, nv, lvs ); + Trace("cegqi-engine") << ss.str() << " "; + } + if( nv.isNull() ){ + Trace("cegqi-warn") << "WARNING: failed getModelValues." << std::endl; + success = false; + } + } + Trace("cegqi-engine") << std::endl; + return success; +} + +Node CegConjecture::getModelValue( Node n ) { + Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; + return d_qe->getModel()->getValue( n ); +} + +void CegConjecture::debugPrint( const char * c ) { + Trace(c) << "Synthesis conjecture : " << d_quant << std::endl; + Trace(c) << " * Candidate program/output symbol : "; + for( unsigned i=0; i<d_candidates.size(); i++ ){ + Trace(c) << d_candidates[i] << " "; + } + Trace(c) << std::endl; + Trace(c) << " * Candidate ce skolems : "; + for( unsigned i=0; i<d_ce_sk.size(); i++ ){ + Trace(c) << d_ce_sk[i] << " "; + } +} + CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ d_conj = new CegConjecture( qe, qe->getSatContext() ); d_last_inst_si = false; @@ -315,26 +932,32 @@ void CegInstantiation::registerQuantifier( Node q ) { //fairness if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ std::vector< Node > mc; - for( unsigned j=0; j<d_conj->d_candidates.size(); j++ ){ - TypeNode tn = d_conj->d_candidates[j].getType(); - if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE ){ - if( tn.isDatatype() ){ - mc.push_back( NodeManager::currentNM()->mkNode( DT_SIZE, d_conj->d_candidates[j] ) ); - } - }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){ - registerMeasuredType( tn ); - std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn ); - if( it!=d_uf_measure.end() ){ - mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) ); + if( options::cegqiUnifCondSol() || + d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED ){ + //measure term is a fresh constant + mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) ); + }else{ + std::vector< Node > clist; + d_conj->getCandidateList( clist, true ); + for( unsigned j=0; j<clist.size(); j++ ){ + TypeNode tn = clist[j].getType(); + if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE ){ + if( tn.isDatatype() ){ + mc.push_back( NodeManager::currentNM()->mkNode( DT_SIZE, clist[j] ) ); + } + }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){ + registerMeasuredType( tn ); + std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn ); + if( it!=d_uf_measure.end() ){ + mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, clist[j] ) ); + } } - }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED ){ - //measure term is a fresh constant - mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) ); } } if( !mc.empty() ){ - d_conj->d_measure_term = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc ); - Trace("cegqi") << "Measure term is : " << d_conj->d_measure_term << std::endl; + Node mt = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc ); + Trace("cegqi") << "Measure term is : " << mt << std::endl; + d_conj->setMeasureTerm( mt ); } } }else{ @@ -351,7 +974,7 @@ void CegInstantiation::assertNode( Node n ) { Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) { //enforce fairness if( d_conj->isAssigned() ){ - d_conj->initializeGuard( d_quantEngine ); + d_conj->initializeGuard(); std::vector< Node > req_dec; const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv(); if( ! ceg_si->d_full_guard.isNull() ){ @@ -374,12 +997,12 @@ Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) { } if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ - Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); + Node lit = d_conj->getFairnessLiteral( d_conj->getCurrentTermSize() ); bool value; if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { if( !value ){ - d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 ); - lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); + d_conj->incrementCurrentTermSize(); + lit = d_conj->getFairnessLiteral( d_conj->getCurrentTermSize() ); Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl; priority = 1; return lit; @@ -398,47 +1021,43 @@ Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) { void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Node q = conj->d_quant; Node aq = conj->d_assert_quant; - Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl; - Trace("cegqi-engine-debug") << " * Candidate program/output symbol : "; - for( unsigned i=0; i<conj->d_candidates.size(); i++ ){ - Trace("cegqi-engine-debug") << conj->d_candidates[i] << " "; - } - Trace("cegqi-engine-debug") << std::endl; - Trace("cegqi-engine-debug") << " * Candidate ce skolems : "; - for( unsigned i=0; i<conj->d_ce_sk.size(); i++ ){ - Trace("cegqi-engine-debug") << conj->d_ce_sk[i] << " "; + if( Trace.isOn("cegqi-engine-debug") ){ + conj->debugPrint("cegqi-engine-debug"); + Trace("cegqi-engine-debug") << std::endl; } - Trace("cegqi-engine-debug") << std::endl; if( conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ - Trace("cegqi-engine") << " * Current term size : " << conj->d_curr_lit.get() << std::endl; - } + Trace("cegqi-engine") << " * Current term size : " << conj->getCurrentTermSize() << std::endl; + } - if( conj->d_ce_sk.empty() ){ - Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; + if( !conj->needsRefinement() ){ if( conj->d_syntax_guided ){ - if( conj->getCegConjectureSingleInv() != NULL ){ - std::vector< Node > lems; - if( conj->doCegConjectureCheck( lems ) ){ - if( !lems.empty() ){ - d_last_inst_si = true; - for( unsigned j=0; j<lems.size(); j++ ){ - Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation instantiation : " << lems[j] << std::endl; - d_quantEngine->addLemma( lems[j] ); - } - d_statistics.d_cegqi_si_lemmas += lems.size(); - Trace("cegqi-engine") << " ...try single invocation." << std::endl; - } - return; + std::vector< Node > clems; + conj->doCegConjectureSingleInvCheck( clems ); + if( !clems.empty() ){ + d_last_inst_si = true; + for( unsigned j=0; j<clems.size(); j++ ){ + Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation instantiation : " << clems[j] << std::endl; + d_quantEngine->addLemma( clems[j] ); } + d_statistics.d_cegqi_si_lemmas += clems.size(); + Trace("cegqi-engine") << " ...try single invocation." << std::endl; + return; } + //ignore return value here + std::vector< Node > clist; + conj->getCandidateList( clist ); std::vector< Node > model_values; - if( getModelValues( conj, conj->d_candidates, model_values ) ){ + if( conj->getModelValues( clist, model_values ) ){ if( options::sygusDirectEval() ){ + Trace("cegqi-debug") << "Do direct evaluation..." << std::endl; std::vector< Node > eager_eval_lem; - for( unsigned j=0; j<conj->d_candidates.size(); j++ ){ - d_quantEngine->getTermDatabaseSygus()->registerModelValue( conj->d_candidates[j], model_values[j], eager_eval_lem ); + for( unsigned j=0; j<clist.size(); j++ ){ + Trace("cegqi-debug") << " register " << clist[j] << " -> " << model_values[j] << std::endl; + d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_eval_lem ); } + Trace("cegqi-debug") << "...produced " << eager_eval_lem.size() << " eager evaluation lemmas." << std::endl; if( !eager_eval_lem.empty() ){ + Trace("cegqi-engine") << " *** Do direct evaluation..." << std::endl; for( unsigned j=0; j<eager_eval_lem.size(); j++ ){ Node lem = eager_eval_lem[j]; if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){ @@ -453,11 +1072,15 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } //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<conj->d_candidates.size(); j++ ){ - getMeasureLemmas( conj->d_candidates[j], model_values[j], lems ); + for( unsigned j=0; j<clist.size(); j++ ){ + Trace("cegqi-debug") << " get measure lemmas for " << clist[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; j<lems.size(); j++ ){ Trace("cegqi-lemma") << "Cegqi::Lemma : measure : " << lems[j] << std::endl; d_quantEngine->addLemma( lems[j] ); @@ -466,156 +1089,75 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { return; } } - //must get a counterexample to the value of the current candidate - Assert( conj->d_candidates.size()==model_values.size() ); - Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() ); - //check whether we will run CEGIS on inner skolem variables - bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 ); - if( sk_refine ){ - conj->d_ce_sk.push_back( std::vector< Node >() ); - } - std::vector< Node > ic; - ic.push_back( aq.negate() ); - std::vector< Node > d; - collectDisjuncts( inst, d ); - Assert( d.size()==conj->d_base_disj.size() ); - //immediately skolemize inner existentials - for( unsigned i=0; i<d.size(); i++ ){ - Node dr = Rewriter::rewrite( d[i] ); - if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){ - ic.push_back( getTermDatabase()->getSkolemizedBody( dr[0] ).negate() ); - if( sk_refine ){ - conj->d_ce_sk.back().push_back( dr[0] ); - } + + 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<cclems.size(); i++ ){ + Node lem = cclems[i]; + d_last_inst_si = false; + //eagerly unfold applications of evaluation function + if( options::sygusDirectEval() ){ + Trace("cegqi-eager") << "pre-unfold counterexample : " << lem << std::endl; + std::map< Node, Node > 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{ - ic.push_back( dr ); - if( sk_refine ){ - conj->d_ce_sk.back().push_back( Node::null() ); - } - if( !conj->d_inner_vars_disj[i].empty() ){ - Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl; + //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; } } } - Node lem = NodeManager::currentNM()->mkNode( OR, ic ); - lem = Rewriter::rewrite( lem ); - d_last_inst_si = false; - //eagerly unfold applications of evaluation function - if( options::sygusDirectEval() ){ - Trace("cegqi-eager") << "pre-unfold counterexample : " << lem << std::endl; - std::map< Node, Node > 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); - Trace("cegqi-engine") << " ...find counterexample." << std::endl; + if( addedLemma ){ + Trace("cegqi-engine") << " ...check for counterexample." << std::endl; }else{ - //this may happen if we eagerly unfold, simplify to true - if( !options::sygusDirectEval() ){ - Trace("cegqi-engine") << " ...FAILED to add candidate!" << std::endl; - }else{ - Trace("cegqi-engine-debug") << " ...FAILED to add candidate!" << std::endl; - } - if( conj->d_refine_count==0 ){ + if( conj->needsRefinement() ){ //immediately go to refine candidate checkCegConjecture( conj ); return; } - } + } } - }else{ Assert( aq==q ); std::vector< Node > model_terms; - if( getModelValues( conj, conj->d_candidates, model_terms ) ){ + std::vector< Node > clist; + conj->getCandidateList( clist, true ); + Assert( clist.size()==q[0].getNumChildren() ); + if( conj->getModelValues( clist, model_terms ) ){ + conj->recordInstantiation( model_terms ); d_quantEngine->addInstantiation( q, model_terms ); } } }else{ Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl; - for( unsigned j=0; j<conj->d_ce_sk.size(); j++ ){ - bool success = true; - std::vector< Node > lem_c; - Assert( conj->d_ce_sk[j].size()==conj->d_base_disj.size() ); - for( unsigned k=0; k<conj->d_ce_sk[j].size(); k++ ){ - Node ce_q = conj->d_ce_sk[j][k]; - Node c_disj = conj->d_base_disj[k]; - if( !ce_q.isNull() ){ - Assert( !conj->d_inner_vars_disj[k].empty() ); - Assert( conj->d_inner_vars_disj[k].size()==getTermDatabase()->d_skolem_constants[ce_q].size() ); - std::vector< Node > model_values; - if( getModelValues( NULL, getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){ - //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate - Node inst_ce_refine = conj->d_base_disj[k][0][1].substitute( conj->d_inner_vars_disj[k].begin(), conj->d_inner_vars_disj[k].end(), - model_values.begin(), model_values.end() ); - lem_c.push_back( inst_ce_refine ); - }else{ - success = false; - break; - } - }else{ - if( conj->d_inner_vars_disj[k].empty() ){ - lem_c.push_back( conj->d_base_disj[k].negate() ); - }else{ - //denegrate case : quantified disjunct was trivially true and does not need to be refined - Trace("cegqi-debug") << "*** skip " << conj->d_base_disj[k] << std::endl; - } - } - } - if( success ){ - Node lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ); - lem = NodeManager::currentNM()->mkNode( OR, conj->getGuard().negate(), lem ); - lem = Rewriter::rewrite( lem ); - Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl; - Trace("cegqi-engine") << " ...refine candidate." << std::endl; - bool res = d_quantEngine->addLemma( lem ); - if( res ){ - ++(d_statistics.d_cegqi_lemmas_refine); - conj->d_refine_count++; - }else{ - Trace("cegqi-engine") << " ...FAILED to add refinement!" << std::endl; - } + std::vector< Node > rlems; + conj->doCegConjectureRefine( rlems ); + bool addedLemma = false; + for( unsigned i=0; i<rlems.size(); i++ ){ + Node lem = rlems[i]; + Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl; + bool res = d_quantEngine->addLemma( lem ); + if( res ){ + ++(d_statistics.d_cegqi_lemmas_refine); + conj->d_refine_count++; + addedLemma = true; + }else{ + Trace("cegqi-warn") << " ...FAILED to add refinement!" << std::endl; } } - conj->d_ce_sk.clear(); - } -} - -bool CegInstantiation::getModelValues( CegConjecture * conj, std::vector< Node >& n, std::vector< Node >& v ) { - bool success = true; - Trace("cegqi-engine") << " * Value is : "; - for( unsigned i=0; i<n.size(); i++ ){ - Node nv = getModelValue( n[i] ); - v.push_back( nv ); - if( Trace.isOn("cegqi-engine") ){ - TypeNode tn = nv.getType(); - Trace("cegqi-engine") << n[i] << " -> "; - std::stringstream ss; - std::vector< Node > lvs; - TermDbSygus::printSygusTerm( ss, nv, lvs ); - Trace("cegqi-engine") << ss.str() << " "; - } - if( nv.isNull() ){ - success = false; - } - if( conj ){ - conj->d_candidate_inst[i].push_back( nv ); + if( addedLemma ){ + Trace("cegqi-engine") << " ...refine candidate." << std::endl; } } - Trace("cegqi-engine") << std::endl; - return success; -} - -Node CegInstantiation::getModelValue( Node n ) { - Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; - return d_quantEngine->getModel()->getValue( n ); -} - -Node CegInstantiation::getModelTerm( Node n ){ - //TODO - return getModelValue( n ); } void CegInstantiation::registerMeasuredType( TypeNode tn ) { @@ -710,13 +1252,7 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited ) } for( unsigned j=1; j<n.getNumChildren(); j++ ){ Node nc = getEagerUnfold( n[j], visited ); - //if( var_list[j-1].getType().isBoolean() ){ - // //TODO: remove this case when boolean term conversion is eliminated - // Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); - // subs.push_back( nc.eqNode( c ) ); - //}else{ subs.push_back( nc ); - //} Assert( subs[j-1].getType()==var_list[j-1].getType() ); } Assert( vars.size()==subs.size() ); @@ -763,6 +1299,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { //} for( unsigned i=0; i<d_conj->d_quant[0].getNumChildren(); i++ ){ Node prog = d_conj->d_quant[0][i]; + Trace("cegqi-debug") << " print solution for " << prog << std::endl; std::stringstream ss; ss << prog; std::string f(ss.str()); @@ -779,8 +1316,9 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { sol = d_conj->getSingleInvocationSolution( 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(); + Node cprog = d_conj->getCandidate( i ); + if( !d_conj->d_cinfo[cprog].d_inst.empty() ){ + sol = d_conj->d_cinfo[cprog].d_inst.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 ){ @@ -844,6 +1382,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { }else{ status = 1; } + }else{ + Trace("cegqi-warn") << "WARNING : No recorded instantiations for syntax-guided solution!" << std::endl; } } if( !(Trace.isOn("cegqi-stats")) ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 7f36f4d25..f49298411 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -31,6 +31,37 @@ namespace quantifiers { class CegConjecture { private: QuantifiersEngine * d_qe; + /** list of constants for quantified formula */ + std::vector< Node > d_candidates; + /** base instantiation */ + Node d_base_inst; + /** expand base inst to disjuncts */ + std::vector< Node > d_base_disj; + /** list of variables on inner quantification */ + std::vector< Node > d_inner_vars; + std::vector< std::vector< Node > > d_inner_vars_disj; + /** current extential quantifeirs whose couterexamples we must refine */ + std::vector< std::vector< Node > > d_ce_sk; + /** the cardinality literals */ + std::map< int, Node > d_lits; + /** current cardinality */ + context::CDO< int > d_curr_lit; + /** active measure term */ + Node d_active_measure_term; + /** refinement lemmas */ + std::vector< Node > d_refinement_lemmas; + std::vector< std::vector< Node > > d_refinement_lemmas_aux_vars; +private: //for condition solutions + /** 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 ); + Node getActiveConditional( Node curr ); + void getContextConditionals( Node curr, Node x, std::vector< Node >& conds, std::vector< Node >& rets, std::map< Node, bool >& cpols ); + Node mkConditional( Node c, std::vector< Node >& args, bool pol = true ); + Node purifyConditionalEvaluations( Node n, std::map< Node, Node >& csol_cond, std::map< Node, Node >& psubs, + std::map< Node, Node >& visited ); + /** register candidate conditional */ + void registerCandidateConditional( Node v ); public: CegConjecture( QuantifiersEngine * qe, context::Context* c ); ~CegConjecture(); @@ -39,33 +70,41 @@ public: Node d_assert_quant; /** quantified formula (after processing) */ Node d_quant; - /** base instantiation */ - Node d_base_inst; - /** expand base inst to disjuncts */ - std::vector< Node > d_base_disj; - /** list of constants for quantified formula */ - std::vector< Node > d_candidates; - /** list of variables on inner quantification */ - std::vector< Node > d_inner_vars; - std::vector< std::vector< Node > > d_inner_vars_disj; - /** list of terms we have instantiated candidates with */ - std::map< int, std::vector< Node > > d_candidate_inst; + + class CandidateInfo { + public: + CandidateInfo() : d_csol_status(-1){} + /** list of terms we have instantiated candidates with */ + std::vector< Node > d_inst; + /** conditional solutions */ + Node d_csol_op; + Node d_csol_cond; + Node d_csol_var[2]; + /** solution status */ + int d_csol_status; + }; + std::map< Node, CandidateInfo > d_cinfo; + /** measure term */ Node d_measure_term; /** measure sum size */ int d_measure_term_size; /** refine count */ unsigned d_refine_count; - /** current extential quantifeirs whose couterexamples we must refine */ - std::vector< std::vector< Node > > d_ce_sk; + /** incomplete candidate values */ + bool d_incomplete_candidate_values; const CegConjectureSingleInv* getCegConjectureSingleInv() const { return d_ceg_si; } + + 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 ); - bool doCegConjectureCheck(std::vector< Node >& lems) { - return d_ceg_si->check(lems); - } + void doCegConjectureSingleInvCheck(std::vector< Node >& lems); + void doCegConjectureCheck(std::vector< Node >& lems, std::vector< Node >& model_values); + void doCegConjectureRefine(std::vector< Node >& lems); Node getSingleInvocationSolution(unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus=true){ @@ -80,21 +119,36 @@ public: 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++ ){ + d_cinfo[d_candidates[i]].d_inst.push_back( vs[i] ); + } + } + Node getCandidate( unsigned int i ) { return d_candidates[i]; } + + void debugPrint( const char * c ); - private: +private: /** single invocation utility */ CegConjectureSingleInv * d_ceg_si; public: //non-syntax guided (deprecated) /** guard */ bool d_syntax_guided; Node d_nsg_guard; -public: //for fairness - /** the cardinality literals */ - std::map< int, Node > d_lits; - /** current cardinality */ - context::CDO< int > d_curr_lit; +public: + /** get current term size */ + int getCurrentTermSize() { return d_curr_lit.get(); } + /** increment current term size */ + void incrementCurrentTermSize() { d_curr_lit.set( d_curr_lit.get() + 1 ); } + /** set measure term */ + void setMeasureTerm( Node mt ); + /** get measure term */ + Node getMeasureTermFactor( Node v ); + Node getMeasureTerm() { return d_measure_term; } /** allocate literal */ - Node getLiteral( QuantifiersEngine * qe, int i ); + Node getFairnessLiteral( int i ); /** get guard */ Node getGuard(); /** is ground */ @@ -110,11 +164,15 @@ public: //for fairness /** preregister conjecture */ void preregisterConjecture( Node q ); /** initialize guard */ - void initializeGuard( QuantifiersEngine * qe ); + void initializeGuard(); /** assign */ void assign( Node q ); /** is assigned */ bool isAssigned() { return !d_quant.isNull(); } + /** get model values */ + bool getModelValues( std::vector< Node >& n, std::vector< Node >& v ); + /** get model value */ + Node getModelValue( Node n ); }; @@ -146,12 +204,6 @@ private: //for enforcing fairness private: /** check conjecture */ void checkCegConjecture( CegConjecture * conj ); - /** get model values */ - bool getModelValues( CegConjecture * conj, std::vector< Node >& n, std::vector< Node >& v ); - /** get model value */ - Node getModelValue( Node n ); - /** get model term */ - Node getModelTerm( Node n ); public: CegInstantiation( QuantifiersEngine * qe, context::Context* c ); ~CegInstantiation(); diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 92d62a177..84743fc1d 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -758,13 +758,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() ); for( unsigned i=0; i<d_single_inv_arg_sk.size(); i++ ){ Trace("csi-sol") << d_single_inv_arg_sk[i] << " "; - //if( varList[i].getType().isBoolean() ){ - // //TODO force boolean term conversion mode - // Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); - // vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) ); - //}else{ vars.push_back( d_single_inv_arg_sk[i] ); - //} d_sol->d_varList.push_back( varList[i] ); } Trace("csi-sol") << std::endl; diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index d93898a1e..8ecd32ab1 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -215,7 +215,7 @@ Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) { if( n0.getKind()==ITE ){ n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ), NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) ); - }else if( n0.getKind()==EQUAL ){ + }else if( n0.getKind()==EQUAL && n0[0].getType().isBoolean() ){ n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ), NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) ); }else{ |