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 | |
parent | 587bc5c82e2921a72cec58dc2ec69e3e0ed71866 (diff) |
More optimizations of quantifier instantiation data structures.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_gen.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_gen.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 256 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 68 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 108 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.h | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 22 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 31 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.h | 2 |
17 files changed, 241 insertions, 310 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 60fa672b3..1e89bb1ea 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -87,9 +87,9 @@ void CandidateGeneratorQE::reset( Node eqc ){ } } bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) { - if( n.hasOperator() && n.getOperator()==d_op ){ + if( n.hasOperator() ){ if( isLegalCandidate( n ) ){ - return true; + return d_qe->getTermDatabase()->getOperator( n )==d_op; } } return false; diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index 157861670..27b87e6a4 100644 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -38,6 +38,9 @@ InstGenProcess::InstGenProcess( Node n ) : d_node( n ){ d_children_map[ i ] = count; count++; } + if( n[i].getKind()==INST_CONSTANT ){ + d_var_num[i] = n[i].getAttribute(InstVarNumAttribute()); + } } } @@ -96,15 +99,15 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto bool hadSuccess CVC4_UNUSED = false; for( int t=(isSelected ? 0 : 1); t<2; t++ ){ if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ - considerTermsMatch[t][n] = InstMatch(); + considerTermsMatch[t][n] = InstMatch( f ); considerTermsSuccess[t][n] = true; for( size_t j=0; j<d_node.getNumChildren(); j++ ){ if( d_children_map.find( j )==d_children_map.end() ){ if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){ if( d_node[j].getKind()==INST_CONSTANT ){ - if( !considerTermsMatch[t][n].setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){ + if( !considerTermsMatch[t][n].set( qe, d_var_num[j], n[j] ) ){ Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to "; - Trace("inst-gen-cm") << considerTermsMatch[t][n].getValue( d_node[j] ) << std::endl; + Trace("inst-gen-cm") << considerTermsMatch[t][n].get( d_var_num[j] ) << std::endl; considerTermsSuccess[t][n] = false; break; } @@ -209,7 +212,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto //if this is an interpreted function if( doProduct ){ //combining children matches - InstMatch curr; + InstMatch curr( f ); std::vector< Node > terms; calculateMatchesInterpreted( qe, f, curr, terms, 0 ); }else{ @@ -217,7 +220,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto Assert( considerVal.size()==1 ); for( int i=0; i<(int)d_children.size(); i++ ){ for( int j=0; j<(int)d_children[ i ].getNumMatches(); j++ ){ - InstMatch m; + InstMatch m( f ); if( d_children[ i ].getMatch( qe->getEqualityQuery(), j, m ) ){ addMatchValue( qe, f, considerVal[0], m ); } diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h index 55afed889..115dd085b 100644 --- a/src/theory/quantifiers/inst_gen.h +++ b/src/theory/quantifiers/inst_gen.h @@ -29,6 +29,7 @@ class InstGenProcess private: //the node we are processing Node d_node; + std::map< int, int > d_var_num; //the sub children for this node std::vector< InstGenProcess > d_children; std::vector< int > d_children_index; 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; diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index eb7f50095..c366c4a09 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -36,16 +36,14 @@ namespace inst { /** basic class defining an instantiation */ class InstMatch { +public: /* map from variable to ground terms */ - std::map< Node, Node > d_map; + std::vector< Node > d_vals; public: - InstMatch(); + InstMatch(){} + InstMatch( Node f ); InstMatch( InstMatch* m ); - /** 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 & st); /** fill all unfilled values with m */ bool add( InstMatch& m ); /** if compatible, fill all unfilled values with m and return true @@ -54,56 +52,36 @@ public: /** debug print method */ void debugPrint( const char* c ); /** is complete? */ - bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); } + bool isComplete(); /** make complete */ void makeComplete( Node f, QuantifiersEngine* qe ); - /** make internal representative */ - //void makeInternalRepresentative( QuantifiersEngine* qe ); /** make representative */ void makeRepresentative( QuantifiersEngine* qe ); - /** get value */ - Node getValue( Node var ) const; + /** empty */ + bool empty(); /** clear */ - void clear(){ d_map.clear(); } - /** is_empty */ - bool empty(){ return d_map.empty(); } + void clear(); /** to stream */ inline void toStream(std::ostream& out) const { out << "INST_MATCH( "; - for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){ - if( it != d_map.begin() ){ out << ", "; } - out << it->first << " -> " << it->second; + bool printed = false; + for( unsigned i=0; i<d_vals.size(); i++ ){ + if( !d_vals[i].isNull() ){ + if( printed ){ out << ", "; } + out << i << " -> " << d_vals[i]; + printed = true; + } } out << " )"; } - - - //for rewrite rules - /** apply rewrite */ void applyRewrite(); - /** erase */ - template<class Iterator> - void erase(Iterator begin, Iterator end){ - for(Iterator i = begin; i != end; ++i){ - d_map.erase(*i); - }; - } - void erase(Node node){ d_map.erase(node); } /** get */ - Node get( TNode var ) { return d_map[var]; } - Node get( QuantifiersEngine* qe, Node f, int i ); + Node get( int i ); /** set */ - void set(TNode var, TNode n); - void set( QuantifiersEngine* qe, Node f, int i, TNode n ); - /** size */ - size_t size(){ return d_map.size(); } - /* iterator */ - std::map< Node, Node >::iterator begin(){ return d_map.begin(); }; - std::map< Node, Node >::iterator end(){ return d_map.end(); }; - std::map< Node, Node >::iterator find(Node var){ return d_map.find(var); }; - /* Node used for matching the trigger only for mono-trigger (just for - efficiency because I need only that) */ + void setValue( int i, TNode n ); + bool set( QuantifiersEngine* qe, int i, TNode n ); + /* Node used for matching the trigger */ Node d_matched; };/* class InstMatch */ @@ -143,7 +121,9 @@ public: 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 modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){ + return addInstMatch( qe, f, m.d_vals, modEq, modInst, imtio, onlyExist, index ); + } 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 */ @@ -176,7 +156,9 @@ public: 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 modInst = false, int index = 0, bool onlyExist = false ) { + return addInstMatch( qe, f, m.d_vals, c, modEq, modInst, index, onlyExist ); + } 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 */ diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index bf4bb15a6..e1d301c09 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -84,6 +84,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat } } Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; + d_match_pattern_op = qe->getTermDatabase()->getOperator( d_match_pattern ); //now, collect children of d_match_pattern int childMatchPolicy = MATCH_GEN_DEFAULT; @@ -127,15 +128,24 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat } Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); //we are matching only in a particular equivalence class - d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); + d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op ); }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){ //we will be scanning lists trying to find d_match_pattern.getOperator() - d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); + d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op ); }else{ d_cg = new CandidateGeneratorQueue; Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; } + for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ + if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ + Node vv = d_match_pattern[i]; + if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ + vv = d_match_pattern[i][0]; + } + d_var_num[i] = vv.getAttribute(InstVarNumAttribute()); + } + } } } @@ -152,7 +162,8 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi EqualityQuery* q = qe->getEqualityQuery(); bool success = true; //save previous match - InstMatch prev( &m ); + //InstMatch prev( &m ); + std::vector< int > prev; //if t is null Assert( !t.isNull() ); Assert( !quantifiers::TermDb::hasInstConstAttr(t) ); @@ -162,21 +173,18 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){ if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ - Node vv = d_match_pattern[i]; Node tt = t[i]; if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ - vv = d_match_pattern[i][0]; tt = NodeManager::currentNM()->mkConst(q->areEqual( tt, d_match_pattern[i][1] )); } - if( !m.setMatch( q, vv, tt ) ){ + bool addToPrev = m.get( d_var_num[i] ).isNull(); + if( !m.set( qe, d_var_num[i], tt ) ){ //match is in conflict - Trace("matching-debug") << "Match in conflict " << tt << " and " - << vv << " because " - << m.get(vv) - << std::endl; - Trace("matching-fail") << "Match fail: " << m.get(vv) << " and " << tt << std::endl; + Trace("matching-fail") << "Match fail: " << m.get(d_var_num[i]) << " and " << tt << std::endl; success = false; break; + }else if( addToPrev ){ + prev.push_back( d_var_num[i] ); } } }else{ @@ -190,6 +198,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } //for relational matching if( !d_eq_class.isNull() && d_eq_class.getKind()==INST_CONSTANT ){ + int v = d_eq_class.getAttribute(InstVarNumAttribute()); //also must fit match to equivalence class bool pol = d_pattern.getKind()!=NOT; Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern; @@ -214,17 +223,20 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi t_match = t; } } - if( !t_match.isNull() && !m.setMatch( q, d_eq_class, t_match ) ){ - success = false; + if( !t_match.isNull() ){ + bool addToPrev = m.get( v ).isNull(); + if( !m.set( qe, v, t_match ) ){ + success = false; + }else if( addToPrev ){ + prev.push_back( v ); + } } } if( success ){ //now, fit children into match //we will be requesting candidates for matching terms for each child - std::vector< Node > reps; for( int i=0; i<(int)d_children.size(); i++ ){ Node rep = q->getRepresentative( t[ d_children_index[i] ] ); - reps.push_back( rep ); d_children[i]->reset( rep, qe ); } if( d_next!=NULL ){ @@ -238,7 +250,10 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } } if( !success ){ - m = InstMatch( &prev ); + //m = InstMatch( &prev ); + for( unsigned i=0; i<prev.size(); i++ ){ + m.d_vals[prev[i]] = Node::null(); + } } return success; } @@ -302,10 +317,9 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ //try to add instantiation for each match produced int addedLemmas = 0; - InstMatch m; + InstMatch m( f ); while( getNextMatch( f, m, qe ) ){ if( !d_active_add ){ - //m.makeInternal( d_quantEngine->getEqualityQuery() ); m.add( baseMatch ); if( qe->addInstantiation( f, m ) ){ addedLemmas++; @@ -325,7 +339,7 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ Assert( options::eagerInstQuant() ); if( !d_match_pattern.isNull() ){ - InstMatch m; + InstMatch m( f ); if( getMatch( f, t, m, qe ) ){ if( qe->addInstantiation( f, m ) ){ return 1; @@ -457,7 +471,7 @@ int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, Qu for( int i=0; i<(int)d_children.size(); i++ ){ Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl; std::vector< InstMatch > newMatches; - InstMatch m; + InstMatch m( f ); while( d_children[i]->getNextMatch( f, m, qe ) ){ //m.makeRepresentative( qe ); newMatches.push_back( InstMatch( &m ) ); @@ -473,7 +487,7 @@ int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, Qu void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){ //see if these produce new matches - d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true ); + d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m ); //possibly only do the following if we know that new matches will be produced? //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that // we can safely skip the following lines, even when we have already produced this match. @@ -493,8 +507,9 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 ); }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){ int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex]; - Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index ); - if( m.find( curr_ic )==m.end() ){ + //Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index ); + Node n = m.get( curr_index ); + if( n.isNull() ){ //if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME // //unique variable(s), defer calculation // unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) ); @@ -505,14 +520,13 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I //shared and non-set variable, add to InstMatch for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){ InstMatch mn( &m ); - mn.set( curr_ic, it->first); + mn.setValue( curr_index, it->first); processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries, trieIndex+1, childIndex, endChildIndex, modEq ); } //} }else{ //shared and set variable, try to merge - Node n = m.get( curr_ic ); std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n ); if( it!=tr->d_data.end() ){ processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries, @@ -555,11 +569,11 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, } if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){ int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex]; - Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index ); + //Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index ); //unique non-set variable, add to InstMatch for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){ InstMatch mn( &m ); - mn.set( curr_ic, it->first); + mn.setValue( curr_index, it->first); processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 ); } }else{ @@ -578,8 +592,9 @@ int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){ Assert( options::eagerInstQuant() ); int addedLemmas = 0; for( int i=0; i<(int)d_children.size(); i++ ){ - if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){ - InstMatch m; + Node t_op = qe->getTermDatabase()->getOperator( t ); + if( ((InstMatchGenerator*)d_children[i])->d_match_pattern_op==t_op ){ + InstMatch m( f ); //if it produces a match, then process it with the rest if( ((InstMatchGenerator*)d_children[i])->getMatch( f, t, m, qe ) ){ processNewMatch( qe, m, i, addedLemmas ); @@ -589,16 +604,29 @@ int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){ return addedLemmas; } +InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ) { + for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){ + if( d_match_pattern[i].getKind()==INST_CONSTANT ){ + d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute()); + } + } +} + +void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) { + d_op = qe->getTermDatabase()->getOperator( d_match_pattern ); +} + int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ - InstMatch m; + InstMatch m( f ); m.add( baseMatch ); int addedLemmas = 0; + if( d_match_pattern.getType()==NodeManager::currentNM()->booleanType() ){ for( int i=0; i<2; i++ ){ - addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]) ); + addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_op ]) ); } }else{ - addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) ); + addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_op ]) ); } return addedLemmas; } @@ -608,18 +636,18 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin //m is an instantiation if( qe->addInstantiation( d_f, m ) ){ addedLemmas++; - Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl; + Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl; } }else{ if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){ - Node ic = d_match_pattern[argIndex]; + int v = d_var_num[argIndex]; for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ Node t = it->first; - if( ( m.get( ic ).isNull() || m.get( ic )==t ) && ic.getType()==t.getType() ){ - Node prev = m.get( ic ); - m.set( ic, t); + Node prev = m.get( v ); + if( ( prev.isNull() || prev==t ) && d_match_pattern[argIndex].getType()==t.getType() ){ + m.setValue( v, t); addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); - m.set( ic, prev); + m.setValue( v, prev); } } }else{ @@ -634,10 +662,10 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){ Assert( options::eagerInstQuant() ); - InstMatch m; + InstMatch m( f ); for( int i=0; i<(int)t.getNumChildren(); i++ ){ if( d_match_pattern[i].getKind()==INST_CONSTANT ){ - m.set(d_match_pattern[i], t[i]); + m.setValue(d_var_num[i], t[i]); }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){ return 0; } diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 5d2128922..e7e07470d 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -65,6 +65,8 @@ private: Node d_eq_class; /** for arithmetic matching */ std::map< Node, Node > d_arith_coeffs; + /** variable numbers */ + std::map< int, int > d_var_num; /** initialize pattern */ void initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ); public: @@ -92,6 +94,8 @@ public: Node d_pattern; /** match pattern */ Node d_match_pattern; + /** match pattern op */ + Node d_match_pattern_op; public: /** reset instantiation round (call this whenever equivalence classes have changed) */ void resetInstantiationRound( QuantifiersEngine* qe ); @@ -165,15 +169,19 @@ private: Node d_f; /** match term */ Node d_match_pattern; + /** operator */ + Node d_op; + /** to indicies */ + std::map< int, int > d_var_num; /** add instantiations */ void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ); public: /** constructors */ - InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){} + InstMatchGeneratorSimple( Node f, Node pat ); /** destructor */ ~InstMatchGeneratorSimple(){} /** reset instantiation round (call this whenever equivalence classes have changed) */ - void resetInstantiationRound( QuantifiersEngine* qe ) {} + void resetInstantiationRound( QuantifiersEngine* qe ); /** reset, eqc is the equivalence class to search in (any if eqc=null) */ void reset( Node eqc, QuantifiersEngine* qe ) {} /** get the next match. must call reset( eqc ) before this function. (not implemented) */ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 6cc446e35..f9b4dd588 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -148,7 +148,7 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ // where e is a vector of terms , and t is vector of ground terms. // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant // We will construct the term ( beta - B*t)/coeff to use for e_i. - InstMatch m; + InstMatch m( f ); //By default, choose the first instantiation constant to be e_i. Node var = d_ceTableaux[ic][x].begin()->first; if( var.getType().isInteger() ){ @@ -292,7 +292,8 @@ bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar } instVal = Rewriter::rewrite( instVal ); //use as instantiation value for var - m.set(var, instVal); + int vn = var.getAttribute(InstVarNumAttribute()); + m.setValue( vn, instVal ); Debug("quant-arith") << "Add instantiation " << m << std::endl; return d_quantEngine->addInstantiation( f, m ); } @@ -333,13 +334,13 @@ int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){ if( e<2 ){ return InstStrategy::STATUS_UNFINISHED; }else if( e==2 ){ - InstMatch m; + InstMatch m( f ); for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){ Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); if( i.getType().isDatatype() ){ Node n = getValueFor( i ); Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl; - m.set(i,n); + m.setValue( j, n); } } //d_quantEngine->addInstantiation( f, m ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index fa5a8d844..460f71f7e 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -70,7 +70,7 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ if( processTrigger ){ //if( d_user_gen[f][i]->isMultiTrigger() ) Trace("process-trigger") << " Process (user) " << (*d_user_gen[f][i]) << "..." << std::endl; - InstMatch baseMatch; + InstMatch baseMatch( f ); int numInst = d_user_gen[f][i]->addInstantiations( baseMatch ); //if( d_user_gen[f][i]->isMultiTrigger() ) Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; @@ -169,7 +169,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) d_processed_trigger[f][tr] = true; //if( tr->isMultiTrigger() ) Trace("process-trigger") << " Process " << (*tr) << "..." << std::endl; - InstMatch baseMatch; + InstMatch baseMatch( f ); int numInst = tr->addInstantiations( baseMatch ); //if( tr->isMultiTrigger() ) Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; @@ -402,7 +402,7 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ if( d_guessed.find( f )==d_guessed.end() ){ Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; d_guessed[f] = true; - InstMatch m; + InstMatch m( f ); if( d_quantEngine->addInstantiation( f, m ) ){ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 707047b93..502a34176 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -264,11 +264,11 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ // Notice() << "Unhandled phase req: " << n << std::endl; // } //} + d_quant_basis_match[f] = InstMatch( f ); for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ - Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, j ); - Node t = d_qe->getTermDatabase()->getModelBasisTerm( ic.getType() ); + Node t = d_qe->getTermDatabase()->getModelBasisTerm( f[0][j].getType() ); //calculate the basis match for f - d_quant_basis_match[f].set( ic, t); + d_quant_basis_match[f].setValue( j, t ); } ++(d_statistics.d_num_quants_init); } @@ -428,9 +428,9 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i riter.increment2( depIndex ); }else{ //instantiation was not shown to be true, construct the match - InstMatch m; + InstMatch m( f ); for( int i=0; i<riter.getNumTerms(); i++ ){ - m.set( d_qe, f, riter.d_index_order[i], riter.getTerm( i ) ); + m.set( d_qe, riter.d_index_order[i], riter.getTerm( i ) ); } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; //add as instantiation @@ -840,7 +840,7 @@ int QModelBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ for( int i=0; i<igp.getNumMatches(); i++ ){ //if the match is not already true in the model if( igp.getMatchValue( i )!=fm->d_true ){ - InstMatch m; + InstMatch m( f ); igp.getMatch( d_qe->getEqualityQuery(), i, m ); //Trace("inst-gen-debug") << "Inst Gen : " << m << std::endl; //we only consider matches that are non-empty @@ -848,10 +848,10 @@ int QModelBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ if( !m.empty() ){ Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl; //translate to be in terms match in terms of fp - InstMatch mp; + InstMatch mp(f); getParentQuantifierMatch( mp, fp, m, f ); //if this is a partial instantion - if( !m.isComplete( f ) ){ + if( !m.isComplete() ){ //need to make it internal here //Trace("mkInternal") << "Make internal representative " << mp << std::endl; //mp.makeInternalRepresentative( d_qe ); @@ -1092,13 +1092,11 @@ void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, Ins //std::cout << " " << fp[0].getNumChildren() << " " << f[0].getNumChildren() << std::endl; int counter = 0; for( size_t i=0; i<fp[0].getNumChildren(); i++ ){ - Node icp = d_qe->getTermDatabase()->getInstantiationConstant( fp, i ); if( (int)counter< (int)f[0].getNumChildren() ){ if( fp[0][i]==f[0][counter] ){ - Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, counter ); - Node n = m.getValue( ic ); + Node n = m.get( counter ); if( !n.isNull() ){ - mp.setMatch( d_qe->getEqualityQuery(), icp, n ); + mp.set( d_qe, i, n ); } counter++; } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index ef4e67a68..9fe0407e5 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -261,9 +261,9 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ int addedLemmas = 0; while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ //instantiation was not shown to be true, construct the match - InstMatch m; + InstMatch m( f ); for( int i=0; i<riter.getNumTerms(); i++ ){ - m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) ); + m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) ); } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 33d658e0a..5e489c5be 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -140,8 +140,9 @@ void RelevantDomain::compute(){ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( n.getKind()==APPLY_UF ){ - RDomain * rf = getRDomain( n.getOperator(), i ); + Node op = d_qe->getTermDatabase()->getOperator( n ); + if( !op.isNull() ){ + RDomain * rf = getRDomain( op, i ); if( n[i].getKind()==INST_CONSTANT ){ Node q = d_qe->getTermDatabase()->getInstConstAttr( n[i] ); //merge the RDomains diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 441ab029c..81de1e11d 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -131,7 +131,7 @@ int RewriteEngine::checkRewriteRule( Node f ) { bool success; do { - InstMatch m; + InstMatch m( f ); success = d_rr_triggers[f][i]->getNextMatch( f, m ); if( success ){ //see if instantiation is true in the model diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 6b1368be1..39ba3e8af 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -61,6 +61,33 @@ void TermDb::addTermEfficient( Node n, std::set< Node >& added){ } +Node TermDb::getOperator( Node n ) { + //return n.getOperator(); + + if( n.getKind()==SELECT || n.getKind()==STORE ){ + //since it is parametric, use a particular one as op + TypeNode tn1 = n[0].getType(); + TypeNode tn2 = n[1].getType(); + Node op = n.getOperator(); + std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > >::iterator ito = d_par_op_map.find( op ); + if( ito!=d_par_op_map.end() ){ + std::map< TypeNode, std::map< TypeNode, Node > >::iterator it = ito->second.find( tn1 ); + if( it!=ito->second.end() ){ + std::map< TypeNode, Node >::iterator it2 = it->second.find( tn2 ); + if( it2!=it->second.end() ){ + return it2->second; + } + } + } + d_par_op_map[op][tn1][tn2] = n; + return n; + }else if( n.getKind()==APPLY_UF ){ + return n.getOperator(); + }else{ + return Node::null(); + } +} + void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ //don't add terms in quantifier bodies if( withinQuant && !options::registerQuantBodyTerms() ){ @@ -77,7 +104,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ if( !TermDb::hasInstConstAttr(n) ){ Trace("term-db") << "register term in db " << n << std::endl; //std::cout << "register trigger term " << n << std::endl; - Node op = n.getOperator(); + Node op = getOperator( n ); d_op_map[op].push_back( n ); added.insert( n ); @@ -170,7 +197,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ computeModelBasisArgAttribute( en ); if( en.getKind()==APPLY_UF && !TermDb::hasInstConstAttr(en) ){ if( !en.getAttribute(NoMatchAttribute()) ){ - Node op = en.getOperator(); + Node op = getOperator( en ); if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ NoMatchAttribute nma; en.setAttribute(nma,true); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 177d8b230..860f087dd 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -111,6 +111,9 @@ private: QuantifiersEngine* d_quantEngine; /** terms processed */ std::hash_set< Node, NodeHashFunction > d_processed; +private: + /** select op map */ + std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > > d_par_op_map; public: TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ){} ~TermDb(){} @@ -128,6 +131,8 @@ public: void addTerm( Node n, std::set< Node >& added, bool withinQuant = false ); /** reset (calculate which terms are active) */ void reset( Theory::Effort effort ); + /** get operation */ + Node getOperator( Node n ); private: /** for efficient e-matching */ void addTermEfficient( Node n, std::set< Node >& added); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index b13e76afb..6912c9e89 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -70,7 +70,8 @@ d_quantEngine( qe ), d_f( f ){ //Notice() << "Trigger : " << (*this) << " for " << f << std::endl; if( options::eagerInstQuant() ){ for( int i=0; i<(int)d_nodes.size(); i++ ){ - qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() ); + Node op = qe->getTermDatabase()->getOperator( d_nodes[i] ); + qe->getTermDatabase()->registerTrigger( this, op ); } } Trace("trigger-debug") << "Finished making trigger." << std::endl; diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 28fb2acda..23cf5f5d0 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -114,12 +114,14 @@ public: static bool isBooleanTermTrigger( Node n ); inline void toStream(std::ostream& out) const { + /* out << "TRIGGER( "; for( int i=0; i<(int)d_nodes.size(); i++ ){ if( i>0 ){ out << ", "; } out << d_nodes[i]; } out << " )"; + */ } }; |