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 | |
parent | d0add0eb12cac4e9cbcf09fe60724d280889002d (diff) |
More optimization of QCF and instantiation caching. Fix CDInstMatchTrie.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 260 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 58 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/qinterval_builder.cpp | 4 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 115 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 6 |
8 files changed, 231 insertions, 232 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index c7d7b7415..d542e878c 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -672,12 +672,8 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, } }else{ //just add the instance - InstMatch m; - for( unsigned j=0; j<inst.size(); j++) { - m.set( d_qe, f, j, inst[j] ); - } d_triedLemmas++; - if( d_qe->addInstantiation( f, m ) ){ + if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; }else{ @@ -792,13 +788,9 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size(); Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index]; if (ev!=d_true) { - InstMatch m; - for( unsigned i=0; i<inst.size(); i++ ){ - m.set( d_qe, f, i, inst[i] ); - } Trace("fmc-exh-debug") << ", add!"; //add as instantiation - if( d_qe->addInstantiation( f, m ) ){ + if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-exh-debug") << " ...success."; addedLemmas++; }else{ 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; } } diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 2cf33bc8e..eb7f50095 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -45,7 +45,7 @@ public: /** set the match of v to m */ bool setMatch( EqualityQuery* q, TNode v, TNode m ); /* This version tell if the variable has been set */ - bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & set); + bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & st); /** fill all unfilled values with m */ bool add( InstMatch& m ); /** if compatible, fill all unfilled values with m and return true @@ -134,55 +134,20 @@ public: bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) { return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index ); } + bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, + bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) { + return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index ); + } /** add match m for quantifier f, take into account equalities if modEq = true, if imtio is non-null, this is the order to add to trie return true if successful */ bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); + bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, + bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); };/* class InstMatchTrie */ - -#if 0 - -/** trie for InstMatch objects */ -class CDInstMatchTrie { -public: - class ImtIndexOrder { - public: - std::vector< int > d_order; - };/* class InstMatchTrie ImtIndexOrder */ -private: - /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ - void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio ); - /** exists match */ - bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ); -public: - /** the data */ - std::map< Node, CDInstMatchTrie* > d_data; - /** is valid */ - context::CDO< bool > d_valid; -public: - CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} - ~CDInstMatchTrie(){} -public: - /** return true if m exists in this trie - modEq is if we check modulo equality - modInst is if we return true if m is an instance of a match that exists - */ - bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - bool modInst = false, ImtIndexOrder* imtio = NULL ); - /** add match m for quantifier f, take into account equalities if modEq = true, - if imtio is non-null, this is the order to add to trie - return true if successful - */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false, - bool modInst = false, ImtIndexOrder* imtio = NULL ); -};/* class CDInstMatchTrie */ - -#else - - /** trie for InstMatch objects */ class CDInstMatchTrie { public: @@ -202,12 +167,18 @@ public: bool modInst = false, int index = 0 ) { return !addInstMatch( qe, f, m, c, modEq, modInst, index, true ); } + bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, + bool modInst = false, int index = 0 ) { + return !addInstMatch( qe, f, m, c, modEq, modInst, index, true ); + } /** add match m for quantifier f, take into account equalities if modEq = true, if imtio is non-null, this is the order to add to trie return true if successful */ bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ); + bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, + bool modInst = false, int index = 0, bool onlyExist = false ); };/* class CDInstMatchTrie */ @@ -232,9 +203,6 @@ public: } };/* class InstMatchTrieOrdered */ -#endif - - }/* CVC4::theory::inst namespace */ typedef CVC4::theory::inst::InstMatch InstMatch; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 6a9327967..fa5a8d844 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -386,11 +386,11 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ if( success ){ index--; //try instantiation - InstMatch m; + std::vector< Node > terms; for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ - m.set( d_quantEngine, f, i, rd->getRDomain( f, i )->d_terms[childIndex[i]] ); + terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] ); } - if( d_quantEngine->addInstantiation( f, m, true, false, false ) ){ + if( d_quantEngine->addInstantiation( f, terms, false ) ){ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); return STATUS_UNKNOWN; } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 493d54b53..707047b93 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -275,7 +275,7 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ //try to add it Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl; //add model basis instantiation - if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){ + if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false ) ){ d_quant_basis_match_added[f] = true; return 1; }else{ diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp index ce85cecc0..ece519d1c 100755 --- a/src/theory/quantifiers/qinterval_builder.cpp +++ b/src/theory/quantifiers/qinterval_builder.cpp @@ -1036,14 +1036,12 @@ bool QIntervalBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, if( fmqint->d_var_order[q]->getInstantiation( fmqint, l, u, inst ) ){
Trace("qint-inst") << "** Instantiate with ";
//just add the instance
- InstMatch m;
for( unsigned j=0; j<inst.size(); j++) {
- m.set( d_qe, q, j, inst[j] );
Trace("qint-inst") << inst[j] << " ";
}
Trace("qint-inst") << std::endl;
d_triedLemmas++;
- if( d_qe->addInstantiation( q, m ) ){
+ if( d_qe->addInstantiation( q, inst ) ){
Trace("qint-inst") << " ...added instantiation." << std::endl;
d_addedLemmas++;
}else{
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 665ae5329..aead93d07 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -69,9 +69,19 @@ void QcfNodeIndex::debugPrint( const char * c, int t ) { }
+void QuantInfo::initialize( Node q ) {
+ d_q = q;
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+ d_match.push_back( TNode::null() );
+ d_match_term.push_back( TNode::null() );
+ }
+}
+
void QuantInfo::reset_round( QuantConflictFind * p ) {
- d_match.clear();
- d_match_term.clear();
+ for( unsigned i=0; i<d_match.size(); i++ ){
+ d_match[i] = TNode::null();
+ d_match_term[i] = TNode::null();
+ }
d_curr_var_deq.clear();
//add built-in variable constraints
for( unsigned r=0; r<2; r++ ){
@@ -102,9 +112,8 @@ void QuantInfo::reset_round( QuantConflictFind * p ) { }
int QuantInfo::getCurrentRepVar( int v ) {
- std::map< int, TNode >::iterator it = d_match.find( v );
- if( it!=d_match.end() ){
- int vn = getVarNum( it->second );
+ if( v!=-1 && !d_match[v].isNull() ){
+ int vn = getVarNum( d_match[v] );
if( vn!=-1 ){
//int vr = getCurrentRepVar( vn );
//d_match[v] = d_vars[vr];
@@ -120,12 +129,11 @@ TNode QuantInfo::getCurrentValue( TNode n ) { if( v==-1 ){
return n;
}else{
- std::map< int, TNode >::iterator it = d_match.find( v );
- if( it==d_match.end() ){
+ if( d_match[v].isNull() ){
return n;
}else{
- Assert( getVarNum( it->second )!=v );
- return getCurrentValue( it->second );
+ Assert( getVarNum( d_match[v] )!=v );
+ return getCurrentValue( d_match[v] );
}
}
}
@@ -170,8 +178,8 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo if( doRemove ){
if( vn!=-1 ){
//if set to this in the opposite direction, clean up opposite instead
- std::map< int, TNode >::iterator itmn = d_match.find( vn );
- if( itmn!=d_match.end() && itmn->second==d_vars[v] ){
+ // std::map< int, TNode >::iterator itmn = d_match.find( vn );
+ if( d_match[vn]==d_vars[v] ){
return addConstraint( p, vn, d_vars[v], v, true, true );
}else{
//unsetting variables equal
@@ -190,20 +198,20 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo }
}
}
- d_match.erase( v );
+ d_match[v] = TNode::null();
return 1;
}else{
- std::map< int, TNode >::iterator itm = d_match.find( v );
+ //std::map< int, TNode >::iterator itm = d_match.find( v );
if( vn!=-1 ){
Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl;
- std::map< int, TNode >::iterator itmn = d_match.find( vn );
- if( itm==d_match.end() ){
+ //std::map< int, TNode >::iterator itmn = d_match.find( vn );
+ if( d_match[v].isNull() ){
//setting variables equal
bool alreadySet = false;
- if( itmn!=d_match.end() ){
+ if( !d_match[vn].isNull() ){
alreadySet = true;
- Assert( !itmn->second.isNull() && !isVar( itmn->second ) );
+ Assert( !isVar( d_match[vn] ) );
}
//copy or check disequalities
@@ -216,7 +224,7 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo d_curr_var_deq[vn][dv] = v;
}
}else{
- if( !p->areMatchDisequal( itmn->second, dv ) ){
+ if( !p->areMatchDisequal( d_match[vn], dv ) ){
Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;
return -1;
}
@@ -227,24 +235,23 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo n = getCurrentValue( n );
}
}else{
- if( itmn==d_match.end() ){
+ if( d_match[vn].isNull() ){
Debug("qcf-match-debug") << " ...Reverse direction" << std::endl;
//set the opposite direction
return addConstraint( p, vn, d_vars[v], v, true, false );
}else{
Debug("qcf-match-debug") << " -> Both variables bound, compare" << std::endl;
//are they currently equal
- return p->areMatchEqual( itm->second, itmn->second ) ? 0 : -1;
+ return p->areMatchEqual( d_match[v], d_match[vn] ) ? 0 : -1;
}
}
}else{
Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl;
- if( itm==d_match.end() ){
-
+ if( d_match[v].isNull() ){
}else{
//compare ground values
- Debug("qcf-match-debug") << " -> Ground value, compare " << itm->second << " "<< n << std::endl;
- return p->areMatchEqual( itm->second, n ) ? 0 : -1;
+ Debug("qcf-match-debug") << " -> Ground value, compare " << d_match[v] << " "<< n << std::endl;
+ return p->areMatchEqual( d_match[v], n ) ? 0 : -1;
}
}
if( setMatch( p, v, n ) ){
@@ -271,10 +278,10 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo }else{
if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){
//check if it respects equality
- std::map< int, TNode >::iterator itm = d_match.find( v );
- if( itm!=d_match.end() ){
+ //std::map< int, TNode >::iterator itm = d_match.find( v );
+ if( !d_match[v].isNull() ){
TNode nv = getCurrentValue( n );
- if( !p->areMatchDisequal( nv, itm->second ) ){
+ if( !p->areMatchDisequal( nv, d_match[v] ) ){
Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;
return -1;
}
@@ -296,8 +303,9 @@ bool QuantInfo::isConstrainedVar( int v ) { return true;
}else{
Node vv = getVar( v );
- for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){
- if( it->second==vv ){
+ //for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){
+ for( unsigned i=0; i<d_match.size(); i++ ){
+ if( d_match[i]==vv ){
return true;
}
}
@@ -324,9 +332,9 @@ bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n ) { bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
for( int i=0; i<getNumVars(); i++ ){
- std::map< int, TNode >::iterator it = d_match.find( i );
- if( it!=d_match.end() ){
- if( !getCurrentCanBeEqual( p, i, it->second, p->d_effort==QuantConflictFind::effort_conflict ) ){
+ //std::map< int, TNode >::iterator it = d_match.find( i );
+ if( !d_match[i].isNull() ){
+ if( !getCurrentCanBeEqual( p, i, d_match[i], p->d_effort==QuantConflictFind::effort_conflict ) ){
return true;
}
}
@@ -340,7 +348,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign std::vector< int > unassigned[2];
std::vector< TypeNode > unassigned_tn[2];
for( int i=0; i<getNumVars(); i++ ){
- if( d_match.find( i )==d_match.end() ){
+ if( d_match[i].isNull() ){
//Assert( i<(int)q[0].getNumChildren() );
int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
unassigned[rindex].push_back( i );
@@ -421,7 +429,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign Trace("qcf-check-unassign") << " Try: " << std::endl;
for( unsigned i=0; i<unassigned[r].size(); i++ ){
int ui = unassigned[r][i];
- if( d_match.find( ui )!=d_match.end() ){
+ if( !d_match[ui].isNull() ){
Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
}
}
@@ -433,7 +441,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign return true;
}else{
for( unsigned i=0; i<assigned.size(); i++ ){
- d_match.erase( assigned[i] );
+ d_match[ assigned[i] ] = TNode::null();
}
assigned.clear();
return false;
@@ -443,7 +451,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign void QuantInfo::debugPrintMatch( const char * c ) {
for( int i=0; i<getNumVars(); i++ ){
Trace(c) << " " << d_vars[i] << " -> ";
- if( d_match.find( i )!=d_match.end() ){
+ if( !d_match[i].isNull() ){
Trace(c) << d_match[i];
}else{
Trace(c) << "(unassigned) ";
@@ -794,8 +802,8 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
Debug("qcf-match") << " Clean up bound var " << it->second << std::endl;
Assert( it->second<qi->getNumVars() );
- qi->d_match.erase( it->second );
- qi->d_match_term.erase( it->second );
+ qi->d_match[ it->second ] = TNode::null();
+ qi->d_match_term[ it->second ] = TNode::null();
}
d_qni_bound.clear();
}
@@ -912,10 +920,9 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { int repVar = qi->getCurrentRepVar( itv->second );
Debug("qcf-match-debug") << " Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;
//get the value the rep variable
- std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );
- if( itm!=qi->d_match.end() ){
- val = itm->second;
- Assert( !val.isNull() );
+ //std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );
+ if( !qi->d_match[repVar].isNull() ){
+ val = qi->d_match[repVar];
Debug("qcf-match-debug") << " Variable is already bound to " << val << std::endl;
}else{
//binding a variable
@@ -1001,7 +1008,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
Debug("qcf-match-debug") << " position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;
if( it->second<(int)qi->d_q[0].getNumChildren() && it->first>0 ){ //if it is an actual variable, we are interested in knowing the actual term
- Assert( qi->d_match.find( it->second )!=qi->d_match.end() );
+ Assert( !qi->d_match[ it->second ].isNull() );
Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );
qi->d_match_term[it->second] = t[it->first-1];
}
@@ -1147,6 +1154,8 @@ void QuantConflictFind::flatten( Node q, Node n ) { //Trace("qcf-qregister") << " Flatten term " << n[i] << std::endl;
d_qinfo[q].d_var_num[n] = d_qinfo[q].d_vars.size();
d_qinfo[q].d_vars.push_back( n );
+ d_qinfo[q].d_match.push_back( TNode::null() );
+ d_qinfo[q].d_match_term.push_back( TNode::null() );
}
for( unsigned i=0; i<n.getNumChildren(); i++ ){
flatten( q, n[i] );
@@ -1157,7 +1166,7 @@ void QuantConflictFind::flatten( Node q, Node n ) { void QuantConflictFind::registerQuantifier( Node q ) {
d_quants.push_back( q );
d_quant_id[q] = d_quants.size();
- d_qinfo[q].d_q = q;
+ d_qinfo[q].initialize( q );
Trace("qcf-qregister") << "Register ";
debugPrintQuant( "qcf-qregister", q );
Trace("qcf-qregister") << " : " << q << std::endl;
@@ -1524,31 +1533,29 @@ void QuantConflictFind::check( Theory::Effort level ) { if( !qi->isMatchSpurious( this ) ){
std::vector< int > assigned;
if( qi->completeMatch( this, assigned ) ){
- InstMatch m;
+ std::vector< Node > terms;
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
//Node cv = qi->getCurrentValue( qi->d_match[i] );
int repVar = qi->getCurrentRepVar( i );
Node cv;
- std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );
- if( itmt!=qi->d_match_term.end() ){
- cv = itmt->second;
+ //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );
+ if( !qi->d_match_term[repVar].isNull() ){
+ cv = qi->d_match_term[repVar];
}else{
cv = qi->d_match[repVar];
}
-
-
Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;
- m.set( d_quantEngine, q, i, cv );
+ terms.push_back( cv );
}
if( Debug.isOn("qcf-check-inst") ){
//if( e==effort_conflict ){
- Node inst = d_quantEngine->getInstantiation( q, m );
+ Node inst = d_quantEngine->getInstantiation( q, terms );
Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
Assert( evaluate( inst )!=1 );
Assert( evaluate( inst )==-1 || e>effort_conflict );
//}
}
- if( d_quantEngine->addInstantiation( q, m ) ){
+ if( d_quantEngine->addInstantiation( q, terms ) ){
Trace("qcf-check") << " ... Added instantiation" << std::endl;
++addedLemmas;
if( e==effort_conflict ){
@@ -1564,7 +1571,7 @@ void QuantConflictFind::check( Theory::Effort level ) { }
//clean up assigned
for( unsigned i=0; i<assigned.size(); i++ ){
- qi->d_match.erase( assigned[i] );
+ qi->d_match[ assigned[i] ] = TNode::null();
}
}else{
Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 5ba7684ef..29ddceb40 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -110,9 +110,11 @@ public: std::map< int, MatchGen * > d_var_mg;
void reset_round( QuantConflictFind * p );
public:
+ //initialize
+ void initialize( Node q );
//current constraints
- std::map< int, TNode > d_match;
- std::map< int, TNode > d_match_term;
+ std::vector< TNode > d_match;
+ std::vector< TNode > d_match_term;
std::map< int, std::map< TNode, int > > d_curr_var_deq;
int getCurrentRepVar( int v );
TNode getCurrentValue( TNode n );
|