From 620ebbaf88f07abc36399499cfa6dfef8c3369d9 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 22 Mar 2017 08:52:42 -0500 Subject: [PATCH] Work on new approach for sygus involving conditional solutions. Refactoring of sygus solver. Bug fix for sygus solution reconstruction. --- src/expr/datatype.cpp | 25 +- src/expr/datatype.h | 3 + src/options/quantifiers_options | 2 + src/parser/smt2/Smt2.g | 14 +- .../quantifiers/ce_guided_instantiation.cpp | 938 ++++++++++++++---- .../quantifiers/ce_guided_instantiation.h | 112 ++- .../quantifiers/ce_guided_single_inv.cpp | 6 - .../quantifiers/ce_guided_single_inv_sol.cpp | 2 +- 8 files changed, 850 insertions(+), 252 deletions(-) diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index ac93114b7..8a6d5d4a3 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -145,6 +145,23 @@ void Datatype::resolve(ExprManager* em, } d_record = new Record(fields); } + + //make the sygus evaluation function + if( isSygus() ){ + PrettyCheckArgument(d_params.empty(), this, "sygus types cannot be parametric"); + NodeManager* nm = NodeManager::fromExprManager(em); + std::string name = "eval_" + getName(); + std::vector evalType; + evalType.push_back(TypeNode::fromType(d_self)); + if( !d_sygus_bvl.isNull() ){ + for(size_t j = 0; j < d_sygus_bvl.getNumChildren(); ++j) { + evalType.push_back(TypeNode::fromType(d_sygus_bvl[j].getType())); + } + } + evalType.push_back(TypeNode::fromType(d_sygus_type)); + TypeNode eval_func_type = nm->mkFunctionType(evalType); + d_sygus_eval = nm->mkSkolem(name, eval_func_type, "sygus evaluation function").toExpr(); + } } void Datatype::addConstructor(const DatatypeConstructor& c) { @@ -156,7 +173,7 @@ void Datatype::addConstructor(const DatatypeConstructor& c) { void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ PrettyCheckArgument(!d_resolved, this, - "cannot set sygus type to a finalized Datatype"); + "cannot set sygus type to a finalized Datatype"); d_sygus_type = st; d_sygus_bvl = bvl; d_sygus_allow_const = allow_const || allow_all; @@ -394,9 +411,7 @@ bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); ExprManagerScope ems(d_self); - Debug("datatypes") << "mkGroundTerm of type " << t << std::endl; - // is this already in the cache ? std::map< Type, Expr >::iterator it = d_ground_term.find( t ); if( it != d_ground_term.end() ){ @@ -589,6 +604,10 @@ bool Datatype::getSygusAllowAll() const { return d_sygus_allow_const; } +Expr Datatype::getSygusEvaluationFunc() const { + return d_sygus_eval; +} + bool Datatype::involvesExternalType() const{ return d_involvesExt; } diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 5a09730d0..88c72ea59 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -491,6 +491,7 @@ private: Expr d_sygus_bvl; bool d_sygus_allow_const; bool d_sygus_allow_all; + Expr d_sygus_eval; // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache @@ -744,6 +745,8 @@ public: bool getSygusAllowConst() const; /** does it allow constants */ bool getSygusAllowAll() const; + /** get the evaluation function for this datatype for the deep embedding */ + Expr getSygusEvaluationFunc() const; /** * Get whether this datatype involves an external type. If so, diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index cf8fca2fa..585ef3dc2 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -253,6 +253,8 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default include constants when reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvAbort --cegqi-si-abort bool :default false abort if synthesis conjecture is not single invocation +option cegqiUnifCondSol --cegqi-unif-csol bool :default false + enable approach which unifies conditional solutions option sygusNormalForm --sygus-nf bool :default true only search for sygus builtin terms that are in normal form diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 15495265e..33674770d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -730,19 +730,7 @@ sygusCommand [CVC4::PtrCloser* cmd] for(size_t i = 0; i < datatypeTypes.size(); ++i) { DatatypeType dtt = datatypeTypes[i]; const Datatype& dt = dtt.getDatatype(); - name = "eval_" + dt.getName(); - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - std::vector evalType; - evalType.push_back(dtt); - if( !terms[0].isNull() ){ - for(size_t j = 0; j < terms[0].getNumChildren(); ++j) { - evalType.push_back(terms[0][j].getType()); - } - } - evalType.push_back(sorts[i]); - const FunctionType eval_func_type = - EXPR_MANAGER->mkFunctionType(evalType); - Expr eval = PARSER_STATE->mkVar(name, eval_func_type); + Expr eval = dt.getSygusEvaluationFunc(); Debug("parser-sygus") << "Make eval " << eval << " for " << dt.getName() << std::endl; evals.insert(std::make_pair(dtt, eval)); 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() ); //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; igetTermDatabase()->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; jmkSkolem( "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; igetOutputChannel().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& 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& 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[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; igetTermDatabase()->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; amkNode( 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; imkNode( 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; imkSkolem( "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 lem_c; + Assert( d_ce_sk[j].size()==d_base_disj.size() ); + std::vector< Node > inst_cond_c; + for( unsigned k=0; kgetTermDatabase()->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; afirst.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; jfirst[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 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 ); + 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; amkSkolem( "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 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 + 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; jmkNode( 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 "; + 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; igetSatContext() ); 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; jd_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; jgetCegqiFairMode()==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; id_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; id_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; jaddLemma( 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; jaddLemma( 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; jd_candidates.size(); j++ ){ - d_quantEngine->getTermDatabaseSygus()->registerModelValue( conj->d_candidates[j], model_values[j], eager_eval_lem ); + for( unsigned j=0; 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; jgetTheoryEngine()->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; jd_candidates.size(); j++ ){ - getMeasureLemmas( conj->d_candidates[j], model_values[j], 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] ); @@ -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; igetSkolemizedBody( 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 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; jd_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; kd_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; iaddLemma( 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 "; - 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; jmkConst(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; id_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& 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 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; imkConst(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{ -- 2.30.2