Fix for rewriterules build breakage.

25 files changed, 17 insertions, 5054 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 450bf063e..03092979a 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -20,7 +20,7 @@ AM_CPPFLAGS = \
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main
-THEORIES = builtin booleans uf arith bv arrays datatypes sets strings quantifiers rewriterules idl
+THEORIES = builtin booleans uf arith bv arrays datatypes sets strings quantifiers idl
 
 lib_LTLIBRARIES = libcvc4.la
 
@@ -307,8 +307,6 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/quant_conflict_find.h \
 	theory/quantifiers/quant_conflict_find.cpp \
 	theory/quantifiers/options_handlers.h \
-	theory/rewriterules/theory_rewriterules.h \
-	theory/rewriterules/theory_rewriterules.cpp \
 	theory/arith/theory_arith_type_rules.h \
 	theory/arith/type_enumerator.h \
 	theory/arith/arithvar.h \
@@ -457,7 +455,6 @@ EXTRA_DIST = \
 	theory/strings/kinds \
 	theory/arrays/kinds \
 	theory/quantifiers/kinds \
-	theory/rewriterules/kinds \
 	theory/arith/kinds \
 	theory/booleans/kinds \
 	theory/example/ecdata.h \
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 8780922c9..18b2c42f4 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -21,8 +21,6 @@ OPTIONS_FILES_SRCS = \
 	../theory/arrays/options.h \
 	../theory/quantifiers/options.cpp \
 	../theory/quantifiers/options.h \
-	../theory/rewriterules/options.cpp \
-	../theory/rewriterules/options.h \
 	../theory/strings/options.cpp \
 	../theory/strings/options.h \
 	../prop/options.cpp \
@@ -84,8 +82,6 @@ nodist_liboptions_la_SOURCES = \
 	../theory/arrays/options.h \
 	../theory/quantifiers/options.cpp \
 	../theory/quantifiers/options.h \
-	../theory/rewriterules/options.cpp \
-	../theory/rewriterules/options.h \
 	../theory/strings/options.cpp \
 	../theory/strings/options.h \
 	../prop/options.cpp \
diff --git a/src/prop/options b/src/prop/options
index cf241479c..8bb9d9135 100644
--- a/src/prop/options
+++ b/src/prop/options
@@ -10,7 +10,7 @@ option - --show-sat-solvers void :handler CVC4::prop::showSatSolvers :handler-in
 
 option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate greater_equal(0.0) less_equal(1.0)
  sets the frequency of random decisions in the sat solver (P=0.0 by default)
-option satRandomSeed random-seed --random-seed=S uint32_t :default
+option satRandomSeed random-seed --random-seed=S uint32_t :default :read-write
  sets the random seed for the sat solver
 
 option satVarDecay double :default 0.95 :predicate less_equal(1.0) greater_equal(0.0)
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index 2448898c0..a0777ae70 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -64,7 +64,6 @@ class CVC4_PUBLIC LogicInfo {
     case theory::THEORY_BUILTIN:
     case theory::THEORY_BOOL:
     case theory::THEORY_QUANTIFIERS:
-    case theory::THEORY_REWRITERULES:
       return false;
     default:
       return true;
@@ -117,7 +116,7 @@ public:
   /** Is this a quantified logic? */
   bool isQuantified() const {
     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES);
+    return isTheoryEnabled(theory::THEORY_QUANTIFIERS);
   }
 
   /** Is this the all-inclusive logic? */
@@ -214,7 +213,6 @@ public:
    */
   void enableQuantifiers() {
     enableTheory(theory::THEORY_QUANTIFIERS);
-    enableTheory(theory::THEORY_REWRITERULES);
   }
 
   /**
@@ -222,7 +220,6 @@ public:
    */
   void disableQuantifiers() {
     disableTheory(theory::THEORY_QUANTIFIERS);
-    disableTheory(theory::THEORY_REWRITERULES);
   }
 
   // these are for arithmetic
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a9e77d3d2..08a9f5d9f 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -18,7 +18,6 @@
 #include "theory/theory_engine.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/options.h"
-#include "theory/rewriterules/efficient_e_matching.h"
 #include "theory/quantifiers/theory_quantifiers.h"
 
 using namespace std;
diff --git a/src/theory/rewriterules/efficient_e_matching.cpp b/src/theory/rewriterules/efficient_e_matching.cpp
deleted file mode 100644
index 05934fc8b..000000000
--- a/src/theory/rewriterules/efficient_e_matching.cpp
+++ /dev/null
@@ -1,680 +0,0 @@
-/*********************                                                        */
-/*! \file efficient_e_matching.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  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 theory uf instantiator class
- **/
-
-#include "theory/rewriterules/efficient_e_matching.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
-#include "theory/quantifiers/candidate_generator.h"
-#include "theory/quantifiers/options.h"
-#include "theory/rewriterules/options.h"
-#include "theory/quantifiers/term_database.h"
-
-#include "theory/theory_engine.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::inst;
-
-namespace CVC4 {
-namespace theory {
-
-inline std::ostream& operator<<(std::ostream& out, const EfficientEMatcher::Ips& ips) {
-  return out;
-};
-
-EqClassInfo::EqClassInfo( context::Context* c ) : d_funs( c ), d_pfuns( c ), d_disequal( c ){
-
-}
-
-//set member
-void EqClassInfo::setMember( Node n, quantifiers::TermDb* db ){
-  if( n.hasOperator() ){
-    d_funs.insertAtContextLevelZero(n.getOperator(),true);
-  }
-  //add parent functions
-  for( std::hash_map< Node, std::hash_map< int, std::vector< Node >  >, NodeHashFunction >::iterator it = db->d_parents[n].begin();
-    it != db->d_parents[n].end(); ++it ){
-    //TODO Is it true to do it at level 0? That depend when SetMember is called
-    // At worst it is a good overapproximation
-    d_pfuns.insertAtContextLevelZero( it->first, true);
-  }
-}
-
-//get has function
-bool EqClassInfo::hasFunction( Node op ){
-  return d_funs.find( op )!=d_funs.end();
-}
-
-bool EqClassInfo::hasParent( Node op ){
-  return d_pfuns.find( op )!=d_pfuns.end();
-}
-
-//merge with another eq class info
-void EqClassInfo::merge( EqClassInfo* eci ){
-  for( BoolMap::iterator it = eci->d_funs.begin(); it != eci->d_funs.end(); it++ ) {
-    d_funs[ (*it).first ] = true;
-  }
-  for( BoolMap::iterator it = eci->d_pfuns.begin(); it != eci->d_pfuns.end(); it++ ) {
-    d_pfuns[ (*it).first ] = true;
-  }
-}
-
-inline void outputEqClassInfo( const char* c, const EqClassInfo* eci){
-  Debug(c) << " funs:";
-  for( EqClassInfo::BoolMap::iterator it = eci->d_funs.begin(); it != eci->d_funs.end(); it++ ) {
-    Debug(c) << (*it).first << ",";
-  }
-  Debug(c) << std::endl << "pfuns:";
-  for( EqClassInfo::BoolMap::iterator it = eci->d_pfuns.begin(); it != eci->d_pfuns.end(); it++ ) {
-    Debug(c) << (*it).first << ",";
-  }
-  Debug(c) << std::endl;
-}
-
-
-
-EfficientEMatcher::EfficientEMatcher( CVC4::theory::QuantifiersEngine* qe ) : d_quantEngine( qe )
-{
-
-}
-
-eq::EqualityEngine* EfficientEMatcher::getEqualityEngine(){
-  //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();
-  return d_quantEngine->getMasterEqualityEngine();
-}
-
-/** new node */
-void EfficientEMatcher::newEqClass( TNode n ){
-
-}
-
-void EfficientEMatcher::newTerms(SetNode& s){
-  static NoMatchAttribute rewrittenNodeAttribute;
-  /* op -> nodes (if the set is empty, the op is not interesting) */
-  std::hash_map< TNode, SetNode, TNodeHashFunction > h;
-  /* types -> nodes (if the set is empty, the type is not interesting) */
-  std::hash_map< TypeNode, SetNode, TypeNodeHashFunction > tyh;
-  for(SetNode::iterator i=s.begin(), end=s.end(); i != end; ++i){
-    if (i->getAttribute(rewrittenNodeAttribute)) continue; /* skip it */
-    if( !d_cand_gens.empty() ){
-      // op
-      TNode op = i->getOperator();
-      std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator
-        is = h.find(op);
-      if(is == h.end()){
-        std::pair<std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator,bool>
-          p = h.insert(make_pair(op,SetNode()));
-        is = p.first;
-        if(d_cand_gens.find(op) != d_cand_gens.end()){
-          is->second.insert(*i);
-        } /* else we have inserted an empty set */
-      }else if(!is->second.empty()){
-        is->second.insert(*i);
-      }
-    }
-    if( !d_cand_gen_types.empty() ){
-      //type
-      TypeNode ty = i->getType();
-      std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator
-        is = tyh.find(ty);
-      if(is == tyh.end()){
-        std::pair<std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator,bool>
-          p = tyh.insert(make_pair(ty,SetNode()));
-        is = p.first;
-        if(d_cand_gen_types.find(ty) != d_cand_gen_types.end()){
-          is->second.insert(*i);
-        } /* else we have inserted an empty set */
-      }else if(!is->second.empty()){
-        is->second.insert(*i);
-      }
-    }
-  }
-  //op
-  for(std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator i=h.begin(), end=h.end();
-      i != end; ++i){
-    //new term, add n to candidate generators
-    if(i->second.empty()) continue;
-    std::map< Node, NodeNewTermDispatcher >::iterator
-      inpc = d_cand_gens.find(i->first);
-    //we know that this op exists
-    Assert(inpc != d_cand_gens.end());
-    inpc->second.send(i->second);
-  }
-  //type
-  for(std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator i=tyh.begin(), end=tyh.end();
-      i != end; ++i){
-    //new term, add n to candidate generators
-    if(i->second.empty()) continue;
-    std::map< TypeNode, NodeNewTermDispatcher >::iterator
-      inpc = d_cand_gen_types.find(i->first);
-    //we know that this op exists
-    Assert(inpc != d_cand_gen_types.end());
-    inpc->second.send(i->second);
-  }
-
-}
-
-
-/** merge */
-void EfficientEMatcher::merge( TNode a, TNode b ){
-  if( options::efficientEMatching() ){
-    //merge eqc_ops of b into a
-    EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a );
-    EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( b );
-
-    if( a.getKind()!=IFF && a.getKind()!=EQUAL && b.getKind()!=IFF && b.getKind()!=EQUAL ){
-      Debug("efficient-e-match") << "Merging " << a << " with " << b << std::endl;
-
-      //determine new candidates for instantiation
-      computeCandidatesPcPairs( a, eci_a, b, eci_b );
-      computeCandidatesPcPairs( b, eci_b, a, eci_a );
-      computeCandidatesPpPairs( a, eci_a, b, eci_b );
-      computeCandidatesPpPairs( b, eci_b, a, eci_a );
-    }
-    computeCandidatesConstants( a, eci_a, b, eci_b);
-    computeCandidatesConstants( b, eci_b, a, eci_a);
-
-    eci_a->merge( eci_b );
-  }
-}
-
-/** assert terms are disequal */
-void EfficientEMatcher::assertDisequal( TNode a, TNode b, TNode reason ){
-
-}
-
-EqClassInfo* EfficientEMatcher::getEquivalenceClassInfo( Node n ) {
-  return d_eqc_ops.find( n )==d_eqc_ops.end() ? NULL : d_eqc_ops[n];
-}
-EqClassInfo* EfficientEMatcher::getOrCreateEquivalenceClassInfo( Node n ){
-  Assert( n==getEqualityEngine()->getRepresentative( n ) );
-  if( d_eqc_ops.find( n )==d_eqc_ops.end() ){
-    EqClassInfo* eci = new EqClassInfo( d_quantEngine->getSatContext() );
-    eci->setMember( n, d_quantEngine->getTermDatabase() );
-    d_eqc_ops[n] = eci;
-  }
-  return d_eqc_ops[n];
-}
-
-void EfficientEMatcher::computeCandidatesPcPairs( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){
-  Debug("efficient-e-match") << "Compute candidates for pc pairs..." << std::endl;
-  Debug("efficient-e-match") << "  Eq class = [";
-  outputEqClass( "efficient-e-match", a);
-  Debug("efficient-e-match") << "]" << std::endl;
-  outputEqClassInfo("efficient-e-match",eci_a);
-  for( EqClassInfo::BoolMap::iterator it = eci_a->d_funs.begin(); it != eci_a->d_funs.end(); it++ ) {
-    //the child function:  a member of eq_class( a ) has top symbol g, in other words g is in funs( a )
-    Node g = (*it).first;
-    Debug("efficient-e-match") << "  Checking application " << g << std::endl;
-    //look at all parent/child pairs
-    for( std::map< Node, std::vector< std::pair< NodePcDispatcher*, Ips > > >::iterator itf = d_pc_pairs[g].begin();
-         itf != d_pc_pairs[g].end(); ++itf ){
-      //f/g is a parent/child pair
-      Node f = itf->first;
-      if( eci_b->hasParent( f ) ){
-        //DO_THIS: determine if f in pfuns( b ), only do the follow if so
-        Debug("efficient-e-match") << "    Checking parent application " << f << std::endl;
-        //scan through the list of inverted path strings/candidate generators
-        for( std::vector< std::pair< NodePcDispatcher*, Ips > >::iterator cit = itf->second.begin();
-             cit != itf->second.end(); ++cit ){
-#ifdef CVC4_DEBUG
-          Debug("efficient-e-match") << "      Checking pattern " << cit->first->pat << std::endl;
-#endif
-          Debug("efficient-e-match") << "          Check inverted path string for pattern ";
-          outputIps( "efficient-e-match", cit->second );
-          Debug("efficient-e-match") << std::endl;
-
-          //collect all new relevant terms
-          SetNode terms;
-          terms.insert( b );
-          collectTermsIps( cit->second, terms );
-          if( terms.empty() ) continue;
-          Debug("efficient-e-match") << "        -> Added terms (" << terms.size() << "): ";
-          for( SetNode::const_iterator t=terms.begin(), end=terms.end();
-               t!=end; ++t ){
-            Debug("efficient-e-match") << (*t) << " ";
-          }
-          Debug("efficient-e-match") << std::endl;
-          //add them as candidates to the candidate generator
-          cit->first->send(terms);
-        }
-      }
-    }
-  }
-}
-
-void EfficientEMatcher::computeCandidatesPpPairs( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){
-  Debug("efficient-e-match") << "Compute candidates for pp pairs..." << std::endl;
-  for( std::map< Node, std::map< Node, std::vector< triple< NodePpDispatcher*, Ips, Ips > > > >::iterator it = d_pp_pairs.begin();
-       it != d_pp_pairs.end(); ++it ){
-    Node f = it->first;
-    if( eci_a->hasParent( f ) ){
-      Debug("efficient-e-match") << "  Checking parent application " << f << std::endl;
-      for( std::map< Node, std::vector< triple<NodePpDispatcher*, Ips, Ips> > >::iterator it2 = it->second.begin();
-           it2 != it->second.end(); ++it2 ){
-        Node g = it2->first;
-        if( eci_b->hasParent( g ) ){
-          Debug("efficient-e-match") << "    Checking parent application " << g << std::endl;
-          //if f in pfuns( a ) and g is in pfuns( b ), only do the follow if so
-          for( std::vector< triple<NodePpDispatcher*, Ips, Ips> > ::iterator cit = it2->second.begin();
-               cit != it2->second.end(); ++cit ){
-#ifdef CVC4_DEBUG
-            Debug("efficient-e-match") << "    Checking pattern " << cit->first->pat1 << " and " << cit->first->pat2 << std::endl;
-#endif
-            Debug("efficient-e-match") << "          Check inverted path string ";
-            outputIps( "efficient-e-match", cit->second );
-            SetNode a_terms;
-            a_terms.insert( a );
-            collectTermsIps( cit->second, a_terms );
-            if( a_terms.empty() ) continue;
-            Debug("efficient-e-match") << "          And check inverted path string ";
-            outputIps( "efficient-e-match", cit->third );
-            SetNode b_terms;
-            b_terms.insert( b );
-            collectTermsIps( cit->third, b_terms );
-            if( b_terms.empty() ) continue;
-            //Start debug
-            Debug("efficient-e-match") << "        -> Possibly Added termsA (" << a_terms.size() << "): ";
-            for( SetNode::const_iterator t=a_terms.begin(), end=a_terms.end();
-                 t!=end; ++t ){
-              Debug("efficient-e-match") << (*t) << " ";
-            }
-            Debug("efficient-e-match") << std::endl;
-            Debug("efficient-e-match") << "        -> Possibly Added termsB (" << b_terms.size() << "): ";
-            for( SetNode::const_iterator t=b_terms.begin(), end=b_terms.end();
-                 t!=end; ++t ){
-              Debug("efficient-e-match") << (*t) << " ";
-            }
-            Debug("efficient-e-match") << std::endl;
-            //End debug
-
-            cit->first->send(a_terms,b_terms);
-          }
-        }
-      }
-    }
-  }
-}
-
-
-void EfficientEMatcher::computeCandidatesConstants( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){
-  Debug("efficient-e-match") << "Compute candidates constants for cc pairs..." << std::endl;
-  Debug("efficient-e-match") << "  Eq class = [";
-  outputEqClass( "efficient-e-match", a);
-  Debug("efficient-e-match") << "]" << std::endl;
-  outputEqClassInfo("efficient-e-match",eci_a);
-  for( std::map< Node, std::map< Node, NodePcDispatcher* > >::iterator
-         it = d_cc_pairs.begin(), end = d_cc_pairs.end();
-       it != end; ++it ) {
-    Debug("efficient-e-match") << "  Checking application " << it->first << std::endl;
-    if( !eci_b->hasFunction(it->first) ) continue;
-    for( std::map< Node, NodePcDispatcher* >::iterator
-           itc = it->second.begin(), end = it->second.end();
-       itc != end; ++itc ) {
-      //The constant
-      Debug("efficient-e-match") << "    Checking constant " << a << std::endl;
-      if(getEqualityEngine()->getRepresentative(itc->first) != a) continue;
-      SetNode s;
-      eq::EqClassIterator eqc_iter( b, getEqualityEngine() );
-      while( !eqc_iter.isFinished() ){
-        Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
-                                         << std::endl;
-        if( (*eqc_iter).hasOperator() && (*eqc_iter).getOperator() == it->first ) s.insert(*eqc_iter);
-        eqc_iter++;
-      }
-
-      if( s.empty() ) continue;
-      Debug("efficient-e-match") << "        -> Added terms (" << s.size() << "): ";
-      for( SetNode::const_iterator t=s.begin(), end=s.end();
-           t!=end; ++t ){
-        Debug("efficient-e-match") << (*t) << " ";
-      }
-      Debug("efficient-e-match") << std::endl;
-      itc->second->send(s);
-    }
-  }
-}
-
-void EfficientEMatcher::collectTermsIps( Ips& ips, SetNode & terms ){
-  Assert( ips.size() > 0);
-  return collectTermsIps( ips, terms,  ips.size() - 1);
-}
-
-void EfficientEMatcher::collectTermsIps( Ips& ips, SetNode& terms, int index ){
-  if( !terms.empty() ){
-    Debug("efficient-e-match-debug") << "> Process " << index << std::endl;
-    Node f = ips[index].first;
-    int arg = ips[index].second;
-
-    //for each term in terms, determine if any term (modulo equality) has parent "f" from position "arg"
-    bool addRep = ( index!=0 ); // We want to keep the top symbol for the last
-    SetNode newTerms;
-    for( SetNode::const_iterator t=terms.begin(), end=terms.end();
-         t!=end; ++t ){
-      collectParentsTermsIps( *t, f, arg, newTerms, addRep );
-    }
-    terms.swap(newTerms);
-
-    Debug("efficient-e-match-debug") << "> Terms are now: ";
-    for( SetNode::const_iterator t=terms.begin(), end=terms.end();
-         t!=end; ++t ){
-      Debug("efficient-e-match-debug") << *t << " ";
-    }
-    Debug("efficient-e-match-debug") << std::endl;
-
-    if(index!=0) collectTermsIps( ips, terms, index-1 );
-  }
-}
-
-bool EfficientEMatcher::collectParentsTermsIps( Node n, Node f, int arg, SetNode & terms, bool addRep, bool modEq ){ //modEq default true
-  bool addedTerm = false;
-
-  if( modEq && getEqualityEngine()->hasTerm( n )){
-    Assert( getEqualityEngine()->getRepresentative( n )==n );
-    //collect modulo equality
-    //DO_THIS: this should (if necessary) compute a current set of (f, arg) parents for n and cache it
-    eq::EqClassIterator eqc_iter( n, getEqualityEngine() );
-    while( !eqc_iter.isFinished() ){
-      Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
-                                       << std::endl;
-      if( collectParentsTermsIps( (*eqc_iter), f, arg, terms, addRep, false ) ){
-        //if only one argument, we know we can stop (since all others added will be congruent)
-        if( f.getType().getNumChildren()==2 ){
-          return true;
-        }
-        addedTerm = true;
-      }
-      eqc_iter++;
-    }
-  }else{
-    quantifiers::TermDb* db = d_quantEngine->getTermDatabase();
-    //see if parent f exists from argument arg
-    const std::vector<Node> & parents = db->getParents(n,f,arg);
-    for( size_t i=0; i<parents.size(); ++i ){
-      TNode t = parents[i];
-      if(!CandidateGenerator::isLegalCandidate(t)) continue;
-      if( addRep ) t = getEqualityEngine()->getRepresentative( t );
-      terms.insert(t);
-      addedTerm = true;
-    }
-  }
-  return addedTerm;
-}
-
-void EfficientEMatcher::registerPatternElementPairs2( Node pat, Ips& ips, PpIpsMap & pp_ips_map, NodePcDispatcher* npc ){
-  Assert( pat.hasOperator() );
-  //add information for possible pp-pair
-  ips.push_back( std::pair< Node, int >( pat.getOperator(), 0 ) ); //0 is just a dumb value
-
-  for( int i=0; i<(int)pat.getNumChildren(); i++ ){
-    if( pat[i].getKind()==INST_CONSTANT ){
-      ips.back().second = i;
-      pp_ips_map[ pat[i] ].push_back( make_pair( pat.getOperator(), Ips( ips ) ) );
-    }
-  }
-
-  for( int i=0; i<(int)pat.getNumChildren(); i++ ){
-    if( pat[i].getKind()==APPLY_UF ){
-      ips.back().second = i;
-      registerPatternElementPairs2( pat[i], ips, pp_ips_map, npc );
-      Debug("pattern-element-opt") << "Found pc-pair ( " << pat.getOperator() << ", " << pat[i].getOperator() << " )" << std::endl;
-      Debug("pattern-element-opt") << "   Path = ";
-      outputIps( "pattern-element-opt", ips );
-      Debug("pattern-element-opt") << std::endl;
-      //pat.getOperator() and pat[i].getOperator() are a pc-pair
-      d_pc_pairs[ pat[i].getOperator() ][ pat.getOperator() ]
-        .push_back( make_pair(npc,Ips(ips)) );
-    }
-  }
-  ips.pop_back();
-}
-
-void EfficientEMatcher::registerPatternElementPairs( Node pat, PpIpsMap & pp_ips_map,
-                                                     NodePcDispatcher* npc,
-                                                     NodePpDispatcher* npp){
-  Ips ips;
-  registerPatternElementPairs2( pat, ips, pp_ips_map, npc );
-  for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
-    // for each variable construct all the pp-pair
-    for( size_t j=0; j<it->second.size(); j++ ){
-      for( size_t k=j+1; k<it->second.size(); k++ ){
-        //found a pp-pair
-        Debug("pattern-element-opt") << "Found pp-pair ( " << it->second[j].first << ", " << it->second[k].first << " )" << std::endl;
-        Debug("pattern-element-opt") << "   Paths = ";
-        outputIps( "pattern-element-opt", it->second[j].second );
-        Debug("pattern-element-opt") << " and ";
-        outputIps( "pattern-element-opt", it->second[k].second );
-        Debug("pattern-element-opt") << std::endl;
-        d_pp_pairs[ it->second[j].first ][ it->second[k].first ]
-          .push_back( make_triple( npp, it->second[j].second, it->second[k].second ));
-      }
-    }
-  }
-};
-
-void findPpSite(Node pat, EfficientEMatcher::Ips& ips, EfficientEMatcher::PpIpsMap & pp_ips_map){
-  Assert( pat.getKind()==APPLY_UF );
-  //add information for possible pp-pair
-
-  ips.push_back( make_pair( pat.getOperator(), 0) );
-  for( size_t i=0; i<pat.getNumChildren(); i++ ){
-    if( pat[i].getKind()==INST_CONSTANT ){
-      ips.back().second = i;
-      pp_ips_map[ pat[i] ].push_back( make_pair( pat.getOperator(), EfficientEMatcher::Ips( ips ) ) );
-    }
-  }
-
-  for( size_t i=0; i<pat.getNumChildren(); i++ ){
-    if( pat[i].getKind()==APPLY_UF ){
-      ips.back().second = i;
-      findPpSite( pat[i], ips, pp_ips_map );
-    }
-  }
-  ips.pop_back();
-}
-
-void EfficientEMatcher::combineMultiPpIpsMap(PpIpsMap & pp_ips_map, MultiPpIpsMap & multi_pp_ips_map,
-                                                EfficientHandler& eh, size_t index2,const std::vector<Node> & pats){
-  hash_map<size_t,NodePpDispatcher*> npps;
-  for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
-    MultiPpIpsMap::iterator mit = multi_pp_ips_map.find(it->first);
-    if(mit == multi_pp_ips_map.end()) continue;
-    // for each variable construct all the pp-pair
-    // j the last pattern treated
-    for( std::vector< std::pair< Node, Ips > >::iterator j=it->second.begin(), jend = it->second.end() ;
-         j != jend; ++j){
-      // k one of the previous one
-      for( std::vector< triple< size_t, Node, Ips > >::iterator k=mit->second.begin(), kend = mit->second.end() ;
-           k != kend; ++k){
-        //found a pp-pair
-        Debug("pattern-element-opt") << "Found multi-pp-pair ( " << j->first
-                                     << ", " << k->second << " in "<< k->first
-                                     << " )" << std::endl;
-        Debug("pattern-element-opt") << "   Paths = ";
-        outputIps( "pattern-element-opt", j->second );
-        Debug("pattern-element-opt") << " and ";
-        outputIps( "pattern-element-opt", k->third );
-        Debug("pattern-element-opt") << std::endl;
-        NodePpDispatcher* dispatcher;
-        hash_map<size_t,NodePpDispatcher*>::iterator inpp = npps.find(k->first);
-        if( inpp != npps.end() ) dispatcher = inpp->second;
-        else{
-          dispatcher = new NodePpDispatcher();
-#ifdef CVC4_DEBUG
-          dispatcher->pat1 = pats[index2];
-          dispatcher->pat2 = pats[k->first];
-#endif
-          dispatcher->addPpDispatcher(&eh,index2,k->first);
-        };
-        d_pp_pairs[ j->first ][ k->second ].push_back( make_triple( dispatcher, j->second, k->third ));
-      }
-    }
-  }
-
-  /** Put pp_ips_map to multi_pp_ips_map */
-  for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
-    for( std::vector< std::pair< Node, Ips > >::iterator j=it->second.begin(), jend = it->second.end() ;
-         j != jend; ++j){
-      multi_pp_ips_map[it->first].push_back(make_triple(index2, j->first, j->second));
-    }
-  }
-
-}
-
-
-void EfficientEMatcher::registerEfficientHandler( EfficientHandler& handler,
-                                                     const std::vector< Node > & pats ){
-  Assert(pats.size() > 0);
-
-  MultiPpIpsMap multi_pp_ips_map;
-  PpIpsMap pp_ips_map;
-  //In a multi-pattern Pattern that is only a variable are specials,
-  //if the variable appears in another pattern, it can be discarded.
-  //Otherwise new term of this term can be candidate. So we stock them
-  //here before adding them.
-  std::vector< size_t > patVars;
-
-  Debug("pattern-element-opt") << "Register patterns" << pats << std::endl;
-  for(size_t i = 0; i < pats.size(); ++i){
-    if( pats[i].getKind() == kind::INST_CONSTANT){
-      patVars.push_back(i);
-      continue;
-    }
-    //to complete
-    if( pats[i].getKind() == kind::NOT && pats[i][0].getKind() == kind::EQUAL){
-      Node cst = NodeManager::currentNM()->mkConst<bool>(false);
-      TNode op = pats[i][0].getOperator();
-      if(d_cc_pairs[op][cst] == NULL){
-        d_cc_pairs[op][cst] = new NodePcDispatcher();
-      }
-      d_cc_pairs[op][cst]->addPcDispatcher(&handler,i);
-      continue;
-    }
-    //end to complete
-    Debug("pattern-element-opt") << " Register candidate generator..." << pats[i] << std::endl;
-    /* Has the pattern already been seen */
-    if( d_pat_cand_gens.find( pats[i] )==d_pat_cand_gens.end() ){
-      NodePcDispatcher* npc = new NodePcDispatcher();
-      NodePpDispatcher* npp = new NodePpDispatcher();
-#ifdef CVC4_DEBUG
-      npc->pat = pats[i];
-      npp->pat1 = pats[i];
-      npp->pat2 = pats[i];
-#endif
-      d_pat_cand_gens[pats[i]] = make_pair(npc,npp);
-      registerPatternElementPairs( pats[i], pp_ips_map, npc, npp );
-    }else{
-      Ips ips;
-      findPpSite(pats[i],ips,pp_ips_map);
-    }
-    //Has the top operator already been seen */
-    TNode op = pats[i].getOperator();
-    d_pat_cand_gens[pats[i]].first->addPcDispatcher(&handler,i);
-    d_pat_cand_gens[pats[i]].second->addPpDispatcher(&handler,i,i);
-    d_cand_gens[op].addNewTermDispatcher(&handler,i);
-
-    combineMultiPpIpsMap(pp_ips_map,multi_pp_ips_map,handler,i,pats);
-
-    pp_ips_map.clear();
-  }
-
-  for(size_t i = 0; i < patVars.size(); ++i){
-    TNode var = pats[patVars[i]];
-    Assert( var.getKind() == kind::INST_CONSTANT );
-    if( multi_pp_ips_map.find(var) != multi_pp_ips_map.end() ){
-      //The variable appear in another pattern, skip it
-      continue;
-    };
-    d_cand_gen_types[var.getType()].addNewTermDispatcher(&handler,patVars[i]);
-  }
-
-  //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 = new GenericCandidateGeneratorClasses(d_quantEngine);
-    cg->reset(Node::null());
-    TNode c;
-    SetNode ele;
-    while( !(c = cg->getNextCandidate()).isNull() ){
-      if( c.getType() == ty ) ele.insert(c);
-    }
-    if( !ele.empty() ){
-      if(Debug.isOn("efficient-e-match-stats")){
-        Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
-      }
-      handler.addMonoCandidate(ele, 0);
-    }
-
-  } else if( pats[0].getKind() == kind::NOT && pats[0][0].getKind() == kind::EQUAL){
-    Node cst = NodeManager::currentNM()->mkConst<bool>(false);
-    TNode op = pats[0][0].getOperator();
-    cst = getEqualityEngine()->getRepresentative(cst);
-    SetNode ele;
-    eq::EqClassIterator eqc_iter( cst, getEqualityEngine() );
-    while( !eqc_iter.isFinished() ){
-      Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
-                                       << std::endl;
-      if( (*eqc_iter).hasOperator() && (*eqc_iter).getOperator() == op ) ele.insert(*eqc_iter);
-      eqc_iter++;
-    }
-    if( !ele.empty() ){
-      if(Debug.isOn("efficient-e-match-stats")){
-        Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
-      }
-      handler.addMonoCandidate(ele, 0);
-    }
-
-  } else {
-    TermDb* db = d_quantEngine->getTermDatabase();
-    Node op = db->getOperator( pats[0] );
-    if(db->d_op_map[op].begin() != db->d_op_map[op].end()){
-      SetNode ele;
-      ele.insert(db->d_op_map[op].begin(), db->d_op_map[op].end());
-      if(Debug.isOn("efficient-e-match-stats")){
-        Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
-      }
-      handler.addMonoCandidate(ele, 0);
-    }
-  }
-  Debug("efficient-e-match") << "Done." << std::endl;
-}
-
-void EfficientEMatcher::outputEqClass( const char* c, Node n ){
-  if( getEqualityEngine()->hasTerm( n ) ){
-    eq::EqClassIterator eqc_iter( getEqualityEngine()->getRepresentative( n ),
-                                  getEqualityEngine() );
-    bool firstTime = true;
-    while( !eqc_iter.isFinished() ){
-      if( !firstTime ){ Debug(c) << ", "; }
-      Debug(c) << (*eqc_iter);
-      firstTime = false;
-      eqc_iter++;
-    }
-  }else{
-    Debug(c) << n;
-  }
-}
-
-void EfficientEMatcher::outputIps( const char* c, Ips& ips ){
-  for( int i=0; i<(int)ips.size(); i++ ){
-    if( i>0 ){ Debug( c ) << "."; }
-    Debug( c ) << ips[i].first << "." << ips[i].second;
-  }
-}
-
-
-} /* namespace theory */
-} /* namespace cvc4 */
diff --git a/src/theory/rewriterules/efficient_e_matching.h b/src/theory/rewriterules/efficient_e_matching.h
deleted file mode 100644
index b02d465fc..000000000
--- a/src/theory/rewriterules/efficient_e_matching.h
+++ /dev/null
@@ -1,450 +0,0 @@
-/*********************                                                        */
-/*! \file efficient_e_matching.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief efficient e-matching
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__EFFICIENT_E_MATCHING_H
-#define __CVC4__EFFICIENT_E_MATCHING_H
-
-#include "expr/node.h"
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "context/cdchunk_list.h"
-
-#include "util/statistics_registry.h"
-#include "util/ntuple.h"
-#include "context/cdqueue.h"
-#include "context/cdo.h"
-
-#include "theory/uf/equality_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-class QuantifiersEngine;
-
-namespace quantifiers{
-  class TermDb;
-}
-
-class EfficientEMatcher;
-class HandlerPcDispatcher;
-class HandlerPpDispatcher;
-
-typedef std::set<Node> SetNode;
-
-template<class T>
-class CleanUpPointer{
-public:
-  inline void operator()(T** e){
-    delete(*e);
-  };
-};
-
-class EfficientHandler{
-public:
-  typedef std::pair< Node, size_t > MonoCandidate;
-  typedef std::pair< MonoCandidate, MonoCandidate > MultiCandidate;
-  typedef std::pair< SetNode, size_t > MonoCandidates;
-  typedef std::pair< MonoCandidates, MonoCandidates > MultiCandidates;
-private:
-  /* Queue of candidates */
-  typedef context::CDQueue< MonoCandidates *, CleanUpPointer<MonoCandidates> > MonoCandidatesQueue;
-  typedef context::CDQueue< MultiCandidates *, CleanUpPointer<MultiCandidates> > MultiCandidatesQueue;
-  MonoCandidatesQueue d_monoCandidates;
-  typedef SetNode::iterator SetNodeIter;
-  context::CDO<SetNodeIter> d_si;
-  context::CDO<bool> d_mono_not_first;
-
-  MonoCandidatesQueue d_monoCandidatesNewTerm;
-  context::CDO<SetNodeIter> d_si_new_term;
-  context::CDO<bool> d_mono_not_first_new_term;
-
-
-  MultiCandidatesQueue d_multiCandidates;
-  context::CDO<SetNodeIter> d_si1;
-  context::CDO<SetNodeIter> d_si2;
-  context::CDO<bool> d_multi_not_first;
-
-
-  friend class EfficientEMatcher;
-  friend class HandlerPcDispatcher;
-  friend class HandlerPpDispatcher;
-  friend class HandlerNewTermDispatcher;
-protected:
-  void addMonoCandidate(SetNode & s, size_t index){
-    Assert(!s.empty());
-    d_monoCandidates.push(new MonoCandidates(s,index));
-  }
-  void addMonoCandidateNewTerm(SetNode & s, size_t index){
-    Assert(!s.empty());
-    d_monoCandidatesNewTerm.push(new MonoCandidates(s,index));
-  }
-  void addMultiCandidate(SetNode & s1, size_t index1, SetNode & s2, size_t index2){
-    Assert(!s1.empty() && !s2.empty());
-    d_multiCandidates.push(new MultiCandidates(MonoCandidates(s1,index1),
-                                               MonoCandidates(s2,index2)));
-  }
-public:
-  EfficientHandler(context::Context * c):
-    //false for d_mono_not_first beacause its the default constructor
-    d_monoCandidates(c), d_si(c), d_mono_not_first(c,false),
-    d_monoCandidatesNewTerm(c), d_si_new_term(c),
-    d_mono_not_first_new_term(c,false),
-    d_multiCandidates(c) , d_si1(c), d_si2(c), d_multi_not_first(c,false) {};
-
-  bool getNextMonoCandidate(MonoCandidate & candidate){
-    if(d_monoCandidates.empty()) return false;
-    const MonoCandidates * front = d_monoCandidates.front();
-    SetNodeIter si_tmp;
-    if(!d_mono_not_first){
-      Assert(front->first.begin() != front->first.end());
-      d_mono_not_first = true;
-      si_tmp=front->first.begin();
-    }else{
-      si_tmp = d_si;
-      ++si_tmp;
-    };
-    if(si_tmp != front->first.end()){
-      candidate.first = (*si_tmp);
-      candidate.second = front->second;
-      d_si = si_tmp;
-      Debug("efficienthandler") << "Mono produces " << candidate.first << " for " << candidate.second << std::endl;
-      return true;
-    };
-    d_monoCandidates.pop();
-    d_mono_not_first = false;
-    return getNextMonoCandidate(candidate);
-  };
-
-  bool getNextMonoCandidateNewTerm(MonoCandidate & candidate){
-    if(d_monoCandidatesNewTerm.empty()) return false;
-    const MonoCandidates * front = d_monoCandidatesNewTerm.front();
-    SetNodeIter si_tmp;
-    if(!d_mono_not_first_new_term){
-      Assert(front->first.begin() != front->first.end());
-      d_mono_not_first_new_term = true;
-      si_tmp=front->first.begin();
-    }else{
-      si_tmp = d_si_new_term;
-      ++si_tmp;
-    };
-    if(si_tmp != front->first.end()){
-      candidate.first = (*si_tmp);
-      candidate.second = front->second;
-      d_si_new_term = si_tmp;
-      Debug("efficienthandler") << "Mono produces " << candidate.first << " for " << candidate.second << std::endl;
-      return true;
-    };
-    d_monoCandidatesNewTerm.pop();
-    d_mono_not_first_new_term = false;
-    return getNextMonoCandidateNewTerm(candidate);
-  };
-
-  bool getNextMultiCandidate(MultiCandidate & candidate){
-    if(d_multiCandidates.empty()) return false;
-    const MultiCandidates* front = d_multiCandidates.front();
-    SetNodeIter si1_tmp;
-    SetNodeIter si2_tmp;
-    if(!d_multi_not_first){
-      Assert(front->first.first.begin() != front->first.first.end());
-      Assert(front->second.first.begin() != front->second.first.end());
-      si1_tmp = front->first.first.begin();
-      si2_tmp = front->second.first.begin();
-    }else{
-      si1_tmp = d_si1;
-      si2_tmp = d_si2;
-      ++si2_tmp;
-    };
-    if(si2_tmp != front->second.first.end()){
-      candidate.first.first = *si1_tmp;
-      candidate.first.second = front->first.second;
-      candidate.second.first = *si2_tmp;
-      candidate.second.second = front->second.second;
-      if(!d_multi_not_first){d_si1 = si1_tmp; d_multi_not_first = true; };
-      d_si2 = si2_tmp;
-      Debug("efficienthandler") << "Multi1 produces "
-                                << candidate.first.first << " for "
-                                << candidate.first.second << " and "
-                                << candidate.second.first << " for "
-                                << candidate.second.second << " and "
-                                << std::endl;
-      return true;
-    }; // end of the second set
-    si2_tmp = front->second.first.begin();
-    ++si1_tmp;
-    if(si1_tmp != front->first.first.end()){
-      candidate.first.first = *si1_tmp;
-      candidate.first.second = front->first.second;
-      candidate.second.first = *si2_tmp;
-      candidate.second.second = front->second.second;
-      d_si1 = si1_tmp;
-      d_si2 = si2_tmp;
-      Debug("efficienthandler") << "Multi2 produces "
-                                << candidate.first.first << " for "
-                                << candidate.first.second << " and "
-                                << candidate.second.first << " for "
-                                << candidate.second.second << " and "
-                                << std::endl;
-      return true;
-    }; // end of the first set
-    d_multiCandidates.pop();
-    d_multi_not_first = false;
-    return getNextMultiCandidate(candidate);
-  }
-};
-
-class PcDispatcher{
-public:
-  virtual ~PcDispatcher(){};
-  /* Send the node to the dispatcher */
-  virtual void send(SetNode & s) = 0;
-};
-
-
-class HandlerPcDispatcher: public PcDispatcher{
-  EfficientHandler* d_handler;
-  size_t d_index;
-public:
-  HandlerPcDispatcher(EfficientHandler* handler, size_t index):
-    d_handler(handler), d_index(index) {};
-  void send(SetNode & s){
-    d_handler->addMonoCandidate(s,d_index);
-  }
-};
-
-
-/** All the dispatcher that correspond to this node */
-class NodePcDispatcher: public PcDispatcher{
-#ifdef CVC4_DEBUG
-public:
-  Node pat;
-#endif/* CVC4_DEBUG*/
-private:
-  std::vector<HandlerPcDispatcher> d_dis;
-public:
-  void send(SetNode & s){
-    Assert(!s.empty());
-    for(std::vector<HandlerPcDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
-        i != end; ++i){
-      (*i).send(s);
-    }
-  }
-  void addPcDispatcher(EfficientHandler* handler, size_t index){
-    d_dis.push_back(HandlerPcDispatcher(handler,index));
-  }
-};
-
-
-class HandlerNewTermDispatcher: public PcDispatcher{
-  EfficientHandler* d_handler;
-  size_t d_index;
-public:
-  HandlerNewTermDispatcher(EfficientHandler* handler, size_t index):
-    d_handler(handler), d_index(index) {};
-  void send(SetNode & s){
-    d_handler->addMonoCandidateNewTerm(s,d_index);
-  }
-};
-
-/** All the dispatcher that correspond to this node */
-class NodeNewTermDispatcher: public PcDispatcher{
-#ifdef CVC4_DEBUG
-public:
-  Node pat;
-#endif/* CVC4_DEBUG*/
-private:
-  std::vector<HandlerNewTermDispatcher> d_dis;
-public:
-  void send(SetNode & s){
-    Assert(!s.empty());
-    for(std::vector<HandlerNewTermDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
-        i != end; ++i){
-      (*i).send(s);
-    }
-  }
-  void addNewTermDispatcher(EfficientHandler* handler, size_t index){
-    d_dis.push_back(HandlerNewTermDispatcher(handler,index));
-  }
-};
-
-class PpDispatcher{
-public:
-  virtual ~PpDispatcher(){};
-  /* Send the node to the dispatcher */
-  virtual void send(SetNode & s1, SetNode & s2, SetNode & sinter) = 0;
-};
-
-
-class HandlerPpDispatcher: public PpDispatcher{
-  EfficientHandler* d_handler;
-  size_t d_index1;
-  size_t d_index2;
-public:
-  HandlerPpDispatcher(EfficientHandler* handler, size_t index1, size_t index2):
-    d_handler(handler), d_index1(index1), d_index2(index2) {};
-  void send(SetNode & s1, SetNode & s2, SetNode & sinter){
-    if(d_index1 == d_index2){
-      if(!sinter.empty())
-        d_handler->addMonoCandidate(sinter,d_index1);
-    }else{
-      d_handler->addMultiCandidate(s1,d_index1,s2,d_index2);
-    }
-  }
-};
-
-
-/** All the dispatcher that correspond to this node */
-class NodePpDispatcher: public PpDispatcher{
-#ifdef CVC4_DEBUG
-public:
-  Node pat1;
-  Node pat2;
-#endif/* CVC4_DEBUG */
-private:
-  std::vector<HandlerPpDispatcher> d_dis;
-  void send(SetNode & s1, SetNode & s2, SetNode & inter){
-    for(std::vector<HandlerPpDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
-        i != end; ++i){
-      (*i).send(s1,s2,inter);
-    }
-  }
-public:
-  void send(SetNode & s1, SetNode & s2){
-    // can be done in HandlerPpDispatcher lazily
-    Assert(!s1.empty() && !s2.empty());
-    SetNode inter;
-    std::set_intersection( s1.begin(), s1.end(), s2.begin(), s2.end(),
-                           std::inserter( inter, inter.begin() ) );
-    send(s1,s2,inter);
-  }
-  void addPpDispatcher(EfficientHandler* handler, size_t index1, size_t index2){
-    d_dis.push_back(HandlerPpDispatcher(handler,index1,index2));
-  }
-};
-
-//equivalence class info
-class EqClassInfo
-{
-public:
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
-  typedef context::CDChunkList<Node> NodeList;
-public:
-  //a list of operators that occur as top symbols in this equivalence class
-  //  Efficient E-Matching for SMT Solvers: "funs"
-  BoolMap d_funs;
-  //a list of operators f for which a term of the form f( ... t ... ) exists
-  //  Efficient E-Matching for SMT Solvers: "pfuns"
-  BoolMap d_pfuns;
-  //a list of equivalence classes that are disequal
-  BoolMap d_disequal;
-public:
-  EqClassInfo( context::Context* c );
-  ~EqClassInfo(){}
-  //set member
-  void setMember( Node n, quantifiers::TermDb* db );
-  //has function "funs"
-  bool hasFunction( Node op );
-  //has parent "pfuns"
-  bool hasParent( Node op );
-  //merge with another eq class info
-  void merge( EqClassInfo* eci );
-};
-
-class EfficientEMatcher{
-protected:
-  /** reference to the quantifiers engine */
-  QuantifiersEngine* d_quantEngine;
-public:
-  EfficientEMatcher(CVC4::theory::QuantifiersEngine* qe);
-  ~EfficientEMatcher() {
-    for(std::map< Node, std::pair<NodePcDispatcher*, NodePpDispatcher*> >::iterator
-          i = d_pat_cand_gens.begin(), end = d_pat_cand_gens.end();
-        i != end; i++){
-      delete(i->second.first);
-      delete(i->second.second);
-    }
-  }
-  /** get equality engine we are using */
-  eq::EqualityEngine* getEqualityEngine();
-private:
-  //information for each equivalence class
-  std::map< Node, EqClassInfo* > d_eqc_ops;
-public:
-  /** new node */
-  void newEqClass( TNode n );
-  /** merge */
-  void merge( TNode a, TNode b );
-  /** assert terms are disequal */
-  void assertDisequal( TNode a, TNode b, TNode reason );
-  /** get equivalence class info */
-  EqClassInfo* getEquivalenceClassInfo( Node n );
-  EqClassInfo* getOrCreateEquivalenceClassInfo( Node n );
-  typedef std::vector< std::pair< Node, int > > Ips;
-  typedef std::map< Node, std::vector< std::pair< Node, Ips > > > PpIpsMap;
-  typedef std::map< Node, std::vector< triple< size_t, Node, Ips > > > MultiPpIpsMap;
-private:
-  /** Parent/Child Pairs (for efficient E-matching)
-      So, for example, if we have the pattern f( g( x ) ), then d_pc_pairs[g][f][f( g( x ) )] = { f.0 }.
-  */
-  std::map< Node, std::map< Node, std::vector< std::pair< NodePcDispatcher*, Ips > > > > d_pc_pairs;
-  /** Parent/Parent Pairs (for efficient E-matching) */
-  std::map< Node, std::map< Node, std::vector< triple< NodePpDispatcher*, Ips, Ips > > > > d_pp_pairs;
-  /** Constants/Child Pairs
-      So, for example, if we have the pattern f( x ) = c, then d_pc_pairs[f][c] = ..., pcdispatcher, ...
-  */
-  //TODO constant in pattern can use the same thing just add an Ips
-  std::map< Node, std::map< Node, NodePcDispatcher* > > d_cc_pairs;
-  /** list of all candidate generators for each operator */
-  std::map< Node, NodeNewTermDispatcher > d_cand_gens;
-  /** list of all candidate generators for each type */
-  std::map< TypeNode, NodeNewTermDispatcher > d_cand_gen_types;
-  /** map from patterns to candidate generators */
-  std::map< Node, std::pair<NodePcDispatcher*, NodePpDispatcher*> > d_pat_cand_gens;
-  /** helper functions */
-  void registerPatternElementPairs2( Node pat, Ips& ips,
-                                     PpIpsMap & pp_ips_map, NodePcDispatcher* npc);
-  void registerPatternElementPairs( Node pat, PpIpsMap & pp_ips_map,
-                                    NodePcDispatcher* npc, NodePpDispatcher* npp);
-  /** find the pp-pair between pattern inside multi-pattern*/
-  void combineMultiPpIpsMap(PpIpsMap & pp_ips_map, MultiPpIpsMap & multi_pp_ips_map,
-                            EfficientHandler& eh, size_t index2,
-                            const std::vector<Node> & pats); //pats for debug
-  /** compute candidates for pc pairs */
-  void computeCandidatesPcPairs( Node a, EqClassInfo*, Node b, EqClassInfo* );
-  /** compute candidates for pp pairs */
-  void computeCandidatesPpPairs( Node a, EqClassInfo*, Node b, EqClassInfo* );
-  /** compute candidates for cc pairs */
-  void computeCandidatesConstants( Node a, EqClassInfo*, Node b, EqClassInfo* );
-  /** collect terms based on inverted path string */
-  void collectTermsIps( Ips& ips, SetNode& terms, int index);
-  bool collectParentsTermsIps( Node n, Node f, int arg, SetNode& terms, bool addRep, bool modEq = true );
-public:
-  void collectTermsIps( Ips& ips, SetNode& terms);
-public:
-  void registerEfficientHandler( EfficientHandler& eh, const std::vector<Node> & pat );
-public:
-  void newTerms(SetNode& s);
-public:
-  /** output eq class */
-  void outputEqClass( const char* c, Node n );
-  /** output inverted path string */
-  void outputIps( const char* c, Ips& ips );
-};/* class EfficientEMatcher */
-
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EFFICIENT_E_MATCHING_H */
diff --git a/src/theory/rewriterules/kinds b/src/theory/rewriterules/kinds
deleted file mode 100644
index 4ea0ecd43..000000000
--- a/src/theory/rewriterules/kinds
+++ /dev/null
@@ -1,17 +0,0 @@
-# kinds                                                               -*- sh -*-
-#
-# For documentation on this file format, please refer to
-# src/theory/builtin/kinds.
-#
-
-theory THEORY_REWRITERULES ::CVC4::theory::rewriterules::TheoryRewriteRules "theory/rewriterules/theory_rewriterules.h"
-typechecker "theory/rewriterules/theory_rewriterules_type_rules.h"
-rewriter ::CVC4::theory::rewriterules::TheoryRewriterulesRewriter "theory/rewriterules/theory_rewriterules_rewriter.h"
-
-properties check
-
-# Theory content goes here.
-
-# constants...
-
-endtheory
diff --git a/src/theory/rewriterules/options b/src/theory/rewriterules/options
deleted file mode 100644
index 285e489be..000000000
--- a/src/theory/rewriterules/options
+++ /dev/null
@@ -1,14 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module REWRITE_RULES "theory/rewriterules/options.h" Rewrite Rules
-
-option efficientEMatching --efficient-e-matching bool :default false
- use efficient E-matching (only for rewrite rules)
-
-option rewriteRulesAsAxioms --rewrite-rules-as-axioms bool :default false
- whether to convert rewrite rules to usual axioms (for debugging only)
-
-endmodule
diff --git a/src/theory/rewriterules/rr_candidate_generator.cpp b/src/theory/rewriterules/rr_candidate_generator.cpp
deleted file mode 100644
index 3ebb3547c..000000000
--- a/src/theory/rewriterules/rr_candidate_generator.cpp
+++ /dev/null
@@ -1,67 +0,0 @@
-/*********************                                                        */
-/*! \file rr_candidate_generator.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  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 rr candidate generator class
- **/
-
-#include "theory/rewriterules/rr_candidate_generator.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/quantifiers/term_database.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::rrinst;
-
-GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe) : d_qe(qe){
-  d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClasses(d_qe->getMasterEqualityEngine());
-}
-
-GenericCandidateGeneratorClasses::~GenericCandidateGeneratorClasses(){
-  delete d_master_can_gen;
-}
-
-void GenericCandidateGeneratorClasses::resetInstantiationRound(){
-  d_master_can_gen->resetInstantiationRound();
-}
-
-void GenericCandidateGeneratorClasses::reset(TNode eqc){
-  d_master_can_gen->reset(eqc);
-}
-
-TNode GenericCandidateGeneratorClasses::getNextCandidate(){
-  return d_master_can_gen->getNextCandidate();
-}
-
-
-GenericCandidateGeneratorClass::GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) {
-  d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClass(d_qe->getMasterEqualityEngine());
-}
-
-GenericCandidateGeneratorClass::~GenericCandidateGeneratorClass(){
-  delete d_master_can_gen;
-}
-
-void GenericCandidateGeneratorClass::resetInstantiationRound(){
-  d_master_can_gen->resetInstantiationRound();
-}
-
-void GenericCandidateGeneratorClass::reset(TNode eqc){
-  d_master_can_gen->reset(eqc);
-}
-
-TNode GenericCandidateGeneratorClass::getNextCandidate(){
-  return d_master_can_gen->getNextCandidate();
-}
-
diff --git a/src/theory/rewriterules/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h
deleted file mode 100644
index d00c8ab83..000000000
--- a/src/theory/rewriterules/rr_candidate_generator.h
+++ /dev/null
@@ -1,199 +0,0 @@
-/*********************                                                        */
-/*! \file rr_candidate_generator.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds, Francois Bobot
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief rr candidate generator
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__REWRITERULES__RR_CANDIDATE_GENERATOR_H
-#define __CVC4__THEORY__REWRITERULES__RR_CANDIDATE_GENERATOR_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/rewriterules/rr_inst_match.h"
-
-using namespace CVC4::theory::quantifiers;
-
-namespace CVC4 {
-namespace theory {
-namespace eq {
-
-namespace rrinst{
-typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
-
-//New CandidateGenerator. They have a simpler semantic than the old one
-
-// Just iterate among the equivalence classes
-// node::Null() must be given to reset
-class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{
-private:
-  //the equality classes iterator
-  eq::EqClassesIterator d_eq;
-  //equalityengine pointer
-  EqualityEngine* d_ee;
-public:
-  CandidateGeneratorTheoryEeClasses( EqualityEngine * ee): d_ee( ee ){}
-  ~CandidateGeneratorTheoryEeClasses(){}
-  void resetInstantiationRound(){};
-  void reset( TNode eqc ){
-    Assert(eqc.isNull());
-    d_eq = eq::EqClassesIterator( d_ee );
-  }; //* the argument is not used
-  TNode getNextCandidate(){
-    if( !d_eq.isFinished() ) return (*(d_eq++));
-    else return Node::null();
-  };
-};
-
-// Just iterate among the equivalence class of the given node
-// node::Null() *can't* be given to reset
-class CandidateGeneratorTheoryEeClass : public CandidateGenerator{
-private:
-  //instantiator pointer
-  EqualityEngine* d_ee;
-  //the equality class iterator
-  eq::EqClassIterator d_eqc;
-  /* For the case where the given term doesn't exists in uf */
-  Node d_retNode;
-public:
-  CandidateGeneratorTheoryEeClass( EqualityEngine* ee): d_ee( ee ){}
-  ~CandidateGeneratorTheoryEeClass(){}
-  void resetInstantiationRound(){};
-  void reset( TNode eqc ){
-    Assert(!eqc.isNull());
-    if( d_ee->hasTerm( eqc ) ){
-      /* eqc is in uf  */
-      eqc = d_ee->getRepresentative( eqc );
-      d_eqc = eq::EqClassIterator( eqc, d_ee );
-      d_retNode = Node::null();
-    }else{
-      /* If eqc if not a term known by uf, it is the only one in its
-         equivalence class. So we will return only it */
-      d_retNode = eqc;
-      d_eqc = eq::EqClassIterator();
-    }
-  }; //* the argument is not used
-  TNode getNextCandidate(){
-    if(d_retNode.isNull()){
-      if( !d_eqc.isFinished() ) return (*(d_eqc++));
-      else return Node::null();
-    }else{
-      /* the case where eqc not in uf */
-      Node ret = d_retNode;
-      d_retNode = Node::null(); /* d_eqc.isFinished() must be true */
-      return ret;
-    }
-  };
-};
-
-
-} /* namespace rrinst */
-} /* namespace eq */
-
-namespace uf{
-namespace rrinst {
-
-typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
-
-class CandidateGeneratorTheoryUfOp : public CandidateGenerator{
-private:
-  Node d_op;
-  //instantiator pointer
-  TermDb* d_tdb;
-  // Since new term can appears we restrict ourself to the one that
-  // exists at resetInstantiationRound
-  size_t d_term_iter_limit;
-  size_t d_term_iter;
-public:
-  CandidateGeneratorTheoryUfOp(Node op, TermDb* tdb): d_op(op), d_tdb( tdb ){}
-  ~CandidateGeneratorTheoryUfOp(){}
-  void resetInstantiationRound(){
-    d_term_iter_limit = d_tdb->d_op_map[d_op].size();
-  };
-  void reset( TNode eqc ){
-    Assert(eqc.isNull());
-    d_term_iter = 0;
-  }; //* the argument is not used
-  TNode getNextCandidate(){
-    if( d_term_iter<d_term_iter_limit ){
-      TNode n = d_tdb->d_op_map[d_op][d_term_iter];
-      ++d_term_iter;
-      return n;
-    } else return Node::null();
-  };
-};
-
-class CandidateGeneratorTheoryUfType : public CandidateGenerator{
-private:
-  TypeNode d_type;
-  //instantiator pointer
-  TermDb* d_tdb;
-  // Since new term can appears we restrict ourself to the one that
-  // exists at resetInstantiationRound
-  size_t d_term_iter_limit;
-  size_t d_term_iter;
-public:
-  CandidateGeneratorTheoryUfType(TypeNode type, TermDb* tdb): d_type(type), d_tdb( tdb ){}
-  ~CandidateGeneratorTheoryUfType(){}
-  void resetInstantiationRound(){
-    d_term_iter_limit = d_tdb->d_type_map[d_type].size();
-  };
-  void reset( TNode eqc ){
-    Assert(eqc.isNull());
-    d_term_iter = 0;
-  }; //* the argument is not used
-  TNode getNextCandidate(){
-    if( d_term_iter<d_term_iter_limit ){
-      TNode n = d_tdb->d_type_map[d_type][d_term_iter];
-      ++d_term_iter;
-      return n;
-    } else return Node::null();
-  };
-};
-
-} /* namespace rrinst */
-} /* namespace uf */
-
-class GenericCandidateGeneratorClasses: public rrinst::CandidateGenerator{
-
-  /** The candidate generators */
-  rrinst::CandidateGenerator* d_master_can_gen;
-  /** QuantifierEngine */
-  QuantifiersEngine* d_qe;
-public:
-  GenericCandidateGeneratorClasses(QuantifiersEngine * qe);
-  ~GenericCandidateGeneratorClasses();
-
-  void resetInstantiationRound();
-  void reset(TNode eqc);
-  TNode getNextCandidate();
-  void lookForNextTheory();
-};
-
-class GenericCandidateGeneratorClass: public rrinst::CandidateGenerator{
-
-  /** The candidate generators */
-  rrinst::CandidateGenerator* d_master_can_gen;
-  /** QuantifierEngine */
-  QuantifiersEngine* d_qe;
-public:
-  GenericCandidateGeneratorClass(QuantifiersEngine * qe);
-  ~GenericCandidateGeneratorClass();
-  void resetInstantiationRound();
-  void reset(TNode eqc);
-  TNode getNextCandidate();
-};
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__REWRITERULES__RR_CANDIDATE_GENERATOR_H */
diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp
deleted file mode 100644
index 2d7cf85fd..000000000
--- a/src/theory/rewriterules/rr_inst_match.cpp
+++ /dev/null
@@ -1,1596 +0,0 @@
-/*********************                                                        */
-/*! \file rr_inst_match.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Francois Bobot
- ** Minor contributors (to current version): Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  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 class
- **/
-
-#include "theory/quantifiers/inst_match.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/datatypes/theory_datatypes.h"
-#include "theory/rewriterules/rr_inst_match.h"
-#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"
-#include "theory/rewriterules/efficient_e_matching.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::rrinst;
-using namespace CVC4::theory::uf::rrinst;
-using namespace CVC4::theory::eq::rrinst;
-
-namespace CVC4{
-namespace theory{
-namespace rrinst{
-
-
-
-
-InstMatch::InstMatch() {
-}
-
-InstMatch::InstMatch( InstMatch* m ) {
-  d_map = m->d_map;
-}
-
-bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){
-  std::map< Node, Node >::iterator vn = d_map.find( v );
-  if( !m.isNull() && !m.getType().isSubtypeOf( v.getType() ) ){
-    set = false;
-    return false;
-  }else if( vn==d_map.end() || vn->second.isNull() ){
-    set = true;
-    this->set(v,m);
-    Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl;
-    return true;
-  }else{
-    set = false;
-    return q->areEqual( vn->second, m );
-  }
-}
-
-bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){
-  bool set;
-  return setMatch(q,v,m,set);
-}
-
-bool InstMatch::add( InstMatch& m ){
-  for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){
-    if( !it->second.isNull() ){
-      std::map< Node, Node >::iterator itf = d_map.find( it->first );
-      if( itf==d_map.end() || itf->second.isNull() ){
-        d_map[it->first] = it->second;
-      }
-    }
-  }
-  return true;
-}
-
-bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
-  for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){
-    if( !it->second.isNull() ){
-      std::map< Node, Node >::iterator itf = d_map.find( it->first );
-      if( itf==d_map.end() || itf->second.isNull() ){
-        d_map[ it->first ] = it->second;
-      }else{
-        if( !q->areEqual( it->second, itf->second ) ){
-          d_map.clear();
-          return false;
-        }
-      }
-    }
-  }
-  return true;
-}
-
-void InstMatch::debugPrint( const char* c ){
-  for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
-    Debug( c ) << "   " << it->first << " -> " << it->second << std::endl;
-  }
-  //if( !d_splits.empty() ){
-  //  Debug( c ) << "   Conditions: ";
-  //  for( std::map< Node, Node >::iterator it = d_splits.begin(); it !=d_splits.end(); ++it ){
-  //    Debug( c ) << it->first << " = " << it->second << " ";
-  //  }
-  //  Debug( c ) << std::endl;
-  //}
-}
-
-void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
-    if( d_map.find( ic )==d_map.end() ){
-      d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
-    }
-  }
-}
-
-//void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){
-//  EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery();
-//  for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
-//    d_map[ it->first ] = eqqe->getInternalRepresentative( it->second );
-//  }
-//}
-
-void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
-  for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
-    if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){
-      d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second );
-    }
-  }
-}
-
-void InstMatch::applyRewrite(){
-  for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
-    it->second = Rewriter::rewrite(it->second);
-  }
-}
-
-/** get value */
-Node InstMatch::getValue( Node var ) const{
-  std::map< Node, Node >::const_iterator it = d_map.find( var );
-  if( it!=d_map.end() ){
-    return it->second;
-  }else{
-    return Node::null();
-  }
-}
-
-Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) {
-  return get( qe->getTermDatabase()->getInstantiationConstant( f, i ) );
-}
-
-void InstMatch::set(TNode var, TNode n){
-  Assert( !var.isNull() );
-  if (Trace.isOn("inst-match-warn")) {
-    // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
-    if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){
-      Trace("inst-match-warn") << quantifiers::TermDb::getInstConstAttr(var) << std::endl;
-      Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
-    }
-  }
-  Assert( n.isNull() || n.getType().isSubtypeOf( var.getType() ) );
-  d_map[var] = n;
-}
-
-void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) {
-  set( qe->getTermDatabase()->getInstantiationConstant( f, i ), n );
-}
-
-
-
-
-
-
-typedef CVC4::theory::rrinst::InstMatch InstMatch;
-typedef CVC4::theory::inst::CandidateGeneratorQueue CandidateGeneratorQueue;
-
-template<bool modEq>
-class InstMatchTrie2Pairs
-{
-  typename std::vector< std::vector < typename InstMatchTrie2Gen<modEq>::Tree > > d_data;
-  InstMatchTrie2Gen<modEq> d_backtrack;
-public:
-  InstMatchTrie2Pairs(context::Context* c,  QuantifiersEngine* q, size_t n):
-  d_backtrack(c,q) {
-    // resize to a triangle
-    //
-    // |     *
-    // |   * *
-    // | * * *
-    // | -----> i
-    d_data.resize(n);
-    for(size_t i=0; i < n; ++i){
-      d_data[i].resize(i+1,typename InstMatchTrie2Gen<modEq>::Tree(0));
-    }
-  };
-  InstMatchTrie2Pairs(const InstMatchTrie2Pairs &) CVC4_UNDEFINED;
-  const InstMatchTrie2Pairs & operator =(const InstMatchTrie2Pairs & e) CVC4_UNDEFINED;
-  /** add match m in the trie,
-      return true if it was never seen */
-  inline bool addInstMatch( size_t i, size_t j, InstMatch& m){
-    size_t k = std::min(i,j);
-    size_t l = std::max(i,j);
-    return d_backtrack.addInstMatch(m,&(d_data[l][k]));
-  };
-  inline bool addInstMatch( size_t i, InstMatch& m){
-    return d_backtrack.addInstMatch(m,&(d_data[i][i]));
-  };
-
-};
-
-
-// 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 nonunifiable( TNode t0, TNode pat, const std::vector<Node> & vars){
-  if(pat.isNull()) return true;
-
-  typedef std::vector<std::pair<TNode,TNode> > tstack;
-  tstack stack(1,std::make_pair(t0,pat)); // 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;
-};
-
-/** New things */
-class DumbMatcher: public Matcher{
-  void resetInstantiationRound( QuantifiersEngine* qe ){};
-  bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){
-    return false;
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return false;
-  }
-};
-
-class DumbPatMatcher: public PatMatcher{
-  void resetInstantiationRound( QuantifiersEngine* qe ){};
-  bool reset( InstMatch& m, QuantifiersEngine* qe ){
-    return false;
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return false;
-  }
-};
-
-
-/* The order of the matching is:
-   reset arg1, nextMatch arg1, reset arg2, nextMatch arg2, ... */
-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();
-    Assert( q != NULL );
-    if( quantifiers::TermDb::hasInstConstAttr(d_pattern[i]) ){
-      if( d_pattern[i].getKind()==INST_CONSTANT ){
-        //It's a variable
-        d_variables.push_back(make_triple((TNode)d_pattern[i],i,q));
-      }else{
-        //It's neither a constant argument neither a variable
-        //we create the matcher for the subpattern
-        d_childrens.push_back(make_triple(mkMatcher((TNode)d_pattern[i], qe),i,q));
-      };
-    }else{
-      // It's a constant
-      d_constants.push_back(make_triple((TNode)d_pattern[i],i,q));
-    }
-  }
-}
-
-void ApplyMatcher::resetInstantiationRound( QuantifiersEngine* qe ){
-  for( size_t i=0; i< d_childrens.size(); i++ ){
-    d_childrens[i].first->resetInstantiationRound( qe );
-  }
-}
-
-bool ApplyMatcher::reset(TNode t, InstMatch & m, QuantifiersEngine* qe){
-  Debug("matching") << "Matching " << t << " against pattern " << d_pattern << " ("
-                    << m.size() << ")"  << std::endl;
-
-  //if t is null
-  Assert( !t.isNull() );
-  Assert( !quantifiers::TermDb::hasInstConstAttr(t) );
-  Assert( t.getKind()==d_pattern.getKind() );
-  Assert( (t.getKind()!=APPLY_UF && t.getKind()!=APPLY_CONSTRUCTOR)
-          || t.getOperator()==d_pattern.getOperator() );
-
-  typedef std::vector< triple<TNode,size_t,EqualityQuery*> >::iterator iterator;
-  for(iterator i = d_constants.begin(), end = d_constants.end();
-      i != end; ++i){
-    if( !i->third->areEqual( i->first, t[i->second] ) ){
-      Debug("matching-fail") << "Match fail arg: " << i->first << " and " << t[i->second] << std::endl;
-      //setMatchFail( qe, d_pattern[i], t[i] );
-      //ground arguments are not equal
-      return false;
-    }
-  }
-
-  d_binded.clear();
-  bool set;
-  for(iterator i = d_variables.begin(), end = d_variables.end();
-      i != end; ++i){
-    if( !m.setMatch( i->third, i->first, t[i->second], set) ){
-      //match is in conflict
-      Debug("matching-debug") << "Match in conflict " << t[i->second] << " and "
-                              << i->first << " because "
-                              << m.get(i->first)
-                              << std::endl;
-      Debug("matching-fail") << "Match fail: " << m.get(i->first) << " and " << t[i->second] << std::endl;
-      //setMatchFail( qe, partial[0].d_map[d_pattern[i]], t[i] );
-      m.erase(d_binded.begin(), d_binded.end());
-      return false;
-    }else{
-      if(set){ //The variable has just been set
-        d_binded.push_back(i->first);
-      }
-    }
-  }
-
-  //now, fit children into match
-  //we will be requesting candidates for matching terms for each child
-  d_reps.clear();
-  for( size_t i=0; i< d_childrens.size(); i++ ){
-    Debug("matching-debug") << "Take the representative of " << t[ d_childrens[i].second ] << std::endl;
-    Assert( d_childrens[i].third->hasTerm(t[ d_childrens[i].second ]) );
-    Node rep = d_childrens[i].third->getRepresentative( t[ d_childrens[i].second ] );
-    d_reps.push_back( rep );
-  }
-
-  if(d_childrens.size() == 0) return true;
-  else return getNextMatch(m, qe, true);
-}
-
-bool ApplyMatcher::getNextMatch(InstMatch& m, QuantifiersEngine* qe, bool reset){
-  Assert(d_childrens.size() > 0);
-  const size_t max = d_childrens.size() - 1;
-  size_t index = reset ? 0 : max;
-  Assert(d_childrens.size() == d_reps.size());
-  while(true){
-    if(reset ?
-       d_childrens[index].first->reset( d_reps[index], m, qe ) :
-       d_childrens[index].first->getNextMatch( m, qe )){
-      if(index==max) return true;
-      ++index;
-      reset=true;
-    }else{
-      if(index==0){
-        m.erase(d_binded.begin(), d_binded.end());
-        return false;
-      }
-      --index;
-      reset=false;
-    };
-  }
-}
-
-bool ApplyMatcher::getNextMatch(InstMatch& m, QuantifiersEngine* qe){
-  if(d_childrens.size() == 0){
-    m.erase(d_binded.begin(), d_binded.end());
-    return false;
-  } else return getNextMatch(m, qe, false);
-}
-
-/** Proxy that call the sub-matcher on the result return by the given candidate generator */
-template <class CG, class M>
-class CandidateGeneratorMatcher: public Matcher{
-  /** candidate generator */
-  CG d_cg;
-  /** the sub-matcher */
-  M d_m;
-public:
-  CandidateGeneratorMatcher(CG cg, M m): d_cg(cg), d_m(m)
-  {/* last is Null */};
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_cg.resetInstantiationRound();
-    d_m.resetInstantiationRound(qe);
-  };
-  bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){
-    d_cg.reset(n);
-    return findMatch(m,qe);
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    // The sub-matcher has another match
-    return d_m.getNextMatch(m, qe) || findMatch(m,qe);
-  }
-private:
-  bool findMatch( InstMatch& m, QuantifiersEngine* qe ){
-    // Otherwise try to find a new candidate that has at least one match
-    while(true){
-      TNode n = d_cg.getNextCandidate();//kept somewhere Term-db
-      Debug("matching") << "GenCand " << n << " (" << this << ")" << std::endl;
-      if(n.isNull()) return false;
-      if(d_m.reset(n,m,qe)) return true;
-    };
-  }
-};
-
-/** Proxy that call the sub-matcher on the result return by the given candidate generator */
-template<class M>
-class PatOfMatcher: public PatMatcher{
-  M d_m;
-public:
-  inline PatOfMatcher(M m): d_m(m){}
-  void resetInstantiationRound(QuantifiersEngine* qe){
-    d_m.resetInstantiationRound(qe);
-  }
-  bool reset(InstMatch& m, QuantifiersEngine* qe){
-    return d_m.reset(Node::null(),m,qe);
-  };
-  bool getNextMatch(InstMatch& m, QuantifiersEngine* qe){
-    return d_m.getNextMatch(m,qe);
-  };
-};
-
-class ArithMatcher: public Matcher{
-private:
-  /** for arithmetic matching */
-  std::map< Node, Node > d_arith_coeffs;
-  /** get the match against ground term or formula t.
-      d_match_mattern and t should have the same shape.
-      only valid for use where !d_match_pattern.isNull().
-  */
-  /** the variable that are set by this matcher */
-  std::vector< TNode > d_binded; /* TNode because the variables are already in d_arith_coeffs */
-  Node d_pattern; //for debugging
-public:
-  ArithMatcher(Node pat, QuantifiersEngine* qe);
-  void resetInstantiationRound( QuantifiersEngine* qe ){};
-  bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe );
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );
-};
-
-/** Match just a variable */
-class VarMatcher: public Matcher{
-  Node d_var;
-  bool d_binded; /* True if the reset bind the variable to some value */
-  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();
-  }
-  void resetInstantiationRound( QuantifiersEngine* qe ){};
-  bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){
-    if(!m.setMatch( d_q, d_var, n, d_binded )){
-      //match is in conflict
-      Debug("matching-fail") << "Match fail: " << m.get(d_var)
-                             << " and " << n << std::endl;
-      return false;
-    } else return true;
-  };
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    //match is in conflict
-    if (d_binded) m.erase(d_var);
-    return false;
-  }
-};
-
-template <class M, class Test >
-class TestMatcher: public Matcher{
-  M d_m;
-  Test d_test;
-public:
-  inline TestMatcher(M m, Test test): d_m(m), d_test(test){}
-  inline void resetInstantiationRound(QuantifiersEngine* qe){
-    d_m.resetInstantiationRound(qe);
-  }
-  inline bool reset(TNode n, InstMatch& m, QuantifiersEngine* qe){
-    return d_test(n) && d_m.reset(n, m, qe);
-  }
-  inline bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return d_m.getNextMatch(m, qe);
-  }
-};
-
-class LegalOpTest/*: public unary_function<TNode,bool>*/ {
-  Node d_op;
-public:
-  inline LegalOpTest(Node op): d_op(op){}
-  inline bool operator() (TNode n) {
-    return
-      CandidateGenerator::isLegalCandidate(n) &&
-      // ( // n.getKind()==SELECT || n.getKind()==STORE ||
-      //  n.getKind()==APPLY_UF || n.getKind()==APPLY_CONSTRUCTOR) &&
-      n.hasOperator() &&
-      n.getOperator()==d_op;
-  };
-};
-
-class LegalKindTest/* : public unary_function<TNode,bool>*/ {
-  Kind d_kind;
-public:
-  inline LegalKindTest(Kind kind): d_kind(kind){}
-  inline bool operator() (TNode n) {
-    return
-      CandidateGenerator::isLegalCandidate(n) &&
-      n.getKind()==d_kind;
-  };
-};
-
-class LegalTypeTest/* : public unary_function<TNode,bool>*/ {
-  TypeNode d_type;
-public:
-  inline LegalTypeTest(TypeNode type): d_type(type){}
-  inline bool operator() (TNode n) {
-    return
-      CandidateGenerator::isLegalCandidate(n) &&
-      n.getType()==d_type;
-  };
-};
-
-class LegalTest/* : public unary_function<TNode,bool>*/ {
-public:
-  inline bool operator() (TNode n) {
-    return CandidateGenerator::isLegalCandidate(n);
-  };
-};
-
-size_t numFreeVar(TNode t){
-  size_t n = 0;
-  for( size_t i=0, size =t.getNumChildren(); i < size; ++i ){
-    if( quantifiers::TermDb::hasInstConstAttr(t[i]) ){
-      if( t[i].getKind()==INST_CONSTANT ){
-        //variable
-        ++n;
-      }else{
-        //neither variable nor constant
-        n += numFreeVar(t[i]);
-      }
-    }
-  }
-  return n;
-}
-
-class OpMatcher: public Matcher{
-  /* The matcher */
-  typedef ApplyMatcher AuxMatcher3;
-  typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2;
-  typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1;
-  AuxMatcher1 d_cgm;
-  static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
-    Assert( pat.getKind() == kind::APPLY_UF );
-    /** In reverse order of matcher sequence */
-    AuxMatcher3 am3(pat,qe);
-    /** Keep only the one that have the good operator */
-    AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator()));
-    /** Iter on the equivalence class of the given term */
-    uf::TheoryUF* uf = static_cast<uf::TheoryUF *>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
-    eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
-    CandidateGeneratorTheoryEeClass cdtUfEq(ee);
-    /* Create a matcher from the candidate generator */
-    AuxMatcher1 am1(cdtUfEq,am2);
-    return am1;
-  }
-  size_t d_num_var;
-  Node d_pat;
-public:
-  OpMatcher( Node pat, QuantifiersEngine* qe ):
-    d_cgm(createCgm(pat, qe)),d_num_var(numFreeVar(pat)),
-    d_pat(pat) {}
-
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_cgm.resetInstantiationRound(qe);
-  };
-  bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){
-    // size_t m_size = m.d_map.size();
-    // if(m_size == d_num_var){
-    //   uf::EqualityEngine<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )))->getEqualityEngine();
-    //   std::cout << "!";
-    //   return ee->areEqual(m.subst(d_pat),t);
-    // }else{
-    // std::cout << m.d_map.size() << std::endl;
-    return d_cgm.reset(t, m, qe);
-    // }
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.getNextMatch(m, qe);
-  }
-};
-
-class DatatypesMatcher: public Matcher{
-  /* The matcher */
-  typedef ApplyMatcher AuxMatcher3;
-  typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2;
-  typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1;
-  AuxMatcher1 d_cgm;
-  static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
-    Assert( pat.getKind() == kind::APPLY_CONSTRUCTOR,
-            "For datatypes only constructor are accepted in pattern" );
-    /** In reverse order of matcher sequence */
-    AuxMatcher3 am3(pat,qe);
-    /** Keep only the one that have the good operator */
-    AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator()));
-    /** Iter on the equivalence class of the given term */
-    datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes *>(qe->getTheoryEngine()->theoryOf( theory::THEORY_DATATYPES ));
-    eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(dt->getEqualityEngine());
-    CandidateGeneratorTheoryEeClass cdtDtEq(ee);
-    /* Create a matcher from the candidate generator */
-    AuxMatcher1 am1(cdtDtEq,am2);
-    return am1;
-  }
-  Node d_pat;
-public:
-  DatatypesMatcher( Node pat, QuantifiersEngine* qe ):
-    d_cgm(createCgm(pat, qe)),
-    d_pat(pat) {}
-
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_cgm.resetInstantiationRound(qe);
-  };
-  bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){
-    Debug("matching") << "datatypes: " << t << " matches " << d_pat << std::endl;
-    return d_cgm.reset(t, m, qe);
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.getNextMatch(m, qe);
-  }
-};
-
-class ArrayMatcher: public Matcher{
-  /* The matcher */
-  typedef ApplyMatcher AuxMatcher3;
-  typedef TestMatcher< AuxMatcher3, LegalKindTest > AuxMatcher2;
-  typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1;
-  AuxMatcher1 d_cgm;
-  static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
-    Assert( pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE );
-    /** In reverse order of matcher sequence */
-    AuxMatcher3 am3(pat,qe);
-    /** Keep only the one that have the good operator */
-    AuxMatcher2 am2(am3, LegalKindTest(pat.getKind()));
-    /** Iter on the equivalence class of the given term */
-    arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(qe->getTheoryEngine()->theoryOf( theory::THEORY_ARRAY ));
-    eq::EqualityEngine* ee =
-      static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
-    CandidateGeneratorTheoryEeClass cdtUfEq(ee);
-    /* Create a matcher from the candidate generator */
-    AuxMatcher1 am1(cdtUfEq,am2);
-    return am1;
-  }
-  size_t d_num_var;
-  Node d_pat;
-public:
-  ArrayMatcher( Node pat, QuantifiersEngine* qe ):
-    d_cgm(createCgm(pat, qe)),d_num_var(numFreeVar(pat)),
-    d_pat(pat) {}
-
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_cgm.resetInstantiationRound(qe);
-  };
-  bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){
-    // size_t m_size = m.d_map.size();
-    // if(m_size == d_num_var){
-    //   uf::EqualityEngine<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )))->getEqualityEngine();
-    //   std::cout << "!";
-    //   return ee->areEqual(m.subst(d_pat),t);
-    // }else{
-    // std::cout << m.d_map.size() << std::endl;
-    return d_cgm.reset(t, m, qe);
-    // }
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.getNextMatch(m, qe);
-  }
-};
-
-class AllOpMatcher: public PatMatcher{
-  /* The matcher */
-  typedef ApplyMatcher AuxMatcher3;
-  typedef TestMatcher< AuxMatcher3, LegalTest > AuxMatcher2;
-  typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryUfOp, AuxMatcher2> AuxMatcher1;
-  AuxMatcher1 d_cgm;
-  static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
-    Assert( pat.hasOperator() );
-    /** In reverse order of matcher sequence */
-    AuxMatcher3 am3(pat,qe);
-    /** Keep only the one that have the good operator */
-    AuxMatcher2 am2(am3,LegalTest());
-    /** Iter on the equivalence class of the given term */
-    TermDb* tdb = qe->getTermDatabase();
-    Node op = tdb->getOperator( pat );
-    CandidateGeneratorTheoryUfOp cdtUfEq(op,tdb);
-    /* Create a matcher from the candidate generator */
-    AuxMatcher1 am1(cdtUfEq,am2);
-    return am1;
-  }
-  size_t d_num_var;
-  Node d_pat;
-public:
-  AllOpMatcher( TNode pat, QuantifiersEngine* qe ):
-    d_cgm(createCgm(pat, qe)), d_num_var(numFreeVar(pat)),
-    d_pat(pat) {}
-
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_cgm.resetInstantiationRound(qe);
-  };
-  bool reset( InstMatch& m, QuantifiersEngine* qe ){
-    //    std::cout << m.d_map.size() << "/" << d_num_var << std::endl;
-    return d_cgm.reset(Node::null(), m, qe);
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.getNextMatch(m, qe);
-  }
-};
-
-template <bool classes> /** true classes | false class */
-class GenericCandidateGeneratorClasses: public CandidateGenerator{
-private:
-  CandidateGenerator* d_cg;
-  QuantifiersEngine* d_qe;
-
-public:
-  void mkCandidateGenerator(){
-    if(classes)
-      d_cg = new GenericCandidateGeneratorClasses(d_qe);
-    else
-      d_cg = new GenericCandidateGeneratorClass(d_qe);
-  }
-
-  GenericCandidateGeneratorClasses(QuantifiersEngine* qe):
-    d_qe(qe) {
-    mkCandidateGenerator();
-  }
-  ~GenericCandidateGeneratorClasses(){
-    delete(d_cg);
-  }
-  const GenericCandidateGeneratorClasses & operator =(const GenericCandidateGeneratorClasses & m){
-    mkCandidateGenerator();
-    return m;
-  };
-  GenericCandidateGeneratorClasses(const GenericCandidateGeneratorClasses & m):
-  d_qe(m.d_qe){
-    mkCandidateGenerator();
-  }
-  void resetInstantiationRound(){
-    d_cg->resetInstantiationRound();
-  };
-  void reset( TNode eqc ){
-    Assert( !classes || eqc.isNull() );
-    d_cg->reset(eqc);
-  }; //* the argument is not used
-  TNode getNextCandidate(){
-    return d_cg->getNextCandidate();
-  };
-}; /* MetaCandidateGeneratorClasses */
-
-
-class GenericMatcher: public Matcher{
-  /* The matcher */
-  typedef ApplyMatcher AuxMatcher3;
-  typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2;
-  typedef CandidateGeneratorMatcher< GenericCandidateGeneratorClasses<false>, AuxMatcher2> AuxMatcher1;
-  AuxMatcher1 d_cgm;
-  static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
-    /** In reverse order of matcher sequence */
-    AuxMatcher3 am3(pat,qe);
-    /** Keep only the one that have the good operator */
-    AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator()));
-    /** Iter on the equivalence class of the given term */
-    GenericCandidateGeneratorClasses<false> cdtG(qe);
-    /* Create a matcher from the candidate generator */
-    AuxMatcher1 am1(cdtG,am2);
-    return am1;
-  }
-  Node d_pat;
-public:
-  GenericMatcher( Node pat, QuantifiersEngine* qe ):
-    d_cgm(createCgm(pat, qe)),
-    d_pat(pat) {}
-
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_cgm.resetInstantiationRound(qe);
-  };
-  bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.reset(t, m, qe);
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.getNextMatch(m, qe);
-  }
-};
-
-
-class GenericPatMatcher: public PatMatcher{
-  /* The matcher */
-  typedef ApplyMatcher AuxMatcher3;
-  typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2;
-  typedef CandidateGeneratorMatcher< GenericCandidateGeneratorClasses<true>, AuxMatcher2> AuxMatcher1;
-  AuxMatcher1 d_cgm;
-  static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
-    /** In reverse order of matcher sequence */
-    AuxMatcher3 am3(pat,qe);
-    /** Keep only the one that have the good operator */
-    AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator()));
-    /** Iter on the equivalence class of the given term */
-    GenericCandidateGeneratorClasses<true> cdtG(qe);
-    /* Create a matcher from the candidate generator */
-    AuxMatcher1 am1(cdtG,am2);
-    return am1;
-  }
-  Node d_pat;
-public:
-  GenericPatMatcher( Node pat, QuantifiersEngine* qe ):
-    d_cgm(createCgm(pat, qe)),
-    d_pat(pat) {}
-
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_cgm.resetInstantiationRound(qe);
-  };
-  bool reset( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.reset(Node::null(), m, qe);
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.getNextMatch(m, qe);
-  }
-};
-
-class MetaCandidateGeneratorClasses: public CandidateGenerator{
-private:
-  CandidateGenerator* d_cg;
-  TypeNode d_ty;
-  TheoryEngine* d_te;
-
-public:
-  CandidateGenerator* mkCandidateGenerator(TypeNode ty, TheoryEngine* te){
-    Debug("inst-match-gen") << "MetaCandidateGenerator for type: " << ty
-                            << " Theory : " << Theory::theoryOf(ty) << std::endl;
-    if( Theory::theoryOf(ty) == theory::THEORY_DATATYPES ){
-      // datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes *>(te->theoryOf( theory::THEORY_DATATYPES ));
-      // return new datatypes::rrinst::CandidateGeneratorTheoryClasses(dt);
-      Unimplemented("MetaCandidateGeneratorClasses for THEORY_DATATYPES");
-    }else if ( Theory::theoryOf(ty) == theory::THEORY_ARRAY ){
-      arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(te->theoryOf( theory::THEORY_ARRAY ));
-      eq::EqualityEngine* ee =
-        static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
-      return new CandidateGeneratorTheoryEeClasses(ee);
-    } else {
-      uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(te->theoryOf( theory::THEORY_UF ));
-      eq::EqualityEngine* ee =
-        static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
-      return new CandidateGeneratorTheoryEeClasses(ee);
-    }
-  }
-  MetaCandidateGeneratorClasses(TypeNode ty, TheoryEngine* te):
-    d_ty(ty), d_te(te) {
-    d_cg = mkCandidateGenerator(ty,te);
-  }
-  ~MetaCandidateGeneratorClasses(){
-    delete(d_cg);
-  }
-  const MetaCandidateGeneratorClasses & operator =(const MetaCandidateGeneratorClasses & m){
-    d_cg = mkCandidateGenerator(m.d_ty, m.d_te);
-    return m;
-  };
-  MetaCandidateGeneratorClasses(const MetaCandidateGeneratorClasses & m):
-  d_ty(m.d_ty), d_te(m.d_te){
-    d_cg = mkCandidateGenerator(m.d_ty, m.d_te);
-  }
-  void resetInstantiationRound(){
-    d_cg->resetInstantiationRound();
-  };
-  void reset( TNode eqc ){
-    d_cg->reset(eqc);
-  }; //* the argument is not used
-  TNode getNextCandidate(){
-    return d_cg->getNextCandidate();
-  };
-}; /* MetaCandidateGeneratorClasses */
-
-/** Match just a variable */
-class AllVarMatcher: public PatMatcher{
-private:
-  /* generator */
-  typedef VarMatcher AuxMatcher3;
-  typedef TestMatcher< AuxMatcher3, LegalTypeTest > AuxMatcher2;
-  typedef CandidateGeneratorMatcher< MetaCandidateGeneratorClasses, AuxMatcher2 > AuxMatcher1;
-  AuxMatcher1 d_cgm;
-  static inline AuxMatcher1 createCgm(TNode pat, QuantifiersEngine* qe){
-    Assert( pat.getKind()==INST_CONSTANT );
-    TypeNode ty = pat.getType();
-    Debug("inst-match-gen") << "create AllVarMatcher for type: " << ty << std::endl;
-    /** In reverse order of matcher sequence */
-    /** Distribute it to all the pattern */
-    AuxMatcher3 am3(pat,qe);
-    /** Keep only the one that have the good type */
-    AuxMatcher2 am2(am3,LegalTypeTest(ty));
-    /** Generate one term by eq classes */
-    MetaCandidateGeneratorClasses mcdt(ty,qe->getTheoryEngine());
-    /* Create a matcher from the candidate generator */
-    AuxMatcher1 am1(mcdt,am2);
-    return am1;
-  }
-public:
-  AllVarMatcher( TNode pat, QuantifiersEngine* qe ):
-    d_cgm(createCgm(pat, qe)){}
-
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_cgm.resetInstantiationRound(qe);
-  };
-  bool reset( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.reset(Node::null(), m, qe); //cdtUfEq doesn't use it's argument for reset
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.getNextMatch(m, qe);
-  }
-};
-
-/** Match all the pattern with the same term */
-class SplitMatcher: public Matcher{
-private:
-  const size_t size;
-  ApplyMatcher d_m; /** Use ApplyMatcher by creating a fake application */
-public:
-  SplitMatcher(std::vector< Node > pats, QuantifiersEngine* qe):
-    size(pats.size()),
-    d_m(NodeManager::currentNM()->mkNode(kind::INST_PATTERN,pats), qe) {}
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_m.resetInstantiationRound(qe);
-  };
-  bool reset( TNode ex, InstMatch& m, QuantifiersEngine* qe ){
-    NodeBuilder<> n(kind::INST_PATTERN);
-    for(size_t i = 0; i < size; ++i) n << ex;
-    Node nn = n;
-    return d_m.reset(nn,m,qe);
-  };
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return getNextMatch(m, qe);
-  }
-};
-
-
-/** Match uf term in a fixed equivalence class */
-class UfCstEqMatcher: public PatMatcher{
-private:
-  /* equivalence class to match */
-  Node d_cst;
-  /* generator */
-  OpMatcher d_cgm;
-public:
-  UfCstEqMatcher( Node pat, Node cst, QuantifiersEngine* qe ):
-    d_cst(cst),
-    d_cgm(OpMatcher(pat,qe)) {};
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_cgm.resetInstantiationRound(qe);
-  };
-  bool reset( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.reset(d_cst, m, qe);
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.getNextMatch(m, qe);
-  }
-};
-
-/** Match equalities */
-class UfEqMatcher: public PatMatcher{
-private:
-  /* generator */
-  typedef SplitMatcher AuxMatcher3;
-  typedef TestMatcher< AuxMatcher3, LegalTypeTest > AuxMatcher2;
-  typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClasses, AuxMatcher2 > AuxMatcher1;
-  AuxMatcher1 d_cgm;
-  static inline AuxMatcher1 createCgm(std::vector<Node> & pat, QuantifiersEngine* qe){
-    Assert( pat.size() > 0);
-    TypeNode ty = pat[0].getType();
-    for(size_t i = 1; i < pat.size(); ++i){
-      Assert(pat[i].getType() == ty);
-    }
-    /** In reverse order of matcher sequence */
-    /** Distribute it to all the pattern */
-    AuxMatcher3 am3(pat,qe);
-    /** Keep only the one that have the good type */
-    AuxMatcher2 am2(am3,LegalTypeTest(ty));
-    /** Generate one term by eq classes */
-    uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
-    eq::EqualityEngine* ee =
-      static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
-    CandidateGeneratorTheoryEeClasses cdtUfEq(ee);
-    /* Create a matcher from the candidate generator */
-    AuxMatcher1 am1(cdtUfEq,am2);
-    return am1;
-  }
-public:
-  UfEqMatcher( std::vector<Node> & pat, QuantifiersEngine* qe ):
-    d_cgm(createCgm(pat, qe)){}
-
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_cgm.resetInstantiationRound(qe);
-  };
-  bool reset( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.reset(Node::null(), m, qe); //cdtUfEq doesn't use it's argument for reset
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.getNextMatch(m, qe);
-  }
-};
-
-
-/** Match dis-equalities */
-class UfDeqMatcher: public PatMatcher{
-private:
-  /* generator */
-  typedef ApplyMatcher AuxMatcher3;
-
-  class EqTest/* : public unary_function<Node,bool>*/ {
-    TypeNode d_type;
-  public:
-    inline EqTest(TypeNode type): d_type(type){};
-    inline bool operator() (Node n) {
-      return
-        CandidateGenerator::isLegalCandidate(n) &&
-        n.getKind() == kind::EQUAL &&
-        n[0].getType()==d_type;
-    };
-  };
-  typedef TestMatcher< AuxMatcher3, EqTest > AuxMatcher2;
-  typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2 > AuxMatcher1;
-  AuxMatcher1 d_cgm;
-  Node false_term;
-  static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){
-    Assert( pat.getKind() == kind::NOT);
-    TNode eq = pat[0];
-    Assert( eq.getKind() == kind::EQUAL);
-    TypeNode ty = eq[0].getType();
-    /** In reverse order of matcher sequence */
-    /** Distribute it to all the pattern */
-    AuxMatcher3 am3(eq,qe);
-    /** Keep only the one that have the good type */
-    AuxMatcher2 am2(am3,EqTest(ty));
-    /** Will generate all the terms of the eq class of false */
-    uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
-    eq::EqualityEngine* ee =
-      static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
-    CandidateGeneratorTheoryEeClass cdtUfEq(ee);
-    /* Create a matcher from the candidate generator */
-    AuxMatcher1 am1(cdtUfEq,am2);
-    return am1;
-  }
-public:
-  UfDeqMatcher( Node pat, QuantifiersEngine* qe ):
-    d_cgm(createCgm(pat, qe)),
-    false_term((static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF )))->getEqualityEngine()->
-                getRepresentative(NodeManager::currentNM()->mkConst<bool>(false) )){};
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    d_cgm.resetInstantiationRound(qe);
-  };
-  bool reset( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.reset(false_term, m, qe);
-  }
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-    return d_cgm.getNextMatch(m, qe);
-  }
-};
-
-Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){
-  Debug("inst-match-gen") << "mkMatcher: Pattern term is " << pat << std::endl;
-
-  // if( pat.getKind() == kind::APPLY_UF){
-  //   return new OpMatcher(pat, qe);
-  // } else if( pat.getKind() == kind::APPLY_CONSTRUCTOR ){
-  //   return new DatatypesMatcher(pat, qe);
-  // } else if( pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE ){
-  //   return new ArrayMatcher(pat, qe);
-  if( pat.getKind() == kind::APPLY_UF ||
-      pat.getKind() == kind::APPLY_CONSTRUCTOR ||
-      pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE ){
-    return new GenericMatcher(pat, qe);
-  } else { /* Arithmetic? */
-    /** TODO: something simpler to see if the pattern is a good
-        arithmetic pattern */
-    std::map< Node, Node > d_arith_coeffs;
-    if( !Trigger::getPatternArithmetic( quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ){
-      Message() << "(?) Unknown matching pattern is " << pat << std::endl;
-      Unimplemented("pattern not implemented");
-      return new DumbMatcher();
-    }else{
-      Debug("matching-arith") << "Generated arithmetic pattern for " << pat << ": " << 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;
-      }
-      ArithMatcher am3 (pat, qe);
-      TestMatcher<ArithMatcher, LegalTypeTest>
-        am2(am3,LegalTypeTest(pat.getType()));
-      /* generator */
-      uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
-      eq::EqualityEngine* ee =
-        static_cast<eq::EqualityEngine*> (uf->getEqualityEngine());
-      CandidateGeneratorTheoryEeClass cdtUfEq(ee);
-      return new CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass,
-        TestMatcher<ArithMatcher, LegalTypeTest> > (cdtUfEq,am2);
-    }
-  }
-};
-
-PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){
-  Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;
-  Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
-
-  if( pat.getKind()==kind::NOT && pat[0].getKind() == kind::EQUAL){
-    /* Difference */
-    return new UfDeqMatcher(pat, qe);
-  } else if (pat.getKind() == kind::EQUAL){
-    if( !quantifiers::TermDb::hasInstConstAttr(pat[0])){
-        Assert(quantifiers::TermDb::hasInstConstAttr(pat[1]));
-        return new UfCstEqMatcher(pat[1], pat[0], qe);
-    }else if( !quantifiers::TermDb::hasInstConstAttr(pat[1] )){
-      Assert(quantifiers::TermDb::hasInstConstAttr(pat[0]));
-      return new UfCstEqMatcher(pat[0], pat[1], qe);
-    }else{
-      std::vector< Node > pats(pat.begin(),pat.end());
-      return new UfEqMatcher(pats,qe);
-    }
-  } else if( Trigger::isAtomicTrigger( pat ) ){
-    return new AllOpMatcher(pat, qe);
-    // return new GenericPatMatcher(pat, qe);
-  } else if( pat.getKind()==INST_CONSTANT ){
-    // just a variable
-    return new AllVarMatcher(pat, qe);
-  } else { /* Arithmetic? */
-    /** TODO: something simpler to see if the pattern is a good
-        arithmetic pattern */
-    std::map< Node, Node > d_arith_coeffs;
-    if( !Trigger::getPatternArithmetic( quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ){
-      Debug("inst-match-gen") << "(?) Unknown matching pattern is " << pat << std::endl;
-      Message() << "(?) Unknown matching pattern is " << pat << std::endl;
-      return new DumbPatMatcher();
-    }else{
-      Debug("matching-arith") << "Generated arithmetic pattern for " << pat << ": " << 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;
-      }
-      ArithMatcher am3 (pat, qe);
-      TestMatcher<ArithMatcher, LegalTest>
-        am2(am3,LegalTest());
-      /* generator */
-      TermDb* tdb = qe->getTermDatabase();
-      CandidateGeneratorTheoryUfType cdtUfEq(pat.getType(),tdb);
-      typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryUfType,
-                                          TestMatcher<ArithMatcher, LegalTest> > AuxMatcher1;
-      return new PatOfMatcher<AuxMatcher1>(AuxMatcher1(cdtUfEq,am2));
-    }
-  }
-};
-
-ArithMatcher::ArithMatcher(Node pat, QuantifiersEngine* qe): d_pattern(pat){
-
-  if(Trigger::getPatternArithmetic(quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) )
-    {
-    Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_pattern << std::endl;
-    Assert(false);
-  }else{
-    Debug("matching-arith") << "Generated arithmetic pattern for " << d_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;
-    }
-  }
-
-};
-
-bool ArithMatcher::reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){
-  Debug("matching-arith") << "Matching " << t << " " << d_pattern << std::endl;
-  d_binded.clear();
-  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 ));
-      d_binded.push_back(ic);
-      //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) ));
-            d_binded.push_back(ic);
-          }
-        }
-      }
-      Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl;
-      return true;
-    }else{
-      m.erase(d_binded.begin(), d_binded.end());
-      return false;
-    }
-  }else{
-    m.erase(d_binded.begin(), d_binded.end());
-    return false;
-  }
-};
-
-bool ArithMatcher::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
-  m.erase(d_binded.begin(), d_binded.end());
-  return false;
-};
-
-
-class MultiPatsMatcher: public PatsMatcher{
-private:
-  bool d_reset_done;
-  std::vector< PatMatcher* > d_patterns;
-  InstMatch d_im;
-  bool reset( QuantifiersEngine* qe ){
-    d_im.clear();
-    d_reset_done = true;
-
-    return getNextMatch(qe,true);
-  };
-
-  bool getNextMatch(QuantifiersEngine* qe, bool reset){
-    const size_t max = d_patterns.size() - 1;
-    size_t index = reset ? 0 : max;
-    while(true){
-      Debug("matching") << "MultiPatsMatcher::index " << index << "/"
-                        << max << (reset ? " reset_phase" : "") << std::endl;
-      if(reset ?
-         d_patterns[index]->reset( d_im, qe ) :
-         d_patterns[index]->getNextMatch( d_im, qe )){
-        if(index==max) return true;
-        ++index;
-        reset=true;
-      }else{
-        if(index==0) return false;
-        --index;
-        reset=false;
-      };
-    }
-  }
-
-public:
-  MultiPatsMatcher(std::vector< Node > & pats, QuantifiersEngine* qe):
-    d_reset_done(false){
-    Assert(pats.size() > 0);
-    for( size_t i=0; i< pats.size(); i++ ){
-      d_patterns.push_back(mkPattern(pats[i],qe));
-    };
-  };
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    for( size_t i=0; i< d_patterns.size(); i++ ){
-      d_patterns[i]->resetInstantiationRound( qe );
-    };
-    d_reset_done = false;
-    d_im.clear();
-  };
-  bool getNextMatch( QuantifiersEngine* qe ){
-    Assert(d_patterns.size()>0);
-    if(d_reset_done) return getNextMatch(qe,false);
-    else return reset(qe);
-  }
-  const InstMatch& getInstMatch(){return d_im;};
-
-  int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe);
-};
-
-enum EffiStep{
-  ES_STOP,
-  ES_GET_MONO_CANDIDATE,
-  ES_GET_MULTI_CANDIDATE,
-  ES_RESET1,
-  ES_RESET2,
-  ES_NEXT1,
-  ES_NEXT2,
-  ES_RESET_OTHER,
-  ES_NEXT_OTHER,
-};
-static inline std::ostream& operator<<(std::ostream& out, const EffiStep& step) {
-  switch(step){
-  case ES_STOP: out << "STOP"; break;
-  case ES_GET_MONO_CANDIDATE: out << "GET_MONO_CANDIDATE"; break;
-  case ES_GET_MULTI_CANDIDATE: out << "GET_MULTI_CANDIDATE"; break;
-  case ES_RESET1: out << "RESET1"; break;
-  case ES_RESET2: out << "RESET2"; break;
-  case ES_NEXT1: out << "NEXT1"; break;
-  case ES_NEXT2: out << "NEXT2"; break;
-  case ES_RESET_OTHER: out << "RESET_OTHER"; break;
-  case ES_NEXT_OTHER: out << "NEXT_OTHER"; break;
-  }
-  return out;
-}
-
-
-int MultiPatsMatcher::addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe){
-  //now, try to add instantiation for each match produced
-  int addedLemmas = 0;
-  resetInstantiationRound( qe );
-  d_im.add( baseMatch );
-  while( getNextMatch( qe ) ){
-    InstMatch im_copy = getInstMatch();
-    std::vector< Node > terms;
-    for( unsigned i=0; i<quant[0].getNumChildren(); i++ ){
-      terms.push_back( im_copy.get( qe, quant, i ) );
-    }
-
-    //m.makeInternal( d_quantEngine->getEqualityQuery() );
-    if( qe->addInstantiation( quant, terms ) ){
-      addedLemmas++;
-    }
-  }
-  //return number of lemmas added
-  return addedLemmas;
-}
-
-PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe ){
-  return new MultiPatsMatcher( pat, qe);
-}
-
-class MultiEfficientPatsMatcher: public PatsMatcher{
-private:
-  bool d_phase_mono;
-  bool d_phase_new_term;
-  std::vector< PatMatcher* > d_patterns;
-  std::vector< Matcher* > d_direct_patterns;
-  InstMatch d_im;
-  EfficientHandler d_eh;
-  EfficientHandler::MultiCandidate d_mc;
-  InstMatchTrie2Pairs<true> d_cache;
-  std::vector<Node> d_pats;
-  // bool indexDone( size_t i){
-  //   return i == d_c.first.second ||
-  //     ( i == d_c.second.second && d_c.second.first.empty());
-  // }
-
-
-
-  static const EffiStep ES_START = ES_GET_MONO_CANDIDATE;
-  EffiStep d_step;
-
-  //return true if it becomes bigger than d_patterns.size() - 1
-  bool incrIndex(size_t & index){
-    if(index == d_patterns.size() - 1) return true;
-    ++index;
-    if(index == d_mc.first.second
-       || (!d_phase_mono && index == d_mc.second.second))
-      return incrIndex(index);
-    else return false;
-  }
-
-  //return true if it becomes smaller than 0
-  bool decrIndex(size_t & index){
-    if(index == 0) return true;
-    --index;
-    if(index == d_mc.first.second
-       || (!d_phase_mono && index == d_mc.second.second))
-      return decrIndex(index);
-    else return false;
-  }
-
-  bool resetOther( QuantifiersEngine* qe ){
-    return getNextMatchOther(qe,true);
-  };
-
-
-  bool getNextMatchOther(QuantifiersEngine* qe, bool reset){
-    size_t index = reset ? 0 : d_patterns.size();
-    if(!reset && decrIndex(index)) return false;
-    if( reset &&
-        (index == d_mc.first.second
-         || (!d_phase_mono && index == d_mc.second.second))
-        && incrIndex(index)) return true;
-    while(true){
-      Debug("matching") << "MultiEfficientPatsMatcher::index " << index << "/"
-                        << d_patterns.size() - 1 << std::endl;
-      if(reset ?
-         d_patterns[index]->reset( d_im, qe ) :
-         d_patterns[index]->getNextMatch( d_im, qe )){
-        if(incrIndex(index)) return true;
-        reset=true;
-      }else{
-        if(decrIndex(index)) return false;
-        reset=false;
-      };
-    }
-  }
-
-  inline EffiStep TestMonoCache(QuantifiersEngine* qe){
-    if( //!d_phase_new_term ||
-       d_pats.size() == 1) return ES_RESET_OTHER;
-    if(d_cache.addInstMatch(d_mc.first.second,d_im)){
-      Debug("inst-match::cache") << "Cache miss" << d_im << std::endl;
-      ++qe->d_statistics.d_mono_candidates_cache_miss;
-      return ES_RESET_OTHER;
-    } else {
-      Debug("inst-match::cache") << "Cache hit" << d_im << std::endl;
-      ++qe->d_statistics.d_mono_candidates_cache_hit;
-      return ES_NEXT1;
-    }
-    // ++qe->d_statistics.d_mono_candidates_cache_miss;
-    // return ES_RESET_OTHER;
-  }
-
-  inline EffiStep TestMultiCache(QuantifiersEngine* qe){
-    if(d_cache.addInstMatch(d_mc.first.second,d_mc.second.second,d_im)){
-      ++qe->d_statistics.d_multi_candidates_cache_miss;
-      return ES_RESET_OTHER;
-    } else {
-      ++qe->d_statistics.d_multi_candidates_cache_hit;
-      return ES_NEXT2;
-    }
-  }
-
-
-public:
-
-  bool getNextMatch( QuantifiersEngine* qe ){
-    Assert( d_step == ES_START || d_step == ES_NEXT_OTHER || d_step == ES_STOP );
-    while(true){
-      Debug("matching") << "d_step=" << d_step << " "
-                        << "d_im=" << d_im << std::endl;
-      switch(d_step){
-      case ES_GET_MONO_CANDIDATE:
-        Assert(d_im.empty());
-        if(d_phase_new_term ? d_eh.getNextMonoCandidate(d_mc.first) : d_eh.getNextMonoCandidateNewTerm(d_mc.first)){
-          if(d_phase_new_term) ++qe->d_statistics.d_num_mono_candidates_new_term;
-          else ++qe->d_statistics.d_num_mono_candidates;
-          d_phase_mono = true;
-          d_step = ES_RESET1;
-        } else if (!d_phase_new_term){
-          d_phase_new_term = true;
-          d_step = ES_GET_MONO_CANDIDATE;
-        } else {
-          d_phase_new_term = false;
-          d_step = ES_GET_MULTI_CANDIDATE;
-        }
-        break;
-      case ES_GET_MULTI_CANDIDATE:
-        Assert(d_im.empty());
-        if(d_eh.getNextMultiCandidate(d_mc)){
-          ++qe->d_statistics.d_num_multi_candidates;
-          d_phase_mono = false;
-          d_step = ES_RESET1;
-        } else d_step = ES_STOP;
-        break;
-      case ES_RESET1:
-        if(d_direct_patterns[d_mc.first.second]->reset(d_mc.first.first,d_im,qe))
-          d_step = d_phase_mono ? TestMonoCache(qe) : ES_RESET2;
-        else d_step = d_phase_mono ? ES_GET_MONO_CANDIDATE : ES_GET_MULTI_CANDIDATE;
-        break;
-      case ES_RESET2:
-        Assert(!d_phase_mono);
-        if(d_direct_patterns[d_mc.second.second]->reset(d_mc.second.first,d_im,qe))
-          d_step = TestMultiCache(qe);
-        else d_step = ES_NEXT1;
-        break;
-      case ES_NEXT1:
-        if(d_direct_patterns[d_mc.first.second]->getNextMatch(d_im,qe))
-          d_step = d_phase_mono ? TestMonoCache(qe) : ES_RESET2;
-        else d_step = d_phase_mono ? ES_GET_MONO_CANDIDATE : ES_GET_MULTI_CANDIDATE;
-        break;
-      case ES_NEXT2:
-        if(d_direct_patterns[d_mc.second.second]->getNextMatch(d_im,qe))
-          d_step = TestMultiCache(qe);
-        else d_step = ES_NEXT1;
-        break;
-      case ES_RESET_OTHER:
-        if(resetOther(qe)){
-          d_step = ES_NEXT_OTHER;
-          return true;
-        } else d_step = d_phase_mono ? ES_NEXT1 : ES_NEXT2;
-        break;
-      case ES_NEXT_OTHER:
-        {
-          if(!getNextMatchOther(qe,false)){
-            d_step = d_phase_mono ? ES_NEXT1 : ES_NEXT2;
-          }else{
-            d_step = ES_NEXT_OTHER;
-            return true;
-          }
-        }
-        break;
-      case ES_STOP:
-        Assert(d_im.empty());
-        return false;
-      }
-    }
-  }
-
-  MultiEfficientPatsMatcher(std::vector< Node > & pats, QuantifiersEngine* qe):
-    d_eh(qe->getTheoryEngine()->getSatContext()),
-    d_cache(qe->getTheoryEngine()->getSatContext(),qe,pats.size()),
-    d_pats(pats), d_step(ES_START) {
-    Assert(pats.size() > 0);
-    for( size_t i=0; i< pats.size(); i++ ){
-      d_patterns.push_back(mkPattern(pats[i],qe));
-      if(pats[i].getKind()==kind::INST_CONSTANT){
-        d_direct_patterns.push_back(new VarMatcher(pats[i],qe));
-      } else if( pats[i].getKind() == kind::NOT && pats[i][0].getKind() == kind::EQUAL){
-        d_direct_patterns.push_back(new ApplyMatcher(pats[i][0],qe));
-      } else {
-        d_direct_patterns.push_back(new ApplyMatcher(pats[i],qe));
-      }
-    };
-    EfficientEMatcher* eem = qe->getEfficientEMatcher();
-    eem->registerEfficientHandler(d_eh, pats);
-  };
-  void resetInstantiationRound( QuantifiersEngine* qe ){
-    Assert(d_step == ES_START || d_step == ES_STOP);
-    for( size_t i=0; i< d_patterns.size(); i++ ){
-      d_patterns[i]->resetInstantiationRound( qe );
-      d_direct_patterns[i]->resetInstantiationRound( qe );
-    };
-    d_step = ES_START;
-    d_phase_new_term = false;
-    Assert(d_im.empty());
-  };
-
-  const InstMatch& getInstMatch(){return d_im;};
-
-  int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe);
-};
-
-int MultiEfficientPatsMatcher::addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe){
-  //now, try to add instantiation for each match produced
-  int addedLemmas = 0;
-  Assert(baseMatch.empty());
-  resetInstantiationRound( qe );
-  while( getNextMatch( qe ) ){
-    InstMatch im_copy = getInstMatch();
-    std::vector< Node > terms;
-    for( unsigned i=0; i<quant[0].getNumChildren(); i++ ){
-      terms.push_back( im_copy.get( qe, quant, i ) );
-    }
-
-    //m.makeInternal( d_quantEngine->getEqualityQuery() );
-    if( qe->addInstantiation( quant, terms ) ){
-      addedLemmas++;
-    }
-  }
-  //return number of lemmas added
-  return addedLemmas;
-};
-
-PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe ){
-  return new MultiEfficientPatsMatcher( pat, qe);
-}
-
-} /* CVC4::theory::rrinst */
-} /* CVC4::theory */
-} /* CVC4 */
diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h
deleted file mode 100644
index c42dd8914..000000000
--- a/src/theory/rewriterules/rr_inst_match.h
+++ /dev/null
@@ -1,341 +0,0 @@
-/*********************                                                        */
-/*! \file rr_inst_match.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Francois Bobot
- ** Minor contributors (to current version): Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  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 class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H
-#define __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H
-
-#include "theory/theory.h"
-#include "util/hash.h"
-#include "util/ntuple.h"
-
-#include <ext/hash_set>
-#include <iostream>
-#include <map>
-
-#include "theory/uf/equality_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "context/cdlist.h"
-
-#include "theory/quantifiers/term_database.h"
-#include "expr/node_manager.h"
-#include "expr/node_builder.h"
-
-#include "theory/quantifiers/options.h"
-#include "theory/rewriterules/options.h"
-
-//#define USE_EFFICIENT_E_MATCHING
-
-namespace CVC4 {
-namespace theory {
-
-class EqualityQuery;
-
-namespace rrinst{
-
-/** basic class defining an instantiation */
-class InstMatch {
-  /* map from variable to ground terms */
-  std::map< Node, Node > d_map;
-public:
-  InstMatch();
-  InstMatch( InstMatch* m );
-
-  /** set the match of v to m */
-  bool setMatch( EqualityQuery* q, TNode v, TNode m );
-  /* This version tell if the variable has been set */
-  bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & set);
-  /** fill all unfilled values with m */
-  bool add( InstMatch& m );
-  /** if compatible, fill all unfilled values with m and return true
-      return false otherwise */
-  bool merge( EqualityQuery* q, InstMatch& m );
-  /** debug print method */
-  void debugPrint( const char* c );
-  /** is complete? */
-  bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
-  /** make complete */
-  void makeComplete( Node f, QuantifiersEngine* qe );
-  /** make internal representative */
-  //void makeInternalRepresentative( QuantifiersEngine* qe );
-  /** make representative */
-  void makeRepresentative( QuantifiersEngine* qe );
-  /** get value */
-  Node getValue( Node var ) const;
-  /** clear */
-  void clear(){ d_map.clear(); }
-  /** is_empty */
-  bool empty(){ return d_map.empty(); }
-  /** to stream */
-  inline void toStream(std::ostream& out) const {
-    out << "INST_MATCH( ";
-    for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){
-      if( it != d_map.begin() ){ out << ", "; }
-      out << it->first << " -> " << it->second;
-    }
-    out << " )";
-  }
-
-
-  //for rewrite rules
-
-  /** apply rewrite */
-  void applyRewrite();
-  /** erase */
-  template<class Iterator>
-  void erase(Iterator begin, Iterator end){
-    for(Iterator i = begin; i != end; ++i){
-      d_map.erase(*i);
-    };
-  }
-  void erase(Node node){ d_map.erase(node); }
-  /** get */
-  Node get( TNode var ) { return d_map[var]; }
-  Node get( QuantifiersEngine* qe, Node f, int i );
-  /** set */
-  void set(TNode var, TNode n);
-  void set( QuantifiersEngine* qe, Node f, int i, TNode n );
-  /** size */
-  size_t size(){ return d_map.size(); }
-  /* iterator */
-  std::map< Node, Node >::iterator begin(){ return d_map.begin(); };
-  std::map< Node, Node >::iterator end(){ return d_map.end(); };
-  std::map< Node, Node >::iterator find(Node var){ return d_map.find(var); };
-  /* Node used for matching the trigger only for mono-trigger (just for
-     efficiency because I need only that) */
-  Node d_matched;
-};/* class InstMatch */
-
-
-
-class CandidateGenerator
-{
-public:
-  CandidateGenerator(){}
-  virtual ~CandidateGenerator(){};
-
-  /** Get candidates functions.  These set up a context to get all match candidates.
-      cg->reset( eqc );
-      do{
-        Node cand = cg->getNextCandidate();
-        //.......
-      }while( !cand.isNull() );
-
-      eqc is the equivalence class you are searching in
-  */
-  virtual void reset( TNode eqc ) = 0;
-  virtual TNode getNextCandidate() = 0;
-  /** call this at the beginning of each instantiation round */
-  virtual void resetInstantiationRound() = 0;
-public:
-  /** legal candidate */
-  static inline bool isLegalCandidate( TNode n ){
-    return !n.getAttribute(NoMatchAttribute()) &&
-      ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n)) &&
-      ( !options::efficientEMatching() || n.hasAttribute(AvailableInTermDb()) );
-}
-
-};
-
-
-inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
-  m.toStream(out);
-  return out;
-}
-
-template<bool modEq = false> class InstMatchTrie2;
-template<bool modEq = false> class InstMatchTrie2Pairs;
-
-template<bool modEq = false>
-class InstMatchTrie2Gen
-{
-  friend class InstMatchTrie2<modEq>;
-  friend class InstMatchTrie2Pairs<modEq>;
-
-private:
-
-  class Tree {
-  public:
-    typedef std::hash_map< Node, Tree *, NodeHashFunction > MLevel;
-    MLevel e;
-    const size_t level; //context level of creation
-    Tree() CVC4_UNDEFINED;
-    const Tree & operator =(const Tree & t){
-      Assert(t.e.empty()); Assert(e.empty());
-      Assert(t.level == level);
-      return t;
-    }
-    Tree(size_t l): level(l) {};
-    ~Tree(){
-      for(typename MLevel::iterator i = e.begin(); i!=e.end(); ++i)
-        delete(i->second);
-    };
-  };
-
-
-  typedef std::pair<Tree *, TNode> Mod;
-
-  class CleanUp{
-  public:
-    inline void operator()(Mod * m){
-      typename Tree::MLevel::iterator i = m->first->e.find(m->second);
-      Assert (i != m->first->e.end()); //should not have been already removed
-      m->first->e.erase(i);
-    };
-  };
-
-  EqualityQuery* d_eQ;
-  CandidateGenerator * d_cG;
-
-  context::Context* d_context;
-  context::CDList<Mod, CleanUp, std::allocator<Mod> > d_mods;
-
-
-  typedef std::map<Node, Node>::const_iterator mapIter;
-
-  /** add the substitution given by the iterator*/
-  void addSubTree( Tree * root, mapIter current, mapIter end, size_t currLevel);
-  /** test if it exists match, modulo uf-equations if modEq is true if
-   *  return false the deepest point of divergence is put in [e] and
-   *  [diverge].
-   */
-  bool existsInstMatch( Tree * root,
-                        mapIter & current, mapIter & end,
-                        Tree * & e, mapIter & diverge) const;
-
-  /** add match m in the trie root
-      return true if it was never seen */
-  bool addInstMatch( InstMatch& m, Tree * root);
-
-public:
-  InstMatchTrie2Gen(context::Context* c,  QuantifiersEngine* q);
-  InstMatchTrie2Gen(const InstMatchTrie2Gen &) CVC4_UNDEFINED;
-  const InstMatchTrie2Gen & operator =(const InstMatchTrie2Gen & e) CVC4_UNDEFINED;
-};
-
-template<bool modEq>
-class InstMatchTrie2
-{
-  typename InstMatchTrie2Gen<modEq>::Tree d_data;
-  InstMatchTrie2Gen<modEq> d_backtrack;
-public:
-  InstMatchTrie2(context::Context* c,  QuantifiersEngine* q): d_data(0),
-                                                              d_backtrack(c,q) {};
-  InstMatchTrie2(const InstMatchTrie2 &) CVC4_UNDEFINED;
-  const InstMatchTrie2 & operator =(const InstMatchTrie2 & e) CVC4_UNDEFINED;
-  /** add match m in the trie,
-      return true if it was never seen */
-  inline bool addInstMatch( InstMatch& m){
-    return d_backtrack.addInstMatch(m,&d_data);
-  };
-
-};/* class InstMatchTrie2 */
-
-class Matcher
-{
-public:
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
-  /** reset the term to match, return false if there is no such term */
-  virtual bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ) = 0;
-  /** get the next match. If it return false once you shouldn't call
-      getNextMatch again before doing a reset */
-  virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
-  /** If reset, or getNextMatch return false they remove from the
-      InstMatch the binding that they have previously created */
-
-  /** virtual Matcher in order to have defined behavior */
-  virtual ~Matcher(){};
-};
-
-
-class ApplyMatcher: public Matcher{
-private:
-  /** What to check first: constant and variable */
-  std::vector< triple< TNode,size_t,EqualityQuery* > > d_constants;
-  std::vector< triple< TNode,size_t,EqualityQuery* > > d_variables;
-  /** children generators, only the sub-pattern which are
-      neither a variable neither a constant appears */
-  std::vector< triple< Matcher*, size_t, EqualityQuery* > > d_childrens;
-  /** the variable that have been set by this matcher (during its own reset) */
-  std::vector< TNode > d_binded; /* TNode because the variable are already in d_pattern */
-  /** the representative of the argument of the term given by the last reset */
-  std::vector< Node > d_reps;
-public:
-  /** The pattern we are producing matches for */
-  Node d_pattern;
-public:
-  /** constructors */
-  ApplyMatcher( Node pat, QuantifiersEngine* qe);
-  /** destructor */
-  ~ApplyMatcher(){/*TODO delete dandling pointers? */}
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  void resetInstantiationRound( QuantifiersEngine* qe );
-  /** reset the term to match */
-  bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe );
-  /** get the next match. */
-  bool getNextMatch(InstMatch& m, QuantifiersEngine* qe);
-private:
-  bool getNextMatch(InstMatch& m, QuantifiersEngine* qe, bool reset);
-};
-
-
-/* Match literal so you don't choose the equivalence class( */
-class PatMatcher
-{
-public:
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
-  /** reset the matcher, return false if there is no such term */
-  virtual bool reset( InstMatch& m, QuantifiersEngine* qe ) = 0;
-  /** get the next match. If it return false once you shouldn't call
-      getNextMatch again before doing a reset */
-  virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
-  /** If reset, or getNextMatch return false they remove from the
-      InstMatch the binding that they have previously created */
-};
-
-Matcher* mkMatcher( Node pat, QuantifiersEngine* qe );
-PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe );
-
-/* Match literal so you don't choose the equivalence class( */
-class PatsMatcher
-{
-public:
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
-  /** reset the matcher, return false if there is no such term */
-  virtual bool getNextMatch( QuantifiersEngine* qe ) = 0;
-  virtual const InstMatch& getInstMatch() = 0;
-  /** Add directly the instantiation to quantifiers engine */
-  virtual int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe) = 0;
-};
-
-PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe );
-PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe );
-
-/** return true if whatever Node is substituted for the variables the
-    given Node can't match the pattern */
-bool nonunifiable( TNode t, TNode pat, const std::vector<Node> & vars);
-
-class InstMatchGenerator;
-
-}/* CVC4::theory rrinst */
-
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_H */
diff --git a/src/theory/rewriterules/rr_inst_match_impl.h b/src/theory/rewriterules/rr_inst_match_impl.h
deleted file mode 100644
index c0dea3ba2..000000000
--- a/src/theory/rewriterules/rr_inst_match_impl.h
+++ /dev/null
@@ -1,126 +0,0 @@
-/*********************                                                        */
-/*! \file rr_inst_match_impl.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Francois Bobot
- ** Minor contributors (to current version): Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  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 class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_IMPL_H
-#define __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_IMPL_H
-
-#include "theory/rewriterules/rr_inst_match.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
-#include "theory/uf/equality_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace rrinst {
-
-template<bool modEq>
-InstMatchTrie2Gen<modEq>::InstMatchTrie2Gen(context::Context* c,  QuantifiersEngine* qe):
-  d_context(c), d_mods(c) {
-  d_eQ = qe->getEqualityQuery();
-  d_cG = new GenericCandidateGeneratorClass(qe);
-};
-
-/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
-template<bool modEq>
-void InstMatchTrie2Gen<modEq>::addSubTree( Tree * root, mapIter current, mapIter end, size_t currLevel ) {
-  if( current == end ) return;
-
-  Assert(root->e.find(current->second) == root->e.end());
-  Tree * root2 = new Tree(currLevel);
-  root->e.insert(std::make_pair(current->second, root2));
-  addSubTree(root2, ++current, end, currLevel );
-}
-
-/** exists match */
-template<bool modEq>
-bool InstMatchTrie2Gen<modEq>::existsInstMatch(InstMatchTrie2Gen<modEq>::Tree * root,
-                                            mapIter & current, mapIter & end,
-                                            Tree * & e, mapIter & diverge) const{
-  if( current == end ) {
-    Debug("Trie2") << "Trie2 Bottom " << std::endl;
-    --current;
-    return true;
-  }; //Already their
-
-  if (current->first > diverge->first){
-    // this point is the deepest point currently seen map are ordered
-    e = root;
-    diverge = current;
-  };
-
-  TNode n = current->second;
-  typename InstMatchTrie2Gen<modEq>::Tree::MLevel::iterator it =
-    root->e.find( n );
-  if( it!=root->e.end() &&
-      existsInstMatch( (*it).second, ++current, end, e, diverge) ){
-    Debug("Trie2") << "Trie2 Directly here " << n << std::endl;
-    --current;
-    return true;
-  }
-  Assert( it==root->e.end() || e != root );
-
-  // Even if n is in the trie others of the equivalence class
-  // can also be in it since the equality can have appeared
-  // after they have been added
-  if( modEq && d_eQ->hasTerm( n ) ){
-    //check modulo equality if any other instantiation match exists
-    d_cG->reset( d_eQ->getRepresentative( n ) );
-    for(TNode en = d_cG->getNextCandidate() ; !en.isNull() ;
-        en = d_cG->getNextCandidate() ){
-      if( en == n ) continue; // already tested
-      typename InstMatchTrie2Gen<modEq>::Tree::MLevel::iterator itc =
-        root->e.find( en );
-      if( itc!=root->e.end() &&
-          existsInstMatch( (*itc).second, ++current, end, e, diverge) ){
-        Debug("Trie2") << "Trie2 Indirectly here by equality " << n << " = " << en << std::endl;
-        --current;
-        return true;
-      }
-      Assert( itc==root->e.end() || e != root );
-    }
-  }
-  --current;
-  return false;
-}
-
-template<bool modEq>
-bool InstMatchTrie2Gen<modEq>::
-addInstMatch( InstMatch& m, InstMatchTrie2Gen<modEq>::Tree* e ) {
-  d_cG->resetInstantiationRound();
- mapIter begin = m.begin();
- mapIter end = m.end();
- mapIter diverge = begin;
- if( !existsInstMatch(e, begin, end, e, diverge ) ){
-   Assert(!diverge->second.isNull());
-   size_t currLevel = d_context->getLevel();
-   addSubTree( e, diverge, end, currLevel );
-   if(e->level != currLevel)
-     //If same level that e, will be removed at the same time than e
-     d_mods.push_back(std::make_pair(e,diverge->second));
-   return true;
- }else{
-   return false;
- }
-}
-
-}/* CVC4::theory::rrinst namespace */
-
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
-
-#endif /*  __CVC4__THEORY__REWRITERULES__RR_INST_MATCH_IMPL_H */
diff --git a/src/theory/rewriterules/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp
deleted file mode 100644
index 13250cf1b..000000000
--- a/src/theory/rewriterules/rr_trigger.cpp
+++ /dev/null
@@ -1,385 +0,0 @@
-/*********************                                                        */
-/*! \file rr_trigger.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds, Francois Bobot
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  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 trigger class
- **/
-
-#include "theory/rewriterules/rr_trigger.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
-#include "theory/uf/equality_engine.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::rrinst;
-
-/** trigger class constructor */
-Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) :
-d_quantEngine( qe ), d_f( f ){
-  d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
-  Debug("trigger") << "Trigger for " << f << ": " << d_nodes << std::endl;
-  if(matchOption == MATCH_GEN_DEFAULT) d_mg = mkPatterns( d_nodes, qe );
-  else d_mg = mkPatternsEfficient( d_nodes, qe );
-  if( d_nodes.size()==1 ){
-    if( isSimpleTrigger( d_nodes[0] ) ){
-      ++(qe->d_statistics.d_triggers);
-    }else{
-      ++(qe->d_statistics.d_simple_triggers);
-    }
-  }else{
-    Debug("multi-trigger") << "Multi-trigger " << (*this) << std::endl;
-    //std::cout << "Multi-trigger for " << f << " : " << std::endl;
-    //std::cout << "   " << (*this) << std::endl;
-    ++(qe->d_statistics.d_multi_triggers);
-  }
-}
-
-void Trigger::resetInstantiationRound(){
-  d_mg->resetInstantiationRound( d_quantEngine );
-}
-
-
-bool Trigger::getNextMatch(){
-  bool retVal = d_mg->getNextMatch( d_quantEngine );
-  //m.makeInternal( d_quantEngine->getEqualityQuery() );
-  return retVal;
-}
-
-// bool Trigger::getMatch( Node t, InstMatch& m ){
-//   //FIXME: this assumes d_mg is an inst match generator
-//   return ((InstMatchGenerator*)d_mg)->getMatch( t, m, d_quantEngine );
-// }
-
-
-int Trigger::addInstantiations( InstMatch& baseMatch ){
-  int addedLemmas = d_mg->addInstantiations( baseMatch,
-                                             quantifiers::TermDb::getInstConstAttr(d_nodes[0]),
-                                             d_quantEngine);
-  if( addedLemmas>0 ){
-    Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was ";
-    for( int i=0; i<(int)d_nodes.size(); i++ ){
-      Debug("inst-trigger") << d_nodes[i] << " ";
-    }
-    Debug("inst-trigger") << std::endl;
-  }
-  return addedLemmas;
-}
-
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption,
-                             bool smartTriggers ){
-  std::vector< Node > trNodes;
-  if( !keepAll ){
-    //only take nodes that contribute variables to the trigger when added
-    std::vector< Node > temp;
-    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
-    std::map< Node, bool > vars;
-    std::map< Node, std::vector< Node > > patterns;
-    for( int i=0; i<(int)temp.size(); i++ ){
-      bool foundVar = false;
-      qe->getTermDatabase()->computeVarContains( temp[i] );
-      for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){
-        Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
-        if( quantifiers::TermDb::getInstConstAttr(v)==f ){
-          if( vars.find( v )==vars.end() ){
-            vars[ v ] = true;
-            foundVar = true;
-          }
-        }
-      }
-      if( foundVar ){
-        trNodes.push_back( temp[i] );
-        for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){
-          Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
-          patterns[ v ].push_back( temp[i] );
-        }
-      }
-    }
-    //now, minimalize the trigger
-    for( int i=0; i<(int)trNodes.size(); i++ ){
-      bool keepPattern = false;
-      Node n = trNodes[i];
-      for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
-        Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
-        if( patterns[v].size()==1 ){
-          keepPattern = true;
-          break;
-        }
-      }
-      if( !keepPattern ){
-        //remove from pattern vector
-        for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
-          Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
-          for( int k=0; k<(int)patterns[v].size(); k++ ){
-            if( patterns[v][k]==n ){
-              patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
-              break;
-            }
-          }
-        }
-        //remove from trigger nodes
-        trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
-        i--;
-      }
-    }
-  }else{
-    trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
-  }
-
-  //check for duplicate?
-  if( trOption==TR_MAKE_NEW ){
-    //static int trNew = 0;
-    //static int trOld = 0;
-    //Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes );
-    //if( t ){
-    //  trOld++;
-    //}else{
-    //  trNew++;
-    //}
-    //if( (trNew+trOld)%100==0 ){
-    //  std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl;
-    //}
-  }else{
-    Trigger* t = qe->getRRTriggerDatabase()->getTrigger( trNodes );
-    if( t ){
-      if( trOption==TR_GET_OLD ){
-        //just return old trigger
-        return t;
-      }else{
-        return NULL;
-      }
-    }
-  }
-  Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers );
-  qe->getRRTriggerDatabase()->addTrigger( trNodes, t );
-  return t;
-}
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){
-  std::vector< Node > nodes;
-  nodes.push_back( n );
-  return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers );
-}
-
-bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){
-  for( int i=0; i<(int)nodes.size(); i++ ){
-    if( !isUsableTrigger( nodes[i], f ) ){
-      return false;
-    }
-  }
-  return true;
-}
-
-bool Trigger::isUsable( Node n, Node f ){
-  if( quantifiers::TermDb::getInstConstAttr(n)==f ){
-    if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){
-      std::map< Node, Node > coeffs;
-      return getPatternArithmetic( f, n, coeffs );
-    }else{
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        if( !isUsable( n[i], f ) ){
-          return false;
-        }
-      }
-      return true;
-    }
-  }else{
-    return true;
-  }
-}
-
-bool Trigger::isSimpleTrigger( Node n ){
-  if( isAtomicTrigger( n ) ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){
-        return false;
-      }
-    }
-    return true;
-  }else{
-    return false;
-  }
-}
-
-
-bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){
-  if( patMap.find( n )==patMap.end() ){
-    patMap[ n ] = false;
-    if( tstrt==TS_MIN_TRIGGER ){
-      if( n.getKind()==FORALL ){
-#ifdef NESTED_PATTERN_SELECTION
-        //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt );
-        return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt );
-#else
-        return false;
-#endif
-      }else{
-        bool retVal = false;
-        for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
-            retVal = true;
-          }
-        }
-        if( retVal ){
-          return true;
-        }else if( isUsableTrigger( n, f ) ){
-          patMap[ n ] = true;
-          return true;
-        }else{
-          return false;
-        }
-      }
-    }else{
-      bool retVal = false;
-      if( isUsableTrigger( n, f ) ){
-        patMap[ n ] = true;
-        if( tstrt==TS_MAX_TRIGGER ){
-          return true;
-        }else{
-          retVal = true;
-        }
-      }
-      if( n.getKind()==FORALL ){
-#ifdef NESTED_PATTERN_SELECTION
-        //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){
-        //  retVal = true;
-        //}
-        if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){
-          retVal = true;
-        }
-#endif
-      }else{
-        for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
-            retVal = true;
-          }
-        }
-      }
-      return retVal;
-    }
-  }else{
-    return patMap[ n ];
-  }
-}
-
-void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){
-  std::map< Node, bool > patMap;
-  if( filterInst ){
-    //immediately do not consider any term t for which another term is an instance of t
-    std::vector< Node > patTerms2;
-    collectPatTerms( qe, f, n, patTerms2, TS_ALL, false );
-    std::vector< Node > temp;
-    temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
-    qe->getTermDatabase()->filterInstances( temp );
-    if( temp.size()!=patTerms2.size() ){
-      Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl;
-      Debug("trigger-filter-instance") << "Old: ";
-      for( int i=0; i<(int)patTerms2.size(); i++ ){
-        Debug("trigger-filter-instance") << patTerms2[i] << " ";
-      }
-      Debug("trigger-filter-instance") << std::endl << "New: ";
-      for( int i=0; i<(int)temp.size(); i++ ){
-        Debug("trigger-filter-instance") << temp[i] << " ";
-      }
-      Debug("trigger-filter-instance") << std::endl;
-    }
-    if( tstrt==TS_ALL ){
-      patTerms.insert( patTerms.begin(), temp.begin(), temp.end() );
-      return;
-    }else{
-      //do not consider terms that have instances
-      for( int i=0; i<(int)patTerms2.size(); i++ ){
-        if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
-          patMap[ patTerms2[i] ] = false;
-        }
-      }
-    }
-  }
-  collectPatTerms2( qe, f, n, patMap, tstrt );
-  for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
-    if( it->second ){
-      patTerms.push_back( it->first );
-    }
-  }
-}
-
-bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){
-  if( n.getKind()==PLUS ){
-    Assert( coeffs.empty() );
-    NodeBuilder<> t(kind::PLUS);
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){
-        if( n[i].getKind()==INST_CONSTANT ){
-          if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){
-            coeffs[ n[i] ] = Node::null();
-          }else{
-            coeffs.clear();
-            return false;
-          }
-        }else if( !getPatternArithmetic( f, n[i], coeffs ) ){
-          coeffs.clear();
-          return false;
-        }
-      }else{
-        t << n[i];
-      }
-    }
-    if( t.getNumChildren()==0 ){
-      coeffs[ Node::null() ] = NodeManager::currentNM()->mkConst( Rational(0) );
-    }else if( t.getNumChildren()==1 ){
-      coeffs[ Node::null() ]  = t.getChild( 0 );
-    }else{
-      coeffs[ Node::null() ]  = t;
-    }
-    return true;
-  }else if( n.getKind()==MULT ){
-    if( n[0].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[0])==f ){
-      Assert( !quantifiers::TermDb::hasInstConstAttr(n[1]) );
-      coeffs[ n[0] ] = n[1];
-      return true;
-    }else if( n[1].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[1])==f ){
-      Assert( !quantifiers::TermDb::hasInstConstAttr(n[0]) );
-      coeffs[ n[1] ] = n[0];
-      return true;
-    }
-  }
-  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/rewriterules/rr_trigger.h b/src/theory/rewriterules/rr_trigger.h
deleted file mode 100644
index f02f38d0e..000000000
--- a/src/theory/rewriterules/rr_trigger.h
+++ /dev/null
@@ -1,157 +0,0 @@
-/*********************                                                        */
-/*! \file rr_trigger.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds, Francois Bobot
- ** Minor contributors (to current version): Tianyi Liang
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief trigger class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H
-#define __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H
-
-#include "theory/rewriterules/rr_inst_match.h"
-
-namespace CVC4 {
-namespace theory {
-namespace rrinst {
-
-//a collect of nodes representing a trigger
-class Trigger {
-private:
-  /** the quantifiers engine */
-  QuantifiersEngine* d_quantEngine;
-  /** the quantifier this trigger is for */
-  Node d_f;
-  /** match generators */
-  PatsMatcher * d_mg;
-private:
-  /** trigger constructor */
-  Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0, bool smartTriggers = false );
-public:
-  ~Trigger(){}
-public:
-  std::vector< Node > d_nodes;
-public:
-  void debugPrint( const char* c );
-  PatsMatcher* getGenerator() { return d_mg; }
-public:
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  void resetInstantiationRound();
-  /** get next match.  must call reset( eqc ) once before this function. */
-  bool getNextMatch();
-  const InstMatch & getInstMatch(){return d_mg->getInstMatch();};
-  /** return whether this is a multi-trigger */
-  bool isMultiTrigger() { return d_nodes.size()>1; }
-public:
-  /** add all available instantiations exhaustively, in any equivalence class
-      if limitInst>0, limitInst is the max # of instantiations to try */
-  int addInstantiations( InstMatch& baseMatch);
-  /** mkTrigger method
-     ie     : quantifier engine;
-     f      : forall something ....
-     nodes  : (multi-)trigger
-     matchOption : which policy to use for creating matches (one of InstMatchGenerator::MATCH_GEN_* )
-     keepAll: don't remove unneeded patterns;
-     trOption : policy for dealing with triggers that already existed (see below)
-  */
-  enum {
-    //options for producing matches
-    MATCH_GEN_DEFAULT = 0,
-    MATCH_GEN_EFFICIENT_E_MATCH,   //generate matches via Efficient E
-  };
-  enum{
-    TR_MAKE_NEW,    //make new trigger even if it already may exist
-    TR_GET_OLD,     //return a previous trigger if it had already been created
-    TR_RETURN_NULL  //return null if a duplicate is found
-  };
-  static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes,
-                             int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW,
-                             bool smartTriggers = false );
-  static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n,
-                             int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW,
-                             bool smartTriggers = false );
-private:
-  /** is subterm of trigger usable */
-  static bool isUsable( Node n, Node f );
-  /** collect all APPLY_UF pattern terms for f in n */
-  static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt );
-public:
-  //different strategies for choosing trigger terms
-  enum {
-    TS_MAX_TRIGGER = 0,
-    TS_MIN_TRIGGER,
-    TS_ALL,
-  };
-  static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst = false );
-public:
-  /** is usable trigger */
-  static inline bool isUsableTrigger( TNode n, TNode f ){
-    return quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f );
-  }
-  static inline bool isAtomicTrigger( TNode n ){
-    return
-      n.getKind()==kind::APPLY_UF ||
-      n.getKind() == kind::APPLY_CONSTRUCTOR ||
-      n.getKind()==kind::SELECT ||
-      n.getKind()==kind::STORE;
-  }
-  static bool isUsableTrigger( std::vector< Node >& nodes, Node f );
-  static bool isSimpleTrigger( Node n );
-  /** get pattern arithmetic */
-  static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs );
-
-  inline void toStream(std::ostream& out) const {
-    out << "TRIGGER( ";
-    for( int i=0; i<(int)d_nodes.size(); i++ ){
-      if( i>0 ){ out << ", "; }
-      out << d_nodes[i];
-    }
-    out << " )";
-  }
-};
-
-inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) {
-  tr.toStream(out);
-  return out;
-}
-
-/** a trie of triggers */
-class TriggerTrie
-{
-private:
-  Trigger* getTrigger2( std::vector< Node >& nodes );
-  void addTrigger2( std::vector< Node >& nodes, Trigger* t );
-public:
-  TriggerTrie() : d_tr( NULL ){}
-  Trigger* d_tr;
-  std::map< Node, TriggerTrie* > d_children;
-  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, Trigger* t ){
-    std::vector< Node > temp;
-    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
-    std::sort( temp.begin(), temp.end() );
-    return addTrigger2( temp, t );
-  }
-};
-
-
-}/* CVC4::theory::rrinst namespace */
-
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__REWRITERULES__RR_TRIGGER_H */
diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
deleted file mode 100644
index 37187e684..000000000
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ /dev/null
@@ -1,78 +0,0 @@
-/*********************                                                        */
-/*! \file theory_rewriterules.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Francois Bobot
- ** Minor contributors (to current version): Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Deals with rewrite rules ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/rewriterules/theory_rewriterules.h"
-#include "theory/rewriter.h"
-
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::rewriterules;
-using namespace CVC4::theory::rrinst;
-
-
-namespace CVC4 {
-namespace theory {
-namespace rewriterules {
-
-
-TheoryRewriteRules::TheoryRewriteRules(context::Context* c,
-                                       context::UserContext* u,
-                                       OutputChannel& out,
-                                       Valuation valuation,
-                                       const LogicInfo& logicInfo) :
-  Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo)
-{
-
-}
-
-void TheoryRewriteRules::check(Effort level) {
-  CodeTimer codeTimer(d_theoryTime);
-
-  while(!done()) {
-    // Get all the assertions
-    // TODO: Test that it have already been ppAsserted
-
-    //if we are here and ppAssert has not been done
-    // that means that ppAssert is off so we need to assert now
-    Assertion assertion = get();
-    // Assertion assertion = get();
-    // TNode fact = assertion.assertion;
-
-    // Debug("rewriterules") << "TheoryRewriteRules::check(): processing " << fact << std::endl;
-    //   if (getValuation().getDecisionLevel()>0)
-    //     Unhandled(getValuation().getDecisionLevel());
-    //   addRewriteRule(fact);
-
-    }
-};
-
-Node TheoryRewriteRules::explain(TNode n){
-
-  return Node::null();
-}
-
-void TheoryRewriteRules::collectModelInfo( TheoryModel* m, bool fullModel ){
-
-}
-
-}/* CVC4::theory::rewriterules namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
deleted file mode 100644
index 85cd9a85c..000000000
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ /dev/null
@@ -1,62 +0,0 @@
-/*********************                                                        */
-/*! \file theory_rewriterules.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds, Francois Bobot
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Rewrite Engine classes
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_H
-#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_H
-
-#include "context/cdlist.h"
-#include "context/cdqueue.h"
-#include "theory/valuation.h"
-#include "theory/theory.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
-#include "context/context_mm.h"
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-namespace rewriterules {
-
-class TheoryRewriteRules : public Theory {
-private:
-
-  KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::rewriterules::theoryTime");
- public:
-  /** Constructs a new instance of TheoryRewriteRules
-      w.r.t. the provided context.*/
-  TheoryRewriteRules(context::Context* c,
-                     context::UserContext* u,
-                     OutputChannel& out,
-                     Valuation valuation,
-                     const LogicInfo& logicInfo);
-
-  /** Usual function for theories */
-  void check(Theory::Effort e);
-  Node explain(TNode n);
-  void collectModelInfo( TheoryModel* m, bool fullModel );
-  void notifyEq(TNode lhs, TNode rhs);
-  std::string identify() const {
-    return "THEORY_REWRITERULES";
-  }
-
-};/* class TheoryRewriteRules */
-
-}/* CVC4::theory::rewriterules namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_H */
diff --git a/src/theory/rewriterules/theory_rewriterules_params.h b/src/theory/rewriterules/theory_rewriterules_params.h
deleted file mode 100644
index e20556ef3..000000000
--- a/src/theory/rewriterules/theory_rewriterules_params.h
+++ /dev/null
@@ -1,86 +0,0 @@
-/*********************                                                        */
-/*! \file theory_rewriterules_params.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Francois Bobot
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Parameters for the rewrite rules theory
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H
-#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H
-
-namespace CVC4 {
-namespace theory {
-namespace rewriterules {
-
-/**
-   Specify if the propagation is done by lemma or by real theory propagation
- */
-static const bool propagate_as_lemma = true;
-
-/**
-   Cache the instantiation of rules in order to remove duplicate
- */
-static const bool cache_match = true;
-
-/**
-   Compute when the rules are created which terms in the body can lead
-   to new instantiation (try only single trigger). During propagation
-   we check if the instantiation of these terms are known terms.
- */
-static const bool compute_opt = true;
-
-/**
-   rewrite the matching found
- */
-static const bool rewrite_instantiation = true;
-
-/**
-   use the representative for the matching found
- */
-static const bool representative_instantiation = false;
-
-/**
-   Wait the specified number of check after a new propagation (a
-   previous unknown guards becomes true) is found before verifying again the guards.
-
-   Allow to break loop with other theories.
- */
-static const size_t checkSlowdown = 0;
-
-/**
-   Use the current model to eliminate guard before asking for notification
- */
-static const bool useCurrentModel = false;
-
-/**
-   Simulate rewriting by tagging rewritten terms.
- */
-static const bool simulateRewritting = true;
-
-/**
-   Do narrowing at full effort
-*/
-static const bool narrowing_full_effort = false;
-
-/**
-   Direct rewrite: Add rewrite rules directly in the rewriter.
- */
-static const bool direct_rewrite = false;
-
-}/* CVC4::theory::rewriterules namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H */
diff --git a/src/theory/rewriterules/theory_rewriterules_preprocess.h b/src/theory/rewriterules/theory_rewriterules_preprocess.h
deleted file mode 100644
index cc24357c6..000000000
--- a/src/theory/rewriterules/theory_rewriterules_preprocess.h
+++ /dev/null
@@ -1,176 +0,0 @@
-/*********************                                                        */
-/*! \file theory_rewriterules_preprocess.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief One utilitise for rewriterules definition
- **
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H
-#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H
-
-#include <vector>
-#include <ext/hash_set>
-#include <ext/hash_map>
-#include "expr/expr.h"
-#include "expr/node.h"
-#include "theory/rewriterules/theory_rewriterules_params.h"
-#include "theory/uf/theory_uf.h"
-
-namespace CVC4 {
-namespace theory {
-namespace rewriterules {
-
-namespace rewriter {
-
-  typedef Node TMPNode;
-  typedef std::vector<Node> Subst;
-  typedef std::vector<Expr> ESubst;
-  typedef std::vector<TMPNode> TSubst;
-
-  struct Step{
-
-    /** match the node and add in Vars the found variables */
-    virtual Node run(TMPNode node) = 0;
-    virtual bool add(TMPNode pattern, TMPNode body, Subst & pvars, Subst & vars) = 0;
-  };/* struct Step */
-
-  struct FinalStep : Step {
-    Node body;
-    TSubst vars;
-
-    Node subst(Subst & subst){
-      return body.substitute(vars.begin(), vars.end(),
-                             subst.begin(), subst.end());
-    }
-
-  };/* struct FinalStep */
-
-  typedef std::hash_map< Node, int, NodeHashFunction > PVars;
-
-  struct Pattern : FinalStep{
-    Node pattern;
-    PVars pattern_vars;
-
-    Node run(TMPNode node){
-      Subst vars = Subst(pattern_vars.size(),Node::null());
-
-      typedef std::vector<std::pair<TMPNode,TMPNode> > tstack;
-      tstack stack(1,std::make_pair(node,pattern)); // t * pat
-
-      while(!stack.empty()){
-        const std::pair<TMPNode,TMPNode> p = stack.back(); stack.pop_back();
-        const TMPNode & t = p.first;
-        const TMPNode & pat = p.second;
-
-        // pat is a variable
-        if( pat.getKind() == kind::INST_CONSTANT ||
-            pat.getKind() == kind::VARIABLE){
-          PVars::iterator i = pattern_vars.find(pat);
-          Assert(i != pattern_vars.end());
-          if(vars[i->second].isNull()) vars[i->second] = t;
-          if(vars[i->second] == t) continue;
-          return Node::null();
-        };
-
-        // t is not an UF application
-        if( t.getKind() != kind::APPLY_UF ){
-          if (t == pat) continue;
-          else return Node::null();
-        };
-
-        //different UF_application
-        if( t.getOperator() != pat.getOperator() ) return Node::null();
-
-        //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]));
-        };
-      }
-
-      // Matching is done
-      return subst(vars);
-    }
-
-    bool add(TMPNode pattern, TMPNode body, Subst & pvars, Subst & vars){
-      return false;
-    }
-    
-  };/* struct Pattern */
-
-
-  struct Args : Step {
-    typedef std::vector<Pattern> Patterns;
-    Patterns d_matches;
-
-    Node run(TMPNode node){
-      Node n;
-      for (Patterns::iterator i = d_matches.begin();
-           i != d_matches.end() && n.isNull(); ++i){
-        Debug("rewriterules-rewrite") << "test?" << i->pattern << std::endl;
-        n = i->run(node);
-      }
-      return n;
-    }
-
-    bool add(TMPNode pattern, TMPNode body, Subst & pvars, Subst & vars){
-      Debug("rewriterules-rewrite") << "theoryrewrite::Args::add" << "("
-                                    << d_matches.size() << ")"
-                                    << pattern << "->" << body << std::endl;
-      d_matches.push_back(Pattern());
-      Pattern & p = d_matches.back();
-      p.body = body;
-      p.vars.reserve(vars.size());
-      for( size_t i=0; i < vars.size(); i++ ){
-        p.vars.push_back(vars[i]);
-      };
-      p.pattern = pattern;
-      for( size_t i=0; i < pvars.size(); i++ ){
-        p.pattern_vars[pvars[i]] = i;
-      };
-      return true;
-    };
-
-    void clear(){
-      d_matches.clear();
-    }
-  };/* struct Args */
-
-class RRPpRewrite : public uf::TheoryUF::PpRewrite {
-  Args d_pattern;
-public:
-  Node ppRewrite(TNode node){
-    Debug("rewriterules-rewrite") << "rewrite?" << node << std::endl;
-    Node t = d_pattern.run(node);
-    Debug("rewriterules-rewrite") << "rewrite:" << node
-                                  << (t.isNull()? " to": " to ")
-                                  << t << std::endl;
-    if (t.isNull()) return node;
-    else return t;
-  }
-
-  bool addRewritePattern(TMPNode pattern, TMPNode body,
-                                Subst & pvars, Subst & vars){
-    return d_pattern.add(pattern,body,pvars,vars);
-  }
-
-};/* class RRPpRewrite */
-
-
-
-}/* CVC4::theory::rewriterules::rewriter namespace */
-
-}/* CVC4::theory::rewriterules namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H */
diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h
deleted file mode 100644
index 511ef3515..000000000
--- a/src/theory/rewriterules/theory_rewriterules_rewriter.h
+++ /dev/null
@@ -1,115 +0,0 @@
-/*********************                                                        */
-/*! \file theory_rewriterules_rewriter.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_REWRITER_H
-#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_REWRITER_H
-
-#include "theory/rewriter.h"
-#include "theory/rewriter_attributes.h"
-
-namespace CVC4 {
-namespace theory {
-namespace rewriterules {
-
-class TheoryRewriterulesRewriter {
-public:
-
-  /**
-   * Rewrite a node into the normal form for the theory of rewriterules.
-   * Called in post-order (really reverse-topological order) when
-   * traversing the expression DAG during rewriting.  This is the
-   * main function of the rewriter, and because of the ordering,
-   * it can assume its children are all rewritten already.
-   *
-   * This function can return one of three rewrite response codes
-   * along with the rewritten node:
-   *
-   *   REWRITE_DONE indicates that no more rewriting is needed.
-   *   REWRITE_AGAIN means that the top-level expression should be
-   *     rewritten again, but that its children are in final form.
-   *   REWRITE_AGAIN_FULL means that the entire returned expression
-   *     should be rewritten again (top-down with preRewrite(), then
-   *     bottom-up with postRewrite()).
-   *
-   * Even if this function returns REWRITE_DONE, if the returned
-   * expression belongs to a different theory, it will be fully
-   * rewritten by that theory's rewriter.
-   */
-  static RewriteResponse postRewrite(TNode node) {
-
-    // Implement me!
-
-    // This default implementation
-    return RewriteResponse(REWRITE_DONE, node);
-  }
-
-  /**
-   * Rewrite a node into the normal form for the theory of rewriterules
-   * in pre-order (really topological order)---meaning that the
-   * children may not be in the normal form.  This is an optimization
-   * for theories with cancelling terms (e.g., 0 * (big-nasty-expression)
-   * in arithmetic rewrites to 0 without the need to look at the big
-   * nasty expression).  Since it's only an optimization, the
-   * implementation here can do nothing.
-   */
-  static RewriteResponse preRewrite(TNode node) {
-    // do nothing
-    return RewriteResponse(REWRITE_DONE, node);
-  }
-
-  /**
-   * Initialize the rewriter.
-   */
-  static inline void init() {
-    // nothing to do
-  }
-
-  /**
-   * Shut down the rewriter.
-   */
-  static inline void shutdown() {
-    // nothing to do
-  }
-
-};/* class TheoryRewriterulesRewriter */
-
-}/* CVC4::theory::rewriterules namespace */
-
-template<>
-struct RewriteAttibute<THEORY_REWRITERULES> {
-  static Node getPreRewriteCache(TNode node) throw() {
-    return node;
-  }
-
-  static void setPreRewriteCache(TNode node, TNode cache) throw() { }
-
-  static Node getPostRewriteCache(TNode node) throw() {
-    return node;
-  }
-
-  static void setPostRewriteCache(TNode node, TNode cache) throw() { }
-
-  typedef expr::Attribute< RewriteCacheTag<true, THEORY_REWRITERULES>, Node> pre_rewrite;
-  typedef expr::Attribute< RewriteCacheTag<false, THEORY_REWRITERULES>, Node> post_rewrite;
-};
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_REWRITER_H */
diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp
deleted file mode 100644
index 38e22ed64..000000000
--- a/src/theory/rewriterules/theory_rewriterules_rules.cpp
+++ /dev/null
@@ -1,403 +0,0 @@
-/*********************                                                        */
-/*! \file theory_rewriterules_rules.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Francois Bobot
- ** Minor contributors (to current version): Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Deals with rewrite rules ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/rewriterules/theory_rewriterules_rules.h"
-#include "theory/rewriterules/theory_rewriterules_params.h"
-#include "theory/rewriterules/theory_rewriterules_preprocess.h"
-#include "theory/rewriterules/theory_rewriterules.h"
-#include "theory/rewriterules/options.h"
-
-#include "theory/quantifiers/term_database.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::rewriterules;
-using namespace CVC4::theory::rrinst;
-
-
-namespace CVC4 {
-namespace theory {
-namespace rewriterules {
-
-// TODO replace by a real dictionnary
-// We should create a real substitution? slower more precise
-// We don't do that often
-bool nonunifiable( TNode t0, TNode pattern, const std::vector<Node> & vars){
-  typedef std::vector<std::pair<TNode,TNode> > tstack;
-  tstack stack(1,std::make_pair(t0,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;
-}
-
-
-void TheoryRewriteRules::computeMatchBody ( const RewriteRule * rule,
-                                            size_t start){
-  std::vector<TNode> stack(1,rule->new_terms);
-
-  while(!stack.empty()){
-    Node t = stack.back(); stack.pop_back();
-
-    // We don't want to consider variable in t
-    if( std::find(rule->free_vars.begin(), rule->free_vars.end(), t)
-        != rule->free_vars.end()) continue;
-    // t we want to consider only UF function
-    if( t.getKind() == APPLY_UF ){
-      for(size_t rid = start, end = d_rules.size(); rid < end; ++rid) {
-        RewriteRule * r = d_rules[rid];
-        if(r->d_split || r->trigger_for_body_match == NULL) continue;
-        //the split rules are not computed and the one with multi-pattern
-        if( !nonunifiable(t, r->trigger_for_body_match->d_pattern, rule->free_vars)){
-          rule->body_match.push_back(std::make_pair(t,r));
-        }
-      }
-    }
-
-    //put the children on the stack
-    for( size_t i=0; i < t.getNumChildren(); i++ ){
-      stack.push_back(t[i]);
-    };
-
-  }
-}
-
-inline void addPattern(TheoryRewriteRules & re,
-                       TNode tri,
-                       std::vector<Node> & pattern,
-                       std::vector<Node> & vars,
-                       std::vector<Node> & inst_constants,
-                       TNode r){
-  if (tri.getKind() == kind::NOT && tri[0].getKind() == kind::APPLY_UF)
-    tri = tri[0];
-  pattern.push_back(
-                    options::rewriteRulesAsAxioms()?
-                    static_cast<Node>(tri):
-                    re.getQuantifiersEngine()->getTermDatabase()->
-                    convertNodeToPattern(tri,r,vars,inst_constants));
-}
-
-/*** Check that triggers contains all the variables */
-void checkPatternVarsAux(TNode pat,const std::vector<Node> & vars,
-                         std::vector<bool> & seen){
-  for(size_t id=0;id < vars.size(); ++id){
-    if(pat == vars[id]){
-      seen[id]=true;
-      break;
-    };
-  };
-  for(Node::iterator i = pat.begin(); i != pat.end(); ++i) {
-    checkPatternVarsAux(*i,vars,seen);
-  };
-}
-
-bool checkPatternVars(const std::vector<Node> & pattern,
-                      const std::vector<Node> & vars){
-  std::vector<bool> seen(vars.size(),false);
-  for(std::vector<Node>::const_iterator i = pattern.begin();
-      i != pattern.end(); ++i) {
-    checkPatternVarsAux(*i,vars,seen);
-  };
-  return (find(seen.begin(),seen.end(),false) == seen.end());
-}
-
-/** Main function for construction of RewriteRule */
-void TheoryRewriteRules::addRewriteRule(const Node r)
-{
-  Assert(r.getKind() == kind::REWRITE_RULE);
-  Kind rrkind = r[2].getKind();
-  /*   Replace variables by Inst_* variable and tag the terms that
-       contain them */
-  std::vector<Node> vars;
-  vars.reserve(r[0].getNumChildren());
-  for( Node::const_iterator v = r[0].begin(); v != r[0].end(); ++v ){
-    vars.push_back(*v);
-  };
-  /* Instantiation version */
-  std::vector<Node> inst_constants = createInstVariable(r,vars);
-  /* Body/Remove_term/Guards/Triggers */
-  Node body = r[2][1];
-  TNode new_terms = r[2][1];
-  std::vector<Node> guards;
-  std::vector<Node> pattern;
-  std::vector<Node> to_remove;  /* "remove" the terms from the database
-                                   when fired */
-  /* shortcut */
-  TNode head = r[2][0];
-  TypeNode booleanType = NodeManager::currentNM()->booleanType();
-  switch(rrkind){
-  case kind::RR_REWRITE:
-    /* Equality */
-    to_remove.push_back(head);
-    addPattern(*this,head,pattern,vars,inst_constants,r);
-    if(head.getType(false) == booleanType) body = head.iffNode(body);
-    else body = head.eqNode(body);
-    break;
-  case kind::RR_REDUCTION:
-    /** Add head to remove */
-      for(Node::iterator i = head.begin(); i != head.end(); ++i) {
-        to_remove.push_back(*i);
-      };
-  case kind::RR_DEDUCTION:
-    /** Add head to guards and pattern */
-    switch(head.getKind()){
-    case kind::AND:
-      guards.reserve(head.getNumChildren());
-      for(Node::iterator i = head.begin(); i != head.end(); ++i) {
-        guards.push_back(*i);
-        addPattern(*this,*i,pattern,vars,inst_constants,r);
-      };
-      break;
-    default:
-      if (head != d_true){
-        guards.push_back(head);
-        addPattern(*this,head,pattern,vars,inst_constants,r);
-      };
-      /** otherwise guards is empty */
-    };
-    break;
-  default:
-    Unreachable("RewriteRules can be of only three kinds");
-  };
-  /* Add the other guards */
-  TNode g = r[1];
-  switch(g.getKind()){
-  case kind::AND:
-    guards.reserve(g.getNumChildren());
-    for(Node::iterator i = g.begin(); i != g.end(); ++i) {
-      guards.push_back(*i);
-    };
-    break;
-  default:
-    if (g != d_true) guards.push_back(g);
-    /** otherwise guards is empty */
-  };
-  /* Add the other triggers */
-  if( r[2].getNumChildren() >= 3 )
-    for(Node::iterator i = r[2][2][0].begin(); i != r[2][2][0].end(); ++i) {
-      // todo test during typing that its a good term (no not, atom, or term...)
-      addPattern(*this,*i,pattern,vars,inst_constants,r);
-    };
-  // Assert(pattern.size() == 1, "currently only single pattern are supported");
-
-
-
-
-  //If we convert to usual axioms
-  if(options::rewriteRulesAsAxioms()){
-    NodeBuilder<> forallB(kind::FORALL);
-    forallB << r[0];
-    NodeBuilder<> guardsB(kind::AND);
-    guardsB.append(guards);
-    forallB << normalizeConjunction(guardsB).impNode(body);
-    NodeBuilder<> patternB(kind::INST_PATTERN);
-    patternB.append(pattern);
-    NodeBuilder<> patternListB(kind::INST_PATTERN_LIST);
-    patternListB << static_cast<Node>(patternB);
-    forallB << static_cast<Node>(patternListB);
-    Node lem = (Node) forallB;
-    lem = Rewriter::rewrite(lem);
-    QRewriteRuleAttribute qra;
-    lem.setAttribute(qra,r);
-    getOutputChannel().lemma(lem);
-    return;
-  }
-
-  //turn all to propagate
-  // if(true){
-  //   NodeBuilder<> guardsB(kind::AND);
-  //   guardsB.append(guards);
-  //   body = normalizeConjunction(guardsB).impNode(body);
-  //   guards.clear();
-  //   rrkind = kind::RR_DEDUCTION;
-  // }
-
-
-  //Every variable must be seen in the pattern
-  if (!checkPatternVars(pattern,inst_constants)){
-    Warning() << Node::setdepth(-1) << "The rule" << r <<
-      " has been removed since it doesn't contain every variables."
-              << std::endl;
-    return;
-  }
-
-
-  //Add to direct rewrite rule
-  bool directrr = false;
-  if(direct_rewrite &&
-     guards.size() == 0 && rrkind == kind::RR_REWRITE
-     && pattern.size() == 1){
-    directrr = addRewritePattern(pattern[0],new_terms, inst_constants, vars);
-  }
-
-
-  // final construction
-  Trigger trigger = createTrigger(r,pattern);
-  ApplyMatcher * applymatcher =
-    pattern.size() == 1 && pattern[0].getKind() == kind::APPLY_UF?
-    new ApplyMatcher(pattern[0],getQuantifiersEngine()) : NULL;
-  RewriteRule * rr = new RewriteRule(*this, trigger, applymatcher,
-                                     guards, body, new_terms,
-                                     vars, inst_constants, to_remove,
-                                     directrr);
-  /** other -> rr */
-  if(compute_opt && !rr->d_split) computeMatchBody(rr);
-  d_rules.push_back(rr);
-  /** rr -> all (including himself) */
-  if(compute_opt && !rr->d_split)
-    for(size_t rid = 0, end = d_rules.size(); rid < end; ++rid)
-      computeMatchBody(d_rules[rid],
-                       d_rules.size() - 1);
-
-  Debug("rewriterules::new") << "created rewriterule"<< (rr->d_split?"(split)":"") << ":(" << d_rules.size() - 1 << ")"
-                        << *rr << std::endl;
-
-}
-
-
-bool willDecide(TNode node, bool positive = true){
-  /* TODO something better */
-  switch(node.getKind()) {
-  case AND:
-    return !positive;
-  case OR:
-    return positive;
-  case IFF:
-    return true;
-  case XOR:
-    return true;
-  case IMPLIES:
-    return true;
-  case ITE:
-    return true;
-  case NOT:
-    return willDecide(node[0],!positive);
-  default:
-    return false;
-  }
-}
-
-static size_t id_next = 0;
-RewriteRule::RewriteRule(TheoryRewriteRules & re,
-                         Trigger & tr, ApplyMatcher * applymatcher,
-                         std::vector<Node> & g, Node b, TNode nt,
-                         std::vector<Node> & fv,std::vector<Node> & iv,
-                         std::vector<Node> & to_r, bool drr) :
-  id(++id_next), d_split(willDecide(b)),
-  trigger(tr), body(b), new_terms(nt), free_vars(), inst_vars(),
-  body_match(re.getSatContext()),trigger_for_body_match(applymatcher),
-  d_cache(re.getSatContext(),re.getQuantifiersEngine()), directrr(drr){
-  free_vars.swap(fv); inst_vars.swap(iv); guards.swap(g); to_remove.swap(to_r);
-};
-
-
-bool RewriteRule::inCache(TheoryRewriteRules & re, rrinst::InstMatch & im)const{
-  bool res = !d_cache.addInstMatch(im);
-  Debug("rewriterules::matching") << "rewriterules::cache " << im
-                                  << (res ? " HIT" : " MISS") << std::endl;
-  return res;
-};
-
-/** A rewrite rule */
-void RewriteRule::toStream(std::ostream& out) const{
-  out << "[" << id << "] ";
-  for(std::vector<Node>::const_iterator
-        iter = guards.begin(); iter != guards.end(); ++iter){
-    out << *iter;
-  };
-  out << "=>" << body << std::endl;
-  out << "{";
-  for(BodyMatch::const_iterator
-        iter = body_match.begin(); iter != body_match.end(); ++iter){
-    out << (*iter).first << "[" << (*iter).second->id << "]" << ",";
-  };
-  out << "}" << (directrr?"*":"") << std::endl;
-}
-
-RewriteRule::~RewriteRule(){
-  Debug("rewriterule::stats") << *this
-                             << "  (" << nb_matched
-                             << ","   << nb_applied
-                             << ","   << nb_propagated
-                             << ")" << std::endl;
-  delete(trigger_for_body_match);
-}
-
-bool TheoryRewriteRules::addRewritePattern(TNode pattern, TNode body,
-                                           rewriter::Subst & pvars,
-                                           rewriter::Subst & vars){
-  Assert(pattern.getKind() == kind::APPLY_UF);
-  TNode op = pattern.getOperator();
-  TheoryRewriteRules::RegisterRRPpRewrite::iterator i =
-    d_registeredRRPpRewrite.find(op);
-
-  rewriter::RRPpRewrite * p;
-  if (i == d_registeredRRPpRewrite.end()){
-    p = new rewriter::RRPpRewrite();
-    d_registeredRRPpRewrite.insert(std::make_pair(op,p));
-    ((uf::TheoryUF*)getQuantifiersEngine()->getTheoryEngine()->theoryOf( THEORY_UF ))->
-      registerPpRewrite(op,p);
-  } else p = i->second;
-
-  return p->addRewritePattern(pattern,body,pvars,vars);
-
-}
-
-std::vector<Node> TheoryRewriteRules::createInstVariable( Node r, 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 );
-    InstConstantAttribute ica;
-    ic.setAttribute(ica,r);
-    //also set the no-match attribute
-    NoMatchAttribute nma;
-    ic.setAttribute(nma,true);
-  };
-  return inst_constant;
-}
-
-
-}/* CVC4::theory::rewriterules namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/rewriterules/theory_rewriterules_rules.h b/src/theory/rewriterules/theory_rewriterules_rules.h
deleted file mode 100644
index 308194667..000000000
--- a/src/theory/rewriterules/theory_rewriterules_rules.h
+++ /dev/null
@@ -1,37 +0,0 @@
-/*********************                                                        */
-/*! \file theory_rewriterules_rules.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Rewrite Engine classes
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_RULES_H
-#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_RULES_H
-
-#include "theory/rewriterules/theory_rewriterules.h"
-#include "theory/rewriterules/theory_rewriterules_params.h"
-
-namespace CVC4 {
-namespace theory {
-namespace rewriterules {
-
-inline std::ostream& operator <<(std::ostream& stream, const RewriteRule& r) {
-  r.toStream(stream);
-  return stream;
-}
-
-}/* CVC4::theory::rewriterules namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_RULES_H */
diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h
deleted file mode 100644
index 28b10f91f..000000000
--- a/src/theory/rewriterules/theory_rewriterules_type_rules.h
+++ /dev/null
@@ -1,35 +0,0 @@
-/*********************                                                        */
-/*! \file theory_rewriterules_type_rules.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Francois Bobot
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_TYPE_RULES_H
-#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_TYPE_RULES_H
-
-#include "node_manager.h"
-
-namespace CVC4 {
-namespace theory {
-namespace rewriterules {
-
-
-
-}/* CVC4::theory::rewriterules namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_TYPE_RULES_H */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 45c9402ab..33ff18126 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1639,22 +1639,20 @@ void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) {
 
 void TheoryEngine::checkTheoryAssertionsWithModel() {
   for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
-    if(theoryId != THEORY_REWRITERULES) {
-      Theory* theory = d_theoryTable[theoryId];
-      if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
-        for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
-              it_end = theory->facts_end();
-            it != it_end;
-            ++it) {
-          Node assertion = (*it).assertion;
-          Node val = getModel()->getValue(assertion);
-          if(val != d_true) {
-            stringstream ss;
-            ss << theoryId << " has an asserted fact that the model doesn't satisfy." << endl
-               << "The fact: " << assertion << endl
-               << "Model value: " << val << endl;
-            InternalError(ss.str());
-          }
+    Theory* theory = d_theoryTable[theoryId];
+    if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
+      for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
+            it_end = theory->facts_end();
+          it != it_end;
+          ++it) {
+        Node assertion = (*it).assertion;
+        Node val = getModel()->getValue(assertion);
+        if(val != d_true) {
+          stringstream ss;
+          ss << theoryId << " has an asserted fact that the model doesn't satisfy." << endl
+             << "The fact: " << assertion << endl
+             << "Model value: " << val << endl;
+          InternalError(ss.str());
         }
       }
     }