diff options
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 255 |
1 files changed, 185 insertions, 70 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index f4cdd1a60..babfe3f40 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -27,7 +27,8 @@ using namespace std; namespace CVC4 { -CegInstantiation::CegConjecture::CegConjecture() { +CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){ + } void CegInstantiation::CegConjecture::assign( Node q ) { @@ -38,6 +39,7 @@ void CegInstantiation::CegConjecture::assign( Node q ) { d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) ); } } + void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ if( d_guard.isNull() ){ d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); @@ -47,8 +49,25 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ } } -CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), d_conj_active( c, false ), d_conj_infeasible( c, false ), d_guard_assertions( c ) { +Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { + std::map< int, Node >::iterator it = d_lits.find( i ); + if( it==d_lits.end() ){ + Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i + d_measure_term_size ) ) ); + lit = Rewriter::rewrite( lit ); + d_lits[i] = lit; + + Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() ); + Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl; + qe->getOutputChannel().lemma( lem ); + qe->getOutputChannel().requirePhase( lit, true ); + return lit; + }else{ + return it->second; + } +} +CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ + d_conj = new CegConjecture( d_quantEngine->getSatContext() ); } bool CegInstantiation::needsCheck( Theory::Effort e ) { @@ -58,9 +77,10 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) { void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ Trace("cegqi-engine") << "---Countexample Guided Instantiation Engine---" << std::endl; - Trace("cegqi-debug") << "Current conjecture status : " << d_conj_active << " " << d_conj_infeasible << std::endl; - if( d_conj_active && !d_conj_infeasible ){ - checkCegConjecture( &d_conj ); + Trace("cegqi-engine-debug") << std::endl; + Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl; + if( d_conj->d_active && !d_conj->d_infeasible ){ + checkCegConjecture( d_conj ); } Trace("cegqi-engine") << "Finished Countexample Guided Instantiation engine." << std::endl; } @@ -68,24 +88,44 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { void CegInstantiation::registerQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==this ){ - if( !d_conj.isAssigned() ){ + if( !d_conj->isAssigned() ){ Trace("cegqi") << "Register conjecture : " << q << std::endl; - d_conj.assign( q ); + d_conj->assign( q ); //construct base instantiation - d_conj.d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj.d_candidates ) ); - Trace("cegqi") << "Base instantiation is : " << d_conj.d_base_inst << std::endl; + d_conj->d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj->d_candidates ) ); + Trace("cegqi") << "Base instantiation is : " << d_conj->d_base_inst << std::endl; if( getTermDatabase()->isQAttrSygus( q ) ){ - Assert( d_conj.d_base_inst.getKind()==NOT ); - Assert( d_conj.d_base_inst[0].getKind()==FORALL ); - for( unsigned j=0; j<d_conj.d_base_inst[0][0].getNumChildren(); j++ ){ - d_conj.d_inner_vars.push_back( d_conj.d_base_inst[0][0][j] ); + Assert( d_conj->d_base_inst.getKind()==NOT ); + Assert( d_conj->d_base_inst[0].getKind()==FORALL ); + for( unsigned j=0; j<d_conj->d_base_inst[0][0].getNumChildren(); j++ ){ + d_conj->d_inner_vars.push_back( d_conj->d_base_inst[0][0][j] ); } }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ //add immediate lemma - Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_base_inst ); + Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_base_inst ); + d_quantEngine->getOutputChannel().lemma( lem ); + } + //fairness + std::vector< Node > mc; + for( unsigned j=0; j<d_conj->d_candidates.size(); j++ ){ + TypeNode tn = d_conj->d_candidates[j].getType(); + 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( !mc.empty() ){ + d_conj->d_measure_term = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc ); + d_conj->d_measure_term_size = mc.size(); + Trace("cegqi") << "Measure term is : " << d_conj->d_measure_term << std::endl; + //Node ax = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), d_conj->d_measure_term ); + //ax = Rewriter::rewrite( ax ); + //Trace("cegqi-lemma") << "Fairness non-negative axiom : " << ax << std::endl; + //d_quantEngine->getOutputChannel().lemma( ax ); } }else{ - Assert( d_conj.d_quant==q ); + Assert( d_conj->d_quant==q ); } } } @@ -94,83 +134,113 @@ void CegInstantiation::assertNode( Node n ) { Trace("cegqi-debug") << "Cegqi : Assert : " << n << std::endl; bool pol = n.getKind()!=NOT; Node lit = n.getKind()==NOT ? n[0] : n; - if( lit==d_conj.d_guard ){ - d_guard_assertions[lit] = pol; - d_conj_infeasible = !pol; + if( lit==d_conj->d_guard ){ + //d_guard_assertions[lit] = pol; + d_conj->d_infeasible = !pol; } - if( lit==d_conj.d_quant ){ - d_conj_active = true; + if( lit==d_conj->d_quant ){ + d_conj->d_active = true; } } Node CegInstantiation::getNextDecisionRequest() { - d_conj.initializeGuard( d_quantEngine ); + d_conj->initializeGuard( d_quantEngine ); bool value; - if( !d_quantEngine->getValuation().hasSatValue( d_conj.d_guard, value ) ) { - if( d_guard_assertions.find( d_conj.d_guard )==d_guard_assertions.end() ){ - if( d_conj.d_guard_split.isNull() ){ - Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_guard ); - d_quantEngine->getOutputChannel().lemma( lem ); + if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) { + if( d_conj->d_guard_split.isNull() ){ + Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard ); + d_quantEngine->getOutputChannel().lemma( lem ); + } + Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl; + return d_conj->d_guard; + } + //enforce fairness + if( d_conj->isAssigned() ){ + Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); + 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() ); + Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl; + return lit; } - Trace("cegqi-debug") << "Decide next on : " << d_conj.d_guard << "..." << std::endl; - return d_conj.d_guard; + }else{ + Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl; + return lit; } } + return Node::null(); } void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Node q = conj->d_quant; - Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl; - Trace("cegqi-engine-debug") << " * Candidate program/output : "; + Trace("cegqi-engine") << "Synthesis conjecture : " << q << std::endl; + Trace("cegqi-engine") << " * 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") << conj->d_candidates[i] << " "; } - Trace("cegqi-engine-debug") << std::endl; - - if( getTermDatabase()->isQAttrSygus( q ) ){ - Trace("cegqi-engine-debug") << " * Values are : "; - bool success = true; - std::vector< Node > model_values; - for( unsigned i=0; i<conj->d_candidates.size(); i++ ){ - Node v = getModelValue( conj->d_candidates[i] ); - model_values.push_back( v ); - Trace("cegqi-engine-debug") << v << " "; - if( v.isNull() ){ - success = false; + Trace("cegqi-engine") << std::endl; + + if( conj->d_ce_sk.empty() ){ + Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; + if( getTermDatabase()->isQAttrSygus( q ) ){ + + std::vector< Node > model_values; + if( getModelValues( conj->d_candidates, model_values ) ){ + //must get a counterexample to the value of the current candidate + Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() ); + inst = Rewriter::rewrite( inst ); + //body should be an existential + Assert( inst.getKind()==NOT ); + Assert( inst[0].getKind()==FORALL ); + //immediately skolemize + Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] ); + Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl; + d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk.negate() ) ); + conj->d_ce_sk.push_back( inst[0] ); } - } - Trace("cegqi-engine-debug") << std::endl; - if( success ){ - //must get a counterexample to the value of the current candidate - Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() ); - inst = Rewriter::rewrite( inst ); - //body should be an existential - Assert( inst.getKind()==NOT ); - Assert( inst[0].getKind()==FORALL ); - //immediately skolemize - Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] ); - Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl; - d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) ); - - //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate - Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[inst[0]].size() ); - Node inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(), - getTermDatabase()->d_skolem_constants[inst[0]].begin(), getTermDatabase()->d_skolem_constants[inst[0]].end() ); - Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine.negate() ); - Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl; - d_quantEngine->addLemma( lem ); + }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ + std::vector< Node > model_terms; + for( unsigned i=0; i<conj->d_candidates.size(); i++ ){ + Node t = getModelTerm( conj->d_candidates[i] ); + model_terms.push_back( t ); + } + d_quantEngine->addInstantiation( q, model_terms, false ); } + }else{ + Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl; + for( unsigned j=0; j<conj->d_ce_sk.size(); j++ ){ + Node ce_q = conj->d_ce_sk[j]; + Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[ce_q].size() ); + std::vector< Node > model_values; + if( getModelValues( 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_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(), + model_values.begin(), model_values.end() ); + Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine ); + Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl; + d_quantEngine->addLemma( lem ); + } + } + conj->d_ce_sk.clear(); + } +} - }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ - std::vector< Node > model_terms; - for( unsigned i=0; i<conj->d_candidates.size(); i++ ){ - Node t = getModelTerm( conj->d_candidates[i] ); - model_terms.push_back( t ); +bool CegInstantiation::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 ); + Trace("cegqi-engine") << nv << " "; + if( nv.isNull() ){ + success = false; } - d_quantEngine->addInstantiation( q, model_terms, false ); } + Trace("cegqi-engine") << std::endl; + return success; } Node CegInstantiation::getModelValue( Node n ) { @@ -210,7 +280,52 @@ Node CegInstantiation::getModelValue( Node n ) { } Node CegInstantiation::getModelTerm( Node n ){ + //TODO return getModelValue( n ); } +void CegInstantiation::registerMeasuredType( TypeNode tn ) { + std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn ); + if( it==d_uf_measure.end() ){ + if( tn.isDatatype() ){ + TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->integerType() ); + Node op = NodeManager::currentNM()->mkSkolem( "tsize", op_tn, "was created by ceg instantiation to enforce fairness." ); + d_uf_measure[tn] = op; + //cycle through constructors + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + Node x = NodeManager::currentNM()->mkBoundVar( tn ); + Node cond = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), x ).negate(); + + std::vector< Node > sumc; + sumc.push_back( NodeManager::currentNM()->mkConst( Rational(1) ) ); + for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ + TypeNode tnc = TypeNode::fromType( ((SelectorType)dt[i][j].getSelector().getType()).getRangeType() ); + if( tnc.isDatatype() ){ + registerMeasuredType( tnc ); + sumc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tnc], + NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, dt[i][j].getSelector(), x ) ) ); + } + } + Node sum = sumc.size()==1 ? sumc[0] : NodeManager::currentNM()->mkNode( PLUS, sumc ); + Node eq = NodeManager::currentNM()->mkNode( EQUAL, NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tn], x ), sum ); + + Node ax = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), + NodeManager::currentNM()->mkNode( OR, cond, eq ) ); + ax = Rewriter::rewrite( ax ); + Trace("cegqi-lemma") << "Fairness axiom : " << ax << std::endl; + d_quantEngine->getOutputChannel().lemma( ax ); + } + //all are non-negative + Node x = NodeManager::currentNM()->mkBoundVar( tn ); + Node ax = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), + NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), + NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tn], x ) ) ); + ax = Rewriter::rewrite( ax ); + Trace("cegqi-lemma") << "Fairness non-negative axiom : " << ax << std::endl; + d_quantEngine->getOutputChannel().lemma( ax ); + } + } +} + }
\ No newline at end of file |