diff options
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 141 |
1 files changed, 140 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 62a87bb99..2a9a764b9 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4; @@ -253,4 +254,142 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol = false; } } -}
\ No newline at end of file +} + + +QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : 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 ) ) ); + } + } +} + +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; + } + } +} |