drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine

47 files changed, 1252 insertions, 2202 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index b71f07852..b2d1b9f09 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -43,9 +43,7 @@ libarith_la_SOURCES = \
 	arith_unate_lemma_mode.h \
 	arith_unate_lemma_mode.cpp \
 	arith_propagation_mode.h \
-	arith_propagation_mode.cpp \
-	theory_arith_instantiator.h \
-	theory_arith_instantiator.cpp
+	arith_propagation_mode.cpp 
 
 EXTRA_DIST = \
 	kinds \
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 0be7d31a5..07cfcc9e5 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -6,7 +6,6 @@
 
 theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h"
 typechecker "theory/arith/theory_arith_type_rules.h"
-instantiator ::CVC4::theory::arith::InstantiatorTheoryArith "theory/arith/theory_arith_instantiator.h"
 
 properties stable-infinite
 properties check propagate ppStaticLearn presolve notifyRestart
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index ad041208d..6a83c501b 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -50,9 +50,12 @@
 
 namespace CVC4 {
 namespace theory {
-namespace arith {
 
-class InstStrategySimplex;
+namespace quantifiers {
+  class InstStrategySimplex;
+}
+
+namespace arith {
 
 /**
  * Implementation of QF_LRA.
@@ -60,7 +63,7 @@ class InstStrategySimplex;
  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  */
 class TheoryArith : public Theory {
-  friend class InstStrategySimplex;
+  friend class quantifiers::InstStrategySimplex;
 private:
   bool d_nlIncomplete;
   // TODO A better would be:
diff --git a/src/theory/arith/theory_arith_instantiator.h b/src/theory/arith/theory_arith_instantiator.h
deleted file mode 100644
index 70bc97bd8..000000000
--- a/src/theory/arith/theory_arith_instantiator.h
+++ /dev/null
@@ -1,110 +0,0 @@
-/*********************                                                        */
-/*! \file theory_arith_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief instantiator_arith_instantiator
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__INSTANTIATOR_ARITH_H
-#define __CVC4__INSTANTIATOR_ARITH_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/arith/arithvar_node_map.h"
-
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class TheoryArith;
-class InstantiatorTheoryArith;
-
-class InstStrategySimplex : public InstStrategy{
-private:
-  /** delta */
-  std::map< TypeNode, Node > d_deltas;
-  /** for each quantifier, simplex rows */
-  std::map< Node, std::vector< ArithVar > > d_instRows;
-  /** tableaux */
-  std::map< ArithVar, Node > d_tableaux_term;
-  std::map< ArithVar, std::map< Node, Node > > d_tableaux_ce_term;
-  std::map< ArithVar, std::map< Node, Node > > d_tableaux;
-  /** ce tableaux */
-  std::map< ArithVar, std::map< Node, Node > > d_ceTableaux;
-  /** get value */
-  Node getTableauxValue( Node n, bool minus_delta = false );
-  Node getTableauxValue( ArithVar v, bool minus_delta = false );
-  /** do instantiation */
-  bool doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var );
-  bool doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
-  /** add term to row */
-  void addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t );
-  /** get arith theory */
-  TheoryArith* getTheoryArith();
-  /** print debug */
-  void debugPrint( const char* c );
-private:
-  /** InstantiatorTheoryUf class */
-  InstantiatorTheoryArith* d_th;
-  /** */
-  int d_counter;
-  /** negative one */
-  Node d_negOne;
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstStrategySimplex( InstantiatorTheoryArith* th, QuantifiersEngine* ie );
-  ~InstStrategySimplex(){}
-  /** identify */
-  std::string identify() const { return std::string("Simplex"); }
-
-  class Statistics {
-  public:
-    IntStat d_instantiations;
-    IntStat d_instantiations_minus;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
-};
-
-class InstantiatorTheoryArith : public Instantiator{
-  friend class QuantifiersEngine;
-  friend class InstStrategySimplex;
-  friend class InstStrategySimplexUfMatch;
-public:
-  InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th);
-  ~InstantiatorTheoryArith() {}
-
-  /** assertNode function, assertion is asserted to theory */
-  void assertNode( Node assertion );
-  /** Pre-register a term.  Done one time for a Node, ever. */
-  void preRegisterTerm( Node t );
-  /** identify */
-  std::string identify() const { return std::string("InstantiatorTheoryArith"); }
-private:
-  /**  reset instantiation */
-  void processResetInstantiationRound( Theory::Effort effort );
-  /** process at effort */
-  int process( Node f, Theory::Effort effort, int e );
-
-
-};/* class InstantiatiorTheoryArith  */
-
-}
-}
-}
-
-#endif
\ No newline at end of file
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index 8b8a5bd48..be3f25ef5 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -17,8 +17,6 @@ libarrays_la_SOURCES = \
 	array_info.cpp \
 	static_fact_manager.h \
 	static_fact_manager.cpp \
-	theory_arrays_instantiator.h \
-	theory_arrays_instantiator.cpp \
 	theory_arrays_model.h \
 	theory_arrays_model.cpp
 
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 46cd5781a..a731d3677 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -6,7 +6,6 @@
 
 theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
 typechecker "theory/arrays/theory_arrays_type_rules.h"
-instantiator ::CVC4::theory::arrays::InstantiatorTheoryArrays "theory/arrays/theory_arrays_instantiator.h"
 
 properties polite stable-infinite parametric
 properties check propagate presolve getNextDecisionRequest
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index b8c1ace4b..f4661c389 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -21,7 +21,6 @@
 #include <map>
 #include "theory/rewriter.h"
 #include "expr/command.h"
-#include "theory/arrays/theory_arrays_instantiator.h"
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/model.h"
 #include "theory/arrays/options.h"
@@ -721,7 +720,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
             }
           }
 
-          // Find all stores in which n[0] appears and get corresponding read terms        
+          // Find all stores in which n[0] appears and get corresponding read terms
           const CTNodeList* instores = d_infoMap.getInStores(array_eqc);
           size_t it = 0;
           for(; it < instores->size(); ++it) {
diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp
deleted file mode 100644
index 4c6c1a967..000000000
--- a/src/theory/arrays/theory_arrays_instantiator.cpp
+++ /dev/null
@@ -1,119 +0,0 @@
-/*********************                                                        */
-/*! \file theory_arrays_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: bobot
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory_arrays_instantiator class
- **/
-
-#include "theory/theory_engine.h"
-#include "theory/arrays/theory_arrays_instantiator.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/quantifiers/options.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arrays;
-
-InstantiatorTheoryArrays::InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-Instantiator( c, ie, th ){
-
-}
-
-void InstantiatorTheoryArrays::preRegisterTerm( Node t ){
-
-}
-
-void InstantiatorTheoryArrays::assertNode( Node assertion ){
-  Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl;
-  //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion );
-  if( options::cbqi() ){
-    if( assertion.hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
-    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
-    }
-  }
-}
-
-
-void InstantiatorTheoryArrays::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e ){
-  return InstStrategy::STATUS_SAT;
-}
-
-bool InstantiatorTheoryArrays::hasTerm( Node a ){
-  return ((TheoryArrays*)d_th)->getEqualityEngine()->hasTerm( a );
-}
-
-bool InstantiatorTheoryArrays::areEqual( Node a, Node b ){
-  if( a==b ){
-    return true;
-  }else if( hasTerm( a ) && hasTerm( b ) ){
-    return ((TheoryArrays*)d_th)->getEqualityEngine()->areEqual( a, b );
-  }else{
-    return false;
-  }
-}
-
-bool InstantiatorTheoryArrays::areDisequal( Node a, Node b ){
-  if( a==b ){
-    return false;
-  }else if( hasTerm( a ) && hasTerm( b ) ){
-    return ((TheoryArrays*)d_th)->getEqualityEngine()->areDisequal( a, b, false );
-  }else{
-    return false;
-  }
-}
-
-Node InstantiatorTheoryArrays::getRepresentative( Node a ){
-  if( hasTerm( a ) ){
-    return ((TheoryArrays*)d_th)->getEqualityEngine()->getRepresentative( a );
-  }else{
-    return a;
-  }
-}
-
-eq::EqualityEngine* InstantiatorTheoryArrays::getEqualityEngine(){
-  return ((TheoryArrays*)d_th)->getEqualityEngine();
-}
-
-void InstantiatorTheoryArrays::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
-  if( hasTerm( a ) ){
-    a = getEqualityEngine()->getRepresentative( a );
-    eq::EqClassIterator eqc_iter( a, getEqualityEngine() );
-    while( !eqc_iter.isFinished() ){
-      if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){
-        eqc.push_back( *eqc_iter );
-      }
-      eqc_iter++;
-    }
-  }
-}
-
-rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClasses(){
-  arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory());
-  eq::EqualityEngine* ee =
-    static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
-  return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee);
-}
-
-rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClass(){
-  arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory());
-  eq::EqualityEngine* ee =
-    static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
-  return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee);
-}
diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h
deleted file mode 100644
index accbff06b..000000000
--- a/src/theory/arrays/theory_arrays_instantiator.h
+++ /dev/null
@@ -1,61 +0,0 @@
-/*********************                                                        */
-/*! \file theory_arrays_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Instantiator for theory of arrays
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__INSTANTIATOR_THEORY_ARRAYS_H
-#define __CVC4__INSTANTIATOR_THEORY_ARRAYS_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/uf/equality_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
-class InstantiatorTheoryArrays : public Instantiator{
-  friend class QuantifiersEngine;
-protected:
-  /** reset instantiation round */
-  void processResetInstantiationRound( Theory::Effort effort );
-  /** process quantifier */
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th);
-  ~InstantiatorTheoryArrays() {}
-  /** Pre-register a term.  */
-  void preRegisterTerm( Node t );
-  /** assertNode function, assertion is asserted to theory */
-  void assertNode( Node assertion );
-  /** identify */
-  std::string identify() const { return std::string("InstantiatorTheoryArrays"); }
-public:
-  /** general queries about equality */
-  bool hasTerm( Node a );
-  bool areEqual( Node a, Node b );
-  bool areDisequal( Node a, Node b );
-  Node getRepresentative( Node a );
-  eq::EqualityEngine* getEqualityEngine();
-  void getEquivalenceClass( Node a, std::vector< Node >& eqc );
-  /** general creators of candidate generators */
-  rrinst::CandidateGenerator* getRRCanGenClasses();
-  rrinst::CandidateGenerator* getRRCanGenClass();
-};/* class Instantiatior */
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am
index b3aa318d5..323e18de9 100644
--- a/src/theory/datatypes/Makefile.am
+++ b/src/theory/datatypes/Makefile.am
@@ -10,9 +10,7 @@ libdatatypes_la_SOURCES = \
 	type_enumerator.h \
 	theory_datatypes.h \
 	datatypes_rewriter.h \
-	theory_datatypes.cpp \
-	theory_datatypes_instantiator.h \
-	theory_datatypes_instantiator.cpp
+	theory_datatypes.cpp 
 	
 EXTRA_DIST = \
 	kinds
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 3968af4dd..2e58677df 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -6,7 +6,7 @@
 
 theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h"
 typechecker "theory/datatypes/theory_datatypes_type_rules.h"
-instantiator ::CVC4::theory::datatypes::InstantiatorTheoryDatatypes "theory/datatypes/theory_datatypes_instantiator.h"
+
 
 properties check presolve parametric propagate
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 7c8f4014e..e23d9deae 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -20,7 +20,6 @@
 #include "expr/kind.h"
 #include "util/datatype.h"
 #include "util/cvc4_assert.h"
-#include "theory/datatypes/theory_datatypes_instantiator.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes_type_rules.h"
 #include "theory/model.h"
diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp
deleted file mode 100644
index f1ac2da24..000000000
--- a/src/theory/datatypes/theory_datatypes_instantiator.cpp
+++ /dev/null
@@ -1,231 +0,0 @@
-/*********************                                                        */
-/*! \file theory_datatypes_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters, bobot
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory_datatypes_instantiator class
- **/
-
-#include "theory/datatypes/theory_datatypes_instantiator.h"
-#include "theory/datatypes/theory_datatypes.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::datatypes;
-
-InstStrategyDatatypesValue::InstStrategyDatatypesValue( QuantifiersEngine* qe ) : InstStrategy( qe ){
-
-}
-
-void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){
-  Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;
-  if( e<2 ){
-    return InstStrategy::STATUS_UNFINISHED;
-  }else if( e==2 ){
-    InstMatch m;
-    for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
-      Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
-      if( i.getType().isDatatype() ){
-        Node n = getValueFor( i );
-        Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;
-        m.set(i,n);
-      }
-    }
-    //d_quantEngine->addInstantiation( f, m );
-  }
-  return InstStrategy::STATUS_UNKNOWN;
-}
-
-Node InstStrategyDatatypesValue::getValueFor( Node n ){
-  //simply get the ground value for n in the current model, if it exists,
-  //  or return an arbitrary ground term otherwise
-  if( !n.hasAttribute(InstConstantAttribute()) ){
-    return n;
-  }else{
-    return n;
-  }
-  /*  FIXME
-
-  Debug("quant-datatypes-debug")  << "get value for " << n << std::endl;
-  if( !n.hasAttribute(InstConstantAttribute()) ){
-    return n;
-  }else{
-    Assert( n.getType().isDatatype() );
-    //check if in equivalence class with ground term
-    Node rep = getRepresentative( n );
-    Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl;
-    if( !rep.hasAttribute(InstConstantAttribute()) ){
-      return rep;
-    }else{
-      if( !n.getType().isDatatype() ){
-        return n.getType().mkGroundTerm();
-      }else{
-        if( n.getKind()==APPLY_CONSTRUCTOR ){
-          std::vector< Node > children;
-          children.push_back( n.getOperator() );
-          for( int i=0; i<(int)n.getNumChildren(); i++ ){
-            children.push_back( getValueFor( n[i] ) );
-          }
-          return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
-        }else{
-          const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
-          TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels;
-          //otherwise, use which constructor the inst constant is current chosen to be
-          if( labels->find( n )!=labels->end() ){
-            TheoryDatatypes::EqList* lbl = (*labels->find( n )).second;
-            int tIndex = -1;
-            if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){
-              Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl;
-              tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr());
-            }else{
-              Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl;
-              //must find a possible choice
-              vector< bool > possibleCons;
-              possibleCons.resize( dt.getNumConstructors(), true );
-              for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {
-                Node leqn = (*j);
-                possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;
-              }
-              for( unsigned int j=0; j<possibleCons.size(); j++ ) {
-                if( possibleCons[j] ){
-                  tIndex = j;
-                  break;
-                }
-              }
-            }
-            Assert( tIndex!=-1 );
-            Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() );
-            Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl;
-            std::vector< Node > children;
-            children.push_back( cons );
-            for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) {
-              Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n );
-              if( n.hasAttribute(InstConstantAttribute()) ){
-                InstConstantAttribute ica;
-                sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) );
-              }
-              Node snn = getValueFor( sn );
-              children.push_back( snn );
-            }
-            return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
-          }else{
-            return n.getType().mkGroundTerm();
-          }
-        }
-      }
-    }
-  }
-  */
-}
-
-InstStrategyDatatypesValue::Statistics::Statistics():
-  d_instantiations("InstStrategyDatatypesValue::Instantiations_Total", 0)
-{
-  StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstStrategyDatatypesValue::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-
-
-
-InstantiatorTheoryDatatypes::InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, TheoryDatatypes* th) :
-Instantiator( c, ie, th ){
-  if( options::cbqi() ){
-    addInstStrategy( new InstStrategyDatatypesValue( ie ) );
-  }
-}
-
-void InstantiatorTheoryDatatypes::assertNode( Node assertion ){
-  Debug("quant-datatypes-assert") << "InstantiatorTheoryDatatypes::check: " << assertion << std::endl;
-  //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion );
-  if( options::cbqi() ){
-    if( assertion.hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
-    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
-    }
-  }
-}
-
-void InstantiatorTheoryDatatypes::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-int InstantiatorTheoryDatatypes::process( Node f, Theory::Effort effort, int e ){
-  return InstStrategy::STATUS_UNKNOWN;
-}
-
-bool InstantiatorTheoryDatatypes::hasTerm( Node a ){
-  return ((TheoryDatatypes*)d_th)->getEqualityEngine()->hasTerm( a );
-}
-
-bool InstantiatorTheoryDatatypes::areEqual( Node a, Node b ){
-  if( a==b ){
-    return true;
-  }else if( hasTerm( a ) && hasTerm( b ) ){
-    return ((TheoryDatatypes*)d_th)->getEqualityEngine()->areEqual( a, b );
-  }else{
-    return false;
-  }
-}
-
-bool InstantiatorTheoryDatatypes::areDisequal( Node a, Node b ){
-  if( a==b ){
-    return false;
-  }else if( hasTerm( a ) && hasTerm( b ) ){
-    return ((TheoryDatatypes*)d_th)->getEqualityEngine()->areDisequal( a, b, false );
-  }else{
-    return false;
-  }
-}
-
-Node InstantiatorTheoryDatatypes::getRepresentative( Node a ){
-  if( hasTerm( a ) ){
-    return ((TheoryDatatypes*)d_th)->getEqualityEngine()->getRepresentative( a );
-  }else{
-    return a;
-  }
-}
-
-eq::EqualityEngine* InstantiatorTheoryDatatypes::getEqualityEngine(){
-  return &((TheoryDatatypes*)d_th)->d_equalityEngine;
-}
-
-void InstantiatorTheoryDatatypes::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
-  if( hasTerm( a ) ){
-    a = getEqualityEngine()->getRepresentative( a );
-    eq::EqClassIterator eqc_iter( a, getEqualityEngine() );
-    while( !eqc_iter.isFinished() ){
-      if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){
-        eqc.push_back( *eqc_iter );
-      }
-      eqc_iter++;
-    }
-  }
-}
-
-CVC4::theory::rrinst::CandidateGenerator* InstantiatorTheoryDatatypes::getRRCanGenClass(){
-  datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes*>(getTheory());
-  eq::EqualityEngine* ee =
-    static_cast<eq::EqualityEngine*>(dt->getEqualityEngine());
-  return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee);
-}
diff --git a/src/theory/datatypes/theory_datatypes_instantiator.h b/src/theory/datatypes/theory_datatypes_instantiator.h
deleted file mode 100644
index d7806a21d..000000000
--- a/src/theory/datatypes/theory_datatypes_instantiator.h
+++ /dev/null
@@ -1,88 +0,0 @@
-/*********************                                                        */
-/*! \file theory_datatypes_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters, bobot
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief instantiator_datatypes_instantiator
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__INSTANTIATOR_DATATYPES_H
-#define __CVC4__INSTANTIATOR_DATATYPES_H
-
-#include "theory/quantifiers_engine.h"
-
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-namespace datatypes {
-
-class TheoryDatatypes;
-
-class InstStrategyDatatypesValue : public InstStrategy
-{
-private:
-  Node getValueFor( Node n );
-public:
-  //constructor
-  InstStrategyDatatypesValue( QuantifiersEngine* qe );
-  ~InstStrategyDatatypesValue(){}
-  /** reset instantiation */
-  void processResetInstantiationRound( Theory::Effort effort );
-  /** process method, returns a status */
-  int process( Node f, Theory::Effort effort, int e );
-  /** identify */
-  std::string identify() const { return std::string("InstStrategyDatatypesValue"); }
-
-  class Statistics {
-  public:
-    IntStat d_instantiations;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
-};/* class InstStrategy */
-
-
-class InstantiatorTheoryDatatypes : public Instantiator{
-  friend class QuantifiersEngine;
-public:
-  InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, TheoryDatatypes* th);
-  ~InstantiatorTheoryDatatypes() {}
-
-  /** assertNode function, assertion is asserted to theory */
-  void assertNode( Node assertion );
-  /** identify */
-  std::string identify() const { return std::string("InstantiatorTheoryDatatypes"); }
-private:
-  /**  reset instantiation */
-  void processResetInstantiationRound( Theory::Effort effort );
-  /** process at effort */
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  /** general queries about equality */
-  bool hasTerm( Node a );
-  bool areEqual( Node a, Node b );
-  bool areDisequal( Node a, Node b );
-  Node getRepresentative( Node a );
-  eq::EqualityEngine* getEqualityEngine();
-  void getEquivalenceClass( Node a, std::vector< Node >& eqc );
-    /** general creators of candidate generators */
-  CVC4::theory::rrinst::CandidateGenerator* getRRCanGenClass();
-};/* class InstantiatiorTheoryDatatypes  */
-
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 371aa5543..316af7616 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -11,16 +11,12 @@ libquantifiers_la_SOURCES = \
 	quantifiers_rewriter.h \
 	quantifiers_rewriter.cpp \
 	theory_quantifiers.cpp \
-	theory_quantifiers_instantiator.h \
-	theory_quantifiers_instantiator.cpp \
 	instantiation_engine.h \
 	instantiation_engine.cpp \
 	trigger.h \
 	trigger.cpp \
 	candidate_generator.h \
 	candidate_generator.cpp \
-	instantiator_default.h \
-	instantiator_default.cpp \
 	inst_match.h \
 	inst_match.cpp \
 	model_engine.h \
@@ -44,7 +40,11 @@ libquantifiers_la_SOURCES = \
 	inst_match_generator.h \
 	inst_match_generator.cpp \
 	macros.h \
-	macros.cpp
+	macros.cpp \
+	inst_strategy_e_matching.h \
+	inst_strategy_e_matching.cpp \
+	inst_strategy_cbqi.h \
+	inst_strategy_cbqi.cpp
 
 EXTRA_DIST = \
 	kinds \
diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index d8dceef80..d79ddee31 100644..100755
--- a/src/theory/arith/theory_arith_instantiator.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -1,337 +1,403 @@
-/*********************                                                        */
-/*! \file theory_arith_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of instantiator_arith_instantiator class
- **/
-
-#include "theory/arith/theory_arith_instantiator.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/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::arith;
-
-#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
-
-InstStrategySimplex::InstStrategySimplex( InstantiatorTheoryArith* th, QuantifiersEngine* ie ) :
-    InstStrategy( ie ), d_th( th ), d_counter( 0 ){
-  d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
-}
-
-TheoryArith* InstStrategySimplex::getTheoryArith(){
-  return (TheoryArith*)d_th->getTheory();
-}
-
-void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
-  Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
-  d_instRows.clear();
-  d_tableaux_term.clear();
-  d_tableaux.clear();
-  d_ceTableaux.clear();
-  //search for instantiation rows in simplex tableaux
-  ArithVarToNodeMap avtnm = getTheoryArith()->d_arithvarNodeMap.getArithVarToNodeMap();
-  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
-    ArithVar x = (*it).first;
-    if( getTheoryArith()->d_partialModel.hasEitherBound( x ) ){
-      Node n = (*it).second;
-      Node f;
-      NodeBuilder<> t(kind::PLUS);
-      if( n.getKind()==PLUS ){
-        for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          addTermToRow( x, n[i], f, t );
-        }
-      }else{
-        addTermToRow( x, n, f, t );
-      }
-      if( f!=Node::null() ){
-        d_instRows[f].push_back( x );
-        //this theory has constraints from f
-        Debug("quant-arith") << "Has constraints from " << f << std::endl;
-        d_th->setQuantifierActive( f );
-        //set tableaux term
-        if( t.getNumChildren()==0 ){
-          d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );
-        }else if( t.getNumChildren()==1 ){
-          d_tableaux_term[x] = t.getChild( 0 );
-        }else{
-          d_tableaux_term[x] = t;
-        }
-      }
-    }
-  }
-  //print debug
-  debugPrint( "quant-arith-debug" );
-  d_counter++;
-}
-
-int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
-  if( e<2 ){
-    return STATUS_UNFINISHED;
-  }else if( e==2 ){
-    //Notice() << f << std::endl;
-    //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;
-    //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;
-    Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl;
-    for( int j=0; j<(int)d_instRows[f].size(); j++ ){
-      ArithVar x = d_instRows[f][j];
-      if( !d_ceTableaux[x].empty() ){
-        Debug("quant-arith-simplex") << "Check row " << x << std::endl;
-        //instantiation row will be A*e + B*t = beta,
-        // where e is a vector of terms , and t is vector of ground terms.
-        // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
-        // We will construct the term ( beta - B*t)/coeff to use for e_i.
-        InstMatch m;
-        //By default, choose the first instantiation constant to be e_i.
-        Node var = d_ceTableaux[x].begin()->first;
-        if( var.getType().isInteger() ){
-          std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();
-          //try to find coefficent that is +/- 1
-          while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){
-            ++it;
-            if( it==d_ceTableaux[x].end() ){
-              var = Node::null();
-            }else{
-              var = it->first;
-            }
-          }
-          //otherwise, try one that divides all ground term coefficients? DO_THIS
-        }
-        if( !var.isNull() ){
-          Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
-          doInstantiation( f, d_tableaux_term[x], x, m, var );
-        }else{
-          Debug("quant-arith-simplex") << "Could not find var." << std::endl;
-        }
-        ////choose a new variable based on alternation strategy
-        //int index = d_counter%(int)d_th->d_ceTableaux[x].size();
-        //Node var;
-        //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){
-        //  if( index==0 ){
-        //    var = it->first;
-        //    break;
-        //  }
-        //  index--;
-        //}
-        //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );
-      }
-    }
-  }
-  return STATUS_UNKNOWN;
-}
-
-
-void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
-  if( n.getKind()==MULT ){
-    if( n[1].hasAttribute(InstConstantAttribute()) ){
-      f = n[1].getAttribute(InstConstantAttribute());
-      if( n[1].getKind()==INST_CONSTANT ){
-        d_ceTableaux[x][ n[1] ] = n[0];
-      }else{
-        d_tableaux_ce_term[x][ n[1] ] = n[0];
-      }
-    }else{
-      d_tableaux[x][ n[1] ] = n[0];
-      t << n;
-    }
-  }else{
-    if( n.hasAttribute(InstConstantAttribute()) ){
-      f = n.getAttribute(InstConstantAttribute());
-      if( n.getKind()==INST_CONSTANT ){
-        d_ceTableaux[x][ n ] = Node::null();
-      }else{
-        d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
-      }
-    }else{
-      d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
-      t << n;
-    }
-  }
-}
-
-void InstStrategySimplex::debugPrint( const char* c ){
-  ArithVarToNodeMap avtnm = getTheoryArith()->d_arithvarNodeMap.getArithVarToNodeMap();
-  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
-    ArithVar x = (*it).first;
-    Node n = (*it).second;
-    //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
-      Debug(c) << x << " : " << n << ", bounds = ";
-      if( getTheoryArith()->d_partialModel.hasLowerBound( x ) ){
-        Debug(c) << getTheoryArith()->d_partialModel.getLowerBound( x );
-      }else{
-        Debug(c) << "-infty";
-      }
-      Debug(c) << " <= ";
-      Debug(c) << getTheoryArith()->d_partialModel.getAssignment( x );
-      Debug(c) << " <= ";
-      if( getTheoryArith()->d_partialModel.hasUpperBound( x ) ){
-        Debug(c) << getTheoryArith()->d_partialModel.getUpperBound( x );
-      }else{
-        Debug(c) << "+infty";
-      }
-      Debug(c) << std::endl;
-      //Debug(c) << "   Term = " << d_tableaux_term[x] << std::endl;
-      //Debug(c) << "   ";
-      //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){
-      //  Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";
-      //}
-      //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){
-      //  Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";
-      //}
-      //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){
-      //  Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";
-      //}
-      //Debug(c) << std::endl;
-    //}
-  }
-  Debug(c) << std::endl;
-
-  for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){
-    Node f = d_quantEngine->getQuantifier( q );
-    Debug(c) << f << std::endl;
-    Debug(c) << "   Inst constants: ";
-    for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
-      if( i>0 ){
-        Debug( c ) << ", ";
-      }
-      Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
-    }
-    Debug(c) << std::endl;
-    Debug(c) << "   Instantiation rows: ";
-    for( int i=0; i<(int)d_instRows[f].size(); i++ ){
-      if( i>0 ){
-        Debug(c) << ", ";
-      }
-      Debug(c) << d_instRows[f][i];
-    }
-    Debug(c) << std::endl;
-  }
-}
-
-//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,
-// where var is an instantiation constant from f,
-// t[e] is a vector of terms containing instantiation constants from f,
-// and term is a ground term (c1*t1 + ... + cn*tn).
-// We construct the term ( beta - term )/coeff to use as an instantiation for var.
-bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){
-  //first try +delta
-  if( doInstantiation2( f, term, x, m, var ) ){
-    ++(d_statistics.d_instantiations);
-    return true;
-  }else{
-#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
-    //otherwise try -delta
-    if( doInstantiation2( f, term, x, m, var, true ) ){
-      ++(d_statistics.d_instantiations_minus);
-      ++(d_statistics.d_instantiations);
-      return true;
-    }else{
-      return false;
-    }
-#else
-    return false;
-#endif
-  }
-}
-
-bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
-  // make term ( beta - term )/coeff
-  Node beta = getTableauxValue( x, minus_delta );
-  Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
-  if( !d_ceTableaux[x][var].isNull() ){
-    if( var.getType().isInteger() ){
-      Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
-      instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal );
-    }else{
-      Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() );
-      instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
-    }
-  }
-  instVal = Rewriter::rewrite( instVal );
-  //use as instantiation value for var
-  m.set(var, instVal);
-  Debug("quant-arith") << "Add instantiation " << m << std::endl;
-  return d_quantEngine->addInstantiation( f, m );
-}
-
-Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
-  if( getTheoryArith()->d_arithvarNodeMap.hasArithVar(n) ){
-    ArithVar v = getTheoryArith()->d_arithvarNodeMap.asArithVar( n );
-    return getTableauxValue( v, minus_delta );
-  }else{
-    return NodeManager::currentNM()->mkConst( Rational(0) );
-  }
-}
-
-Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
-  const Rational& delta = getTheoryArith()->d_partialModel.getDelta();
-  DeltaRational drv = getTheoryArith()->d_partialModel.getAssignment( v );
-  Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
-  return mkRationalNode(qmodel);
-}
-
-
-
-InstStrategySimplex::Statistics::Statistics():
-  d_instantiations("InstStrategySimplex::Instantiations_Total", 0),
-  d_instantiations_minus("InstStrategySimplex::Instantiations_minus_delta", 0)
-{
-  StatisticsRegistry::registerStat(&d_instantiations);
-  StatisticsRegistry::registerStat(&d_instantiations_minus);
-}
-
-InstStrategySimplex::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_instantiations);
-  StatisticsRegistry::unregisterStat(&d_instantiations_minus);
-}
-
-
-
-
-
-
-
-InstantiatorTheoryArith::InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-Instantiator( c, ie, th ){
-  if( options::cbqi() ){
-    addInstStrategy( new InstStrategySimplex( this, d_quantEngine ) );
-  }
-}
-
-void InstantiatorTheoryArith::preRegisterTerm( Node t ){
-
-}
-
-void InstantiatorTheoryArith::assertNode( Node assertion ){
-  Debug("quant-arith-assert") << "InstantiatorTheoryArith::check: " << assertion << std::endl;
-  //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion );
-  if( options::cbqi() ){
-    if( assertion.hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
-    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
-    }
-  }
-}
-
-void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-int InstantiatorTheoryArith::process( Node f, Theory::Effort effort, int e ){
-  Debug("quant-arith") << "Arith: Try to solve (" << effort << ") for " << f << "... " << std::endl;
-  return InstStrategy::STATUS_UNKNOWN;
-}
+/*********************                                                        */

+/*! \file inst_strategy_cbqi.cpp

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

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

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

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

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

+ ** information.\endverbatim

+ **

+ ** \brief Implementation of cbqi instantiation strategies

+ **/

+

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

+#include "theory/arith/theory_arith.h"

+#include "theory/theory_engine.h"

+#include "theory/quantifiers/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::quantifiers;

+using namespace CVC4::theory::arith;

+using namespace CVC4::theory::datatypes;

+

+#define ARITH_INSTANTIATOR_USE_MINUS_DELTA

+

+InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :

+    InstStrategy( ie ), d_th( th ), d_counter( 0 ){

+  d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );

+}

+

+bool InstStrategySimplex::calculateShouldProcess( Node f ){

+  //DO_THIS

+  return false;

+}

+

+void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){

+  Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;

+  d_instRows.clear();

+  d_tableaux_term.clear();

+  d_tableaux.clear();

+  d_ceTableaux.clear();

+  //search for instantiation rows in simplex tableaux

+  ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();

+  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){

+    ArithVar x = (*it).first;

+    if( d_th->d_partialModel.hasEitherBound( x ) ){

+      Node n = (*it).second;

+      Node f;

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

+      if( n.getKind()==PLUS ){

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

+          addTermToRow( x, n[i], f, t );

+        }

+      }else{

+        addTermToRow( x, n, f, t );

+      }

+      if( f!=Node::null() ){

+        d_instRows[f].push_back( x );

+        //this theory has constraints from f

+        Debug("quant-arith") << "Has constraints from " << f << std::endl;

+        //set that we should process it

+        d_quantActive[ f ] = true;

+        //set tableaux term

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

+          d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );

+        }else if( t.getNumChildren()==1 ){

+          d_tableaux_term[x] = t.getChild( 0 );

+        }else{

+          d_tableaux_term[x] = t;

+        }

+      }

+    }

+  }

+  //print debug

+  debugPrint( "quant-arith-debug" );

+  d_counter++;

+}

+

+int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){

+  if( e<2 ){

+    return STATUS_UNFINISHED;

+  }else if( e==2 ){

+    //Notice() << f << std::endl;

+    //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;

+    //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;

+    Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl;

+    for( int j=0; j<(int)d_instRows[f].size(); j++ ){

+      ArithVar x = d_instRows[f][j];

+      if( !d_ceTableaux[x].empty() ){

+        Debug("quant-arith-simplex") << "Check row " << x << std::endl;

+        //instantiation row will be A*e + B*t = beta,

+        // where e is a vector of terms , and t is vector of ground terms.

+        // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant

+        // We will construct the term ( beta - B*t)/coeff to use for e_i.

+        InstMatch m;

+        //By default, choose the first instantiation constant to be e_i.

+        Node var = d_ceTableaux[x].begin()->first;

+        if( var.getType().isInteger() ){

+          std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();

+          //try to find coefficent that is +/- 1

+          while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){

+            ++it;

+            if( it==d_ceTableaux[x].end() ){

+              var = Node::null();

+            }else{

+              var = it->first;

+            }

+          }

+          //otherwise, try one that divides all ground term coefficients? DO_THIS

+        }

+        if( !var.isNull() ){

+          Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;

+          doInstantiation( f, d_tableaux_term[x], x, m, var );

+        }else{

+          Debug("quant-arith-simplex") << "Could not find var." << std::endl;

+        }

+        ////choose a new variable based on alternation strategy

+        //int index = d_counter%(int)d_th->d_ceTableaux[x].size();

+        //Node var;

+        //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){

+        //  if( index==0 ){

+        //    var = it->first;

+        //    break;

+        //  }

+        //  index--;

+        //}

+        //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );

+      }

+    }

+  }

+  return STATUS_UNKNOWN;

+}

+

+

+void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){

+  if( n.getKind()==MULT ){

+    if( n[1].hasAttribute(InstConstantAttribute()) ){

+      f = n[1].getAttribute(InstConstantAttribute());

+      if( n[1].getKind()==INST_CONSTANT ){

+        d_ceTableaux[x][ n[1] ] = n[0];

+      }else{

+        d_tableaux_ce_term[x][ n[1] ] = n[0];

+      }

+    }else{

+      d_tableaux[x][ n[1] ] = n[0];

+      t << n;

+    }

+  }else{

+    if( n.hasAttribute(InstConstantAttribute()) ){

+      f = n.getAttribute(InstConstantAttribute());

+      if( n.getKind()==INST_CONSTANT ){

+        d_ceTableaux[x][ n ] = Node::null();

+      }else{

+        d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );

+      }

+    }else{

+      d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );

+      t << n;

+    }

+  }

+}

+

+void InstStrategySimplex::debugPrint( const char* c ){

+  ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();

+  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){

+    ArithVar x = (*it).first;

+    Node n = (*it).second;

+    //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){

+      Debug(c) << x << " : " << n << ", bounds = ";

+      if( d_th->d_partialModel.hasLowerBound( x ) ){

+        Debug(c) << d_th->d_partialModel.getLowerBound( x );

+      }else{

+        Debug(c) << "-infty";

+      }

+      Debug(c) << " <= ";

+      Debug(c) << d_th->d_partialModel.getAssignment( x );

+      Debug(c) << " <= ";

+      if( d_th->d_partialModel.hasUpperBound( x ) ){

+        Debug(c) << d_th->d_partialModel.getUpperBound( x );

+      }else{

+        Debug(c) << "+infty";

+      }

+      Debug(c) << std::endl;

+      //Debug(c) << "   Term = " << d_tableaux_term[x] << std::endl;

+      //Debug(c) << "   ";

+      //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){

+      //  Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";

+      //}

+      //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){

+      //  Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";

+      //}

+      //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){

+      //  Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";

+      //}

+      //Debug(c) << std::endl;

+    //}

+  }

+  Debug(c) << std::endl;

+

+  for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){

+    Node f = d_quantEngine->getQuantifier( q );

+    Debug(c) << f << std::endl;

+    Debug(c) << "   Inst constants: ";

+    for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){

+      if( i>0 ){

+        Debug( c ) << ", ";

+      }

+      Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );

+    }

+    Debug(c) << std::endl;

+    Debug(c) << "   Instantiation rows: ";

+    for( int i=0; i<(int)d_instRows[f].size(); i++ ){

+      if( i>0 ){

+        Debug(c) << ", ";

+      }

+      Debug(c) << d_instRows[f][i];

+    }

+    Debug(c) << std::endl;

+  }

+}

+

+//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,

+// where var is an instantiation constant from f,

+// t[e] is a vector of terms containing instantiation constants from f,

+// and term is a ground term (c1*t1 + ... + cn*tn).

+// We construct the term ( beta - term )/coeff to use as an instantiation for var.

+bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){

+  //first try +delta

+  if( doInstantiation2( f, term, x, m, var ) ){

+    ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith);

+    return true;

+  }else{

+#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA

+    //otherwise try -delta

+    if( doInstantiation2( f, term, x, m, var, true ) ){

+      ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus);

+      return true;

+    }else{

+      return false;

+    }

+#else

+    return false;

+#endif

+  }

+}

+

+bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){

+  // make term ( beta - term )/coeff

+  Node beta = getTableauxValue( x, minus_delta );

+  Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );

+  if( !d_ceTableaux[x][var].isNull() ){

+    if( var.getType().isInteger() ){

+      Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );

+      instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal );

+    }else{

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

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

+    }

+  }

+  instVal = Rewriter::rewrite( instVal );

+  //use as instantiation value for var

+  m.set(var, instVal);

+  Debug("quant-arith") << "Add instantiation " << m << std::endl;

+  return d_quantEngine->addInstantiation( f, m );

+}

+

+Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){

+  if( d_th->d_arithvarNodeMap.hasArithVar(n) ){

+    ArithVar v = d_th->d_arithvarNodeMap.asArithVar( n );

+    return getTableauxValue( v, minus_delta );

+  }else{

+    return NodeManager::currentNM()->mkConst( Rational(0) );

+  }

+}

+

+Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){

+  const Rational& delta = d_th->d_partialModel.getDelta();

+  DeltaRational drv = d_th->d_partialModel.getAssignment( v );

+  Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );

+  return mkRationalNode(qmodel);

+}

+

+

+InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) :

+  InstStrategy( qe ), d_th( th ){

+

+}

+

+bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){

+  //DO_THIS

+  return false;

+}

+

+void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){

+

+}

+

+int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){

+  Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;

+  if( e<2 ){

+    return InstStrategy::STATUS_UNFINISHED;

+  }else if( e==2 ){

+    InstMatch m;

+    for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){

+      Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );

+      if( i.getType().isDatatype() ){

+        Node n = getValueFor( i );

+        Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;

+        m.set(i,n);

+      }

+    }

+    //d_quantEngine->addInstantiation( f, m );

+  }

+  return InstStrategy::STATUS_UNKNOWN;

+}

+

+Node InstStrategyDatatypesValue::getValueFor( Node n ){

+  //simply get the ground value for n in the current model, if it exists,

+  //  or return an arbitrary ground term otherwise

+  if( !n.hasAttribute(InstConstantAttribute()) ){

+    return n;

+  }else{

+    return n;

+  }

+  /*  FIXME

+

+  Debug("quant-datatypes-debug")  << "get value for " << n << std::endl;

+  if( !n.hasAttribute(InstConstantAttribute()) ){

+    return n;

+  }else{

+    Assert( n.getType().isDatatype() );

+    //check if in equivalence class with ground term

+    Node rep = getRepresentative( n );

+    Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl;

+    if( !rep.hasAttribute(InstConstantAttribute()) ){

+      return rep;

+    }else{

+      if( !n.getType().isDatatype() ){

+        return n.getType().mkGroundTerm();

+      }else{

+        if( n.getKind()==APPLY_CONSTRUCTOR ){

+          std::vector< Node > children;

+          children.push_back( n.getOperator() );

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

+            children.push_back( getValueFor( n[i] ) );

+          }

+          return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );

+        }else{

+          const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();

+          TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels;

+          //otherwise, use which constructor the inst constant is current chosen to be

+          if( labels->find( n )!=labels->end() ){

+            TheoryDatatypes::EqList* lbl = (*labels->find( n )).second;

+            int tIndex = -1;

+            if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){

+              Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl;

+              tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr());

+            }else{

+              Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl;

+              //must find a possible choice

+              vector< bool > possibleCons;

+              possibleCons.resize( dt.getNumConstructors(), true );

+              for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {

+                Node leqn = (*j);

+                possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;

+              }

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

+                if( possibleCons[j] ){

+                  tIndex = j;

+                  break;

+                }

+              }

+            }

+            Assert( tIndex!=-1 );

+            Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() );

+            Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl;

+            std::vector< Node > children;

+            children.push_back( cons );

+            for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) {

+              Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n );

+              if( n.hasAttribute(InstConstantAttribute()) ){

+                InstConstantAttribute ica;

+                sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) );

+              }

+              Node snn = getValueFor( sn );

+              children.push_back( snn );

+            }

+            return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );

+          }else{

+            return n.getType().mkGroundTerm();

+          }

+        }

+      }

+    }

+  }

+  */

+}

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
new file mode 100755
index 000000000..3ee423fe7
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -0,0 +1,110 @@
+/*********************                                                        */

+/*! \file inst_strategy_cbqi.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

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

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

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

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

+ ** information.\endverbatim

+ **

+ ** \brief instantiator_arith_instantiator

+ **/

+

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__INST_STRATEGT_CBQI_H

+#define __CVC4__INST_STRATEGT_CBQI_H

+

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

+#include "theory/arith/arithvar_node_map.h"

+

+#include "util/statistics_registry.h"

+

+namespace CVC4 {

+namespace theory {

+

+namespace arith {

+  class TheoryArith;

+}

+

+namespace datatypes {

+  class TheoryDatatypes;

+}

+

+namespace quantifiers {

+

+

+class InstStrategySimplex : public InstStrategy{

+protected:

+  /** calculate if we should process this quantifier */

+  bool calculateShouldProcess( Node f );

+private:

+  /** reference to theory arithmetic */

+  arith::TheoryArith* d_th;

+  /** delta */

+  std::map< TypeNode, Node > d_deltas;

+  /** for each quantifier, simplex rows */

+  std::map< Node, std::vector< arith::ArithVar > > d_instRows;

+  /** tableaux */

+  std::map< arith::ArithVar, Node > d_tableaux_term;

+  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term;

+  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux;

+  /** ce tableaux */

+  std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux;

+  /** get value */

+  Node getTableauxValue( Node n, bool minus_delta = false );

+  Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );

+  /** do instantiation */

+  bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var );

+  bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );

+  /** add term to row */

+  void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t );

+  /** print debug */

+  void debugPrint( const char* c );

+private:

+  /** */

+  int d_counter;

+  /** negative one */

+  Node d_negOne;

+  /** process functions */

+  void processResetInstantiationRound( Theory::Effort effort );

+  int process( Node f, Theory::Effort effort, int e );

+public:

+  InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );

+  ~InstStrategySimplex(){}

+  /** identify */

+  std::string identify() const { return std::string("Simplex"); }

+};

+

+

+class InstStrategyDatatypesValue : public InstStrategy

+{

+protected:

+  /** calculate if we should process this quantifier */

+  bool calculateShouldProcess( Node f );

+private:

+  /** reference to theory datatypes */

+  datatypes::TheoryDatatypes* d_th;

+  /** get value function */

+  Node getValueFor( Node n );

+public:

+  //constructor

+  InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );

+  ~InstStrategyDatatypesValue(){}

+  /** reset instantiation */

+  void processResetInstantiationRound( Theory::Effort effort );

+  /** process method, returns a status */

+  int process( Node f, Theory::Effort effort, int e );

+  /** identify */

+  std::string identify() const { return std::string("InstStrategyDatatypesValue"); }

+

+};/* class InstStrategy */

+

+}

+}

+}

+

+#endif
\ No newline at end of file
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 8c90d569a..48af334ff 100644..100755
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -1,381 +1,379 @@
-/*********************                                                        */
-/*! \file inst_strategy.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): bobot
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory uf instantiation strategies
- **/
-
-#include "theory/uf/inst_strategy.h"
-
-#include "theory/uf/theory_uf_instantiator.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/quantifiers/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::uf;
-using namespace CVC4::theory::inst;
-
-#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
-//#define MULTI_TRIGGER_FULL_EFFORT_HALF
-#define MULTI_MULTI_TRIGGERS
-
-struct sortQuantifiersForSymbol {
-  QuantifiersEngine* d_qe;
-  bool operator() (Node i, Node j) {
-    int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );
-    int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );
-    if( nqfsi<nqfsj ){
-      return true;
-    }else if( nqfsi>nqfsj ){
-      return false;
-    }else{
-      return false;
-    }
-  }
-};
-
-void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
-  //reset triggers
-  for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
-    for( int i=0; i<(int)it->second.size(); i++ ){
-      it->second[i]->resetInstantiationRound();
-      it->second[i]->reset( Node::null() );
-    }
-  }
-}
-
-int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
-  if( e==0 ){
-    return STATUS_UNFINISHED;
-  }else if( e==1 ){
-    d_counter[f]++;
-    Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl;
-    //Notice() << "Try user-provided patterns..." << std::endl;
-    for( int i=0; i<(int)d_user_gen[f].size(); i++ ){
-      bool processTrigger = true;
-      if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){
-//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
-//        processTrigger = d_counter[f]%2==0;
-//#endif
-      }
-      if( processTrigger ){
-        //if( d_user_gen[f][i]->isMultiTrigger() )
-          //Notice() << "  Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;
-        InstMatch baseMatch;
-        int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
-        //if( d_user_gen[f][i]->isMultiTrigger() )
-          //Notice() << "  Done, numInst = " << numInst << "." << std::endl;
-        //d_statistics.d_instantiations += numInst;
-        if( d_user_gen[f][i]->isMultiTrigger() ){
-          d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
-        }
-        //d_quantEngine->d_hasInstantiated[f] = true;
-      }
-    }
-    Debug("quant-uf-strategy") << "done." << std::endl;
-    //Notice() << "done" << std::endl;
-  }
-  return STATUS_UNKNOWN;
-}
-
-void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
-  //add to generators
-  std::vector< Node > nodes;
-  for( int i=0; i<(int)pat.getNumChildren(); i++ ){
-    nodes.push_back( pat[i] );
-  }
-  if( Trigger::isUsableTrigger( nodes, f ) ){
-    //extend to literal matching
-    d_quantEngine->getPhaseReqTerms( f, nodes );
-    //check match option
-    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
-    d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,
-                                                 options::smartTriggers() ) );
-  }
-}
-/*
-InstStrategyUserPatterns::Statistics::Statistics():
-  d_instantiations("InstStrategyUserPatterns::Instantiations", 0)
-{
-  StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstStrategyUserPatterns::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-*/
-
-void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
-  //reset triggers
-  for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){
-    for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
-      itt->first->resetInstantiationRound();
-      itt->first->reset( Node::null() );
-    }
-  }
-}
-
-int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
-  int peffort = f.getNumChildren()==3 ? 2 : 1;
-  //int peffort = f.getNumChildren()==3 ? 2 : 1;
-  //int peffort = 1;
-  if( e<peffort ){
-    return STATUS_UNFINISHED;
-  }else{
-    bool gen = false;
-    if( e==peffort ){
-      if( d_counter.find( f )==d_counter.end() ){
-        d_counter[f] = 0;
-        gen = true;
-      }else{
-        d_counter[f]++;
-        gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;
-      }
-    }else{
-      gen = true;
-    }
-    if( gen ){
-      generateTriggers( f );
-    }
-    Debug("quant-uf-strategy")  << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;
-    //Notice() << "Try auto-generated triggers..." << std::endl;
-    for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){
-      Trigger* tr = itt->first;
-      if( tr ){
-        bool processTrigger = itt->second;
-        if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){
-#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
-          processTrigger = d_counter[f]%2==0;
-#endif
-        }
-        if( processTrigger ){
-          //if( tr->isMultiTrigger() )
-            Debug("quant-uf-strategy-auto-gen-triggers") << "  Process " << (*tr) << "..." << std::endl;
-          InstMatch baseMatch;
-          int numInst = tr->addInstantiations( baseMatch );
-          //if( tr->isMultiTrigger() )
-            Debug("quant-uf-strategy-auto-gen-triggers") << "  Done, numInst = " << numInst << "." << std::endl;
-          //if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
-          //  d_statistics.d_instantiations_min += numInst;
-          //}else{
-          //  d_statistics.d_instantiations += numInst;
-          //}
-          if( tr->isMultiTrigger() ){
-            d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
-          }
-          //d_quantEngine->d_hasInstantiated[f] = true;
-        }
-      }
-    }
-    Debug("quant-uf-strategy") << "done." << std::endl;
-    //Notice() << "done" << std::endl;
-  }
-  return STATUS_UNKNOWN;
-}
-
-void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
-  Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
-  if( d_patTerms[0].find( f )==d_patTerms[0].end() ){
-    //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
-    d_patTerms[0][f].clear();
-    d_patTerms[1][f].clear();
-    std::vector< Node > patTermsF;
-    Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );
-    Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;
-    Debug("auto-gen-trigger") << "   ";
-    for( int i=0; i<(int)patTermsF.size(); i++ ){
-      Debug("auto-gen-trigger") << patTermsF[i] << " ";
-    }
-    Debug("auto-gen-trigger") << std::endl;
-    //extend to literal matching (if applicable)
-    d_quantEngine->getPhaseReqTerms( f, patTermsF );
-    //sort into single/multi triggers
-    std::map< Node, std::vector< Node > > varContains;
-    d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains );
-    for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
-      if( it->second.size()==f[0].getNumChildren() ){
-        d_patTerms[0][f].push_back( it->first );
-        d_is_single_trigger[ it->first ] = true;
-      }else{
-        d_patTerms[1][f].push_back( it->first );
-        d_is_single_trigger[ it->first ] = false;
-      }
-    }
-    d_made_multi_trigger[f] = false;
-    Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;
-    Debug("auto-gen-trigger") << "   ";
-    for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
-      Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " ";
-    }
-    Debug("auto-gen-trigger") << std::endl;
-    Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
-    Debug("auto-gen-trigger") << "   ";
-    for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){
-      Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " ";
-    }
-    Debug("auto-gen-trigger") << std::endl;
-  }
-
-  //populate candidate pattern term vector for the current trigger
-  std::vector< Node > patTerms;
-#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
-  //try to add single triggers first
-  for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
-    if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){
-      patTerms.push_back( d_patTerms[0][f][i] );
-    }
-  }
-  //if no single triggers exist, add multi trigger terms
-  if( patTerms.empty() ){
-    patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
-  }
-#else
-  patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() );
-  patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
-#endif
-
-  if( !patTerms.empty() ){
-    Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
-    //sort terms based on relevance
-    if( d_rlv_strategy==RELEVANCE_DEFAULT ){
-      sortQuantifiersForSymbol sqfs;
-      sqfs.d_qe = d_quantEngine;
-      //sort based on # occurrences (this will cause Trigger to select rarer symbols)
-      std::sort( patTerms.begin(), patTerms.end(), sqfs );
-      Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
-      for( int i=0; i<(int)patTerms.size(); i++ ){
-        Debug("relevant-trigger") << "   " << patTerms[i] << " (";
-        Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
-      }
-      //Notice() << "Terms based on relevance: " << std::endl;
-      //for( int i=0; i<(int)patTerms.size(); i++ ){
-      //  Notice() << "   " << patTerms[i] << " (";
-      //  Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
-      //}
-    }
-    //now, generate the trigger...
-    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
-    Trigger* tr = NULL;
-    if( d_is_single_trigger[ patTerms[0] ] ){
-      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL,
-                               options::smartTriggers() );
-      d_single_trigger_gen[ patTerms[0] ] = true;
-    }else{
-      //if we are re-generating triggers, shuffle based on some method
-      if( d_made_multi_trigger[f] ){
-#ifndef MULTI_MULTI_TRIGGERS
-        return;
-#endif
-        std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly
-      }else{
-        d_made_multi_trigger[f] = true;
-      }
-      //will possibly want to get an old trigger
-      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD,
-                               options::smartTriggers() );
-    }
-    if( tr ){
-      if( tr->isMultiTrigger() ){
-        //disable all other multi triggers
-        for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){
-          if( it->first->isMultiTrigger() ){
-            d_auto_gen_trigger[f][ it->first ] = false;
-          }
-        }
-      }
-      //making it during an instantiation round, so must reset
-      if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){
-        tr->resetInstantiationRound();
-        tr->reset( Node::null() );
-      }
-      d_auto_gen_trigger[f][tr] = true;
-      //if we are generating additional triggers...
-      if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){
-        int index = 0;
-        if( index<(int)patTerms.size() ){
-          //Notice() << "check add additional" << std::endl;
-          //check if similar patterns exist, and if so, add them additionally
-          int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
-          index++;
-          bool success = true;
-          while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
-            success = false;
-            if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
-              d_single_trigger_gen[ patTerms[index] ] = true;
-              Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,
-                                                 options::smartTriggers() );
-              if( tr2 ){
-                //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
-                tr2->resetInstantiationRound();
-                tr2->reset( Node::null() );
-                d_auto_gen_trigger[f][tr2] = true;
-              }
-              success = true;
-            }
-            index++;
-          }
-          //Notice() << "done check add additional" << std::endl;
-        }
-      }
-    }
-  }
-}
-/*
-InstStrategyAutoGenTriggers::Statistics::Statistics():
-  d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),
-  d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)
-{
-  StatisticsRegistry::registerStat(&d_instantiations);
-  StatisticsRegistry::registerStat(&d_instantiations_min);
-}
-
-InstStrategyAutoGenTriggers::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_instantiations);
-  StatisticsRegistry::unregisterStat(&d_instantiations_min);
-}
-*/
-
-void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
-}
-
-int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
-  if( e<5 ){
-    return STATUS_UNFINISHED;
-  }else{
-    if( d_guessed.find( f )==d_guessed.end() ){
-      d_guessed[f] = true;
-      Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;
-      InstMatch m;
-      if( d_quantEngine->addInstantiation( f, m ) ){
-        //++(d_statistics.d_instantiations);
-        //d_quantEngine->d_hasInstantiated[f] = true;
-      }
-    }
-    return STATUS_UNKNOWN;
-  }
-}
-/*
-InstStrategyFreeVariable::Statistics::Statistics():
-  d_instantiations("InstStrategyGuess::Instantiations", 0)
-{
-  StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstStrategyFreeVariable::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-*/
\ No newline at end of file
+/*********************                                                        */

+/*! \file inst_strategy_e_matching.cpp

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: mdeters

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

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

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

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

+ ** information.\endverbatim

+ **

+ ** \brief Implementation of e matching instantiation strategies

+ **/

+

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

+

+#include "theory/theory_engine.h"

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

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

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

+

+using namespace std;

+using namespace CVC4;

+using namespace CVC4::kind;

+using namespace CVC4::context;

+using namespace CVC4::theory;

+using namespace CVC4::theory::inst;

+using namespace CVC4::theory::quantifiers;

+

+#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER

+//#define MULTI_TRIGGER_FULL_EFFORT_HALF

+#define MULTI_MULTI_TRIGGERS

+

+struct sortQuantifiersForSymbol {

+  QuantifiersEngine* d_qe;

+  bool operator() (Node i, Node j) {

+    int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );

+    int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );

+    if( nqfsi<nqfsj ){

+      return true;

+    }else if( nqfsi>nqfsj ){

+      return false;

+    }else{

+      return false;

+    }

+  }

+};

+

+void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){

+  //reset triggers

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

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

+      it->second[i]->resetInstantiationRound();

+      it->second[i]->reset( Node::null() );

+    }

+  }

+}

+

+int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){

+  if( e==0 ){

+    return STATUS_UNFINISHED;

+  }else if( e==1 ){

+    d_counter[f]++;

+    Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl;

+    //Notice() << "Try user-provided patterns..." << std::endl;

+    for( int i=0; i<(int)d_user_gen[f].size(); i++ ){

+      bool processTrigger = true;

+      if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){

+//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF

+//        processTrigger = d_counter[f]%2==0;

+//#endif

+      }

+      if( processTrigger ){

+        //if( d_user_gen[f][i]->isMultiTrigger() )

+          //Notice() << "  Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;

+        InstMatch baseMatch;

+        int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );

+        //if( d_user_gen[f][i]->isMultiTrigger() )

+          //Notice() << "  Done, numInst = " << numInst << "." << std::endl;

+        d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;

+        if( d_user_gen[f][i]->isMultiTrigger() ){

+          d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;

+        }

+        //d_quantEngine->d_hasInstantiated[f] = true;

+      }

+    }

+    Debug("quant-uf-strategy") << "done." << std::endl;

+    //Notice() << "done" << std::endl;

+  }

+  return STATUS_UNKNOWN;

+}

+

+void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){

+  //add to generators

+  std::vector< Node > nodes;

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

+    nodes.push_back( pat[i] );

+  }

+  if( Trigger::isUsableTrigger( nodes, f ) ){

+    //extend to literal matching

+    d_quantEngine->getPhaseReqTerms( f, nodes );

+    //check match option

+    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;

+    d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,

+                                                 options::smartTriggers() ) );

+  }

+}

+/*

+InstStrategyUserPatterns::Statistics::Statistics():

+  d_instantiations("InstStrategyUserPatterns::Instantiations", 0)

+{

+  StatisticsRegistry::registerStat(&d_instantiations);

+}

+

+InstStrategyUserPatterns::Statistics::~Statistics(){

+  StatisticsRegistry::unregisterStat(&d_instantiations);

+}

+*/

+

+void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){

+  //reset triggers

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

+    for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){

+      itt->first->resetInstantiationRound();

+      itt->first->reset( Node::null() );

+    }

+  }

+}

+

+int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){

+  int peffort = f.getNumChildren()==3 ? 2 : 1;

+  //int peffort = f.getNumChildren()==3 ? 2 : 1;

+  //int peffort = 1;

+  if( e<peffort ){

+    return STATUS_UNFINISHED;

+  }else{

+    bool gen = false;

+    if( e==peffort ){

+      if( d_counter.find( f )==d_counter.end() ){

+        d_counter[f] = 0;

+        gen = true;

+      }else{

+        d_counter[f]++;

+        gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;

+      }

+    }else{

+      gen = true;

+    }

+    if( gen ){

+      generateTriggers( f );

+    }

+    Debug("quant-uf-strategy")  << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;

+    //Notice() << "Try auto-generated triggers..." << std::endl;

+    for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){

+      Trigger* tr = itt->first;

+      if( tr ){

+        bool processTrigger = itt->second;

+        if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){

+#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF

+          processTrigger = d_counter[f]%2==0;

+#endif

+        }

+        if( processTrigger ){

+          //if( tr->isMultiTrigger() )

+            Debug("quant-uf-strategy-auto-gen-triggers") << "  Process " << (*tr) << "..." << std::endl;

+          InstMatch baseMatch;

+          int numInst = tr->addInstantiations( baseMatch );

+          //if( tr->isMultiTrigger() )

+            Debug("quant-uf-strategy-auto-gen-triggers") << "  Done, numInst = " << numInst << "." << std::endl;

+          if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){

+            d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;

+          }else{

+            d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst;

+          }

+          if( tr->isMultiTrigger() ){

+            d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;

+          }

+          //d_quantEngine->d_hasInstantiated[f] = true;

+        }

+      }

+    }

+    Debug("quant-uf-strategy") << "done." << std::endl;

+    //Notice() << "done" << std::endl;

+  }

+  return STATUS_UNKNOWN;

+}

+

+void InstStrategyAutoGenTriggers::generateTriggers( Node f ){

+  Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;

+  if( d_patTerms[0].find( f )==d_patTerms[0].end() ){

+    //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy

+    d_patTerms[0][f].clear();

+    d_patTerms[1][f].clear();

+    std::vector< Node > patTermsF;

+    Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );

+    Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;

+    Debug("auto-gen-trigger") << "   ";

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

+      Debug("auto-gen-trigger") << patTermsF[i] << " ";

+    }

+    Debug("auto-gen-trigger") << std::endl;

+    //extend to literal matching (if applicable)

+    d_quantEngine->getPhaseReqTerms( f, patTermsF );

+    //sort into single/multi triggers

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

+    d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains );

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

+      if( it->second.size()==f[0].getNumChildren() ){

+        d_patTerms[0][f].push_back( it->first );

+        d_is_single_trigger[ it->first ] = true;

+      }else{

+        d_patTerms[1][f].push_back( it->first );

+        d_is_single_trigger[ it->first ] = false;

+      }

+    }

+    d_made_multi_trigger[f] = false;

+    Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;

+    Debug("auto-gen-trigger") << "   ";

+    for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){

+      Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " ";

+    }

+    Debug("auto-gen-trigger") << std::endl;

+    Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;

+    Debug("auto-gen-trigger") << "   ";

+    for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){

+      Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " ";

+    }

+    Debug("auto-gen-trigger") << std::endl;

+  }

+

+  //populate candidate pattern term vector for the current trigger

+  std::vector< Node > patTerms;

+#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER

+  //try to add single triggers first

+  for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){

+    if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){

+      patTerms.push_back( d_patTerms[0][f][i] );

+    }

+  }

+  //if no single triggers exist, add multi trigger terms

+  if( patTerms.empty() ){

+    patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );

+  }

+#else

+  patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() );

+  patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );

+#endif

+

+  if( !patTerms.empty() ){

+    Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;

+    //sort terms based on relevance

+    if( d_rlv_strategy==RELEVANCE_DEFAULT ){

+      sortQuantifiersForSymbol sqfs;

+      sqfs.d_qe = d_quantEngine;

+      //sort based on # occurrences (this will cause Trigger to select rarer symbols)

+      std::sort( patTerms.begin(), patTerms.end(), sqfs );

+      Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;

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

+        Debug("relevant-trigger") << "   " << patTerms[i] << " (";

+        Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;

+      }

+      //Notice() << "Terms based on relevance: " << std::endl;

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

+      //  Notice() << "   " << patTerms[i] << " (";

+      //  Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;

+      //}

+    }

+    //now, generate the trigger...

+    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;

+    Trigger* tr = NULL;

+    if( d_is_single_trigger[ patTerms[0] ] ){

+      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL,

+                               options::smartTriggers() );

+      d_single_trigger_gen[ patTerms[0] ] = true;

+    }else{

+      //if we are re-generating triggers, shuffle based on some method

+      if( d_made_multi_trigger[f] ){

+#ifndef MULTI_MULTI_TRIGGERS

+        return;

+#endif

+        std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly

+      }else{

+        d_made_multi_trigger[f] = true;

+      }

+      //will possibly want to get an old trigger

+      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD,

+                               options::smartTriggers() );

+    }

+    if( tr ){

+      if( tr->isMultiTrigger() ){

+        //disable all other multi triggers

+        for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){

+          if( it->first->isMultiTrigger() ){

+            d_auto_gen_trigger[f][ it->first ] = false;

+          }

+        }

+      }

+      //making it during an instantiation round, so must reset

+      if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){

+        tr->resetInstantiationRound();

+        tr->reset( Node::null() );

+      }

+      d_auto_gen_trigger[f][tr] = true;

+      //if we are generating additional triggers...

+      if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){

+        int index = 0;

+        if( index<(int)patTerms.size() ){

+          //Notice() << "check add additional" << std::endl;

+          //check if similar patterns exist, and if so, add them additionally

+          int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );

+          index++;

+          bool success = true;

+          while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){

+            success = false;

+            if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){

+              d_single_trigger_gen[ patTerms[index] ] = true;

+              Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,

+                                                 options::smartTriggers() );

+              if( tr2 ){

+                //Notice() << "Add additional trigger " << patTerms[index] << std::endl;

+                tr2->resetInstantiationRound();

+                tr2->reset( Node::null() );

+                d_auto_gen_trigger[f][tr2] = true;

+              }

+              success = true;

+            }

+            index++;

+          }

+          //Notice() << "done check add additional" << std::endl;

+        }

+      }

+    }

+  }

+}

+/*

+InstStrategyAutoGenTriggers::Statistics::Statistics():

+  d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),

+  d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)

+{

+  StatisticsRegistry::registerStat(&d_instantiations);

+  StatisticsRegistry::registerStat(&d_instantiations_min);

+}

+

+InstStrategyAutoGenTriggers::Statistics::~Statistics(){

+  StatisticsRegistry::unregisterStat(&d_instantiations);

+  StatisticsRegistry::unregisterStat(&d_instantiations_min);

+}

+*/

+

+void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){

+}

+

+int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){

+  if( e<5 ){

+    return STATUS_UNFINISHED;

+  }else{

+    if( d_guessed.find( f )==d_guessed.end() ){

+      d_guessed[f] = true;

+      Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;

+      InstMatch m;

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

+        ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);

+        //d_quantEngine->d_hasInstantiated[f] = true;

+      }

+    }

+    return STATUS_UNKNOWN;

+  }

+}

+/*

+InstStrategyFreeVariable::Statistics::Statistics():

+  d_instantiations("InstStrategyGuess::Instantiations", 0)

+{

+  StatisticsRegistry::registerStat(&d_instantiations);

+}

+

+InstStrategyFreeVariable::Statistics::~Statistics(){

+  StatisticsRegistry::unregisterStat(&d_instantiations);

+}

+*/

diff --git a/src/theory/uf/inst_strategy.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 42d401126..ea22486a6 100644..100755
--- a/src/theory/uf/inst_strategy.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -1,168 +1,132 @@
-/*********************                                                        */
-/*! \file inst_strategy.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Theory uf instantiation strategies
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__INST_STRATEGY_H
-#define __CVC4__INST_STRATEGY_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/trigger.h"
-
-#include "context/context.h"
-#include "context/context_mm.h"
-
-#include "util/statistics_registry.h"
-#include "theory/uf/theory_uf.h"
-
-namespace CVC4 {
-namespace theory {
-namespace uf {
-
-class InstantiatorTheoryUf;
-
-//instantiation strategies
-
-class InstStrategyUserPatterns : public InstStrategy{
-private:
-  /** InstantiatorTheoryUf class */
-  InstantiatorTheoryUf* d_th;
-  /** explicitly provided patterns */
-  std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
-  /** counter for quantifiers */
-  std::map< Node, int > d_counter;
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstStrategyUserPatterns( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
-      InstStrategy( ie ), d_th( th ){}
-  ~InstStrategyUserPatterns(){}
-public:
-  /** add pattern */
-  void addUserPattern( Node f, Node pat );
-  /** get num patterns */
-  int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }
-  /** get user pattern */
-  inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
-  /** identify */
-  std::string identify() const { return std::string("UserPatterns"); }
-public:
-  /** statistics class */
-  //class Statistics {
-  //public:
-  //  IntStat d_instantiations;
-  //  Statistics();
-  //  ~Statistics();
-  //};
-  //Statistics d_statistics;
-};/* class InstStrategyUserPatterns */
-
-class InstStrategyAutoGenTriggers : public InstStrategy{
-public:
-  enum {
-    RELEVANCE_NONE,
-    RELEVANCE_DEFAULT,
-  };
-private:
-  /** InstantiatorTheoryUf class */
-  InstantiatorTheoryUf* d_th;
-  /** trigger generation strategy */
-  int d_tr_strategy;
-  /** relevance strategy */
-  int d_rlv_strategy;
-  /** regeneration */
-  bool d_regenerate;
-  int d_regenerate_frequency;
-  /** generate additional triggers */
-  bool d_generate_additional;
-  /** triggers for each quantifier */
-  std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;
-  std::map< Node, int > d_counter;
-  /** single, multi triggers for each quantifier */
-  std::map< Node, std::vector< Node > > d_patTerms[2];
-  std::map< Node, bool > d_is_single_trigger;
-  std::map< Node, bool > d_single_trigger_gen;
-  std::map< Node, bool > d_made_multi_trigger;
-private:
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
-  /** generate triggers */
-  void generateTriggers( Node f );
-public:
-  InstStrategyAutoGenTriggers( InstantiatorTheoryUf* th, QuantifiersEngine* ie, int tstrt, int rstrt, int rgfr = -1 ) :
-      InstStrategy( ie ), d_th( th ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){
-    setRegenerateFrequency( rgfr );
-  }
-  ~InstStrategyAutoGenTriggers(){}
-public:
-  /** get auto-generated trigger */
-  inst::Trigger* getAutoGenTrigger( Node f );
-  /** identify */
-  std::string identify() const { return std::string("AutoGenTriggers"); }
-  /** set regenerate frequency, if fr<0, turn off regenerate */
-  void setRegenerateFrequency( int fr ){
-    if( fr<0 ){
-      d_regenerate = false;
-    }else{
-      d_regenerate_frequency = fr;
-      d_regenerate = true;
-    }
-  }
-  /** set generate additional */
-  void setGenerateAdditional( bool val ) { d_generate_additional = val; }
-public:
-  /** statistics class */
-  //class Statistics {
-  //public:
-  //  IntStat d_instantiations;
-  //  IntStat d_instantiations_min;
-  //  Statistics();
-  //  ~Statistics();
-  //};
-  //Statistics d_statistics;
-};/* class InstStrategyAutoGenTriggers */
-
-class InstStrategyFreeVariable : public InstStrategy{
-private:
-  /** InstantiatorTheoryUf class */
-  InstantiatorTheoryUf* d_th;
-  /** guessed instantiations */
-  std::map< Node, bool > d_guessed;
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstStrategyFreeVariable( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
-      InstStrategy( ie ), d_th( th ){}
-  ~InstStrategyFreeVariable(){}
-  /** identify */
-  std::string identify() const { return std::string("FreeVariable"); }
-public:
-  /** statistics class */
-  //class Statistics {
-  //public:
-  //  IntStat d_instantiations;
-  //  Statistics();
-  //  ~Statistics();
-  //};
-  //Statistics d_statistics;
-};/* class InstStrategyFreeVariable */
-
-}/* CVC4::theory::uf namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif
+/*********************                                                        */

+/*! \file inst_strategy_e_matching.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

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

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

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

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

+ ** information.\endverbatim

+ **

+ ** \brief E matching instantiation strategies

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H

+#define __CVC4__INST_STRATEGY_E_MATCHING_H

+

+#include "theory/quantifiers_engine.h"

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

+

+#include "context/context.h"

+#include "context/context_mm.h"

+

+#include "util/statistics_registry.h"

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

+

+namespace CVC4 {

+namespace theory {

+namespace quantifiers {

+

+//instantiation strategies

+

+class InstStrategyUserPatterns : public InstStrategy{

+private:

+  /** explicitly provided patterns */

+  std::map< Node, std::vector< inst::Trigger* > > d_user_gen;

+  /** counter for quantifiers */

+  std::map< Node, int > d_counter;

+  /** process functions */

+  void processResetInstantiationRound( Theory::Effort effort );

+  int process( Node f, Theory::Effort effort, int e );

+public:

+  InstStrategyUserPatterns( QuantifiersEngine* ie ) :

+      InstStrategy( ie ){}

+  ~InstStrategyUserPatterns(){}

+public:

+  /** add pattern */

+  void addUserPattern( Node f, Node pat );

+  /** get num patterns */

+  int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }

+  /** get user pattern */

+  inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }

+  /** identify */

+  std::string identify() const { return std::string("UserPatterns"); }

+};/* class InstStrategyUserPatterns */

+

+class InstStrategyAutoGenTriggers : public InstStrategy{

+public:

+  enum {

+    RELEVANCE_NONE,

+    RELEVANCE_DEFAULT,

+  };

+private:

+  /** trigger generation strategy */

+  int d_tr_strategy;

+  /** relevance strategy */

+  int d_rlv_strategy;

+  /** regeneration */

+  bool d_regenerate;

+  int d_regenerate_frequency;

+  /** generate additional triggers */

+  bool d_generate_additional;

+  /** triggers for each quantifier */

+  std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;

+  std::map< Node, int > d_counter;

+  /** single, multi triggers for each quantifier */

+  std::map< Node, std::vector< Node > > d_patTerms[2];

+  std::map< Node, bool > d_is_single_trigger;

+  std::map< Node, bool > d_single_trigger_gen;

+  std::map< Node, bool > d_made_multi_trigger;

+private:

+  /** process functions */

+  void processResetInstantiationRound( Theory::Effort effort );

+  int process( Node f, Theory::Effort effort, int e );

+  /** generate triggers */

+  void generateTriggers( Node f );

+public:

+  InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) :

+      InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){

+    setRegenerateFrequency( rgfr );

+  }

+  ~InstStrategyAutoGenTriggers(){}

+public:

+  /** get auto-generated trigger */

+  inst::Trigger* getAutoGenTrigger( Node f );

+  /** identify */

+  std::string identify() const { return std::string("AutoGenTriggers"); }

+  /** set regenerate frequency, if fr<0, turn off regenerate */

+  void setRegenerateFrequency( int fr ){

+    if( fr<0 ){

+      d_regenerate = false;

+    }else{

+      d_regenerate_frequency = fr;

+      d_regenerate = true;

+    }

+  }

+  /** set generate additional */

+  void setGenerateAdditional( bool val ) { d_generate_additional = val; }

+};/* class InstStrategyAutoGenTriggers */

+

+class InstStrategyFreeVariable : public InstStrategy{

+private:

+  /** guessed instantiations */

+  std::map< Node, bool > d_guessed;

+  /** process functions */

+  void processResetInstantiationRound( Theory::Effort effort );

+  int process( Node f, Theory::Effort effort, int e );

+public:

+  InstStrategyFreeVariable( QuantifiersEngine* qe ) :

+      InstStrategy( qe ){}

+  ~InstStrategyFreeVariable(){}

+  /** identify */

+  std::string identify() const { return std::string("FreeVariable"); }

+};/* class InstStrategyFreeVariable */

+

+}

+}/* CVC4::theory namespace */

+}/* CVC4 namespace */

+

+#endif

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 8d935a323..579c53665 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -15,10 +15,12 @@
 #include "theory/quantifiers/instantiation_engine.h"
 
 #include "theory/theory_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/inst_strategy_e_matching.h"
+#include "theory/quantifiers/inst_strategy_cbqi.h"
+#include "theory/quantifiers/trigger.h"
 
 using namespace std;
 using namespace CVC4;
@@ -26,12 +28,49 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
+using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
 QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
 
 }
 
+void InstantiationEngine::finishInit(){
+  //for UF terms
+  if( !options::finiteModelFind() || options::fmfInstEngine() ){
+    //if( options::cbqi() ){
+    //  addInstStrategy( new InstStrategyCheckCESolved( this, d_quantEngine ) );
+    //}
+    //these are the instantiation strategies for basic E-matching
+    if( options::userPatternsQuant() ){
+      d_isup = new InstStrategyUserPatterns( d_quantEngine );
+      addInstStrategy( d_isup );
+    }else{
+      d_isup = NULL;
+    }
+    InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL,
+                                                                         InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 );
+    i_ag->setGenerateAdditional( true );
+    addInstStrategy( i_ag );
+    //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
+    if( !options::finiteModelFind() ){
+      addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) );
+    }
+    //d_isup->setPriorityOver( i_ag );
+    //d_isup->setPriorityOver( i_agm );
+    //i_ag->setPriorityOver( i_agm );
+  }
+  //CBQI: FIXME
+  //for arithmetic
+  //if( options::cbqi() ){
+  //  addInstStrategy( new InstStrategySimplex( d_quantEngine ) );
+  //}
+  //for datatypes
+  //if( options::cbqi() ){
+  //  addInstStrategy( new InstStrategyDatatypesValue( d_quantEngine ) );
+  //}
+}
+
 
 bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   //if counterexample-based quantifier instantiation is active
@@ -68,9 +107,10 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   //reset the quantifiers engine
   Debug("inst-engine-ctrl") << "Reset IE" << std::endl;
   //reset the instantiators
-  for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
-    if( d_quantEngine->getInstantiator( i ) ){
-      d_quantEngine->getInstantiator( i )->resetInstantiationRound( effort );
+  for( size_t i=0; i<d_instStrategies.size(); ++i ){
+    InstStrategy* is = d_instStrategies[i];
+    if( isActiveStrategy( is ) ){
+      is->processResetInstantiationRound( effort );
     }
   }
   //iterate over an internal effort level e
@@ -90,11 +130,12 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
         //int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e;
         int e_use = e;
         if( e_use>=0 ){
-          //use each theory instantiator to instantiate f
-          for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
-            if( d_quantEngine->getInstantiator( i ) ){
-              Debug("inst-engine-debug") << "Do " << d_quantEngine->getInstantiator( i )->identify() << " " << e_use << std::endl;
-              int quantStatus = d_quantEngine->getInstantiator( i )->doInstantiation( f, effort, e_use );
+          //check each instantiation strategy
+          for( size_t i=0; i<d_instStrategies.size(); ++i ){
+            InstStrategy* is = d_instStrategies[i];
+            if( isActiveStrategy( is ) && is->shouldProcess( f ) ){
+              Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
+              int quantStatus = is->process( f, effort, e_use );
               Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
               InstStrategy::updateStatus( d_inst_round_status, quantStatus );
             }
@@ -112,13 +153,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   Debug("inst-engine") << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
   //Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
   if( !d_quantEngine->hasAddedLemma() ){
-    Debug("inst-engine-stuck") << "No instantiations produced at this state: " << std::endl;
-    for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
-      if( d_quantEngine->getInstantiator( i ) ){
-        d_quantEngine->getInstantiator( i )->debugPrint("inst-engine-stuck");
-        Debug("inst-engine-stuck") << std::endl;
-      }
-    }
+    Debug("inst-engine-stuck") << "No instantiations produced at this state." << std::endl;
     Debug("inst-engine-ctrl") << "---Fail." << std::endl;
     return false;
   }else{
@@ -238,9 +273,6 @@ void InstantiationEngine::registerQuantifier( Node f ){
   Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
   if( !doCbqi( f ) ){
     d_quantEngine->addTermToDatabase( ceBody, true );
-    //need to tell which instantiators will be responsible
-    //by default, just chose the UF instantiator
-    d_quantEngine->getInstantiator( theory::THEORY_UF )->setQuantifierActive( f );
   }
 
   //take into account user patterns
@@ -249,7 +281,7 @@ void InstantiationEngine::registerQuantifier( Node f ){
     //add patterns
     for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
       //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
-      ((uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( theory::THEORY_UF ))->addUserPattern( f, subsPat[i] );
+      addUserPattern( f, subsPat[i] );
     }
   }
 }
@@ -359,4 +391,38 @@ Node InstantiationEngine::getNextDecisionRequest(){
     }
   }
   return Node::null();
-}
\ No newline at end of file
+}
+
+void InstantiationEngine::addUserPattern( Node f, Node pat ){
+  if( d_isup ){
+    d_isup->addUserPattern( f, pat );
+  }
+}
+
+InstantiationEngine::Statistics::Statistics():
+  d_instantiations_user_patterns("InstantiationEngine::Instantiations_User_Patterns", 0),
+  d_instantiations_auto_gen("InstantiationEngine::Instantiations_Auto_Gen", 0),
+  d_instantiations_auto_gen_min("InstantiationEngine::Instantiations_Auto_Gen_Min", 0),
+  d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0),
+  d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0),
+  d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0),
+  d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0)
+{
+  StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
+  StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
+  StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min);
+  StatisticsRegistry::registerStat(&d_instantiations_guess);
+  StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
+  StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus);
+  StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes);
+}
+
+InstantiationEngine::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns);
+  StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen);
+  StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min);
+  StatisticsRegistry::unregisterStat(&d_instantiations_guess);
+  StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
+  StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
+  StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes);
+}
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index b3bbbce4a..a7ae1ae8e 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -24,9 +24,71 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class InstStrategyUserPatterns;
+
+/** instantiation strategy class */
+class InstStrategy {
+public:
+  enum Status {
+    STATUS_UNFINISHED,
+    STATUS_UNKNOWN,
+    STATUS_SAT,
+  };/* enum Status */
+protected:
+  /** reference to the instantiation engine */
+  QuantifiersEngine* d_quantEngine;
+  /** should process a quantifier */
+  std::map< Node, bool > d_quantActive;
+  /** calculate should process */
+  virtual bool calculateShouldProcess( Node f ) { return true; }
+public:
+  InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
+  virtual ~InstStrategy(){}
+
+  /** should process quantified formula f? */
+  bool shouldProcess( Node f ) {
+    if( d_quantActive.find( f )==d_quantActive.end() ){
+      d_quantActive[f] = calculateShouldProcess( f );
+    }
+    return d_quantActive[f];
+  }
+  /** reset instantiation */
+  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
+  /** process method, returns a status */
+  virtual int process( Node f, Theory::Effort effort, int e ) = 0;
+  /** update status */
+  static void updateStatus( int& currStatus, int addStatus ){
+    if( addStatus==STATUS_UNFINISHED ){
+      currStatus = STATUS_UNFINISHED;
+    }else if( addStatus==STATUS_UNKNOWN ){
+      if( currStatus==STATUS_SAT ){
+        currStatus = STATUS_UNKNOWN;
+      }
+    }
+  }
+  /** identify */
+  virtual std::string identify() const { return std::string("Unknown"); }
+};/* class InstStrategy */
+
 class InstantiationEngine : public QuantifiersModule
 {
 private:
+  /** instantiation strategies */
+  std::vector< InstStrategy* > d_instStrategies;
+  /** instantiation strategies active */
+  std::map< InstStrategy*, bool > d_instStrategyActive;
+  /** user-pattern instantiation strategy */
+  InstStrategyUserPatterns* d_isup;
+  /** is instantiation strategy active */
+  bool isActiveStrategy( InstStrategy* is ) {
+    return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
+  }
+  /** add inst strategy */
+  void addInstStrategy( InstStrategy* is ){
+    d_instStrategies.push_back( is );
+    d_instStrategyActive[is] = true;
+  }
+private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   /** status of instantiation round (one of InstStrategy::STATUS_*) */
   int d_inst_round_status;
@@ -62,6 +124,8 @@ private:
 public:
   InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
   ~InstantiationEngine(){}
+  /** initialize */
+  void finishInit();
 
   bool needsCheck( Theory::Effort e );
   void check( Theory::Effort e );
@@ -69,6 +133,23 @@ public:
   void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
   Node getNextDecisionRequest();
+  /** add user pattern */
+  void addUserPattern( Node f, Node pat );
+public:
+  /** statistics class */
+  class Statistics {
+  public:
+    IntStat d_instantiations_user_patterns;
+    IntStat d_instantiations_auto_gen;
+    IntStat d_instantiations_auto_gen_min;
+    IntStat d_instantiations_guess;
+    IntStat d_instantiations_cbqi_arith;
+    IntStat d_instantiations_cbqi_arith_minus;
+    IntStat d_instantiations_cbqi_datatypes;
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
 };/* class InstantiationEngine */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/instantiator_default.cpp b/src/theory/quantifiers/instantiator_default.cpp
deleted file mode 100644
index def3c9f58..000000000
--- a/src/theory/quantifiers/instantiator_default.cpp
+++ /dev/null
@@ -1,54 +0,0 @@
-/*********************                                                        */
-/*! \file instantiator_default.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of instantiator_default class
- **/
-
-#include "theory/quantifiers/instantiator_default.h"
-#include "theory/theory_engine.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-
-InstantiatorDefault::InstantiatorDefault(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-  Instantiator( c, ie, th ) {
-}
-
-void InstantiatorDefault::assertNode( Node assertion ){
-}
-
-void InstantiatorDefault::processResetInstantiationRound( Theory::Effort effort ){
-}
-
-int InstantiatorDefault::process( Node f, Theory::Effort effort, int e ){
-  /*
-  if( e < 4 ){
-    return InstStrategy::STATUS_UNFINISHED;
-  }else if( e == 4 ){
-    Debug("quant-default") << "Process " << f << " : " << std::endl;
-    InstMatch m;
-    for( int j=0; j<(int)d_quantEngine->getNumInstantiationConstants( f ); j++ ){
-      Node i = d_quantEngine->getInstantiationConstant( f, j );
-      Debug("quant-default") << "Getting value for " << i << std::endl;
-      if( d_quantEngine->getTheoryEngine()->theoryOf( i )==getTheory() ){    //if it belongs to this theory
-        Node val = d_th->getValue( i );
-        Debug("quant-default") << "Default Instantiate for " << d_th->getId() << ", setting " << i << " = " << val << std::endl;
-        m.set( i, val);
-      }
-    }
-    d_quantEngine->addInstantiation( f, m );
-  }
-  */
-  return InstStrategy::STATUS_UNKNOWN;
-}
diff --git a/src/theory/quantifiers/instantiator_default.h b/src/theory/quantifiers/instantiator_default.h
deleted file mode 100644
index d21499ae0..000000000
--- a/src/theory/quantifiers/instantiator_default.h
+++ /dev/null
@@ -1,46 +0,0 @@
-/*********************                                                        */
-/*! \file instantiator_default.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief instantiator_default
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H
-#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H
-
-#include <string>
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-class InstantiatorDefault : public Instantiator {
-  friend class QuantifiersEngine;
-protected:
-  /** reset instantiation round */
-  void processResetInstantiationRound(Theory::Effort effort);
-  /** process quantifier */
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstantiatorDefault(context::Context* c, QuantifiersEngine* ie, Theory* th);
-  ~InstantiatorDefault() { }
-  /** check function, assertion is asserted to theory */
-  void assertNode( Node assertion );
-  /** identify */
-  std::string identify() const { return std::string("InstantiatorDefault"); }
-};/* class InstantiatorDefault */
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATOR_DEFAULT_H */
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index c81816528..ab0e9d934 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -6,7 +6,6 @@
 
 theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
 typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
-instantiator ::CVC4::theory::quantifiers::InstantiatorTheoryQuantifiers "theory/quantifiers/theory_quantifiers_instantiator.h"
 
 properties check propagate presolve getNextDecisionRequest
 
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index c7e68acb1..2f44140c2 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -17,7 +17,6 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_model.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -25,6 +24,7 @@
 #include "theory/quantifiers/model_builder.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/inst_gen.h"
+#include "theory/quantifiers/trigger.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 456914818..bf6ea11f0 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -17,7 +17,6 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/quantifiers/options.h"
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9a26878b5..d60aa2ef4 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -106,7 +106,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
                 addedLemmas += d_op_triggers[op][i]->addTerm( n );
               }
               //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
-              d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() );
+              d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
             }
           }
         }
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 446c9285e..cfdb30f38 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -22,7 +22,6 @@
 #include "theory/quantifiers/model_engine.h"
 #include "expr/kind.h"
 #include "util/cvc4_assert.h"
-#include "theory/quantifiers/theory_quantifiers_instantiator.h"
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
deleted file mode 100644
index eabb4ceda..000000000
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
+++ /dev/null
@@ -1,73 +0,0 @@
-/*********************                                                        */
-/*! \file theory_quantifiers_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory_quantifiers_instantiator class
- **/
-
-#include "theory/quantifiers/theory_quantifiers_instantiator.h"
-#include "theory/quantifiers/theory_quantifiers.h"
-#include "theory/quantifiers/options.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::quantifiers;
-
-InstantiatorTheoryQuantifiers::InstantiatorTheoryQuantifiers(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-Instantiator( c, ie, th ){
-
-}
-
-void InstantiatorTheoryQuantifiers::assertNode( Node assertion ){
-  Debug("quant-quant-assert") << "InstantiatorTheoryQuantifiers::check: " << assertion << std::endl;
-  if( options::cbqi() ){
-    if( assertion.hasAttribute(InstConstantAttribute()) ){
-      Debug("quant-quant-assert") << "   -> has constraints from " << assertion.getAttribute(InstConstantAttribute()) << std::endl;
-      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
-    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      Debug("quant-quant-assert") << "   -> has constraints from " << assertion[0].getAttribute(InstConstantAttribute()) << std::endl;
-      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
-    }
-  }
-}
-
-void InstantiatorTheoryQuantifiers::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-
-int InstantiatorTheoryQuantifiers::process( Node f, Theory::Effort effort, int e ){
-  Debug("quant-quant") << "Quant: Try to solve (" << e << ") for " << f << "... " << std::endl;
-  if( e<5 ){
-    return InstStrategy::STATUS_UNFINISHED;
-  }else if( e==5 ){
-    //add random addition
-    InstMatch m;
-    if( d_quantEngine->addInstantiation( f, m ) ){
-      ++(d_statistics.d_instantiations);
-    }
-  }
-  return InstStrategy::STATUS_UNKNOWN;
-}
-
-InstantiatorTheoryQuantifiers::Statistics::Statistics():
-  d_instantiations("InstantiatorTheoryQuantifiers::Instantiations_Total", 0)
-{
-  StatisticsRegistry::registerStat(&d_instantiations);
-}
-
-InstantiatorTheoryQuantifiers::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_instantiations);
-}
-
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.h b/src/theory/quantifiers/theory_quantifiers_instantiator.h
deleted file mode 100644
index 5722c264f..000000000
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.h
+++ /dev/null
@@ -1,58 +0,0 @@
-/*********************                                                        */
-/*! \file theory_quantifiers_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief instantiator_quantifiers_instantiator
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H
-
-#include "theory/quantifiers_engine.h"
-
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class InstantiatorTheoryQuantifiers : public Instantiator{
-  friend class QuantifiersEngine;
-public:
-  InstantiatorTheoryQuantifiers(context::Context* c, QuantifiersEngine* ie, Theory* th);
-  ~InstantiatorTheoryQuantifiers() {}
-
-  /** check function, assertion is asserted to theory */
-  void assertNode( Node assertion );
-  /** identify */
-  std::string identify() const { return std::string("InstantiatorTheoryQuantifiers"); }
-private:
-  /**  reset instantiation */
-  void processResetInstantiationRound( Theory::Effort effort );
-  /** process at effort */
-  int process( Node f, Theory::Effort effort, int e );
-
-  class Statistics {
-  public:
-    IntStat d_instantiations;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
-};/* class InstantiatiorTheoryQuantifiers */
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 4d5efcd8d..bc577fda6 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -15,7 +15,6 @@
 #include "theory/quantifiers/trigger.h"
 #include "theory/theory_engine.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/quantifiers/candidate_generator.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/quantifiers/options.h"
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ce62e2f8b..c04920ab8 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -14,7 +14,6 @@
 
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/arrays/theory_arrays.h"
@@ -25,6 +24,7 @@
 #include "theory/quantifiers/instantiation_engine.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/trigger.h"
 #include "theory/rewriterules/efficient_e_matching.h"
 #include "theory/rewriterules/rr_trigger.h"
 
@@ -84,9 +84,9 @@ EqualityQuery* QuantifiersEngine::getEqualityQuery() {
   return d_eq_query;
 }
 
-Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){
-  return d_te->theoryOf( id )->getInstantiator();
-}
+//Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){
+//  return d_te->theoryOf( id )->getInstantiator();
+//}
 
 context::Context* QuantifiersEngine::getSatContext(){
   return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
@@ -100,6 +100,12 @@ Valuation& QuantifiersEngine::getValuation(){
   return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation();
 }
 
+void QuantifiersEngine::finishInit(){
+  for( int i=0; i<(int)d_modules.size(); i++ ){
+    d_modules[i]->finishInit();
+  }
+}
+
 void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_time);
   bool needsCheck = e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 719620e76..8169c78fb 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -45,6 +45,8 @@ public:
   virtual ~QuantifiersModule(){}
   //get quantifiers engine
   QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
+  /** initialize */
+  virtual void finishInit() {}
   /* whether this module needs to check this round */
   virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
   /* Call during quantifier engine's check */
@@ -122,7 +124,7 @@ public:
   QuantifiersEngine(context::Context* c, TheoryEngine* te);
   ~QuantifiersEngine();
   /** get instantiator for id */
-  Instantiator* getInstantiator( theory::TheoryId id );
+  //Instantiator* getInstantiator( theory::TheoryId id );
   /** get theory engine */
   TheoryEngine* getTheoryEngine() { return d_te; }
   /** get equality query object for the given type. The default is the
@@ -147,6 +149,8 @@ public:
   /** get efficient e-matching utility */
   EfficientEMatcher* getEfficientEMatcher() { return d_eem; }
 public:
+  /** initialize */
+  void finishInit();
   /** check at level */
   void check( Theory::Effort e );
   /** register quantifier */
diff --git a/src/theory/rewriterules/efficient_e_matching.cpp b/src/theory/rewriterules/efficient_e_matching.cpp
index 7f03bf8f8..2f39d8098 100755
--- a/src/theory/rewriterules/efficient_e_matching.cpp
+++ b/src/theory/rewriterules/efficient_e_matching.cpp
@@ -92,7 +92,8 @@ EfficientEMatcher::EfficientEMatcher( CVC4::theory::QuantifiersEngine* qe ) : d_
 }

 

 eq::EqualityEngine* EfficientEMatcher::getEqualityEngine(){

-  return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();

+  //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();

+  return d_quantEngine->getMasterEqualityEngine();

 }

 

 /** new node */

diff --git a/src/theory/rewriterules/rr_candidate_generator.cpp b/src/theory/rewriterules/rr_candidate_generator.cpp
index 2957b4ddb..3f2895397 100644
--- a/src/theory/rewriterules/rr_candidate_generator.cpp
+++ b/src/theory/rewriterules/rr_candidate_generator.cpp
@@ -24,100 +24,44 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::rrinst;
 
-GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(qe->getInstantiator(i) != NULL)
-      d_can_gen[i] = qe->getInstantiator(i)->getRRCanGenClasses();
-    else d_can_gen[i] = NULL;
-  }
+GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe) : d_qe(qe){
+  d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClasses(d_qe->getMasterEqualityEngine());
 }
 
 GenericCandidateGeneratorClasses::~GenericCandidateGeneratorClasses(){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    delete(d_can_gen[i]);
-  }
+  delete d_master_can_gen;
 }
 
 void GenericCandidateGeneratorClasses::resetInstantiationRound(){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound();
-  }
-  d_can_gen_id=THEORY_FIRST;
+  d_master_can_gen->resetInstantiationRound();
 }
 
 void GenericCandidateGeneratorClasses::reset(TNode eqc){
-  Assert(eqc.isNull());
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc);
-  }
-  d_can_gen_id=THEORY_FIRST;
-  lookForNextTheory();
+  d_master_can_gen->reset(eqc);
 }
 
 TNode GenericCandidateGeneratorClasses::getNextCandidate(){
-  Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST);
-  /** No more */
-  if(d_can_gen_id == THEORY_LAST) return TNode::null();
-  /** Try with this theory */
-  TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate();
-  if( !cand.isNull() ) return cand;
-  lookForNextTheory();
-  return getNextCandidate();
+  return d_master_can_gen->getNextCandidate();
 }
 
-void GenericCandidateGeneratorClasses::lookForNextTheory(){
-  do{ /* look for the next available generator */
-    ++d_can_gen_id;
-  } while( d_can_gen_id < THEORY_LAST && d_can_gen[d_can_gen_id] == NULL);
-}
 
 GenericCandidateGeneratorClass::GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) {
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(d_qe->getInstantiator(i) != NULL)
-      d_can_gen[i] = d_qe->getInstantiator(i)->getRRCanGenClass();
-    else d_can_gen[i] = NULL;
-  }
+  d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClass(d_qe->getMasterEqualityEngine());
 }
 
 GenericCandidateGeneratorClass::~GenericCandidateGeneratorClass(){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    delete(d_can_gen[i]);
-  }
+  delete d_master_can_gen;
 }
 
 void GenericCandidateGeneratorClass::resetInstantiationRound(){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound();
-  }
-  d_can_gen_id=THEORY_FIRST;
+  d_master_can_gen->resetInstantiationRound();
 }
 
 void GenericCandidateGeneratorClass::reset(TNode eqc){
-  for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
-    if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc);
-  }
-  d_can_gen_id=THEORY_FIRST;
-  d_node = eqc;
-  lookForNextTheory();
+  d_master_can_gen->reset(eqc);
 }
 
 TNode GenericCandidateGeneratorClass::getNextCandidate(){
-  Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST);
-  /** No more */
-  if(d_can_gen_id == THEORY_LAST) return TNode::null();
-  /** Try with this theory */
-  TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate();
-  if( !cand.isNull() ) return cand;
-  lookForNextTheory();
-  return getNextCandidate();
+  return d_master_can_gen->getNextCandidate();
 }
 
-void GenericCandidateGeneratorClass::lookForNextTheory(){
-  do{ /* look for the next available generator, where the element is */
-    ++d_can_gen_id;
-  } while(
-          d_can_gen_id < THEORY_LAST &&
-          (d_can_gen[d_can_gen_id] == NULL ||
-           !d_qe->getInstantiator( d_can_gen_id )->hasTerm( d_node ))
-          );
-}
diff --git a/src/theory/rewriterules/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h
index 8ebaae343..97c710219 100644
--- a/src/theory/rewriterules/rr_candidate_generator.h
+++ b/src/theory/rewriterules/rr_candidate_generator.h
@@ -166,10 +166,9 @@ public:
 class GenericCandidateGeneratorClasses: public rrinst::CandidateGenerator{
 
   /** The candidate generators */
-  rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST];
-  /** The current theory which candidategenerator is used */
-  TheoryId d_can_gen_id;
-
+  rrinst::CandidateGenerator* d_master_can_gen;
+  /** QuantifierEngine */
+  QuantifiersEngine* d_qe;
 public:
   GenericCandidateGeneratorClasses(QuantifiersEngine * qe);
   ~GenericCandidateGeneratorClasses();
@@ -183,22 +182,15 @@ public:
 class GenericCandidateGeneratorClass: public rrinst::CandidateGenerator{
 
   /** The candidate generators */
-  rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST];
-  /** The current theory which candidategenerator is used */
-  TheoryId d_can_gen_id;
-  /** current node to look for equivalence class */
-  Node d_node;
+  rrinst::CandidateGenerator* d_master_can_gen;
   /** QuantifierEngine */
   QuantifiersEngine* d_qe;
-
 public:
   GenericCandidateGeneratorClass(QuantifiersEngine * qe);
   ~GenericCandidateGeneratorClass();
   void resetInstantiationRound();
-
   void reset(TNode eqc);
   TNode getNextCandidate();
-  void lookForNextTheory();
 };
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp
index 5f10e1daa..5c3a55831 100644
--- a/src/theory/rewriterules/rr_inst_match.cpp
+++ b/src/theory/rewriterules/rr_inst_match.cpp
@@ -15,7 +15,6 @@
 #include "theory/quantifiers/inst_match.h"
 #include "theory/theory_engine.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/datatypes/theory_datatypes.h"
diff --git a/src/theory/rewriterules/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp
index ad77f0bcb..4f48a72ae 100644
--- a/src/theory/rewriterules/rr_trigger.cpp
+++ b/src/theory/rewriterules/rr_trigger.cpp
@@ -15,7 +15,6 @@
 #include "theory/rewriterules/rr_trigger.h"
 #include "theory/theory_engine.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/rewriterules/rr_candidate_generator.h"
 #include "theory/uf/equality_engine.h"
 
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index f8e2ec777..ea3902d59 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -17,7 +17,6 @@
 #include "theory/theory.h"
 #include "util/cvc4_assert.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/instantiator_default.h"
 
 #include <vector>
 
@@ -184,15 +183,18 @@ Instantiator::~Instantiator() {
 }
 
 void Instantiator::resetInstantiationRound(Theory::Effort effort) {
+  /*
   for(int i = 0; i < (int) d_instStrategies.size(); ++i) {
     if(isActiveStrategy(d_instStrategies[i])) {
       d_instStrategies[i]->processResetInstantiationRound(effort);
     }
   }
   processResetInstantiationRound(effort);
+  */
 }
 
 int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) {
+  /*
   if( getQuantifierActive(f) ) {
     int status = process(f, effort, e );
     if(d_instStrategies.empty()) {
@@ -215,6 +217,8 @@ int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) {
     Debug("inst-engine-inst") << "We have no constraints from this quantifier." << endl;
     return InstStrategy::STATUS_SAT;
   }
+  */
+  return 0;
 }
 
 //void Instantiator::doInstantiation(int effort) {
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 4d535a8af..1f55a4b90 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -820,40 +820,6 @@ namespace eq{
   class EqualityEngine;
 }
 
-/** instantiation strategy class */
-class InstStrategy {
-public:
-  enum Status {
-    STATUS_UNFINISHED,
-    STATUS_UNKNOWN,
-    STATUS_SAT,
-  };/* enum Status */
-protected:
-  /** reference to the instantiation engine */
-  QuantifiersEngine* d_quantEngine;
-
-
-public:
-  InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
-  virtual ~InstStrategy(){}
-
-  /** reset instantiation */
-  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
-  /** process method, returns a status */
-  virtual int process( Node f, Theory::Effort effort, int e ) = 0;
-  /** update status */
-  static void updateStatus( int& currStatus, int addStatus ){
-    if( addStatus==STATUS_UNFINISHED ){
-      currStatus = STATUS_UNFINISHED;
-    }else if( addStatus==STATUS_UNKNOWN ){
-      if( currStatus==STATUS_SAT ){
-        currStatus = STATUS_UNKNOWN;
-      }
-    }
-  }
-  /** identify */
-  virtual std::string identify() const { return std::string("Unknown"); }
-};/* class InstStrategy */
 
 /** instantiator class */
 class Instantiator {
@@ -863,21 +829,6 @@ protected:
   QuantifiersEngine* d_quantEngine;
   /** reference to the theory that it looks at */
   Theory* d_th;
-  /** instantiation strategies */
-  std::vector< InstStrategy* > d_instStrategies;
-  /** instantiation strategies active */
-  std::map< InstStrategy*, bool > d_instStrategyActive;
-  /** has constraints from quantifier */
-  std::map< Node, bool > d_quantActive;
-  /** is instantiation strategy active */
-  bool isActiveStrategy( InstStrategy* is ) {
-    return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
-  }
-  /** add inst strategy */
-  void addInstStrategy( InstStrategy* is ){
-    d_instStrategies.push_back( is );
-    d_instStrategyActive[is] = true;
-  }
   /** reset instantiation round */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   /** process quantifier */
@@ -899,10 +850,6 @@ public:
   /** print debug information */
   virtual void debugPrint( const char* c ) {}
 public:
-  /** set has constraints from quantifier f */
-  void setQuantifierActive( Node f ) { d_quantActive[f] = true; }
-  /** has constraints from */
-  bool getQuantifierActive( Node f ) { return d_quantActive.find(f) != d_quantActive.end() && d_quantActive[f]; }
   /** reset instantiation round */
   void resetInstantiationRound( Theory::Effort effort );
   /** do instantiation method*/
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ce3ccebf3..c0aa58647 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -53,6 +53,7 @@ using namespace CVC4::theory;
 
 void TheoryEngine::finishInit() {
   if (d_logicInfo.isQuantified()) {
+    d_quantEngine->finishInit();
     Assert(d_masterEqualityEngine == 0);
     d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master");
 
@@ -70,6 +71,9 @@ void TheoryEngine::eqNotifyNewClass(TNode t){
 
 void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
   //TODO: add notification to efficient E-matching
+  if (d_logicInfo.isQuantified()) {
+    d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
+  }
 }
 
 void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index e027f8909..82129c72b 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -15,12 +15,8 @@ libuf_la_SOURCES = \
 	equality_engine.cpp \
 	symmetry_breaker.h \
 	symmetry_breaker.cpp \
-	theory_uf_instantiator.h \
-	theory_uf_instantiator.cpp \
 	theory_uf_strong_solver.h \
 	theory_uf_strong_solver.cpp \
-	inst_strategy.h \
-	inst_strategy.cpp \
 	theory_uf_model.h \
 	theory_uf_model.cpp 
 
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 1d179248c..fa24df717 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -6,7 +6,6 @@
 
 theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h"
 typechecker "theory/uf/theory_uf_type_rules.h"
-instantiator ::CVC4::theory::uf::InstantiatorTheoryUf "theory/uf/theory_uf_instantiator.h"
 
 properties stable-infinite parametric
 properties check propagate ppStaticLearn presolve getNextDecisionRequest
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 23f100f74..3f033f3b8 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -18,12 +18,9 @@
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/options.h"
 #include "theory/quantifiers/options.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/model.h"
 #include "theory/type_enumerator.h"
-//included since efficient e matching needs notifications from UF
-#include "theory/rewriterules/efficient_e_matching.h"
 
 using namespace std;
 using namespace CVC4;
@@ -479,15 +476,11 @@ void TheoryUF::eqNotifyNewClass(TNode t) {
   if (d_thss != NULL) {
     d_thss->newEqClass(t);
   }
-  // this can be called very early, during initialization
-  if (!getLogicInfo().isLocked() || getLogicInfo().isQuantified()) {
-    //getQuantifiersEngine()->addTermToDatabase( t );
-  }
 }
 
 void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) {
   if (getLogicInfo().isQuantified()) {
-    getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 );
+    //getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 );
   }
 }
 
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
deleted file mode 100644
index 9ae6bbd37..000000000
--- a/src/theory/uf/theory_uf_instantiator.cpp
+++ /dev/null
@@ -1,185 +0,0 @@
-/*********************                                                        */
-/*! \file theory_uf_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: bobot
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory uf instantiator class
- **/
-
-#include "theory/uf/theory_uf_instantiator.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/rewriterules/options.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
-#include "theory/rewriterules/efficient_e_matching.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
-using namespace CVC4::theory::inst;
-
-namespace CVC4 {
-namespace theory {
-namespace uf {
-
-InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th) :
-Instantiator( c, qe, th )
-{
-  if( !options::finiteModelFind() || options::fmfInstEngine() ){
-    //if( options::cbqi() ){
-    //  addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
-    //}
-    //these are the instantiation strategies for basic E-matching
-    if( options::userPatternsQuant() ){
-      d_isup = new InstStrategyUserPatterns( this, qe );
-      addInstStrategy( d_isup );
-    }else{
-      d_isup = NULL;
-    }
-    InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( this, qe, Trigger::TS_ALL,
-                                                                         InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 );
-    i_ag->setGenerateAdditional( true );
-    addInstStrategy( i_ag );
-    //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
-    if( !options::finiteModelFind() ){
-      addInstStrategy( new InstStrategyFreeVariable( this, qe ) );
-    }
-    //d_isup->setPriorityOver( i_ag );
-    //d_isup->setPriorityOver( i_agm );
-    //i_ag->setPriorityOver( i_agm );
-  }
-}
-
-void InstantiatorTheoryUf::preRegisterTerm( Node t ){
-  //d_quantEngine->addTermToDatabase( t );
-}
-
-void InstantiatorTheoryUf::assertNode( Node assertion )
-{
-  Debug("quant-uf-assert") << "InstantiatorTheoryUf::check: " << assertion << std::endl;
-  //preRegisterTerm( assertion );
-  //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion );
-  if( options::cbqi() ){
-    if( assertion.hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
-    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
-    }
-  }
-}
-
-void InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){
-  if( d_isup ){
-    d_isup->addUserPattern( f, pat );
-    setQuantifierActive( f );
-  }
-}
-
-
-void InstantiatorTheoryUf::processResetInstantiationRound( Theory::Effort effort ){
-  //d_ground_reps.clear();
-}
-
-int InstantiatorTheoryUf::process( Node f, Theory::Effort effort, int e ){
-  Debug("quant-uf") << "UF: Try to solve (" << e << ") for " << f << "... " << std::endl;
-  return InstStrategy::STATUS_SAT;
-}
-
-void InstantiatorTheoryUf::debugPrint( const char* c )
-{
-
-}
-
-bool InstantiatorTheoryUf::hasTerm( Node a ){
-  return ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( a );
-}
-
-bool InstantiatorTheoryUf::areEqual( Node a, Node b ){
-  if( a==b ){
-    return true;
-  }else if( hasTerm( a ) && hasTerm( b ) ){
-    return ((TheoryUF*)d_th)->d_equalityEngine.areEqual( a, b );
-  }else{
-    return false;
-  }
-}
-
-bool InstantiatorTheoryUf::areDisequal( Node a, Node b ){
-  if( a==b ){
-    return false;
-  }else if( hasTerm( a ) && hasTerm( b ) ){
-    return ((TheoryUF*)d_th)->d_equalityEngine.areDisequal( a, b, false );
-  }else{
-    return false;
-  }
-}
-
-Node InstantiatorTheoryUf::getRepresentative( Node a ){
-  if( hasTerm( a ) ){
-    return ((TheoryUF*)d_th)->d_equalityEngine.getRepresentative( a );
-  }else{
-    return a;
-  }
-}
-
-eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){
-  return &((TheoryUF*)d_th)->d_equalityEngine;
-}
-
-void InstantiatorTheoryUf::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
-  if( hasTerm( a ) ){
-    a = getEqualityEngine()->getRepresentative( a );
-    eq::EqClassIterator eqc_iter( a, getEqualityEngine() );
-    while( !eqc_iter.isFinished() ){
-      if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){
-        eqc.push_back( *eqc_iter );
-      }
-      eqc_iter++;
-    }
-  }
-}
-
-void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){
-  if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) ){
-    eq::EqClassIterator eqc_iter( getRepresentative( n ),
-                                  &((TheoryUF*)d_th)->d_equalityEngine );
-    bool firstTime = true;
-    while( !eqc_iter.isFinished() ){
-      if( !firstTime ){ Debug(c) << ", "; }
-      Debug(c) << (*eqc_iter);
-      firstTime = false;
-      eqc_iter++;
-    }
-  }else{
-    Debug(c) << n;
-  }
-}
-
-rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClasses(){
-  uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory());
-  eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
-  return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee);
-}
-
-rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClass(){
-  uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory());
-  eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
-  return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee);
-}
-
-
-} /* namespace uf */
-} /* namespace theory */
-} /* namespace cvc4 */
diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h
deleted file mode 100644
index fe34c9487..000000000
--- a/src/theory/uf/theory_uf_instantiator.h
+++ /dev/null
@@ -1,87 +0,0 @@
-/*********************                                                        */
-/*! \file theory_uf_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: bobot
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Theory uf instantiator
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_UF_INSTANTIATOR_H
-#define __CVC4__THEORY_UF_INSTANTIATOR_H
-
-#include "theory/uf/inst_strategy.h"
-
-#include "context/context.h"
-#include "context/context_mm.h"
-#include "context/cdchunk_list.h"
-
-#include "util/statistics_registry.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/quantifiers/trigger.h"
-#include "theory/quantifiers/inst_match_generator.h"
-#include "util/ntuple.h"
-#include "context/cdqueue.h"
-
-namespace CVC4 {
-namespace theory {
-
-namespace quantifiers{
-  class TermDb;
-}
-
-namespace uf {
-
-class InstantiatorTheoryUf : public Instantiator{
-protected:
-  /** instantiation strategies */
-  InstStrategyUserPatterns* d_isup;
-public:
-  InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th);
-  ~InstantiatorTheoryUf() {}
-  /** assertNode method */
-  void assertNode( Node assertion );
-  /** Pre-register a term.  Done one time for a Node, ever. */
-  void preRegisterTerm( Node t );
-  /** identify */
-  std::string identify() const { return std::string("InstantiatorTheoryUf"); }
-  /** debug print */
-  void debugPrint( const char* c );
-  /** add user pattern */
-  void addUserPattern( Node f, Node pat );
-private:
-  /** reset instantiation */
-  void processResetInstantiationRound( Theory::Effort effort );
-  /** calculate matches for quantifier f at effort */
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  /** general queries about equality */
-  bool hasTerm( Node a );
-  bool areEqual( Node a, Node b );
-  bool areDisequal( Node a, Node b );
-  Node getRepresentative( Node a );
-  Node getInternalRepresentative( Node a );
-  eq::EqualityEngine* getEqualityEngine();
-  void getEquivalenceClass( Node a, std::vector< Node >& eqc );
-  /** general creators of candidate generators */
-  rrinst::CandidateGenerator* getRRCanGenClasses();
-  rrinst::CandidateGenerator* getRRCanGenClass();
-public:
-  /** output eq class */
-  void outputEqClass( const char* c, Node n );
-};/* class InstantiatorTheoryUf */
-
-
-
-}
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 0ec89af0b..46ac5aa60 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -15,8 +15,8 @@
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/equality_engine.h"
-#include "theory/uf/theory_uf_instantiator.h"
 #include "theory/theory_engine.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/uf/options.h"
 #include "theory/model.h"