From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 28 Jan 2014 15:51:33 +0000 (-0600)
Subject: More optimizations of quantifier instantiation data structures.
X-Git-Tag: cvc5-1.0.0~7118
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d3822db24e15e255766866a47e6ffa0d8d91911b;p=cvc5.git

More optimizations of quantifier instantiation data structures.
---

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 << " )";
+    */
   }
 };
 
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; i<d_term_db->d_inst_constants[f].size(); i++ ){
-    Node n = m.getValue( d_term_db->d_inst_constants[f][i] );
+  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+    Node n = m.get( i );
     if( !n.isNull() ){
       vars.push_back( f[0][i] );
       terms.push_back( n );
@@ -471,9 +471,9 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool
   std::vector< Node > terms;
   //make sure there are values for each variable we are instantiating
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    Node ic = d_term_db->getInstantiationConstant( 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<Node>::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<Node>::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; 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 );
+    }
+  }
+}
+
+//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<bool modEq>
@@ -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; i<quant[0].getNumChildren(); i++ ){
+      terms.push_back( im_copy.get( qe, quant, i ) );
+    }
+
     //m.makeInternal( d_quantEngine->getEqualityQuery() );
-    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; i<quant[0].getNumChildren(); i++ ){
+      terms.push_back( im_copy.get( qe, quant, i ) );
+    }
+
     //m.makeInternal( d_quantEngine->getEqualityQuery() );
-    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<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 );
+  /** 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<TNode, TNode, TNodeHashFunction> 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;