23 files changed, 1311 insertions, 1243 deletions

diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 57b99c59b..ed60e77a9 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -40,7 +40,9 @@ libquantifiers_la_SOURCES = \
 	inst_gen.h \
 	inst_gen.cpp \
 	quant_util.h \
-	quant_util.cpp
+	quant_util.cpp \
+	inst_match_generator.h \
+	inst_match_generator.cpp
 
 EXTRA_DIST = \
 	kinds \
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index c8fcb7c44..3779579fd 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -24,13 +24,6 @@
 namespace CVC4 {
 namespace theory {
 
-struct ModelBasisAttributeId {};
-typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
-//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
-//                    0 : term has no direct child with model basis attribute.
-struct ModelBasisArgAttributeId {};
-typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
-
 class QuantifiersEngine;
 
 namespace quantifiers{
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index d00885abf..36f265c30 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -13,16 +13,9 @@
  **/
 
 #include "theory/quantifiers/inst_match.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/candidate_generator.h"
-#include "theory/uf/theory_uf_instantiator.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4;
@@ -216,672 +209,6 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, b
   }
 }
 
-InstMatchGenerator::InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){
-  initializePattern( pat, qe );
-}
-
-InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){
-  if( pats.size()==1 ){
-    initializePattern( pats[0], qe );
-  }else{
-    initializePatterns( pats, qe );
-  }
-}
-
-void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){
-  int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy;
-  for( int i=0; i<(int)pats.size(); i++ ){
-    d_children.push_back( new InstMatchGenerator( pats[i], qe, childMatchPolicy ) );
-  }
-  d_pattern = Node::null();
-  d_match_pattern = Node::null();
-  d_cg = NULL;
-}
-
-void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
-  Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;
-  Assert( pat.hasAttribute(InstConstantAttribute()) );
-  d_pattern = pat;
-  d_match_pattern = pat;
-  if( d_match_pattern.getKind()==NOT ){
-    //we want to add the children of the NOT
-    d_match_pattern = d_pattern[0];
-  }
-  if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){
-    if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){
-      Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );
-      //swap sides
-      d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );
-      d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern;
-      if( pat.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching
-        d_match_pattern = d_match_pattern[1];
-      }else{
-        d_match_pattern = d_pattern[0][0];
-      }
-    }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){
-      Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );
-      if( pat.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching
-        d_match_pattern = d_match_pattern[0];
-      }
-    }
-  }
-  int childMatchPolicy = MATCH_GEN_DEFAULT;
-  for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
-    if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
-      if( d_match_pattern[i].getKind()!=INST_CONSTANT ){
-        d_children.push_back( new InstMatchGenerator( d_match_pattern[i], qe, childMatchPolicy ) );
-        d_children_index.push_back( i );
-      }
-    }
-  }
-
-  Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
-
-  //create candidate generator
-  if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
-    Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
-    //we will be producing candidates via literal matching heuristics
-    if( d_pattern.getKind()!=NOT ){
-      //candidates will be all equalities
-      d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern );
-    }else{
-      //candidates will be all disequalities
-      d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
-    }
-  }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){
-    Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
-    if( d_pattern.getKind()==NOT ){
-      Unimplemented("Disequal generator unimplemented");
-    }else{
-      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() );
-      //store the equivalence class that we will call d_cg->reset( ... ) on
-      d_eq_class = d_pattern[1];
-    }
-  }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
-    //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){
-      //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;
-    //}
-    //we will be scanning lists trying to find d_match_pattern.getOperator()
-    d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
-  }else{
-    d_cg = new CandidateGeneratorQueue;
-    if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
-      Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
-      Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
-      d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
-    }else{
-      Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl;
-      for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
-        Debug("matching-arith") << "   " << it->first << " -> " << it->second << std::endl;
-      }
-      //we will treat this as match gen internal arithmetic
-      d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC;
-    }
-  }
-}
-
-/** get match (not modulo equality) */
-bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){
-  Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
-                    << m.size() << ")" << ", " << d_children.size() << std::endl;
-  Assert( !d_match_pattern.isNull() );
-  if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){
-    return true;
-  }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){
-    return getMatchArithmetic( t, m, qe );
-  }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){
-    return false;
-  }else{
-    EqualityQuery* q = qe->getEqualityQuery();
-    //add m to partial match vector
-    std::vector< InstMatch > partial;
-    partial.push_back( InstMatch( &m ) );
-    //if t is null
-    Assert( !t.isNull() );
-    Assert( !t.hasAttribute(InstConstantAttribute()) );
-    Assert( t.getKind()==d_match_pattern.getKind() );
-    Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
-    //first, check if ground arguments are not equal, or a match is in conflict
-    for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
-      if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
-        if( d_match_pattern[i].getKind()==INST_CONSTANT ){
-          if( !partial[0].setMatch( q, d_match_pattern[i], t[i] ) ){
-            //match is in conflict
-            Debug("matching-debug") << "Match in conflict " << t[i] << " and "
-                                    << d_match_pattern[i] << " because "
-                                    << partial[0].get(d_match_pattern[i])
-                                    << std::endl;
-            Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl;
-            return false;
-          }
-        }
-      }else{
-        if( !q->areEqual( d_match_pattern[i], t[i] ) ){
-          Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;
-          //ground arguments are not equal
-          return false;
-        }
-      }
-    }
-    //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]->d_cg->reset( rep );
-    }
-
-    //combine child matches
-    int index = 0;
-    while( index>=0 && index<(int)d_children.size() ){
-      partial.push_back( InstMatch( &partial[index] ) );
-      if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){
-        index++;
-      }else{
-        d_children[index]->d_cg->reset( reps[index] );
-        partial.pop_back();
-        if( !partial.empty() ){
-          partial.pop_back();
-        }
-        index--;
-      }
-    }
-    if( index>=0 ){
-      m = partial.back();
-      return true;
-    }else{
-      return false;
-    }
-  }
-}
-
-bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){
-  bool success = false;
-  Node t;
-  do{
-    //get the next candidate term t
-    t = d_cg->getNextCandidate();
-    //if t not null, try to fit it into match m
-    if( !t.isNull() && t.getType()==d_match_pattern.getType() ){
-      success = getMatch( t, m, qe );
-    }
-  }while( !success && !t.isNull() );
-  if (saveMatched) m.d_matched = t;
-  return success;
-}
-
-bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){
-  Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl;
-  if( !d_arith_coeffs.empty() ){
-    NodeBuilder<> tb(kind::PLUS);
-    Node ic = Node::null();
-    for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
-      Debug("matching-arith") << it->first << " -> " << it->second << std::endl;
-      if( !it->first.isNull() ){
-        if( m.find( it->first )==m.end() ){
-          //see if we can choose this to set
-          if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){
-            ic = it->first;
-          }
-        }else{
-          Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl;
-          Node tm = m.get( it->first );
-          if( !it->second.isNull() ){
-            tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm );
-          }
-          tb << tm;
-        }
-      }else{
-        tb << it->second;
-      }
-    }
-    if( !ic.isNull() ){
-      Node tm;
-      if( tb.getNumChildren()==0 ){
-        tm = t;
-      }else{
-        tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
-        tm = NodeManager::currentNM()->mkNode( MINUS, t, tm );
-      }
-      if( !d_arith_coeffs[ ic ].isNull() ){
-        Assert( !ic.getType().isInteger() );
-        Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() );
-        tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm );
-      }
-      m.set( ic, Rewriter::rewrite( tm ));
-      //set the rest to zeros
-      for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
-        if( !it->first.isNull() ){
-          if( m.find( it->first )==m.end() ){
-            m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) );
-          }
-        }
-      }
-      Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl;
-      return true;
-    }else{
-      return false;
-    }
-  }else{
-    return false;
-  }
-}
-
-
-/** reset instantiation round */
-void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
-  if( d_match_pattern.isNull() ){
-    for( int i=0; i<(int)d_children.size(); i++ ){
-      d_children[i]->resetInstantiationRound( qe );
-    }
-  }else{
-    if( d_cg ){
-      d_cg->resetInstantiationRound();
-    }
-  }
-}
-
-void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
-  if( d_match_pattern.isNull() ){
-    for( int i=0; i<(int)d_children.size(); i++ ){
-      d_children[i]->reset( eqc, qe );
-    }
-    d_partial.clear();
-  }else{
-    if( !d_eq_class.isNull() ){
-      //we have a specific equivalence class in mind
-      //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
-      //just look in equivalence class of the RHS
-      d_cg->reset( d_eq_class );
-    }else{
-      d_cg->reset( eqc );
-    }
-  }
-}
-
-bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-  m.d_matched = Node::null();
-  if( d_match_pattern.isNull() ){
-    int index = (int)d_partial.size();
-    while( index>=0 && index<(int)d_children.size() ){
-      if( index>0 ){
-        d_partial.push_back( InstMatch( &d_partial[index-1] ) );
-      }else{
-        d_partial.push_back( InstMatch() );
-      }
-      if( d_children[index]->getNextMatch( d_partial[index], qe ) ){
-        index++;
-      }else{
-        d_children[index]->reset( Node::null(), qe );
-        d_partial.pop_back();
-        if( !d_partial.empty() ){
-          d_partial.pop_back();
-        }
-        index--;
-      }
-    }
-    if( index>=0 ){
-      m = d_partial.back();
-      d_partial.pop_back();
-      return true;
-    }else{
-      return false;
-    }
-  }else{
-    bool res = getNextMatch2( m, qe, true );
-    Assert(!res || !m.d_matched.isNull());
-    return res;
-  }
-}
-
-
-
-// Currently the implementation doesn't take into account that
-// variable should have the same value given.
-// TODO use the d_children way perhaps
-// TODO replace by a real dictionnary
-// We should create a real substitution? slower more precise
-// We don't do that often
-bool InstMatchGenerator::nonunifiable( TNode t0, const std::vector<Node> & vars){
-  if(d_match_pattern.isNull()) return true;
-
-  typedef std::vector<std::pair<TNode,TNode> > tstack;
-  tstack stack(1,std::make_pair(t0,d_match_pattern)); // t * pat
-
-  while(!stack.empty()){
-    const std::pair<TNode,TNode> p = stack.back(); stack.pop_back();
-    const TNode & t = p.first;
-    const TNode & pat = p.second;
-
-    // t or pat is a variable currently we consider that can match anything
-    if( find(vars.begin(),vars.end(),t) != vars.end() ) continue;
-    if( pat.getKind() == INST_CONSTANT ) continue;
-
-    // t and pat are nonunifiable
-    if( !Trigger::isAtomicTrigger( t ) || !Trigger::isAtomicTrigger( pat ) ) {
-      if(t == pat) continue;
-      else return true;
-    };
-    if( t.getOperator() != pat.getOperator() ) return true;
-
-    //put the children on the stack
-    for( size_t i=0; i < pat.getNumChildren(); i++ ){
-      stack.push_back(std::make_pair(t[i],pat[i]));
-    };
-  }
-  // The heuristic can't find non-unifiability
-  return false;
-}
-
-int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
-  //now, try to add instantiation for each match produced
-  int addedLemmas = 0;
-  InstMatch m;
-  while( getNextMatch( m, qe ) ){
-    //m.makeInternal( d_quantEngine->getEqualityQuery() );
-    m.add( baseMatch );
-    if( qe->addInstantiation( f, m ) ){
-      addedLemmas++;
-      if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){
-        return addedLemmas;
-      }
-    }
-    m.clear();
-  }
-  //return number of lemmas added
-  return addedLemmas;
-}
-
-int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
-  Assert( options::eagerInstQuant() );
-  if( !d_match_pattern.isNull() ){
-    InstMatch m;
-    if( getMatch( t, m, qe ) ){
-      if( qe->addInstantiation( f, m ) ){
-        return 1;
-      }
-    }
-  }else{
-    for( int i=0; i<(int)d_children.size(); i++ ){
-      d_children[i]->addTerm( f, t, qe );
-    }
-  }
-  return 0;
-}
-
-/** constructors */
-InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) :
-d_f( f ){
-  Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;
-  std::map< Node, std::vector< Node > > var_contains;
-  qe->getTermDatabase()->getVarContains( f, pats, var_contains );
-  //convert to indicies
-  for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
-    Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";
-    for( int i=0; i<(int)it->second.size(); i++ ){
-      Debug("smart-multi-trigger") << it->second[i] << " ";
-      int index = it->second[i].getAttribute(InstVarNumAttribute());
-      d_var_contains[ it->first ].push_back( index );
-      d_var_to_node[ index ].push_back( it->first );
-    }
-    Debug("smart-multi-trigger") << std::endl;
-  }
-  for( int i=0; i<(int)pats.size(); i++ ){
-    Node n = pats[i];
-    //make the match generator
-    d_children.push_back( new InstMatchGenerator( n, qe, matchOption ) );
-    //compute unique/shared variables
-    std::vector< int > unique_vars;
-    std::map< int, bool > shared_vars;
-    int numSharedVars = 0;
-    for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
-      if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
-        Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
-        unique_vars.push_back( d_var_contains[n][j] );
-      }else{
-        shared_vars[ d_var_contains[n][j] ] = true;
-        numSharedVars++;
-      }
-    }
-    //we use the latest shared variables, then unique variables
-    std::vector< int > vars;
-    int index = i==0 ? (int)(pats.size()-1) : (i-1);
-    while( numSharedVars>0 && index!=i ){
-      for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
-        if( it->second ){
-          if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=
-              d_var_contains[ pats[index] ].end() ){
-            vars.push_back( it->first );
-            shared_vars[ it->first ] = false;
-            numSharedVars--;
-          }
-        }
-      }
-      index = index==0 ? (int)(pats.size()-1) : (index-1);
-    }
-    vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
-    Debug("smart-multi-trigger") << "   Index[" << i << "]: ";
-    for( int i=0; i<(int)vars.size(); i++ ){
-      Debug("smart-multi-trigger") << vars[i] << " ";
-    }
-    Debug("smart-multi-trigger") << std::endl;
-    //make ordered inst match trie
-    InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder;
-    imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() );
-    d_children_trie.push_back( InstMatchTrieOrdered( imtio ) );
-  }
-
-}
-
-/** reset instantiation round (call this whenever equivalence classes have changed) */
-void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){
-  for( int i=0; i<(int)d_children.size(); i++ ){
-    d_children[i]->resetInstantiationRound( qe );
-  }
-}
-
-/** reset, eqc is the equivalence class to search in (any if eqc=null) */
-void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
-  for( int i=0; i<(int)d_children.size(); i++ ){
-    d_children[i]->reset( eqc, qe );
-  }
-}
-
-int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
-  int addedLemmas = 0;
-  Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
-  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;
-    while( d_children[i]->getNextMatch( m, qe ) ){
-      m.makeRepresentative( qe );
-      newMatches.push_back( InstMatch( &m ) );
-      m.clear();
-    }
-    for( int j=0; j<(int)newMatches.size(); j++ ){
-      processNewMatch( qe, newMatches[j], i, addedLemmas );
-    }
-  }
-  return addedLemmas;
-}
-
-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 );
-  //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.
-  Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl;
-  //process new instantiations
-  int childIndex = (fromChildIndex+1)%(int)d_children.size();
-  std::vector< IndexedTrie > unique_var_tries;
-  processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(),
-                            unique_var_tries, 0, childIndex, fromChildIndex, true );
-}
-
-void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
-                                                        std::vector< IndexedTrie >& unique_var_tries,
-                                                        int trieIndex, int childIndex, int endChildIndex, bool modEq ){
-  if( childIndex==endChildIndex ){
-    //now, process unique variables
-    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() ){
-      //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 ) );
-      //  int newChildIndex = (childIndex+1)%(int)d_children.size();
-      //  processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
-      //                            0, newChildIndex, endChildIndex, modEq );
-      //}else{
-        //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);
-          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,
-                                  trieIndex+1, childIndex, endChildIndex, modEq );
-      }
-      if( modEq ){
-        //check modulo equality for other possible instantiations
-        if( 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 = tr->d_data.find( en );
-              if( itc!=tr->d_data.end() ){
-                processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,
-                                          trieIndex+1, childIndex, endChildIndex, modEq );
-              }
-            }
-            ++eqc;
-          }
-        }
-      }
-    }
-  }else{
-    int newChildIndex = (childIndex+1)%(int)d_children.size();
-    processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
-                              0, newChildIndex, endChildIndex, modEq );
-  }
-}
-
-void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
-                                                         std::vector< IndexedTrie >& unique_var_tries,
-                                                         int uvtIndex, InstMatchTrie* tr, int trieIndex ){
-  if( uvtIndex<(int)unique_var_tries.size() ){
-    int childIndex = unique_var_tries[uvtIndex].first.first;
-    if( !tr ){
-      tr = unique_var_tries[uvtIndex].second;
-      trieIndex = unique_var_tries[uvtIndex].first.second;
-    }
-    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 );
-      //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);
-        processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );
-      }
-    }else{
-      processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );
-    }
-  }else{
-    //m is an instantiation
-    if( qe->addInstantiation( d_f, m ) ){
-      addedLemmas++;
-      Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;
-    }
-  }
-}
-
-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;
-      //if it produces a match, then process it with the rest
-      if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){
-        processNewMatch( qe, m, i, addedLemmas );
-      }
-    }
-  }
-  return addedLemmas;
-}
-
-int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
-  InstMatch m;
-  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() ]) );
-    }
-  }else{
-    addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) );
-  }
-  return addedLemmas;
-}
-
-void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
-  if( argIndex==(int)d_match_pattern.getNumChildren() ){
-    //m is an instantiation
-    if( qe->addInstantiation( d_f, m ) ){
-      addedLemmas++;
-      Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl;
-    }
-  }else{
-    if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
-      Node ic = d_match_pattern[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 ){
-          Node prev = m.get( ic );
-          m.set( ic, t);
-          addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
-          m.set( ic, prev);
-        }
-      }
-    }else{
-      Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
-      std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
-      if( it!=tat->d_data.end() ){
-        addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
-      }
-    }
-  }
-}
-
-int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
-  Assert( options::eagerInstQuant() );
-  InstMatch m;
-  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]);
-    }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){
-      return 0;
-    }
-  }
-  return qe->addInstantiation( f, m ) ? 1 : 0;
-}
 
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index a0db1336f..426adc02d 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -20,81 +20,19 @@
 #include "util/hash.h"
 
 #include <ext/hash_set>
-#include <iostream>
 #include <map>
 
 #include "context/cdlist.h"
-#include "theory/quantifiers/candidate_generator.h"
-
-//#define USE_EFFICIENT_E_MATCHING
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace theory {
 
-/** Attribute true for nodes that should not be used for matching */
-struct NoMatchAttributeId {};
-/** use the special for boolean flag */
-typedef expr::Attribute< NoMatchAttributeId,
-                         bool,
-                         expr::attr::NullCleanupStrategy,
-                         true // context dependent
-                       > NoMatchAttribute;
-
-// attribute for "contains instantiation constants from"
-struct InstConstantAttributeId {};
-typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
-
-struct InstLevelAttributeId {};
-typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
-
-struct InstVarNumAttributeId {};
-typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
-
-// Attribute that tell if a node have been asserted in this branch
-struct AvailableInTermDbId {};
-/** use the special for boolean flag */
-typedef expr::Attribute<AvailableInTermDbId,
-                        bool,
-                        expr::attr::NullCleanupStrategy,
-                        true  // context dependent
-                        > AvailableInTermDb;
-
-
 class QuantifiersEngine;
-namespace quantifiers{
-  class TermArgTrie;
-}
-
-namespace uf{
-  class InstantiatorTheoryUf;
-  class TheoryUF;
-}/* CVC4::theory::uf namespace */
+class EqualityQuery;
 
 namespace inst {
 
-class EqualityQuery {
-public:
-  EqualityQuery(){}
-  virtual ~EqualityQuery(){};
-  /** contains term */
-  virtual bool hasTerm( Node a ) = 0;
-  /** get the representative of the equivalence class of a */
-  virtual Node getRepresentative( Node a ) = 0;
-  /** returns true if a and b are equal in the current context */
-  virtual bool areEqual( Node a, Node b ) = 0;
-  /** returns true is a and b are disequal in the current context */
-  virtual bool areDisequal( Node a, Node b ) = 0;
-  /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
-      If cbqi is active, this will return a term in the equivalence class of "a" that does
-      not contain instantiation constants, if such a term exists.
-   */
-  virtual Node getInternalRepresentative( Node a ) = 0;
-  /** get the equality engine associated with this query */
-  virtual eq::EqualityEngine* getEngine() = 0;
-  /** get the equivalence class of a */
-  virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
-};/* class EqualityQuery */
-
 /** basic class defining an instantiation */
 class InstMatch {
   /* map from variable to ground terms */
@@ -230,176 +168,9 @@ public:
   }
 };/* class InstMatchTrieOrdered */
 
-/** base class for producing InstMatch objects */
-class IMGenerator {
-public:
-  /** reset instantiation round (call this at beginning of instantiation round) */
-  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
-  /** get the next match.  must call reset( eqc ) before this function. */
-  virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
-  /** return true if whatever Node is substituted for the variables the
-      given Node can't match the pattern */
-  virtual bool nonunifiable( TNode t, const std::vector<Node> & vars) = 0;
-  /** add instantiations directly */
-  virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
-  /** add ground term t, called when t is added to term db */
-  virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;
-};/* class IMGenerator */
-
-
-class InstMatchGenerator : public IMGenerator {
-private:
-  /** candidate generator */
-  CandidateGenerator* d_cg;
-  /** policy to use for matching */
-  int d_matchPolicy;
-  /** children generators */
-  std::vector< InstMatchGenerator* > d_children;
-  std::vector< int > d_children_index;
-  /** partial vector */
-  std::vector< InstMatch > d_partial;
-  /** eq class */
-  Node d_eq_class;
-  /** for arithmetic matching */
-  std::map< Node, Node > d_arith_coeffs;
-  /** initialize pattern */
-  void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe );
-  void initializePattern( Node pat, QuantifiersEngine* qe );
-public:
-  enum {
-    //options for producing matches
-    MATCH_GEN_DEFAULT = 0,
-    MATCH_GEN_EFFICIENT_E_MATCH,   //generate matches via Efficient E-matching for SMT solvers
-    //others (internally used)
-    MATCH_GEN_INTERNAL_ARITHMETIC,
-    MATCH_GEN_INTERNAL_ERROR,
-  };
-private:
-  /** get the next match.  must call d_cg->reset( ... ) before using.
-      only valid for use where !d_match_pattern.isNull().
-  */
-  bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );
-  /** for arithmetic */
-  bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );
-public:
-  /** get the match against ground term or formula t.
-      d_match_pattern and t should have the same shape.
-      only valid for use where !d_match_pattern.isNull().
-  */
-  bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );
-
-  /** constructors */
-  InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 );
-  InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
-  /** destructor */
-  ~InstMatchGenerator(){}
-  /** The pattern we are producing matches for.
-      If null, this is a multi trigger that is merging matches from d_children.
-  */
-  Node d_pattern;
-  /** match pattern */
-  Node d_match_pattern;
-public:
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  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. */
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );
-  /** return true if whatever Node is substituted for the variables the
-      given Node can't match the pattern */
-  bool nonunifiable( TNode t, const std::vector<Node> & vars);
-  /** add instantiations */
-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t */
-  int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGenerator */
-
-/** smart multi-trigger implementation */
-class InstMatchGeneratorMulti : public IMGenerator {
-private:
-  /** indexed trie */
-  typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
-  /** process new match */
-  void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );
-  /** process new instantiations */
-  void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
-                                 std::vector< IndexedTrie >& unique_var_tries,
-                                 int trieIndex, int childIndex, int endChildIndex, bool modEq );
-  /** process new instantiations 2 */
-  void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
-                                  std::vector< IndexedTrie >& unique_var_tries,
-                                  int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
-private:
-  /** var contains (variable indices) for each pattern node */
-  std::map< Node, std::vector< int > > d_var_contains;
-  /** variable indices contained to pattern nodes */
-  std::map< int, std::vector< Node > > d_var_to_node;
-  /** quantifier to use */
-  Node d_f;
-  /** policy to use for matching */
-  int d_matchPolicy;
-  /** children generators */
-  std::vector< InstMatchGenerator* > d_children;
-  /** inst match tries for each child */
-  std::vector< InstMatchTrieOrdered > d_children_trie;
-  /** calculate matches */
-  void calculateMatches( QuantifiersEngine* qe );
-public:
-  /** constructors */
-  InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
-  /** destructor */
-  ~InstMatchGeneratorMulti(){}
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  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) */
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
-  /** return true if whatever Node is substituted for the variables the
-      given Node can't match the pattern */
-  bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
-  /** add instantiations */
-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t */
-  int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGeneratorMulti */
-
-/** smart (single)-trigger implementation */
-class InstMatchGeneratorSimple : public IMGenerator {
-private:
-  /** quantifier for match term */
-  Node d_f;
-  /** match term */
-  Node d_match_pattern;
-  /** 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 ){}
-  /** destructor */
-  ~InstMatchGeneratorSimple(){}
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  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) */
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
-  /** return true if whatever Node is substituted for the variables the
-      given Node can't match the pattern */
-  bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
-  /** add instantiations */
-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t, possibly add instantiations */
-  int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGeneratorSimple */
-
 }/* CVC4::theory::inst namespace */
 
 typedef CVC4::theory::inst::InstMatch InstMatch;
-typedef CVC4::theory::inst::EqualityQuery EqualityQuery;
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
new file mode 100755
index 000000000..acd733e22
--- /dev/null
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -0,0 +1,664 @@
+/*********************                                                        */

+/*! \file inst_match_generator.cpp

+** \verbatim

+** Original author: ajreynol

+** Major contributors: bobot

+** Minor contributors (to current version): barrett, mdeters

+** This file is part of the CVC4 prototype.

+** Copyright (c) 2009-2012  New York University and The University of Iowa

+** See the file COPYING in the top-level source directory for licensing

+** information.\endverbatim

+**

+** \brief Implementation of inst match generator class

+**/

+

+#include "theory/quantifiers/inst_match_generator.h"

+#include "theory/quantifiers/trigger.h"

+#include "theory/quantifiers/term_database.h"

+#include "theory/quantifiers/candidate_generator.h"

+#include "theory/quantifiers_engine.h"

+

+using namespace std;

+using namespace CVC4;

+using namespace CVC4::kind;

+using namespace CVC4::context;

+using namespace CVC4::theory;

+

+namespace CVC4 {

+namespace theory {

+namespace inst {

+

+

+InstMatchGenerator::InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){

+  initializePattern( pat, qe );

+}

+

+InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){

+  if( pats.size()==1 ){

+    initializePattern( pats[0], qe );

+  }else{

+    initializePatterns( pats, qe );

+  }

+}

+

+void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){

+  int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy;

+  for( int i=0; i<(int)pats.size(); i++ ){

+    d_children.push_back( new InstMatchGenerator( pats[i], qe, childMatchPolicy ) );

+  }

+  d_pattern = Node::null();

+  d_match_pattern = Node::null();

+  d_cg = NULL;

+}

+

+void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){

+  Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;

+  Assert( pat.hasAttribute(InstConstantAttribute()) );

+  d_pattern = pat;

+  d_match_pattern = pat;

+  if( d_match_pattern.getKind()==NOT ){

+    //we want to add the children of the NOT

+    d_match_pattern = d_pattern[0];

+  }

+  if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){

+    if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){

+      Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );

+      //swap sides

+      d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );

+      d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern;

+      if( pat.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching

+        d_match_pattern = d_match_pattern[1];

+      }else{

+        d_match_pattern = d_pattern[0][0];

+      }

+    }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){

+      Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );

+      if( pat.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching

+        d_match_pattern = d_match_pattern[0];

+      }

+    }

+  }

+  int childMatchPolicy = MATCH_GEN_DEFAULT;

+  for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){

+    if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){

+      if( d_match_pattern[i].getKind()!=INST_CONSTANT ){

+        d_children.push_back( new InstMatchGenerator( d_match_pattern[i], qe, childMatchPolicy ) );

+        d_children_index.push_back( i );

+      }

+    }

+  }

+

+  Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;

+

+  //create candidate generator

+  if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){

+    Assert( d_matchPolicy==MATCH_GEN_DEFAULT );

+    //we will be producing candidates via literal matching heuristics

+    if( d_pattern.getKind()!=NOT ){

+      //candidates will be all equalities

+      d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern );

+    }else{

+      //candidates will be all disequalities

+      d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );

+    }

+  }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){

+    Assert( d_matchPolicy==MATCH_GEN_DEFAULT );

+    if( d_pattern.getKind()==NOT ){

+      Unimplemented("Disequal generator unimplemented");

+    }else{

+      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() );

+      //store the equivalence class that we will call d_cg->reset( ... ) on

+      d_eq_class = d_pattern[1];

+    }

+  }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){

+    //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){

+      //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;

+    //}

+    //we will be scanning lists trying to find d_match_pattern.getOperator()

+    d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );

+  }else{

+    d_cg = new CandidateGeneratorQueue;

+    if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){

+      Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;

+      Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;

+      d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;

+    }else{

+      Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl;

+      for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){

+        Debug("matching-arith") << "   " << it->first << " -> " << it->second << std::endl;

+      }

+      //we will treat this as match gen internal arithmetic

+      d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC;

+    }

+  }

+}

+

+/** get match (not modulo equality) */

+bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){

+  Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("

+                    << m.size() << ")" << ", " << d_children.size() << std::endl;

+  Assert( !d_match_pattern.isNull() );

+  if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){

+    return true;

+  }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){

+    return getMatchArithmetic( t, m, qe );

+  }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){

+    return false;

+  }else{

+    EqualityQuery* q = qe->getEqualityQuery();

+    //add m to partial match vector

+    std::vector< InstMatch > partial;

+    partial.push_back( InstMatch( &m ) );

+    //if t is null

+    Assert( !t.isNull() );

+    Assert( !t.hasAttribute(InstConstantAttribute()) );

+    Assert( t.getKind()==d_match_pattern.getKind() );

+    Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );

+    //first, check if ground arguments are not equal, or a match is in conflict

+    for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){

+      if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){

+        if( d_match_pattern[i].getKind()==INST_CONSTANT ){

+          if( !partial[0].setMatch( q, d_match_pattern[i], t[i] ) ){

+            //match is in conflict

+            Debug("matching-debug") << "Match in conflict " << t[i] << " and "

+                                    << d_match_pattern[i] << " because "

+                                    << partial[0].get(d_match_pattern[i])

+                                    << std::endl;

+            Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl;

+            return false;

+          }

+        }

+      }else{

+        if( !q->areEqual( d_match_pattern[i], t[i] ) ){

+          Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;

+          //ground arguments are not equal

+          return false;

+        }

+      }

+    }

+    //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]->d_cg->reset( rep );

+    }

+

+    //combine child matches

+    int index = 0;

+    while( index>=0 && index<(int)d_children.size() ){

+      partial.push_back( InstMatch( &partial[index] ) );

+      if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){

+        index++;

+      }else{

+        d_children[index]->d_cg->reset( reps[index] );

+        partial.pop_back();

+        if( !partial.empty() ){

+          partial.pop_back();

+        }

+        index--;

+      }

+    }

+    if( index>=0 ){

+      m = partial.back();

+      return true;

+    }else{

+      return false;

+    }

+  }

+}

+

+bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){

+  bool success = false;

+  Node t;

+  do{

+    //get the next candidate term t

+    t = d_cg->getNextCandidate();

+    //if t not null, try to fit it into match m

+    if( !t.isNull() && t.getType()==d_match_pattern.getType() ){

+      success = getMatch( t, m, qe );

+    }

+  }while( !success && !t.isNull() );

+  if (saveMatched) m.d_matched = t;

+  return success;

+}

+

+bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){

+  Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl;

+  if( !d_arith_coeffs.empty() ){

+    NodeBuilder<> tb(kind::PLUS);

+    Node ic = Node::null();

+    for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){

+      Debug("matching-arith") << it->first << " -> " << it->second << std::endl;

+      if( !it->first.isNull() ){

+        if( m.find( it->first )==m.end() ){

+          //see if we can choose this to set

+          if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){

+            ic = it->first;

+          }

+        }else{

+          Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl;

+          Node tm = m.get( it->first );

+          if( !it->second.isNull() ){

+            tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm );

+          }

+          tb << tm;

+        }

+      }else{

+        tb << it->second;

+      }

+    }

+    if( !ic.isNull() ){

+      Node tm;

+      if( tb.getNumChildren()==0 ){

+        tm = t;

+      }else{

+        tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;

+        tm = NodeManager::currentNM()->mkNode( MINUS, t, tm );

+      }

+      if( !d_arith_coeffs[ ic ].isNull() ){

+        Assert( !ic.getType().isInteger() );

+        Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() );

+        tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm );

+      }

+      m.set( ic, Rewriter::rewrite( tm ));

+      //set the rest to zeros

+      for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){

+        if( !it->first.isNull() ){

+          if( m.find( it->first )==m.end() ){

+            m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) );

+          }

+        }

+      }

+      Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl;

+      return true;

+    }else{

+      return false;

+    }

+  }else{

+    return false;

+  }

+}

+

+

+/** reset instantiation round */

+void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){

+  if( d_match_pattern.isNull() ){

+    for( int i=0; i<(int)d_children.size(); i++ ){

+      d_children[i]->resetInstantiationRound( qe );

+    }

+  }else{

+    if( d_cg ){

+      d_cg->resetInstantiationRound();

+    }

+  }

+}

+

+void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){

+  if( d_match_pattern.isNull() ){

+    for( int i=0; i<(int)d_children.size(); i++ ){

+      d_children[i]->reset( eqc, qe );

+    }

+    d_partial.clear();

+  }else{

+    if( !d_eq_class.isNull() ){

+      //we have a specific equivalence class in mind

+      //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term

+      //just look in equivalence class of the RHS

+      d_cg->reset( d_eq_class );

+    }else{

+      d_cg->reset( eqc );

+    }

+  }

+}

+

+bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){

+  m.d_matched = Node::null();

+  if( d_match_pattern.isNull() ){

+    int index = (int)d_partial.size();

+    while( index>=0 && index<(int)d_children.size() ){

+      if( index>0 ){

+        d_partial.push_back( InstMatch( &d_partial[index-1] ) );

+      }else{

+        d_partial.push_back( InstMatch() );

+      }

+      if( d_children[index]->getNextMatch( d_partial[index], qe ) ){

+        index++;

+      }else{

+        d_children[index]->reset( Node::null(), qe );

+        d_partial.pop_back();

+        if( !d_partial.empty() ){

+          d_partial.pop_back();

+        }

+        index--;

+      }

+    }

+    if( index>=0 ){

+      m = d_partial.back();

+      d_partial.pop_back();

+      return true;

+    }else{

+      return false;

+    }

+  }else{

+    bool res = getNextMatch2( m, qe, true );

+    Assert(!res || !m.d_matched.isNull());

+    return res;

+  }

+}

+

+

+

+int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){

+  //now, try to add instantiation for each match produced

+  int addedLemmas = 0;

+  InstMatch m;

+  while( getNextMatch( m, qe ) ){

+    //m.makeInternal( d_quantEngine->getEqualityQuery() );

+    m.add( baseMatch );

+    if( qe->addInstantiation( f, m ) ){

+      addedLemmas++;

+      if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){

+        return addedLemmas;

+      }

+    }

+    m.clear();

+  }

+  //return number of lemmas added

+  return addedLemmas;

+}

+

+int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){

+  Assert( options::eagerInstQuant() );

+  if( !d_match_pattern.isNull() ){

+    InstMatch m;

+    if( getMatch( t, m, qe ) ){

+      if( qe->addInstantiation( f, m ) ){

+        return 1;

+      }

+    }

+  }else{

+    for( int i=0; i<(int)d_children.size(); i++ ){

+      d_children[i]->addTerm( f, t, qe );

+    }

+  }

+  return 0;

+}

+

+/** constructors */

+InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) :

+d_f( f ){

+  Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;

+  std::map< Node, std::vector< Node > > var_contains;

+  qe->getTermDatabase()->getVarContains( f, pats, var_contains );

+  //convert to indicies

+  for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){

+    Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";

+    for( int i=0; i<(int)it->second.size(); i++ ){

+      Debug("smart-multi-trigger") << it->second[i] << " ";

+      int index = it->second[i].getAttribute(InstVarNumAttribute());

+      d_var_contains[ it->first ].push_back( index );

+      d_var_to_node[ index ].push_back( it->first );

+    }

+    Debug("smart-multi-trigger") << std::endl;

+  }

+  for( int i=0; i<(int)pats.size(); i++ ){

+    Node n = pats[i];

+    //make the match generator

+    d_children.push_back( new InstMatchGenerator( n, qe, matchOption ) );

+    //compute unique/shared variables

+    std::vector< int > unique_vars;

+    std::map< int, bool > shared_vars;

+    int numSharedVars = 0;

+    for( int j=0; j<(int)d_var_contains[n].size(); j++ ){

+      if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){

+        Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;

+        unique_vars.push_back( d_var_contains[n][j] );

+      }else{

+        shared_vars[ d_var_contains[n][j] ] = true;

+        numSharedVars++;

+      }

+    }

+    //we use the latest shared variables, then unique variables

+    std::vector< int > vars;

+    int index = i==0 ? (int)(pats.size()-1) : (i-1);

+    while( numSharedVars>0 && index!=i ){

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

+        if( it->second ){

+          if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=

+              d_var_contains[ pats[index] ].end() ){

+            vars.push_back( it->first );

+            shared_vars[ it->first ] = false;

+            numSharedVars--;

+          }

+        }

+      }

+      index = index==0 ? (int)(pats.size()-1) : (index-1);

+    }

+    vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );

+    Debug("smart-multi-trigger") << "   Index[" << i << "]: ";

+    for( int i=0; i<(int)vars.size(); i++ ){

+      Debug("smart-multi-trigger") << vars[i] << " ";

+    }

+    Debug("smart-multi-trigger") << std::endl;

+    //make ordered inst match trie

+    InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder;

+    imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() );

+    d_children_trie.push_back( InstMatchTrieOrdered( imtio ) );

+  }

+

+}

+

+/** reset instantiation round (call this whenever equivalence classes have changed) */

+void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){

+  for( int i=0; i<(int)d_children.size(); i++ ){

+    d_children[i]->resetInstantiationRound( qe );

+  }

+}

+

+/** reset, eqc is the equivalence class to search in (any if eqc=null) */

+void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){

+  for( int i=0; i<(int)d_children.size(); i++ ){

+    d_children[i]->reset( eqc, qe );

+  }

+}

+

+int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){

+  int addedLemmas = 0;

+  Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;

+  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;

+    while( d_children[i]->getNextMatch( m, qe ) ){

+      m.makeRepresentative( qe );

+      newMatches.push_back( InstMatch( &m ) );

+      m.clear();

+    }

+    for( int j=0; j<(int)newMatches.size(); j++ ){

+      processNewMatch( qe, newMatches[j], i, addedLemmas );

+    }

+  }

+  return addedLemmas;

+}

+

+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 );

+  //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.

+  Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl;

+  //process new instantiations

+  int childIndex = (fromChildIndex+1)%(int)d_children.size();

+  std::vector< IndexedTrie > unique_var_tries;

+  processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(),

+                            unique_var_tries, 0, childIndex, fromChildIndex, true );

+}

+

+void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,

+                                                        std::vector< IndexedTrie >& unique_var_tries,

+                                                        int trieIndex, int childIndex, int endChildIndex, bool modEq ){

+  if( childIndex==endChildIndex ){

+    //now, process unique variables

+    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() ){

+      //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 ) );

+      //  int newChildIndex = (childIndex+1)%(int)d_children.size();

+      //  processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,

+      //                            0, newChildIndex, endChildIndex, modEq );

+      //}else{

+        //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);

+          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,

+                                  trieIndex+1, childIndex, endChildIndex, modEq );

+      }

+      if( modEq ){

+        //check modulo equality for other possible instantiations

+        if( 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 = tr->d_data.find( en );

+              if( itc!=tr->d_data.end() ){

+                processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,

+                                          trieIndex+1, childIndex, endChildIndex, modEq );

+              }

+            }

+            ++eqc;

+          }

+        }

+      }

+    }

+  }else{

+    int newChildIndex = (childIndex+1)%(int)d_children.size();

+    processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,

+                              0, newChildIndex, endChildIndex, modEq );

+  }

+}

+

+void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,

+                                                         std::vector< IndexedTrie >& unique_var_tries,

+                                                         int uvtIndex, InstMatchTrie* tr, int trieIndex ){

+  if( uvtIndex<(int)unique_var_tries.size() ){

+    int childIndex = unique_var_tries[uvtIndex].first.first;

+    if( !tr ){

+      tr = unique_var_tries[uvtIndex].second;

+      trieIndex = unique_var_tries[uvtIndex].first.second;

+    }

+    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 );

+      //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);

+        processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );

+      }

+    }else{

+      processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );

+    }

+  }else{

+    //m is an instantiation

+    if( qe->addInstantiation( d_f, m ) ){

+      addedLemmas++;

+      Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;

+    }

+  }

+}

+

+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;

+      //if it produces a match, then process it with the rest

+      if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){

+        processNewMatch( qe, m, i, addedLemmas );

+      }

+    }

+  }

+  return addedLemmas;

+}

+

+int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){

+  InstMatch m;

+  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() ]) );

+    }

+  }else{

+    addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) );

+  }

+  return addedLemmas;

+}

+

+void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){

+  if( argIndex==(int)d_match_pattern.getNumChildren() ){

+    //m is an instantiation

+    if( qe->addInstantiation( d_f, m ) ){

+      addedLemmas++;

+      Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl;

+    }

+  }else{

+    if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){

+      Node ic = d_match_pattern[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 ){

+          Node prev = m.get( ic );

+          m.set( ic, t);

+          addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );

+          m.set( ic, prev);

+        }

+      }

+    }else{

+      Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );

+      std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );

+      if( it!=tat->d_data.end() ){

+        addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );

+      }

+    }

+  }

+}

+

+int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){

+  Assert( options::eagerInstQuant() );

+  InstMatch m;

+  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]);

+    }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){

+      return 0;

+    }

+  }

+  return qe->addInstantiation( f, m ) ? 1 : 0;

+}

+

+}/* CVC4::theory::inst namespace */

+}/* CVC4::theory namespace */

+}/* CVC4 namespace */

diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
new file mode 100755
index 000000000..af65e809b
--- /dev/null
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -0,0 +1,192 @@
+/*********************                                                        */

+/*! \file inst_match_generator.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: bobot

+ ** Minor contributors (to current version): mdeters

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009-2012  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief inst match generator class

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H

+#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H

+

+#include "theory/quantifiers/inst_match.h"

+#include <map>

+

+namespace CVC4 {

+namespace theory {

+

+class QuantifiersEngine;

+namespace quantifiers{

+  class TermArgTrie;

+}

+

+namespace inst {

+

+/** base class for producing InstMatch objects */

+class IMGenerator {

+public:

+  /** reset instantiation round (call this at beginning of instantiation round) */

+  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;

+  /** reset, eqc is the equivalence class to search in (any if eqc=null) */

+  virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;

+  /** get the next match.  must call reset( eqc ) before this function. */

+  virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;

+  /** add instantiations directly */

+  virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;

+  /** add ground term t, called when t is added to term db */

+  virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;

+};/* class IMGenerator */

+

+class CandidateGenerator;

+

+class InstMatchGenerator : public IMGenerator {

+private:

+  /** candidate generator */

+  CandidateGenerator* d_cg;

+  /** policy to use for matching */

+  int d_matchPolicy;

+  /** children generators */

+  std::vector< InstMatchGenerator* > d_children;

+  std::vector< int > d_children_index;

+  /** partial vector */

+  std::vector< InstMatch > d_partial;

+  /** eq class */

+  Node d_eq_class;

+  /** for arithmetic matching */

+  std::map< Node, Node > d_arith_coeffs;

+  /** initialize pattern */

+  void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe );

+  void initializePattern( Node pat, QuantifiersEngine* qe );

+public:

+  enum {

+    //options for producing matches

+    MATCH_GEN_DEFAULT = 0,

+    MATCH_GEN_EFFICIENT_E_MATCH,   //generate matches via Efficient E-matching for SMT solvers

+    //others (internally used)

+    MATCH_GEN_INTERNAL_ARITHMETIC,

+    MATCH_GEN_INTERNAL_ERROR,

+  };

+private:

+  /** get the next match.  must call d_cg->reset( ... ) before using.

+      only valid for use where !d_match_pattern.isNull().

+  */

+  bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );

+  /** for arithmetic */

+  bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );

+public:

+  /** get the match against ground term or formula t.

+      d_match_pattern and t should have the same shape.

+      only valid for use where !d_match_pattern.isNull().

+  */

+  bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );

+

+  /** constructors */

+  InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 );

+  InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );

+  /** destructor */

+  ~InstMatchGenerator(){}

+  /** The pattern we are producing matches for.

+      If null, this is a multi trigger that is merging matches from d_children.

+  */

+  Node d_pattern;

+  /** match pattern */

+  Node d_match_pattern;

+public:

+  /** reset instantiation round (call this whenever equivalence classes have changed) */

+  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. */

+  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );

+  /** add instantiations */

+  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );

+  /** add ground term t */

+  int addTerm( Node f, Node t, QuantifiersEngine* qe );

+};/* class InstMatchGenerator */

+

+/** smart multi-trigger implementation */

+class InstMatchGeneratorMulti : public IMGenerator {

+private:

+  /** indexed trie */

+  typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;

+  /** process new match */

+  void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );

+  /** process new instantiations */

+  void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,

+                                 std::vector< IndexedTrie >& unique_var_tries,

+                                 int trieIndex, int childIndex, int endChildIndex, bool modEq );

+  /** process new instantiations 2 */

+  void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,

+                                  std::vector< IndexedTrie >& unique_var_tries,

+                                  int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );

+private:

+  /** var contains (variable indices) for each pattern node */

+  std::map< Node, std::vector< int > > d_var_contains;

+  /** variable indices contained to pattern nodes */

+  std::map< int, std::vector< Node > > d_var_to_node;

+  /** quantifier to use */

+  Node d_f;

+  /** policy to use for matching */

+  int d_matchPolicy;

+  /** children generators */

+  std::vector< InstMatchGenerator* > d_children;

+  /** inst match tries for each child */

+  std::vector< InstMatchTrieOrdered > d_children_trie;

+  /** calculate matches */

+  void calculateMatches( QuantifiersEngine* qe );

+public:

+  /** constructors */

+  InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );

+  /** destructor */

+  ~InstMatchGeneratorMulti(){}

+  /** reset instantiation round (call this whenever equivalence classes have changed) */

+  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) */

+  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }

+  /** add instantiations */

+  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );

+  /** add ground term t */

+  int addTerm( Node f, Node t, QuantifiersEngine* qe );

+};/* class InstMatchGeneratorMulti */

+

+/** smart (single)-trigger implementation */

+class InstMatchGeneratorSimple : public IMGenerator {

+private:

+  /** quantifier for match term */

+  Node d_f;

+  /** match term */

+  Node d_match_pattern;

+  /** 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 ){}

+  /** destructor */

+  ~InstMatchGeneratorSimple(){}

+  /** reset instantiation round (call this whenever equivalence classes have changed) */

+  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) */

+  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }

+  /** add instantiations */

+  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );

+  /** add ground term t, possibly add instantiations */

+  int addTerm( Node f, Node t, QuantifiersEngine* qe );

+};/* class InstMatchGeneratorSimple */

+

+}

+}

+}

+

+#endif

diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index f61083029..598b50957 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -243,10 +243,12 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
       }
       //for calculating terms that we don't need to consider
       if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
-        //need to consider if it is not congruent modulo model basis
-        if( !tabt.addTerm( d_qe, n ) ){
-           BasisNoMatchAttribute bnma;
-           n.setAttribute(bnma,true);
+        if( !n.getAttribute(BasisNoMatchAttribute()) ){
+          //need to consider if it is not congruent modulo model basis
+          if( !tabt.addTerm( d_qe, n ) ){
+             BasisNoMatchAttribute bnma;
+             n.setAttribute(bnma,true);
+          }
         }
       }
     }
@@ -263,6 +265,17 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
   }
 }
 
+bool ModelEngineBuilder::hasConstantDefinition( Node n ){
+  Node lit = n.getKind()==NOT ? n[0] : n;
+  if( lit.getKind()==APPLY_UF ){
+    Node op = lit.getOperator();
+    if( !d_uf_prefs[op].d_const_val.isNull() ){
+      return true;
+    }
+  }
+  return false;
+}
+
 bool ModelEngineBuilder::optUseModel() {
   return options::fmfModelBasedInst();
 }
@@ -305,8 +318,8 @@ bool ModelEngineBuilder::isQuantifierActive( Node f ){
 bool ModelEngineBuilder::isTermActive( Node n ){
   return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term
          ( n.getAttribute(ModelBasisArgAttribute())==1 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments
-                                                                                                      //and is not congruent to another
-                                                                                                      //active term
+                                                                                                      //and is not congruent modulo model basis
+                                                                                                      //to another active term
 }
 
 
@@ -347,7 +360,7 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f )
         isConst = false;
         if( gn.getKind()==APPLY_UF ){
           uf_terms.push_back( gn );
-          isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull();
+          isConst = hasConstantDefinition( gn );
         }else if( gn.getKind()==EQUAL ){
           isConst = true;
           for( int j=0; j<2; j++ ){
@@ -355,7 +368,7 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f )
               if( n[j].getKind()==APPLY_UF &&
                   fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){
                 uf_terms.push_back( gn[j] );
-                isConst = isConst && !d_uf_prefs[ gn[j].getOperator() ].d_const_val.isNull();
+                isConst = isConst && hasConstantDefinition( gn[j] );
               }else{
                 isConst = false;
               }
@@ -456,10 +469,8 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
       std::vector< Node > tr_terms;
       if( lit.getKind()==APPLY_UF ){
         //only match predicates that are contrary to this one, use literal matching
-        std::vector< Node > children;
-        children.push_back( lit );
-        children.push_back( !phase ? fm->d_true : fm->d_false );
-        Node eq = d_qe->getTermDatabase()->mkNodeInstConstant( IFF, children, f );
+        Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
+        d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f );
         tr_terms.push_back( eq );
       }else if( lit.getKind()==EQUAL ){
         //collect trigger terms
@@ -595,10 +606,16 @@ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f )
     d_quant_selection_formula[f] = s;
     Node gs = d_qe->getTermDatabase()->getModelBasis( f, s );
     setSelectedTerms( gs );
+    //quick check if it is constant sat
+    if( hasConstantDefinition( s ) ){
+      d_quant_sat[f] = true;
+    }
   }
   //analyze sub quantifiers
-  for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
-    analyzeQuantifier( fm, d_sub_quants[f][i] );
+  if( d_quant_sat.find( f )==d_quant_sat.end() ){
+    for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
+      analyzeQuantifier( fm, d_sub_quants[f][i] );
+    }
   }
 }
 
@@ -610,78 +627,80 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
   if( fp!=f ) Trace("inst-gen") << "   ";
   Trace("inst-gen") << "Sel Form :      " << d_quant_selection_formula[f] << std::endl;
   int addedLemmas = 0;
-  //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
-  //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
-  //  effectively acting as partial instantiations instead of pointwise instantiations.
-  if( !d_quant_selection_formula[f].isNull() ){
-    //first, try on sub quantifiers
-    for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
-      addedLemmas += doInstGen( fm, d_sub_quants[f][i] );
-    }
-    if( addedLemmas>0 ){
-      Trace("inst-gen") << " -> children added lemmas" << std::endl;
-      return addedLemmas;
-    }else{
-      Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl;
-      //get all possible values of selection formula
-      InstGenProcess igp( d_quant_selection_formula[f] );
-      igp.calculateMatches( d_qe, f );
-      Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl;
-      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;
-          igp.getMatch( d_qe->getEqualityQuery(), i, m );
-          //we only consider matches that are non-empty
-          //  matches that are empty should trigger other instances that are non-empty
-          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;
-            getParentQuantifierMatch( mp, fp, m, f );
-
-            //if this is a partial instantion
-            if( !m.isComplete( f ) ){
-              //if the instantiation does not yet exist
-              if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){
-                //get the partial instantiation pf
-                Node pf = d_qe->getInstantiation( fp, mp );
-                Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl;
-                Trace("inst-gen-pi") << "                         " << pf << std::endl;
-                d_sub_quants[ f ].push_back( pf );
-                d_sub_quant_inst[ pf ] = InstMatch( &mp );
-                d_sub_quant_parent[ pf ] = fp;
-                mp.add( d_quant_basis_match[ fp ] );
-                d_quant_basis_match[ pf ] = InstMatch( &mp );
-                addedLemmas += initializeQuantifier( pf, fp );
-                Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl;
-              }
-            }else{
-              if( d_qe->addInstantiation( fp, mp ) ){
-                addedLemmas++;
+  if( d_quant_sat.find( f )==d_quant_sat.end() ){
+    //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
+    //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
+    //  effectively acting as partial instantiations instead of pointwise instantiations.
+    if( !d_quant_selection_formula[f].isNull() ){
+      //first, try on sub quantifiers
+      for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
+        addedLemmas += doInstGen( fm, d_sub_quants[f][i] );
+      }
+      if( addedLemmas>0 ){
+        Trace("inst-gen") << " -> children added lemmas" << std::endl;
+        return addedLemmas;
+      }else{
+        Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl;
+        //get all possible values of selection formula
+        InstGenProcess igp( d_quant_selection_formula[f] );
+        igp.calculateMatches( d_qe, f );
+        Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl;
+        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;
+            igp.getMatch( d_qe->getEqualityQuery(), i, m );
+            //we only consider matches that are non-empty
+            //  matches that are empty should trigger other instances that are non-empty
+            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;
+              getParentQuantifierMatch( mp, fp, m, f );
+
+              //if this is a partial instantion
+              if( !m.isComplete( f ) ){
+                //if the instantiation does not yet exist
+                if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){
+                  //get the partial instantiation pf
+                  Node pf = d_qe->getInstantiation( fp, mp );
+                  Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl;
+                  Trace("inst-gen-pi") << "                         " << pf << std::endl;
+                  d_sub_quants[ f ].push_back( pf );
+                  d_sub_quant_inst[ pf ] = InstMatch( &mp );
+                  d_sub_quant_parent[ pf ] = fp;
+                  mp.add( d_quant_basis_match[ fp ] );
+                  d_quant_basis_match[ pf ] = InstMatch( &mp );
+                  addedLemmas += initializeQuantifier( pf, fp );
+                  Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl;
+                }
+              }else{
+                if( d_qe->addInstantiation( fp, mp ) ){
+                  addedLemmas++;
+                }
               }
             }
           }
         }
-      }
-      if( addedLemmas==0 ){
-        //all sub quantifiers must be satisfied as well
-        bool subQuantSat = true;
-        for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
-          if( d_quant_sat.find( d_sub_quants[f][i] )==d_quant_sat.end() ){
-            subQuantSat = false;
-            break;
+        if( addedLemmas==0 ){
+          //all sub quantifiers must be satisfied as well
+          bool subQuantSat = true;
+          for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
+            if( d_quant_sat.find( d_sub_quants[f][i] )==d_quant_sat.end() ){
+              subQuantSat = false;
+              break;
+            }
+          }
+          if( subQuantSat ){
+            d_quant_sat[ f ] = true;
           }
         }
-        if( subQuantSat ){
-          d_quant_sat[ f ] = true;
-        }
-      }
-      if( fp!=f ) Trace("inst-gen") << "   ";
-      Trace("inst-gen") << "  -> added lemmas = " << addedLemmas << std::endl;
-      if( d_quant_sat.find( f )!=d_quant_sat.end() ){
         if( fp!=f ) Trace("inst-gen") << "   ";
-        Trace("inst-gen") << "  -> *** it is satisfied" << std::endl;
+        Trace("inst-gen") << "  -> added lemmas = " << addedLemmas << std::endl;
+        if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+          if( fp!=f ) Trace("inst-gen") << "   ";
+          Trace("inst-gen") << "  -> *** it is satisfied" << std::endl;
+        }
       }
     }
   }
@@ -697,24 +716,52 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar
     ret = getSelectionFormula( fn[0], n[0], !polarity, useOption );
   }else if( n.getKind()==OR || n.getKind()==IMPLIES || n.getKind()==AND ){
     //whether we only need to find one or all
-    bool posPol = (( n.getKind()==OR || n.getKind()==IMPLIES ) && polarity ) || ( n.getKind()==AND && !polarity );
+    bool favorPol = ( n.getKind()!=AND && polarity ) || ( n.getKind()==AND && !polarity );
     std::vector< Node > children;
-    bool retSet = false;
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
       Node fnc = ( i==0 && fn.getKind()==IMPLIES ) ? fn[i].negate() : fn[i];
       Node nc = ( i==0 && n.getKind()==IMPLIES ) ? n[i].negate() : n[i];
       Node nn = getSelectionFormula( fnc, nc, polarity, useOption );
-      if( nn.isNull()!=posPol ){   //TODO: may want to weaken selection formula
-        ret = nn;
-        retSet = true;
+      if( nn.isNull() && !favorPol ){
+        //cannot make selection formula
+        children.clear();
         break;
       }
-      if( std::find( children.begin(), children.end(), nn )==children.end() ){
-        children.push_back( nn );
+      if( !nn.isNull() ){
+        if( favorPol ){   //temporary
+          return nn;      //
+        }                 //
+        if( std::find( children.begin(), children.end(), nn )==children.end() ){
+          children.push_back( nn );
+        }
       }
     }
-    if( !retSet && !posPol ){
-      ret = NodeManager::currentNM()->mkNode( AND, children );
+    if( !children.empty() ){
+      if( favorPol ){
+        //filter which formulas we wish to keep, make disjunction
+        Node min_lit;
+        int min_score = -1;
+        for( size_t i=0; i<children.size(); i++ ){
+          //if it is constant apply uf application, return it for sure
+          if( hasConstantDefinition( children[i] ) ){
+            min_lit = children[i];
+            break;
+          }else{
+            int score = getSelectionFormulaScore( children[i] );
+            if( min_score<0 || score<min_score ){
+              min_score = score;
+              min_lit = children[i];
+            }
+          }
+        }
+        //currently just return the best single literal
+        ret = min_lit;
+      }else{
+        //selection formula must be conjunction of children
+        ret = NodeManager::currentNM()->mkNode( AND, children );
+      }
+    }else{
+      ret = Node::null();
     }
   }else if( n.getKind()==ITE ){
     Node nn;
@@ -771,6 +818,24 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar
   return ret;
 }
 
+int ModelEngineBuilderInstGen::getSelectionFormulaScore( Node fn ){
+  if( fn.getType().isBoolean() ){
+    if( fn.getKind()==APPLY_UF ){
+      Node op = fn.getOperator();
+      //return total number of terms
+      return d_qe->getTermDatabase()->d_op_count[op];
+    }else{
+      int score = 0;
+      for( size_t i=0; i<fn.getNumChildren(); i++ ){
+        score += getSelectionFormulaScore( fn[i] );
+      }
+      return score;
+    }
+  }else{
+    return 0;
+  }
+}
+
 void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){
 
   //if it is apply uf and has model basis arguments, then mark term as being "selected"
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index e2f422a0a..7c720d604 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -95,6 +95,9 @@ public:
   bool d_considerAxioms;
   // set effort
   void setEffort( int effort );
+protected:  //helper functions
+  /** term has constant definition */
+  bool hasConstantDefinition( Node n );
 public:
   //options
   virtual bool optUseModel();
@@ -177,6 +180,8 @@ protected:
 private:
   //get selection formula for quantifier body
   Node getSelectionFormula( Node fn, Node n, bool polarity, int useOption );
+  //get a heuristic score for a selection formula
+  int getSelectionFormulaScore( Node fn );
   //set selected terms in term
   void setSelectedTerms( Node s );
   //is usable selection literal
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 7a2d965b8..d1b0e0fea 100755
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -14,6 +14,7 @@
 

 #include "theory/quantifiers/quant_util.h"

 #include "theory/quantifiers/inst_match.h"

+#include "theory/quantifiers/term_database.h"

 

 using namespace std;

 using namespace CVC4;

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 1479f910e..18aaab01f 100755
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -18,6 +18,7 @@
 #define __CVC4__THEORY__QUANT_UTIL_H

 

 #include "theory/theory.h"

+#include "theory/uf/equality_engine.h"

 

 #include <ext/hash_set>

 #include <iostream>

@@ -71,6 +72,30 @@ public:
   std::map< Node, Node > d_phase_reqs_equality_term;

 };

 

+

+class EqualityQuery {

+public:

+  EqualityQuery(){}

+  virtual ~EqualityQuery(){};

+  /** contains term */

+  virtual bool hasTerm( Node a ) = 0;

+  /** get the representative of the equivalence class of a */

+  virtual Node getRepresentative( Node a ) = 0;

+  /** returns true if a and b are equal in the current context */

+  virtual bool areEqual( Node a, Node b ) = 0;

+  /** returns true is a and b are disequal in the current context */

+  virtual bool areDisequal( Node a, Node b ) = 0;

+  /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.

+      If cbqi is active, this will return a term in the equivalence class of "a" that does

+      not contain instantiation constants, if such a term exists.

+   */

+  virtual Node getInternalRepresentative( Node a ) = 0;

+  /** get the equality engine associated with this query */

+  virtual eq::EqualityEngine* getEngine() = 0;

+  /** get the equivalence class of a */

+  virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;

+};/* class EqualityQuery */

+

 }

 }

 

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 3b2778061..43548f021 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -45,33 +45,6 @@ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
   }
 }
 
-Trigger* TrTrie::getTrigger2( std::vector< Node >& nodes ){
-  if( nodes.empty() ){
-    return d_tr;
-  }else{
-    Node n = nodes.back();
-    nodes.pop_back();
-    if( d_children.find( n )!=d_children.end() ){
-      return d_children[n]->getTrigger2( nodes );
-    }else{
-      return NULL;
-    }
-  }
-}
-
-void TrTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
-  if( nodes.empty() ){
-    d_tr = t;
-  }else{
-    Node n = nodes.back();
-    nodes.pop_back();
-    if( d_children.find( n )==d_children.end() ){
-      d_children[n] = new TrTrie;
-    }
-    d_children[n]->addTrigger2( nodes, t );
-  }
-}
-
 void TermDb::addTermEfficient( Node n, std::set< Node >& added){
   static AvailableInTermDb aitdi;
   if (inst::Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){
@@ -106,14 +79,14 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
         d_op_map[op].push_back( n );
         added.insert( n );
 
-        uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
           addTerm( n[i], added, withinQuant );
           if( options::efficientEMatching() ){
+            uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
             if( d_parents[n[i]][op].empty() ){
               //must add parent to equivalence class info
-              Node nir = d_ith->getRepresentative( n[i] );
-              uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir );
+              Node nir = ith->getRepresentative( n[i] );
+              uf::EqClassInfo* eci_nir = ith->getEquivalenceClassInfo( nir );
               if( eci_nir ){
                 eci_nir->d_pfuns[ op ] = true;
               }
@@ -126,9 +99,10 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
           }
           if( options::eagerInstQuant() ){
             if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
+              uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
               int addedLemmas = 0;
-              for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
-                addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n );
+              for( int i=0; i<(int)ith->d_op_triggers[op].size(); i++ ){
+                addedLemmas += ith->d_op_triggers[op][i]->addTerm( n );
               }
               //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
               d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() );
@@ -157,6 +131,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
    int alreadyCongruentCount = 0;
    //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
    for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
+     d_op_count[ it->first ] = 0;
      if( !it->second.empty() ){
        if( it->second[0].getType().isBoolean() ){
          d_pred_map_trie[ 0 ][ it->first ].d_data.clear();
@@ -174,6 +149,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
                congruentCount++;
              }else{
                nonCongruentCount++;
+               d_op_count[ it->first ]++;
              }
            }else{
              congruentCount++;
@@ -200,6 +176,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
              congruentCount++;
            }else{
              nonCongruentCount++;
+             d_op_count[ op ]++;
            }
          }else{
            alreadyCongruentCount++;
@@ -360,12 +337,6 @@ Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & var
   return n2;
 }
 
-Node TermDb::mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f ){
-  Node n = NodeManager::currentNM()->mkNode( k, children );
-  setInstantiationConstantAttr( n, f );
-  return n;
-}
-
 
 
 Node TermDb::getSkolemizedBody( Node f ){
@@ -379,24 +350,10 @@ Node TermDb::getSkolemizedBody( Node f ){
     }
     d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(),
                                             d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() );
-    if( f.hasAttribute(InstLevelAttribute()) ){
-      setInstantiationLevelAttr( d_skolem_body[ f ], f.getAttribute(InstLevelAttribute()) );
-    }
   }
   return d_skolem_body[ f ];
 }
 
-
-void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){
-  if( !n.hasAttribute(InstLevelAttribute()) ){
-    InstLevelAttribute ila;
-    n.setAttribute(ila,level);
-  }
-  for( int i=0; i<(int)n.getNumChildren(); i++ ){
-    setInstantiationLevelAttr( n[i], level );
-  }
-}
-
 Node TermDb::getFreeVariableForInstConstant( Node n ){
   TypeNode tn = n.getType();
   if( d_free_vars.find( tn )==d_free_vars.end() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index bcd6b833d..e1786d44c 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -24,6 +24,42 @@
 namespace CVC4 {
 namespace theory {
 
+/** Attribute true for nodes that should not be used for matching */
+struct NoMatchAttributeId {};
+/** use the special for boolean flag */
+typedef expr::Attribute< NoMatchAttributeId,
+                         bool,
+                         expr::attr::NullCleanupStrategy,
+                         true // context dependent
+                       > NoMatchAttribute;
+
+// attribute for "contains instantiation constants from"
+struct InstConstantAttributeId {};
+typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
+
+struct InstLevelAttributeId {};
+typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
+
+struct InstVarNumAttributeId {};
+typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
+
+// Attribute that tell if a node have been asserted in this branch
+struct AvailableInTermDbId {};
+/** use the special for boolean flag */
+typedef expr::Attribute<AvailableInTermDbId,
+                        bool,
+                        expr::attr::NullCleanupStrategy,
+                        true  // context dependent
+                        > AvailableInTermDb;
+
+struct ModelBasisAttributeId {};
+typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
+//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
+//                    0 : term has no direct child with model basis attribute.
+struct ModelBasisArgAttributeId {};
+typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
+
+
 class QuantifiersEngine;
 
 namespace inst{
@@ -43,45 +79,21 @@ public:
 };/* class TermArgTrie */
 
 
-/** a trie of triggers */
-class TrTrie {
-private:
-  inst::Trigger* getTrigger2( std::vector< Node >& nodes );
-  void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t );
-public:
-  TrTrie() : d_tr( NULL ){}
-  inst::Trigger* d_tr;
-  std::map< TNode, TrTrie* > d_children;
-  inst::Trigger* getTrigger( std::vector< Node >& nodes ){
-    std::vector< Node > temp;
-    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
-    std::sort( temp.begin(), temp.end() );
-    return getTrigger2( temp );
-  }
-  void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){
-    std::vector< Node > temp;
-    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
-    std::sort( temp.begin(), temp.end() );
-    return addTrigger2( temp, t );
-  }
-};/* class inst::Trigger::TrTrie */
-
-
 class TermDb {
   friend class ::CVC4::theory::QuantifiersEngine;
   friend class ::CVC4::theory::inst::Trigger;
 private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
-  /** calculated no match terms */
-  bool d_matching_active;
   /** terms processed */
   std::hash_set< Node, NodeHashFunction > d_processed;
 public:
-  TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){}
+  TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
   ~TermDb(){}
   /** map from APPLY_UF operators to ground terms for that operator */
   std::map< Node, std::vector< Node > > d_op_map;
+  /** count number of APPLY_UF terms per operator */
+  std::map< Node, int > d_op_count;
   /** map from APPLY_UF functions to trie */
   std::map< Node, TermArgTrie > d_func_map_trie;
   /** map from APPLY_UF predicates to trie */
@@ -92,10 +104,6 @@ public:
   void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
   /** reset (calculate which terms are active) */
   void reset( Theory::Effort effort );
-  /** set active */
-  void setMatchingActive( bool a ) { d_matching_active = a; }
-  /** get active */
-  bool getMatchingActive() { return d_matching_active; }
 private:
   /** for efficient e-matching */
   void addTermEfficient( Node n, std::set< Node >& added);
@@ -168,10 +176,6 @@ public:
   Node convertNodeToPattern( Node n, Node f,
                              const std::vector<Node> & vars,
                              const std::vector<Node> & nvars);
-  /** get iff term */
-  Node getInstConstantIffTerm( Node n, bool pol );
-  /** make node, validating the inst constant attribute */
-  Node mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f );
   /** set instantiation constant attr */
   void setInstantiationConstantAttr( Node n, Node f );
 
@@ -194,8 +198,6 @@ private:
 public:
   /** get free variable for instantiation constant */
   Node getFreeVariableForInstConstant( Node n );
-  /** set instantiation level attr */
-  void setInstantiationLevelAttr( Node n, uint64_t level );
 
 //for triggers
 private:
@@ -212,14 +214,6 @@ public:
   void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
   /** get var contains for node n */
   void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
-private:
-  /** all triggers will be stored in this trie */
-  TrTrie d_tr_trie;
-public:
-  /** get trigger */
-  inst::Trigger* getTrigger( std::vector< Node >& nodes ){ return d_tr_trie.getTrigger( nodes ); }
-  /** add trigger */
-  void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){ d_tr_trie.addTrigger( nodes, t ); }
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 90a673715..c64a75ec4 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -20,6 +20,7 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/inst_match_generator.h"
 
 using namespace std;
 using namespace CVC4;
@@ -97,6 +98,10 @@ int Trigger::addTerm( Node t ){
   return d_mg->addTerm( d_f, t, d_quantEngine );
 }
 
+//bool Trigger::nonunifiable( TNode t, const std::vector<Node> & vars){
+//  return d_mg->nonunifiable(t,vars);
+//}
+
 int Trigger::addInstantiations( InstMatch& baseMatch ){
   int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine );
   if( addedLemmas>0 ){
@@ -183,7 +188,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
     //  Notice() << "Trigger new old = " << trNew << " " << trOld << std::endl;
     //}
   }else{
-    Trigger* t = qe->getTermDatabase()->getTrigger( trNodes );
+    Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes );
     if( t ){
       if( trOption==TR_GET_OLD ){
         //just return old trigger
@@ -194,7 +199,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
     }
   }
   Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers );
-  qe->getTermDatabase()->addTrigger( trNodes, t );
+  qe->getTriggerDatabase()->addTrigger( trNodes, t );
   return t;
 }
 Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){
@@ -470,3 +475,30 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef
   }
   return false;
 }
+
+Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
+  if( nodes.empty() ){
+    return d_tr;
+  }else{
+    Node n = nodes.back();
+    nodes.pop_back();
+    if( d_children.find( n )!=d_children.end() ){
+      return d_children[n]->getTrigger2( nodes );
+    }else{
+      return NULL;
+    }
+  }
+}
+
+void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
+  if( nodes.empty() ){
+    d_tr = t;
+  }else{
+    Node n = nodes.back();
+    nodes.pop_back();
+    if( d_children.find( n )==d_children.end() ){
+      d_children[n] = new TriggerTrie;
+    }
+    d_children[n]->addTrigger2( nodes, t );
+  }
+}
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 945b5db2a..267debb02 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -18,11 +18,19 @@
 #define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
 
 #include "theory/quantifiers/inst_match.h"
+#include "expr/node.h"
+#include "util/hash.h"
+#include <map>
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace inst {
 
+class IMGenerator;
+
 //a collect of nodes representing a trigger
 class Trigger {
 private:
@@ -56,11 +64,6 @@ public:
   bool getMatch( Node t, InstMatch& m);
   /** add ground term t, called when t is added to the TermDb */
   int addTerm( Node t );
-  /** return true if whatever Node is subsituted for the variables the
-      given Node can't match the pattern */
-  bool nonunifiable( TNode t, const std::vector<Node> & vars){
-    return d_mg->nonunifiable(t,vars);
-  }
   /** return whether this is a multi-trigger */
   bool isMultiTrigger() { return d_nodes.size()>1; }
 public:
@@ -127,6 +130,30 @@ inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) {
   return out;
 }
 
+
+/** a trie of triggers */
+class TriggerTrie {
+private:
+  inst::Trigger* getTrigger2( std::vector< Node >& nodes );
+  void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t );
+public:
+  TriggerTrie() : d_tr( NULL ){}
+  inst::Trigger* d_tr;
+  std::map< TNode, TriggerTrie* > d_children;
+  inst::Trigger* getTrigger( std::vector< Node >& nodes ){
+    std::vector< Node > temp;
+    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
+    std::sort( temp.begin(), temp.end() );
+    return getTrigger2( temp );
+  }
+  void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){
+    std::vector< Node > temp;
+    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
+    std::sort( temp.begin(), temp.end() );
+    return addTrigger2( temp, t );
+  }
+};/* class inst::Trigger::Trigger */
+
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4e933a511..a44a3ff1f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -25,7 +25,6 @@
 #include "theory/quantifiers/instantiation_engine.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
 
 using namespace std;
 using namespace CVC4;
@@ -39,6 +38,7 @@ d_te( te ),
 d_quant_rel( false ){ //currently do not care about relevance
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
   d_term_db = new quantifiers::TermDb( this );
+  d_tr_trie = new inst::TriggerTrie;
   d_hasAddedLemma = false;
 
   //the model object
@@ -124,18 +124,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
 }
 
-std::vector<Node> QuantifiersEngine::createInstVariable( std::vector<Node> & vars ){
-  std::vector<Node> inst_constant;
-  inst_constant.reserve(vars.size());
-  for( std::vector<Node>::const_iterator v = vars.begin();
-       v != vars.end(); ++v ){
-    //make instantiation constants
-    Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() );
-    inst_constant.push_back( ic );
-  };
-  return inst_constant;
-}
-
 void QuantifiersEngine::registerQuantifier( Node f ){
   if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
     d_quants.push_back( f );
@@ -227,6 +215,61 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No
   }
 }
 
+bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
+  Assert( f.getKind()==FORALL );
+  Assert( !f.hasAttribute(InstConstantAttribute()) );
+  Assert( vars.size()==terms.size() );
+  Node body = getInstantiation( f, vars, terms );
+  //make the lemma
+  NodeBuilder<> nb(kind::OR);
+  nb << f.notNode() << body;
+  Node lem = nb;
+  //check for duplication
+  if( addLemma( lem ) ){
+    Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
+    uint64_t maxInstLevel = 0;
+    for( int i=0; i<(int)terms.size(); i++ ){
+      if( terms[i].hasAttribute(InstConstantAttribute()) ){
+        Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
+        for( int i=0; i<(int)terms.size(); i++ ){
+          Debug("inst") << "   " << terms[i] << std::endl;
+        }
+        Unreachable("Bad instantiation");
+      }else{
+        Trace("inst") << "   " << terms[i];
+        //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute());
+        Trace("inst") << std::endl;
+        if( terms[i].hasAttribute(InstLevelAttribute()) ){
+          if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
+            maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
+          }
+        }else{
+          setInstantiationLevelAttr( terms[i], 0 );
+        }
+      }
+    }
+    Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
+    setInstantiationLevelAttr( body, maxInstLevel+1 );
+    ++(d_statistics.d_instantiations);
+    d_statistics.d_total_inst_var += (int)terms.size();
+    d_statistics.d_max_instantiation_level.maxAssign( maxInstLevel+1 );
+    return true;
+  }else{
+    ++(d_statistics.d_inst_duplicate);
+    return false;
+  }
+}
+
+void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
+  if( !n.hasAttribute(InstLevelAttribute()) ){
+    InstLevelAttribute ila;
+    n.setAttribute(ila,level);
+  }
+  for( int i=0; i<(int)n.getNumChildren(); i++ ){
+    setInstantiationLevelAttr( n[i], level );
+  }
+}
+
 Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
   Node body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
   //process partial instantiation if necessary
@@ -272,51 +315,6 @@ bool QuantifiersEngine::addLemma( Node lem ){
   }
 }
 
-bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
-  Assert( f.getKind()==FORALL );
-  Assert( !f.hasAttribute(InstConstantAttribute()) );
-  Assert( vars.size()==terms.size() );
-  Node body = getInstantiation( f, vars, terms );
-  //make the lemma
-  NodeBuilder<> nb(kind::OR);
-  nb << f.notNode() << body;
-  Node lem = nb;
-  //check for duplication
-  if( addLemma( lem ) ){
-    Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
-    uint64_t maxInstLevel = 0;
-    for( int i=0; i<(int)terms.size(); i++ ){
-      if( terms[i].hasAttribute(InstConstantAttribute()) ){
-        Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
-        for( int i=0; i<(int)terms.size(); i++ ){
-          Debug("inst") << "   " << terms[i] << std::endl;
-        }
-        Unreachable("Bad instantiation");
-      }else{
-        Trace("inst") << "   " << terms[i];
-        //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute());
-        Trace("inst") << std::endl;
-        if( terms[i].hasAttribute(InstLevelAttribute()) ){
-          if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
-            maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
-          }
-        }else{
-          d_term_db->setInstantiationLevelAttr( terms[i], 0 );
-        }
-      }
-    }
-    Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
-    d_term_db->setInstantiationLevelAttr( body, maxInstLevel+1 );
-    ++(d_statistics.d_instantiations);
-    d_statistics.d_total_inst_var += (int)terms.size();
-    d_statistics.d_max_instantiation_level.maxAssign( maxInstLevel+1 );
-    return true;
-  }else{
-    ++(d_statistics.d_inst_duplicate);
-    return false;
-  }
-}
-
 bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){
   //make sure there are values for each variable we are instantiating
   m.makeComplete( f, this );
@@ -395,10 +393,8 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
       bool nodeChanged = false;
       if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
         bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
-        std::vector< Node > children;
-        children.push_back( nodes[i] );
-        children.push_back( NodeManager::currentNM()->mkConst<bool>(preq) );
-        nodes[i] = d_term_db->mkNodeInstConstant( IFF, children, f );
+        nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
+        d_term_db->setInstantiationConstantAttr( nodes[i], f );
         nodeChanged = true;
       }
       //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
@@ -416,6 +412,56 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
     d_statistics.d_lit_phase_nreq += (int)nodes.size();
   }
 }
+/*
+EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) {
+  // Should use skeleton (in order to have the type and the kind
+  //  or any needed other information) instead of only the type
+
+  // TheoryId id = Theory::theoryOf(t);
+  // inst::EqualityQuery* eq = d_eq_query_arr[id];
+  // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF];
+  // else return eq;
+
+  // hack because the generic one is too slow
+  // TheoryId id = Theory::theoryOf(t);
+  // if( true || id == theory::THEORY_UF){
+  //   uf::InstantiatorTheoryUf* ith = static_cast<uf::InstantiatorTheoryUf*>( getInstantiator( theory::THEORY_UF ));
+  //   return new uf::EqualityQueryInstantiatorTheoryUf(ith);
+  // }
+  // inst::EqualityQuery* eq = d_eq_query_arr[id];
+  // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF];
+  // else return eq;
+
+
+  //Currently we use the generic EqualityQuery
+  return getEqualityQuery();
+}
+
+
+rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses() {
+  return new GenericCandidateGeneratorClasses(this);
+}
+
+rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass() {
+  return new GenericCandidateGeneratorClass(this);
+}
+
+rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses(TypeNode t) {
+  // TheoryId id = Theory::theoryOf(t);
+  // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClasses();
+  // if(eq == NULL) return getInstantiator(id)->getRRCanGenClasses();
+  // else return eq;
+  return getRRCanGenClasses();
+}
+
+rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) {
+  // TheoryId id = Theory::theoryOf(t);
+  // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClass();
+  // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass();
+  // else return eq;
+  return getRRCanGenClass();
+}
+*/
 
 QuantifiersEngine::Statistics::Statistics():
   d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
@@ -602,52 +648,3 @@ void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< N
     eqc.push_back( a );
   }
 }
-
-inst::EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) {
-  /** Should use skeleton (in order to have the type and the kind
-      or any needed other information) instead of only the type */
-
-  // TheoryId id = Theory::theoryOf(t);
-  // inst::EqualityQuery* eq = d_eq_query_arr[id];
-  // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF];
-  // else return eq;
-
-  /** hack because the generic one is too slow */
-  // TheoryId id = Theory::theoryOf(t);
-  // if( true || id == theory::THEORY_UF){
-  //   uf::InstantiatorTheoryUf* ith = static_cast<uf::InstantiatorTheoryUf*>( getInstantiator( theory::THEORY_UF ));
-  //   return new uf::EqualityQueryInstantiatorTheoryUf(ith);
-  // }
-  // inst::EqualityQuery* eq = d_eq_query_arr[id];
-  // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF];
-  // else return eq;
-
-
-  //Currently we use the generic EqualityQuery
-  return getEqualityQuery();
-}
-
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses() {
-  return new GenericCandidateGeneratorClasses(this);
-}
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass() {
-  return new GenericCandidateGeneratorClass(this);
-}
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses(TypeNode t) {
-  // TheoryId id = Theory::theoryOf(t);
-  // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClasses();
-  // if(eq == NULL) return getInstantiator(id)->getRRCanGenClasses();
-  // else return eq;
-  return getRRCanGenClasses();
-}
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) {
-  // TheoryId id = Theory::theoryOf(t);
-  // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClass();
-  // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass();
-  // else return eq;
-  return getRRCanGenClass();
-}
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index be8830710..18635a823 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -62,6 +62,9 @@ namespace quantifiers {
   class FirstOrderModel;
 }/* CVC4::theory::quantifiers */
 
+namespace inst {
+  class TriggerTrie;
+}/* CVC4::theory::inst */
 
 class QuantifiersEngine {
   friend class quantifiers::InstantiationEngine;
@@ -84,20 +87,20 @@ private:
   /** phase requirements for each quantifier for each instantiation literal */
   std::map< Node, QuantPhaseReq* > d_phase_reqs;
 private:
-  /** list of all quantifiers (pre-rewrite) */
+  /** list of all quantifiers seen */
   std::vector< Node > d_quants;
-  /** lemmas produced */
+  /** list of all lemmas produced */
   std::map< Node, bool > d_lemmas_produced;
   /** lemmas waiting */
   std::vector< Node > d_lemmas_waiting;
   /** has added lemma this round */
   bool d_hasAddedLemma;
-  /** inst matches produced for each quantifier */
+  /** list of all instantiations produced for each quantifier */
   std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
-  /** owner of quantifiers */
-  std::map< Node, Theory* > d_owner;
   /** term database */
   quantifiers::TermDb* d_term_db;
+  /** all triggers will be stored in this trie */
+  inst::TriggerTrie* d_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
 private:
@@ -111,15 +114,7 @@ public:
   TheoryEngine* getTheoryEngine() { return d_te; }
   /** get equality query object for the given type. The default is the
       generic one */
-  inst::EqualityQuery* getEqualityQuery(TypeNode t);
-  inst::EqualityQuery* getEqualityQuery() { return d_eq_query; }
-  /** get equality query object for the given type. The default is the
-      one of UF */
-  rrinst::CandidateGenerator* getRRCanGenClasses(TypeNode t);
-  rrinst::CandidateGenerator* getRRCanGenClass(TypeNode t);
-  /* generic candidate generator */
-  rrinst::CandidateGenerator* getRRCanGenClasses();
-  rrinst::CandidateGenerator* getRRCanGenClass();
+  EqualityQuery* getEqualityQuery() { return d_eq_query; }
   /** get instantiation engine */
   quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
   /** get model engine */
@@ -151,14 +146,13 @@ public:
   Node getNextDecisionRequest();
   /** reset instantiation round */
   void resetInstantiationRound( Theory::Effort level );
-
-  //create inst variable
-  std::vector<Node> createInstVariable( std::vector<Node> & vars );
 private:
   /** compute term vector */
   void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
   /** instantiate f with arguments terms */
   bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
+  /** set instantiation level attr */
+  void setInstantiationLevelAttr( Node n, uint64_t level );
 public:
   /** get instantiation */
   Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
@@ -190,6 +184,8 @@ public:
   quantifiers::FirstOrderModel* getModel() { return d_model; }
   /** get term database */
   quantifiers::TermDb* getTermDatabase() { return d_term_db; }
+  /** get trigger database */
+  inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
   /** add term to database */
   void addTermToDatabase( Node n, bool withinQuant = false );
 public:
diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp
index 572ccfad2..af4cdeb50 100644
--- a/src/theory/rewriterules/rr_inst_match.cpp
+++ b/src/theory/rewriterules/rr_inst_match.cpp
@@ -23,6 +23,7 @@
 #include "theory/rewriterules/rr_trigger.h"
 #include "theory/rewriterules/rr_inst_match_impl.h"
 #include "theory/rewriterules/rr_candidate_generator.h"
+#include "theory/quantifiers/candidate_generator.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -140,7 +141,8 @@ ApplyMatcher::ApplyMatcher( Node pat, QuantifiersEngine* qe): d_pattern(pat){
 
   //set-up d_variables, d_constants, d_childrens
   for( size_t i=0; i< d_pattern.getNumChildren(); ++i ){
-    EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType());
+    //EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType());
+    EqualityQuery* q = qe->getEqualityQuery();
     Assert( q != NULL );
     if( d_pattern[i].hasAttribute(InstConstantAttribute()) ){
       if( d_pattern[i].getKind()==INST_CONSTANT ){
@@ -327,7 +329,8 @@ class VarMatcher: public Matcher{
   EqualityQuery* d_q;
 public:
   VarMatcher(Node var, QuantifiersEngine* qe): d_var(var), d_binded(false){
-    d_q = qe->getEqualityQuery(var.getType());
+    //d_q = qe->getEqualityQuery(var.getType());
+    d_q = qe->getEqualityQuery();
   }
   void resetInstantiationRound( QuantifiersEngine* qe ){};
   bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){
@@ -600,9 +603,9 @@ private:
 public:
   void mkCandidateGenerator(){
     if(classes)
-      d_cg = d_qe->getRRCanGenClasses();
+      d_cg = new GenericCandidateGeneratorClasses(d_qe);
     else
-     d_cg = d_qe->getRRCanGenClass();
+      d_cg = new GenericCandidateGeneratorClass(d_qe);
   }
 
   GenericCandidateGeneratorClasses(QuantifiersEngine* qe):
diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h
index 14873b501..63728a95b 100644
--- a/src/theory/rewriterules/rr_inst_match.h
+++ b/src/theory/rewriterules/rr_inst_match.h
@@ -30,6 +30,7 @@
 #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"
 
@@ -55,7 +56,7 @@ public:
         Node cand = cg->getNextCandidate();
         //.......
       }while( !cand.isNull() );
-      
+
       eqc is the equivalence class you are searching in
   */
   virtual void reset( TNode eqc ) = 0;
diff --git a/src/theory/rewriterules/rr_inst_match_impl.h b/src/theory/rewriterules/rr_inst_match_impl.h
index 43161a9e5..388d1a702 100644
--- a/src/theory/rewriterules/rr_inst_match_impl.h
+++ b/src/theory/rewriterules/rr_inst_match_impl.h
@@ -31,7 +31,7 @@ template<bool modEq>
 InstMatchTrie2Gen<modEq>::InstMatchTrie2Gen(context::Context* c,  QuantifiersEngine* qe):
   d_context(c), d_mods(c) {
   d_eQ = qe->getEqualityQuery();
-  d_cG = qe->getRRCanGenClass();
+  d_cG = new GenericCandidateGeneratorClass(qe);
 };
 
 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index 5e06bfd0b..4a27b4559 100644
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -263,6 +263,9 @@ private:
                          rewriter::Subst & pvars,
                          rewriter::Subst & vars);
 
+  //create inst variable
+  std::vector<Node> createInstVariable( std::vector<Node> & vars );
+
     /** statistics class */
   class Statistics {
   public:
diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp
index cc01a01ff..20e5fa084 100644
--- a/src/theory/rewriterules/theory_rewriterules_rules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp
@@ -151,8 +151,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r)
     vars.push_back(*v);
   };
   /* Instantiation version */
-  std::vector<Node> inst_constants =
-    getQuantifiersEngine()->createInstVariable(vars);
+  std::vector<Node> inst_constants = createInstVariable(vars);
   /* Body/Remove_term/Guards/Triggers */
   Node body = r[2][1];
   TNode new_terms = r[2][1];
@@ -377,6 +376,18 @@ bool TheoryRewriteRules::addRewritePattern(TNode pattern, TNode body,
 
 }
 
+std::vector<Node> TheoryRewriteRules::createInstVariable( std::vector<Node> & vars ){
+  std::vector<Node> inst_constant;
+  inst_constant.reserve(vars.size());
+  for( std::vector<Node>::const_iterator v = vars.begin();
+       v != vars.end(); ++v ){
+    //make instantiation constants
+    Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() );
+    inst_constant.push_back( ic );
+  };
+  return inst_constant;
+}
+
 
 }/* CVC4::theory::rewriterules namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
index 24da83786..eceb4715b 100644
--- a/src/theory/uf/theory_uf_instantiator.cpp
+++ b/src/theory/uf/theory_uf_instantiator.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/options.h"
 #include "theory/rewriterules/options.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/candidate_generator.h"
 
 using namespace std;
 using namespace CVC4;
@@ -771,7 +772,7 @@ void InstantiatorTheoryUf::registerEfficientHandler( EfficientHandler& handler,
   //take all terms from the uf term db and add to candidate generator
   if( pats[0].getKind() == kind::INST_CONSTANT ){
     TypeNode ty = pats[0].getType();
-    rrinst::CandidateGenerator* cg = d_quantEngine->getRRCanGenClasses(ty);
+    rrinst::CandidateGenerator* cg = new GenericCandidateGeneratorClasses(d_quantEngine);
     cg->reset(Node::null());
     TNode c;
     SetNode ele;
diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h
index 13a35d8a3..501ef9a6d 100644
--- a/src/theory/uf/theory_uf_instantiator.h
+++ b/src/theory/uf/theory_uf_instantiator.h
@@ -26,6 +26,7 @@
 #include "util/statistics_registry.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/inst_match_generator.h"
 #include "util/ntuple.h"
 #include "context/cdqueue.h"