Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

16 files changed, 3576 insertions, 25 deletions

diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 50147b997..2c9cd3b80 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -14,6 +14,14 @@ libuf_la_SOURCES = \
 	equality_engine_types.h \
 	equality_engine.cpp \
 	symmetry_breaker.h \
-	symmetry_breaker.cpp
+	symmetry_breaker.cpp \
+	theory_uf_instantiator.h \
+	theory_uf_instantiator.cpp \
+	theory_uf_strong_solver.h \
+	theory_uf_strong_solver.cpp \
+	theory_uf_candidate_generator.h \
+	theory_uf_candidate_generator.cpp \
+	inst_strategy.h \
+	inst_strategy.cpp
 
 EXTRA_DIST = kinds
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 25645c472..96c8e8b59 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -211,6 +211,11 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
 
   Debug("equality") << d_name << "::eq::newNode(" << node << ") => " << newId << std::endl;
 
+  // notify e.g. the UF theory strong solver
+  if (d_performNotify) {
+    d_notify.eqNotifyNewClass(node);
+  }
+
   return newId;
 }
 
@@ -346,7 +351,12 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
     if (hasTerm(eq[0]) && hasTerm(eq[1]) && areDisequal(eq[0], eq[1], false)) {
       return;
     }
-    
+
+    // notify the theory
+    if (d_performNotify) {
+      d_notify.eqNotifyDisequal(eq[0], eq[1], reason);
+    }
+
     Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl;
 
     assertEqualityInternal(eq, d_false, reason);
@@ -437,6 +447,21 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   EqualityNodeId class1Id = class1.getFind();
   EqualityNodeId class2Id = class2.getFind();
 
+  Node n1 = d_nodes[class1Id];
+  Node n2 = d_nodes[class2Id];
+  EqualityNode cc1 = getEqualityNode(n1);
+  EqualityNode cc2 = getEqualityNode(n2);
+  bool doNotify = false;
+  // notify the theory
+  // the second part of this check is needed due to the internal implementation of this class.
+  // It ensures that we are merging terms and not operators.
+  if (d_performNotify && class1Id==cc1.getFind() && class2Id==cc2.getFind()) {
+    doNotify = true;
+  }
+  if (doNotify) {
+    d_notify.eqNotifyPreMerge(n1, n2);
+  }
+
   // Check for constant merges
   bool class1isConstant = d_isConstant[class1Id];
   bool class2isConstant = d_isConstant[class2Id];
@@ -559,7 +584,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
     
   // Now merge the lists
   class1.merge<true>(class2);
-  
+
+  // notify the theory
+  if (doNotify) {
+    d_notify.eqNotifyPostMerge(n1, n2);
+  }
+
   // Go through the trigger term disequalities and propagate
   if (!propagateTriggerTermDisequalities(class1OnlyTags, class1triggerRef, class2disequalitiesToNotify)) {
     return false;
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 8cf159cd7..cb0c81872 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -39,6 +39,9 @@ namespace CVC4 {
 namespace theory {
 namespace eq {
 
+class EqClassesIterator;
+class EqClassIterator;
+
 /**
  * Interface for equality engine notifications. All the notifications
  * are safe as TNodes, but not necessarily for negations.
@@ -62,7 +65,7 @@ public:
   /**
    * Notifies about a trigger predicate that became true or false.
    *
-   * @param predicate the trigger predicate that bacame true or false
+   * @param predicate the trigger predicate that became true or false
    * @param value the value of the predicate
    */
   virtual bool eqNotifyTriggerPredicate(TNode predicate, bool value) = 0;
@@ -82,10 +85,43 @@ public:
    * can do is ask for explanations.
    *
    * @param t1 a constant term
-   * @param t2 a constnat term
+   * @param t2 a constant term
    */
   virtual void eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0;
-};
+
+  /**
+   * Notifies about the creation of a new equality class.
+   *
+   * @param t the term forming the new class
+   */
+  virtual void eqNotifyNewClass(TNode t) = 0;
+
+  /**
+   * Notifies about the merge of two classes (just before the merge).
+   *
+   * @param t1 a term
+   * @param t2 a term
+   */
+  virtual void eqNotifyPreMerge(TNode t1, TNode t2) = 0;
+
+  /**
+   * Notifies about the merge of two classes (just after the merge).
+   *
+   * @param t1 a term
+   * @param t2 a term
+   */
+  virtual void eqNotifyPostMerge(TNode t1, TNode t2) = 0;
+
+  /**
+   * Notifies about the disequality of two terms.
+   *
+   * @param t1 a term
+   * @param t2 a term
+   * @param reason the reason
+   */
+  virtual void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) = 0;
+
+};/* class EqualityEngineNotify */
 
 /**
  * Implementation of the notification interface that ignores all the
@@ -97,7 +133,11 @@ public:
   bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
   bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
   void eqNotifyConstantTermMerge(TNode t1, TNode t2) { }
-};
+  void eqNotifyNewClass(TNode t) { }
+  void eqNotifyPreMerge(TNode t1, TNode t2) { }
+  void eqNotifyPostMerge(TNode t1, TNode t2) { }
+  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+};/* class EqualityEngineNotifyNone */
 
 
 /**
@@ -106,6 +146,9 @@ public:
  */
 class EqualityEngine : public context::ContextNotifyObj {
 
+  friend class EqClassesIterator;
+  friend class EqClassIterator;
+
   /** Default implementation of the notification object */
   static EqualityEngineNotifyNone s_notifyNone;
 
@@ -140,14 +183,14 @@ public:
       StatisticsRegistry::unregisterStat(&functionTermsCount);
       StatisticsRegistry::unregisterStat(&constantTermsCount);
     }
-  };
+  };/* struct EqualityEngine::statistics */
 
   /**
    * Store the application lookup, with enough information to backtrack
    */
   void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId);
 
-private:
+//private:
 
   /** The context we are using */
   context::Context* d_context;
@@ -212,7 +255,7 @@ private:
     /** Equality constructor */
     Equality(EqualityNodeId lhs = null_id, EqualityNodeId rhs = null_id)
     : lhs(lhs), rhs(rhs) {}
-  };
+  };/* struct EqualityEngine::Equality */
 
   /** The ids of the classes we have merged */
   std::vector<Equality> d_assertedEqualities;
@@ -253,7 +296,7 @@ private:
 
     /** The reason of this edge */
     TNode getReason() const { return d_reason; }
-};
+  };/* class EqualityEngine::EqualityEdge */
 
   /**
    * All the equality edges (twice as many as the number of asserted equalities. If an equality
@@ -268,7 +311,7 @@ private:
   std::string edgesToString(EqualityEdgeId edgeId) const;
 
   /**
-   * Map from a node to it's first edge in the equality graph. Edges are added to the front of the
+   * Map from a node to its first edge in the equality graph. Edges are added to the front of the
    * list which makes the insertion/backtracking easy.
    */
   std::vector<EqualityEdgeId> d_equalityGraph;
@@ -297,7 +340,7 @@ private:
    */
   bool merge(EqualityNode& class1, EqualityNode& class2, std::vector<TriggerId>& triggers);
 
-  /** Undo the mereg of class2 into class1 */
+  /** Undo the merge of class2 into class1 */
   void undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id);
 
   /** Backtrack the information if necessary */
@@ -314,7 +357,7 @@ private:
 
     Trigger(EqualityNodeId classId = null_id, TriggerId nextTrigger = null_trigger)
     : classId(classId), nextTrigger(nextTrigger) {}
-  };
+  };/* struct EqualityEngine::Trigger */
 
   /**
    * Vector of triggers. Triggers come in pairs for an
@@ -436,7 +479,7 @@ private:
     EqualityNodeId getTrigger(TheoryId tag) const {
       return triggers[Theory::setIndex(tag, tags)];
     }
-  };
+  };/* struct EqualityEngine::TriggerTermSet */
 
   /** Internal tags for creating a new set */
   Theory::Set d_newSetTags;
@@ -451,7 +494,7 @@ private:
   char* d_triggerDatabase;
 
   /** Allocated size of the trigger term database */
-  DefaultSizeType d_triggerDatabaseAllocatedSize ;
+  DefaultSizeType d_triggerDatabaseAllocatedSize;
 
   /** Reference for the trigger terms set */
   typedef DefaultSizeType TriggerTermSetRef;
@@ -482,7 +525,7 @@ private:
     TriggerTermSetRef oldValue;
     TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id) 
     : classId(classId), oldValue(oldValue) {}
-  };
+  };/* struct EqualityEngine::TriggerSetUpdate */
 
   /**
    * List of trigger updates for backtracking.
@@ -685,7 +728,7 @@ public:
    * Add term to the set of trigger terms with a corresponding tag. The notify class will get
    * notified when two trigger terms with the same tag become equal or dis-equal. The notification
    * will not happen on all the terms, but only on the ones that are represent the class. Note that
-   * a term can be added more than once with different tags, and each tag apperance will merit
+   * a term can be added more than once with different tags, and each tag appearance will merit
    * it's own notification.
    *
    * @param t the trigger term
@@ -743,7 +786,97 @@ public:
 
 };
 
-} // Namespace uf
+class EqClassesIterator {
+
+  eq::EqualityEngine* d_ee;
+  size_t d_it;
+
+public:
+
+  EqClassesIterator() { }
+  EqClassesIterator(eq::EqualityEngine* ee) : d_ee(ee) {
+    d_it = 0;
+    if ( d_it < d_ee->d_nodesCount &&
+         d_ee->getRepresentative(d_ee->d_nodes[d_it]) != d_ee->d_nodes[d_it] ) {
+      ++*this;
+    }
+  }
+  Node operator*() {
+    return d_ee->d_nodes[d_it];
+  }
+  bool operator==(const EqClassesIterator& i) {
+    return d_ee == i.d_ee && d_it == i.d_it;
+  }
+  bool operator!=(const EqClassesIterator& i) {
+    return !(*this == i);
+  }
+  EqClassesIterator& operator++() {
+    Node orig = d_ee->d_nodes[d_it];
+    ++d_it;
+    while ( d_it<d_ee->d_nodesCount &&
+            ( d_ee->getRepresentative(d_ee->d_nodes[d_it]) != d_ee->d_nodes[d_it]
+              || d_ee->d_nodes[d_it] == orig ) ) { // this line is necessary for ignoring duplicates
+      ++d_it;
+    }
+    return *this;
+  }
+  EqClassesIterator operator++(int) {
+    EqClassesIterator i = *this;
+    ++*this;
+    return i;
+  }
+  bool isFinished() {
+    return d_it>=d_ee->d_nodesCount;
+  }
+};/* class EqClassesIterator */
+
+class EqClassIterator {
+
+  Node d_rep;
+  eq::EqualityNode d_curr;
+  Node d_curr_node;
+  eq::EqualityEngine* d_ee;
+
+public:
+
+  EqClassIterator() { }
+  EqClassIterator(Node eqc, eq::EqualityEngine* ee) : d_ee(ee) {
+    Assert( d_ee->getRepresentative(eqc) == eqc );
+    d_rep = eqc;
+    d_curr_node = eqc;
+    d_curr = d_ee->getEqualityNode(eqc);
+  }
+  Node operator*() {
+    return d_curr_node;
+  }
+  bool operator==(const EqClassIterator& i) {
+    return d_ee == i.d_ee && d_curr_node == i.d_curr_node;
+  }
+  bool operator!=(const EqClassIterator& i) {
+    return !(*this == i);
+  }
+  EqClassIterator& operator++() {
+    Node next = d_ee->d_nodes[ d_curr.getNext() ];
+    Assert( d_rep==d_ee->getRepresentative(next) );
+    if (d_rep != next) { // we end when we have cycled back to the original representative
+      d_curr_node = next;
+      d_curr = d_ee->getEqualityNode(d_curr.getNext());
+    } else {
+      d_curr_node = Node::null();
+    }
+    return *this;
+  }
+  EqClassIterator operator++(int) {
+    EqClassIterator i = *this;
+    ++*this;
+    return i;
+  }
+  bool isFinished() {
+    return d_curr_node == Node::null();
+  }
+};/* class EqClassIterator */
+
+} // Namespace eq
 } // Namespace theory
 } // Namespace CVC4
 
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
new file mode 100644
index 000000000..2ca2dcb5a
--- /dev/null
+++ b/src/theory/uf/inst_strategy.cpp
@@ -0,0 +1,412 @@
+/*********************                                                        */
+/*! \file inst_strategy.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+
+#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->getNumQuantifiersForSymbol( i.getOperator() );
+    int nqfsj = d_qe->getNumQuantifiersForSymbol( j.getOperator() );
+    if( nqfsi<nqfsj ){
+      return true;
+    }else if( nqfsi>nqfsj ){
+      return false;
+    }else{
+      return false;
+    }
+  }
+};
+
+
+void InstStrategyCheckCESolved::processResetInstantiationRound( Theory::Effort effort ){
+  for( std::map< Node, bool >::iterator it = d_solved.begin(); it != d_solved.end(); ++it ){
+    calcSolved( it->first );
+  }
+}
+
+int InstStrategyCheckCESolved::process( Node f, Theory::Effort effort, int e, int instLimit ){
+  if( e==0 ){
+    //calc solved if not done so already
+    if( d_solved.find( f )==d_solved.end() ){
+      calcSolved( f );
+    }
+    //check if f is counterexample-solved
+    Debug("quant-uf-strategy") << "Try CE-solved.." << std::endl;
+    if( d_solved[ f ] ){
+      if( d_quantEngine->addInstantiation( f, d_th->d_baseMatch[f] ) ){
+        ++(d_th->d_statistics.d_instantiations_ce_solved);
+        //d_quantEngine->d_hasInstantiated[f] = true;
+      }
+      d_solved[f] = false;
+    } 
+    Debug("quant-uf-strategy") << "done." << std::endl;
+  }
+  return STATUS_UNKNOWN;
+}
+
+void InstStrategyCheckCESolved::calcSolved( Node f ){
+  d_th->d_baseMatch[f].clear();
+  d_solved[ f ]= true;
+  //check if instantiation constants are solved for
+  for( int j = 0; j<(int)d_quantEngine->getNumInstantiationConstants( f ); j++ ){
+    Node i = d_quantEngine->getInstantiationConstant( f, j );
+    Node rep = d_th->getInternalRepresentative( i );
+    if( !rep.hasAttribute(InstConstantAttribute()) ){
+      d_th->d_baseMatch[f].d_map[ i ] = rep;
+    }else{
+      d_solved[ f ] = 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, int instLimit ){
+  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;
+        int numInst = d_user_gen[f][i]->addInstantiations( d_th->d_baseMatch[f], instLimit );
+        //if( d_user_gen[f][i]->isMultiTrigger() ) 
+          //Notice() << "  Done, numInst = " << numInst << "." << std::endl;
+        d_th->d_statistics.d_instantiations_user_pattern += 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::current()->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::current()->smartTriggers ) );
+  }
+}
+ 
+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 instLimit ){
+  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;
+          int numInst = tr->addInstantiations( d_th->d_baseMatch[f], instLimit );
+          //if( tr->isMultiTrigger() ) 
+            Debug("quant-uf-strategy-auto-gen-triggers") << "  Done, numInst = " << numInst << "." << std::endl;
+          if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
+            d_th->d_statistics.d_instantiations_auto_gen_min += numInst;
+          }else{
+            d_th->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->getCounterexampleBody( f ), patTermsF, d_tr_strategy, true );
+    Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getCounterexampleBody( 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
+    d_quantEngine->getPhaseReqTerms( f, patTermsF );
+    //sort into single/multi triggers
+    std::map< Node, std::vector< Node > > varContains;
+    Trigger::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->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::current()->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::current()->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::current()->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->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->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::current()->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;
+        }
+      }
+    }
+  }
+}
+
+#if 0
+
+void InstStrategyAddFailSplits::processResetInstantiationRound( Theory::Effort effort ){
+}
+
+int InstStrategyAddFailSplits::process( Node f, Theory::Effort effort, int e, int instLimit ){
+  if( e<4 ){
+    return STATUS_UNFINISHED;
+  }else{
+    for( std::map< Node, std::map< Node, std::vector< InstMatchGenerator* > > >::iterator it = InstMatchGenerator::d_match_fails.begin(); 
+         it != InstMatchGenerator::d_match_fails.end(); ++it ){
+      for( std::map< Node, std::vector< InstMatchGenerator* > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+        if( !it2->second.empty() ){
+          Node n1 = it->first;
+          Node n2 = it2->first;
+          if( !d_quantEngine->getEqualityQuery()->areEqual( n1, n2 ) && !d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 ) ){
+            d_quantEngine->addSplitEquality( n1, n2, true );
+          }
+          it2->second.clear();
+        }
+      }
+    }
+    return STATUS_UNKNOWN;
+  }
+}
+
+#endif /* 0 */
+
+void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
+}
+
+int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e, int instLimit ){
+  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_th->d_statistics.d_instantiations_guess);
+        //d_quantEngine->d_hasInstantiated[f] = true;
+      }
+    }
+    return STATUS_UNKNOWN;
+  }
+}
diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h
new file mode 100644
index 000000000..906169811
--- /dev/null
+++ b/src/theory/uf/inst_strategy.h
@@ -0,0 +1,179 @@
+/*********************                                                        */
+/*! \file inst_strategy.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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 "context/context.h"
+#include "context/context_mm.h"
+
+#include "util/stats.h"
+#include "theory/uf/theory_uf.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+class InstantiatorTheoryUf;
+
+//instantiation strategies
+
+class InstStrategyCheckCESolved : public InstStrategy{
+private:
+  /** InstantiatorTheoryUf class */
+  InstantiatorTheoryUf* d_th;
+  /** is solved? */
+  std::map< Node, bool > d_solved;
+  /** calc if f is solved */
+  void calcSolved( Node f );
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  int process( Node f, Theory::Effort effort, int e, int instLimit );
+public:
+  InstStrategyCheckCESolved( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : 
+      InstStrategy( ie ), d_th( th ){}
+  ~InstStrategyCheckCESolved(){}
+  /** identify */
+  std::string identify() const { return std::string("CheckCESolved"); }
+};/* class InstStrategyCheckCESolved */
+
+class InstStrategyUserPatterns : public InstStrategy{
+private:
+  /** InstantiatorTheoryUf class */
+  InstantiatorTheoryUf* d_th;
+  /** explicitly provided patterns */
+  std::map< Node, std::vector< 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, int instLimit );
+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 */
+  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:
+  /** 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< 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, int instLimit );
+  /** 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 */
+  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 */
+
+#if 0
+
+class InstStrategyAddFailSplits : public InstStrategy{
+private:
+  /** InstantiatorTheoryUf class */
+  InstantiatorTheoryUf* d_th;
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  int process( Node f, Theory::Effort effort, int e, int instLimit );
+public:
+  InstStrategyAddFailSplits( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : 
+      InstStrategy( ie ), d_th( th ){}
+  ~InstStrategyAddFailSplits(){}
+  /** identify */
+  std::string identify() const { return std::string("AddFailSplits"); }
+};/* class InstStrategyAddFailSplits */
+
+#endif /* 0 */
+
+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, int instLimit );
+public:
+  InstStrategyFreeVariable( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : 
+      InstStrategy( ie ), d_th( th ){}
+  ~InstStrategyFreeVariable(){}
+  /** identify */
+  std::string identify() const { return std::string("FreeVariable"); }
+};/* class InstStrategyFreeVariable */
+
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 2de3715e1..ec353dc59 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -6,6 +6,7 @@
 
 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 staticLearning presolve
@@ -15,4 +16,8 @@ parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
 
 typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule
 
+operator CARDINALITY_CONSTRAINT 2 "cardinality constraint"
+
+typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule
+
 endtheory
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 5761ee4f5..26678f21d 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -443,6 +443,16 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) {
 
   Assert(p.size() > 1);
 
+  // check that the types match
+  Permutation::iterator permIt = p.begin();
+  TypeNode type = (*permIt++).getType();
+  do {
+    if(type != (*permIt++).getType()) {
+      Debug("ufsymm") << "UFSYMM types don't match, aborting.." << endl;
+      return false;
+    }
+  } while(permIt != p.end());
+
   // check P_swap
   vector<Node> subs;
   vector<Node> repls;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 7583f8ee7..dc7bb7c92 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -18,6 +18,8 @@
  **/
 
 #include "theory/uf/theory_uf.h"
+#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/uf/theory_uf_strong_solver.h"
 
 using namespace std;
 using namespace CVC4;
@@ -25,8 +27,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 
 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_UF, c, u, out, valuation, logicInfo),
+TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
+  Theory(THEORY_UF, c, u, out, valuation, logicInfo, qe),
   d_notify(*this),
   d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
   d_conflict(c, false),
@@ -36,6 +38,12 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel&
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
+
+  if (Options::current()->finiteModelFind) {
+    d_thss = new StrongSolverTheoryUf(c, u, out, this);
+  } else {
+    d_thss = NULL;
+  }
 }/* TheoryUF::TheoryUF() */
 
 static Node mkAnd(const std::vector<TNode>& conjunctions) {
@@ -62,29 +70,46 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) {
 
 void TheoryUF::check(Effort level) {
 
-  while (!done() && !d_conflict) 
+  while (!done() && !d_conflict)
   {
     // Get all the assertions
     Assertion assertion = get();
     TNode fact = assertion.assertion;
 
     Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
+    if (d_thss != NULL) {
+      bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
+      d_thss->assertNode(fact, isDecision);
+    }
 
     // Do the work
     bool polarity = fact.getKind() != kind::NOT;
     TNode atom = polarity ? fact : fact[0];
     if (atom.getKind() == kind::EQUAL) {
       d_equalityEngine.assertEquality(atom, polarity, fact);
+    } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT) {
+      // do nothing
     } else {
       d_equalityEngine.assertPredicate(atom, polarity, fact);
     }
   }
 
+
+  if (d_thss != NULL) {
+    if (! d_conflict) {
+      d_thss->check(level);
+    }
+  }
+
 }/* TheoryUF::check() */
 
 void TheoryUF::preRegisterTerm(TNode node) {
   Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
 
+  if (d_thss != NULL) {
+    d_thss->preRegisterTerm(node);
+  }
+
   switch (node.getKind()) {
   case kind::EQUAL:
     // Add the trigger for equality
@@ -124,6 +149,12 @@ bool TheoryUF::propagate(TNode literal) {
   return ok;
 }/* TheoryUF::propagate(TNode) */
 
+void TheoryUF::propagate(Effort effort) {
+  if (d_thss != NULL) {
+    return d_thss->propagate(effort);
+  }
+}
+
 void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;
@@ -395,3 +426,54 @@ void TheoryUF::conflict(TNode a, TNode b) {
   d_out->conflict(d_conflictNode);
   d_conflict = true;
 }
+
+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()) {
+    ((InstantiatorTheoryUf*) getInstantiator())->newEqClass(t);
+  }
+}
+
+void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) {
+  if (getLogicInfo().isQuantified()) {
+    ((InstantiatorTheoryUf*) getInstantiator())->merge(t1, t2);
+  }
+}
+
+void TheoryUF::eqNotifyPostMerge(TNode t1, TNode t2) {
+  if (d_thss != NULL) {
+    d_thss->merge(t1, t2);
+  }
+}
+
+void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+  if (d_thss != NULL) {
+    d_thss->assertDisequal(t1, t2, reason);
+  }
+  if (getLogicInfo().isQuantified()) {
+    ((InstantiatorTheoryUf*) getInstantiator())->assertDisequal(t1, t2, reason);
+  }
+}
+
+Node TheoryUF::ppRewrite(TNode node) {
+
+  if (node.getKind() != kind::APPLY_UF) {
+    return node;
+  }
+
+  // perform the callbacks requested by TheoryUF::registerPpRewrite()
+  RegisterPpRewrites::iterator c = d_registeredPpRewrites.find(node.getOperator());
+  if (c == d_registeredPpRewrites.end()) {
+    return node;
+  } else {
+    Node res = c->second->ppRewrite(node);
+    if (res != node) {
+      return ppRewrite(res);
+    } else {
+      return res;
+    }
+  }
+}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index eceead38a..a55ef92b5 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -36,7 +36,15 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
+class UfTermDb;
+class InstantiatorTheoryUf;
+class StrongSolverTheoryUf;
+
 class TheoryUF : public Theory {
+
+  friend class InstantiatorTheoryUf;
+  friend class StrongSolverTheoryUf;
+
 public:
 
   class NotifyClass : public eq::EqualityEngineNotify {
@@ -76,13 +84,43 @@ public:
       Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_uf.conflict(t1, t2);
     }
-  };
+
+    void eqNotifyNewClass(TNode t) {
+      Debug("uf") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
+      d_uf.eqNotifyNewClass(t);
+    }
+
+    void eqNotifyPreMerge(TNode t1, TNode t2) {
+      Debug("uf") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
+      d_uf.eqNotifyPreMerge(t1, t2);
+    }
+
+    void eqNotifyPostMerge(TNode t1, TNode t2) {
+      Debug("uf") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
+      d_uf.eqNotifyPostMerge(t1, t2);
+    }
+
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+      Debug("uf") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
+      d_uf.eqNotifyDisequal(t1, t2, reason);
+    }
+
+  };/* class TheoryUF::NotifyClass */
+
+  /** A callback class for ppRewrite().  See registerPpRewrite(), below. */
+  class PpRewrite {
+  public:
+    virtual Node ppRewrite(TNode node) = 0;
+  };/* class TheoryUF::PpRewrite */
 
 private:
 
   /** The notify class */
   NotifyClass d_notify;
 
+  /** The associated theory strong solver (or NULL if none) */
+  StrongSolverTheoryUf* d_thss;
+
   /** Equaltity engine */
   eq::EqualityEngine d_equalityEngine;
 
@@ -118,10 +156,37 @@ private:
   /** Conflict when merging two constants */
   void conflict(TNode a, TNode b);
 
+  /** called when a new equivalance class is created */
+  void eqNotifyNewClass(TNode t);
+
+  /** called when two equivalance classes will merge */
+  void eqNotifyPreMerge(TNode t1, TNode t2);
+
+  /** called when two equivalance classes have merged */
+  void eqNotifyPostMerge(TNode t1, TNode t2);
+
+  /** called when two equivalence classes are made disequal */
+  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+
+  /** a registry type for keeping Node-specific callbacks for ppRewrite() */
+  typedef std::hash_map<Node, PpRewrite*, NodeHashFunction> RegisterPpRewrites;
+
+  /** a collection of callbacks to issue while doing a ppRewrite() */
+  RegisterPpRewrites d_registeredPpRewrites;
+
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+
+  ~TheoryUF() {
+    // destruct all ppRewrite() callbacks
+    for(RegisterPpRewrites::iterator i = d_registeredPpRewrites.begin();
+        i != d_registeredPpRewrites.end();
+        ++i) {
+      delete i->second;
+    }
+  }
 
   void check(Effort);
   void preRegisterTerm(TNode term);
@@ -133,7 +198,7 @@ public:
   void addSharedTerm(TNode n);
   void computeCareGraph();
 
-  void propagate(Effort effort) {}
+  void propagate(Effort effort);
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
@@ -141,6 +206,24 @@ public:
     return "THEORY_UF";
   }
 
+  eq::EqualityEngine* getEqualityEngine() {
+    return &d_equalityEngine;
+  }
+
+  StrongSolverTheoryUf* getStrongSolver() {
+    return d_thss;
+  }
+
+  Node ppRewrite(TNode node);
+
+  /**
+   * Register a ppRewrite() callback on "op."  TheoryUF owns
+   * the callback, and will delete it when it is destructed.
+   */
+  void registerPpRewrite(TNode op, PpRewrite* callback) {
+    d_registeredPpRewrites.insert(std::make_pair(op, callback));
+  }
+
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */
diff --git a/src/theory/uf/theory_uf_candidate_generator.cpp b/src/theory/uf/theory_uf_candidate_generator.cpp
new file mode 100644
index 000000000..e8aa98aa7
--- /dev/null
+++ b/src/theory/uf/theory_uf_candidate_generator.cpp
@@ -0,0 +1,170 @@
+/*********************                                                        */
+/*! \file theory_uf_candidate_generator.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of theory uf candidate generator class
+ **/
+
+#include "theory/uf/theory_uf_candidate_generator.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/theory_uf.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+
+CandidateGeneratorTheoryUf::CandidateGeneratorTheoryUf( InstantiatorTheoryUf* ith, Node op ) : 
+  d_op( op ), d_ith( ith ), d_term_iter( -2 ){
+  Assert( !d_op.isNull() );
+}
+void CandidateGeneratorTheoryUf::resetInstantiationRound(){
+  d_term_iter_limit = d_ith->getQuantifiersEngine()->getTermDatabase()->d_op_map[d_op].size();
+}
+
+void CandidateGeneratorTheoryUf::reset( Node eqc ){
+  if( eqc.isNull() ){
+    d_term_iter = 0;
+  }else{
+    //create an equivalence class iterator in eq class eqc
+    if( ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->hasTerm( eqc ) ){
+      eqc = ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->getRepresentative( eqc );
+      d_eqc = eq::EqClassIterator( eqc, ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() );
+      d_retNode = Node::null();
+    }else{
+      d_retNode = eqc;
+    }
+    d_term_iter = -1;
+  }
+}
+
+Node CandidateGeneratorTheoryUf::getNextCandidate(){
+  if( d_term_iter>=0 ){
+    //get next candidate term in the uf term database
+    while( d_term_iter<d_term_iter_limit ){
+      Node n = d_ith->getQuantifiersEngine()->getTermDatabase()->d_op_map[d_op][d_term_iter];
+      d_term_iter++;
+      if( isLegalCandidate( n ) ){
+        return n;
+      }
+    }
+  }else if( d_term_iter==-1 ){
+    if( d_retNode.isNull() ){
+      //get next candidate term in equivalence class
+      while( !d_eqc.isFinished() ){
+        Node n = (*d_eqc);
+        ++d_eqc;
+        if( n.getKind()==APPLY_UF && n.getOperator()==d_op ){
+          if( isLegalCandidate( n ) ){
+            return n;
+          }
+        }
+      }
+    }else{
+      Node ret;
+      if( d_retNode.hasOperator() && d_retNode.getOperator()==d_op ){
+        ret = d_retNode;
+      }
+      d_term_iter = -2; //done returning matches
+      return ret;
+    }
+  }
+  return Node::null();
+}
+
+
+//CandidateGeneratorTheoryUfDisequal::CandidateGeneratorTheoryUfDisequal( InstantiatorTheoryUf* ith, Node eqc ) : 
+//  d_ith( ith ), d_eq_class( eqc ){
+//  d_eci = NULL;
+//}
+//void CandidateGeneratorTheoryUfDisequal::resetInstantiationRound(){
+//  
+//}
+////we will iterate over all terms that are disequal from eqc
+//void CandidateGeneratorTheoryUfDisequal::reset( Node eqc ){
+//  //Assert( !eqc.isNull() );
+//  ////begin iterating over equivalence classes that are disequal from eqc
+//  //d_eci = d_ith->getEquivalenceClassInfo( eqc );
+//  //if( d_eci ){
+//  //  d_eqci_iter = d_eci->d_disequal.begin();
+//  //}
+//}
+//Node CandidateGeneratorTheoryUfDisequal::getNextCandidate(){
+//  //if( d_eci ){
+//  //  while( d_eqci_iter != d_eci->d_disequal.end() ){
+//  //    if( (*d_eqci_iter).second ){
+//  //      //we have an equivalence class that is disequal from eqc
+//  //      d_cg->reset( (*d_eqci_iter).first );
+//  //      Node n = d_cg->getNextCandidate();
+//  //      //if there is a candidate in this equivalence class, return it
+//  //      if( !n.isNull() ){
+//  //        return n;
+//  //      }
+//  //    }
+//  //    ++d_eqci_iter;
+//  //  }
+//  //}
+//  return Node::null();
+//}
+
+
+CandidateGeneratorTheoryUfLitEq::CandidateGeneratorTheoryUfLitEq( InstantiatorTheoryUf* ith, Node mpat ) : 
+  d_match_pattern( mpat ), d_ith( ith ){
+  
+}
+void CandidateGeneratorTheoryUfLitEq::resetInstantiationRound(){
+  
+}
+void CandidateGeneratorTheoryUfLitEq::reset( Node eqc ){
+  d_eq = eq::EqClassesIterator( ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() );
+}
+Node CandidateGeneratorTheoryUfLitEq::getNextCandidate(){
+  while( d_eq.isFinished() ){
+    Node n = (*d_eq);
+    ++d_eq;
+    if( n.getType()==d_match_pattern[0].getType() ){
+      //an equivalence class with the same type as the pattern, return reflexive equality
+      return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
+    }
+  }
+  return Node::null();
+}
+
+
+CandidateGeneratorTheoryUfLitDeq::CandidateGeneratorTheoryUfLitDeq( InstantiatorTheoryUf* ith, Node mpat ) : 
+  d_match_pattern( mpat ), d_ith( ith ){
+  
+}
+void CandidateGeneratorTheoryUfLitDeq::resetInstantiationRound(){
+  
+}
+void CandidateGeneratorTheoryUfLitDeq::reset( Node eqc ){
+  Node false_term = ((TheoryUF*)d_ith->getTheory())->getEqualityEngine()->getRepresentative( 
+                      NodeManager::currentNM()->mkConst<bool>(false) );
+  d_eqc_false = eq::EqClassIterator( false_term, ((TheoryUF*)d_ith->getTheory())->getEqualityEngine() );
+}
+Node CandidateGeneratorTheoryUfLitDeq::getNextCandidate(){
+  //get next candidate term in equivalence class
+  while( !d_eqc_false.isFinished() ){
+    Node n = (*d_eqc_false);
+    ++d_eqc_false;
+    if( n.getKind()==d_match_pattern.getKind() ){
+      //found an iff or equality, try to match it
+      //DO_THIS: cache to avoid redundancies?
+      //DO_THIS: do we need to try the symmetric equality for n?  or will it also exist in the eq class of false?
+      return n;
+    }
+  }
+  return Node::null();
+}
diff --git a/src/theory/uf/theory_uf_candidate_generator.h b/src/theory/uf/theory_uf_candidate_generator.h
new file mode 100644
index 000000000..948573439
--- /dev/null
+++ b/src/theory/uf/theory_uf_candidate_generator.h
@@ -0,0 +1,115 @@
+/*********************                                                        */
+/*! \file theory_uf_candidate generator.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Theory uf candidate generator
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H
+#define __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/uf/theory_uf_instantiator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+class CandidateGeneratorTheoryUfDisequal;
+
+class CandidateGeneratorTheoryUf : public CandidateGenerator
+{
+  friend class CandidateGeneratorTheoryUfDisequal;
+private:
+  //operator you are looking for
+  Node d_op;
+  //instantiator pointer
+  InstantiatorTheoryUf* d_ith;
+  //the equality class iterator
+  eq::EqClassIterator d_eqc;
+  int d_term_iter;
+  int d_term_iter_limit;
+private:
+  Node d_retNode;
+public:
+  CandidateGeneratorTheoryUf( InstantiatorTheoryUf* ith, Node op );
+  ~CandidateGeneratorTheoryUf(){}
+
+  void resetInstantiationRound();
+  void reset( Node eqc );
+  Node getNextCandidate();
+};
+
+//class CandidateGeneratorTheoryUfDisequal : public CandidateGenerator
+//{
+//private:
+//  //equivalence class 
+//  Node d_eq_class;
+//  //equivalence class info
+//  EqClassInfo* d_eci;
+//  //equivalence class iterator
+//  EqClassInfo::BoolMap::const_iterator d_eqci_iter;
+//  //instantiator pointer
+//  InstantiatorTheoryUf* d_ith;
+//public:
+//  CandidateGeneratorTheoryUfDisequal( InstantiatorTheoryUf* ith, Node eqc );
+//  ~CandidateGeneratorTheoryUfDisequal(){}
+//
+//  void resetInstantiationRound();
+//  void reset( Node eqc );   //should be what you want to be disequal from
+//  Node getNextCandidate();
+//};
+
+class CandidateGeneratorTheoryUfLitEq : public CandidateGenerator
+{
+private:
+  //the equality classes iterator
+  eq::EqClassesIterator d_eq;
+  //equality you are trying to match equalities for
+  Node d_match_pattern;
+  //einstantiator pointer
+  InstantiatorTheoryUf* d_ith;
+public:
+  CandidateGeneratorTheoryUfLitEq( InstantiatorTheoryUf* ith, Node mpat );
+  ~CandidateGeneratorTheoryUfLitEq(){}
+
+  void resetInstantiationRound();
+  void reset( Node eqc );
+  Node getNextCandidate();
+};
+
+class CandidateGeneratorTheoryUfLitDeq : public CandidateGenerator
+{
+private:
+  //the equality class iterator for false
+  eq::EqClassIterator d_eqc_false;
+  //equality you are trying to match disequalities for
+  Node d_match_pattern;
+  //einstantiator pointer
+  InstantiatorTheoryUf* d_ith;
+public:
+  CandidateGeneratorTheoryUfLitDeq( InstantiatorTheoryUf* ith, Node mpat );
+  ~CandidateGeneratorTheoryUfLitDeq(){}
+
+  void resetInstantiationRound();
+  void reset( Node eqc );
+  Node getNextCandidate();
+};
+
+
+}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
new file mode 100644
index 000000000..9fdcb5952
--- /dev/null
+++ b/src/theory/uf/theory_uf_instantiator.cpp
@@ -0,0 +1,520 @@
+/*********************                                                        */
+/*! \file theory_uf_instantiator.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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/uf/inst_strategy_model_find.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+
+EqClassInfo::EqClassInfo( context::Context* c ) : d_funs( c ), d_pfuns( c ), d_disequal( c ){
+
+}
+
+//set member
+void EqClassInfo::setMember( Node n, TermDb* db ){
+  if( n.getKind()==APPLY_UF ){
+    d_funs[n.getOperator()] = true;
+  }
+  //add parent functions
+  for( std::map< Node, std::map< int, std::vector< Node > > >::iterator it = db->d_parents[n].begin();
+    it != db->d_parents[n].end(); ++it ){
+    d_pfuns[ it->first ] = true;
+  }
+}
+
+//get has function
+bool EqClassInfo::hasFunction( Node op ){
+  return d_funs.find( op )!=d_funs.end();
+}
+
+bool EqClassInfo::hasParent( Node op ){
+  return d_pfuns.find( op )!=d_pfuns.end();
+}
+
+//merge with another eq class info
+void EqClassInfo::merge( EqClassInfo* eci ){
+  for( BoolMap::iterator it = eci->d_funs.begin(); it != eci->d_funs.end(); it++ ) {
+    d_funs[ (*it).first ] = true;
+  }
+  for( BoolMap::iterator it = eci->d_pfuns.begin(); it != eci->d_pfuns.end(); it++ ) {
+    d_pfuns[ (*it).first ] = true;
+  }
+}
+
+InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th) :
+Instantiator( c, qe, th )
+{
+  qe->setEqualityQuery( new EqualityQueryInstantiatorTheoryUf( this ) );
+
+  if( Options::current()->finiteModelFind ){
+    //if( Options::current()->cbqi ){
+    //  addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
+    //}
+    //addInstStrategy( new InstStrategyFiniteModelFind( c, this, ((TheoryUF*)th)->getStrongSolver(), qe ) );
+    qe->getTermDatabase()->setMatchingActive( false );
+  }else{
+    if( Options::current()->cbqi ){
+      addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
+    }
+    if( Options::current()->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 ) );
+    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 );
+  d_quantEngine->addTermToDatabase( assertion );
+  if( Options::current()->cbqi ){
+    if( assertion.hasAttribute(InstConstantAttribute()) ){
+      setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
+    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
+      setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) );
+    }
+  }
+}
+
+void InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){
+  if( d_isup ){
+    d_isup->addUserPattern( f, pat );
+  }
+  setHasConstraintsFrom( f );
+}
+
+
+void InstantiatorTheoryUf::processResetInstantiationRound( Theory::Effort effort ){
+  d_ground_reps.clear();
+}
+
+int InstantiatorTheoryUf::process( Node f, Theory::Effort effort, int e, int instLimit ){
+  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( hasTerm( a ) && hasTerm( b ) ){
+    return ((TheoryUF*)d_th)->d_equalityEngine.areEqual( a, b );
+  }else{
+    return a==b;
+  }
+}
+
+bool InstantiatorTheoryUf::areDisequal( Node a, Node b ){
+  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;
+  }
+}
+
+Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
+  if( d_ground_reps.find( a )==d_ground_reps.end() ){
+    if( !hasTerm( a ) ){
+      return a;
+    }else{
+      Node rep = getRepresentative( a );
+      if( !rep.hasAttribute(InstConstantAttribute()) ){
+        //return the representative of a
+        d_ground_reps[a] = rep;
+        return rep;
+      }else{
+        //otherwise, must search eq class
+        eq::EqClassIterator eqc_iter( rep, &((TheoryUF*)d_th)->d_equalityEngine );
+        rep = Node::null();
+        while( !eqc_iter.isFinished() ){
+          if( !(*eqc_iter).hasAttribute(InstConstantAttribute()) ){
+            d_ground_reps[ a ] = *eqc_iter;
+            return *eqc_iter;
+          }
+          eqc_iter++;
+        }
+        d_ground_reps[ a ] = a;
+      }
+    }
+  }
+  return d_ground_reps[a];
+}
+
+InstantiatorTheoryUf::Statistics::Statistics():
+  //d_instantiations("InstantiatorTheoryUf::Total_Instantiations", 0),
+  d_instantiations_ce_solved("InstantiatorTheoryUf::Instantiations_CE-Solved", 0),
+  d_instantiations_e_induced("InstantiatorTheoryUf::Instantiations_E-Induced", 0),
+  d_instantiations_user_pattern("InstantiatorTheoryUf::Instantiations_User_Pattern", 0),
+  d_instantiations_guess("InstantiatorTheoryUf::Instantiations_Free_Var", 0),
+  d_instantiations_auto_gen("InstantiatorTheoryUf::Instantiations_Auto_Gen", 0),
+  d_instantiations_auto_gen_min("InstantiatorTheoryUf::Instantiations_Auto_Gen_Min", 0),
+  d_splits("InstantiatorTheoryUf::Total_Splits", 0)
+{
+  //StatisticsRegistry::registerStat(&d_instantiations);
+  StatisticsRegistry::registerStat(&d_instantiations_ce_solved);
+  StatisticsRegistry::registerStat(&d_instantiations_e_induced);
+  StatisticsRegistry::registerStat(&d_instantiations_user_pattern );
+  StatisticsRegistry::registerStat(&d_instantiations_guess );
+  StatisticsRegistry::registerStat(&d_instantiations_auto_gen );
+  StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min );
+  StatisticsRegistry::registerStat(&d_splits);
+}
+
+InstantiatorTheoryUf::Statistics::~Statistics(){
+  //StatisticsRegistry::unregisterStat(&d_instantiations);
+  StatisticsRegistry::unregisterStat(&d_instantiations_ce_solved);
+  StatisticsRegistry::unregisterStat(&d_instantiations_e_induced);
+  StatisticsRegistry::unregisterStat(&d_instantiations_user_pattern );
+  StatisticsRegistry::unregisterStat(&d_instantiations_guess );
+  StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen );
+  StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min );
+  StatisticsRegistry::unregisterStat(&d_splits);
+}
+
+/** new node */
+void InstantiatorTheoryUf::newEqClass( TNode n ){
+  d_quantEngine->addTermToDatabase( n );
+}
+
+/** merge */
+void InstantiatorTheoryUf::merge( TNode a, TNode b ){
+  if( Options::current()->efficientEMatching ){
+    if( a.getKind()!=IFF && a.getKind()!=EQUAL && b.getKind()!=IFF && b.getKind()!=EQUAL ){
+      Debug("efficient-e-match") << "Merging " << a << " with " << b << std::endl;
+
+      //determine new candidates for instantiation
+      computeCandidatesPcPairs( a, b );
+      computeCandidatesPcPairs( b, a );
+      computeCandidatesPpPairs( a, b );
+      computeCandidatesPpPairs( b, a );
+    }
+    //merge eqc_ops of b into a
+    EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a );
+    EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( b );
+    eci_a->merge( eci_b );
+  }
+}
+
+/** assert terms are disequal */
+void InstantiatorTheoryUf::assertDisequal( TNode a, TNode b, TNode reason ){
+
+}
+
+EqClassInfo* InstantiatorTheoryUf::getEquivalenceClassInfo( Node n ) {
+  return d_eqc_ops.find( n )==d_eqc_ops.end() ? NULL : d_eqc_ops[n];
+}
+EqClassInfo* InstantiatorTheoryUf::getOrCreateEquivalenceClassInfo( Node n ){
+  Assert( n==getRepresentative( n ) );
+  if( d_eqc_ops.find( n )==d_eqc_ops.end() ){
+    EqClassInfo* eci = new EqClassInfo( d_th->getSatContext() );
+    eci->setMember( n, d_quantEngine->getTermDatabase() );
+    d_eqc_ops[n] = eci;
+  }
+  return d_eqc_ops[n];
+}
+
+void InstantiatorTheoryUf::computeCandidatesPcPairs( Node a, Node b ){
+  Debug("efficient-e-match") << "Compute candidates for pc pairs..." << std::endl;
+  Debug("efficient-e-match") << "  Eq class = [";
+  outputEqClass( "efficient-e-match", a);
+  Debug("efficient-e-match") << "]" << std::endl;
+  EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a );
+  EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( a );
+  for( BoolMap::iterator it = eci_a->d_funs.begin(); it != eci_a->d_funs.end(); it++ ) {
+    //the child function:  a member of eq_class( a ) has top symbol g, in other words g is in funs( a )
+    Node g = (*it).first;
+    Debug("efficient-e-match") << "  Checking application " << g << std::endl;
+    //look at all parent/child pairs
+    for( std::map< Node, std::map< Node, std::vector< InvertedPathString > > >::iterator itf = d_pc_pairs[g].begin();
+         itf != d_pc_pairs[g].end(); ++itf ){
+      //f/g is a parent/child pair
+      Node f = itf->first;
+      if( eci_b->hasParent( f ) || true ){
+        //DO_THIS: determine if f in pfuns( b ), only do the follow if so
+        Debug("efficient-e-match") << "    Checking parent application " << f << std::endl;
+        //scan through the list of inverted path strings/candidate generators
+        for( std::map< Node, std::vector< InvertedPathString > >::iterator cit = itf->second.begin();
+            cit != itf->second.end(); ++cit ){
+          Node pat = cit->first;
+          Debug("efficient-e-match") << "      Checking pattern " << pat << std::endl;
+          for( int c=0; c<(int)cit->second.size(); c++ ){
+            Debug("efficient-e-match") << "        Check inverted path string for pattern ";
+            outputInvertedPathString( "efficient-e-match", cit->second[c] );
+            Debug("efficient-e-match") << std::endl;
+
+            //collect all new relevant terms
+            std::vector< Node > terms;
+            terms.push_back( b );
+            collectTermsIps( cit->second[c], terms );
+            if( !terms.empty() ){
+              Debug("efficient-e-match") << "        -> Added terms (" << (int)terms.size() << "): ";
+              //add them as candidates to the candidate generator
+              for( int t=0; t<(int)terms.size(); t++ ){
+                Debug("efficient-e-match") << terms[t] << " ";
+                //Notice() << "Add candidate (PC) " << terms[t] << std::endl;
+                for( int cg=0; cg<(int)d_pat_cand_gens[pat].size(); cg++ ){
+                  d_pat_cand_gens[pat][cg]->addCandidate( terms[t] );
+                }
+              }
+              Debug("efficient-e-match") << std::endl;
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+void InstantiatorTheoryUf::computeCandidatesPpPairs( Node a, Node b ){
+  Debug("efficient-e-match") << "Compute candidates for pp pairs..." << std::endl;
+  EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a );
+  EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( a );
+  for( std::map< Node, std::map< Node, std::map< Node, std::vector< IpsPair > > > >::iterator it = d_pp_pairs.begin();
+       it != d_pp_pairs.end(); ++it ){
+    Node f = it->first;
+    if( eci_a->hasParent( f ) ){
+      Debug("efficient-e-match") << "  Checking parent application " << f << std::endl;
+      for( std::map< Node, std::map< Node, std::vector< IpsPair > > >::iterator it2 = it->second.begin();
+           it2 != it->second.end(); ++it2 ){
+        Node g = it2->first;
+        if( eci_b->hasParent( g ) ){
+          Debug("efficient-e-match") << "    Checking parent application " << g << std::endl;
+          //if f in pfuns( a ) and g is in pfuns( b ), only do the follow if so
+          for( std::map< Node, std::vector< IpsPair > >::iterator cit = it2->second.begin();
+               cit != it2->second.end(); ++cit ){
+            Node pat = cit->first;
+            for( int c=0; c<(int)cit->second.size(); c++ ){
+              std::vector< Node > a_terms;
+              a_terms.push_back( a );
+              if( !a_terms.empty() ){
+                collectTermsIps( cit->second[c].first, a_terms );
+                std::vector< Node > b_terms;
+                b_terms.push_back( b );
+                collectTermsIps( cit->second[c].first, b_terms );
+                //take intersection
+                for( int t=0; t<(int)a_terms.size(); t++ ){
+                  if( std::find( b_terms.begin(), b_terms.end(), a_terms[t] )!=b_terms.end() ){
+                                //Notice() << "Add candidate (PP) " << a_terms[t] << std::endl;
+                    Debug("efficient-e-match") << "      -> Add term " << a_terms[t] << std::endl;
+                    //add to all candidate generators having this term
+                    for( int cg=0; cg<(int)d_pat_cand_gens[pat].size(); cg++ ){
+                      d_pat_cand_gens[pat][cg]->addCandidate( a_terms[t] );
+                    }
+                  }
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+void InstantiatorTheoryUf::collectTermsIps( InvertedPathString& ips, std::vector< Node >& terms, int index ){
+  if( index<(int)ips.size() && !terms.empty() ){
+    Debug("efficient-e-match-debug") << "> Process " << index << std::endl;
+    Node f = ips[index].first;
+    int arg = ips[index].second;
+
+    //for each term in terms, determine if any term (modulo equality) has parent "f" from position "arg"
+    bool addRep = ( index!=(int)ips.size()-1 );
+    std::vector< Node > newTerms;
+    for( int t=0; t<(int)terms.size(); t++ ){
+      collectParentsTermsIps( terms[t], f, arg, newTerms, addRep );
+    }
+    terms.clear();
+    terms.insert( terms.begin(), newTerms.begin(), newTerms.end() );
+
+    Debug("efficient-e-match-debug") << "> Terms are now: ";
+    for( int t=0; t<(int)terms.size(); t++ ){
+      Debug("efficient-e-match-debug") << terms[t] << " ";
+    }
+    Debug("efficient-e-match-debug") << std::endl;
+
+    collectTermsIps( ips, terms, index+1 );
+  }
+}
+
+bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, std::vector< Node >& terms, bool addRep, bool modEq ){
+  bool addedTerm = false;
+  if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) && modEq ){
+    Assert( getRepresentative( n )==n );
+    //collect modulo equality
+    //DO_THIS: this should (if necessary) compute a current set of (f, arg) parents for n and cache it
+    eq::EqClassIterator eqc_iter( getRepresentative( n ), &((TheoryUF*)d_th)->d_equalityEngine );
+    while( !eqc_iter.isFinished() ){
+      if( collectParentsTermsIps( (*eqc_iter), f, arg, terms, addRep, false ) ){
+        //if only one argument, we know we can stop (since all others added will be congruent)
+        if( f.getType().getNumChildren()==2 ){
+          return true;
+        }
+        addedTerm = true;
+      }
+      eqc_iter++;
+    }
+  }else{
+    TermDb* db = d_quantEngine->getTermDatabase();
+    //see if parent f exists from argument arg
+    if( db->d_parents.find( n )!=db->d_parents.end() ){
+      if( db->d_parents[n].find( f )!=db->d_parents[n].end() ){
+        if( db->d_parents[n][f].find( arg )!=db->d_parents[n][f].end() ){
+          for( int i=0; i<(int)db->d_parents[n][f][arg].size(); i++ ){
+            Node t = db->d_parents[n][f][arg][i];
+            if( addRep ){
+              t = getRepresentative( t );
+            }
+            if( std::find( terms.begin(), terms.end(), t )==terms.end() ){
+              terms.push_back( t );
+            }
+            addedTerm = true;
+          }
+        }
+      }
+    }
+  }
+  return addedTerm;
+}
+
+void InstantiatorTheoryUf::registerPatternElementPairs2( Node opat, Node pat, InvertedPathString& ips,
+                                                       std::map< Node, std::vector< std::pair< Node, InvertedPathString > > >& ips_map  ){
+  Assert( pat.getKind()==APPLY_UF );
+  //add information for possible pp-pair
+  for( int i=0; i<(int)pat.getNumChildren(); i++ ){
+    if( pat[i].getKind()==INST_CONSTANT ){
+      ips_map[ pat[i] ].push_back( std::pair< Node, InvertedPathString >( pat.getOperator(), InvertedPathString( ips ) ) );
+    }
+  }
+  ips.push_back( std::pair< Node, int >( pat.getOperator(), 0 ) );
+  for( int i=0; i<(int)pat.getNumChildren(); i++ ){
+    if( pat[i].getKind()==APPLY_UF ){
+      ips.back().second = i;
+      registerPatternElementPairs2( opat, pat[i], ips, ips_map );
+      Debug("pattern-element-opt") << "Found pc-pair ( " << pat.getOperator() << ", " << pat[i].getOperator() << " )" << std::endl;
+      Debug("pattern-element-opt") << "   Path = ";
+      outputInvertedPathString( "pattern-element-opt", ips );
+      Debug("pattern-element-opt") << std::endl;
+      //pat.getOperator() and pat[i].getOperator() are a pc-pair
+      d_pc_pairs[ pat[i].getOperator() ][ pat.getOperator() ][opat].push_back( InvertedPathString( ips ) );
+    }
+  }
+  ips.pop_back();
+}
+
+void InstantiatorTheoryUf::registerPatternElementPairs( Node pat ){
+  InvertedPathString ips;
+  std::map< Node, std::vector< std::pair< Node, InvertedPathString > > > ips_map;
+  registerPatternElementPairs2( pat, pat, ips, ips_map );
+  for( std::map< Node, std::vector< std::pair< Node, InvertedPathString > > >::iterator it = ips_map.begin(); it != ips_map.end(); ++it ){
+    for( int j=0; j<(int)it->second.size(); j++ ){
+      for( int k=j+1; k<(int)it->second.size(); k++ ){
+        //found a pp-pair
+        Debug("pattern-element-opt") << "Found pp-pair ( " << it->second[j].first << ", " << it->second[k].first << " )" << std::endl;
+        Debug("pattern-element-opt") << "   Paths = ";
+        outputInvertedPathString( "pattern-element-opt", it->second[j].second );
+        Debug("pattern-element-opt") << " and ";
+        outputInvertedPathString( "pattern-element-opt", it->second[k].second );
+        Debug("pattern-element-opt") << std::endl;
+        d_pp_pairs[ it->second[j].first ][ it->second[k].first ][pat].push_back( IpsPair( it->second[j].second, it->second[k].second ) );
+      }
+    }
+  }
+}
+
+void InstantiatorTheoryUf::registerCandidateGenerator( CandidateGenerator* cg, Node pat ){
+  Debug("efficient-e-match") << "Register candidate generator..." << pat << std::endl;
+  if( d_pat_cand_gens.find( pat )==d_pat_cand_gens.end() ){
+    registerPatternElementPairs( pat );
+  }
+  d_pat_cand_gens[pat].push_back( cg );
+
+  //take all terms from the uf term db and add to candidate generator
+  Node op = pat.getOperator();
+  TermDb* db = d_quantEngine->getTermDatabase();
+  for( int i=0; i<(int)db->d_op_map[op].size(); i++ ){
+    cg->addCandidate( db->d_op_map[op][i] );
+  }
+  d_cand_gens[op].push_back( cg );
+
+  Debug("efficient-e-match") << "Done." << std::endl;
+}
+
+void InstantiatorTheoryUf::registerTrigger( Trigger* tr, Node op ){
+  if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
+    d_op_triggers[op].push_back( tr );
+  }
+}
+
+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;
+  }
+}
+
+void InstantiatorTheoryUf::outputInvertedPathString( const char* c, InvertedPathString& ips ){
+  for( int i=0; i<(int)ips.size(); i++ ){
+    if( i>0 ){ Debug( c ) << "."; }
+    Debug( c ) << ips[i].first << "." << ips[i].second;
+  }
+}
diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h
new file mode 100644
index 000000000..e50e3823c
--- /dev/null
+++ b/src/theory/uf/theory_uf_instantiator.h
@@ -0,0 +1,201 @@
+/*********************                                                        */
+/*! \file theory_uf_instantiator.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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/stats.h"
+#include "theory/uf/theory_uf.h"
+
+namespace CVC4 {
+namespace theory {
+
+class TermDb;
+
+namespace uf {
+
+class InstantiatorTheoryUf;
+
+//equivalence class info
+class EqClassInfo
+{
+public:
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
+  typedef context::CDChunkList<Node> NodeList;
+public:
+  //a list of operators that occur as top symbols in this equivalence class
+  //  Efficient E-Matching for SMT Solvers: "funs"
+  BoolMap d_funs;
+  //a list of operators f for which a term of the form f( ... t ... ) exists
+  //  Efficient E-Matching for SMT Solvers: "pfuns"
+  BoolMap d_pfuns;
+  //a list of equivalence classes that are disequal
+  BoolMap d_disequal;
+public:
+  EqClassInfo( context::Context* c );
+  ~EqClassInfo(){}
+  //set member
+  void setMember( Node n, TermDb* db );
+  //has function "funs"
+  bool hasFunction( Node op );
+  //has parent "pfuns"
+  bool hasParent( Node op );
+  //merge with another eq class info
+  void merge( EqClassInfo* eci );
+};
+
+class InstantiatorTheoryUf : public Instantiator{
+  friend class ::CVC4::theory::InstMatchGenerator;
+  friend class ::CVC4::theory::TermDb;
+protected:
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
+  typedef context::CDHashMap<Node, int, NodeHashFunction> IntMap;
+  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeLists;
+  /** map to representatives used */
+  std::map< Node, Node > d_ground_reps;
+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, int instLimit );
+public:
+  /** statistics class */
+  class Statistics {
+  public:
+    //IntStat d_instantiations;
+    IntStat d_instantiations_ce_solved;
+    IntStat d_instantiations_e_induced;
+    IntStat d_instantiations_user_pattern;
+    IntStat d_instantiations_guess;
+    IntStat d_instantiations_auto_gen;
+    IntStat d_instantiations_auto_gen_min;
+    IntStat d_splits;
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
+public:
+  /** the base match */
+  std::map< Node, InstMatch > d_baseMatch;
+private:
+  //for each equivalence class
+  std::map< Node, EqClassInfo* > d_eqc_ops;
+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 );
+  /** new node */
+  void newEqClass( TNode n );
+  /** merge */
+  void merge( TNode a, TNode b );
+  /** assert terms are disequal */
+  void assertDisequal( TNode a, TNode b, TNode reason );
+  /** get equivalence class info */
+  EqClassInfo* getEquivalenceClassInfo( Node n );
+  EqClassInfo* getOrCreateEquivalenceClassInfo( Node n );
+private:
+  typedef std::vector< std::pair< Node, int > > InvertedPathString;
+  typedef std::pair< InvertedPathString, InvertedPathString > IpsPair;
+  /** Parent/Child Pairs (for efficient E-matching)
+      So, for example, if we have the pattern f( g( x ) ), then d_pc_pairs[g][f][f( g( x ) )] = { f.0 }.
+  */
+  std::map< Node, std::map< Node, std::map< Node, std::vector< InvertedPathString > > > > d_pc_pairs;
+  /** Parent/Parent Pairs (for efficient E-matching) */
+  std::map< Node, std::map< Node, std::map< Node, std::vector< IpsPair > > > > d_pp_pairs;
+  /** list of all candidate generators for each operator */
+  std::map< Node, std::vector< CandidateGenerator* > > d_cand_gens;
+  /** map from patterns to candidate generators */
+  std::map< Node, std::vector< CandidateGenerator* > > d_pat_cand_gens;
+  /** helper functions */
+  void registerPatternElementPairs2( Node opat, Node pat, InvertedPathString& ips,
+                                     std::map< Node, std::vector< std::pair< Node, InvertedPathString > > >& ips_map );
+  void registerPatternElementPairs( Node pat );
+  /** compute candidates for pc pairs */
+  void computeCandidatesPcPairs( Node a, Node b );
+  /** compute candidates for pp pairs */
+  void computeCandidatesPpPairs( Node a, Node b );
+  /** collect terms based on inverted path string */
+  void collectTermsIps( InvertedPathString& ips, std::vector< Node >& terms, int index = 0 );
+  bool collectParentsTermsIps( Node n, Node f, int arg, std::vector< Node >& terms, bool addRep, bool modEq = true );
+public:
+  /** Register candidate generator cg for pattern pat. (for use with efficient e-matching)
+      This request will ensure that calls will be made to cg->addCandidate( n ) for all
+      ground terms n that are relevant for matching with pat.
+  */
+  void registerCandidateGenerator( CandidateGenerator* cg, Node pat );
+private:
+  /** triggers */
+  std::map< Node, std::vector< Trigger* > > d_op_triggers;
+public:
+  /** register trigger (for eager quantifier instantiation) */
+  void registerTrigger( Trigger* tr, Node op );
+public:
+  /** output eq class */
+  void outputEqClass( const char* c, Node n );
+  /** output inverted path string */
+  void outputInvertedPathString( const char* c, InvertedPathString& ips );
+};/* class InstantiatorTheoryUf */
+
+/** equality query object using instantiator theory uf */
+class EqualityQueryInstantiatorTheoryUf : public EqualityQuery
+{
+private:
+  /** pointer to instantiator uf class */
+  InstantiatorTheoryUf* d_ith;
+public:
+  EqualityQueryInstantiatorTheoryUf( InstantiatorTheoryUf* ith ) : d_ith( ith ){}
+  ~EqualityQueryInstantiatorTheoryUf(){}
+  /** general queries about equality */
+  bool hasTerm( Node a ) { return d_ith->hasTerm( a ); }
+  Node getRepresentative( Node a ) { return d_ith->getRepresentative( a ); }
+  bool areEqual( Node a, Node b ) { return d_ith->areEqual( a, b ); }
+  bool areDisequal( Node a, Node b ) { return d_ith->areDisequal( a, b ); }
+  Node getInternalRepresentative( Node a ) { return d_ith->getInternalRepresentative( a ); }
+}; /* EqualityQueryInstantiatorTheoryUf */
+
+}
+}/* 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
new file mode 100644
index 000000000..a793b6a57
--- /dev/null
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -0,0 +1,1267 @@
+/*********************                                                        */
+/*! \file theory_uf_strong_solver.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of theory uf strong solver class
+ **/
+
+#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"
+
+//#define USE_REGION_SAT
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+
+void StrongSolverTheoryUf::ConflictFind::Region::takeNode( StrongSolverTheoryUf::ConflictFind::Region* r, Node n ){
+  //Debug("uf-ss") << "takeNode " << r << " " << n << std::endl;
+  //Debug("uf-ss") << "r : " << std::endl;
+  //r->debugPrint("uf-ss");
+  //Debug("uf-ss") << "this : " << std::endl;
+  //debugPrint("uf-ss");
+  Assert( !hasRep( n ) );
+  Assert( r->hasRep( n ) );
+  //add representative
+  setRep( n, true );
+  //take disequalities from r
+  RegionNodeInfo* rni = r->d_nodes[n];
+  for( int t=0; t<2; t++ ){
+    RegionNodeInfo::DiseqList* del = rni->d_disequalities[t];
+    for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){
+      if( (*it).second ){
+        r->setDisequal( n, (*it).first, t, false );
+        if( t==0 ){
+          if( hasRep( (*it).first ) ){
+            setDisequal( (*it).first, n, 0, false );
+            setDisequal( (*it).first, n, 1, true );
+            setDisequal( n, (*it).first, 1, true );
+          }else{
+            setDisequal( n, (*it).first, 0, true );
+          }
+        }else{
+          r->setDisequal( (*it).first, n, 1, false );
+          r->setDisequal( (*it).first, n, 0, true );
+          setDisequal( n, (*it).first, 0, true );
+        }
+      }
+    }
+  }
+  //remove representative
+  r->setRep( n, false );
+  //Debug("uf-ss") << "done takeNode " << r << " " << n << std::endl;
+}
+
+void StrongSolverTheoryUf::ConflictFind::Region::combine( StrongSolverTheoryUf::ConflictFind::Region* r ){
+  //take all nodes from r
+  for( std::map< Node, RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){
+    if( it->second->d_valid ){
+      setRep( it->first, true );
+    }
+  }
+  for( std::map< Node, RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){
+    if( it->second->d_valid ){
+      //take disequalities from r
+      Node n = it->first;
+      RegionNodeInfo* rni = it->second;
+      for( int t=0; t<2; t++ ){
+        RegionNodeInfo::DiseqList* del = rni->d_disequalities[t];
+        for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){
+          if( (*it2).second ){
+            if( t==0 && hasRep( (*it2).first ) ){
+              setDisequal( (*it2).first, n, 0, false );
+              setDisequal( (*it2).first, n, 1, true );
+              setDisequal( n, (*it2).first, 1, true );
+            }else{
+              setDisequal( n, (*it2).first, t, true );
+            }
+          }
+        }
+      }
+    }
+  }
+  r->d_valid = false;
+}
+
+void StrongSolverTheoryUf::ConflictFind::Region::setRep( Node n, bool valid ){
+  Assert( hasRep( n )!=valid );
+  if( d_nodes.find( n )==d_nodes.end() && valid ){
+    d_nodes[n] = new RegionNodeInfo( d_cf->d_th->getSatContext() );
+  }
+  d_nodes[n]->d_valid = valid;
+  d_reps_size = d_reps_size + ( valid ? 1 : -1 );
+  if( d_testClique.find( n )!=d_testClique.end() && d_testClique[n] ){
+    Assert( !valid );
+    d_testClique[n] = false;
+    d_testCliqueSize = d_testCliqueSize - 1;
+    //remove all splits involving n
+    for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++it ){
+      if( (*it).second ){
+        if( (*it).first[0]==n || (*it).first[1]==n ){
+          d_splits[ (*it).first ] = false;
+          d_splitsSize = d_splitsSize - 1;
+        }
+      }
+    }
+  }
+}
+
+/** setEqual */
+void StrongSolverTheoryUf::ConflictFind::Region::setEqual( Node a, Node b ){
+  Assert( hasRep( a ) && hasRep( b ) );
+  //move disequalities of b over to a
+  for( int t=0; t<2; t++ ){
+    RegionNodeInfo::DiseqList* del = d_nodes[b]->d_disequalities[t];
+    for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){
+      if( (*it).second ){
+        Node n = (*it).first;
+        Region* nr = d_cf->d_regions[ d_cf->d_regions_map[ n ] ];
+        if( !isDisequal( a, n, t ) ){
+          setDisequal( a, n, t, true );
+          nr->setDisequal( n, a, t, true );
+        }
+        setDisequal( b, n, t, false );
+        nr->setDisequal( n, b, t, false );
+      }
+    }
+  }
+  //remove b from representatives
+  setRep( b, false );
+}
+
+void StrongSolverTheoryUf::ConflictFind::Region::setDisequal( Node n1, Node n2, int type, bool valid ){
+  //Debug("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " " << type << " " << valid << std::endl;
+  //debugPrint("uf-ss-region-debug");
+  //Assert( isDisequal( n1, n2, type )!=valid );
+  if( isDisequal( n1, n2, type )!=valid ){    //DO_THIS: make assertion
+    d_nodes[ n1 ]->d_disequalities[type]->setDisequal( n2, valid );
+    if( type==0 ){
+      d_total_diseq_external = d_total_diseq_external + ( valid ? 1 : -1 );
+    }else{
+      d_total_diseq_internal = d_total_diseq_internal + ( valid ? 1 : -1 );
+      if( valid ){
+        //if they are both a part of testClique, then remove split
+        if( d_testClique.find( n1 )!=d_testClique.end() && d_testClique[n1] &&
+            d_testClique.find( n2 )!=d_testClique.end() && d_testClique[n2] ){
+          Node eq = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 );
+          if( d_splits.find( eq )!=d_splits.end() && d_splits[ eq ] ){
+            Debug("uf-ss-debug") << "removing split for " << n1 << " " << n2 << std::endl;
+            d_splits[ eq ] = false;
+            d_splitsSize = d_splitsSize - 1;
+          }
+        }
+      }
+    }
+  }
+}
+
+bool StrongSolverTheoryUf::ConflictFind::Region::isDisequal( Node n1, Node n2, int type ){
+  RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->d_disequalities[type];
+  return del->d_disequalities.find( n2 )!=del->d_disequalities.end() && del->d_disequalities[n2];
+}
+
+bool StrongSolverTheoryUf::ConflictFind::Region::getMustCombine( int cardinality ){
+  if( d_total_diseq_external>=long(cardinality) ){
+    //The number of external disequalities is greater than or equal to cardinality.
+    //Thus, a clique of size cardinality+1 may exist between nodes in d_regions[i] and other regions
+    //Check if this is actually the case:  must have n nodes with outgoing degree (cardinality+1-n) for some n>0
+    std::vector< int > degrees;
+    for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+      RegionNodeInfo* rni = it->second;
+      if( rni->d_valid ){
+        if( rni->getNumDisequalities()>=cardinality ){
+          int outDeg = rni->getNumExternalDisequalities();
+          if( outDeg>=cardinality ){
+            //we have 1 node of degree greater than (cardinality)
+            return true;
+          }else if( outDeg>0 ){
+            degrees.push_back( outDeg );
+            if( (int)degrees.size()>=cardinality ){
+              //we have (cardinality) nodes of degree 1
+              return true;
+            }
+          }
+        }
+      }
+    }
+    std::sort( degrees.begin(), degrees.end() );
+    for( int i=0; i<(int)degrees.size(); i++ ){
+      if( degrees[i]>=cardinality+1-((int)degrees.size()-i) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+struct sortInternalDegree {
+  StrongSolverTheoryUf::ConflictFind::Region* r;
+  bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumInternalDisequalities()>r->d_nodes[j]->getNumInternalDisequalities());}
+};
+
+
+bool StrongSolverTheoryUf::ConflictFind::Region::check( Theory::Effort level, int cardinality, std::vector< Node >& clique ){
+  if( d_reps_size>long(cardinality) ){
+    if( d_reps_size>long(cardinality) && d_total_diseq_internal==d_reps_size*( d_reps_size - 1 ) ){
+      //quick clique check, all reps form a clique
+      for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+        if( it->second->d_valid ){
+          clique.push_back( it->first );
+        }
+      }
+      return true;
+    }else{
+      //build test clique, up to size cardinality+1
+      if( d_testCliqueSize<=long(cardinality) ){
+        std::vector< Node > newClique;
+        if( d_testCliqueSize<long(cardinality) ){
+          for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+            //if not in the test clique, add it to the set of new members
+            if( it->second->d_valid && ( d_testClique.find( it->first )==d_testClique.end() || !d_testClique[ it->first ] ) ){
+              newClique.push_back( it->first );
+            }
+          }
+          //choose remaining nodes with the highest degrees
+          sortInternalDegree sidObj;
+          sidObj.r = this;
+          std::sort( newClique.begin(), newClique.end(), sidObj );
+          newClique.erase( newClique.begin() + ( cardinality - d_testCliqueSize ) + 1, newClique.end() );
+        }else{
+          //scan for the highest degree
+          int maxDeg = -1;
+          Node maxNode;
+          for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+            //if not in the test clique, add it to the set of new members
+            if( it->second->d_valid && ( d_testClique.find( it->first )==d_testClique.end() || !d_testClique[ it->first ] ) ){
+              if( it->second->getNumInternalDisequalities()>maxDeg ){
+                maxDeg = it->second->getNumInternalDisequalities();
+                maxNode = it->first;
+              }
+            }
+          }
+          Assert( maxNode!=Node::null() );
+          newClique.push_back( maxNode );
+        }
+        //check splits internal to new members
+        for( int j=0; j<(int)newClique.size(); j++ ){
+          Debug("uf-ss-debug") << "Choose to add clique member " << newClique[j] << std::endl;
+          for( int k=(j+1); k<(int)newClique.size(); k++ ){
+            if( !isDisequal( newClique[j], newClique[k], 1 ) ){
+              d_splits[ NodeManager::currentNM()->mkNode( EQUAL, newClique[j], newClique[k] ) ] = true;
+              d_splitsSize = d_splitsSize + 1;
+            }
+          }
+          //check disequalities with old members
+          for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){
+            if( (*it).second ){
+              if( !isDisequal( (*it).first, newClique[j], 1 ) ){
+                d_splits[ NodeManager::currentNM()->mkNode( EQUAL, (*it).first, newClique[j] ) ] = true;
+                d_splitsSize = d_splitsSize + 1;
+              }
+            }
+          }
+        }
+        //add new clique members to test clique
+        for( int j=0; j<(int)newClique.size(); j++ ){
+          d_testClique[ newClique[j] ] = true;
+          d_testCliqueSize = d_testCliqueSize + 1;
+        }
+      }
+      Assert( d_testCliqueSize==long(cardinality+1) );
+      if( d_splitsSize==0 ){
+        //test clique is a clique
+        for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){
+          if( (*it).second ){
+            clique.push_back( (*it).first );
+          }
+        }
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+Node StrongSolverTheoryUf::ConflictFind::Region::getBestSplit(){
+  //take the first split you find
+  for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++it ){
+    if( (*it).second ){
+      return (*it).first;
+    }
+  }
+  return Node::null();
+}
+
+void StrongSolverTheoryUf::ConflictFind::Region::addSplit( OutputChannel* out ){
+  Node s = getBestSplit();
+  //add lemma to output channel
+  Assert( s!=Node::null() && s.getKind()==EQUAL );
+  s = Rewriter::rewrite( s );
+  Debug("uf-ss-lemma") << "*** Split on " << s << std::endl;
+  //Debug("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
+  //Debug("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
+  //Debug("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
+  debugPrint("uf-ss-temp");
+  //Notice() << "*** Split on " << s << std::endl;
+  //split on the equality s
+  out->split( s );
+  //tell the sat solver to explore the equals branch first
+  out->requirePhase( s, true );
+}
+
+void StrongSolverTheoryUf::ConflictFind::Region::getRepresentatives( std::vector< Node >& reps ){
+  for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+    RegionNodeInfo* rni = it->second;
+    if( rni->d_valid ){
+      reps.push_back( it->first );
+    }
+  }
+}
+
+bool StrongSolverTheoryUf::ConflictFind::Region::minimize( OutputChannel* out ){
+  if( hasSplits() ){
+    addSplit( out );
+    return false;
+  }else{
+    return true;
+  }
+}
+
+void StrongSolverTheoryUf::ConflictFind::Region::getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ){
+  for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+    RegionNodeInfo* rni = it->second;
+    if( rni->d_valid ){
+      RegionNodeInfo::DiseqList* del = rni->d_disequalities[0];
+      for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){
+        if( (*it2).second ){
+          num_ext_disequalities[ (*it2).first ]++;
+        }
+      }
+    }
+  }
+}
+
+void StrongSolverTheoryUf::ConflictFind::Region::debugPrint( const char* c, bool incClique ){
+  Debug( c ) << "Num reps: " << d_reps_size << std::endl;
+  for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+    RegionNodeInfo* rni = it->second;
+    if( rni->d_valid ){
+      Node n = it->first;
+      Debug( c ) << "   " << n << std::endl;
+      for( int i=0; i<2; i++ ){
+        Debug( c ) << "      " << ( i==0 ? "Ext" : "Int" ) << " disequal:";
+        RegionNodeInfo::DiseqList* del = rni->d_disequalities[i];
+        for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){
+          if( (*it2).second ){
+            Debug( c ) << " " << (*it2).first;
+          }
+        }
+        Debug( c ) << ", total = " << del->d_size << std::endl;
+      }
+    }
+  }
+  Debug( c ) << "Total disequal: " << d_total_diseq_external << " external," << std::endl;
+  Debug( c ) << "                " << d_total_diseq_internal<< " internal." << std::endl;
+
+  if( incClique ){
+    Debug( c ) << "Candidate clique members: " << std::endl;
+    Debug( c ) << "   ";
+    for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++ it ){
+      if( (*it).second ){
+        Debug( c ) << (*it).first << " ";
+      }
+    }
+    Debug( c ) << ", size = " << d_testCliqueSize << std::endl;
+    Debug( c ) << "Required splits: " << std::endl;
+    Debug( c ) << "   ";
+    for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++ it ){
+      if( (*it).second ){
+        Debug( c ) << (*it).first << " ";
+      }
+    }
+    Debug( c ) << ", size = " << d_splitsSize << std::endl;
+  }
+}
+
+void StrongSolverTheoryUf::ConflictFind::combineRegions( int ai, int bi ){
+  Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl;
+  Assert( isValid( ai ) && isValid( bi ) );
+  for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[bi]->d_nodes.begin(); it != d_regions[bi]->d_nodes.end(); ++it ){
+    Region::RegionNodeInfo* rni = it->second;
+    if( rni->d_valid ){
+      d_regions_map[ it->first ] = ai;
+    }
+  }
+  //update regions disequal DO_THIS?
+  d_regions[ai]->combine( d_regions[bi] );
+  d_regions[bi]->d_valid = false;
+}
+
+void StrongSolverTheoryUf::ConflictFind::moveNode( Node n, int ri ){
+  Debug("uf-ss-region") << "uf-ss: Move node " << n << " to Region #" << ri << std::endl;
+  Assert( isValid( d_regions_map[ n ] ) );
+  Assert( isValid( ri ) );
+  ////update regions disequal DO_THIS?
+  //Region::RegionNodeInfo::DiseqList* del = d_regions[ d_regions_map[n] ]->d_nodes[n]->d_disequalities[0];
+  //for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){
+  //  if( (*it).second ){
+  //  }
+  //}
+  //move node to region ri
+  d_regions[ri]->takeNode( d_regions[ d_regions_map[n] ], n );
+  d_regions_map[n] = ri;
+}
+
+int StrongSolverTheoryUf::ConflictFind::getNumDisequalitiesToRegion( Node n, int ri ){
+  int ni = d_regions_map[n];
+  int counter = 0;
+  Region::RegionNodeInfo::DiseqList* del = d_regions[ni]->d_nodes[n]->d_disequalities[0];
+  for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){
+    if( (*it).second ){
+      if( d_regions_map[ (*it).first ]==ri ){
+        counter++;
+      }
+    }
+  }
+  return counter;
+}
+
+void StrongSolverTheoryUf::ConflictFind::getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq ){
+  for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[ri]->d_nodes.begin();
+       it != d_regions[ri]->d_nodes.end(); ++it ){
+    if( it->second->d_valid ){
+      Region::RegionNodeInfo::DiseqList* del = it->second->d_disequalities[0];
+      for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){
+        if( (*it2).second ){
+          //if( !isValid( d_regions_map[ (*it2).first ] ) ){
+          //  Debug( "uf-ss-temp" ) << "^^^" << ri << " " << d_regions_map[ (*it2).first ].get() << std::endl;
+          //  debugPrint( "uf-ss-temp" );
+          //}
+          Assert( isValid( d_regions_map[ (*it2).first ] ) );
+          //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
+          regions_diseq[ d_regions_map[ (*it2).first ] ]++;
+        }
+      }
+    }
+  }
+}
+
+void StrongSolverTheoryUf::ConflictFind::explainClique( std::vector< Node >& clique, OutputChannel* out ){
+  Assert( d_cardinality>0 );
+  while( clique.size()>long(d_cardinality+1) ){
+    clique.pop_back();
+  }
+  //found a clique
+  Debug("uf-ss") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
+  Debug("uf-ss") << "   ";
+  for( int i=0; i<(int)clique.size(); i++ ){
+    Debug("uf-ss") << clique[i] << " ";
+  }
+  Debug("uf-ss") << std::endl;
+  Debug("uf-ss") << "Finding clique disequalities..." << std::endl;
+  std::vector< Node > conflict;
+  //collect disequalities, and nodes that must be equal within representatives
+  std::map< Node, std::map< Node, bool > > explained;
+  std::map< Node, std::map< Node, bool > > nodesWithinRep;
+  for( int i=0; i<(int)d_disequalities_index; i++ ){
+    //if both sides of disequality exist in clique
+    Node r1 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] );
+    Node r2 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] );
+    if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) &&
+        std::find( clique.begin(), clique.end(), r1 )!=clique.end() &&
+        std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){
+      explained[r1][r2] = true;
+      explained[r2][r1] = true;
+      conflict.push_back( d_disequalities[i] );
+      nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true;
+      nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true;
+      if( conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) ){
+        break;
+      }
+    }
+  }
+  //Debug("uf-ss") << conflict.size() << " " << clique.size() << std::endl;
+  Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) );
+  //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 );
+  Debug("uf-ss") << "Finding clique equalities internal to eq classes..." << std::endl;
+  //now, we must explain equalities within each equivalence class
+  for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){
+    if( it->second.size()>1 ){
+      Node prev;
+      //add explanation of t1 = t2 = ... = tn
+      for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+        if( prev!=Node::null() ){
+          //explain it2->first and prev
+          std::vector< TNode > expl;
+          d_th->d_equalityEngine.explainEquality( it2->first, prev, true, expl );
+          for( int i=0; i<(int)expl.size(); i++ ){
+            if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){
+              conflict.push_back( expl[i] );
+            }
+          }
+        }
+        prev = it2->first;
+      }
+    }
+  }
+  Debug("uf-ss") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl;
+  for( int i=0; i<(int)conflict.size(); i++ ){
+    Debug("uf-ss") << conflict[i] << " ";
+  }
+  Debug("uf-ss") << std::endl;
+  //now, make the conflict
+  Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict );
+  //add cardinality constraint
+  //Node cardNode = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_lemma_term,
+  //                                                  NodeManager::currentNM()->mkConst( Rational(d_cardinality) ) );
+  Node cardNode = d_cardinality_literal[ d_cardinality ];
+  conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
+  Debug("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
+  //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
+  out->lemma( conflictNode );
+  ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas );
+
+  //DO_THIS: ensure that the same clique is not reported???  Check standard effort after assertDisequal can produce same clique.
+}
+
+/** new node */
+void StrongSolverTheoryUf::ConflictFind::newEqClass( Node n ){
+  if( d_regions_map.find( n )==d_regions_map.end() ){
+    d_regions_map[n] = d_regions_index;
+    Debug("uf-ss") << "StrongSolverTheoryUf: New Eq Class " << n << std::endl;
+    Debug("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size() << std::endl;
+    if( d_regions_index<d_regions.size() ){
+      d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true);
+      d_regions[ d_regions_index ]->d_valid = true;
+      //Assert( d_regions[ d_regions_index ]->d_valid );
+      Assert( d_regions[ d_regions_index ]->getNumReps()==0 );
+    }else{
+      d_regions.push_back( new Region( this, d_th->getSatContext() ) );
+    }
+    d_regions[ d_regions_index ]->setRep( n, true );
+    d_regions_index = d_regions_index + 1;
+    d_reps = d_reps + 1;
+  }
+}
+
+/** merge */
+void StrongSolverTheoryUf::ConflictFind::merge( Node a, Node b ){
+  //Assert( a==d_th->d_equalityEngine.getRepresentative( a ) );
+  //Assert( b==d_th->d_equalityEngine.getRepresentative( b ) );
+  Debug("uf-ss") << "StrongSolverTheoryUf: Merging " << a << " = " << b << "..." << std::endl;
+  if( a!=b ){
+    Assert( d_regions_map.find( a )!=d_regions_map.end() );
+    Assert( d_regions_map.find( b )!=d_regions_map.end() );
+    int ai = d_regions_map[a];
+    int bi = d_regions_map[b];
+    Debug("uf-ss") << "   regions: " << ai << " " << bi << std::endl;
+    if( ai!=bi ){
+      if( d_regions[ai]->getNumReps()==1 ){
+        combineRegions( bi, ai );
+        d_regions[bi]->setEqual( a, b );
+        checkRegion( bi );
+      }else if( d_regions[bi]->getNumReps()==1 ){
+        combineRegions( ai, bi );
+        d_regions[ai]->setEqual( a, b );
+        checkRegion( ai );
+      }else{
+        // either move a to d_regions[bi], or b to d_regions[ai]
+        int aex = d_regions[ai]->d_nodes[a]->getNumInternalDisequalities() - getNumDisequalitiesToRegion( a, bi );
+        int bex = d_regions[bi]->d_nodes[b]->getNumInternalDisequalities() - getNumDisequalitiesToRegion( b, ai );
+        //based on which would produce the fewest number of external disequalities
+        if( aex<bex ){
+          moveNode( a, bi );
+          d_regions[bi]->setEqual( a, b );
+        }else{
+          moveNode( b, ai );
+          d_regions[ai]->setEqual( a, b );
+        }
+        checkRegion( ai );
+        checkRegion( bi );
+      }
+    }else{
+      d_regions[ai]->setEqual( a, b );
+      checkRegion( ai );
+    }
+    d_reps = d_reps - 1;
+    d_regions_map[b] = -1;
+  }
+  Debug("uf-ss") << "Done merge." << std::endl;
+}
+
+/** assert terms are disequal */
+void StrongSolverTheoryUf::ConflictFind::assertDisequal( Node a, Node b, Node reason ){
+  //if they are not already disequal
+  a = d_th->d_equalityEngine.getRepresentative( a );
+  b = d_th->d_equalityEngine.getRepresentative( b );
+  if( !d_th->d_equalityEngine.areDisequal( a, b, true ) ){
+    Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl;
+    //if( reason.getKind()!=NOT || ( reason[0].getKind()!=EQUAL && reason[0].getKind()!=IFF ) ||
+    //    a!=reason[0][0] || b!=reason[0][1] ){
+    //  Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl;
+    //}
+    Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..." << std::endl;
+    //add to list of disequalities
+    if( d_disequalities_index<d_disequalities.size() ){
+      d_disequalities[d_disequalities_index] = reason;
+    }else{
+      d_disequalities.push_back( reason );
+    }
+    d_disequalities_index = d_disequalities_index + 1;
+    //now, add disequalities to regions
+    Assert( d_regions_map.find( a )!=d_regions_map.end() );
+    Assert( d_regions_map.find( b )!=d_regions_map.end() );
+    int ai = d_regions_map[a];
+    int bi = d_regions_map[b];
+    Debug("uf-ss") << "   regions: " << ai << " " << bi << std::endl;
+    if( ai==bi ){
+      //internal disequality
+      d_regions[ai]->setDisequal( a, b, 1, true );
+      d_regions[ai]->setDisequal( b, a, 1, true );
+    }else{
+      //external disequality
+      d_regions[ai]->setDisequal( a, b, 0, true );
+      d_regions[bi]->setDisequal( b, a, 0, true );
+      checkRegion( ai );
+      checkRegion( bi );
+    }
+    //Notice() << "done" << std::endl;
+  }
+}
+
+void StrongSolverTheoryUf::ConflictFind::assertCardinality( int c, bool val ){
+  Assert( d_cardinality_literal.find( c )!=d_cardinality_literal.end() );
+  d_cardinality_assertions[ d_cardinality_literal[c] ] = val;
+  if( val ){
+    d_hasCard = true;
+  }
+}
+
+bool StrongSolverTheoryUf::ConflictFind::checkRegion( int ri, bool rec ){
+  if( isValid(ri) ){
+    Assert( d_cardinality>0 );
+    //first check if region is in conflict
+    std::vector< Node > clique;
+    if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
+      //explain clique
+      explainClique( clique, &d_th->getOutputChannel() );
+      return false;
+    }else if( d_regions[ri]->getMustCombine( d_cardinality ) ){
+      //this region must merge with another
+      Debug("uf-ss-check-region") << "We must combine Region #" << ri << ". " << std::endl;
+      d_regions[ri]->debugPrint("uf-ss-check-region");
+      ////alternatively, check if we can reduce the number of external disequalities by moving single nodes
+      //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){
+      //  if( it->second ){
+      //    int inDeg = d_regions[i]->d_disequalities_size[1][ it-> first ];
+      //    int outDeg = d_regions[i]->d_disequalities_size[1][ it-> first ];
+      //    if( inDeg<outDeg ){
+      //    }
+      //  }
+      //}
+      //take region with maximum disequality density
+      double maxScore = 0;
+      int maxRegion = -1;
+      std::map< int, int > regions_diseq;
+      getDisequalitiesToRegions( ri, regions_diseq );
+      for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){
+        Debug("uf-ss-check-region") << it->first << " : " << it->second << std::endl;
+      }
+      for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){
+        Assert( it->first!=ri );
+        Assert( isValid( it->first ) );
+        Assert( d_regions[ it->first ]->getNumReps()>0 );
+        double tempScore = double(it->second)/double(d_regions[it->first]->getNumReps() );
+        if( tempScore>maxScore ){
+          maxRegion = it->first;
+          maxScore = tempScore;
+        }
+      }
+      Assert( maxRegion!=-1 );
+      Debug("uf-ss-check-region") << "Combine with region #" << maxRegion << ":" << std::endl;
+      d_regions[maxRegion]->debugPrint("uf-ss-check-region");
+      combineRegions( ri, maxRegion );
+      if( rec ){
+        checkRegion( ri, rec );
+      }
+      //std::vector< Node > clique;
+      //if( d_regions[ri]->check( Theory::EFFORT_STANDARD, cardinality, clique ) ){
+      //  //explain clique
+      //  Notice() << "found clique " << std::endl;
+      //}
+      return true;
+    }
+  }
+  return false;
+}
+
+bool StrongSolverTheoryUf::ConflictFind::disambiguateTerms( OutputChannel* out ){
+  Debug("uf-ss-disamb") << "Disambiguate terms." << std::endl;
+  bool lemmaAdded = false;
+  //otherwise, determine ambiguous pairs of ground terms for relevant sorts
+  TermDb* db = d_th->getQuantifiersEngine()->getTermDatabase();
+  for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){
+    Debug("uf-ss-disamb") << "Check " << it->first << std::endl;
+    if( it->second.size()>1 ){
+      if( StrongSolverTheoryUf::involvesRelevantType( it->second[0] ) ){
+        for( int i=0; i<(int)it->second.size(); i++ ){
+          for( int j=(i+1); j<(int)it->second.size(); j++ ){
+            Kind knd = it->second[i].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
+            Node eq = NodeManager::currentNM()->mkNode( knd, it->second[i], it->second[j] );
+            eq = Rewriter::rewrite(eq);
+            //determine if they are ambiguous
+            if( d_term_amb.find( eq )==d_term_amb.end() ){
+              Debug("uf-ss-disamb") << "Check disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
+              d_term_amb[ eq ] = true;
+              //if they are equal
+              if( d_th->d_equalityEngine.areEqual( it->second[i], it->second[j] ) ){
+                d_term_amb[ eq ] = false;
+              }else{
+                //if an argument is disequal, then they are not ambiguous
+                for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
+                  if( d_th->d_equalityEngine.areDisequal( it->second[i][k], it->second[j][k], true ) ){
+                    d_term_amb[ eq ] = false;
+                    break;
+                  }
+                }
+              }
+              if( d_term_amb[ eq ] ){
+                Debug("uf-ss-disamb") << "Disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
+                //must add lemma
+                std::vector< Node > children;
+                children.push_back( eq );
+                for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
+                  Kind knd2 = it->second[i][k].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
+                  Node eqc = NodeManager::currentNM()->mkNode( knd2, it->second[i][k], it->second[j][k] );
+                  children.push_back( eqc.notNode() );
+                }
+                Assert( children.size()>1 );
+                Node lem = NodeManager::currentNM()->mkNode( OR, children );
+                Debug( "uf-ss-lemma" ) << "*** Diambiguate lemma : " << lem << std::endl;
+                //Notice() << "*** Diambiguate lemma : " << lem << std::endl;
+                out->lemma( lem );
+                d_term_amb[ eq ] = false;
+                lemmaAdded = true;
+                ++( d_th->getStrongSolver()->d_statistics.d_disamb_term_lemmas );
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  Debug("uf-ss-disamb") << "Done disambiguate terms. " << lemmaAdded << std::endl;
+  return lemmaAdded;
+}
+
+/** check */
+void StrongSolverTheoryUf::ConflictFind::check( Theory::Effort level, OutputChannel* out ){
+  if( level>=Theory::EFFORT_STANDARD ){
+    Assert( d_cardinality>0 );
+    Debug("uf-ss") << "StrongSolverTheoryUf: Check " << level << " " << d_type << std::endl;
+    //Notice() << "StrongSolverTheoryUf: Check " << level << std::endl;
+    if( d_reps<=(unsigned)d_cardinality ){
+      Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
+      if( level==Theory::EFFORT_FULL ){
+        Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
+        //Notice() << "We have " << d_reps << " representatives for type " << d_type << ", <= " << cardinality << std::endl;
+        //Notice() << "Model size for " << d_type << " is " << cardinality << std::endl;
+        //Notice() << cardinality << " ";
+      }
+      return;
+    }else{
+      //do a check within each region
+      for( int i=0; i<(int)d_regions_index; i++ ){
+        if( d_regions[i]->d_valid ){
+          std::vector< Node > clique;
+          if( d_regions[i]->check( level, d_cardinality, clique ) ){
+            //explain clique
+            explainClique( clique, out );
+            return;
+          }else{
+            Debug("uf-ss-debug") << "No clique in Region #" << i << std::endl;
+          }
+        }
+      }
+      if( level==Theory::EFFORT_FULL ){
+        Debug("uf-ss-debug") << "Add splits?" << std::endl;
+        //see if we have any recommended splits
+        bool addedLemma = false;
+        for( int i=0; i<(int)d_regions_index; i++ ){
+          if( d_regions[i]->d_valid ){
+            if( d_regions[i]->hasSplits() ){
+              d_regions[i]->addSplit( out );
+              addedLemma = true;
+              ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas );
+            }
+          }
+        }
+        if( !addedLemma ){
+          Debug("uf-ss") << "No splits added." << std::endl;
+          if( Options::current()->fmfRegionSat ){
+            //otherwise, try to disambiguate individual terms
+            if( !disambiguateTerms( out ) ){
+              //no disequalities can be propagated
+              //we are in a situation where it suffices to apply a coloring to equivalence classes
+              //due to our invariants, we know no coloring conflicts will occur between regions, and thus
+              //  we are SAT in this case.
+              Debug("uf-ss-sat") << "SAT: regions = " << getNumRegions() << std::endl;
+              //Notice() << "Model size for " << d_type << " is " << cardinality << ", regions = " << getNumRegions() << std::endl;
+              debugPrint("uf-ss-sat");
+            }
+          }else{
+            //naive strategy. combine the first two valid regions
+            int regIndex = -1;
+            for( int i=0; i<(int)d_regions_index; i++ ){
+              if( d_regions[i]->d_valid ){
+                if( regIndex==-1 ){
+                  regIndex = i;
+                }else{
+                  combineRegions( regIndex, i );
+                  check( level, out );
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+void StrongSolverTheoryUf::ConflictFind::propagate( Theory::Effort level, OutputChannel* out ){
+  Assert( d_cardinality>0 );
+
+  //propagate the current cardinality as a decision literal
+  Node cn = d_cardinality_literal[ d_cardinality ];
+  Debug("uf-ss-prop-as-dec") << "Propagate as decision " << d_type << ", cardinality = " << d_cardinality << std::endl;
+  Assert( !cn.isNull() );
+  if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){
+    out->propagateAsDecision( d_cardinality_literal[ d_cardinality ] );
+    Debug("uf-ss-prop-as-dec") << "Propagate as decision " << d_cardinality_literal[ d_cardinality ];
+    Debug("uf-ss-prop-as-dec") << " " << d_cardinality_literal[ d_cardinality ][0].getType() << std::endl;
+  }
+
+}
+
+void StrongSolverTheoryUf::ConflictFind::debugPrint( const char* c ){
+  Debug( c ) << "--  Conflict Find:" << std::endl;
+  Debug( c ) << "Number of reps = " << d_reps << std::endl;
+  Debug( c ) << "Cardinality req = " << d_cardinality << std::endl;
+  unsigned debugReps = 0;
+  for( int i=0; i<(int)d_regions_index; i++ ){
+    if( d_regions[i]->d_valid ){
+      Debug( c ) << "Region #" << i << ": " << std::endl;
+      d_regions[i]->debugPrint( c, true );
+      Debug( c ) << std::endl;
+      for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[i]->d_nodes.begin(); it != d_regions[i]->d_nodes.end(); ++it ){
+        if( it->second->d_valid ){
+          if( d_regions_map[ it->first ]!=i ){
+            Debug( c ) << "***Bad regions map : " << it->first << " " << d_regions_map[ it->first ].get() << std::endl;
+          }
+        }
+      }
+      debugReps += d_regions[i]->getNumReps();
+    }
+  }
+  if( debugReps!=d_reps ){
+    Debug( c ) << "***Bad reps: " << d_reps << ", actual = " << debugReps << std::endl;
+  }
+}
+
+int StrongSolverTheoryUf::ConflictFind::getNumRegions(){
+  int count = 0;
+  for( int i=0; i<(int)d_regions_index; i++ ){
+    if( d_regions[i]->d_valid ){
+      count++;
+    }
+  }
+  return count;
+}
+
+void StrongSolverTheoryUf::ConflictFind::setCardinality( int c, OutputChannel* out ){
+  d_cardinality = c;
+  //add appropriate lemma
+  Node lem = getCardinalityLemma();
+  out->lemma( lem );
+  //add the appropriate lemma
+  Debug("uf-ss-fmf") << "Set cardinality " << d_type << " = " << c << std::endl;
+  Debug("uf-ss-prop-as-dec") << "Propagate as decision " << lem[0] << std::endl;
+  out->propagateAsDecision( lem[0] );
+  d_is_cardinality_requested = true;
+  d_is_cardinality_requested_c = true;
+  //now, require old literal to be decided false
+  //if( d_cardinality_literal.find( c-1 )!=d_cardinality_literal.end() ){
+  //  Debug("uf-ss-req-phase") << "Require phase " << d_cardinality_literal[c-1] << " = false " << std::endl;
+  //  out->requirePhase( d_cardinality_literal[c-1], false );
+  //}
+}
+
+void StrongSolverTheoryUf::ConflictFind::getRepresentatives( std::vector< Node >& reps ){
+  if( !Options::current()->fmfRegionSat ){
+    bool foundRegion = false;
+    for( int i=0; i<(int)d_regions_index; i++ ){
+      //should not have multiple regions at this point
+      if( foundRegion ){
+        Assert( !d_regions[i]->d_valid );
+      }
+      if( d_regions[i]->d_valid ){
+        //this is the only valid region
+        d_regions[i]->getRepresentatives( reps );
+        foundRegion = true;
+      }
+    }
+  }else{
+    Unimplemented("Build representatives for fmf region sat is not implemented");
+  }
+}
+
+bool StrongSolverTheoryUf::ConflictFind::minimize( OutputChannel* out ){
+  int validRegionIndex = -1;
+  for( int i=0; i<(int)d_regions_index; i++ ){
+    if( d_regions[i]->d_valid ){
+      if( validRegionIndex!=-1 ){
+        combineRegions( validRegionIndex, i );
+        if( !d_regions[validRegionIndex]->minimize( out ) ){
+          return false;
+        }
+      }else{
+        validRegionIndex = i;
+      }
+    }
+  }
+  if( !d_regions[validRegionIndex]->minimize( out ) ){
+    return false;
+  }
+  return true;
+}
+
+
+Node StrongSolverTheoryUf::ConflictFind::getCardinalityLemma(){
+  if( d_cardinality_lemma.find( d_cardinality )==d_cardinality_lemma.end() ){
+    if( d_cardinality_lemma_term.isNull() ){
+      std::stringstream ss;
+      ss << "fmf_term_" << d_type;
+      d_cardinality_lemma_term = NodeManager::currentNM()->mkVar( ss.str(), d_type );
+      ModelBasisAttribute mba;
+      d_cardinality_lemma_term.setAttribute(mba,true);
+    }
+    Node lem = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_lemma_term,
+                                  NodeManager::currentNM()->mkConst( Rational( d_cardinality ) ) );
+    lem = Rewriter::rewrite(lem);
+    d_cardinality_literal[ d_cardinality ] = lem;
+    lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
+    d_cardinality_lemma[ d_cardinality ] = lem;
+  }
+  return d_cardinality_lemma[ d_cardinality ];
+}
+
+StrongSolverTheoryUf::StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
+d_out( &out ),
+d_th( th ),
+d_conf_find_init( c )
+{
+
+}
+
+/** new node */
+void StrongSolverTheoryUf::newEqClass( Node n ){
+  TypeNode tn = n.getType();
+  ConflictFind* c = getConflictFind( tn );
+  if( c ){
+    Debug("uf-ss-solver") << "StrongSolverTheoryUf: New eq class " << n << " " << tn << std::endl;
+    c->newEqClass( n );
+  }
+  //else if( isRelevantType( tn ) ){
+  //  //Debug("uf-ss-solver") << "WAIT: StrongSolverTheoryUf: New eq class " << n << " " << tn << std::endl;
+  //  //d_new_eq_class_waiting[tn].push_back( n );
+  //}
+}
+
+/** merge */
+void StrongSolverTheoryUf::merge( Node a, Node b ){
+  TypeNode tn = a.getType();
+  ConflictFind* c = getConflictFind( tn );
+  if( c ){
+    Debug("uf-ss-solver") << "StrongSolverTheoryUf: Merge " << a << " " << b << " " << tn << std::endl;
+    c->merge( a, b );
+  }
+  //else if( isRelevantType( tn ) ){
+  //}
+}
+
+/** assert terms are disequal */
+void StrongSolverTheoryUf::assertDisequal( Node a, Node b, Node reason ){
+  TypeNode tn = a.getType();
+  ConflictFind* c = getConflictFind( tn );
+  if( c ){
+    Debug("uf-ss-solver") << "StrongSolverTheoryUf: Assert disequal " << a << " " << b << " " << tn << std::endl;
+    //Assert( d_th->d_equalityEngine.getRepresentative( a )==a );
+    //Assert( d_th->d_equalityEngine.getRepresentative( b )==b );
+    c->assertDisequal( a, b, reason );
+  }
+  //else if( isRelevantType( tn ) ){
+  //}
+}
+
+/** assert a node */
+void StrongSolverTheoryUf::assertNode( Node n, bool isDecision ){
+  Debug("uf-ss-assert") << "Assert " << n << " " << isDecision << std::endl;
+  if( n.getKind()==CARDINALITY_CONSTRAINT ){
+    TypeNode tn = n[0].getType();
+    Assert( d_conf_find[tn]->getCardinality()>0 );
+    Assert( isRelevantType( tn ) );
+    Assert( d_conf_find[tn] );
+    long nCard = n[1].getConst<Rational>().getNumerator().getLong();
+    d_conf_find[tn]->assertCardinality( nCard, true );
+    if( nCard==d_conf_find[tn]->getCardinality() ){
+      d_conf_find[tn]->d_is_cardinality_set = true;
+      d_conf_find[tn]->d_is_cardinality_requested = false;
+      d_conf_find[tn]->d_is_cardinality_requested_c = false;
+    }
+  }else if( n.getKind()==NOT && n[0].getKind()==CARDINALITY_CONSTRAINT ){
+    //must add new lemma
+    Node nn = n[0];
+    TypeNode tn = nn[0].getType();
+    Assert( isRelevantType( tn ) );
+    Assert( d_conf_find[tn] );
+    long nCard = nn[1].getConst<Rational>().getNumerator().getLong();
+    d_conf_find[tn]->assertCardinality( nCard, false );
+    if( nCard==d_conf_find[tn]->getCardinality() ){
+      AlwaysAssert(!isDecision, "Error: Negative cardinality node decided upon");
+      Debug("uf-ss-fmf") << "No model of size " << d_conf_find[tn]->getCardinality() << " exists for type " << tn << std::endl;
+      //Notice() << "No model of size " << d_conf_find[tn]->getCardinality() << " exists for type " << tn << std::endl;
+      //increment to next cardinality
+      d_statistics.d_max_model_size.maxAssign( d_conf_find[tn]->getCardinality() + 1 );
+      d_conf_find[tn]->setCardinality( d_conf_find[tn]->getCardinality() + 1, d_out );
+      //Notice() << d_conf_find[tn]->getCardinality() << " ";
+      ////give up permanently on this cardinality
+      //d_out->lemma( n );
+    }
+  }else{
+    ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but
+    ////       a theory propagation is not a decision.
+    //if( isDecision ){
+    //  for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){
+    //    if( !it->second->hasCardinalityAsserted() ){
+    //      Notice() << "Assert " << n << " " << isDecision << std::endl;
+    //      Notice() << "Error: constraint asserted before cardinality for " << it->first << std::endl;
+    //      Unimplemented();
+    //    }
+    //  }
+    //}
+  }
+}
+
+
+/** check */
+void StrongSolverTheoryUf::check( Theory::Effort level ){
+  Debug("uf-ss-solver") << "StrongSolverTheoryUf: check " << level << std::endl;
+  if( level==Theory::EFFORT_FULL ){
+    debugPrint( "uf-ss-debug" );
+  }
+  for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){
+    it->second->check( level, d_out );
+  }
+  Debug("uf-ss-solver") << "Done StrongSolverTheoryUf: check " << level << std::endl;
+}
+
+/** propagate */
+void StrongSolverTheoryUf::propagate( Theory::Effort level ){
+  for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){
+    it->second->propagate( level, d_out );
+  }
+}
+
+void StrongSolverTheoryUf::preRegisterTerm( TNode n ){
+  //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)  FIXME
+  TypeNode tn = n.getType();
+  if( isRelevantType( tn ) ){
+    preRegisterType( tn );
+  }
+}
+
+void StrongSolverTheoryUf::registerQuantifier( Node f ){
+  Debug("uf-ss-register") << "Register quantifier " << f << std::endl;
+  //must ensure the quantifier does not quantify over arithmetic
+  for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
+    TypeNode tn = f[0][i].getType();
+    if( isRelevantType( tn ) ){
+      preRegisterType( tn );
+    }else{
+      if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
+        Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier";
+        Debug("uf-ss-na") << " (" << f << ")";
+        Debug("uf-ss-na") << std::endl;
+        Unimplemented("Cannot perform finite model finding on arithmetic quantifier");
+      }else if( tn.isDatatype() ){
+        Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier";
+        Debug("uf-ss-na") << " (" << f << ")";
+        Debug("uf-ss-na") << std::endl;
+        Unimplemented("Cannot perform finite model finding on datatype quantifier");
+      }
+    }
+  }
+}
+
+void StrongSolverTheoryUf::preRegisterType( TypeNode tn ){
+  if( d_conf_find.find( tn )==d_conf_find.end() ){
+    Debug("uf-ss-register") << "Preregister " << tn << "." << std::endl;
+    //enter into incremental finite model finding mode: try cardinality = 1 first
+    //if( !d_conf_types.empty() ){
+    //  Debug("uf-ss-na") << "Strong solver unimplemented for multiple sorts." << std::endl;
+    //  Unimplemented();
+    //}
+    d_conf_find[tn] = new ConflictFind( tn, d_th->getSatContext(), d_th );
+    //assign cardinality restriction
+    d_statistics.d_max_model_size.maxAssign( 1 );
+    d_conf_find[tn]->setCardinality( 1, d_out );
+    ////add waiting equivalence classes now
+    //if( !d_new_eq_class_waiting[tn].empty() ){
+    //  Debug("uf-ss-register") << "Add " << (int)d_new_eq_class_waiting[tn].size() << " new eq classes." << std::endl;
+    //  for( int i=0; i<(int)d_new_eq_class_waiting[tn].size(); i++ ){
+    //    newEqClass( d_new_eq_class_waiting[tn][i] );
+    //  }
+    //  d_new_eq_class_waiting[tn].clear();
+    //}
+    d_conf_types.push_back( tn );
+  }
+}
+
+StrongSolverTheoryUf::ConflictFind* StrongSolverTheoryUf::getConflictFind( TypeNode tn ){
+  std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.find( tn );
+  //pre-register the type if not done already
+  if( it==d_conf_find.end() ){
+    if( isRelevantType( tn ) ){
+      preRegisterType( tn );
+      it = d_conf_find.find( tn );
+    }
+  }
+  if( it!=d_conf_find.end() ){
+    //initialize the type if necessary
+    if( d_conf_find_init.find( tn )==d_conf_find_init.end() ){
+      //assign cardinality restriction
+      d_statistics.d_max_model_size.maxAssign( 1 );
+      it->second->setCardinality( 1, d_out );
+      d_conf_find_init[tn] = true;
+    }
+    return it->second;
+  }else{
+    return NULL;
+  }
+}
+
+void StrongSolverTheoryUf::notifyRestart(){
+  Debug("uf-ss-prop-as-dec") << "Restart?" << std::endl;
+}
+
+/** get cardinality for sort */
+int StrongSolverTheoryUf::getCardinality( TypeNode t ) {
+  ConflictFind* c = getConflictFind( t );
+  if( c ){
+    return c->getCardinality();
+  }else{
+    return -1;
+  }
+}
+
+void StrongSolverTheoryUf::getRepresentatives( TypeNode t, std::vector< Node >& reps ){
+  ConflictFind* c = getConflictFind( t );
+  if( c ){
+    c->getRepresentatives( reps );
+  }
+}
+
+Node StrongSolverTheoryUf::getCardinalityTerm( TypeNode t ){
+  ConflictFind* c = getConflictFind( t );
+  if( c ){
+    return c->getCardinalityTerm();
+  }else{
+    return Node::null();
+  }
+}
+
+bool StrongSolverTheoryUf::minimize(){
+  for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){
+    if( !it->second->minimize( d_out ) ){
+      return false;
+    }
+  }
+  return true;
+}
+
+//print debug
+void StrongSolverTheoryUf::debugPrint( const char* c ){
+  //EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine );
+  //while( !eqc_iter.isFinished() ){
+  //  Debug( c ) << "Eq class [[" << (*eqc_iter) << "]]" << std::endl;
+  //  EqClassIterator< TheoryUF::NotifyClass > eqc_iter2( *eqc_iter, &((TheoryUF*)d_th)->d_equalityEngine );
+  //  Debug( c ) << "   ";
+  //  while( !eqc_iter2.isFinished() ){
+  //    Debug( c ) << "[" << (*eqc_iter2) << "] ";
+  //    eqc_iter2++;
+  //  }
+  //  Debug( c ) << std::endl;
+  //  eqc_iter++;
+  //}
+
+  for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){
+    Debug( c ) << "Conflict find structure for " << it->first << ": " << std::endl;
+    it->second->debugPrint( c );
+    Debug( c ) << std::endl;
+  }
+}
+
+StrongSolverTheoryUf::Statistics::Statistics():
+  d_clique_lemmas("StrongSolverTheoryUf::Clique_Lemmas", 0),
+  d_split_lemmas("StrongSolverTheoryUf::Split_Lemmas", 0),
+  d_disamb_term_lemmas("StrongSolverTheoryUf::Disambiguate_Term_Lemmas", 0),
+  d_max_model_size("StrongSolverTheoryUf::Max_Model_Size", 0)
+{
+  StatisticsRegistry::registerStat(&d_clique_lemmas);
+  StatisticsRegistry::registerStat(&d_split_lemmas);
+  StatisticsRegistry::registerStat(&d_disamb_term_lemmas);
+  StatisticsRegistry::registerStat(&d_max_model_size);
+}
+
+StrongSolverTheoryUf::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_clique_lemmas);
+  StatisticsRegistry::unregisterStat(&d_split_lemmas);
+  StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas);
+  StatisticsRegistry::unregisterStat(&d_max_model_size);
+}
+
+bool StrongSolverTheoryUf::isRelevantType( TypeNode t ){
+  return t!=NodeManager::currentNM()->booleanType() &&
+         t!=NodeManager::currentNM()->integerType() &&
+         t!=NodeManager::currentNM()->realType() &&
+         t!=NodeManager::currentNM()->builtinOperatorType() &&
+         !t.isFunction() &&
+         !t.isDatatype();
+}
+
+bool StrongSolverTheoryUf::involvesRelevantType( Node n ){
+  if( n.getKind()==APPLY_UF ){
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      if( isRelevantType( n[i].getType() ) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
new file mode 100644
index 000000000..e36441f6d
--- /dev/null
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -0,0 +1,322 @@
+/*********************                                                        */
+/*! \file theory_uf_strong_solver.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Theory uf strong solver
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_UF_STRONG_SOLVER_H
+#define __CVC4__THEORY_UF_STRONG_SOLVER_H
+
+#include "theory/theory.h"
+
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdchunk_list.h"
+
+#include "util/stats.h"
+
+namespace CVC4 {
+namespace theory {
+
+struct ModelBasisAttributeId {};
+typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
+
+namespace uf {
+
+class TheoryUF;
+
+class StrongSolverTheoryUf{
+protected:
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDList<bool> BoolList;
+  typedef context::CDHashMap<TypeNode, bool, TypeNodeHashFunction> TypeNodeBoolMap;
+public:
+  /** information for incremental conflict/clique finding for a particular sort */
+  class ConflictFind {
+  public:
+    /** a partition of the current equality graph for which cliques can occur internally */
+    class Region {
+    public:
+      /** conflict find pointer */
+      ConflictFind* d_cf;
+      /** information stored about each node in region */
+      class RegionNodeInfo {
+      public:
+        /** disequality list for node */
+        class DiseqList {
+        public:
+          DiseqList( context::Context* c ) : d_size( c, 0 ), d_disequalities( c ){}
+          ~DiseqList(){}
+          context::CDO< unsigned > d_size;
+          NodeBoolMap d_disequalities;
+          void setDisequal( Node n, bool valid ){
+            Assert( d_disequalities.find( n )==d_disequalities.end() || d_disequalities[n]!=valid );
+            d_disequalities[ n ] = valid;
+            d_size = d_size + ( valid ? 1 : -1 );
+          }
+        };
+      private:
+        DiseqList d_internal;
+        DiseqList d_external;
+      public:
+        /** constructor */
+        RegionNodeInfo( context::Context* c ) : d_internal( c ), d_external( c ), d_valid( c, true ){
+          d_disequalities[0] = &d_internal;
+          d_disequalities[1] = &d_external;
+        }
+        ~RegionNodeInfo(){}
+        context::CDO< bool > d_valid;
+        DiseqList* d_disequalities[2];
+
+        int getNumDisequalities() { return d_disequalities[0]->d_size + d_disequalities[1]->d_size; }
+        int getNumExternalDisequalities() { return d_disequalities[0]->d_size; }
+        int getNumInternalDisequalities() { return d_disequalities[1]->d_size; }
+      };
+      ///** end class RegionNodeInfo */
+    private:
+      //a postulated clique
+      NodeBoolMap d_testClique;
+      context::CDO< unsigned > d_testCliqueSize;
+      //disequalities needed for this clique to happen
+      NodeBoolMap d_splits;
+      context::CDO< unsigned > d_splitsSize;
+      /** get split */
+      Node getBestSplit();
+    private:
+      //number of valid representatives in this region
+      context::CDO< unsigned > d_reps_size;
+      //total disequality size (external)
+      context::CDO< unsigned > d_total_diseq_external;
+      //total disequality size (internal)
+      context::CDO< unsigned > d_total_diseq_internal;
+    public:
+      //constructor
+      Region( ConflictFind* cf, context::Context* c ) : d_cf( cf ), d_testClique( c ), d_testCliqueSize( c, 0 ),
+        d_splits( c ), d_splitsSize( c, 0 ), d_reps_size( c, 0 ), d_total_diseq_external( c, 0 ),
+        d_total_diseq_internal( c, 0 ), d_valid( c, true ) {
+      }
+      ~Region(){}
+      //region node infomation
+      std::map< Node, RegionNodeInfo* > d_nodes;
+      //whether region is valid
+      context::CDO< bool > d_valid;
+    public:
+      //get num reps
+      int getNumReps() { return d_reps_size; }
+      // has representative
+      bool hasRep( Node n ) { return d_nodes.find( n )!=d_nodes.end() && d_nodes[n]->d_valid; }
+      //take node from region
+      void takeNode( Region* r, Node n );
+      //merge with other region
+      void combine( Region* r );
+      /** set rep */
+      void setRep( Node n, bool valid );
+      /** merge */
+      void setEqual( Node a, Node b );
+      //set n1 != n2 to value 'valid', type is whether it is internal/external
+      void setDisequal( Node n1, Node n2, int type, bool valid );
+      // is disequal
+      bool isDisequal( Node n1, Node n2, int type );
+    public:
+      /** get must merge */
+      bool getMustCombine( int cardinality );
+      /** check for cliques */
+      bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique );
+      /** has splits */
+      bool hasSplits() { return d_splitsSize>0; }
+      /** add split */
+      void addSplit( OutputChannel* out );
+      /** get representatives */
+      void getRepresentatives( std::vector< Node >& reps );
+      /** minimize */
+      bool minimize( OutputChannel* out );
+      /** get external disequalities */
+      void getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities );
+      //print debug
+      void debugPrint( const char* c, bool incClique = false );
+    };
+  private:
+    /** theory uf pointer */
+    TheoryUF* d_th;
+    /** regions used to d_region_index */
+    context::CDO< unsigned > d_regions_index;
+    /** vector of regions */
+    std::vector< Region* > d_regions;
+    /** map from Nodes to index of d_regions they exist in, -1 means invalid */
+    NodeIntMap d_regions_map;
+    /** regions used to d_region_index */
+    context::CDO< unsigned > d_disequalities_index;
+    /** list of all disequalities */
+    std::vector< Node > d_disequalities;
+    /** number of representatives in all regions */
+    context::CDO< unsigned > d_reps;
+    /** whether two terms are ambiguous (indexed by equalities) */
+    NodeBoolMap d_term_amb;
+  private:
+    /** merge regions */
+    void combineRegions( int ai, int bi );
+    /** move node n to region ri */
+    void moveNode( Node n, int ri );
+    /** get number of disequalities from node n to region ri */
+    int getNumDisequalitiesToRegion( Node n, int ri );
+    /** get number of disequalities from Region r to other regions */
+    void getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq );
+    /** check if we need to combine region ri */
+    bool checkRegion( int ri, bool rec = true );
+    /** explain clique */
+    void explainClique( std::vector< Node >& clique, OutputChannel* out );
+    /** is valid */
+    bool isValid( int ri ) { return ri>=0 && ri<(int)d_regions_index && d_regions[ ri ]->d_valid; }
+    /** check ambiguous terms */
+    bool disambiguateTerms( OutputChannel* out );
+  private:
+    /** cardinality operating with */
+    context::CDO< int > d_cardinality;
+    /** type */
+    TypeNode d_type;
+    /** cardinality lemma term */
+    Node d_cardinality_lemma_term;
+    /** cardinality literals */
+    std::map< int, Node > d_cardinality_literal;
+    /** cardinality lemmas */
+    std::map< int, Node > d_cardinality_lemma;
+    /** cardinality assertions (indexed by cardinality literals ) */
+    NodeBoolMap d_cardinality_assertions;
+  public:
+    ConflictFind( TypeNode tn, context::Context* c, TheoryUF* th ) :
+        d_th( th ), d_regions_index( c, 0 ), d_regions_map( c ), d_disequalities_index( c, 0 ),
+        d_reps( c, 0 ), d_term_amb( c ), d_cardinality( c, 1 ), d_type( tn ),
+        d_cardinality_assertions( c ), d_is_cardinality_set( c, false ),
+        d_is_cardinality_requested_c( c, false ), d_is_cardinality_requested( false ), d_hasCard( c, false ){}
+    ~ConflictFind(){}
+    /** new node */
+    void newEqClass( Node n );
+    /** merge */
+    void merge( Node a, Node b );
+    /** assert terms are disequal */
+    void assertDisequal( Node a, Node b, Node reason );
+    /** assert cardinality */
+    void assertCardinality( int c, bool val );
+    /** whether cardinality has been asserted */
+    bool hasCardinalityAsserted() { return d_hasCard; }
+    /** check */
+    void check( Theory::Effort level, OutputChannel* out );
+    /** propagate */
+    void propagate( Theory::Effort level, OutputChannel* out );
+    //print debug
+    void debugPrint( const char* c );
+    /** set cardinality */
+    void setCardinality( int c, OutputChannel* out );
+    /** get cardinality */
+    int getCardinality() { return d_cardinality; }
+    /** get representatives */
+    void getRepresentatives( std::vector< Node >& reps );
+    /** get model basis term */
+    Node getCardinalityTerm() { return d_cardinality_lemma_term; }
+    /** minimize */
+    bool minimize( OutputChannel* out );
+    /** get cardinality lemma */
+    Node getCardinalityLemma();
+  public:
+    /** get number of regions (for debugging) */
+    int getNumRegions();
+    /** is cardinality set */
+    context::CDO< bool > d_is_cardinality_set;
+    context::CDO< bool > d_is_cardinality_requested_c;
+    bool d_is_cardinality_requested;
+    /** whether a positive cardinality constraint has been asserted */
+    context::CDO< bool > d_hasCard;
+  }; /** class ConflictFind */
+private:
+  /** The output channel for the strong solver. */
+  OutputChannel* d_out;
+  /** theory uf pointer */
+  TheoryUF* d_th;
+  /** conflict find structure, one for each type */
+  std::map< TypeNode, ConflictFind* > d_conf_find;
+  /** all types */
+  std::vector< TypeNode > d_conf_types;
+  /** whether conflict find data structures have been initialized */
+  TypeNodeBoolMap d_conf_find_init;
+  /** pre register type */
+  void preRegisterType( TypeNode tn );
+  /** get conflict find */
+  ConflictFind* getConflictFind( TypeNode tn );
+public:
+  StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th);
+  ~StrongSolverTheoryUf() {}
+  /** new node */
+  void newEqClass( Node n );
+  /** merge */
+  void merge( Node a, Node b );
+  /** assert terms are disequal */
+  void assertDisequal( Node a, Node b, Node reason );
+  /** assert node */
+  void assertNode( Node n, bool isDecision );
+public:
+  /** check */
+  void check( Theory::Effort level );
+  /** propagate */
+  void propagate( Theory::Effort level );
+  /** preregister a term */
+  void preRegisterTerm( TNode n );
+  /** preregister a quantifier */
+  void registerQuantifier( Node f );
+  /** notify restart */
+  void notifyRestart();
+public:
+  /** identify */
+  std::string identify() const { return std::string("StrongSolverTheoryUf"); }
+  //print debug
+  void debugPrint( const char* c );
+public:
+  /** get number of types */
+  int getNumCardinalityTypes() { return (int)d_conf_types.size(); }
+  /** get type */
+  TypeNode getCardinalityType( int i ) { return d_conf_types[i]; }
+  /** get cardinality for sort */
+  int getCardinality( TypeNode t );
+  /** get representatives */
+  void getRepresentatives( TypeNode t, std::vector< Node >& reps );
+  /** get cardinality term */
+  Node getCardinalityTerm( TypeNode t );
+  /** minimize */
+  bool minimize();
+
+  class Statistics {
+  public:
+    IntStat d_clique_lemmas;
+    IntStat d_split_lemmas;
+    IntStat d_disamb_term_lemmas;
+    IntStat d_max_model_size;
+    Statistics();
+    ~Statistics();
+  };
+  /** statistics class */
+  Statistics d_statistics;
+
+  /** is relavant type */
+  static bool isRelevantType( TypeNode t );
+  /** involves relavant type */
+  static bool involvesRelevantType( Node n );
+};/* class StrongSolverTheoryUf */
+
+}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY_UF_STRONG_SOLVER_H */
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 3d7e51746..b68a11abd 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -59,6 +59,20 @@ public:
   }
 };/* class UfTypeRule */
 
+class CardinalityConstraintTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw(TypeCheckingExceptionPrivate) {
+    if( check ) {
+      TypeNode valType = n[1].getType(check);
+      if( valType != nodeManager->integerType() ) {
+        throw TypeCheckingExceptionPrivate(n, "cardinality constraint must be integer");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* class UfTypeRule */
+
 }/* CVC4::theory::uf namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */