From d3822db24e15e255766866a47e6ffa0d8d91911b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 28 Jan 2014 09:51:33 -0600 Subject: [PATCH] More optimizations of quantifier instantiation data structures. --- .../quantifiers/candidate_generator.cpp | 4 +- src/theory/quantifiers/inst_gen.cpp | 13 +- src/theory/quantifiers/inst_gen.h | 1 + src/theory/quantifiers/inst_match.cpp | 256 +++++------------- src/theory/quantifiers/inst_match.h | 68 ++--- .../quantifiers/inst_match_generator.cpp | 108 +++++--- src/theory/quantifiers/inst_match_generator.h | 12 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 9 +- .../quantifiers/inst_strategy_e_matching.cpp | 6 +- src/theory/quantifiers/model_builder.cpp | 22 +- src/theory/quantifiers/model_engine.cpp | 4 +- src/theory/quantifiers/relevant_domain.cpp | 5 +- src/theory/quantifiers/rewrite_engine.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 31 ++- src/theory/quantifiers/term_database.h | 5 + src/theory/quantifiers/trigger.cpp | 3 +- src/theory/quantifiers/trigger.h | 2 + src/theory/quantifiers_engine.cpp | 11 +- .../rewriterules/efficient_e_matching.cpp | 8 +- src/theory/rewriterules/rr_inst_match.cpp | 158 ++++++++++- src/theory/rewriterules/rr_inst_match.h | 78 +++++- .../rewriterules/theory_rewriterules.cpp | 6 +- src/theory/rewriterules/theory_rewriterules.h | 4 +- .../theory_rewriterules_rules.cpp | 2 +- 24 files changed, 485 insertions(+), 333 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; jgetEqualityQuery(), 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; id_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::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; iareEqual( 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[i] << std::endl; + } } } -void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ - for( size_t i=0; igetTermDatabase()->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::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::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; igetTermDatabase()->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; igetEqualityQuery()->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; igetTermDatabase()->getInstantiationConstant( f, i ), n ); +void InstMatch::clear() { + for( unsigned i=0; id_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[i]; + printed = true; + } } out << " )"; } - - - //for rewrite rules - /** apply rewrite */ void applyRewrite(); - /** erase */ - template - 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; igetEqualityQuery() ); 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; igetTermDatabase()->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; id_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; igetTermDatabase()->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; igetTermDatabase()->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 << " )"; + */ } }; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 6f3879d39..a454d8334 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -290,8 +290,8 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ } void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, 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] ); + for( size_t i=0; i terms; //make sure there are values for each variable we are instantiating for( size_t i=0; igetInstantiationConstant( f, i ); - Node val = m.getValue( ic ); + Node val = m.get( i ); if( val.isNull() ){ + Node ic = d_term_db->getInstantiationConstant( f, i ); val = d_term_db->getFreeVariableForInstConstant( ic ); Trace("inst-add-debug") << "mkComplete " << val << std::endl; } @@ -498,8 +498,8 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo Trace("inst-add-debug") << std::endl; //check for duplication - bool alreadyExists = false; ///* + bool alreadyExists = false; if( options::incrementalSolving() ){ Trace("inst-add-debug") << "Adding into context-dependent inst trie" << std::endl; inst::CDInstMatchTrie* imt; @@ -520,6 +520,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo ++(d_statistics.d_inst_duplicate_eq); return false; } + //*/ //add the instantiation bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms ); diff --git a/src/theory/rewriterules/efficient_e_matching.cpp b/src/theory/rewriterules/efficient_e_matching.cpp index a9e1cfbb5..05934fc8b 100644 --- a/src/theory/rewriterules/efficient_e_matching.cpp +++ b/src/theory/rewriterules/efficient_e_matching.cpp @@ -612,9 +612,6 @@ void EfficientEMatcher::registerEfficientHandler( EfficientHandler& handler, if( c.getType() == ty ) ele.insert(c); } if( !ele.empty() ){ - // for(std::vector::iterator i = db->d_op_map[op].begin(), end = db->d_op_map[op].end(); i != end; ++i){ - // if(CandidateGenerator::isLegalCandidate(*i)) ele.insert(*i); - // } if(Debug.isOn("efficient-e-match-stats")){ Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl; } @@ -641,13 +638,10 @@ void EfficientEMatcher::registerEfficientHandler( EfficientHandler& handler, } } else { - Node op = pats[0].getOperator(); TermDb* db = d_quantEngine->getTermDatabase(); + Node op = db->getOperator( pats[0] ); if(db->d_op_map[op].begin() != db->d_op_map[op].end()){ SetNode ele; - // for(std::vector::iterator i = db->d_op_map[op].begin(), end = db->d_op_map[op].end(); i != end; ++i){ - // if(CandidateGenerator::isLegalCandidate(*i)) ele.insert(*i); - // } ele.insert(db->d_op_map[op].begin(), db->d_op_map[op].end()); if(Debug.isOn("efficient-e-match-stats")){ Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl; diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp index 4908e5ec0..2d7cf85fd 100644 --- a/src/theory/rewriterules/rr_inst_match.cpp +++ b/src/theory/rewriterules/rr_inst_match.cpp @@ -37,7 +37,146 @@ namespace CVC4{ namespace theory{ namespace rrinst{ -typedef CVC4::theory::inst::InstMatch InstMatch; + + + +InstMatch::InstMatch() { +} + +InstMatch::InstMatch( InstMatch* m ) { + d_map = m->d_map; +} + +bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){ + std::map< Node, Node >::iterator vn = d_map.find( v ); + if( !m.isNull() && !m.getType().isSubtypeOf( v.getType() ) ){ + set = false; + return false; + }else if( vn==d_map.end() || vn->second.isNull() ){ + set = true; + this->set(v,m); + Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl; + return true; + }else{ + set = false; + return q->areEqual( vn->second, m ); + } +} + +bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){ + bool set; + return setMatch(q,v,m,set); +} + +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; + } + } + } + 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; + }else{ + if( !q->areEqual( it->second, itf->second ) ){ + d_map.clear(); + return false; + } + } + } + } + return true; +} + +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 ){ + for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ); + if( d_map.find( ic )==d_map.end() ){ + d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); + } + } +} + +//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 ) ){ + d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second ); + } + } +} + +void InstMatch::applyRewrite(){ + for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ + it->second = Rewriter::rewrite(it->second); + } +} + +/** 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(); + } +} + +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")) { + // 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 ; + } + } + 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 ); +} + + + + + + +typedef CVC4::theory::rrinst::InstMatch InstMatch; typedef CVC4::theory::inst::CandidateGeneratorQueue CandidateGeneratorQueue; template @@ -569,7 +708,8 @@ class AllOpMatcher: public PatMatcher{ AuxMatcher2 am2(am3,LegalTest()); /** Iter on the equivalence class of the given term */ TermDb* tdb = qe->getTermDatabase(); - CandidateGeneratorTheoryUfOp cdtUfEq(pat.getOperator(),tdb); + Node op = tdb->getOperator( pat ); + CandidateGeneratorTheoryUfOp cdtUfEq(op,tdb); /* Create a matcher from the candidate generator */ AuxMatcher1 am1(cdtUfEq,am2); return am1; @@ -1204,8 +1344,13 @@ int MultiPatsMatcher::addInstantiations( InstMatch& baseMatch, Node quant, Quant d_im.add( baseMatch ); while( getNextMatch( qe ) ){ InstMatch im_copy = getInstMatch(); + std::vector< Node > terms; + for( unsigned i=0; igetEqualityQuery() ); - if( qe->addInstantiation( quant, im_copy ) ){ + if( qe->addInstantiation( quant, terms ) ){ addedLemmas++; } } @@ -1428,8 +1573,13 @@ int MultiEfficientPatsMatcher::addInstantiations( InstMatch& baseMatch, Node qua resetInstantiationRound( qe ); while( getNextMatch( qe ) ){ InstMatch im_copy = getInstMatch(); + std::vector< Node > terms; + for( unsigned i=0; igetEqualityQuery() ); - if( qe->addInstantiation( quant, im_copy ) ){ + if( qe->addInstantiation( quant, terms ) ){ addedLemmas++; } } diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h index aa89430c1..c42dd8914 100644 --- a/src/theory/rewriterules/rr_inst_match.h +++ b/src/theory/rewriterules/rr_inst_match.h @@ -29,7 +29,6 @@ #include "theory/uf/theory_uf.h" #include "context/cdlist.h" -#include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/term_database.h" #include "expr/node_manager.h" #include "expr/node_builder.h" @@ -42,8 +41,85 @@ namespace CVC4 { namespace theory { +class EqualityQuery; + namespace rrinst{ +/** basic class defining an instantiation */ +class InstMatch { + /* map from variable to ground terms */ + std::map< Node, Node > d_map; +public: + InstMatch(); + 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 & set); + /** fill all unfilled values with m */ + bool add( InstMatch& m ); + /** if compatible, fill all unfilled values with m and return true + return false otherwise */ + bool merge( EqualityQuery* q, InstMatch& m ); + /** debug print method */ + void debugPrint( const char* c ); + /** is complete? */ + bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); } + /** 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; + /** clear */ + void clear(){ d_map.clear(); } + /** is_empty */ + bool empty(){ return d_map.empty(); } + /** 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; + } + out << " )"; + } + + + //for rewrite rules + + /** apply rewrite */ + void applyRewrite(); + /** erase */ + template + 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 ); + /** 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) */ + Node d_matched; +};/* class InstMatch */ + + + class CandidateGenerator { public: diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index df74ea8b3..7fe625da1 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -139,7 +139,7 @@ TheoryRewriteRules::TheoryRewriteRules(context::Context* c, } void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r, - InstMatch & im, + rrinst::InstMatch & im, bool delay){ ++r->nb_matched; ++d_statistics.d_match_found; @@ -214,7 +214,7 @@ void TheoryRewriteRules::check(Effort level) { /** Test the possible matching one by one */ while(tr.getNextMatch()){ - InstMatch im = tr.getInstMatch(); + rrinst::InstMatch im = tr.getInstMatch(); addMatchRuleTrigger(r, im, true); } } @@ -540,7 +540,7 @@ void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){ ApplyMatcher * tr = r->trigger_for_body_match; Assert(tr != NULL); tr->resetInstantiationRound(getQuantifiersEngine()); - InstMatch im; + rrinst::InstMatch im; TNode m = inst->substNode(*this,(*p).first, cache); Assert( m.getKind() == kind::APPLY_UF ); ee->addTerm(m); diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index ea9eb4769..30e6f9709 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -81,7 +81,7 @@ typedef std::hash_map TCache; ~RewriteRule(); bool noGuard()const throw () { return guards.size() == 0; }; - bool inCache(TheoryRewriteRules & re, InstMatch & im)const; + bool inCache(TheoryRewriteRules & re, rrinst::InstMatch & im)const; void toStream(std::ostream& out) const; @@ -249,7 +249,7 @@ private: void addRewriteRule(const Node r); void computeMatchBody ( const RewriteRule * r, size_t start = 0); void addMatchRuleTrigger(const RewriteRule* r, - InstMatch & im, bool delay = true); + rrinst::InstMatch & im, bool delay = true); Node normalizeConjunction(NodeBuilder<> & conjunction); diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp index 7e1d42bb2..38e22ed64 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.cpp +++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp @@ -328,7 +328,7 @@ RewriteRule::RewriteRule(TheoryRewriteRules & re, }; -bool RewriteRule::inCache(TheoryRewriteRules & re, InstMatch & im)const{ +bool RewriteRule::inCache(TheoryRewriteRules & re, rrinst::InstMatch & im)const{ bool res = !d_cache.addInstMatch(im); Debug("rewriterules::matching") << "rewriterules::cache " << im << (res ? " HIT" : " MISS") << std::endl; -- 2.30.2