diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-28 01:57:20 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-28 01:57:20 -0600 |
commit | c5d1a5d8f898bf22c6bbc98f1d484b07706c035b (patch) | |
tree | 49b5cc92ea74d720178d60bab2837bf897559813 /src/theory/quantifiers/inst_match.cpp | |
parent | bcbf52ffbe0416ecf70bdb644017c338c0540793 (diff) |
made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 82 |
1 files changed, 82 insertions, 0 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 1a48ec161..dcd7a1b79 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -217,6 +217,88 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, b } + +/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ +void CDInstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio ){ + if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){ + int i_index = imtio ? imtio->d_order[index] : index; + Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); + std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); + if( it!=d_data.end() ){ + it->second->addInstMatch2( qe, f, m, c, index+1, imtio ); + }else{ + CDInstMatchTrie* imt = new CDInstMatchTrie( c ); + d_data[n] = imt; + imt->d_valid = true; + imt->addInstMatch2( qe, f, m, c, index+1, imtio ); + } + } +} + +/** exists match */ +bool CDInstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){ + if( !d_valid ){ + return false; + }else if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){ + return true; + }else{ + int i_index = imtio ? imtio->d_order[index] : index; + Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); + std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); + if( it!=d_data.end() ){ + if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ + return true; + } + } + //check if m is an instance of another instantiation if modInst is true + if( modInst ){ + if( !n.isNull() ){ + Node nl; + it = d_data.find( nl ); + if( it!=d_data.end() ){ + if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ + return true; + } + } + } + } + if( modEq ){ + //check modulo equality if any other instantiation match exists + if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ + eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ), + qe->getEqualityQuery()->getEngine() ); + while( !eqc.isFinished() ){ + Node en = (*eqc); + if( en!=n ){ + std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en ); + if( itc!=d_data.end() ){ + if( itc->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ + return true; + } + } + } + ++eqc; + } + } + } + return false; + } +} + +bool CDInstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){ + return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio ); +} + +bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, Context* c, bool modEq, bool modInst, ImtIndexOrder* imtio ){ + if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){ + addInstMatch2( qe, f, m, c, 0, imtio ); + return true; + }else{ + return false; + } +} + + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |