diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-28 09:51:33 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-28 09:51:44 -0600 |
commit | d3822db24e15e255766866a47e6ffa0d8d91911b (patch) | |
tree | 221298973f410f4305f74cd6041b6a017aaa3075 /src/theory/quantifiers/inst_match.cpp | |
parent | 587bc5c82e2921a72cec58dc2ec69e3e0ed71866 (diff) |
More optimizations of quantifier instantiation data structures.
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 256 |
1 files changed, 65 insertions, 191 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 8d472879e..e72e19119 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -27,55 +27,33 @@ namespace CVC4 { namespace theory { namespace inst { -InstMatch::InstMatch() { -} - -InstMatch::InstMatch( InstMatch* m ) { - d_map = m->d_map; -} - -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() ) ){ - st = false; - return false; - }else if( vn==d_map.end() || vn->second.isNull() ){ - st = true; - set(v,m); - Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl; - return true; - }else{ - st = false; - return q->areEqual( vn->second, m ); +InstMatch::InstMatch( Node f ) { + for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ + d_vals.push_back( Node::null() ); } } -bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){ - bool set; - return setMatch(q,v,m,set); +InstMatch::InstMatch( InstMatch* m ) { + d_vals.insert( d_vals.end(), m->d_vals.begin(), m->d_vals.end() ); } bool InstMatch::add( InstMatch& m ){ - for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){ - if( !it->second.isNull() ){ - std::map< Node, Node >::iterator itf = d_map.find( it->first ); - if( itf==d_map.end() || itf->second.isNull() ){ - d_map[it->first] = it->second; - } + for( unsigned i=0; i<d_vals.size(); i++ ){ + if( d_vals[i].isNull() ){ + d_vals[i] = m.d_vals[i]; } } return true; } bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){ - for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){ - if( !it->second.isNull() ){ - std::map< Node, Node >::iterator itf = d_map.find( it->first ); - if( itf==d_map.end() || itf->second.isNull() ){ - d_map[ it->first ] = it->second; + for( unsigned i=0; i<m.d_vals.size(); i++ ){ + if( !m.d_vals[i].isNull() ){ + if( d_vals[i].isNull() ){ + d_vals[i] = m.d_vals[i]; }else{ - if( !q->areEqual( it->second, itf->second ) ){ - d_map.clear(); + if( !q->areEqual( d_vals[i], m.d_vals[i]) ){ + clear(); return false; } } @@ -85,118 +63,83 @@ bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){ } 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; + for( unsigned i=0; i<d_vals.size(); i++ ){ + if( !d_vals[i].isNull() ){ + Debug( c ) << " " << i << " -> " << d_vals[i] << std::endl; + } } } -void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i ); - if( d_map.find( ic )==d_map.end() ){ - d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); +bool InstMatch::isComplete() { + for( unsigned i=0; i<d_vals.size(); i++ ){ + if( d_vals[i].isNull() ){ + return false; } } + return true; } -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 ) ){ - d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second ); +bool InstMatch::empty() { + for( unsigned i=0; i<d_vals.size(); i++ ){ + if( !d_vals[i].isNull() ){ + return false; } } + return true; } -void InstMatch::applyRewrite(){ - for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ - it->second = Rewriter::rewrite(it->second); +void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ + for( unsigned i=0; i<d_vals.size(); i++ ){ + if( d_vals[i].isNull() ){ + Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i ); + d_vals[i] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); + } } } -/** get value */ -Node InstMatch::getValue( Node var ) const{ - std::map< Node, Node >::const_iterator it = d_map.find( var ); - if( it!=d_map.end() ){ - return it->second; - }else{ - return Node::null(); +void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ + for( unsigned i=0; i<d_vals.size(); i++ ){ + if( !d_vals[i].isNull() ){ + if( qe->getEqualityQuery()->getEngine()->hasTerm( d_vals[i] ) ){ + d_vals[i] = qe->getEqualityQuery()->getEngine()->getRepresentative( d_vals[i] ); + } + } } } -Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) { - return get( qe->getTermDatabase()->getInstantiationConstant( f, i ) ); -} - -void InstMatch::set(TNode var, TNode n){ - Assert( !var.isNull() ); - if (Trace.isOn("inst-match-warn")) { - 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 ; +void InstMatch::applyRewrite(){ + for( unsigned i=0; i<d_vals.size(); i++ ){ + if( !d_vals[i].isNull() ){ + d_vals[i] = Rewriter::rewrite( d_vals[i] ); } } - Assert( n.isNull() || n.getType().isSubtypeOf( var.getType() ) ); - d_map[var] = n; } -void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) { - set( qe->getTermDatabase()->getInstantiationConstant( f, i ), n ); +void InstMatch::clear() { + for( unsigned i=0; i<d_vals.size(); i++ ){ + d_vals[i] = Node::null(); + } } +/** get value */ +Node InstMatch::get( int i ) { + return d_vals[i]; +} -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() ){ - 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; - } - } - } - ++eqc; - } - } - } -*/ - if( !onlyExist ){ - d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 ); +void InstMatch::setValue( int i, TNode n ) { + d_vals[i] = n; +} + +bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) { + if( !d_vals[i].isNull() ){ + if( qe->getEqualityQuery()->areEqual( d_vals[i], n ) ){ + return true; + }else{ + return false; } + }else{ + d_vals[i] = n; return true; } } @@ -229,7 +172,6 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No } } */ - /* if( modEq ){ //check modulo equality if any other instantiation match exists if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ @@ -249,7 +191,6 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No } } } - */ if( !onlyExist ){ d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 ); } @@ -257,73 +198,6 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No } } -/** exists match */ -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 true; - }else{ - d_valid.set( true ); - reset = true; - } - } - if( index==(int)f[0].getNumChildren() ){ - return false; - }else{ - Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, 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; - } -} - 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; |