From e179e62b57eb207d41647a6bbd50ef0f8c723e96 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 27 Jan 2014 08:34:52 -0600 Subject: [PATCH] More optimization of QCF and instantiation caching. Fix CDInstMatchTrie. --- src/theory/quantifiers/full_model_check.cpp | 12 +- src/theory/quantifiers/inst_match.cpp | 260 ++++++++++-------- src/theory/quantifiers/inst_match.h | 58 +--- .../quantifiers/inst_strategy_e_matching.cpp | 6 +- src/theory/quantifiers/model_builder.cpp | 2 +- src/theory/quantifiers/qinterval_builder.cpp | 4 +- .../quantifiers/quant_conflict_find.cpp | 115 ++++---- src/theory/quantifiers/quant_conflict_find.h | 6 +- src/theory/quantifiers_engine.cpp | 51 ++-- src/theory/quantifiers_engine.h | 4 +- 10 files changed, 261 insertions(+), 257 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; jaddInstantiation( 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; iaddInstantiation( 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)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; igetRDomain( 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; jaddInstantiation( 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::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::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& assign Trace("qcf-check-unassign") << " Try: " << std::endl; for( unsigned i=0; i " << 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& assign void QuantInfo::debugPrintMatch( const char * c ) { for( int i=0; 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->secondgetNumVars() ); - 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; iisMatchSpurious( this ) ){ std::vector< int > assigned; if( qi->completeMatch( this, assigned ) ){ - InstMatch m; + std::vector< Node > terms; for( unsigned i=0; igetCurrentValue( 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; id_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 ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 111aa9ac5..6f3879d39 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -467,8 +467,8 @@ bool QuantifiersEngine::addLemma( Node lem ){ } } -bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){ - Trace("inst-add-debug") << "Add instantiation: " << m << std::endl; +bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){ + std::vector< Node > terms; //make sure there are values for each variable we are instantiating for( size_t i=0; igetInstantiationConstant( f, i ); @@ -476,21 +476,32 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool if( val.isNull() ){ val = d_term_db->getFreeVariableForInstConstant( ic ); Trace("inst-add-debug") << "mkComplete " << val << std::endl; - m.set( ic, val ); } + terms.push_back( val ); + } + return addInstantiation( f, terms, mkRep, modEq, modInst ); +} + +bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) { + Assert( terms.size()==f[0].getNumChildren() ); + Trace("inst-add-debug") << "Add instantiation: "; + for( unsigned i=0; i0 ) Trace("inst-add-debug") << ", "; + Trace("inst-add-debug") << f[0][i] << " -> " << terms[i]; //make it representative, this is helpful for recognizing duplication if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term - Node r = d_eq_query->getInternalRepresentative( val, f, i ); - Trace("inst-add-debug") << "mkRep " << r << " " << val << std::endl; - m.set( ic, r ); + terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i ); + //Trace("inst-add-debug") << " (" << terms[i] << ")"; } } - //check for duplication modulo equality + Trace("inst-add-debug") << std::endl; + + //check for duplication bool alreadyExists = false; ///* - Trace("inst-add-debug") << "Adding into inst trie" << std::endl; if( options::incrementalSolving() ){ + Trace("inst-add-debug") << "Adding into context-dependent inst trie" << std::endl; inst::CDInstMatchTrie* imt; std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( f ); if( it!=d_c_inst_match_trie.end() ){ @@ -499,30 +510,21 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool imt = new CDInstMatchTrie( getUserContext() ); d_c_inst_match_trie[f] = imt; } - alreadyExists = !imt->addInstMatch( this, f, m, getUserContext(), modEq, modInst ); + alreadyExists = !imt->addInstMatch( this, f, terms, getUserContext(), modEq, modInst ); }else{ - alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ); + Trace("inst-add-debug") << "Adding into inst trie" << std::endl; + alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, terms, modEq, modInst ); } - //*/ if( alreadyExists ){ - Trace("inst-add-debug") << " -> Already exists." << std::endl; - ++(d_statistics.d_inst_duplicate_eq); - return false; - } - Trace("inst-add-debug") << "compute terms" << std::endl; - //compute the vector of terms for the instantiation - std::vector< Node > terms; - for( size_t i=0; id_inst_constants[f].size(); i++ ){ - Node n = m.getValue( d_term_db->d_inst_constants[f][i] ); - Assert( !n.isNull() ); - terms.push_back( n ); + Trace("inst-add-debug") << " -> Already exists." << std::endl; + ++(d_statistics.d_inst_duplicate_eq); + return false; } + //add the instantiation bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms ); //report the result if( addedInst ){ - Trace("inst-add") << "Added instantiation for " << f << ": " << std::endl; - Trace("inst-add") << " " << m << std::endl; Trace("inst-add-debug") << " -> Success." << std::endl; return true; }else{ @@ -531,6 +533,7 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool } } + bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){ n = Rewriter::rewrite( n ); Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() ); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 9d341194f..fd51e4fb1 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -212,7 +212,9 @@ public: /** add lemma lem */ bool addLemma( Node lem ); /** do instantiation specified by m */ - bool addInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false, bool mkRep = true ); + bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false ); + /** add instantiation */ + bool addInstantiation( Node f, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false ); /** split on node n */ bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); /** add split equality */ -- 2.30.2