diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-29 13:08:31 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-29 13:08:31 +0100 |
commit | 51d642e075466bc6655cae9752350f6760b2bd0f (patch) | |
tree | 9c4e752e2d7ced10854c82555fa148b8e73e6d78 /src/theory/quantifiers/quant_util.cpp | |
parent | 4a8045f5f57c1e71dc4a2cdadc02ca09114c70af (diff) |
Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers module. Refactor QuantifiersEngine registration and check.
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 139 |
1 files changed, 0 insertions, 139 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 088ba093f..f73bc7bb2 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -255,142 +255,3 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& } } } - - -QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_wasInvoked( false ), d_qe( qe ), d_lte_asserts( c ){ - -} - -/** add quantifier */ -bool QuantLtePartialInst::addQuantifier( Node q ) { - if( d_do_inst.find( q )!=d_do_inst.end() ){ - if( d_do_inst[q] ){ - d_lte_asserts.push_back( q ); - return true; - }else{ - return false; - } - }else{ - d_vars[q].clear(); - //check if this quantified formula is eligible for partial instantiation - std::map< Node, bool > vars; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - vars[q[0][i]] = true; - } - getEligibleInstVars( q[1], vars ); - - //TODO : instantiate only if we would force ground instances? - bool doInst = true; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - if( vars[q[0][i]] ){ - d_vars[q].push_back( q[0][i] ); - }else{ - doInst = false; - break; - } - } - Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl; - d_do_inst[q] = doInst; - if( doInst ){ - d_lte_asserts.push_back( q ); - } - return doInst; - } -} - -void QuantLtePartialInst::getEligibleInstVars( Node n, std::map< Node, bool >& vars ) { - if( n.getKind()!=APPLY_UF || n.getType().isBoolean() ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( vars.find( n[i] )!=vars.end() ){ - vars[n[i]] = false; - } - } - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - getEligibleInstVars( n[i], vars ); - } -} - -void QuantLtePartialInst::reset() { - d_reps.clear(); - eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ - TNode r = (*eqcs_i); - TypeNode tn = r.getType(); - d_reps[tn].push_back( r ); - ++eqcs_i; - } -} - -/** get instantiations */ -void QuantLtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { - Trace("lte-partial-inst") << "LTE : get instantiations, # quant = " << d_lte_asserts.size() << std::endl; - reset(); - for( unsigned i=0; i<d_lte_asserts.size(); i++ ){ - Node q = d_lte_asserts[i]; - Assert( d_do_inst.find( q )!=d_do_inst.end() && d_do_inst[q] ); - if( d_inst.find( q )==d_inst.end() ){ - Trace("lte-partial-inst") << "LTE : Get partial instantiations for " << q << "..." << std::endl; - d_inst[q] = true; - Assert( !d_vars[q].empty() ); - //make bound list - Node bvl; - std::vector< Node > bvs; - for( unsigned j=0; j<q[0].getNumChildren(); j++ ){ - if( std::find( d_vars[q].begin(), d_vars[q].end(), q[0][j] )==d_vars[q].end() ){ - bvs.push_back( q[0][j] ); - } - } - if( !bvs.empty() ){ - bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ); - } - std::vector< Node > conj; - std::vector< Node > terms; - std::vector< TypeNode > types; - for( unsigned j=0; j<d_vars[q].size(); j++ ){ - types.push_back( d_vars[q][j].getType() ); - } - getPartialInstantiations( conj, q, bvl, d_vars[q], terms, types, 0 ); - Assert( !conj.empty() ); - lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) ); - d_wasInvoked = true; - } - } -} - -void QuantLtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, - std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, unsigned index ){ - if( index==vars.size() ){ - Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - if( bvl.isNull() ){ - conj.push_back( body ); - Trace("lte-partial-inst") << " - ground conjunct : " << body << std::endl; - }else{ - Node nq; - if( q.getNumChildren()==3 ){ - Node ipl = q[2].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body, ipl ); - }else{ - nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); - } - Trace("lte-partial-inst") << " - quantified conjunct : " << nq << std::endl; - LtePartialInstAttribute ltpia; - nq.setAttribute(ltpia,true); - conj.push_back( nq ); - } - }else{ - std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[index] ); - if( it!=d_reps.end() ){ - terms.push_back( Node::null() ); - Trace("lte-partial-inst-debug") << it->second.size() << " reps of type " << types[index] << std::endl; - for( unsigned i=0; i<it->second.size(); i++ ){ - terms[index] = it->second[i]; - getPartialInstantiations( conj, q, bvl, vars, terms, types, index+1 ); - } - terms.pop_back(); - }else{ - Trace("lte-partial-inst-debug") << "No reps found of type " << types[index] << std::endl; - } - } -} |