Support for relational operators identity and join image

5 files changed, 417 insertions, 75 deletions

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index cfe7eb632..34fef7d64 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -50,6 +50,8 @@ operator JOIN 		   2  "set join"
 operator PRODUCT 	   2  "set cartesian product"
 operator TRANSPOSE 	   1  "set transpose"
 operator TCLOSURE      1  "set transitive closure"
+operator JOIN_IMAGE	   2  "set join image"
+operator IDEN 	   	   1  "set identity"
 
 typerule UNION          ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 typerule INTERSECTION   ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
@@ -67,6 +69,8 @@ typerule JOIN 			::CVC4::theory::sets::RelBinaryOperatorTypeRule
 typerule PRODUCT 		::CVC4::theory::sets::RelBinaryOperatorTypeRule
 typerule TRANSPOSE 		::CVC4::theory::sets::RelTransposeTypeRule
 typerule TCLOSURE 	    ::CVC4::theory::sets::RelTransClosureTypeRule
+typerule JOIN_IMAGE	    ::CVC4::theory::sets::JoinImageTypeRule
+typerule IDEN 			::CVC4::theory::sets::RelIdenTypeRule
 
 construle UNION         ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 construle INTERSECTION  ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
@@ -80,5 +84,7 @@ construle JOIN 			::CVC4::theory::sets::RelBinaryOperatorTypeRule
 construle PRODUCT 		::CVC4::theory::sets::RelBinaryOperatorTypeRule
 construle TRANSPOSE 	::CVC4::theory::sets::RelTransposeTypeRule
 construle TCLOSURE 	    ::CVC4::theory::sets::RelTransClosureTypeRule
+construle JOIN_IMAGE 	::CVC4::theory::sets::JoinImageTypeRule
+construle IDEN 			::CVC4::theory::sets::RelIdenTypeRule
 
 endtheory
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 0c5c7a6a2..03e0c64f8 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -58,8 +58,6 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
 
         if( kind_terms.find(kind::TRANSPOSE) != kind_terms.end() ) {
           std::vector<Node> tp_terms = kind_terms[kind::TRANSPOSE];
-          // exp is a membership term and tp_terms contains all
-          // transposed terms that are equal to the right hand side of exp
           if( tp_terms.size() > 0 ) {
             applyTransposeRule( tp_terms );
             applyTransposeRule( tp_terms[0], rel_rep, exp );
@@ -67,9 +65,6 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
         }
         if( kind_terms.find(kind::JOIN) != kind_terms.end() ) {
           std::vector<Node> join_terms = kind_terms[kind::JOIN];
-          // exp is a membership term and join_terms contains all
-          // terms involving "join" operator that are in the same
-          // equivalence class with the right hand side of exp
           for( unsigned int j = 0; j < join_terms.size(); j++ ) {
             applyJoinRule( join_terms[j], rel_rep, exp );
           }
@@ -86,6 +81,18 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
             applyTCRule( mem, tc_terms[j], rel_rep, exp );
           }
         }
+        if( kind_terms.find(kind::JOIN_IMAGE) != kind_terms.end() ) {
+          std::vector<Node> join_image_terms = kind_terms[kind::JOIN_IMAGE];
+          for( unsigned int j = 0; j < join_image_terms.size(); j++ ) {
+            applyJoinImageRule( mem, join_image_terms[j], exp );
+          }
+        }
+        if( kind_terms.find(kind::IDEN) != kind_terms.end() ) {
+          std::vector<Node> iden_terms = kind_terms[kind::IDEN];
+          for( unsigned int j = 0; j < iden_terms.size(); j++ ) {
+            applyIdenRule( mem, iden_terms[j], exp );
+          }
+        }
       }
       m_it++;
     }
@@ -115,7 +122,18 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
               buildTCGraphForRel( *term_it );
               term_it++;
             }
-
+          } else if( k_t_it->first == kind::JOIN_IMAGE ) {
+            std::vector<Node>::iterator term_it = k_t_it->second.begin();
+            while( term_it != k_t_it->second.end() ) {
+              computeMembersForJoinImageTerm( *term_it );
+              term_it++;
+            }
+          } else if( k_t_it->first == kind::IDEN ) {
+            std::vector<Node>::iterator term_it = k_t_it->second.begin();
+            while( term_it != k_t_it->second.end() ) {
+              computeMembersForIdenTerm( *term_it );
+              term_it++;
+            }
           }
           k_t_it++;
         }
@@ -136,7 +154,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
       Node                      eqc_rep  = (*eqcs_i);
       eq::EqClassIterator       eqc_i   = eq::EqClassIterator( eqc_rep, d_eqEngine );
 
-      Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << std::endl;
+      Trace("rels-ee") << "[sets-rels-ee] Eqc term representative: " << eqc_rep << " with type " << eqc_rep.getType() << std::endl;
 
       while( !eqc_i.isFinished() ){
         Node eqc_node = (*eqc_i);
@@ -164,16 +182,13 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
                 computeTupleReps(tup_rep);
                 d_membership_trie[rel_rep].addTerm(tup_rep, d_tuple_reps[tup_rep]);
               }
-            } else {
-              if( safelyAddToMap(d_rReps_nonMemberReps_cache, rel_rep, tup_rep) ) {
-                addToMap(d_rReps_nonMemberReps_exp_cache, rel_rep, reason);
-              }
             }
           }
         // collect relational terms info
         } else if( eqc_rep.getType().isSet() && eqc_rep.getType().getSetElementType().isTuple() ) {
           if( eqc_node.getKind() == kind::TRANSPOSE || eqc_node.getKind() == kind::JOIN ||
-              eqc_node.getKind() == kind::PRODUCT || eqc_node.getKind() == kind::TCLOSURE ) {
+              eqc_node.getKind() == kind::PRODUCT || eqc_node.getKind() == kind::TCLOSURE ||
+              eqc_node.getKind() == kind::JOIN_IMAGE || eqc_node.getKind() == kind::IDEN ) {
             std::vector<Node> terms;
             std::map< kind::Kind_t, std::vector<Node> >  rel_terms;
             TERM_IT terms_it = d_terms_cache.find(eqc_rep);
@@ -210,6 +225,205 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     Trace("rels-debug") << "[Theory::Rels] Done with collecting relational terms!" << std::endl;
   }
 
+  /* JOIN-IMAGE UP  :   (x, x1) IS_IN R, ..., (x, xn) IS_IN R  (R JOIN_IMAGE n)
+  *                     -------------------------------------------------------
+  *                     x IS_IN (R JOIN_IMAGE n) || NOT DISTINCT(x1, ... , xn)
+  *
+  */
+
+  void TheorySetsRels::computeMembersForJoinImageTerm( Node join_image_term ) {
+    Trace("rels-debug") << "\n[Theory::Rels] *********** Compute members for JoinImage Term = " << join_image_term << std::endl;
+    MEM_IT rel_mem_it = d_rReps_memberReps_cache.find( getRepresentative( join_image_term[0] ) );
+
+    if( rel_mem_it == d_rReps_memberReps_cache.end() ) {
+      return;
+    }
+
+    Node join_image_rel = join_image_term[0];
+    std::hash_set< Node, NodeHashFunction > hasChecked;
+    Node join_image_rel_rep = getRepresentative( join_image_rel );
+    std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin();
+    MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep );
+    std::vector< Node >::iterator mem_rep_exp_it = (*rel_mem_exp_it).second.begin();
+    unsigned int min_card = join_image_term[1].getConst<Rational>().getNumerator().getUnsignedInt();
+
+    while( mem_rep_it != (*rel_mem_it).second.end() ) {
+      Node fst_mem_rep = RelsUtils::nthElementOfTuple( *mem_rep_it, 0 );
+
+      if( hasChecked.find( fst_mem_rep ) != hasChecked.end() ) {
+        ++mem_rep_it;
+        ++mem_rep_exp_it;
+        continue;
+      }
+      hasChecked.insert( fst_mem_rep );
+
+      Datatype dt = join_image_term.getType().getSetElementType().getDatatype();
+      Node new_membership = NodeManager::currentNM()->mkNode(kind::MEMBER,
+                                                             NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR,
+                                                                                               Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ),
+                                                             join_image_term);
+      if( holds( new_membership ) ) {
+        ++mem_rep_it;
+        ++mem_rep_exp_it;
+        continue;
+      }
+
+      std::vector< Node > reasons;
+      std::vector< Node > existing_members;
+      std::vector< Node >::iterator mem_rep_exp_it_snd = (*rel_mem_exp_it).second.begin();
+
+      while( mem_rep_exp_it_snd != (*rel_mem_exp_it).second.end() ) {
+        Node fst_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 0 );
+
+        if( areEqual( fst_mem_rep,  fst_element_snd_mem ) ) {
+          bool notExist = true;
+          std::vector< Node >::iterator existing_mem_it = existing_members.begin();
+          Node snd_element_snd_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it_snd)[0], 1 );
+
+          while( existing_mem_it != existing_members.end() ) {
+            if( areEqual( (*existing_mem_it), snd_element_snd_mem ) ) {
+              notExist = false;
+              break;
+            }
+            ++existing_mem_it;
+          }
+
+          if( notExist ) {
+            existing_members.push_back( snd_element_snd_mem );
+            reasons.push_back( *mem_rep_exp_it_snd );
+            if( fst_mem_rep != fst_element_snd_mem ) {
+              reasons.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, fst_mem_rep, fst_element_snd_mem ) );
+            }
+            if( join_image_rel != (*mem_rep_exp_it_snd)[1] ) {
+              reasons.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it_snd)[1], join_image_rel ));
+            }
+            if( existing_members.size() == min_card ) {
+              if( min_card >= 2) {
+                new_membership = NodeManager::currentNM()->mkNode( kind::OR, new_membership, NodeManager::currentNM()->mkNode( kind::NOT, NodeManager::currentNM()->mkNode( kind::DISTINCT, existing_members ) ));
+              }
+              Assert(reasons.size() >= 1);
+              sendInfer( new_membership, reasons.size() > 1 ? NodeManager::currentNM()->mkNode( kind::AND, reasons) : reasons[0], "JOIN-IMAGE UP" );
+              break;
+            }
+          }
+        }
+        ++mem_rep_exp_it_snd;
+      }
+      ++mem_rep_it;
+      ++mem_rep_exp_it;
+    }
+    Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for JoinImage Term" << join_image_term << "*********** " << std::endl;
+  }
+
+  /* JOIN-IMAGE DOWN  : (x) IS_IN (R JOIN_IMAGE n)
+  *                     -------------------------------------------------------
+  *                     (x, x1) IS_IN R .... (x, xn) IS_IN R  DISTINCT(x1, ... , xn)
+  *
+  */
+
+  void TheorySetsRels::applyJoinImageRule( Node mem_rep, Node join_image_term, Node exp ) {
+    Trace("rels-debug") << "\n[Theory::Rels] *********** applyJoinImageRule on " << join_image_term
+                        << " with mem_rep = " << mem_rep  << " and exp = " << exp << std::endl;
+    if( d_rel_nodes.find( join_image_term ) == d_rel_nodes.end() ) {
+      computeMembersForJoinImageTerm( join_image_term );
+      d_rel_nodes.insert( join_image_term );
+    }
+
+    Node join_image_rel = join_image_term[0];
+    Node join_image_rel_rep = getRepresentative( join_image_rel );
+    MEM_IT rel_mem_it = d_rReps_memberReps_cache.find( join_image_rel_rep );
+    unsigned int min_card = join_image_term[1].getConst<Rational>().getNumerator().getUnsignedInt();
+
+    if( rel_mem_it != d_rReps_memberReps_cache.end() ) {
+      if( d_membership_trie.find( join_image_rel_rep ) != d_membership_trie.end() ) {
+        computeTupleReps( mem_rep );
+        if( d_membership_trie[join_image_rel_rep].findSuccessors(d_tuple_reps[mem_rep]).size() >= min_card ) {
+          return;
+        }
+      }
+    }
+
+    Node reason = exp;
+    Node conclusion = d_trueNode;
+    std::vector< Node > distinct_skolems;
+    Node fst_mem_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
+
+    if( exp[1] != join_image_term ) {
+      reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], join_image_term ) );
+    }
+    for( unsigned int i = 0; i < min_card; i++ ) {
+      Node skolem = NodeManager::currentNM()->mkSkolem( "jig", join_image_rel.getType()[0].getTupleTypes()[0] );
+      distinct_skolems.push_back( skolem );
+      conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( join_image_rel, fst_mem_element, skolem ), join_image_rel ) );
+    }
+    if( distinct_skolems.size() >= 2 ) {
+      conclusion =  NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::DISTINCT, distinct_skolems ) );
+    }
+    sendInfer( conclusion, reason, "JOIN-IMAGE DOWN" );
+    Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl;
+
+  }
+
+
+  /* IDENTITY-DOWN  : (x, y) IS_IN IDEN(R)
+  *               -------------------------------------------------------
+  *                   x = y,  (x IS_IN R)
+  *
+  */
+
+  void TheorySetsRels::applyIdenRule( Node mem_rep, Node iden_term, Node exp) {
+    Trace("rels-debug") << "\n[Theory::Rels] *********** applyIdenRule on " << iden_term
+                        << " with mem_rep = " << mem_rep  << " and exp = " << exp << std::endl;
+    if( d_rel_nodes.find( iden_term ) == d_rel_nodes.end() ) {
+      computeMembersForIdenTerm( iden_term );
+      d_rel_nodes.insert( iden_term );
+    }
+    Node reason = exp;
+    Node fst_mem = RelsUtils::nthElementOfTuple( exp[0], 0 );
+    Node snd_mem = RelsUtils::nthElementOfTuple( exp[0], 1 );
+    Datatype dt = iden_term[0].getType().getSetElementType().getDatatype();
+    Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ), iden_term[0] );
+
+    if( exp[1] != iden_term ) {
+      reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], iden_term ) );
+    }
+    sendInfer( NodeManager::currentNM()->mkNode( kind::AND, fact, NodeManager::currentNM()->mkNode( kind::EQUAL, fst_mem, snd_mem ) ), reason, "IDENTITY-DOWN" );
+    Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyIdenRule on " << iden_term << std::endl;
+  }
+
+  /* IDEN UP  : (x) IS_IN R        IDEN(R) IN T
+  *             --------------------------------
+  *                   (x, x) IS_IN IDEN(R)
+  *
+  */
+
+  void TheorySetsRels::computeMembersForIdenTerm( Node iden_term ) {
+    Trace("rels-debug") << "\n[Theory::Rels] *********** Compute members for Iden Term = " << iden_term << std::endl;
+    Node iden_term_rel = iden_term[0];
+    Node iden_term_rel_rep = getRepresentative( iden_term_rel );
+
+    if( d_rReps_memberReps_cache.find( iden_term_rel_rep ) == d_rReps_memberReps_cache.end() ) {
+      return;
+    }
+
+    MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( iden_term_rel_rep );
+    std::vector< Node >::iterator mem_rep_exp_it = (*rel_mem_exp_it).second.begin();
+
+    while( mem_rep_exp_it != (*rel_mem_exp_it).second.end() ) {
+      Node reason = *mem_rep_exp_it;
+      Node fst_exp_mem = RelsUtils::nthElementOfTuple( (*mem_rep_exp_it)[0], 0 );
+      Node new_mem = RelsUtils::constructPair( iden_term, fst_exp_mem, fst_exp_mem );
+
+      if( (*mem_rep_exp_it)[1] != iden_term_rel ) {
+        reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, (*mem_rep_exp_it)[1], iden_term_rel ) );
+      }
+      sendInfer( NodeManager::currentNM()->mkNode( kind::MEMBER, new_mem, iden_term ), reason, "IDENTITY-UP" );
+      ++mem_rep_exp_it;
+    }
+    Trace("rels-debug") << "\n[Theory::Rels] *********** Done with computing members for Iden Term = " << iden_term << std::endl;
+  }
+
+
   /*
    * Construct transitive closure graph for tc_rep based on the members of tc_r_rep
    */
@@ -434,7 +648,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     if( cur_set != tc_graph.end() ) {
       for( std::hash_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin();
            set_it != cur_set->second.end(); set_it++ ) {
-        Node new_pair = constructPair( tc_rel, cur_node_rep, *set_it );
+        Node new_pair = RelsUtils::constructPair( tc_rel, cur_node_rep, *set_it );
         std::vector< Node > new_reasons( reasons );
         new_reasons.push_back( rel_tc_graph_exps.find( new_pair )->second );
         doTCInference( tc_rel, new_reasons, tc_graph, rel_tc_graph_exps, start_node_rep, *set_it, seen );
@@ -548,6 +762,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     computeTupleReps(mem2);
 
     std::vector<Node> elements = d_membership_trie[r1_rep].findTerms(d_tuple_reps[mem1]);
+
     for(unsigned int j = 0; j < elements.size(); j++) {
       std::vector<Node> new_tup;
       new_tup.push_back(elements[j]);
@@ -966,11 +1181,6 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     }
   }
 
-  inline Node TheorySetsRels::constructPair(Node tc_rep, Node a, Node b) {
-    Datatype dt = tc_rep.getType().getSetElementType().getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b);
-  }
-
   /*
    * Node n[0] is a tuple variable, reduce n[0] to a concrete representation,
    * which is (e1, ..., en) where e1, ... ,en are concrete elements of tuple n[0].
@@ -1011,6 +1221,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     d_eqEngine->addFunctionKind(kind::JOIN);
     d_eqEngine->addFunctionKind(kind::TRANSPOSE);
     d_eqEngine->addFunctionKind(kind::TCLOSURE);
+    d_eqEngine->addFunctionKind(kind::JOIN_IMAGE);
+    d_eqEngine->addFunctionKind(kind::IDEN);
   }
 
   TheorySetsRels::~TheorySetsRels() {
@@ -1045,6 +1257,27 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
     }
   }
 
+  std::vector<Node> TupleTrie::findSuccessors( std::vector< Node >& reps, int argIndex ) {
+    std::vector<Node>   nodes;
+    std::map< Node, TupleTrie >::iterator it;
+
+    if( argIndex==(int)reps.size() ){
+      it = d_data.begin();
+      while(it != d_data.end()) {
+        nodes.push_back(it->first);
+        it++;
+      }
+      return nodes;
+    }else{
+      it = d_data.find( reps[argIndex] );
+      if( it==d_data.end() ){
+        return nodes;
+      }else{
+        return it->second.findSuccessors( reps, argIndex+1 );
+      }
+    }
+  }
+
   Node TupleTrie::existsTerm( std::vector< Node >& reps, int argIndex ) {
     if( argIndex==(int)reps.size() ){
       if( d_data.empty() ){        
@@ -1483,16 +1716,3 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction >
 }
 }
 }
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index fed808de4..576430eb1 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -36,6 +36,7 @@ public:
   std::map< Node, TupleTrie > d_data;
 public:
   std::vector<Node> findTerms( std::vector< Node >& reps, int argIndex = 0 );
+  std::vector<Node> findSuccessors( std::vector< Node >& reps, int argIndex = 0 );
   Node existsTerm( std::vector< Node >& reps, int argIndex = 0 );
   bool addTerm( Node n, std::vector< Node >& reps, int argIndex = 0 );
   void debugPrint( const char * c, Node n, unsigned depth = 0 );
@@ -45,12 +46,7 @@ public:
 class TheorySetsRels {
 
   typedef context::CDChunkList< Node >                            NodeList;
-  typedef context::CDChunkList< int >                             IdList;
-  typedef context::CDHashMap< int, IdList* >                      IdListMap;
   typedef context::CDHashSet< Node, NodeHashFunction >            NodeSet;
-  typedef context::CDHashMap< Node, bool, NodeHashFunction >      NodeBoolMap;
-  typedef context::CDHashMap< Node, NodeList*, NodeHashFunction > NodeListMap;
-  typedef context::CDHashMap< Node, NodeSet*, NodeHashFunction >  NodeSetMap;
   typedef context::CDHashMap< Node, Node, NodeHashFunction >      NodeMap;
 
 public:
@@ -71,7 +67,6 @@ private:
    * d_not_mem tuples that are not members of this equivalence class
    * d_tp is a node of kind TRANSPOSE (if any) in this equivalence class,
    * d_pt is a node of kind PRODUCT (if any) in this equivalence class,
-   * d_join is a node of kind JOIN (if any) in this equivalence class,
    * d_tc is a node of kind TCLOSURE (if any) in this equivalence class,
    */
   class EqcInfo
@@ -101,15 +96,13 @@ private:
   Node                          d_falseNode;
 
   /** Facts and lemmas to be sent to EE */
-  std::map< Node, Node >        d_pending_facts;
-  std::vector< Node >           d_lemmas_out;
   NodeList                      d_pending_merge;
-
-  /** inferences: maintained to ensure ref count for internally introduced nodes */
   NodeSet                       d_lemmas_produced;
   NodeSet                       d_shared_terms;
+  std::vector< Node >           d_lemmas_out;
+  std::map< Node, Node >        d_pending_facts;
+
 
-  /** Relations that have been applied JOIN, PRODUCT, TC composition rules */
   std::hash_set< Node, NodeHashFunction >       d_rel_nodes;
   std::map< Node, std::vector<Node> >           d_tuple_reps;
   std::map< Node, TupleTrie >                   d_membership_trie;
@@ -117,41 +110,21 @@ private:
   /** Symbolic tuple variables that has been reduced to concrete ones */
   std::hash_set< Node, NodeHashFunction >       d_symbolic_tuples;
 
-  /** Mapping between relation and its (non)member representatives */
-  std::map< Node, std::vector<Node> >           d_rReps_memberReps_cache;
-  std::map< Node, std::vector<Node> >           d_rReps_nonMemberReps_cache;
-
-
-  /** Mapping between relation and its (non)member representatives explanation */
-  std::map< Node, std::vector<Node> >           d_rReps_memberReps_exp_cache;
-  std::map< Node, std::vector<Node> >           d_rReps_nonMemberReps_exp_cache;
-
   /** Mapping between relation and its member representatives */
-  std::map< Node, std::vector<Node> >           d_membership_db;
+  std::map< Node, std::vector< Node > >           d_rReps_memberReps_cache;
 
-  /** Mapping between relation and its members' explanation */
-  std::map< Node, std::vector<Node> >           d_membership_exp_db;
+  /** Mapping between relation and its member representatives explanation */
+  std::map< Node, std::vector< Node > >           d_rReps_memberReps_exp_cache;
 
   /** Mapping between a relation representative and its equivalent relations involving relational operators */
   std::map< Node, std::map<kind::Kind_t, std::vector<Node> > >                  d_terms_cache;
 
-  /** Mapping between relation and its member representatives */
-  std::map< Node, std::vector<Node> >           d_arg_rep_tp_terms;
-
-  /** Mapping between TC(r) and one explanation when building TC graph*/
-  std::map< Node, Node >                                                        d_membership_tc_exp_cache;
-
-  /** Mapping between transitive closure relation TC(r) (is not necessary a representative) and members directly asserted members */
-  std::map< Node, std::hash_set<Node, NodeHashFunction> >                       d_tc_membership_db;
-
   /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/
-  std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > >     d_tc_r_graph;
   std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > >     d_rRep_tcGraph;
   std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > >     d_tcr_tcGraph;
   std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps;
   std::map< Node, std::vector< Node > > d_tc_lemmas_last;
 
-  /** Mapping between transitive closure TC(r)'s representative and TC(r) */
   std::map< Node, EqcInfo* > d_eqc_info;
 
 public:
@@ -176,6 +149,8 @@ private:
   void applyTransposeRule( Node rel, Node rel_rep, Node exp );
   void applyProductRule( Node rel, Node rel_rep, Node exp );
   void applyJoinRule( Node rel, Node rel_rep, Node exp);
+  void applyJoinImageRule( Node mem_rep, Node rel_rep, Node exp);
+  void applyIdenRule( Node mem_rep, Node rel_rep, Node exp);
   void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp);
   void buildTCGraphForRel( Node tc_rel );
   void doTCInference();
@@ -185,7 +160,9 @@ private:
 
   void composeMembersForRels( Node );
   void computeMembersForBinOpRel( Node );
+  void computeMembersForIdenTerm( Node );
   void computeMembersForUnaryOpRel( Node );
+  void computeMembersForJoinImageTerm( Node );
 
   bool isTCReachable( Node mem_rep, Node tc_rel );
   void isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen,
@@ -206,7 +183,6 @@ private:
   void computeTupleReps( Node );
   bool areEqual( Node a, Node b );
   Node getRepresentative( Node t );
-  bool insertIntoIdList(IdList&, int);
   bool exists( std::vector<Node>&, Node );
   Node mkAnd( std::vector< TNode >& assumptions );
   inline void addToMembershipDB( Node, Node, Node  );
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 8facf1f48..3590fc62d 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -288,7 +288,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
       std::set<Node> newSet;
       std::set_union(left.begin(), left.end(), right.begin(), right.end(),
-			  std::inserter(newSet, newSet.begin()));
+                          std::inserter(newSet, newSet.begin()));
       Node newNode = NormalForm::elementsToSet(newSet, node.getType());
       Assert(newNode.isConst());
       Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
@@ -381,7 +381,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
         std::set<Node>::iterator right_it = right.begin();
         int right_len = (*right_it).getType().getTupleLength();
         while(right_it != right.end()) {
-          Trace("rels-debug") << "Sets::postRewrite processing left_it = " <<  *right_it << std::endl;
+          Trace("rels-debug") << "Sets::postRewrite processing right_it = " <<  *right_it << std::endl;
           std::vector<Node> right_tuple;
           for(int j = 0; j < right_len; j++) {
             right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j));
@@ -468,6 +468,77 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     break;
   }
   
+  case kind::IDEN: {
+    if(node[0].getKind() == kind::EMPTYSET) {
+      return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
+    } else if (node[0].isConst()) {
+      std::set<Node> iden_rel_mems;
+      std::set<Node> rel_mems = NormalForm::getElementsFromNormalConstant(node[0]);
+      std::set<Node>::iterator rel_mems_it = rel_mems.begin();
+
+      while( rel_mems_it != rel_mems.end() ) {
+        Node fst_mem = RelsUtils::nthElementOfTuple( *rel_mems_it, 0);
+        iden_rel_mems.insert(RelsUtils::constructPair(node, fst_mem, fst_mem));
+        ++rel_mems_it;
+      }
+
+      Node new_node = NormalForm::elementsToSet(iden_rel_mems, node.getType());
+      Assert(new_node.isConst());
+      Trace("rels-postrewrite") << "Rels::postRewrite returning " << new_node << std::endl;
+      return RewriteResponse(REWRITE_DONE, new_node);
+
+    } else {
+      Trace("rels-postrewrite") << "Rels::postRewrite miss to handle term " << node << std::endl;
+    }
+    break;
+  }
+
+  case kind::JOIN_IMAGE: {
+    unsigned int min_card = node[1].getConst<Rational>().getNumerator().getUnsignedInt();
+    Trace("rels-postrewrite") << "Rels::postRewrite  " << node << " with min_card = " << min_card << std::endl;
+
+    if( min_card == 0) {
+      return RewriteResponse(REWRITE_DONE, nm->mkNullaryOperator( node.getType(), kind::UNIVERSE_SET ));
+    } else if(node[0].getKind() == kind::EMPTYSET) {
+      return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
+    } else if (node[0].isConst()) {
+      std::set<Node> has_checked;
+      std::set<Node> join_img_mems;
+      std::set<Node> rel_mems = NormalForm::getElementsFromNormalConstant(node[0]);
+      std::set<Node>::iterator rel_mems_it = rel_mems.begin();
+
+      while( rel_mems_it != rel_mems.end() ) {
+        Node fst_mem = RelsUtils::nthElementOfTuple( *rel_mems_it, 0);
+        if( has_checked.find( fst_mem ) != has_checked.end() ) {
+          ++rel_mems_it;
+          continue;
+        }
+        has_checked.insert( fst_mem );
+        std::set<Node> existing_mems;
+        std::set<Node>::iterator rel_mems_it_snd = rel_mems.begin();
+        while( rel_mems_it_snd != rel_mems.end() ) {
+          Node fst_mem_snd = RelsUtils::nthElementOfTuple( *rel_mems_it_snd, 0);
+          if( fst_mem == fst_mem_snd ) {
+            existing_mems.insert( RelsUtils::nthElementOfTuple( *rel_mems_it_snd, 1) );
+          }
+          ++rel_mems_it_snd;
+        }
+        if( existing_mems.size() >= min_card ) {
+          Datatype dt = node.getType().getSetElementType().getDatatype();
+          join_img_mems.insert(NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ));
+        }
+        ++rel_mems_it;
+      }
+      Node new_node = NormalForm::elementsToSet(join_img_mems, node.getType());
+      Assert(new_node.isConst());
+      Trace("rels-postrewrite") << "Rels::postRewrite returning " << new_node << std::endl;
+      return RewriteResponse(REWRITE_DONE, new_node);
+    } else {
+      Trace("rels-postrewrite") << "Rels::postRewrite miss to handle term " << node << std::endl;
+    }
+    break;
+  }
+
   default:
     break;
   }//switch(node.getKind())
@@ -494,13 +565,13 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
     size_t setNodeIndex =  node.getNumChildren()-1;
     for(size_t i = 1; i < setNodeIndex; ++i) {
       insertedElements = nm->mkNode(kind::UNION, 
-				    insertedElements,
-				    nm->mkNode(kind::SINGLETON, node[i]));
+                                    insertedElements,
+                                    nm->mkNode(kind::SINGLETON, node[i]));
     }
     return RewriteResponse(REWRITE_AGAIN, 
-			   nm->mkNode(kind::UNION,
-				      insertedElements, 
-				      node[setNodeIndex]));
+                           nm->mkNode(kind::UNION,
+                                      insertedElements,
+                                      node[setNodeIndex]));
 
   }//kind::INSERT
   else if(node.getKind() == kind::SUBSET) {
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 25ca63c28..a3abdf508 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -227,10 +227,10 @@ struct RelBinaryOperatorTypeRule {
     TypeNode resultType = firstRelType;
 
     if(!firstRelType.isSet() || !secondRelType.isSet()) {
-      throw TypeCheckingExceptionPrivate(n, " set operator operates on non-sets");
+      throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-sets");
     }
     if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) {
-      throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)");
+      throw TypeCheckingExceptionPrivate(n, " Relational operator operates on non-relations (sets of tuples)");
     }
 
     std::vector<TypeNode> newTupleTypes;
@@ -306,6 +306,75 @@ struct RelTransClosureTypeRule {
     }
 };/* struct RelTransClosureTypeRule */
 
+struct JoinImageTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::JOIN_IMAGE);
+
+    TypeNode firstRelType = n[0].getType(check);
+
+    if(!firstRelType.isSet()) {
+      throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations");
+    }
+    if(!firstRelType[0].isTuple()) {
+      throw TypeCheckingExceptionPrivate(n, " JoinImage operator operates on non-relations (sets of tuples)");
+    }
+
+    std::vector<TypeNode> tupleTypes = firstRelType[0].getTupleTypes();
+    if(tupleTypes.size() != 2) {
+      throw TypeCheckingExceptionPrivate(n, " JoinImage operates on a non-binary relation");
+    }
+    TypeNode valType = n[1].getType(check);
+    if (valType != nodeManager->integerType()) {
+      throw TypeCheckingExceptionPrivate(
+          n, " JoinImage cardinality constraint must be integer");
+    }
+    if (n[1].getKind() != kind::CONST_RATIONAL) {
+      throw TypeCheckingExceptionPrivate(
+          n, " JoinImage cardinality constraint must be a constant");
+    }
+    CVC4::Rational r(INT_MAX);
+    if (n[1].getConst<Rational>() > r) {
+      throw TypeCheckingExceptionPrivate(
+          n, " JoinImage Exceeded INT_MAX in cardinality constraint");
+    }
+    if (n[1].getConst<Rational>().getNumerator().getSignedInt() < 0) {
+      throw TypeCheckingExceptionPrivate(
+          n, " JoinImage cardinality constraint must be non-negative");
+    }
+    std::vector<TypeNode> newTupleTypes;
+    newTupleTypes.push_back(tupleTypes[0]);
+    return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
+  }
+
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+    Assert(n.getKind() == kind::JOIN_IMAGE);
+    return false;
+  }
+};/* struct JoinImageTypeRule */
+
+struct RelIdenTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::IDEN);
+    TypeNode setType = n[0].getType(check);
+    if(check) {
+      if(!setType.isSet() && !setType.getSetElementType().isTuple()) {
+        throw TypeCheckingExceptionPrivate(n, " Identity operates on non-relation");
+      }
+      if(setType[0].getTupleTypes().size() != 1) {
+        throw TypeCheckingExceptionPrivate(n, " Identity operates on non-unary relations");
+      }
+    }
+    std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
+    tupleTypes.push_back(tupleTypes[0]);
+    return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes));
+  }
+
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+      return false;
+    }
+};/* struct RelIdenTypeRule */
 
 struct SetsProperties {
   inline static Cardinality computeCardinality(TypeNode type) {