refactored the code

- send out facts as lemmas
- fixed the non-termination problem caused by sending facts as lemmas
- unfolded symbolic tuples by adding equality lemmas

10 files changed, 484 insertions, 270 deletions

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 6ea13aa67..f8a4d009d 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -40,14 +40,14 @@ typedef std::map<Node, std::map<kind::Kind_t, std::vector<Node> > >::iterator te
 typedef std::map<Node, std::vector<Node> >::iterator mem_it;
 
   void TheorySetsRels::check(Theory::Effort level) {
-    Trace("rels-debug") << "[sets-rels] Start the relational solver..." << std::endl;
+    Trace("rels") << "\n[sets-rels] ************ Start the relational solver ************\n" << std::endl;
     collectRelsInfo();
     check();
-    doPendingSplitFacts();
+//    doPendingFacts();
     doPendingLemmas();
     Assert(d_lemma_cache.empty());
     Assert(d_pending_facts.empty());
-    Trace("rels-debug") << "[sets-rels] Done with the relational solver..." << std::endl;
+    Trace("rels") << "\n[sets-rels] ************ Done with the relational solver ************\n" << std::endl;
   }
 
   void TheorySetsRels::check() {
@@ -103,39 +103,43 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     while( !eqcs_i.isFinished() ){
       Node r = (*eqcs_i);
       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, d_eqEngine );
-      Trace("rels-ee") << "[sets-rels] term representative: " << r << std::endl;
+      Trace("rels-ee") << "[sets-rels-ee] term representative: " << r << std::endl;
       while( !eqc_i.isFinished() ){
         Node n = (*eqc_i);
         Trace("rels-ee") << "  term : " << n << std::endl;
         if(getRepresentative(r) == getRepresentative(d_trueNode) ||
            getRepresentative(r) == getRepresentative(d_falseNode)) {
           // collect membership info
-          if(n.getKind() == kind::MEMBER) {
+          if(n.getKind() == kind::MEMBER && n[1].getType().getSetElementType().isTuple()) {
             Node tup_rep = getRepresentative(n[0]);
             Node rel_rep = getRepresentative(n[1]);
-            // No rel_rep is found
-            if( d_membership_cache.find(rel_rep) == d_membership_cache.end() ) {
-              std::vector<Node> tups;
-              tups.push_back(tup_rep);
-              d_membership_cache[rel_rep] = tups;
-              Node exp = n;
-              if(getRepresentative(r) == getRepresentative(d_falseNode))
-                exp = n.negate();
-              tups.clear();
-              tups.push_back(exp);
-              d_membership_exp_cache[rel_rep] = tups;
-            } else if( std::find(d_membership_cache[rel_rep].begin(),
-                                 d_membership_cache[rel_rep].end(), tup_rep)
-                       == d_membership_cache[rel_rep].end() ) {
-              d_membership_cache[rel_rep].push_back(tup_rep);
+
+            // Todo: check n[0] or n[0] rep is a var??
+            if(tup_rep.isVar() && d_symbolic_tuples.find(tup_rep) == d_symbolic_tuples.end()) {
+              std::vector<Node> tuple_elements;
+              tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor()));
+              for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) {
+                tuple_elements.push_back(selectElement(n[0], i));
+              }
+              Node unfold_membership = MEMBER(NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements), n[1]);
+              Node tuple_unfold_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, unfold_membership);
+              sendLemma(tuple_unfold_lemma, d_trueNode, "tuple-unfold");
+              d_symbolic_tuples.insert(tup_rep);
+            }
+            computeTupleReps(tup_rep);
+            // Todo: Need to safe add trie
+            d_membership_trie[rel_rep].addTerm( tup_rep, d_tuple_reps[tup_rep]);
+
+            if(safeAddToMap(d_membership_cache, rel_rep, tup_rep)) {
+              addToMap(d_membership_db, rel_rep, tup_rep);
               Node exp = n;
               if(getRepresentative(r) == getRepresentative(d_falseNode))
                 exp = n.negate();
-              d_membership_exp_cache.at(rel_rep).push_back(exp);
+              addToMap(d_membership_exp_cache, rel_rep, exp);
             }
           }
         // collect term info
-        } else if( r.getType().isSet() ) {
+        } else if( r.getType().isSet() && r.getType().getSetElementType().isTuple() ) {
           if( n.getKind() == kind::TRANSPOSE ||
               n.getKind() == kind::JOIN ||
               n.getKind() == kind::PRODUCT ||
@@ -154,7 +158,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
                 terms.push_back(n);
                 rel_terms[n.getKind()] = terms;
               } else {
-                rel_terms.at(n.getKind()).push_back(n);
+                rel_terms[n.getKind()].push_back(n);
               }
             }
           }
@@ -166,7 +170,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     Trace("rels-debug") << "[sets-rels] Done with collecting relational terms!" << std::endl;
   }
 
- /*  join-split rule:    (a, b) IS_IN (X PRODUCT Y)
+ /*  product-split rule:    (a, b) IS_IN (X PRODUCT Y)
   *                  ----------------------------------
   *                       a IS_IN X  && b IS_IN Y
   *
@@ -176,60 +180,61 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
   */
 
   void TheorySetsRels::applyProductRule(Node exp, Node rel_rep, Node product_term) {
-    Trace("rels-debug") << "\n[sets-rels] Apply PRODUCT rule on term: " << product_term
-                        << " with explaination: " << exp << std::endl;
     bool polarity = exp.getKind() != kind::NOT;
     Node atom = polarity ? exp : exp[0];
     Node r1_rep = getRepresentative(product_term[0]);
     Node r2_rep = getRepresentative(product_term[1]);
 
     if(polarity) {
-      Node t1;
-      Node t2;
-      unsigned int s1_len = 1;
+      Trace("rels-debug") << "\n[sets-rels] Apply PRODUCT-SPLIT rule on term: " << product_term
+                          << " with explaination: " << exp << std::endl;
       std::vector<Node> r1_element;
       std::vector<Node> r2_element;
       Node::iterator child_it = atom[0].begin();
       NodeManager *nm = NodeManager::currentNM();
+      Datatype dt = r1_rep.getType().getSetElementType().getDatatype();
+      unsigned int s1_len = r1_rep.getType().getSetElementType().getTupleLength();
+
+      r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+      for(unsigned int i = 0; i < s1_len; ++child_it) {
+        r1_element.push_back(*child_it);
+        ++i;
+      }
+
+      dt = r2_rep.getType().getSetElementType().getDatatype();
+      r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+      for(; child_it != atom[0].end(); ++child_it) {
+        r2_element.push_back(*child_it);
+      }
 
-      if(r1_rep.getType().getSetElementType().isTuple()) {
-        Datatype dt = r1_rep.getType().getSetElementType().getDatatype();
-        s1_len = r1_rep.getType().getSetElementType().getTupleLength();
-        r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
-        for(unsigned int i = 0; i < s1_len; ++child_it) {
-          r1_element.push_back(*child_it);
-          ++i;
+      Node fact;
+      Node reason = exp;
+      Node t1 = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element));
+      Node t2 = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, r2_element));
+
+      if(!hasTuple(r1_rep, t1)) {
+        fact = MEMBER( t1, r1_rep );
+        if(r1_rep != product_term[0])
+          reason = Rewriter::rewrite(AND(reason, EQUAL(r1_rep, product_term[0])));
+        if(safeAddToMap(d_membership_db, r1_rep, t1)) {
+          addToMap(d_membership_exp_cache, r1_rep, reason);
         }
-        t1 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element);
-      } else {
-        t1 = *child_it;
-        ++child_it;
+        sendInfer(fact, reason, "product-split");
       }
 
-      if(r2_rep.getType().getSetElementType().isTuple()) {
-        Datatype dt = r2_rep.getType().getSetElementType().getDatatype();
-        r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
-        for(; child_it != atom[0].end(); ++child_it) {
-          r2_element.push_back(*child_it);
+      if(!hasTuple(r2_rep, t2)) {
+        fact = MEMBER( t2, r2_rep );
+        if(r2_rep != product_term[1])
+          reason = Rewriter::rewrite(AND(reason, EQUAL(r2_rep, product_term[1])));
+        if(safeAddToMap(d_membership_db, r2_rep, t2)) {
+          addToMap(d_membership_exp_cache, r2_rep, reason);
         }
-        t2 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r2_element);
-      } else {
-        t2 = *child_it;
+        sendInfer(fact, reason, "product-split");
       }
-      Node f1 = nm->mkNode(kind::MEMBER, t1, r1_rep);
-      Node f2 = nm->mkNode(kind::MEMBER, t2, r2_rep);
-      Node reason = exp;
-      if(atom[1] != product_term)
-        reason = AND(reason, EQUAL(atom[1], product_term));
-      if(r1_rep != product_term[0])
-        reason = AND(reason, EQUAL(r1_rep, product_term[0]));
-      if(r2_rep != product_term[1])
-        reason = Rewriter::rewrite(AND(reason, EQUAL(r2_rep, product_term[1])));
-
-      sendInfer(f1, reason, "product-split");
-      sendInfer(f2, reason, "product-split");
     } else {
       // ONLY need to explicitly compute joins if there are negative literals involving PRODUCT
+      Trace("rels-debug") << "\n[sets-rels] Apply PRODUCT-COMPOSE rule on term: " << product_term
+                          << " with explaination: " << exp << std::endl;
       computeRels(product_term);
     }
   }
@@ -244,107 +249,129 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
    *                                      (a, c) IS_IN (X JOIN Y)
    */
   void TheorySetsRels::applyJoinRule(Node exp, Node rel_rep, Node join_term) {
-    Trace("rels-debug") <<  "\n[sets-rels] Apply JOIN rule on term: " << join_term
-                        << " with explaination: " << exp << std::endl;
     bool polarity = exp.getKind() != kind::NOT;
     Node atom = polarity ? exp : exp[0];
     Node r1_rep = getRepresentative(join_term[0]);
     Node r2_rep = getRepresentative(join_term[1]);
 
     if(polarity) {
-      Node t1;
-      Node t2;
-      TypeNode shared_type;
-      unsigned int s1_len = 1;
+      Trace("rels-debug") <<  "\n[sets-rels] Apply JOIN-SPLIT rule on term: " << join_term
+                          << " with explaination: " << exp << std::endl;
+
       std::vector<Node> r1_element;
       std::vector<Node> r2_element;
       Node::iterator child_it = atom[0].begin();
       NodeManager *nm = NodeManager::currentNM();
+      TypeNode shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0];
+      Node shared_x = nm->mkSkolem("sde_", shared_type);
+      Datatype dt = r1_rep.getType().getSetElementType().getDatatype();
+      unsigned int s1_len = r1_rep.getType().getSetElementType().getTupleLength();
 
-      if(r2_rep.getType().getSetElementType().isTuple()) {
-        shared_type = r2_rep.getType().getSetElementType().getTupleTypes()[0];
-      } else {
-        shared_type = r2_rep.getType().getSetElementType();
+      r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+      for(unsigned int i = 0; i < s1_len-1; ++child_it, ++i) {
+        r1_element.push_back(*child_it);
       }
-
-      Node shared_x = nm->mkSkolem("sde_", shared_type);
-      if(r1_rep.getType().getSetElementType().isTuple()) {
-        Datatype dt = r1_rep.getType().getSetElementType().getDatatype();
-        s1_len = r1_rep.getType().getSetElementType().getTupleLength();
-        r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
-        for(unsigned int i = 0; i < s1_len-1; ++child_it) {
-          r1_element.push_back(*child_it);
-          ++i;
-        }
-        r1_element.push_back(shared_x);
-        t1 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element);
-      } else {
-        t1 = shared_x;
+      r1_element.push_back(shared_x);
+      dt = r2_rep.getType().getSetElementType().getDatatype();
+      r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+      r2_element.push_back(shared_x);
+      for(; child_it != atom[0].end(); ++child_it) {
+        r2_element.push_back(*child_it);
       }
 
-      if(r2_rep.getType().getSetElementType().isTuple()) {
-        Datatype dt = r2_rep.getType().getSetElementType().getDatatype();
-        r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
-        r2_element.push_back(shared_x);
-        for(; child_it != atom[0].end(); ++child_it) {
-          r2_element.push_back(*child_it);
+
+      Node t1 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element);
+      Node t2 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r2_element);
+      computeTupleReps(t1);
+      computeTupleReps(t2);
+      std::vector<Node> elements = d_membership_trie[r1_rep].existsTerm(d_tuple_reps[t1]);
+      if(elements.size() != 0) {
+        std::vector<Node> new_tup;
+        for(unsigned int j = 0; j < elements.size(); j++) {
+          new_tup.push_back(elements[j]);
+          new_tup.insert(new_tup.end(), d_tuple_reps[t2].begin(), d_tuple_reps[t2].end());
+          if(d_membership_trie[r2_rep].existsTerm(new_tup).size() != 0) {
+            return;
+          }
         }
-        t2 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element);
       } else {
-        t2 = shared_x;
+        Node fact;
+        Node reason = atom[1] == join_term ? exp : AND(exp, EQUAL(atom[1], join_term));
+        Node reasons;
+        fact = nm->mkNode(kind::MEMBER, t1, r1_rep);
+
+        if(r1_rep != join_term[0])
+          reasons = Rewriter::rewrite(AND(reason, EQUAL(r1_rep, join_term[0])));
+        addToMap(d_membership_db, r1_rep, t1);
+        addToMap(d_membership_exp_cache, r1_rep, reasons);
+        computeTupleReps(t1);
+        d_membership_trie[r1_rep].addTerm(t1, d_tuple_reps[t1]);
+        // Todo: need to safe add to trie
+        sendInfer(fact, reasons, "join-split");
+
+        fact = nm->mkNode(kind::MEMBER, t2, r2_rep);
+        if(r2_rep != join_term[1])
+          reasons = Rewriter::rewrite(AND(reason, EQUAL(r2_rep, join_term[1])));
+        addToMap(d_membership_db, r2_rep, t2);
+        addToMap(d_membership_exp_cache, r2_rep, t2);
+        computeTupleReps(t2);
+        d_membership_trie[r2_rep].addTerm(t2, d_tuple_reps[t2]);
+        //Todo: need to safe add to trie
+        sendInfer(fact, reasons, "join-split");
       }
-
-      Node f1 = nm->mkNode(kind::MEMBER, t1, r1_rep);
-      Node f2 = nm->mkNode(kind::MEMBER, t2, r2_rep);
-      Node reason = exp;
-      if(atom[1] != join_term)
-        reason = AND(reason, EQUAL(atom[1], join_term));
-      if(r1_rep != join_term[0])
-        reason = AND(reason, EQUAL(r1_rep, join_term[0]));
-      if(r2_rep != join_term[1])
-        reason = Rewriter::rewrite(AND(reason, EQUAL(r2_rep, join_term[1])));
-      sendInfer(f1, reason, "join-split");
-      sendInfer(f2, reason, "join-split");
     } else {
       // ONLY need to explicitly compute joins if there are negative literals involving JOIN
+      Trace("rels-debug") <<  "\n[sets-rels] Apply JOIN-COMPOSE rule on term: " << join_term
+                          << " with explaination: " << exp << std::endl;
       computeRels(join_term);
     }
   }
 
-  /* transpose rule: (a, b) IS_IN X   NOT (t, u) IS_IN (TRANSPOSE X)
+  /*
+   * transpose rule: (a, b) IS_IN X   NOT (t, u) IS_IN (TRANSPOSE X)
    *                ------------------------------------------------
    *                         (b, a) IS_IN (TRANSPOSE X)
+   *
+   * transpose rule:       [NOT] (a, b) IS_IN (TRANSPOSE X)
+   *                ------------------------------------------------
+   *                            [NOT] (b, a) IS_IN X
    */
   void TheorySetsRels::applyTransposeRule(Node exp, Node rel_rep, Node tp_term) {
     Trace("rels-debug") << "\n[sets-rels] Apply transpose rule on term: " << tp_term
                         << " with explaination: " << exp << std::endl;
     bool polarity = exp.getKind() != kind::NOT;
     Node atom = polarity ? exp : exp[0];
-    Node reversedTuple = reverseTuple(atom[0]);
-    Node reason = exp;
-
-    if(atom[1] != tp_term)
-      reason = AND(reason, EQUAL(rel_rep, tp_term));
-    Node fact = MEMBER(reversedTuple, tp_term[0]);
+    Node reversedTuple = getRepresentative(reverseTuple(atom[0]));
+    Node tp_t0_rep = getRepresentative(tp_term[0]);
+    Node reason = atom[1] == tp_term ? exp : Rewriter::rewrite(AND(exp, EQUAL(atom[1], tp_term)));
+    Node fact = MEMBER(reversedTuple, tp_t0_rep);
 
     if(!polarity) {
-      if(d_terms_cache[getRepresentative(fact[1])].find(kind::JOIN)
-         != d_terms_cache[getRepresentative(fact[1])].end()) {
-        std::vector<Node> join_terms = d_terms_cache[getRepresentative(fact[1])][kind::JOIN];
+      // tp_term is a nested term
+      if(d_terms_cache[tp_t0_rep].find(kind::JOIN)
+         != d_terms_cache[tp_t0_rep].end()) {
+        std::vector<Node> join_terms = d_terms_cache[tp_t0_rep][kind::JOIN];
         for(unsigned int i = 0; i < join_terms.size(); i++) {
           computeRels(join_terms[i]);
         }
       }
-      if(d_terms_cache[getRepresentative(fact[1])].find(kind::PRODUCT)
-         != d_terms_cache[getRepresentative(fact[1])].end()) {
-        std::vector<Node> product_terms = d_terms_cache[getRepresentative(fact[1])][kind::PRODUCT];
+      if(d_terms_cache[tp_t0_rep].find(kind::PRODUCT)
+         != d_terms_cache[tp_t0_rep].end()) {
+        std::vector<Node> product_terms = d_terms_cache[tp_t0_rep][kind::PRODUCT];
         for(unsigned int i = 0; i < product_terms.size(); i++) {
           computeRels(product_terms[i]);
         }
       }
       fact = fact.negate();
     }
-    sendInfer(fact, exp, "transpose-rule");
+    if(!holds(fact)) {
+      sendInfer(fact, reason, "transpose-rule");
+      if(polarity) {
+        if(safeAddToMap(d_membership_db, tp_t0_rep, reversedTuple)) {
+          addToMap(d_membership_exp_cache, tp_t0_rep, reversedTuple);
+        }
+      }
+    }
   }
 
   void TheorySetsRels::computeRels(Node n) {
@@ -373,20 +400,18 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
       break;
     }
 
-    if(d_membership_cache.find(getRepresentative(n[0])) == d_membership_cache.end() ||
-       d_membership_cache.find(getRepresentative(n[1])) == d_membership_cache.end())
+    if(d_membership_db.find(getRepresentative(n[0])) == d_membership_db.end() ||
+       d_membership_db.find(getRepresentative(n[1])) == d_membership_db.end())
           return;
     composeTuplesForRels(n);
   }
 
   void TheorySetsRels::computeTransposeRelations(Node n) {
     switch(n[0].getKind()) {
-    case kind::JOIN:
-      computeRels(n[0]);
-      break;
     case kind::TRANSPOSE:
       computeTransposeRelations(n[0]);
       break;
+    case kind::JOIN:
     case kind::PRODUCT:
       computeRels(n[0]);
       break;
@@ -394,30 +419,31 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
       break;
     }
 
-    if(d_membership_cache.find(getRepresentative(n[0])) == d_membership_cache.end())
+    if(d_membership_db.find(getRepresentative(n[0])) == d_membership_db.end())
       return;
     std::vector<Node> rev_tuples;
     std::vector<Node> rev_exps;
     Node n_rep = getRepresentative(n);
     Node n0_rep = getRepresentative(n[0]);
 
-    if(d_membership_cache.find(n_rep) != d_membership_cache.end()) {
-      rev_tuples = d_membership_cache[n_rep];
+    if(d_membership_db.find(n_rep) != d_membership_db.end()) {
+      rev_tuples = d_membership_db[n_rep];
       rev_exps = d_membership_exp_cache[n_rep];
     }
-    std::vector<Node> tuples = d_membership_cache[n0_rep];
+    std::vector<Node> tuples = d_membership_db[n0_rep];
     std::vector<Node> exps = d_membership_exp_cache[n0_rep];
     for(unsigned int i = 0; i < tuples.size(); i++) {
       // Todo: Need to consider duplicates
-      Node reason = exps[i];
-      Node rev_tup = reverseTuple(tuples[i]);
-      if(exps[i][1] != n0_rep)
-        reason = AND(reason, EQUAL(exps[i][1], n0_rep));
+      Node reason = exps[i][1] == n0_rep ? exps[i] : AND(exps[i], EQUAL(exps[i][1], n0_rep));
+      Node rev_tup = getRepresentative(reverseTuple(tuples[i]));
+      Node fact = MEMBER(rev_tup, n_rep);
+      if(holds(fact))
+        continue;
       rev_tuples.push_back(rev_tup);
       rev_exps.push_back(Rewriter::rewrite(reason));
-      sendInfer(MEMBER(rev_tup, n_rep), Rewriter::rewrite(reason), "transpose-rule");
+      sendInfer(fact, Rewriter::rewrite(reason), "transpose-rule");
     }
-    d_membership_cache[n_rep] = rev_tuples;
+    d_membership_db[n_rep] = rev_tuples;
     d_membership_exp_cache[n_rep] = rev_exps;
   }
 
@@ -435,98 +461,92 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     Trace("rels-debug") << "[sets-rels] start composing tuples in relations "
                         << r1 << " and " << r2 << std::endl;
 
-    if(d_membership_cache.find(r1_rep) == d_membership_cache.end() ||
-       d_membership_cache.find(r2_rep) == d_membership_cache.end())
+    if(d_membership_db.find(r1_rep) == d_membership_db.end() ||
+       d_membership_db.find(r2_rep) == d_membership_db.end())
     return;
 
     std::vector<Node> new_tups;
     std::vector<Node> new_exps;
-    std::vector<Node> r1_elements = d_membership_cache[r1_rep];
-    std::vector<Node> r2_elements = d_membership_cache[r2_rep];
+    std::vector<Node> r1_elements = d_membership_db[r1_rep];
+    std::vector<Node> r2_elements = d_membership_db[r2_rep];
     std::vector<Node> r1_exps = d_membership_exp_cache[r1_rep];
     std::vector<Node> r2_exps = d_membership_exp_cache[r2_rep];
-    Node new_rel = n.getKind() == kind::JOIN ? NodeManager::currentNM()->mkNode(kind::JOIN, r1_rep, r2_rep)
-                                             : NodeManager::currentNM()->mkNode(kind::PRODUCT, r1_rep, r2_rep);
+    Node new_rel = n.getKind() == kind::JOIN ? nm->mkNode(kind::JOIN, r1_rep, r2_rep)
+                                             : nm->mkNode(kind::PRODUCT, r1_rep, r2_rep);
+    Trace("rels-debug") << "[sets-rels] elements sizes: "
+                            << r1_elements.size() << " and " << r2_elements.size()
+                            << "  " << r1_elements[0] << " and " << r2_elements[0]<< std::endl;
+
     Node new_rel_rep = getRepresentative(new_rel);
-    unsigned int t1_len = 1;
-    unsigned int t2_len = 1;
-    if(r1_elements.front().getType().isTuple())
-      t1_len = r1_elements.front().getType().getTupleLength();
-    if(r2_elements.front().getType().isTuple())
-      t2_len = r2_elements.front().getType().getTupleLength();
+    unsigned int t1_len = r1_elements.front().getType().getTupleLength();
+    unsigned int t2_len = r2_elements.front().getType().getTupleLength();
+
     for(unsigned int i = 0; i < r1_elements.size(); i++) {
       for(unsigned int j = 0; j < r2_elements.size(); j++) {
-
-        std::vector<Node> composedTuple;
+        std::vector<Node> composed_tuple;
         TypeNode tn = n.getType().getSetElementType();
-        if(tn.isTuple()) {
-          composedTuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
-        }
-        Node r1_e = r1_elements[i];
-        Node r2_e = r2_elements[j];
-        if(r1_e.getType().isTuple())
-          r1_e = r1_elements[i][t1_len-1];
-        if(r2_e.getType().isTuple())
-          r2_e = r2_elements[j][0];
-
-        if((areEqual(r1_e, r2_e) && n.getKind() == kind::JOIN) ||
-           n.getKind() == kind::PRODUCT) {
+        Node r2_lmost = selectElement(r2_elements[j], 0);
+        Node r1_rmost = selectElement(r1_elements[i], t1_len-1);
+        composed_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
+        Trace("rels-debug") << "[sets-rels$$$$$$] r2_elements[j] = "<< r2_elements[j] << " is const? " << r2_elements[j].isConst()
+                            << " is Var? " << r2_elements[j].isVar()
+                            << " r1_element equal to r2_element? " << areEqual(r1_rmost, r2_lmost) << std::endl;
+        if((areEqual(r1_rmost, r2_lmost) && n.getKind() == kind::JOIN) ||
+            n.getKind() == kind::PRODUCT) {
           unsigned int k = 0;
           unsigned int l = 1;
           for(; k < t1_len - 1; ++k) {
-            composedTuple.push_back(r1_elements[i][k]);
+            composed_tuple.push_back(selectElement(r1_elements[i], k));
           }
           if(kind::PRODUCT == n.getKind()) {
-            composedTuple.push_back(r1_elements[i][k]);
-            composedTuple.push_back(r2_elements[j][0]);
+            composed_tuple.push_back(selectElement(r1_elements[i], k));
+            composed_tuple.push_back(selectElement(r2_elements[j], 0));
           }
           for(; l < t2_len; ++l) {
-            composedTuple.push_back(r2_elements[j][l]);
+            composed_tuple.push_back(selectElement(r2_elements[j], l));
           }
-          Node fact;
-          if(tn.isTuple()) {
-            fact = nm->mkNode(kind::APPLY_CONSTRUCTOR, composedTuple);
-          } else {
-            fact = composedTuple[0];
+          Node composed_tuple_node = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, composed_tuple));
+          Node fact = MEMBER(composed_tuple_node, new_rel_rep);
+          if(holds(fact)) {
+            Trace("rels-debug") << "New fact: " << fact << " already holds! Skip..." << std::endl;
+            continue;
           }
-          new_tups.push_back(fact);
-          fact = MEMBER(fact, new_rel_rep);
+
           std::vector<Node> reasons;
           reasons.push_back(r1_exps[i]);
           reasons.push_back(r2_exps[j]);
-
-          //Todo: think about how to deal with shared terms(?)
           if(n.getKind() == kind::JOIN)
-            reasons.push_back(EQUAL(r1_e, r2_e));
-
+            reasons.push_back(EQUAL(r1_rmost, r2_lmost));
           if(r1 != r1_rep) {
             reasons.push_back(EQUAL(r1, r1_rep));
           }
           if(r2 != r2_rep) {
             reasons.push_back(EQUAL(r2, r2_rep));
           }
-          Node reason = theory::Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, reasons));
-          new_exps.push_back(reason);
+          Node reason = Rewriter::rewrite(nm->mkNode(kind::AND, reasons));
+          if(safeAddToMap(d_membership_db, new_rel_rep, composed_tuple_node)) {
+            safeAddToMap(d_membership_exp_cache, new_rel_rep, reason);
+          }
           Trace("rels-debug") << "[sets-rels] compose tuples: " << r1_elements[i]
                              << " and " << r2_elements[j]
-                             << "\n new fact: " << fact
+                             << "\n Generate a new fact: " << fact
                              << "\n reason: " << reason<< std::endl;
           if(kind::JOIN == n.getKind())
-            sendInfer(fact, reason, "join-compose");
+            sendInfer( fact, reason, "join-compose" );
           else if(kind::PRODUCT == n.getKind())
             sendInfer( fact, reason, "product-compose" );
         }
       }
     }
 
-    if(d_membership_cache.find( new_rel_rep ) != d_membership_cache.end()) {
-      std::vector<Node> tups = d_membership_cache[new_rel_rep];
+    if(d_membership_db.find( new_rel_rep ) != d_membership_db.end()) {
+      std::vector<Node> tups = d_membership_db[new_rel_rep];
       std::vector<Node> exps = d_membership_exp_cache[new_rel_rep];
       // Todo: Need to take care of duplicate tuples
       tups.insert( tups.end(), new_tups.begin(), new_tups.end() );
       exps.insert( exps.end(), new_exps.begin(), new_exps.end() );
     } else {
-      d_membership_cache[new_rel_rep] = new_tups;
+      d_membership_db[new_rel_rep] = new_tups;
       d_membership_exp_cache[new_rel_rep] = new_exps;
     }
     Trace("rels-debug") << "[sets-rels] Done with joining tuples !" << std::endl;
@@ -535,43 +555,52 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
   void TheorySetsRels::doPendingLemmas() {
     if( !(*d_conflict) && (!d_lemma_cache.empty() || !d_pending_facts.empty())){
       for( unsigned i=0; i < d_lemma_cache.size(); i++ ){
-        Trace("rels-debug") << "[sets-rels] Process pending lemma : " << d_lemma_cache[i] << std::endl;
+        if(holds( d_lemma_cache[i] )) {
+          Trace("rels-lemma") << "[sets-rels-lemma-skip] Skip the already held lemma: "
+                              << d_lemma_cache[i]<< std::endl;
+          continue;
+        }
+        Trace("rels-lemma") << "[sets-rels-lemma] Process pending lemma : "
+                            << d_lemma_cache[i] << std::endl;
         d_sets.d_out->lemma( d_lemma_cache[i] );
       }
       for( std::map<Node, Node>::iterator child_it = d_pending_facts.begin();
            child_it != d_pending_facts.end(); child_it++ ) {
         if(holds(child_it->first)) {
-          Trace("rels-debug") << "[sets-rels] Skip the already processed fact,: " << child_it->first << std::endl;
+          Trace("rels-lemma") << "[sets-rels-fact-lemma-skip] Skip the already held fact,: "
+                              << child_it->first << std::endl;
           continue;
         }
-
-        Trace("rels-debug") << "[sets-rels] Process pending fact as lemma : " << child_it->first << std::endl;
+        Trace("rels-lemma") << "[sets-rels-fact-lemma] Process pending fact as lemma : "
+                            << child_it->first << std::endl;
         d_sets.d_out->lemma(child_it->first);
       }
     }
     d_pending_facts.clear();
+    d_membership_cache.clear();
+    d_membership_db.clear();
+    d_membership_exp_cache.clear();
+    d_terms_cache.clear();
     d_lemma_cache.clear();
+
   }
 
   void TheorySetsRels::sendSplit(Node a, Node b, const char * c) {
     Node eq = a.eqNode( b );
     Node neq = NOT( eq );
     Node lemma_or = OR( eq, neq );
-    Trace("rels-lemma") << "[sets-rels] Lemma " << c << " SPLIT : " << lemma_or << std::endl;
+    Trace("rels-lemma") << "[sets-lemma] Lemma " << c << " SPLIT : " << lemma_or << std::endl;
     d_lemma_cache.push_back( lemma_or );
   }
 
   void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) {
-    Trace("rels-lemma") << "[sets-rels] Infer " << conc << " from " << ant << " by " << c << std::endl;
+    Trace("rels-lemma") << "[sets-lemma] Infer " << conc << " from " << ant << " by " << c << std::endl;
     d_lemma_cache.push_back(conc);
+//    d_lemma.push_back(conc);
   }
 
   void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) {
-    Trace("rels-lemma") << "[sets-rels] Infer " << fact << " from " << exp << " by " << c << std::endl;
-    if( std::strcmp( c, "join-split" ) == 0 ) {
-      d_pending_split_facts[fact] = exp;
-      return;
-    }
+    Trace("rels-lemma") << "[sets-fact] Infer " << fact << " from " << exp << " by " << c << std::endl;
     d_pending_facts[fact] = exp;
     d_infer.push_back( fact );
     d_infer_exp.push_back( exp );
@@ -598,6 +627,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     }
     d_pending_facts.clear();
     d_membership_cache.clear();
+    d_membership_db.clear();
     d_membership_exp_cache.clear();
     d_terms_cache.clear();
   }
@@ -615,6 +645,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
           assertMembership(atom, exp, polarity);
         }
       } else {
+        Trace("rels-lemma") << "[sets-split-fact] Send " << fact << " from " << exp << std::endl;
         bool polarity = fact.getKind() != kind::NOT;
         Node atom = polarity ? fact : fact[0];
         assertMembership(atom, exp, polarity);
@@ -657,7 +688,11 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
   }
 
   bool TheorySetsRels::areEqual( Node a, Node b ){
+    Trace("rels-debug") << "[sets-rel] compare the equality of a = " << a
+                        << " and b = " << b << std::endl;
     if( hasTerm( a ) && hasTerm( b ) ){
+      Trace("rels-debug") << "[sets-rel] ********* has term a = " << a
+                              << " and b = " << b << std::endl;
 //      if( d_eqEngine->isTriggerTerm(a, THEORY_SETS) &&
 //          d_eqEngine->isTriggerTerm(b, THEORY_SETS) ) {
 //        // Get representative trigger terms
@@ -694,42 +729,83 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     }else if( a.isConst() && b.isConst() ){
       return a == b;
     }else {
-      Trace("rels-debug") << "to split a and b " << a << " " << b << std::endl;
-      Node x = NodeManager::currentNM()->mkSkolem( "sde", a.getType() );
-      Node y = NodeManager::currentNM()->mkSkolem( "sde", b.getType() );
-      Node set_a = NodeManager::currentNM()->mkNode( kind::SINGLETON, a );
-      Node set_b = NodeManager::currentNM()->mkNode( kind::SINGLETON, b );
-      Node dummy_lemma_1 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, set_a );
-      Node dummy_lemma_2 = NodeManager::currentNM()->mkNode( kind::MEMBER, y, set_b );
-      sendLemma( dummy_lemma_1, d_trueNode, "dummy-lemma" );
-      sendLemma( dummy_lemma_2, d_trueNode, "dummy-lemma" );
-      addSharedTerm(a);
-      addSharedTerm(b);
-//      sendSplit(a, b, "tuple-element-equality");
+      makeSharedTerm(a);
+      makeSharedTerm(b);
       return false;
     }
   }
 
-  void TheorySetsRels::addSharedTerm(TNode n) {
+  bool TheorySetsRels::safeAddToMap(std::map< Node, std::vector<Node> >& map, Node rel_rep, Node member) {
+    if(map.find(rel_rep) == map.end()) {
+      std::vector<Node> members;
+      members.push_back(member);
+      map[rel_rep] = members;
+      return true;
+    } else if(std::find(map[rel_rep].begin(), map[rel_rep].end(), member) == map[rel_rep].end()) {
+      map[rel_rep].push_back(member);
+      return true;
+    }
+    return false;
+  }
+
+  void TheorySetsRels::addToMap(std::map< Node, std::vector<Node> >& map, Node rel_rep, Node member) {
+    if(map.find(rel_rep) == map.end()) {
+      std::vector<Node> members;
+      members.push_back(member);
+      map[rel_rep] = members;
+    } else {
+      map[rel_rep].push_back(member);
+    }
+  }
+
+  inline Node TheorySetsRels::selectElement( Node tuple, int n_th ) {
+    if(tuple.isConst() || (!tuple.isVar() && !tuple.isConst()))
+      return tuple[n_th];
+    Datatype dt = tuple.getType().getDatatype();
+    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][n_th].getSelector(), tuple);
+  }
+
+  void TheorySetsRels::addSharedTerm( TNode n ) {
     Trace("rels-debug") << "[sets-rels] Add a shared term:  " << n << std::endl;
     d_sets.addSharedTerm(n);
     d_eqEngine->addTriggerTerm(n, THEORY_SETS);
   }
 
-  bool TheorySetsRels::exists( std::vector<Node>& v, Node n ){
-    return std::find(v.begin(), v.end(), n) != v.end();
+  bool TheorySetsRels::hasTuple( Node rel_rep, Node tuple ){
+    if(d_membership_db.find(rel_rep) == d_membership_db.end())
+      return false;
+    return std::find(d_membership_db[rel_rep].begin(),
+                     d_membership_db[rel_rep].end(), tuple) != d_membership_db[rel_rep].end();
+  }
+
+  void TheorySetsRels::makeSharedTerm( Node n ) {
+    if(d_shared_terms.find(n) == d_shared_terms.end()) {
+      Node skolem = NodeManager::currentNM()->mkSkolem( "sde", n.getType() );
+      sendLemma(MEMBER(skolem, SINGLETON(n)), d_trueNode, "share-term");
+      d_shared_terms.insert(n);
+    }
   }
 
+  // Todo: change this
   bool TheorySetsRels::holds(Node node) {
     bool polarity = node.getKind() != kind::NOT;
     Node atom = polarity ? node : node[0];
     Node polarity_atom = polarity ? d_trueNode : d_falseNode;
     Node atom_mod = NodeManager::currentNM()->mkNode(atom.getKind(), getRepresentative(atom[0]),
-                                                      getRepresentative(atom[1]) );
+                                                     getRepresentative(atom[1]) );
+    //Trace("rels-lemma-compare-element") << "[sets-rels*******] atom_mod = " << atom_mod << std::endl;
     d_eqEngine->addTerm(atom_mod);
     return areEqual(atom_mod, polarity_atom);
   }
 
+  void TheorySetsRels::computeTupleReps( Node n ) {
+    if( d_tuple_reps.find( n ) == d_tuple_reps.end() ){
+      for( unsigned i = 0; i < n.getNumChildren(); i++ ){
+        d_tuple_reps[n].push_back( getRepresentative( n[i] ) );
+      }
+    }
+  }
+
   TheorySetsRels::TheorySetsRels(context::Context* c,
                                  context::UserContext* u,
                                  eq::EqualityEngine* eq,
@@ -751,7 +827,56 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
 
   TheorySetsRels::~TheorySetsRels() {}
 
+  std::vector<Node> TupleTrie::existsTerm( std::vector< Node >& reps, int argIndex ) {
+    std::vector<Node> nodes;
+    if( argIndex==(int)reps.size() ){
+      if( d_data.empty() ){
+        return nodes;
+      }else{
+        nodes.push_back(d_data.begin()->first);
+        return nodes;
+      }
+    }else{
+//      std::map< TNode, TermArgTrie >::iterator it = d_data.find( reps[argIndex] );
+      std::map< Node, TupleTrie >::iterator it;
+      if(reps[argIndex].getKind() == kind::SKOLEM) {
+        it = d_data.begin();
+        while(it != d_data.end()) {
+          nodes.push_back(it->first);
+          it++;
+        }
+        return nodes;
+      }
+      it = d_data.find( reps[argIndex] );
+      if( it==d_data.end() ){
+        return nodes;
+      }else{
+        return it->second.existsTerm( reps, argIndex+1 );
+      }
+    }
+  }
+
+  bool TupleTrie::addTerm( Node n, std::vector< Node >& reps, int argIndex ){
+    if( argIndex==(int)reps.size() ){
+      if( d_data.empty() ){
+        //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
+        d_data[n].clear();
+        return true;
+      }else{
+        return false;
+      }
+    }else{
+      return d_data[reps[argIndex]].addTerm( n, reps, argIndex+1 );
+    }
+  }
 
+  void TupleTrie::debugPrint( const char * c, Node n, unsigned depth ) {
+    for( std::map< Node, TupleTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
+      for( unsigned i=0; i<depth; i++ ){ Debug(c) << "  "; }
+      Debug(c) << it->first << std::endl;
+      it->second.debugPrint( c, n, depth+1 );
+    }
+  }
 }
 }
 }
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index a63a0c253..b297a25d3 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -28,9 +28,22 @@ namespace sets {
 
 class TheorySets;
 
+
+class TupleTrie {
+public:
+  /** the data */
+  std::map< Node, TupleTrie > d_data;
+public:
+  std::vector<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 );
+  void clear() { d_data.clear(); }
+};/* class TupleTrie */
+
 class TheorySetsRels {
 
   typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
 public:
   TheorySetsRels(context::Context* c,
@@ -60,8 +73,14 @@ private:
   /** inferences: maintained to ensure ref count for internally introduced nodes */
   NodeList d_infer;
   NodeList d_infer_exp;
+//  NodeList d_lemma;
 
+  std::map< Node, std::vector<Node> > d_tuple_reps;
+  std::map< Node, TupleTrie > d_membership_trie;
+  std::hash_set< Node, NodeHashFunction > d_shared_terms;
+  std::hash_set< Node, NodeHashFunction > d_symbolic_tuples;
   std::map< Node, std::vector<Node> > d_membership_cache;
+  std::map< Node, std::vector<Node> > d_membership_db;
   std::map< Node, std::vector<Node> > d_membership_exp_cache;
   std::map< Node, std::map<kind::Kind_t, std::vector<Node> > > d_terms_cache;
 
@@ -87,14 +106,21 @@ private:
   void addSharedTerm( TNode n );
 
   // Helper functions
+  inline Node selectElement( Node, int);
+  bool safeAddToMap( std::map< Node, std::vector<Node> >&, Node, Node );
+  void addToMap( std::map< Node, std::vector<Node> >&, Node, Node );
+  bool hasTuple( Node, Node );
   Node getRepresentative( Node t );
   bool hasTerm( Node a );
   bool areEqual( Node a, Node b );
   bool exists( std::vector<Node>&, Node );
-  bool holds(Node);
+  bool holds( Node );
+  void computeTupleReps( Node );
+  void makeSharedTerm( Node );
 
 };
 
+
 }/* CVC4::theory::sets namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 6a606ef5c..0e80795ea 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -179,60 +179,28 @@ struct RelBinaryOperatorTypeRule {
       if(!firstRelType.isSet() || !secondRelType.isSet()) {
         throw TypeCheckingExceptionPrivate(n, " set operator operates on non-sets");
       }
-//      if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) {
-//        throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)");
-//      }
+      if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) {
+        throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)");
+      }
 
       std::vector<TypeNode> newTupleTypes;
-      TypeNode set_element_type_1 = firstRelType.getSetElementType();
-      TypeNode set_element_type_2 = secondRelType.getSetElementType();
-      std::vector<TypeNode> firstTupleTypes;
-      std::vector<TypeNode> secondTupleTypes;
+      std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes();
+      std::vector<TypeNode> secondTupleTypes = secondRelType[0].getTupleTypes();
 
       // JOIN is not allowed to apply on two unary sets
       if( n.getKind() == kind::JOIN ) {
-        if( !set_element_type_1.isTuple() && !set_element_type_2.isTuple()) {
+        if((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) {
           throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations");
-        } else if ( !set_element_type_1.isTuple() ) {
-          secondTupleTypes = set_element_type_2.getTupleTypes();
-          if(set_element_type_1 != secondTupleTypes.front()) {
-            throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations");
-          }
-          newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end());
-        } else if ( !set_element_type_2.isTuple() ) {
-          firstTupleTypes = set_element_type_1.getTupleTypes();
-          if(set_element_type_2 != firstTupleTypes.front()) {
-            throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations");
-          }
-          newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1);
-        } else {
-          firstTupleTypes = set_element_type_1.getTupleTypes();
-          secondTupleTypes = set_element_type_2.getTupleTypes();
-          if(firstTupleTypes.back() != secondTupleTypes.front()) {
-            throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations");
-          }
-          newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1);
-          newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end());
+        } else if(firstTupleTypes.back() != secondTupleTypes.front()) {
+          throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations");
         }
+        newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1);
+        newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end());
       }else if( n.getKind() == kind::PRODUCT ) {
-        if( !set_element_type_1.isTuple() ) {
-          firstTupleTypes.push_back(set_element_type_1);
-        } else {
-          firstTupleTypes = set_element_type_1.getTupleTypes();
-        }
-        if( !set_element_type_2.isTuple() ) {
-          secondTupleTypes.push_back(set_element_type_2);
-        } else {
-          secondTupleTypes = set_element_type_2.getTupleTypes();
-        }
         newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end());
         newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end());
       }
-      Assert(newTupleTypes.size() >= 1);
-      if(newTupleTypes.size() > 1)
-        resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
-      else
-        resultType = nodeManager->mkSetType(newTupleTypes[0]);
+      resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
     }
     return resultType;
   }
@@ -248,25 +216,16 @@ struct RelTransposeTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate, AssertionException) {
     Assert(n.getKind() == kind::TRANSPOSE);
-
-
     TypeNode setType = n[0].getType(check);
-    if(check && !setType.isSet()) {
+    if(check && !setType.isSet() && !setType.getSetElementType().isTuple()) {
         throw TypeCheckingExceptionPrivate(n, "relation transpose operats on non-relation");
     }
-    if(!setType.getSetElementType().isTuple())
-      return setType;
-
-    std::vector<TypeNode> tupleTypes;
-    std::vector<TypeNode> originalTupleTypes = setType[0].getTupleTypes();
-    for(std::vector<TypeNode>::reverse_iterator it = originalTupleTypes.rbegin(); it != originalTupleTypes.rend(); ++it) {
-      tupleTypes.push_back(*it);
-    }
+    std::vector<TypeNode> tupleTypes = setType[0].getTupleTypes();
+    std::reverse(tupleTypes.begin(), tupleTypes.end());
     return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes));
   }
 
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-      //Assert(n.getKind() == kind::TRANSCLOSURE);
       return false;
     }
 };/* struct RelTransposeTypeRule */
diff --git a/test/regress/regress0/sets/rels/rel_join_0_1.cvc b/test/regress/regress0/sets/rels/rel_join_0_1.cvc
index 70e35164a..a7fa7efb9 100644
--- a/test/regress/regress0/sets/rels/rel_join_0_1.cvc
+++ b/test/regress/regress0/sets/rels/rel_join_0_1.cvc
@@ -15,6 +15,7 @@ a : IntPair;
 ASSERT a = (1,5);
 
 ASSERT (1, 7) IS_IN x;
+ASSERT (4, 3) IS_IN x;
 ASSERT (7, 5) IS_IN y;
 
 ASSERT z IS_IN x;
diff --git a/test/regress/regress0/sets/rels/rel_symbolic_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_1.cvc
new file mode 100644
index 000000000..08ed32411
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_symbolic_1.cvc
@@ -0,0 +1,21 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+f : INT;
+d : IntPair;
+ASSERT d = (f,3);
+ASSERT d IS_IN y;
+e : IntPair;
+ASSERT e = (4, f);
+ASSERT e IS_IN x;
+
+a : IntPair;
+ASSERT a = (4,3);
+
+ASSERT r = (x JOIN y);
+
+ASSERT NOT (a IS_IN r);
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc
new file mode 100644
index 000000000..df2d7f412
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+d : IntPair;
+ASSERT d IS_IN y;
+
+a : IntPair;
+ASSERT a IS_IN x;
+
+e : IntPair;
+ASSERT e = (4,3);
+
+ASSERT r = (x JOIN y);
+
+ASSERT NOT (e IS_IN r);
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_1.cvc b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc
index dca0a3bfa..60b6edf58 100644
--- a/test/regress/regress0/sets/rels/rel_tp_join_1.cvc
+++ b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc
@@ -6,12 +6,20 @@ y : SET OF IntPair;
 z : SET OF IntPair;
 r : SET OF IntPair;
 
-ASSERT (1, 7) IS_IN x;
-ASSERT (2, 3) IS_IN x;
+b : IntPair;
+ASSERT b = (1,7);
+c : IntPair;
+ASSERT c = (2,3);
+ASSERT b IS_IN x;
+ASSERT c IS_IN x;
 
+d : IntPair;
+ASSERT d = (7,3);
+e : IntPair;
+ASSERT e = (4,7);
 
-ASSERT (7, 3) IS_IN y;
-ASSERT (4, 7) IS_IN y;
+ASSERT d IS_IN y;
+ASSERT e IS_IN y;
 
 ASSERT (3, 4) IS_IN z;
 
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc
new file mode 100644
index 000000000..54e16dd51
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc
@@ -0,0 +1,28 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+
+ASSERT x = {(1,7), (2,3)};
+
+d : IntPair;
+ASSERT d = (7,3);
+e : IntPair;
+ASSERT e = (4,7);
+
+ASSERT d IS_IN y;
+ASSERT e IS_IN y;
+
+ASSERT (3, 4) IS_IN z;
+
+a : IntPair;
+ASSERT a = (4,1);
+
+ASSERT r = ((x JOIN y) JOIN z);
+
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_int.cvc b/test/regress/regress0/sets/rels/rel_tp_join_int.cvc
new file mode 100644
index 000000000..8d149a48d
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_int.cvc
@@ -0,0 +1,26 @@
+% EXPECT: unsat
+% crash on this
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+w : SET OF IntPair;
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+t : INT;
+u : INT;
+
+ASSERT 4 < t AND t < 6;
+ASSERT 4 < u AND u < 6;
+
+ASSERT (1, u) IS_IN x;
+ASSERT (t, 3) IS_IN y;
+
+a : IntPair;
+ASSERT a = (1,3);
+
+ASSERT NOT (a IS_IN  (x JOIN y));
+
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_var.cvc b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc
index c7757bd3e..aacf6c054 100644
--- a/test/regress/regress0/sets/rels/rel_tp_join_var.cvc
+++ b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc
@@ -13,8 +13,8 @@ u : INT;
 ASSERT 4 < t AND t < 6;
 ASSERT 4 < u AND u < 6;
 
-ASSERT (1, u) IS_IN x;
-ASSERT (t, 3) IS_IN y;
+ASSERT (1, t) IS_IN x;
+ASSERT (u, 3) IS_IN y;
 
 a : IntPair;
 ASSERT a = (1,3);