diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-27 08:34:52 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-27 08:34:52 -0600 |
commit | e179e62b57eb207d41647a6bbd50ef0f8c723e96 (patch) | |
tree | 9a768eeae815f2851f34dc3fbb3fd3661e939c8d /src/theory/quantifiers/inst_match.cpp | |
parent | d0add0eb12cac4e9cbcf09fe60724d280889002d (diff) |
More optimization of QCF and instantiation caching. Fix CDInstMatchTrie.
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 260 |
1 files changed, 146 insertions, 114 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 8428069aa..8d472879e 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -34,18 +34,18 @@ InstMatch::InstMatch( InstMatch* m ) { d_map = m->d_map; } -bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){ +bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & st ){ std::map< Node, Node >::iterator vn = d_map.find( v ); if( !m.isNull() && !m.getType().isSubtypeOf( v.getType() ) ){ - set = false; + st = false; return false; }else if( vn==d_map.end() || vn->second.isNull() ){ - set = true; - this->set(v,m); + st = true; + set(v,m); Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl; return true; }else{ - set = false; + st = false; return q->areEqual( vn->second, m ); } } @@ -88,13 +88,6 @@ void InstMatch::debugPrint( const char* c ){ for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ Debug( c ) << " " << it->first << " -> " << it->second << std::endl; } - //if( !d_splits.empty() ){ - // Debug( c ) << " Conditions: "; - // for( std::map< Node, Node >::iterator it = d_splits.begin(); it !=d_splits.end(); ++it ){ - // Debug( c ) << it->first << " = " << it->second << " "; - // } - // Debug( c ) << std::endl; - //} } void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ @@ -106,13 +99,6 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ } } -//void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){ -// EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery(); -// for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ -// d_map[ it->first ] = eqqe->getInternalRepresentative( it->second ); -// } -//} - void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){ @@ -144,7 +130,6 @@ Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) { void InstMatch::set(TNode var, TNode n){ Assert( !var.isNull() ); if (Trace.isOn("inst-match-warn")) { - // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){ Trace("inst-match-warn") << quantifiers::TermDb::getInstConstAttr(var) << std::endl; Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ; @@ -160,40 +145,35 @@ void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) { - -/* -void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, 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 ) ); - d_data[n].addInstMatch2( qe, f, m, index+1, imtio ); - } -} - -bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){ - if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){ - return true; +bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, + bool modEq, bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ){ + if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){ + return false; }else{ int i_index = imtio ? imtio->d_order[index] : index; Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); std::map< Node, InstMatchTrie >::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; + bool ret = it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 ); + if( !onlyExist || !ret ){ + return ret; } } + /* //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; + std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl ); + if( itm!=d_data.end() ){ + if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){ + return false; } } } } + */ + /* if( modEq ){ //check modulo equality if any other instantiation match exists if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ @@ -204,8 +184,8 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& if( en!=n ){ std::map< Node, InstMatchTrie >::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; + if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){ + return false; } } } @@ -213,105 +193,95 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& } } } - return false; - } -} - -bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){ - return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio ); -} - -bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){ - if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){ - addInstMatch2( qe, f, m, 0, imtio ); +*/ + if( !onlyExist ){ + d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 ); + } return true; - }else{ - return false; } } -*/ - - - -bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ){ +bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq, + bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ) { if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){ return false; }else{ int i_index = imtio ? imtio->d_order[index] : index; - Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); + Node n = m[i_index]; std::map< Node, InstMatchTrie >::iterator it = d_data.find( n ); if( it!=d_data.end() ){ - return it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 ); - }else{ - - /* - //check if m is an instance of another instantiation if modInst is true - if( modInst ){ - if( !n.isNull() ){ - Node nl; - std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl ); - if( itm!=d_data.end() ){ - if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){ - return false; - } + bool ret = it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 ); + if( !onlyExist || !ret ){ + return ret; + } + } + /* + //check if m is an instance of another instantiation if modInst is true + if( modInst ){ + if( !n.isNull() ){ + Node nl; + std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl ); + if( itm!=d_data.end() ){ + if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){ + return false; } } } - */ - /* - 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, InstMatchTrie >::iterator itc = d_data.find( en ); - if( itc!=d_data.end() ){ - if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){ - return false; - } + } + */ + /* + 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, InstMatchTrie >::iterator itc = d_data.find( en ); + if( itc!=d_data.end() ){ + if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){ + return false; } } - ++eqc; } + ++eqc; } } - */ - if( !onlyExist ){ - d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 ); - } - return true; } + */ + if( !onlyExist ){ + d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 ); + } + return true; } } - - /** exists match */ -bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){ +bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, + context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){ + bool reset = false; if( !d_valid.get() ){ if( onlyExist ){ - return false; + return true; }else{ d_valid.set( true ); + reset = true; } } if( index==(int)f[0].getNumChildren() ){ - return true; + return false; }else{ Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, index ) ); - if( onlyExist ){ - std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); - if( it!=d_data.end() ){ - if( !it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){ - return false; - } + std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); + if( it!=d_data.end() ){ + bool ret = it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, onlyExist ); + if( !onlyExist || !ret ){ + return reset || ret; } } //check if m is an instance of another instantiation if modInst is true + /* if( modInst ){ if( !n.isNull() ){ Node nl; @@ -323,6 +293,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, } } } + */ if( modEq ){ //check modulo equality if any other instantiation match exists if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ @@ -342,19 +313,80 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, } } } + if( !onlyExist ){ std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); - CDInstMatchTrie* imt; - if( it!=d_data.end() ){ - imt = it->second; - it->second->d_valid.set( true ); - }else{ - imt = new CDInstMatchTrie( c ); - d_data[n] = imt; - } - return imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false ); + CDInstMatchTrie* imt = new CDInstMatchTrie( c ); + d_data[n] = imt; + imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false ); } + return true; + } +} + +bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, + context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){ + bool reset = false; + if( !d_valid.get() ){ + if( onlyExist ){ + return true; + }else{ + d_valid.set( true ); + reset = true; + } + } + if( index==(int)f[0].getNumChildren() ){ return false; + }else{ + Node n = m[ index ]; + std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); + if( it!=d_data.end() ){ + bool ret = it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, onlyExist ); + if( !onlyExist || !ret ){ + return reset || ret; + } + } + //check if m is an instance of another instantiation if modInst is true + /* + if( modInst ){ + if( !n.isNull() ){ + Node nl; + std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl ); + if( itm!=d_data.end() ){ + if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){ + return false; + } + } + } + } + */ + 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->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){ + return false; + } + } + } + ++eqc; + } + } + } + + if( !onlyExist ){ + std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); + CDInstMatchTrie* imt = new CDInstMatchTrie( c ); + d_data[n] = imt; + imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false ); + } + return true; } } |