More optimization of QCF and instantiation caching. Fix CDInstMatchTrie.

10 files changed, 261 insertions, 257 deletions

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index c7d7b7415..d542e878c 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -672,12 +672,8 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
                 }
               }else{
                 //just add the instance
-                InstMatch m;
-                for( unsigned j=0; j<inst.size(); j++) {
-                  m.set( d_qe, f, j, inst[j] );
-                }
                 d_triedLemmas++;
-                if( d_qe->addInstantiation( f, m ) ){
+                if( d_qe->addInstantiation( f, inst ) ){
                   Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
                   d_addedLemmas++;
                 }else{
@@ -792,13 +788,9 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size();
       Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
       if (ev!=d_true) {
-        InstMatch m;
-        for( unsigned i=0; i<inst.size(); i++ ){
-          m.set( d_qe, f, i, inst[i] );
-        }
         Trace("fmc-exh-debug") << ", add!";
         //add as instantiation
-        if( d_qe->addInstantiation( f, m ) ){
+        if( d_qe->addInstantiation( f, inst ) ){
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;
         }else{
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 8428069aa..8d472879e 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -34,18 +34,18 @@ InstMatch::InstMatch( InstMatch* m ) {
   d_map = m->d_map;
 }
 
-bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){
+bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & st ){
   std::map< Node, Node >::iterator vn = d_map.find( v );
   if( !m.isNull() && !m.getType().isSubtypeOf( v.getType() ) ){
-    set = false;
+    st = false;
     return false;
   }else if( vn==d_map.end() || vn->second.isNull() ){
-    set = true;
-    this->set(v,m);
+    st = true;
+    set(v,m);
     Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl;
     return true;
   }else{
-    set = false;
+    st = false;
     return q->areEqual( vn->second, m );
   }
 }
@@ -88,13 +88,6 @@ void InstMatch::debugPrint( const char* c ){
   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
     Debug( c ) << "   " << it->first << " -> " << it->second << std::endl;
   }
-  //if( !d_splits.empty() ){
-  //  Debug( c ) << "   Conditions: ";
-  //  for( std::map< Node, Node >::iterator it = d_splits.begin(); it !=d_splits.end(); ++it ){
-  //    Debug( c ) << it->first << " = " << it->second << " ";
-  //  }
-  //  Debug( c ) << std::endl;
-  //}
 }
 
 void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
@@ -106,13 +99,6 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
   }
 }
 
-//void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){
-//  EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery();
-//  for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
-//    d_map[ it->first ] = eqqe->getInternalRepresentative( it->second );
-//  }
-//}
-
 void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
     if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){
@@ -144,7 +130,6 @@ Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) {
 void InstMatch::set(TNode var, TNode n){
   Assert( !var.isNull() );
   if (Trace.isOn("inst-match-warn")) {
-    // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
     if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){
       Trace("inst-match-warn") << quantifiers::TermDb::getInstConstAttr(var) << std::endl;
       Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
@@ -160,40 +145,35 @@ void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) {
 
 
 
-
-/*
-void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
-  if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
-    int i_index = imtio ? imtio->d_order[index] : index;
-    Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
-    d_data[n].addInstMatch2( qe, f, m, index+1, imtio );
-  }
-}
-
-bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){
-  if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
-    return true;
+bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m,
+                                  bool modEq, bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ){
+  if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
+    return false;
   }else{
     int i_index = imtio ? imtio->d_order[index] : index;
     Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
     std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
     if( it!=d_data.end() ){
-      if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
-        return true;
+      bool ret = it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 );
+      if( !onlyExist || !ret ){
+        return ret;
       }
     }
+    /*
     //check if m is an instance of another instantiation if modInst is true
     if( modInst ){
       if( !n.isNull() ){
         Node nl;
-        it = d_data.find( nl );
-        if( it!=d_data.end() ){
-          if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
-            return true;
+        std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl );
+        if( itm!=d_data.end() ){
+          if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
+            return false;
           }
         }
       }
     }
+    */
+    /*
     if( modEq ){
       //check modulo equality if any other instantiation match exists
       if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
@@ -204,8 +184,8 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch&
           if( en!=n ){
             std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
             if( itc!=d_data.end() ){
-              if( itc->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
-                return true;
+              if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
+                return false;
               }
             }
           }
@@ -213,105 +193,95 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch&
         }
       }
     }
-    return false;
-  }
-}
-
-bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
-  return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio );
-}
-
-bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
-  if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){
-    addInstMatch2( qe, f, m, 0, imtio );
+*/
+    if( !onlyExist ){
+      d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
+    }
     return true;
-  }else{
-    return false;
   }
 }
-*/
-
-
-
 
-bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ){
+bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq,
+                                  bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ) {
   if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
     return false;
   }else{
     int i_index = imtio ? imtio->d_order[index] : index;
-    Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
+    Node n = m[i_index];
     std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
     if( it!=d_data.end() ){
-      return it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 );
-    }else{
-
-      /*
-      //check if m is an instance of another instantiation if modInst is true
-      if( modInst ){
-        if( !n.isNull() ){
-          Node nl;
-          std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl );
-          if( itm!=d_data.end() ){
-            if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
-              return false;
-            }
+      bool ret = it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 );
+      if( !onlyExist || !ret ){
+        return ret;
+      }
+    }
+    /*
+    //check if m is an instance of another instantiation if modInst is true
+    if( modInst ){
+      if( !n.isNull() ){
+        Node nl;
+        std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl );
+        if( itm!=d_data.end() ){
+          if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
+            return false;
           }
         }
       }
-      */
-      /*
-      if( modEq ){
-        //check modulo equality if any other instantiation match exists
-        if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
-          eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
-                                   qe->getEqualityQuery()->getEngine() );
-          while( !eqc.isFinished() ){
-            Node en = (*eqc);
-            if( en!=n ){
-              std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
-              if( itc!=d_data.end() ){
-                if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
-                  return false;
-                }
+    }
+    */
+    /*
+    if( modEq ){
+      //check modulo equality if any other instantiation match exists
+      if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+        eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
+                                 qe->getEqualityQuery()->getEngine() );
+        while( !eqc.isFinished() ){
+          Node en = (*eqc);
+          if( en!=n ){
+            std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
+            if( itc!=d_data.end() ){
+              if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
+                return false;
               }
             }
-            ++eqc;
           }
+          ++eqc;
         }
       }
-      */
-      if( !onlyExist ){
-        d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
-      }
-      return true;
     }
+    */
+    if( !onlyExist ){
+      d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
+    }
+    return true;
   }
 }
 
-
-
 /** exists match */
-bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
+bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m,
+                                    context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
+  bool reset = false;
   if( !d_valid.get() ){
     if( onlyExist ){
-      return false;
+      return true;
     }else{
       d_valid.set( true );
+      reset = true;
     }
   }
   if( index==(int)f[0].getNumChildren() ){
-    return true;
+    return false;
   }else{
     Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, index ) );
-    if( onlyExist ){
-      std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
-      if( it!=d_data.end() ){
-        if( !it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
-          return false;
-        }
+    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+    if( it!=d_data.end() ){
+      bool ret = it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, onlyExist );
+      if( !onlyExist || !ret ){
+        return reset || ret;
       }
     }
     //check if m is an instance of another instantiation if modInst is true
+    /*
     if( modInst ){
       if( !n.isNull() ){
         Node nl;
@@ -323,6 +293,7 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m,
         }
       }
     }
+    */
     if( modEq ){
       //check modulo equality if any other instantiation match exists
       if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
@@ -342,19 +313,80 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m,
         }
       }
     }
+
     if( !onlyExist ){
       std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
-      CDInstMatchTrie* imt;
-      if( it!=d_data.end() ){
-        imt = it->second;
-        it->second->d_valid.set( true );
-      }else{
-        imt = new CDInstMatchTrie( c );
-        d_data[n] = imt;
-      }
-      return imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false );
+      CDInstMatchTrie* imt = new CDInstMatchTrie( c );
+      d_data[n] = imt;
+      imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false );
     }
+    return true;
+  }
+}
+
+bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
+                                    context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
+  bool reset = false;
+  if( !d_valid.get() ){
+    if( onlyExist ){
+      return true;
+    }else{
+      d_valid.set( true );
+      reset = true;
+    }
+  }
+  if( index==(int)f[0].getNumChildren() ){
     return false;
+  }else{
+    Node n = m[ index ];
+    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+    if( it!=d_data.end() ){
+      bool ret = it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, onlyExist );
+      if( !onlyExist || !ret ){
+        return reset || ret;
+      }
+    }
+    //check if m is an instance of another instantiation if modInst is true
+    /*
+    if( modInst ){
+      if( !n.isNull() ){
+        Node nl;
+        std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl );
+        if( itm!=d_data.end() ){
+          if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
+            return false;
+          }
+        }
+      }
+    }
+    */
+    if( modEq ){
+      //check modulo equality if any other instantiation match exists
+      if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+        eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
+                                 qe->getEqualityQuery()->getEngine() );
+        while( !eqc.isFinished() ){
+          Node en = (*eqc);
+          if( en!=n ){
+            std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
+            if( itc!=d_data.end() ){
+              if( itc->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
+                return false;
+              }
+            }
+          }
+          ++eqc;
+        }
+      }
+    }
+
+    if( !onlyExist ){
+      std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+      CDInstMatchTrie* imt = new CDInstMatchTrie( c );
+      d_data[n] = imt;
+      imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false );
+    }
+    return true;
   }
 }
 
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 2cf33bc8e..eb7f50095 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -45,7 +45,7 @@ public:
   /** set the match of v to m */
   bool setMatch( EqualityQuery* q, TNode v, TNode m );
   /* This version tell if the variable has been set */
-  bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & set);
+  bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & st);
   /** fill all unfilled values with m */
   bool add( InstMatch& m );
   /** if compatible, fill all unfilled values with m and return true
@@ -134,55 +134,20 @@ public:
                         bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
     return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
   }
+  bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
+                        bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
+    return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
+  }
   /** add match m for quantifier f, take into account equalities if modEq = true,
       if imtio is non-null, this is the order to add to trie
       return true if successful
   */
   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
                      bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
+  bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
+                     bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
 };/* class InstMatchTrie */
 
-
-#if 0
-
-/** trie for InstMatch objects */
-class CDInstMatchTrie {
-public:
-  class ImtIndexOrder {
-  public:
-    std::vector< int > d_order;
-  };/* class InstMatchTrie ImtIndexOrder */
-private:
-  /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
-  void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio );
-  /** exists match */
-  bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
-public:
-  /** the data */
-  std::map< Node, CDInstMatchTrie* > d_data;
-  /** is valid */
-  context::CDO< bool > d_valid;
-public:
-  CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
-  ~CDInstMatchTrie(){}
-public:
-  /** return true if m exists in this trie
-        modEq is if we check modulo equality
-        modInst is if we return true if m is an instance of a match that exists
-   */
-  bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                        bool modInst = false, ImtIndexOrder* imtio = NULL );
-  /** add match m for quantifier f, take into account equalities if modEq = true,
-      if imtio is non-null, this is the order to add to trie
-      return true if successful
-  */
-  bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
-                     bool modInst = false, ImtIndexOrder* imtio = NULL );
-};/* class CDInstMatchTrie */
-
-#else
-
-
 /** trie for InstMatch objects */
 class CDInstMatchTrie {
 public:
@@ -202,12 +167,18 @@ public:
                         bool modInst = false, int index = 0 ) {
     return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
   }
+  bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
+                        bool modInst = false, int index = 0 ) {
+    return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
+  }
   /** add match m for quantifier f, take into account equalities if modEq = true,
       if imtio is non-null, this is the order to add to trie
       return true if successful
   */
   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
                      bool modInst = false, int index = 0, bool onlyExist = false );
+  bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
+                     bool modInst = false, int index = 0, bool onlyExist = false );
 };/* class CDInstMatchTrie */
 
 
@@ -232,9 +203,6 @@ public:
   }
 };/* class InstMatchTrieOrdered */
 
-#endif
-
-
 }/* CVC4::theory::inst namespace */
 
 typedef CVC4::theory::inst::InstMatch InstMatch;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 6a9327967..fa5a8d844 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -386,11 +386,11 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
         if( success ){
           index--;
           //try instantiation
-          InstMatch m;
+          std::vector< Node > terms;
           for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-            m.set( d_quantEngine, f, i, rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+            terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
           }
-          if( d_quantEngine->addInstantiation( f, m, true, false, false ) ){
+          if( d_quantEngine->addInstantiation( f, terms, false ) ){
             ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
             return STATUS_UNKNOWN;
           }
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 493d54b53..707047b93 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -275,7 +275,7 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
     //try to add it
     Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
     //add model basis instantiation
-    if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){
+    if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false ) ){
       d_quant_basis_match_added[f] = true;
       return 1;
     }else{
diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp
index ce85cecc0..ece519d1c 100755
--- a/src/theory/quantifiers/qinterval_builder.cpp
+++ b/src/theory/quantifiers/qinterval_builder.cpp
@@ -1036,14 +1036,12 @@ bool QIntervalBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q,
         if( fmqint->d_var_order[q]->getInstantiation( fmqint, l, u, inst ) ){

           Trace("qint-inst") << "** Instantiate with ";

           //just add the instance

-          InstMatch m;

           for( unsigned j=0; j<inst.size(); j++) {

-            m.set( d_qe, q, j, inst[j] );

             Trace("qint-inst") << inst[j] << " ";

           }

           Trace("qint-inst") << std::endl;

           d_triedLemmas++;

-          if( d_qe->addInstantiation( q, m ) ){

+          if( d_qe->addInstantiation( q, inst ) ){

             Trace("qint-inst") << "   ...added instantiation." << std::endl;

             d_addedLemmas++;

           }else{

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 665ae5329..aead93d07 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -69,9 +69,19 @@ void QcfNodeIndex::debugPrint( const char * c, int t ) {
 }

 

 

+void QuantInfo::initialize( Node q ) {

+  d_q = q;

+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){

+    d_match.push_back( TNode::null() );

+    d_match_term.push_back( TNode::null() );

+  }

+}

+

 void QuantInfo::reset_round( QuantConflictFind * p ) {

-  d_match.clear();

-  d_match_term.clear();

+  for( unsigned i=0; i<d_match.size(); i++ ){

+    d_match[i] = TNode::null();

+    d_match_term[i] = TNode::null();

+  }

   d_curr_var_deq.clear();

   //add built-in variable constraints

   for( unsigned r=0; r<2; r++ ){

@@ -102,9 +112,8 @@ void QuantInfo::reset_round( QuantConflictFind * p ) {
 }

 

 int QuantInfo::getCurrentRepVar( int v ) {

-  std::map< int, TNode >::iterator it = d_match.find( v );

-  if( it!=d_match.end() ){

-    int vn = getVarNum( it->second );

+  if( v!=-1 && !d_match[v].isNull() ){

+    int vn = getVarNum( d_match[v] );

     if( vn!=-1 ){

       //int vr = getCurrentRepVar( vn );

       //d_match[v] = d_vars[vr];

@@ -120,12 +129,11 @@ TNode QuantInfo::getCurrentValue( TNode n ) {
   if( v==-1 ){

     return n;

   }else{

-    std::map< int, TNode >::iterator it = d_match.find( v );

-    if( it==d_match.end() ){

+    if( d_match[v].isNull() ){

       return n;

     }else{

-      Assert( getVarNum( it->second )!=v );

-      return getCurrentValue( it->second );

+      Assert( getVarNum( d_match[v] )!=v );

+      return getCurrentValue( d_match[v] );

     }

   }

 }

@@ -170,8 +178,8 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
       if( doRemove ){

         if( vn!=-1 ){

           //if set to this in the opposite direction, clean up opposite instead

-          std::map< int, TNode >::iterator itmn = d_match.find( vn );

-          if( itmn!=d_match.end() && itmn->second==d_vars[v] ){

+          //          std::map< int, TNode >::iterator itmn = d_match.find( vn );

+          if( d_match[vn]==d_vars[v] ){

             return addConstraint( p, vn, d_vars[v], v, true, true );

           }else{

             //unsetting variables equal

@@ -190,20 +198,20 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
             }

           }

         }

-        d_match.erase( v );

+        d_match[v] = TNode::null();

         return 1;

       }else{

-        std::map< int, TNode >::iterator itm = d_match.find( v );

+        //std::map< int, TNode >::iterator itm = d_match.find( v );

 

         if( vn!=-1 ){

           Debug("qcf-match-debug") << "  ...Variable bound to variable" << std::endl;

-          std::map< int, TNode >::iterator itmn = d_match.find( vn );

-          if( itm==d_match.end() ){

+          //std::map< int, TNode >::iterator itmn = d_match.find( vn );

+          if( d_match[v].isNull() ){

             //setting variables equal

             bool alreadySet = false;

-            if( itmn!=d_match.end() ){

+            if( !d_match[vn].isNull() ){

               alreadySet = true;

-              Assert( !itmn->second.isNull() && !isVar( itmn->second ) );

+              Assert( !isVar( d_match[vn] ) );

             }

 

             //copy or check disequalities

@@ -216,7 +224,7 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
                     d_curr_var_deq[vn][dv] = v;

                   }

                 }else{

-                  if( !p->areMatchDisequal( itmn->second, dv ) ){

+                  if( !p->areMatchDisequal( d_match[vn], dv ) ){

                     Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;

                     return -1;

                   }

@@ -227,24 +235,23 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
               n = getCurrentValue( n );

             }

           }else{

-            if( itmn==d_match.end() ){

+            if( d_match[vn].isNull() ){

               Debug("qcf-match-debug") << " ...Reverse direction" << std::endl;

               //set the opposite direction

               return addConstraint( p, vn, d_vars[v], v, true, false );

             }else{

               Debug("qcf-match-debug") << "  -> Both variables bound, compare" << std::endl;

               //are they currently equal

-              return p->areMatchEqual( itm->second, itmn->second ) ? 0 : -1;

+              return p->areMatchEqual( d_match[v], d_match[vn] ) ? 0 : -1;

             }

           }

         }else{

           Debug("qcf-match-debug") << "  ...Variable bound to ground" << std::endl;

-          if( itm==d_match.end() ){

-

+          if( d_match[v].isNull() ){

           }else{

             //compare ground values

-            Debug("qcf-match-debug") << "  -> Ground value, compare " << itm->second << " "<< n << std::endl;

-            return p->areMatchEqual( itm->second, n ) ? 0 : -1;

+            Debug("qcf-match-debug") << "  -> Ground value, compare " << d_match[v] << " "<< n << std::endl;

+            return p->areMatchEqual( d_match[v], n ) ? 0 : -1;

           }

         }

         if( setMatch( p, v, n ) ){

@@ -271,10 +278,10 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
       }else{

         if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){

           //check if it respects equality

-          std::map< int, TNode >::iterator itm = d_match.find( v );

-          if( itm!=d_match.end() ){

+          //std::map< int, TNode >::iterator itm = d_match.find( v );

+          if( !d_match[v].isNull() ){

             TNode nv = getCurrentValue( n );

-            if( !p->areMatchDisequal( nv, itm->second ) ){

+            if( !p->areMatchDisequal( nv, d_match[v] ) ){

               Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;

               return -1;

             }

@@ -296,8 +303,9 @@ bool QuantInfo::isConstrainedVar( int v ) {
     return true;

   }else{

     Node vv = getVar( v );

-    for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){

-      if( it->second==vv ){

+    //for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){

+    for( unsigned i=0; i<d_match.size(); i++ ){

+      if( d_match[i]==vv ){

         return true;

       }

     }

@@ -324,9 +332,9 @@ bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n ) {
 

 bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {

   for( int i=0; i<getNumVars(); i++ ){

-    std::map< int, TNode >::iterator it = d_match.find( i );

-    if( it!=d_match.end() ){

-      if( !getCurrentCanBeEqual( p, i, it->second, p->d_effort==QuantConflictFind::effort_conflict ) ){

+    //std::map< int, TNode >::iterator it = d_match.find( i );

+    if( !d_match[i].isNull() ){

+      if( !getCurrentCanBeEqual( p, i, d_match[i], p->d_effort==QuantConflictFind::effort_conflict ) ){

         return true;

       }

     }

@@ -340,7 +348,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
   std::vector< int > unassigned[2];

   std::vector< TypeNode > unassigned_tn[2];

   for( int i=0; i<getNumVars(); i++ ){

-    if( d_match.find( i )==d_match.end() ){

+    if( d_match[i].isNull() ){

       //Assert( i<(int)q[0].getNumChildren() );

       int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;

       unassigned[rindex].push_back( i );

@@ -421,7 +429,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
           Trace("qcf-check-unassign") << "  Try: " << std::endl;

           for( unsigned i=0; i<unassigned[r].size(); i++ ){

             int ui = unassigned[r][i];

-            if( d_match.find( ui )!=d_match.end() ){

+            if( !d_match[ui].isNull() ){

               Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;

             }

           }

@@ -433,7 +441,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
     return true;

   }else{

     for( unsigned i=0; i<assigned.size(); i++ ){

-      d_match.erase( assigned[i] );

+      d_match[ assigned[i] ] = TNode::null();

     }

     assigned.clear();

     return false;

@@ -443,7 +451,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
 void QuantInfo::debugPrintMatch( const char * c ) {

   for( int i=0; i<getNumVars(); i++ ){

     Trace(c) << "  " << d_vars[i] << " -> ";

-    if( d_match.find( i )!=d_match.end() ){

+    if( !d_match[i].isNull() ){

       Trace(c) << d_match[i];

     }else{

       Trace(c) << "(unassigned) ";

@@ -794,8 +802,8 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
         for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){

           Debug("qcf-match") << "       Clean up bound var " << it->second << std::endl;

           Assert( it->second<qi->getNumVars() );

-          qi->d_match.erase( it->second );

-          qi->d_match_term.erase( it->second );

+          qi->d_match[ it->second ] = TNode::null();

+          qi->d_match_term[ it->second ] = TNode::null();

         }

         d_qni_bound.clear();

       }

@@ -912,10 +920,9 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
             int repVar = qi->getCurrentRepVar( itv->second );

             Debug("qcf-match-debug") << "       Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;

             //get the value the rep variable

-            std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );

-            if( itm!=qi->d_match.end() ){

-              val = itm->second;

-              Assert( !val.isNull() );

+            //std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );

+            if( !qi->d_match[repVar].isNull() ){

+              val = qi->d_match[repVar];

               Debug("qcf-match-debug") << "       Variable is already bound to " << val << std::endl;

             }else{

               //binding a variable

@@ -1001,7 +1008,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
         for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){

           Debug("qcf-match-debug") << "       position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;

           if( it->second<(int)qi->d_q[0].getNumChildren() && it->first>0 ){   //if it is an actual variable, we are interested in knowing the actual term

-            Assert( qi->d_match.find( it->second )!=qi->d_match.end() );

+            Assert( !qi->d_match[ it->second ].isNull() );

             Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );

             qi->d_match_term[it->second] = t[it->first-1];

           }

@@ -1147,6 +1154,8 @@ void QuantConflictFind::flatten( Node q, Node n ) {
       //Trace("qcf-qregister") << "    Flatten term " << n[i] << std::endl;

       d_qinfo[q].d_var_num[n] = d_qinfo[q].d_vars.size();

       d_qinfo[q].d_vars.push_back( n );

+      d_qinfo[q].d_match.push_back( TNode::null() );

+      d_qinfo[q].d_match_term.push_back( TNode::null() );

     }

     for( unsigned i=0; i<n.getNumChildren(); i++ ){

       flatten( q, n[i] );

@@ -1157,7 +1166,7 @@ void QuantConflictFind::flatten( Node q, Node n ) {
 void QuantConflictFind::registerQuantifier( Node q ) {

   d_quants.push_back( q );

   d_quant_id[q] = d_quants.size();

-  d_qinfo[q].d_q = q;

+  d_qinfo[q].initialize( q );

   Trace("qcf-qregister") << "Register ";

   debugPrintQuant( "qcf-qregister", q );

   Trace("qcf-qregister") << " : " << q << std::endl;

@@ -1524,31 +1533,29 @@ void QuantConflictFind::check( Theory::Effort level ) {
               if( !qi->isMatchSpurious( this ) ){

                 std::vector< int > assigned;

                 if( qi->completeMatch( this, assigned ) ){

-                  InstMatch m;

+                  std::vector< Node > terms;

                   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){

                     //Node cv = qi->getCurrentValue( qi->d_match[i] );

                     int repVar = qi->getCurrentRepVar( i );

                     Node cv;

-                    std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );

-                    if( itmt!=qi->d_match_term.end() ){

-                      cv = itmt->second;

+                    //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );

+                    if( !qi->d_match_term[repVar].isNull() ){

+                      cv = qi->d_match_term[repVar];

                     }else{

                       cv = qi->d_match[repVar];

                     }

-

-

                     Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;

-                    m.set( d_quantEngine, q, i, cv );

+                    terms.push_back( cv );

                   }

                   if( Debug.isOn("qcf-check-inst") ){

                     //if( e==effort_conflict ){

-                    Node inst = d_quantEngine->getInstantiation( q, m );

+                    Node inst = d_quantEngine->getInstantiation( q, terms );

                     Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;

                     Assert( evaluate( inst )!=1 );

                     Assert( evaluate( inst )==-1 || e>effort_conflict );

                     //}

                   }

-                  if( d_quantEngine->addInstantiation( q, m ) ){

+                  if( d_quantEngine->addInstantiation( q, terms ) ){

                     Trace("qcf-check") << "   ... Added instantiation" << std::endl;

                     ++addedLemmas;

                     if( e==effort_conflict ){

@@ -1564,7 +1571,7 @@ void QuantConflictFind::check( Theory::Effort level ) {
                   }

                   //clean up assigned

                   for( unsigned i=0; i<assigned.size(); i++ ){

-                    qi->d_match.erase( assigned[i] );

+                    qi->d_match[ assigned[i] ] = TNode::null();

                   }

                 }else{

                   Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 5ba7684ef..29ddceb40 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -110,9 +110,11 @@ public:
   std::map< int, MatchGen * > d_var_mg;

   void reset_round( QuantConflictFind * p );

 public:

+  //initialize

+  void initialize( Node q );

   //current constraints

-  std::map< int, TNode > d_match;

-  std::map< int, TNode > d_match_term;

+  std::vector< TNode > d_match;

+  std::vector< TNode > d_match_term;

   std::map< int, std::map< TNode, int > > d_curr_var_deq;

   int getCurrentRepVar( int v );

   TNode getCurrentValue( TNode n );

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 111aa9ac5..6f3879d39 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -467,8 +467,8 @@ bool QuantifiersEngine::addLemma( Node lem ){
   }
 }
 
-bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){
-  Trace("inst-add-debug") << "Add instantiation: " << m << std::endl;
+bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){
+  std::vector< Node > terms;
   //make sure there are values for each variable we are instantiating
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
     Node ic = d_term_db->getInstantiationConstant( f, i );
@@ -476,21 +476,32 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool
     if( val.isNull() ){
       val = d_term_db->getFreeVariableForInstConstant( ic );
       Trace("inst-add-debug") << "mkComplete " << val << std::endl;
-      m.set( ic, val );
     }
+    terms.push_back( val );
+  }
+  return addInstantiation( f, terms, mkRep, modEq, modInst );
+}
+
+bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) {
+  Assert( terms.size()==f[0].getNumChildren() );
+  Trace("inst-add-debug") << "Add instantiation: ";
+  for( unsigned i=0; i<terms.size(); i++ ){
+    if( i>0 ) Trace("inst-add-debug") << ", ";
+    Trace("inst-add-debug") << f[0][i] << " -> " << terms[i];
     //make it representative, this is helpful for recognizing duplication
     if( mkRep ){
       //pick the best possible representative for instantiation, based on past use and simplicity of term
-      Node r = d_eq_query->getInternalRepresentative( val, f, i );
-      Trace("inst-add-debug") << "mkRep " << r << " " << val << std::endl;
-      m.set( ic, r );
+      terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i );
+      //Trace("inst-add-debug") << " (" << terms[i] << ")";
     }
   }
-  //check for duplication modulo equality
+  Trace("inst-add-debug") << std::endl;
+
+  //check for duplication
   bool alreadyExists = false;
   ///*
-  Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
   if( options::incrementalSolving() ){
+    Trace("inst-add-debug") << "Adding into context-dependent inst trie" << std::endl;
     inst::CDInstMatchTrie* imt;
     std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( f );
     if( it!=d_c_inst_match_trie.end() ){
@@ -499,30 +510,21 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool
       imt = new CDInstMatchTrie( getUserContext() );
       d_c_inst_match_trie[f] = imt;
     }
-    alreadyExists = !imt->addInstMatch( this, f, m, getUserContext(), modEq, modInst );
+    alreadyExists = !imt->addInstMatch( this, f, terms, getUserContext(), modEq, modInst );
   }else{
-    alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst );
+    Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+    alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, terms, modEq, modInst );
   }
-  //*/
   if( alreadyExists ){
-      Trace("inst-add-debug") << " -> Already exists." << std::endl;
-      ++(d_statistics.d_inst_duplicate_eq);
-      return false;
-  }
-  Trace("inst-add-debug") << "compute terms" << std::endl;
-  //compute the vector of terms for the instantiation
-  std::vector< Node > terms;
-  for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){
-    Node n = m.getValue( d_term_db->d_inst_constants[f][i] );
-    Assert( !n.isNull() );
-    terms.push_back( n );
+    Trace("inst-add-debug") << " -> Already exists." << std::endl;
+    ++(d_statistics.d_inst_duplicate_eq);
+    return false;
   }
+
   //add the instantiation
   bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms );
   //report the result
   if( addedInst ){
-    Trace("inst-add") << "Added instantiation for " << f << ": " << std::endl;
-    Trace("inst-add") << "   " << m << std::endl;
     Trace("inst-add-debug") << " -> Success." << std::endl;
     return true;
   }else{
@@ -531,6 +533,7 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool
   }
 }
 
+
 bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
   n = Rewriter::rewrite( n );
   Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 9d341194f..fd51e4fb1 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -212,7 +212,9 @@ public:
   /** add lemma lem */
   bool addLemma( Node lem );
   /** do instantiation specified by m */
-  bool addInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false, bool mkRep = true );
+  bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false );
+  /** add instantiation */
+  bool addInstantiation( Node f, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false );
   /** split on node n */
   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
   /** add split equality */