diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-24 19:42:21 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-24 19:42:21 +0100 |
commit | 79ad2d6ec3ebd5c45dce4e13e895d0bed0a6f525 (patch) | |
tree | 7524e1376337c2b3d6544eeda832f8f3d574b409 /src/theory/quantifiers/quant_util.cpp | |
parent | 73cecf65a750b9ee59486083af5ee55734da0a6a (diff) |
Variable patterns only look at eligible terms. Minor refactoring of quantifiers check for sat.
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 2a9a764b9..088ba093f 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -257,8 +257,8 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& } -QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_lte_asserts( c ){ - +QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_wasInvoked( false ), d_qe( qe ), d_lte_asserts( c ){ + } /** add quantifier */ @@ -278,7 +278,7 @@ bool QuantLtePartialInst::addQuantifier( Node q ) { 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++ ){ @@ -290,7 +290,7 @@ bool QuantLtePartialInst::addQuantifier( Node q ) { } } Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl; - d_do_inst[q] = doInst; + d_do_inst[q] = doInst; if( doInst ){ d_lte_asserts.push_back( q ); } @@ -354,11 +354,12 @@ void QuantLtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { 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, +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() ); |