Merge quantifiers2-trunk:

   - new syntax for rewrite rules
   - better rewrite rules theory
   - remove the rewriting with rewrite rules during ppRewrite temporarily
   - theory can define their own candidate generator
   - define a general candidate generator (inefficient ask to every theory)
   - split inst_match between the pattern matching used for quantifiers (inst_match.*) and
     the one used for rewrite rules (rr_inst_match.*):
      - the pattern matching is less exhaustive for quantifiers,
      - the one for rewrite rules can use efficient-e-matching.

8 files changed, 982 insertions, 155 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index fe75b5f59..9376c858d 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -65,6 +65,10 @@ void EqualityEngine::init() {
   d_triggerDatabaseAllocatedSize = 100000;
   d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
 
+  //We can't notify during the initialization because it notifies
+  // QuantifiersEngine.AddTermToDatabase that try to access to the uf
+  // instantiator that currently doesn't exist.
+  ScopedBool sb(d_performNotify, false);
   addTerm(d_true);
   addTerm(d_false);
 
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 9228e29d4..0b461131e 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -794,7 +794,7 @@ class EqClassesIterator {
 
 public:
 
-  EqClassesIterator() { }
+  EqClassesIterator(): d_ee(NULL), d_it(0){ }
   EqClassesIterator(eq::EqualityEngine* ee) : d_ee(ee) {
     d_it = 0;
     if ( d_it < d_ee->d_nodesCount &&
@@ -840,7 +840,7 @@ class EqClassIterator {
 
 public:
 
-  EqClassIterator() { }
+  EqClassIterator(): d_ee(NULL){ }
   EqClassIterator(Node eqc, eq::EqualityEngine* ee) : d_ee(ee) {
     Assert( d_ee->getRepresentative(eqc) == eqc );
     d_rep = eqc;
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
index 669df055a..5696251ed 100644
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/uf/inst_strategy.cpp
@@ -28,6 +28,7 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
+using namespace CVC4::theory::inst;
 
 #define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
 //#define MULTI_TRIGGER_FULL_EFFORT_HALF
@@ -83,7 +84,7 @@ void InstStrategyCheckCESolved::calcSolved( Node f ){
     Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
     Node rep = d_th->getInternalRepresentative( i );
     if( !rep.hasAttribute(InstConstantAttribute()) ){
-      d_th->d_baseMatch[f].d_map[ i ] = rep;
+      d_th->d_baseMatch[f].set(i,rep);
     }else{
       d_solved[ f ] = false;
     }
diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h
index 09b8087f2..a0091c4b4 100644
--- a/src/theory/uf/inst_strategy.h
+++ b/src/theory/uf/inst_strategy.h
@@ -20,6 +20,7 @@
 #define __CVC4__INST_STRATEGY_H
 
 #include "theory/quantifiers_engine.h"
+#include "theory/trigger.h"
 
 #include "context/context.h"
 #include "context/context_mm.h"
@@ -59,7 +60,7 @@ private:
   /** InstantiatorTheoryUf class */
   InstantiatorTheoryUf* d_th;
   /** explicitly provided patterns */
-  std::map< Node, std::vector< Trigger* > > d_user_gen;
+  std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
   /** counter for quantifiers */
   std::map< Node, int > d_counter;
   /** process functions */
@@ -75,7 +76,7 @@ public:
   /** 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 ]; }
+  inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
   /** identify */
   std::string identify() const { return std::string("UserPatterns"); }
 };/* class InstStrategyUserPatterns */
@@ -99,7 +100,7 @@ private:
   /** 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, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;
   std::map< Node, int > d_counter;
   /** single, multi triggers for each quantifier */
   std::map< Node, std::vector< Node > > d_patTerms[2];
@@ -120,7 +121,7 @@ public:
   ~InstStrategyAutoGenTriggers(){}
 public:
   /** get auto-generated trigger */
-  Trigger* getAutoGenTrigger( Node f );
+  inst::Trigger* getAutoGenTrigger( Node f );
   /** identify */
   std::string identify() const { return std::string("AutoGenTriggers"); }
   /** set regenerate frequency, if fr<0, turn off regenerate */
diff --git a/src/theory/uf/theory_uf_candidate_generator.cpp b/src/theory/uf/theory_uf_candidate_generator.cpp
index 5342188f7..80151d1e1 100644
--- a/src/theory/uf/theory_uf_candidate_generator.cpp
+++ b/src/theory/uf/theory_uf_candidate_generator.cpp
@@ -26,6 +26,11 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 
+namespace CVC4{
+namespace theory{
+namespace uf{
+namespace inst{
+
 CandidateGeneratorTheoryUf::CandidateGeneratorTheoryUf( InstantiatorTheoryUf* ith, Node op ) :
   d_op( op ), d_ith( ith ), d_term_iter( -2 ){
   Assert( !d_op.isNull() );
@@ -45,6 +50,7 @@ void CandidateGeneratorTheoryUf::reset( Node eqc ){
       d_retNode = Node::null();
     }else{
       d_retNode = eqc;
+
     }
     d_term_iter = -1;
   }
@@ -169,3 +175,8 @@ Node CandidateGeneratorTheoryUfLitDeq::getNextCandidate(){
   }
   return Node::null();
 }
+
+}
+}
+}
+}
diff --git a/src/theory/uf/theory_uf_candidate_generator.h b/src/theory/uf/theory_uf_candidate_generator.h
index 668d619db..a06f04f99 100644
--- a/src/theory/uf/theory_uf_candidate_generator.h
+++ b/src/theory/uf/theory_uf_candidate_generator.h
@@ -20,11 +20,155 @@
 #define __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H
 
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/uf/theory_uf_instantiator.h"
+#include "theory/rr_inst_match.h"
+
+using namespace CVC4::theory::quantifiers;
 
 namespace CVC4 {
 namespace theory {
+namespace eq {
+
+namespace rrinst{
+typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
+
+//New CandidateGenerator. They have a simpler semantic than the old one
+
+// Just iterate amoung the equivalence classes
+// node::Null() must be given to reset
+class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{
+private:
+  //the equality classes iterator
+  eq::EqClassesIterator d_eq;
+  //equalityengine pointer
+  EqualityEngine* d_ee;
+public:
+  CandidateGeneratorTheoryEeClasses( EqualityEngine * ee): d_ee( ee ){}
+  ~CandidateGeneratorTheoryEeClasses(){}
+  void resetInstantiationRound(){};
+  void reset( TNode eqc ){
+    Assert(eqc.isNull());
+    d_eq = eq::EqClassesIterator( d_ee );
+  }; //* the argument is not used
+  TNode getNextCandidate(){
+    if( !d_eq.isFinished() ) return (*(d_eq++));
+    else return Node::null();
+  };
+};
+
+// Just iterate amoung the equivalence class of the given node
+// node::Null() *can't* be given to reset
+class CandidateGeneratorTheoryEeClass : public CandidateGenerator{
+private:
+  //instantiator pointer
+  EqualityEngine* d_ee;
+  //the equality class iterator
+  eq::EqClassIterator d_eqc;
+  /* For the case where the given term doesn't exists in uf */
+  Node d_retNode;
+public:
+  CandidateGeneratorTheoryEeClass( EqualityEngine* ee): d_ee( ee ){}
+  ~CandidateGeneratorTheoryEeClass(){}
+  void resetInstantiationRound(){};
+  void reset( TNode eqc ){
+    Assert(!eqc.isNull());
+    if( d_ee->hasTerm( eqc ) ){
+      /* eqc is in uf  */
+      eqc = d_ee->getRepresentative( eqc );
+      d_eqc = eq::EqClassIterator( eqc, d_ee );
+      d_retNode = Node::null();
+    }else{
+      /* If eqc if not a term known by uf, it is the only one in its
+         equivalence class. So we will return only it */
+      d_retNode = eqc;
+      d_eqc = eq::EqClassIterator();
+    }
+  }; //* the argument is not used
+  TNode getNextCandidate(){
+    if(d_retNode.isNull()){
+      if( !d_eqc.isFinished() ) return (*(d_eqc++));
+      else return Node::null();
+    }else{
+      /* the case where eqc not in uf */
+      Node ret = d_retNode;
+      d_retNode = Node::null(); /* d_eqc.isFinished() must be true */
+      return ret;
+    }
+  };
+};
+
+
+} /* namespace rrinst */
+} /* namespace eq */
+
 namespace uf {
+namespace rrinst {
+
+typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
+
+class CandidateGeneratorTheoryUfOp : public CandidateGenerator{
+private:
+  Node d_op;
+  //instantiator pointer
+  TermDb* d_tdb;
+  // Since new term can appears we restrict ourself to the one that
+  // exists at resetInstantiationRound
+  size_t d_term_iter_limit;
+  size_t d_term_iter;
+public:
+  CandidateGeneratorTheoryUfOp(Node op, TermDb* tdb): d_op(op), d_tdb( tdb ){}
+  ~CandidateGeneratorTheoryUfOp(){}
+  void resetInstantiationRound(){
+    d_term_iter_limit = d_tdb->d_op_map[d_op].size();
+  };
+  void reset( TNode eqc ){
+    Assert(eqc.isNull());
+    d_term_iter = 0;
+  }; //* the argument is not used
+  TNode getNextCandidate(){
+    if( d_term_iter<d_term_iter_limit ){
+      TNode n = d_tdb->d_op_map[d_op][d_term_iter];
+      ++d_term_iter;
+      return n;
+    } else return Node::null();
+  };
+};
+
+class CandidateGeneratorTheoryUfType : public CandidateGenerator{
+private:
+  TypeNode d_type;
+  //instantiator pointer
+  TermDb* d_tdb;
+  // Since new term can appears we restrict ourself to the one that
+  // exists at resetInstantiationRound
+  size_t d_term_iter_limit;
+  size_t d_term_iter;
+public:
+  CandidateGeneratorTheoryUfType(TypeNode type, TermDb* tdb): d_type(type), d_tdb( tdb ){}
+  ~CandidateGeneratorTheoryUfType(){}
+  void resetInstantiationRound(){
+    d_term_iter_limit = d_tdb->d_type_map[d_type].size();
+  };
+  void reset( TNode eqc ){
+    Assert(eqc.isNull());
+    d_term_iter = 0;
+  }; //* the argument is not used
+  TNode getNextCandidate(){
+    if( d_term_iter<d_term_iter_limit ){
+      TNode n = d_tdb->d_type_map[d_type][d_term_iter];
+      ++d_term_iter;
+      return n;
+    } else return Node::null();
+  };
+};
+
+} /* namespace rrinst */
+
+namespace inst{
+typedef CVC4::theory::inst::CandidateGenerator CandidateGenerator;
+
+//Old CandidateGenerator
 
 class CandidateGeneratorTheoryUfDisequal;
 
@@ -108,7 +252,8 @@ public:
 };
 
 
-}
+}/* CVC4::theory::uf::inst namespace */
+}/* CVC4::theory::uf namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
index e3999c163..257bed0a2 100644
--- a/src/theory/uf/theory_uf_instantiator.cpp
+++ b/src/theory/uf/theory_uf_instantiator.cpp
@@ -17,6 +17,7 @@
 #include "theory/uf/theory_uf_instantiator.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/theory_uf.h"
+#include "theory/uf/theory_uf_candidate_generator.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/quantifiers/term_database.h"
 
@@ -26,6 +27,15 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
+using namespace CVC4::theory::inst;
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+inline std::ostream& operator<<(std::ostream& out, const InstantiatorTheoryUf::Ips& ips) {
+  return out;
+};
 
 EqClassInfo::EqClassInfo( context::Context* c ) : d_funs( c ), d_pfuns( c ), d_disequal( c ){
 
@@ -33,13 +43,15 @@ EqClassInfo::EqClassInfo( context::Context* c ) : d_funs( c ), d_pfuns( c ), d_d
 
 //set member
 void EqClassInfo::setMember( Node n, quantifiers::TermDb* db ){
-  if( n.getKind()==APPLY_UF ){
-    d_funs[n.getOperator()] = true;
+  if( n.hasOperator() ){
+    d_funs.insertAtContextLevelZero(n.getOperator(),true);
   }
   //add parent functions
-  for( std::map< Node, std::map< int, std::vector< Node > > >::iterator it = db->d_parents[n].begin();
+  for( std::hash_map< Node, std::hash_map< int, std::vector< Node >  >, NodeHashFunction >::iterator it = db->d_parents[n].begin();
     it != db->d_parents[n].end(); ++it ){
-    d_pfuns[ it->first ] = true;
+    //TODO Is it true to do it at level 0? That depend when SetMember is called
+    // At worst it is a good overapproximation
+    d_pfuns.insertAtContextLevelZero( it->first, true);
   }
 }
 
@@ -62,6 +74,20 @@ void EqClassInfo::merge( EqClassInfo* eci ){
   }
 }
 
+inline void outputEqClassInfo( const char* c, const EqClassInfo* eci){
+  Debug(c) << " funs:";
+  for( EqClassInfo::BoolMap::iterator it = eci->d_funs.begin(); it != eci->d_funs.end(); it++ ) {
+    Debug(c) << (*it).first << ",";
+  }
+  Debug(c) << std::endl << "pfuns:";
+  for( EqClassInfo::BoolMap::iterator it = eci->d_pfuns.begin(); it != eci->d_pfuns.end(); it++ ) {
+    Debug(c) << (*it).first << ",";
+  }
+  Debug(c) << std::endl;
+}
+
+
+
 InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th) :
 Instantiator( c, qe, th )
 {
@@ -221,21 +247,92 @@ void InstantiatorTheoryUf::newEqClass( TNode n ){
   d_quantEngine->addTermToDatabase( n );
 }
 
+void InstantiatorTheoryUf::newTerms(SetNode& s){
+  static NoMatchAttribute rewrittenNodeAttribute;
+  /* op -> nodes (if the set is empty, the op is not interesting) */
+  std::hash_map< TNode, SetNode, TNodeHashFunction > h;
+  /* types -> nodes (if the set is empty, the type is not interesting) */
+  std::hash_map< TypeNode, SetNode, TypeNodeHashFunction > tyh;
+  for(SetNode::iterator i=s.begin(), end=s.end(); i != end; ++i){
+    if (i->getAttribute(rewrittenNodeAttribute)) continue; /* skip it */
+    if( !d_cand_gens.empty() ){
+      // op
+      TNode op = i->getOperator();
+      std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator
+        is = h.find(op);
+      if(is == h.end()){
+        std::pair<std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator,bool>
+          p = h.insert(make_pair(op,SetNode()));
+        is = p.first;
+        if(d_cand_gens.find(op) != d_cand_gens.end()){
+          is->second.insert(*i);
+        } /* else we have inserted an empty set */
+      }else if(!is->second.empty()){
+        is->second.insert(*i);
+      }
+    }
+    if( !d_cand_gen_types.empty() ){
+      //type
+      TypeNode ty = i->getType();
+      std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator
+        is = tyh.find(ty);
+      if(is == tyh.end()){
+        std::pair<std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator,bool>
+          p = tyh.insert(make_pair(ty,SetNode()));
+        is = p.first;
+        if(d_cand_gen_types.find(ty) != d_cand_gen_types.end()){
+          is->second.insert(*i);
+        } /* else we have inserted an empty set */
+      }else if(!is->second.empty()){
+        is->second.insert(*i);
+      }
+    }
+  }
+  //op
+  for(std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator i=h.begin(), end=h.end();
+      i != end; ++i){
+    //new term, add n to candidate generators
+    if(i->second.empty()) continue;
+    std::map< Node, NodeNewTermDispatcher >::iterator
+      inpc = d_cand_gens.find(i->first);
+    //we know that this op exists
+    Assert(inpc != d_cand_gens.end());
+    inpc->second.send(i->second);
+  }
+  //type
+  for(std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator i=tyh.begin(), end=tyh.end();
+      i != end; ++i){
+    //new term, add n to candidate generators
+    if(i->second.empty()) continue;
+    std::map< TypeNode, NodeNewTermDispatcher >::iterator
+      inpc = d_cand_gen_types.find(i->first);
+    //we know that this op exists
+    Assert(inpc != d_cand_gen_types.end());
+    inpc->second.send(i->second);
+  }
+
+}
+
+
 /** merge */
 void InstantiatorTheoryUf::merge( TNode a, TNode b ){
   if( Options::current()->efficientEMatching ){
+    //merge eqc_ops of b into a
+    EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a );
+    EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( b );
+
     if( a.getKind()!=IFF && a.getKind()!=EQUAL && b.getKind()!=IFF && b.getKind()!=EQUAL ){
       Debug("efficient-e-match") << "Merging " << a << " with " << b << std::endl;
 
       //determine new candidates for instantiation
-      computeCandidatesPcPairs( a, b );
-      computeCandidatesPcPairs( b, a );
-      computeCandidatesPpPairs( a, b );
-      computeCandidatesPpPairs( b, a );
+      computeCandidatesPcPairs( a, eci_a, b, eci_b );
+      computeCandidatesPcPairs( b, eci_b, a, eci_a );
+      computeCandidatesPpPairs( a, eci_a, b, eci_b );
+      computeCandidatesPpPairs( b, eci_b, a, eci_a );
     }
-    //merge eqc_ops of b into a
-    EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a );
-    EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( b );
+    computeCandidatesConstants( a, eci_a, b, eci_b);
+    computeCandidatesConstants( b, eci_b, a, eci_a);
+
     eci_a->merge( eci_b );
   }
 }
@@ -258,97 +355,99 @@ EqClassInfo* InstantiatorTheoryUf::getOrCreateEquivalenceClassInfo( Node n ){
   return d_eqc_ops[n];
 }
 
-void InstantiatorTheoryUf::computeCandidatesPcPairs( Node a, Node b ){
+void InstantiatorTheoryUf::computeCandidatesPcPairs( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){
   Debug("efficient-e-match") << "Compute candidates for pc pairs..." << std::endl;
   Debug("efficient-e-match") << "  Eq class = [";
   outputEqClass( "efficient-e-match", a);
   Debug("efficient-e-match") << "]" << std::endl;
-  EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a );
-  EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( a );
+  outputEqClassInfo("efficient-e-match",eci_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();
+    for( std::map< Node, std::vector< std::pair< NodePcDispatcher*, Ips > > >::iterator itf = d_pc_pairs[g].begin();
          itf != d_pc_pairs[g].end(); ++itf ){
       //f/g is a parent/child pair
       Node f = itf->first;
-      if( eci_b->hasParent( f ) || true ){
+      if( eci_b->hasParent( f ) ){
         //DO_THIS: determine if f in pfuns( b ), only do the follow if so
         Debug("efficient-e-match") << "    Checking parent application " << f << std::endl;
         //scan through the list of inverted path strings/candidate generators
-        for( std::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;
-            }
+        for( std::vector< std::pair< NodePcDispatcher*, Ips > >::iterator cit = itf->second.begin();
+             cit != itf->second.end(); ++cit ){
+#ifdef CVC4_DEBUG
+          Debug("efficient-e-match") << "      Checking pattern " << cit->first->pat << std::endl;
+#endif
+          Debug("efficient-e-match") << "          Check inverted path string for pattern ";
+          outputIps( "efficient-e-match", cit->second );
+          Debug("efficient-e-match") << std::endl;
+
+          //collect all new relevant terms
+          SetNode terms;
+          terms.insert( b );
+          collectTermsIps( cit->second, terms );
+          if( terms.empty() ) continue;
+          Debug("efficient-e-match") << "        -> Added terms (" << terms.size() << "): ";
+          for( SetNode::const_iterator t=terms.begin(), end=terms.end();
+               t!=end; ++t ){
+            Debug("efficient-e-match") << (*t) << " ";
           }
+          Debug("efficient-e-match") << std::endl;
+          //add them as candidates to the candidate generator
+          cit->first->send(terms);
         }
       }
     }
   }
 }
 
-void InstantiatorTheoryUf::computeCandidatesPpPairs( Node a, Node b ){
+void InstantiatorTheoryUf::computeCandidatesPpPairs( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_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();
+  for( std::map< Node, std::map< Node, std::vector< triple< NodePpDispatcher*, Ips, Ips > > > >::iterator it = d_pp_pairs.begin();
        it != d_pp_pairs.end(); ++it ){
     Node f = it->first;
     if( eci_a->hasParent( f ) ){
       Debug("efficient-e-match") << "  Checking parent application " << f << std::endl;
-      for( std::map< Node, std::map< Node, std::vector< IpsPair > > >::iterator it2 = it->second.begin();
+      for( std::map< Node, std::vector< triple<NodePpDispatcher*, Ips, Ips> > >::iterator it2 = it->second.begin();
            it2 != it->second.end(); ++it2 ){
         Node g = it2->first;
         if( eci_b->hasParent( g ) ){
           Debug("efficient-e-match") << "    Checking parent application " << g << std::endl;
           //if f in pfuns( a ) and g is in pfuns( b ), only do the follow if so
-          for( std::map< Node, std::vector< IpsPair > >::iterator cit = it2->second.begin();
+          for( std::vector< triple<NodePpDispatcher*, Ips, Ips> > ::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] );
-                    }
-                  }
-                }
-              }
+#ifdef CVC4_DEBUG
+            Debug("efficient-e-match") << "    Checking pattern " << cit->first->pat1 << " and " << cit->first->pat2 << std::endl;
+#endif
+            Debug("efficient-e-match") << "          Check inverted path string ";
+            outputIps( "efficient-e-match", cit->second );
+            SetNode a_terms;
+            a_terms.insert( a );
+            collectTermsIps( cit->second, a_terms );
+            if( a_terms.empty() ) continue;
+            Debug("efficient-e-match") << "          And check inverted path string ";
+            outputIps( "efficient-e-match", cit->third );
+            SetNode b_terms;
+            b_terms.insert( b );
+            collectTermsIps( cit->third, b_terms );
+            if( b_terms.empty() ) continue;
+            //Start debug
+            Debug("efficient-e-match") << "        -> Possibly Added termsA (" << a_terms.size() << "): ";
+            for( SetNode::const_iterator t=a_terms.begin(), end=a_terms.end();
+                 t!=end; ++t ){
+              Debug("efficient-e-match") << (*t) << " ";
+            }
+            Debug("efficient-e-match") << std::endl;
+            Debug("efficient-e-match") << "        -> Possibly Added termsB (" << b_terms.size() << "): ";
+            for( SetNode::const_iterator t=b_terms.begin(), end=b_terms.end();
+                 t!=end; ++t ){
+              Debug("efficient-e-match") << (*t) << " ";
             }
+            Debug("efficient-e-match") << std::endl;
+            //End debug
+
+            cit->first->send(a_terms,b_terms);
           }
         }
       }
@@ -356,39 +455,87 @@ void InstantiatorTheoryUf::computeCandidatesPpPairs( Node a, Node b ){
   }
 }
 
-void InstantiatorTheoryUf::collectTermsIps( InvertedPathString& ips, std::vector< Node >& terms, int index ){
-  if( index<(int)ips.size() && !terms.empty() ){
+
+void InstantiatorTheoryUf::computeCandidatesConstants( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){
+  Debug("efficient-e-match") << "Compute candidates constants for cc pairs..." << std::endl;
+  Debug("efficient-e-match") << "  Eq class = [";
+  outputEqClass( "efficient-e-match", a);
+  Debug("efficient-e-match") << "]" << std::endl;
+  outputEqClassInfo("efficient-e-match",eci_a);
+  for( std::map< Node, std::map< Node, NodePcDispatcher* > >::iterator
+         it = d_cc_pairs.begin(), end = d_cc_pairs.end();
+       it != end; ++it ) {
+    Debug("efficient-e-match") << "  Checking application " << it->first << std::endl;
+    if( !eci_b->hasFunction(it->first) ) continue;
+    for( std::map< Node, NodePcDispatcher* >::iterator
+           itc = it->second.begin(), end = it->second.end();
+       itc != end; ++itc ) {
+      //The constant
+      Debug("efficient-e-match") << "    Checking constant " << a << std::endl;
+      if(getRepresentative(itc->first) != a) continue;
+      SetNode s;
+      eq::EqClassIterator eqc_iter( b, &((TheoryUF*)d_th)->d_equalityEngine );
+      while( !eqc_iter.isFinished() ){
+        Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
+                                         << std::endl;
+        if( (*eqc_iter).hasOperator() && (*eqc_iter).getOperator() == it->first ) s.insert(*eqc_iter);
+        eqc_iter++;
+      }
+
+      if( s.empty() ) continue;
+      Debug("efficient-e-match") << "        -> Added terms (" << s.size() << "): ";
+      for( SetNode::const_iterator t=s.begin(), end=s.end();
+           t!=end; ++t ){
+        Debug("efficient-e-match") << (*t) << " ";
+      }
+      Debug("efficient-e-match") << std::endl;
+      itc->second->send(s);
+    }
+  }
+}
+
+void InstantiatorTheoryUf::collectTermsIps( Ips& ips, SetNode & terms ){
+  Assert( ips.size() > 0);
+  return collectTermsIps( ips, terms,  ips.size() - 1);
+}
+
+void InstantiatorTheoryUf::collectTermsIps( Ips& ips, SetNode& terms, int index ){
+  if( !terms.empty() ){
     Debug("efficient-e-match-debug") << "> Process " << index << std::endl;
     Node f = ips[index].first;
     int arg = ips[index].second;
 
     //for each term in terms, determine if any term (modulo equality) has parent "f" from position "arg"
-    bool addRep = ( index!=(int)ips.size()-1 );
-    std::vector< Node > newTerms;
-    for( int t=0; t<(int)terms.size(); t++ ){
-      collectParentsTermsIps( terms[t], f, arg, newTerms, addRep );
+    bool addRep = ( index!=0 ); // We want to keep the top symbol for the last
+    SetNode newTerms;
+    for( SetNode::const_iterator t=terms.begin(), end=terms.end();
+         t!=end; ++t ){
+      collectParentsTermsIps( *t, f, arg, newTerms, addRep );
     }
-    terms.clear();
-    terms.insert( terms.begin(), newTerms.begin(), newTerms.end() );
+    terms.swap(newTerms);
 
     Debug("efficient-e-match-debug") << "> Terms are now: ";
-    for( int t=0; t<(int)terms.size(); t++ ){
-      Debug("efficient-e-match-debug") << terms[t] << " ";
+    for( SetNode::const_iterator t=terms.begin(), end=terms.end();
+         t!=end; ++t ){
+      Debug("efficient-e-match-debug") << *t << " ";
     }
     Debug("efficient-e-match-debug") << std::endl;
 
-    collectTermsIps( ips, terms, index+1 );
+    if(index!=0) collectTermsIps( ips, terms, index-1 );
   }
 }
 
-bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, std::vector< Node >& terms, bool addRep, bool modEq ){
+bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, SetNode & terms, bool addRep, bool modEq ){ //modEq default true
   bool addedTerm = false;
-  if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) && modEq ){
+  
+  if( modEq && ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n )){
     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 );
+    eq::EqClassIterator eqc_iter( n, &((TheoryUF*)d_th)->d_equalityEngine );
     while( !eqc_iter.isFinished() ){
+      Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
+                                       << std::endl;
       if( collectParentsTermsIps( (*eqc_iter), f, arg, terms, addRep, false ) ){
         //if only one argument, we know we can stop (since all others added will be congruent)
         if( f.getType().getNumChildren()==2 ){
@@ -401,90 +548,263 @@ bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, std:
   }else{
     quantifiers::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;
-          }
-        }
-      }
+    const std::vector<Node> & parents = db->getParents(n,f,arg);
+    for( size_t i=0; i<parents.size(); ++i ){
+      TNode t = parents[i];
+      if(!CandidateGenerator::isLegalCandidate(t)) continue;
+      if( addRep ) t = getRepresentative( t );
+      terms.insert(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 );
+void InstantiatorTheoryUf::registerPatternElementPairs2( Node pat, Ips& ips, PpIpsMap & pp_ips_map, NodePcDispatcher* npc ){
+  Assert( pat.hasOperator() );
   //add information for possible pp-pair
+  ips.push_back( std::pair< Node, int >( pat.getOperator(), 0 ) ); //0 is just a dumb value
+
   for( int i=0; i<(int)pat.getNumChildren(); i++ ){
     if( pat[i].getKind()==INST_CONSTANT ){
-      ips_map[ pat[i] ].push_back( std::pair< Node, InvertedPathString >( pat.getOperator(), InvertedPathString( ips ) ) );
+      ips.back().second = i;
+      pp_ips_map[ pat[i] ].push_back( make_pair( pat.getOperator(), Ips( 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 );
+      registerPatternElementPairs2( pat[i], ips, pp_ips_map, npc );
       Debug("pattern-element-opt") << "Found pc-pair ( " << pat.getOperator() << ", " << pat[i].getOperator() << " )" << std::endl;
       Debug("pattern-element-opt") << "   Path = ";
-      outputInvertedPathString( "pattern-element-opt", ips );
+      outputIps( "pattern-element-opt", ips );
       Debug("pattern-element-opt") << std::endl;
       //pat.getOperator() and pat[i].getOperator() are a pc-pair
-      d_pc_pairs[ pat[i].getOperator() ][ pat.getOperator() ][opat].push_back( InvertedPathString( ips ) );
+      d_pc_pairs[ pat[i].getOperator() ][ pat.getOperator() ]
+        .push_back( make_pair(npc,Ips(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++ ){
+void InstantiatorTheoryUf::registerPatternElementPairs( Node pat, PpIpsMap & pp_ips_map,
+                                                        NodePcDispatcher* npc,
+                                                        NodePpDispatcher* npp){
+  Ips ips;
+  registerPatternElementPairs2( pat, ips, pp_ips_map, npc );
+  for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
+    // for each variable construct all the pp-pair
+    for( size_t j=0; j<it->second.size(); j++ ){
+      for( size_t k=j+1; k<it->second.size(); k++ ){
         //found a pp-pair
         Debug("pattern-element-opt") << "Found pp-pair ( " << it->second[j].first << ", " << it->second[k].first << " )" << std::endl;
         Debug("pattern-element-opt") << "   Paths = ";
-        outputInvertedPathString( "pattern-element-opt", it->second[j].second );
+        outputIps( "pattern-element-opt", it->second[j].second );
         Debug("pattern-element-opt") << " and ";
-        outputInvertedPathString( "pattern-element-opt", it->second[k].second );
+        outputIps( "pattern-element-opt", it->second[k].second );
         Debug("pattern-element-opt") << std::endl;
-        d_pp_pairs[ it->second[j].first ][ it->second[k].first ][pat].push_back( IpsPair( it->second[j].second, it->second[k].second ) );
+        d_pp_pairs[ it->second[j].first ][ it->second[k].first ]
+          .push_back( make_triple( npp, it->second[j].second, it->second[k].second ));
       }
     }
   }
+};
+
+void findPpSite(Node pat, InstantiatorTheoryUf::Ips& ips, InstantiatorTheoryUf::PpIpsMap & pp_ips_map){
+  Assert( pat.getKind()==APPLY_UF );
+  //add information for possible pp-pair
+
+  ips.push_back( make_pair( pat.getOperator(), 0) );
+  for( size_t i=0; i<pat.getNumChildren(); i++ ){
+    if( pat[i].getKind()==INST_CONSTANT ){
+      ips.back().second = i;
+      pp_ips_map[ pat[i] ].push_back( make_pair( pat.getOperator(), InstantiatorTheoryUf::Ips( ips ) ) );
+    }
+  }
+
+  for( size_t i=0; i<pat.getNumChildren(); i++ ){
+    if( pat[i].getKind()==APPLY_UF ){
+      ips.back().second = i;
+      findPpSite( pat[i], ips, pp_ips_map );
+    }
+  }
+  ips.pop_back();
 }
 
-void 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 );
+void InstantiatorTheoryUf::combineMultiPpIpsMap(PpIpsMap & pp_ips_map, MultiPpIpsMap & multi_pp_ips_map,
+                                                EfficientHandler& eh, size_t index2,const std::vector<Node> & pats){
+  hash_map<size_t,NodePpDispatcher*> npps;
+  for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
+    MultiPpIpsMap::iterator mit = multi_pp_ips_map.find(it->first);
+    if(mit == multi_pp_ips_map.end()) continue;
+    // for each variable construct all the pp-pair
+    // j the last pattern treated
+    for( std::vector< std::pair< Node, Ips > >::iterator j=it->second.begin(), jend = it->second.end() ;
+         j != jend; ++j){
+      // k one of the previous one
+      for( std::vector< triple< size_t, Node, Ips > >::iterator k=mit->second.begin(), kend = mit->second.end() ;
+           k != kend; ++k){
+        //found a pp-pair
+        Debug("pattern-element-opt") << "Found multi-pp-pair ( " << j->first
+                                     << ", " << k->second << " in "<< k->first
+                                     << " )" << std::endl;
+        Debug("pattern-element-opt") << "   Paths = ";
+        outputIps( "pattern-element-opt", j->second );
+        Debug("pattern-element-opt") << " and ";
+        outputIps( "pattern-element-opt", k->third );
+        Debug("pattern-element-opt") << std::endl;
+        NodePpDispatcher* dispatcher;
+        hash_map<size_t,NodePpDispatcher*>::iterator inpp = npps.find(k->first);
+        if( inpp != npps.end() ) dispatcher = inpp->second;
+        else{
+          dispatcher = new NodePpDispatcher();
+#ifdef CVC4_DEBUG
+          dispatcher->pat1 = pats[index2];
+          dispatcher->pat2 = pats[k->first];
+#endif
+          dispatcher->addPpDispatcher(&eh,index2,k->first);
+        };
+        d_pp_pairs[ j->first ][ k->second ].push_back( make_triple( dispatcher, j->second, k->third ));
+      }
+    }
   }
-  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();
-  quantifiers::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] );
+  /** Put pp_ips_map to multi_pp_ips_map */
+  for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){
+    for( std::vector< std::pair< Node, Ips > >::iterator j=it->second.begin(), jend = it->second.end() ;
+         j != jend; ++j){
+      multi_pp_ips_map[it->first].push_back(make_triple(index2, j->first, j->second));
+    }
+  }
+
+}
+
+
+void InstantiatorTheoryUf::registerEfficientHandler( EfficientHandler& handler,
+                                                     const std::vector< Node > & pats ){
+  Assert(pats.size() > 0);
+
+  MultiPpIpsMap multi_pp_ips_map;
+  PpIpsMap pp_ips_map;
+  //In a multi-pattern Pattern that is only a variable are specials,
+  //if the variable appears in another pattern, it can be discarded.
+  //Otherwise new term of this term can be candidate. So we stock them
+  //here before adding them.
+  std::vector< size_t > patVars;
+
+  Debug("pattern-element-opt") << "Register patterns" << pats << std::endl;
+  for(size_t i = 0; i < pats.size(); ++i){
+    if( pats[i].getKind() == kind::INST_CONSTANT){
+      patVars.push_back(i);
+      continue;
+    }
+    //to complete
+    if( pats[i].getKind() == kind::NOT && pats[i][0].getKind() == kind::EQUAL){
+      Node cst = NodeManager::currentNM()->mkConst<bool>(false);
+      TNode op = pats[i][0].getOperator();
+      if(d_cc_pairs[op][cst] == NULL){
+        d_cc_pairs[op][cst] = new NodePcDispatcher();
+      }
+      d_cc_pairs[op][cst]->addPcDispatcher(&handler,i);
+      continue;
+    }
+    //end to complete
+    Debug("pattern-element-opt") << " Register candidate generator..." << pats[i] << std::endl;
+    /* Has the pattern already been seen */
+    if( d_pat_cand_gens.find( pats[i] )==d_pat_cand_gens.end() ){
+      NodePcDispatcher* npc = new NodePcDispatcher();
+      NodePpDispatcher* npp = new NodePpDispatcher();
+#ifdef CVC4_DEBUG
+      npc->pat = pats[i];
+      npp->pat1 = pats[i];
+      npp->pat2 = pats[i];
+#endif
+      d_pat_cand_gens[pats[i]] = make_pair(npc,npp);
+      registerPatternElementPairs( pats[i], pp_ips_map, npc, npp );
+    }else{
+      Ips ips;
+      findPpSite(pats[i],ips,pp_ips_map);
+    }
+    //Has the top operator already been seen */
+    TNode op = pats[i].getOperator();
+    d_pat_cand_gens[pats[i]].first->addPcDispatcher(&handler,i);
+    d_pat_cand_gens[pats[i]].second->addPpDispatcher(&handler,i,i);
+    d_cand_gens[op].addNewTermDispatcher(&handler,i);
+    
+    combineMultiPpIpsMap(pp_ips_map,multi_pp_ips_map,handler,i,pats);
+
+    pp_ips_map.clear();
+  }
+
+  for(size_t i = 0; i < patVars.size(); ++i){
+    TNode var = pats[patVars[i]];
+    Assert( var.getKind() == kind::INST_CONSTANT );
+    if( multi_pp_ips_map.find(var) != multi_pp_ips_map.end() ){
+      //The variable appear in another pattern, skip it
+      continue;
+    };
+    d_cand_gen_types[var.getType()].addNewTermDispatcher(&handler,patVars[i]);
   }
-  d_cand_gens[op].push_back( cg );
 
+  //take all terms from the uf term db and add to candidate generator
+  if( pats[0].getKind() == kind::INST_CONSTANT ){
+    TypeNode ty = pats[0].getType();
+    rrinst::CandidateGenerator* cg = d_quantEngine->getRRCanGenClasses(ty);
+    cg->reset(Node::null());
+    TNode c;
+    SetNode ele;
+    while( !(c = cg->getNextCandidate()).isNull() ){
+      if( c.getType() == ty ) ele.insert(c);
+    }
+    if( !ele.empty() ){
+      // for(std::vector<Node>::iterator i = db->d_op_map[op].begin(), end = db->d_op_map[op].end(); i != end; ++i){
+      //   if(CandidateGenerator::isLegalCandidate(*i)) ele.insert(*i);
+      // }
+      if(Debug.isOn("efficient-e-match-stats")){
+        Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
+      }
+      handler.addMonoCandidate(ele, 0);
+    }
+
+  } else if( pats[0].getKind() == kind::NOT && pats[0][0].getKind() == kind::EQUAL){
+    Node cst = NodeManager::currentNM()->mkConst<bool>(false);
+    TNode op = pats[0][0].getOperator();
+    cst = getRepresentative(cst);
+    SetNode ele;
+    eq::EqClassIterator eqc_iter( cst, &((TheoryUF*)d_th)->d_equalityEngine );
+    while( !eqc_iter.isFinished() ){
+      Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)
+                                       << std::endl;
+      if( (*eqc_iter).hasOperator() && (*eqc_iter).getOperator() == op ) ele.insert(*eqc_iter);
+      eqc_iter++;
+    }
+    if( !ele.empty() ){
+      if(Debug.isOn("efficient-e-match-stats")){
+        Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
+      }
+      handler.addMonoCandidate(ele, 0);
+    }
+
+  } else {
+    Node op = pats[0].getOperator();
+    TermDb* db = d_quantEngine->getTermDatabase();
+    if(db->d_op_map[op].begin() != db->d_op_map[op].end()){
+      SetNode ele;
+      // for(std::vector<Node>::iterator i = db->d_op_map[op].begin(), end = db->d_op_map[op].end(); i != end; ++i){
+      //   if(CandidateGenerator::isLegalCandidate(*i)) ele.insert(*i);
+      // }
+      ele.insert(db->d_op_map[op].begin(), db->d_op_map[op].end());
+      if(Debug.isOn("efficient-e-match-stats")){
+        Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
+      }
+      handler.addMonoCandidate(ele, 0);
+    }
+  }
   Debug("efficient-e-match") << "Done." << std::endl;
 }
 
-void InstantiatorTheoryUf::registerTrigger( Trigger* tr, Node op ){
+void InstantiatorTheoryUf::registerTrigger( theory::inst::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 );
   }
@@ -506,9 +826,28 @@ void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){
   }
 }
 
-void InstantiatorTheoryUf::outputInvertedPathString( const char* c, InvertedPathString& ips ){
+void InstantiatorTheoryUf::outputIps( const char* c, Ips& ips ){
   for( int i=0; i<(int)ips.size(); i++ ){
     if( i>0 ){ Debug( c ) << "."; }
     Debug( c ) << ips[i].first << "." << ips[i].second;
   }
 }
+
+rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClasses(){
+  uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory());
+  eq::EqualityEngine* ee =
+    static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
+  return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee);
+}
+
+rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClass(){
+  uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory());
+  eq::EqualityEngine* ee =
+    static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
+  return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee);
+}
+
+
+} /* namespace uf */
+} /* namespace theory */
+} /* namespace cvc4 */
diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h
index 4ddc01986..3a2a5cc0e 100644
--- a/src/theory/uf/theory_uf_instantiator.h
+++ b/src/theory/uf/theory_uf_instantiator.h
@@ -27,6 +27,9 @@
 
 #include "util/stats.h"
 #include "theory/uf/theory_uf.h"
+#include "theory/trigger.h"
+#include "util/ntuple.h"
+#include "context/cdqueue.h"
 
 namespace CVC4 {
 namespace theory {
@@ -38,6 +41,300 @@ namespace quantifiers{
 namespace uf {
 
 class InstantiatorTheoryUf;
+class HandlerPcDispatcher;
+class HandlerPpDispatcher;
+
+typedef std::set<Node> SetNode;
+
+template<class T>
+class CleanUpPointer{
+public:
+  inline void operator()(T** e){
+    delete(*e);
+  };
+};
+
+class EfficientHandler{
+public:
+  typedef std::pair< Node, size_t > MonoCandidate;
+  typedef std::pair< MonoCandidate, MonoCandidate > MultiCandidate;
+  typedef std::pair< SetNode, size_t > MonoCandidates;
+  typedef std::pair< MonoCandidates, MonoCandidates > MultiCandidates;
+private:
+  /* Queue of candidates */
+  typedef context::CDQueue< MonoCandidates *, CleanUpPointer<MonoCandidates> > MonoCandidatesQueue;
+  typedef context::CDQueue< MultiCandidates *, CleanUpPointer<MultiCandidates> > MultiCandidatesQueue;
+  MonoCandidatesQueue d_monoCandidates;
+  typedef uf::SetNode::iterator SetNodeIter;
+  context::CDO<SetNodeIter> d_si;
+  context::CDO<bool> d_mono_not_first;
+
+  MonoCandidatesQueue d_monoCandidatesNewTerm;
+  context::CDO<SetNodeIter> d_si_new_term;
+  context::CDO<bool> d_mono_not_first_new_term;
+
+
+  MultiCandidatesQueue d_multiCandidates;
+  context::CDO<SetNodeIter> d_si1;
+  context::CDO<SetNodeIter> d_si2;
+  context::CDO<bool> d_multi_not_first;
+
+
+  friend class InstantiatorTheoryUf;
+  friend class HandlerPcDispatcher;
+  friend class HandlerPpDispatcher;
+  friend class HandlerNewTermDispatcher;
+protected:
+  void addMonoCandidate(SetNode & s, size_t index){
+    Assert(!s.empty());
+    d_monoCandidates.push(new MonoCandidates(s,index));
+  }
+  void addMonoCandidateNewTerm(SetNode & s, size_t index){
+    Assert(!s.empty());
+    d_monoCandidatesNewTerm.push(new MonoCandidates(s,index));
+  }
+  void addMultiCandidate(SetNode & s1, size_t index1, SetNode & s2, size_t index2){
+    Assert(!s1.empty() && !s2.empty());
+    d_multiCandidates.push(new MultiCandidates(MonoCandidates(s1,index1),
+                                               MonoCandidates(s2,index2)));
+  }
+public:
+  EfficientHandler(context::Context * c):
+    //false for d_mono_not_first beacause its the default constructor
+    d_monoCandidates(c), d_si(c), d_mono_not_first(c,false),
+    d_monoCandidatesNewTerm(c), d_si_new_term(c),
+    d_mono_not_first_new_term(c,false),
+    d_multiCandidates(c) , d_si1(c), d_si2(c), d_multi_not_first(c,false) {};
+
+  bool getNextMonoCandidate(MonoCandidate & candidate){
+    if(d_monoCandidates.empty()) return false;
+    const MonoCandidates * front = d_monoCandidates.front();
+    SetNodeIter si_tmp;
+    if(!d_mono_not_first){
+      Assert(front->first.begin() != front->first.end());
+      d_mono_not_first = true;
+      si_tmp=front->first.begin();
+    }else{
+      si_tmp = d_si;
+      ++si_tmp;
+    };
+    if(si_tmp != front->first.end()){
+      candidate.first = (*si_tmp);
+      candidate.second = front->second;
+      d_si = si_tmp;
+      Debug("efficienthandler") << "Mono produces " << candidate.first << " for " << candidate.second << std::endl;
+      return true;
+    };
+    d_monoCandidates.pop();
+    d_mono_not_first = false;
+    return getNextMonoCandidate(candidate);
+  };
+
+  bool getNextMonoCandidateNewTerm(MonoCandidate & candidate){
+    if(d_monoCandidatesNewTerm.empty()) return false;
+    const MonoCandidates * front = d_monoCandidatesNewTerm.front();
+    SetNodeIter si_tmp;
+    if(!d_mono_not_first_new_term){
+      Assert(front->first.begin() != front->first.end());
+      d_mono_not_first_new_term = true;
+      si_tmp=front->first.begin();
+    }else{
+      si_tmp = d_si_new_term;
+      ++si_tmp;
+    };
+    if(si_tmp != front->first.end()){
+      candidate.first = (*si_tmp);
+      candidate.second = front->second;
+      d_si_new_term = si_tmp;
+      Debug("efficienthandler") << "Mono produces " << candidate.first << " for " << candidate.second << std::endl;
+      return true;
+    };
+    d_monoCandidatesNewTerm.pop();
+    d_mono_not_first_new_term = false;
+    return getNextMonoCandidateNewTerm(candidate);
+  };
+
+  bool getNextMultiCandidate(MultiCandidate & candidate){
+    if(d_multiCandidates.empty()) return false;
+    const MultiCandidates* front = d_multiCandidates.front();
+    SetNodeIter si1_tmp;
+    SetNodeIter si2_tmp;
+    if(!d_multi_not_first){
+      Assert(front->first.first.begin() != front->first.first.end());
+      Assert(front->second.first.begin() != front->second.first.end());
+      si1_tmp = front->first.first.begin();
+      si2_tmp = front->second.first.begin();
+    }else{
+      si1_tmp = d_si1;
+      si2_tmp = d_si2;
+      ++si2_tmp;
+    };
+    if(si2_tmp != front->second.first.end()){
+      candidate.first.first = *si1_tmp;
+      candidate.first.second = front->first.second;
+      candidate.second.first = *si2_tmp;
+      candidate.second.second = front->second.second;
+      if(!d_multi_not_first){d_si1 = si1_tmp; d_multi_not_first = true; };
+      d_si2 = si2_tmp;
+      Debug("efficienthandler") << "Multi1 produces "
+                                << candidate.first.first << " for "
+                                << candidate.first.second << " and "
+                                << candidate.second.first << " for "
+                                << candidate.second.second << " and "
+                                << std::endl;
+      return true;
+    }; // end of the second set
+    si2_tmp = front->second.first.begin();
+    ++si1_tmp;
+    if(si1_tmp != front->first.first.end()){
+      candidate.first.first = *si1_tmp;
+      candidate.first.second = front->first.second;
+      candidate.second.first = *si2_tmp;
+      candidate.second.second = front->second.second;
+      d_si1 = si1_tmp;
+      d_si2 = si2_tmp;
+      Debug("efficienthandler") << "Multi2 produces "
+                                << candidate.first.first << " for "
+                                << candidate.first.second << " and "
+                                << candidate.second.first << " for "
+                                << candidate.second.second << " and "
+                                << std::endl;
+      return true;
+    }; // end of the first set
+    d_multiCandidates.pop();
+    d_multi_not_first = false;
+    return getNextMultiCandidate(candidate);
+  }
+};
+
+class PcDispatcher{
+public:
+  virtual ~PcDispatcher(){};
+  /* Send the node to the dispatcher */
+  virtual void send(SetNode & s) = 0;
+};
+
+
+class HandlerPcDispatcher: public PcDispatcher{
+  EfficientHandler* d_handler;
+  size_t d_index;
+public:
+  HandlerPcDispatcher(EfficientHandler* handler, size_t index):
+    d_handler(handler), d_index(index) {};
+  void send(SetNode & s){
+    d_handler->addMonoCandidate(s,d_index);
+  }
+};
+
+
+/** All the dispatcher that correspond to this node */
+class NodePcDispatcher: public PcDispatcher{
+#ifdef CVC4_DEBUG
+public:
+  Node pat;
+#endif/* CVC4_DEBUG*/
+private:
+  std::vector<HandlerPcDispatcher> d_dis;
+public:
+  void send(SetNode & s){
+    Assert(!s.empty());
+    for(std::vector<HandlerPcDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
+        i != end; ++i){
+      (*i).send(s);
+    }
+  }
+  void addPcDispatcher(EfficientHandler* handler, size_t index){
+    d_dis.push_back(HandlerPcDispatcher(handler,index));
+  }
+};
+
+
+class HandlerNewTermDispatcher: public PcDispatcher{
+  EfficientHandler* d_handler;
+  size_t d_index;
+public:
+  HandlerNewTermDispatcher(EfficientHandler* handler, size_t index):
+    d_handler(handler), d_index(index) {};
+  void send(SetNode & s){
+    d_handler->addMonoCandidateNewTerm(s,d_index);
+  }
+};
+
+/** All the dispatcher that correspond to this node */
+class NodeNewTermDispatcher: public PcDispatcher{
+#ifdef CVC4_DEBUG
+public:
+  Node pat;
+#endif/* CVC4_DEBUG*/
+private:
+  std::vector<HandlerNewTermDispatcher> d_dis;
+public:
+  void send(SetNode & s){
+    Assert(!s.empty());
+    for(std::vector<HandlerNewTermDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
+        i != end; ++i){
+      (*i).send(s);
+    }
+  }
+  void addNewTermDispatcher(EfficientHandler* handler, size_t index){
+    d_dis.push_back(HandlerNewTermDispatcher(handler,index));
+  }
+};
+
+class PpDispatcher{
+public:
+  virtual ~PpDispatcher(){};
+  /* Send the node to the dispatcher */
+  virtual void send(SetNode & s1, SetNode & s2, SetNode & sinter) = 0;
+};
+
+
+class HandlerPpDispatcher: public PpDispatcher{
+  EfficientHandler* d_handler;
+  size_t d_index1;
+  size_t d_index2;
+public:
+  HandlerPpDispatcher(EfficientHandler* handler, size_t index1, size_t index2):
+    d_handler(handler), d_index1(index1), d_index2(index2) {};
+  void send(SetNode & s1, SetNode & s2, SetNode & sinter){
+    if(d_index1 == d_index2){
+      if(!sinter.empty())
+        d_handler->addMonoCandidate(sinter,d_index1);
+    }else{
+      d_handler->addMultiCandidate(s1,d_index1,s2,d_index2);
+    }
+  }
+};
+
+
+/** All the dispatcher that correspond to this node */
+class NodePpDispatcher: public PpDispatcher{
+#ifdef CVC4_DEBUG
+public:
+  Node pat1;
+  Node pat2;
+#endif/* CVC4_DEBUG */
+private:
+  std::vector<HandlerPpDispatcher> d_dis;
+  void send(SetNode & s1, SetNode & s2, SetNode & inter){
+    for(std::vector<HandlerPpDispatcher>::iterator i = d_dis.begin(), end = d_dis.end();
+        i != end; ++i){
+      (*i).send(s1,s2,inter);
+    }
+  }
+public:
+  void send(SetNode & s1, SetNode & s2){
+    // can be done in HandlerPpDispatcher lazily
+    Assert(!s1.empty() && !s2.empty());
+    SetNode inter;
+    std::set_intersection( s1.begin(), s1.end(), s2.begin(), s2.end(),
+                           std::inserter( inter, inter.begin() ) );
+    send(s1,s2,inter);
+  }
+  void addPpDispatcher(EfficientHandler* handler, size_t index1, size_t index2){
+    d_dis.push_back(HandlerPpDispatcher(handler,index1,index2));
+  }
+};
 
 //equivalence class info
 class EqClassInfo
@@ -68,7 +365,7 @@ public:
 };
 
 class InstantiatorTheoryUf : public Instantiator{
-  friend class ::CVC4::theory::InstMatchGenerator;
+  friend class ::CVC4::theory::inst::InstMatchGenerator;
   friend class ::CVC4::theory::quantifiers::TermDb;
 protected:
   typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
@@ -82,7 +379,14 @@ protected:
   InstStrategyUserPatterns* d_isup;
 public:
   InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th);
-  ~InstantiatorTheoryUf() {}
+  ~InstantiatorTheoryUf() {
+    for(std::map< Node, std::pair<NodePcDispatcher*, NodePpDispatcher*> >::iterator
+          i = d_pat_cand_gens.begin(), end = d_pat_cand_gens.end();
+        i != end; i++){
+      delete(i->second.first);
+      delete(i->second.second);
+    }
+  }
   /** assertNode method */
   void assertNode( Node assertion );
   /** Pre-register a term.  Done one time for a Node, ever. */
@@ -127,6 +431,9 @@ public:
   bool areDisequal( Node a, Node b );
   Node getRepresentative( Node a );
   Node getInternalRepresentative( Node a );
+  /** general creators of candidate generators */
+  rrinst::CandidateGenerator* getRRCanGenClasses();
+  rrinst::CandidateGenerator* getRRCanGenClass();
   /** new node */
   void newEqClass( TNode n );
   /** merge */
@@ -136,47 +443,66 @@ public:
   /** get equivalence class info */
   EqClassInfo* getEquivalenceClassInfo( Node n );
   EqClassInfo* getOrCreateEquivalenceClassInfo( Node n );
+  typedef std::vector< std::pair< Node, int > > Ips;
+  typedef std::map< Node, std::vector< std::pair< Node, Ips > > > PpIpsMap;
+  typedef std::map< Node, std::vector< triple< size_t, Node, Ips > > > MultiPpIpsMap;
+
 private:
-  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;
+  std::map< Node, std::map< Node, std::vector< std::pair< NodePcDispatcher*, Ips > > > > d_pc_pairs;
   /** Parent/Parent Pairs (for efficient E-matching) */
-  std::map< Node, std::map< Node, std::map< Node, std::vector< IpsPair > > > > d_pp_pairs;
+  std::map< Node, std::map< Node, std::vector< triple< NodePpDispatcher*, Ips, Ips > > > > d_pp_pairs;
+  /** Constants/Child Pairs
+      So, for example, if we have the pattern f( x ) = c, then d_pc_pairs[f][c] = ..., pcdispatcher, ...
+  */
+  //TODO constant in pattern can use the same thing just add an Ips
+  std::map< Node, std::map< Node, NodePcDispatcher* > > d_cc_pairs;
   /** list of all candidate generators for each operator */
-  std::map< Node, std::vector< CandidateGenerator* > > d_cand_gens;
+  std::map< Node, NodeNewTermDispatcher > d_cand_gens;
+  /** list of all candidate generators for each type */
+  std::map< TypeNode, NodeNewTermDispatcher > d_cand_gen_types;
   /** map from patterns to candidate generators */
-  std::map< Node, std::vector< CandidateGenerator* > > d_pat_cand_gens;
+  std::map< Node, std::pair<NodePcDispatcher*, NodePpDispatcher*> > 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 );
+  void registerPatternElementPairs2( Node pat, Ips& ips,
+                                     PpIpsMap & pp_ips_map, NodePcDispatcher* npc);
+  void registerPatternElementPairs( Node pat, PpIpsMap & pp_ips_map,
+                                    NodePcDispatcher* npc, NodePpDispatcher* npp);
+  /** find the pp-pair between pattern inside multi-pattern*/
+  void combineMultiPpIpsMap(PpIpsMap & pp_ips_map, MultiPpIpsMap & multi_pp_ips_map,
+                            EfficientHandler& eh, size_t index2,
+                            const std::vector<Node> & pats); //pats for debug
   /** compute candidates for pc pairs */
-  void computeCandidatesPcPairs( Node a, Node b );
+  void computeCandidatesPcPairs( Node a, EqClassInfo*, Node b, EqClassInfo* );
   /** compute candidates for pp pairs */
-  void computeCandidatesPpPairs( Node a, Node b );
+  void computeCandidatesPpPairs( Node a, EqClassInfo*, Node b, EqClassInfo* );
+  /** compute candidates for cc pairs */
+  void computeCandidatesConstants( Node a, EqClassInfo*, Node b, EqClassInfo* );
   /** collect terms based on inverted path string */
-  void collectTermsIps( 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 );
+  void collectTermsIps( Ips& ips, SetNode& terms, int index);
+  bool collectParentsTermsIps( Node n, Node f, int arg, SetNode& terms, bool addRep, bool modEq = true );
 public:
+  void collectTermsIps( Ips& ips, SetNode& terms);
   /** 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;
+  std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
 public:
   /** register trigger (for eager quantifier instantiation) */
-  void registerTrigger( Trigger* tr, Node op );
+  void registerTrigger( inst::Trigger* tr, Node op );
+  void registerEfficientHandler( EfficientHandler& eh, const std::vector<Node> & pat );
+public:
+  void newTerms(SetNode& s);
 public:
   /** output eq class */
   void outputEqClass( const char* c, Node n );
   /** output inverted path string */
-  void outputInvertedPathString( const char* c, InvertedPathString& ips );
+  void outputIps( const char* c, Ips& ips );
 };/* class InstantiatorTheoryUf */
 
 /** equality query object using instantiator theory uf */