From: PaulMeng <baolmeng@gmail.com>
Date: Wed, 9 Mar 2016 01:26:13 +0000 (-0600)
Subject: make skolems and tuple reduction terms as shared terms
X-Git-Tag: cvc5-1.0.0~6071
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7d9fe09b55eb7b9cf319594f163d1b57fc78c272;p=cvc5.git

make skolems and tuple reduction terms as shared terms

- added more benchmarks for pressure and theory combination tests
- fixed find terms method in trie data structure
- use a separate membership map to store positive membership terms
---

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 4530e3879..11667f850 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") << "\n[sets-rels] ************ Start the relational solver ************\n" << std::endl;
+    Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver *******************************\n" << std::endl;
     collectRelsInfo();
     check();
 //    doPendingFacts();
     doPendingLemmas();
     Assert(d_lemma_cache.empty());
     Assert(d_pending_facts.empty());
-    Trace("rels") << "\n[sets-rels] ************ Done with the relational solver ************\n" << std::endl;
+    Trace("rels") << "\n[sets-rels] ******************************* Done with the relational solver *******************************\n" << std::endl;
   }
 
   void TheorySetsRels::check() {
@@ -113,32 +113,37 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
           if(n.getKind() == kind::MEMBER && n[1].getType().getSetElementType().isTuple()) {
             Node tup_rep = getRepresentative(n[0]);
             Node rel_rep = getRepresentative(n[1]);
-
             // Todo: check n[0] or n[0]'s 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));
+            if(n[0].isVar()) {
+              if(d_symbolic_tuples.find(n[0]) == 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++) {
+                  Node element = selectElement(n[0], i);
+                  makeSharedTerm(element);
+                  tuple_elements.push_back(element);
+                }
+                Node concrete_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
+                concrete_tuple = MEMBER(concrete_tuple, n[1]);
+                Node concrete_tuple_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, concrete_tuple);
+                sendLemma(concrete_tuple_lemma, d_trueNode, "tuple-concretize");
+                d_symbolic_tuples.insert(n[0]);
+              }
+              // not put symbolic tuple var in the membership exp map if possible
+            } else {
+              if(safeAddToMap(d_membership_cache, rel_rep, tup_rep)) {
+                bool true_eq = areEqual(r, d_trueNode);
+                Node reason = true_eq ? n : n.negate();
+                if(true_eq && safeAddToMap(d_membership_db, rel_rep, tup_rep)) {
+                  computeTupleReps(n[0]);
+                  d_membership_trie[rel_rep].addTerm(n[0], d_tuple_reps[n[0]]);
+                  addToMap(d_membership_exp_db, rel_rep, reason);
+                }
+                addToMap(d_membership_exp_cache, rel_rep, reason);
               }
-              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-instantiate");
-              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();
-              addToMap(d_membership_exp_cache, rel_rep, exp);
             }
           }
-        // collect term info
+        // collect relational terms info
         } else if( r.getType().isSet() && r.getType().getSetElementType().isTuple() ) {
           if( n.getKind() == kind::TRANSPOSE ||
               n.getKind() == kind::JOIN ||
@@ -217,9 +222,8 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
         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);
-        }
+        addToMap(d_membership_db, r1_rep, t1);
+        addToMap(d_membership_exp_db, r1_rep, reason);
         sendInfer(fact, reason, "product-split");
       }
 
@@ -227,9 +231,8 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
         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);
-        }
+        addToMap(d_membership_db, r2_rep, t2);
+        addToMap(d_membership_exp_db, r2_rep, reason);
         sendInfer(fact, reason, "product-split");
       }
     } else {
@@ -286,41 +289,38 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
       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]);
+      d_membership_trie[r1_rep].debugPrint("rels-trie", r1_rep);
+      std::vector<Node> elements = d_membership_trie[r1_rep].findTerms(d_tuple_reps[t1]);
       if(elements.size() != 0) {
-        std::vector<Node> new_tup;
         for(unsigned int j = 0; j < elements.size(); j++) {
+          std::vector<Node> new_tup;
           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) {
+          new_tup.insert(new_tup.end(), d_tuple_reps[t2].begin()+1, d_tuple_reps[t2].end());
+          d_membership_trie[r2_rep].debugPrint("rels-trie", r2_rep);
+          if(d_membership_trie[r2_rep].existsTerm(new_tup) != Node::null()) {
             return;
           }
         }
-      } else {
-        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 fact;
+      Node reason = atom[1] == join_term ? exp : AND(exp, EQUAL(atom[1], join_term));
+      Node reasons = reason;
+
+      fact = MEMBER(t1, r1_rep);
+      if(r1_rep != join_term[0])
+        reasons = Rewriter::rewrite(AND(reason, EQUAL(r1_rep, join_term[0])));
+      produceNewMembership(r1_rep, t1, reasons);
+      sendInfer(fact, reasons, "join-split");
+
+      reasons = reason;
+      fact = MEMBER(t2, r2_rep);
+      if(r2_rep != join_term[1])
+        reasons = Rewriter::rewrite(AND(reason, EQUAL(r2_rep, join_term[1])));
+      produceNewMembership(r2_rep, t2, reasons);
+      sendInfer(fact, reasons, "join-split");
+
+      // Need to make the skolem "shared_x" as shared term
+      makeSharedTerm(shared_x);
     } 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
@@ -366,16 +366,17 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
       }
       fact = fact.negate();
     }
-    if(!holds(fact)) {
+    if(holds(fact)) {
+      Trace("rels-debug") << "[sets-rels] New fact: " << fact << " already holds. Skip...." << std::endl;
+    } else {
       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);
-        }
+        produceNewMembership(tp_t0_rep, reversedTuple, reason);
       }
     }
   }
 
+  // Bottom-up fashion to compute relations
   void TheorySetsRels::computeRels(Node n) {
     Trace("rels-debug") << "\n[sets-rels] computeJoinOrProductRelations for relation  " << n << std::endl;
     switch(n[0].getKind()) {
@@ -423,30 +424,23 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
 
     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_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_db[n0_rep];
-    std::vector<Node> exps = d_membership_exp_cache[n0_rep];
+    std::vector<Node> exps = d_membership_exp_db[n0_rep];
+    Assert(tuples.size() == exps.size());
     for(unsigned int i = 0; i < tuples.size(); i++) {
-      // Todo: Need to consider duplicates
       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(fact, Rewriter::rewrite(reason), "transpose-rule");
+      if(holds(fact)) {
+        Trace("rels-debug") << "[sets-rels] New fact: " << fact << " already holds! Skip..." << std::endl;
+      } else {
+        produceNewMembership(n_rep, rev_tup, Rewriter::rewrite(reason));
+        sendInfer(fact, Rewriter::rewrite(reason), "transpose-rule");
+      }
     }
-    d_membership_db[n_rep] = rev_tuples;
-    d_membership_exp_cache[n_rep] = rev_exps;
   }
 
   /*
@@ -471,8 +465,8 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     std::vector<Node> new_exps;
     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];
+    std::vector<Node> r1_exps = d_membership_exp_db[r1_rep];
+    std::vector<Node> r2_exps = d_membership_exp_db[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);
 
@@ -490,62 +484,52 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
 
         if((areEqual(r1_rmost, r2_lmost) && n.getKind() == kind::JOIN) ||
             n.getKind() == kind::PRODUCT) {
+          bool isProduct = n.getKind() == kind::PRODUCT;
           unsigned int k = 0;
           unsigned int l = 1;
           for(; k < t1_len - 1; ++k) {
             composed_tuple.push_back(selectElement(r1_elements[i], k));
           }
-          if(kind::PRODUCT == n.getKind()) {
+          if(isProduct) {
             composed_tuple.push_back(selectElement(r1_elements[i], k));
             composed_tuple.push_back(selectElement(r2_elements[j], 0));
           }
           for(; l < t2_len; ++l) {
             composed_tuple.push_back(selectElement(r2_elements[j], l));
           }
-          Node composed_tuple_node = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, composed_tuple));
-          Node fact = MEMBER(composed_tuple_node, new_rel_rep);
+          Node composed_tuple_rep = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, composed_tuple));
+          Node fact = MEMBER(composed_tuple_rep, new_rel_rep);
           if(holds(fact)) {
-            Trace("rels-debug") << "New fact: " << fact << " already holds! Skip..." << std::endl;
-            continue;
-          }
+            Trace("rels-debug") << "[sets-rels] New fact: " << fact << " already holds! Skip..." << std::endl;
+          } else {
+            std::vector<Node> reasons;
+            reasons.push_back(r1_exps[i]);
+            reasons.push_back(r2_exps[j]);
+            if(!isProduct)
+              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));
+            }
 
-          std::vector<Node> reasons;
-          reasons.push_back(r1_exps[i]);
-          reasons.push_back(r2_exps[j]);
-          if(n.getKind() == kind::JOIN)
-            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 = Rewriter::rewrite(nm->mkNode(kind::AND, reasons));
-          if(safeAddToMap(d_membership_db, new_rel_rep, composed_tuple_node)) {
-            addToMap(d_membership_exp_cache, new_rel_rep, reason);
+            Node reason = Rewriter::rewrite(nm->mkNode(kind::AND, reasons));
+            produceNewMembership(new_rel_rep, composed_tuple_rep, reason);
+
+            if(isProduct)
+              sendInfer( fact, reason, "product-compose" );
+            else
+              sendInfer( fact, reason, "join-compose" );
+
+            Trace("rels-debug") << "[sets-rels] Compose tuples: " << r1_elements[i]
+                               << " and " << r2_elements[j]
+                               << "\n            Produce a new fact: " << fact
+                               << "\n            Reason: " << reason<< std::endl;
           }
-          Trace("rels-debug") << "[sets-rels] compose tuples: " << r1_elements[i]
-                             << " and " << r2_elements[j]
-                             << "\n Generate a new fact: " << fact
-                             << "\n reason: " << reason<< std::endl;
-          if(kind::JOIN == n.getKind())
-            sendInfer( fact, reason, "join-compose" );
-          else if(kind::PRODUCT == n.getKind())
-            sendInfer( fact, reason, "product-compose" );
         }
       }
     }
-
-    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_db[new_rel_rep] = new_tups;
-      d_membership_exp_cache[new_rel_rep] = new_exps;
-    }
     Trace("rels-debug") << "[sets-rels] Done with composing tuples !" << std::endl;
   }
 
@@ -569,17 +553,20 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
           continue;
         }
         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);
+                            << child_it->first << " with reason " << child_it->second << std::endl;
+        // Todo: send facts as implications???
+        d_sets.d_out->lemma(NodeManager::currentNM()->mkNode(kind::IMPLIES, child_it->second, child_it->first));
       }
     }
     d_pending_facts.clear();
     d_membership_cache.clear();
-    d_membership_db.clear();
     d_membership_exp_cache.clear();
+    d_membership_db.clear();
+    d_membership_exp_db.clear();
     d_terms_cache.clear();
     d_lemma_cache.clear();
-
+    d_membership_trie.clear();
+    d_tuple_reps.clear();
   }
 
   void TheorySetsRels::sendSplit(Node a, Node b, const char * c) {
@@ -592,8 +579,9 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
 
   void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) {
     Trace("rels-lemma") << "[sets-lemma] Infer " << conc << " from " << ant << " by " << c << std::endl;
-    d_lemma_cache.push_back(conc);
-    d_lemma.push_back(conc);
+    Node lemma = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
+    d_lemma_cache.push_back(lemma);
+    d_lemma.push_back(lemma);
   }
 
   void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) {
@@ -659,11 +647,9 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     std::reverse( tuple_types.begin(), tuple_types.end() );
     TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types );
     Datatype dt = tn.getDatatype();
-
     elements.push_back( Node::fromExpr(dt[0].getConstructor() ) );
-    for(Node::iterator child_it = tuple.end()-1;
-        child_it != tuple.begin()-1; --child_it) {
-      elements.push_back( *child_it );
+    for(int i = tuple_types.size() - 1; i >= 0; --i) {
+      elements.push_back( selectElement(tuple, i) );
     }
     return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements );
   }
@@ -685,7 +671,11 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
   }
 
   bool TheorySetsRels::areEqual( Node a, Node b ){
-    if( hasTerm( a ) && hasTerm( b ) ){
+    if(a == b) {
+      return true;
+    } else if(a.isConst() && b.isConst()) {
+      return a == b;
+    } else if( hasTerm( a ) && hasTerm( b ) ){
 //      if( d_eqEngine->isTriggerTerm(a, THEORY_SETS) &&
 //          d_eqEngine->isTriggerTerm(b, THEORY_SETS) ) {
 //        // Get representative trigger terms
@@ -719,9 +709,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
 //          }
 //      }
       return d_eqEngine->areEqual( a, b );
-    }else if( a.isConst() && b.isConst() ){
-      return a == b;
-    }else {
+    } else {
       makeSharedTerm(a);
       makeSharedTerm(b);
       return false;
@@ -798,12 +786,19 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
 
   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] ) );
+      for( unsigned i = 0; i < n.getType().getTupleLength(); i++ ){
+        d_tuple_reps[n].push_back( getRepresentative( selectElement(n, i) ) );
       }
     }
   }
 
+  void TheorySetsRels::produceNewMembership(Node rel, Node member, Node reasons) {
+    addToMap(d_membership_db, rel, member);
+    addToMap(d_membership_exp_db, rel, reasons);
+    computeTupleReps(member);
+    d_membership_trie[rel].addTerm(member, d_tuple_reps[member]);
+  }
+
   TheorySetsRels::TheorySetsRels(context::Context* c,
                                  context::UserContext* u,
                                  eq::EqualityEngine* eq,
@@ -826,29 +821,39 @@ 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> TupleTrie::findTerms( 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;
+    std::map< Node, TupleTrie >::iterator it;
+    if( argIndex==(int)reps.size()-1 ){
       if(reps[argIndex].getKind() == kind::SKOLEM) {
         it = d_data.begin();
         while(it != d_data.end()) {
           nodes.push_back(it->first);
           it++;
         }
-        return nodes;
       }
+      return nodes;
+    }else{
       it = d_data.find( reps[argIndex] );
       if( it==d_data.end() ){
         return nodes;
+      }else{
+        return it->second.findTerms( reps, argIndex+1 );
+      }
+    }
+  }
+
+  Node TupleTrie::existsTerm( std::vector< Node >& reps, int argIndex ) {
+    if( argIndex==(int)reps.size() ){
+      if( d_data.empty() ){
+        return Node::null();
+      }else{
+        return d_data.begin()->first;
+      }
+    }else{
+      std::map< Node, TupleTrie >::iterator it = d_data.find( reps[argIndex] );
+      if( it==d_data.end() ){
+        return Node::null();
       }else{
         return it->second.existsTerm( reps, argIndex+1 );
       }
@@ -876,6 +881,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
       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 077e950e3..9b3678d01 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -34,7 +34,8 @@ public:
   /** the data */
   std::map< Node, TupleTrie > d_data;
 public:
-  std::vector<Node> existsTerm( std::vector< Node >& reps, int argIndex = 0 );
+  Node existsTerm( std::vector< Node >& reps, int argIndex = 0 );
+  std::vector<Node> findTerms( 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(); }
@@ -81,6 +82,7 @@ private:
   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_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;
 
@@ -117,6 +119,7 @@ private:
   bool holds( Node );
   void computeTupleReps( Node );
   void makeSharedTerm( Node );
+  inline void produceNewMembership( Node, Node, Node  );
 
 };
 
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 8b639a2e5..5c59d96ce 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -62,37 +62,37 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       bool isMember = checkConstantMembership(node[0], S);
       return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
     }
-    if(node[1].getKind() == kind::TRANSPOSE) {
-      // only work for node[0] is an actual tuple like (a, b), won't work for tuple variables
-      if(node[0].getType().isSet() && !node[0].getType().getSetElementType().isTuple()) {
-        Node atom = node;
-        bool polarity = node.getKind() != kind::NOT;
-        if( !polarity )
-          atom = atom[0];
-        Node new_node = NodeManager::currentNM()->mkNode(kind::MEMBER, atom[0], atom[1][0]);
-        if(!polarity)
-          new_node = new_node.negate();
-        return RewriteResponse(REWRITE_AGAIN, new_node);
-      }
-      if(node[0].isVar())
-        return RewriteResponse(REWRITE_DONE, node);
-      std::vector<Node> elements;
-      std::vector<TypeNode> tuple_types = node[0].getType().getTupleTypes();
-      std::reverse(tuple_types.begin(), tuple_types.end());
-      TypeNode tn = NodeManager::currentNM()->mkTupleType(tuple_types);
-      Datatype dt = tn.getDatatype();
-      elements.push_back(Node::fromExpr(dt[0].getConstructor()));
-      for(Node::iterator child_it = node[0].end()-1;
-                child_it != node[0].begin()-1; --child_it) {
-        elements.push_back(*child_it);
-      }
-      Node new_node = NodeManager::currentNM()->mkNode(kind::MEMBER,
-                                                       NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, elements),
-                                                       node[1][0]);
-      if(node.getKind() == kind::NOT)
-        new_node = NodeManager::currentNM()->mkNode(kind::NOT, new_node);
-      return RewriteResponse(REWRITE_AGAIN, new_node);
-    }
+//    if(node[1].getKind() == kind::TRANSPOSE) {
+//      // only work for node[0] is an actual tuple like (a, b), won't work for tuple variables
+//      if(node[0].getType().isSet() && !node[0].getType().getSetElementType().isTuple()) {
+//        Node atom = node;
+//        bool polarity = node.getKind() != kind::NOT;
+//        if( !polarity )
+//          atom = atom[0];
+//        Node new_node = NodeManager::currentNM()->mkNode(kind::MEMBER, atom[0], atom[1][0]);
+//        if(!polarity)
+//          new_node = new_node.negate();
+//        return RewriteResponse(REWRITE_AGAIN, new_node);
+//      }
+//      if(node[0].isVar())
+//        return RewriteResponse(REWRITE_DONE, node);
+//      std::vector<Node> elements;
+//      std::vector<TypeNode> tuple_types = node[0].getType().getTupleTypes();
+//      std::reverse(tuple_types.begin(), tuple_types.end());
+//      TypeNode tn = NodeManager::currentNM()->mkTupleType(tuple_types);
+//      Datatype dt = tn.getDatatype();
+//      elements.push_back(Node::fromExpr(dt[0].getConstructor()));
+//      for(Node::iterator child_it = node[0].end()-1;
+//                child_it != node[0].begin()-1; --child_it) {
+//        elements.push_back(*child_it);
+//      }
+//      Node new_node = NodeManager::currentNM()->mkNode(kind::MEMBER,
+//                                                       NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, elements),
+//                                                       node[1][0]);
+//      if(node.getKind() == kind::NOT)
+//        new_node = NodeManager::currentNM()->mkNode(kind::NOT, new_node);
+//      return RewriteResponse(REWRITE_AGAIN, new_node);
+//    }
     break;
   }//kind::MEMBER
 
diff --git a/test/regress/regress0/sets/rels/rel_1tup_0.cvc b/test/regress/regress0/sets/rels/rel_1tup_0.cvc
new file mode 100644
index 000000000..50d4defd5
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_1tup_0.cvc
@@ -0,0 +1,24 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntTup: TYPE = [INT];
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntTup;
+z: SET OF IntTup;
+
+b : IntPair;
+ASSERT b = (2, 1);
+ASSERT b IS_IN x;
+
+a : IntTup;
+ASSERT a = TUPLE(1);
+ASSERT a IS_IN y;
+
+c : IntTup;
+ASSERT c = TUPLE(2);
+
+ASSERT z = (x JOIN y);
+
+ASSERT NOT (c IS_IN z);
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/sets/rels/rel_complex_0.cvc b/test/regress/regress0/sets/rels/rel_complex_0.cvc
new file mode 100644
index 000000000..dcb753973
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_complex_0.cvc
@@ -0,0 +1,31 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+z : SET OF INT;
+f : INT;
+g : INT;
+
+e : IntPair;
+ASSERT e = (4, f);
+ASSERT e IS_IN x;
+
+d : IntPair;
+ASSERT d = (g,3);
+ASSERT d IS_IN y;
+
+
+ASSERT z = {f, g};
+ASSERT 0 = f - g;
+
+
+
+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_complex_1.cvc b/test/regress/regress0/sets/rels/rel_complex_1.cvc
new file mode 100644
index 000000000..969d0d71c
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_complex_1.cvc
@@ -0,0 +1,34 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+w : SET OF IntTup;
+z : SET OF IntTup;
+r2 : SET OF IntPair;
+
+a : IntPair;
+ASSERT a = (3,1);
+ASSERT a IS_IN x;
+
+d : IntPair;
+ASSERT d = (1,3);
+ASSERT d IS_IN y;
+
+e : IntPair;
+ASSERT e = (4,3);
+ASSERT r = (x JOIN y);
+
+ASSERT TUPLE(1) IS_IN w;
+ASSERT TUPLE(2) IS_IN z;
+ASSERT r2 = (w PRODUCT z);
+
+ASSERT NOT (e IS_IN r);
+%ASSERT e IS_IN r2;
+ASSERT (r <= r2);
+ASSERT NOT ((3,3) IS_IN r2);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_mix_0.cvc b/test/regress/regress0/sets/rels/rel_mix_0.cvc
new file mode 100644
index 000000000..723a9b2e2
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_mix_0.cvc
@@ -0,0 +1,30 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+w : SET OF IntTup;
+z : SET OF IntTup;
+r2 : SET OF IntPair;
+
+d : IntPair;
+ASSERT d = (1,3);
+ASSERT (1,3) IS_IN y;
+
+a : IntPair;
+ASSERT a IS_IN x;
+
+e : IntPair;
+ASSERT e = (4,3);
+
+ASSERT r = (x JOIN y);
+ASSERT r2 = (w PRODUCT z);
+
+ASSERT NOT (e IS_IN r);
+%ASSERT e IS_IN r2;
+ASSERT NOT (r = r2);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_pressure_0.cvc b/test/regress/regress0/sets/rels/rel_pressure_0.cvc
new file mode 100644
index 000000000..6cdf03600
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_pressure_0.cvc
@@ -0,0 +1,617 @@
+% 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;
+
+a11 : IntPair;
+ASSERT a11 = (1, 1);
+ASSERT a11 IS_IN x;
+a12 : IntPair;
+ASSERT a12 = (1, 2);
+ASSERT a12 IS_IN x;
+a13 : IntPair;
+ASSERT a13 = (1, 3);
+ASSERT a13 IS_IN x;
+a14 : IntPair;
+ASSERT a14 = (1, 4);
+ASSERT a14 IS_IN x;
+a15 : IntPair;
+ASSERT a15 = (1, 5);
+ASSERT a15 IS_IN x;
+a16 : IntPair;
+ASSERT a16 = (1, 6);
+ASSERT a16 IS_IN x;
+a17 : IntPair;
+ASSERT a17 = (1, 7);
+ASSERT a17 IS_IN x;
+a18 : IntPair;
+ASSERT a18 = (1, 8);
+ASSERT a18 IS_IN x;
+a19 : IntPair;
+ASSERT a19 = (1, 9);
+ASSERT a19 IS_IN x;
+a110 : IntPair;
+ASSERT a110 = (1, 10);
+ASSERT a110 IS_IN x;
+a21 : IntPair;
+ASSERT a21 = (2, 1);
+ASSERT a21 IS_IN x;
+a22 : IntPair;
+ASSERT a22 = (2, 2);
+ASSERT a22 IS_IN x;
+a23 : IntPair;
+ASSERT a23 = (2, 3);
+ASSERT a23 IS_IN x;
+a24 : IntPair;
+ASSERT a24 = (2, 4);
+ASSERT a24 IS_IN x;
+a25 : IntPair;
+ASSERT a25 = (2, 5);
+ASSERT a25 IS_IN x;
+a26 : IntPair;
+ASSERT a26 = (2, 6);
+ASSERT a26 IS_IN x;
+a27 : IntPair;
+ASSERT a27 = (2, 7);
+ASSERT a27 IS_IN x;
+a28 : IntPair;
+ASSERT a28 = (2, 8);
+ASSERT a28 IS_IN x;
+a29 : IntPair;
+ASSERT a29 = (2, 9);
+ASSERT a29 IS_IN x;
+a210 : IntPair;
+ASSERT a210 = (2, 10);
+ASSERT a210 IS_IN x;
+a31 : IntPair;
+ASSERT a31 = (3, 1);
+ASSERT a31 IS_IN x;
+a32 : IntPair;
+ASSERT a32 = (3, 2);
+ASSERT a32 IS_IN x;
+a33 : IntPair;
+ASSERT a33 = (3, 3);
+ASSERT a33 IS_IN x;
+a34 : IntPair;
+ASSERT a34 = (3, 4);
+ASSERT a34 IS_IN x;
+a35 : IntPair;
+ASSERT a35 = (3, 5);
+ASSERT a35 IS_IN x;
+a36 : IntPair;
+ASSERT a36 = (3, 6);
+ASSERT a36 IS_IN x;
+a37 : IntPair;
+ASSERT a37 = (3, 7);
+ASSERT a37 IS_IN x;
+a38 : IntPair;
+ASSERT a38 = (3, 8);
+ASSERT a38 IS_IN x;
+a39 : IntPair;
+ASSERT a39 = (3, 9);
+ASSERT a39 IS_IN x;
+a310 : IntPair;
+ASSERT a310 = (3, 10);
+ASSERT a310 IS_IN x;
+a41 : IntPair;
+ASSERT a41 = (4, 1);
+ASSERT a41 IS_IN x;
+a42 : IntPair;
+ASSERT a42 = (4, 2);
+ASSERT a42 IS_IN x;
+a43 : IntPair;
+ASSERT a43 = (4, 3);
+ASSERT a43 IS_IN x;
+a44 : IntPair;
+ASSERT a44 = (4, 4);
+ASSERT a44 IS_IN x;
+a45 : IntPair;
+ASSERT a45 = (4, 5);
+ASSERT a45 IS_IN x;
+a46 : IntPair;
+ASSERT a46 = (4, 6);
+ASSERT a46 IS_IN x;
+a47 : IntPair;
+ASSERT a47 = (4, 7);
+ASSERT a47 IS_IN x;
+a48 : IntPair;
+ASSERT a48 = (4, 8);
+ASSERT a48 IS_IN x;
+a49 : IntPair;
+ASSERT a49 = (4, 9);
+ASSERT a49 IS_IN x;
+a410 : IntPair;
+ASSERT a410 = (4, 10);
+ASSERT a410 IS_IN x;
+a51 : IntPair;
+ASSERT a51 = (5, 1);
+ASSERT a51 IS_IN x;
+a52 : IntPair;
+ASSERT a52 = (5, 2);
+ASSERT a52 IS_IN x;
+a53 : IntPair;
+ASSERT a53 = (5, 3);
+ASSERT a53 IS_IN x;
+a54 : IntPair;
+ASSERT a54 = (5, 4);
+ASSERT a54 IS_IN x;
+a55 : IntPair;
+ASSERT a55 = (5, 5);
+ASSERT a55 IS_IN x;
+a56 : IntPair;
+ASSERT a56 = (5, 6);
+ASSERT a56 IS_IN x;
+a57 : IntPair;
+ASSERT a57 = (5, 7);
+ASSERT a57 IS_IN x;
+a58 : IntPair;
+ASSERT a58 = (5, 8);
+ASSERT a58 IS_IN x;
+a59 : IntPair;
+ASSERT a59 = (5, 9);
+ASSERT a59 IS_IN x;
+a510 : IntPair;
+ASSERT a510 = (5, 10);
+ASSERT a510 IS_IN x;
+a61 : IntPair;
+ASSERT a61 = (6, 1);
+ASSERT a61 IS_IN x;
+a62 : IntPair;
+ASSERT a62 = (6, 2);
+ASSERT a62 IS_IN x;
+a63 : IntPair;
+ASSERT a63 = (6, 3);
+ASSERT a63 IS_IN x;
+a64 : IntPair;
+ASSERT a64 = (6, 4);
+ASSERT a64 IS_IN x;
+a65 : IntPair;
+ASSERT a65 = (6, 5);
+ASSERT a65 IS_IN x;
+a66 : IntPair;
+ASSERT a66 = (6, 6);
+ASSERT a66 IS_IN x;
+a67 : IntPair;
+ASSERT a67 = (6, 7);
+ASSERT a67 IS_IN x;
+a68 : IntPair;
+ASSERT a68 = (6, 8);
+ASSERT a68 IS_IN x;
+a69 : IntPair;
+ASSERT a69 = (6, 9);
+ASSERT a69 IS_IN x;
+a610 : IntPair;
+ASSERT a610 = (6, 10);
+ASSERT a610 IS_IN x;
+a71 : IntPair;
+ASSERT a71 = (7, 1);
+ASSERT a71 IS_IN x;
+a72 : IntPair;
+ASSERT a72 = (7, 2);
+ASSERT a72 IS_IN x;
+a73 : IntPair;
+ASSERT a73 = (7, 3);
+ASSERT a73 IS_IN x;
+a74 : IntPair;
+ASSERT a74 = (7, 4);
+ASSERT a74 IS_IN x;
+a75 : IntPair;
+ASSERT a75 = (7, 5);
+ASSERT a75 IS_IN x;
+a76 : IntPair;
+ASSERT a76 = (7, 6);
+ASSERT a76 IS_IN x;
+a77 : IntPair;
+ASSERT a77 = (7, 7);
+ASSERT a77 IS_IN x;
+a78 : IntPair;
+ASSERT a78 = (7, 8);
+ASSERT a78 IS_IN x;
+a79 : IntPair;
+ASSERT a79 = (7, 9);
+ASSERT a79 IS_IN x;
+a710 : IntPair;
+ASSERT a710 = (7, 10);
+ASSERT a710 IS_IN x;
+a81 : IntPair;
+ASSERT a81 = (8, 1);
+ASSERT a81 IS_IN x;
+a82 : IntPair;
+ASSERT a82 = (8, 2);
+ASSERT a82 IS_IN x;
+a83 : IntPair;
+ASSERT a83 = (8, 3);
+ASSERT a83 IS_IN x;
+a84 : IntPair;
+ASSERT a84 = (8, 4);
+ASSERT a84 IS_IN x;
+a85 : IntPair;
+ASSERT a85 = (8, 5);
+ASSERT a85 IS_IN x;
+a86 : IntPair;
+ASSERT a86 = (8, 6);
+ASSERT a86 IS_IN x;
+a87 : IntPair;
+ASSERT a87 = (8, 7);
+ASSERT a87 IS_IN x;
+a88 : IntPair;
+ASSERT a88 = (8, 8);
+ASSERT a88 IS_IN x;
+a89 : IntPair;
+ASSERT a89 = (8, 9);
+ASSERT a89 IS_IN x;
+a810 : IntPair;
+ASSERT a810 = (8, 10);
+ASSERT a810 IS_IN x;
+a91 : IntPair;
+ASSERT a91 = (9, 1);
+ASSERT a91 IS_IN x;
+a92 : IntPair;
+ASSERT a92 = (9, 2);
+ASSERT a92 IS_IN x;
+a93 : IntPair;
+ASSERT a93 = (9, 3);
+ASSERT a93 IS_IN x;
+a94 : IntPair;
+ASSERT a94 = (9, 4);
+ASSERT a94 IS_IN x;
+a95 : IntPair;
+ASSERT a95 = (9, 5);
+ASSERT a95 IS_IN x;
+a96 : IntPair;
+ASSERT a96 = (9, 6);
+ASSERT a96 IS_IN x;
+a97 : IntPair;
+ASSERT a97 = (9, 7);
+ASSERT a97 IS_IN x;
+a98 : IntPair;
+ASSERT a98 = (9, 8);
+ASSERT a98 IS_IN x;
+a99 : IntPair;
+ASSERT a99 = (9, 9);
+ASSERT a99 IS_IN x;
+a910 : IntPair;
+ASSERT a910 = (9, 10);
+ASSERT a910 IS_IN x;
+a101 : IntPair;
+ASSERT a101 = (10, 1);
+ASSERT a101 IS_IN x;
+a102 : IntPair;
+ASSERT a102 = (10, 2);
+ASSERT a102 IS_IN x;
+a103 : IntPair;
+ASSERT a103 = (10, 3);
+ASSERT a103 IS_IN x;
+a104 : IntPair;
+ASSERT a104 = (10, 4);
+ASSERT a104 IS_IN x;
+a105 : IntPair;
+ASSERT a105 = (10, 5);
+ASSERT a105 IS_IN x;
+a106 : IntPair;
+ASSERT a106 = (10, 6);
+ASSERT a106 IS_IN x;
+a107 : IntPair;
+ASSERT a107 = (10, 7);
+ASSERT a107 IS_IN x;
+a108 : IntPair;
+ASSERT a108 = (10, 8);
+ASSERT a108 IS_IN x;
+a109 : IntPair;
+ASSERT a109 = (10, 9);
+ASSERT a109 IS_IN x;
+a1010 : IntPair;
+ASSERT a1010 = (10, 10);
+ASSERT a1010 IS_IN x;
+b11 : IntPair;
+ASSERT b11 = (1, 1);
+ASSERT b11 IS_IN y;
+b12 : IntPair;
+ASSERT b12 = (1, 2);
+ASSERT b12 IS_IN y;
+b13 : IntPair;
+ASSERT b13 = (1, 3);
+ASSERT b13 IS_IN y;
+b14 : IntPair;
+ASSERT b14 = (1, 4);
+ASSERT b14 IS_IN y;
+b15 : IntPair;
+ASSERT b15 = (1, 5);
+ASSERT b15 IS_IN y;
+b16 : IntPair;
+ASSERT b16 = (1, 6);
+ASSERT b16 IS_IN y;
+b17 : IntPair;
+ASSERT b17 = (1, 7);
+ASSERT b17 IS_IN y;
+b18 : IntPair;
+ASSERT b18 = (1, 8);
+ASSERT b18 IS_IN y;
+b19 : IntPair;
+ASSERT b19 = (1, 9);
+ASSERT b19 IS_IN y;
+b110 : IntPair;
+ASSERT b110 = (1, 10);
+ASSERT b110 IS_IN y;
+b21 : IntPair;
+ASSERT b21 = (2, 1);
+ASSERT b21 IS_IN y;
+b22 : IntPair;
+ASSERT b22 = (2, 2);
+ASSERT b22 IS_IN y;
+b23 : IntPair;
+ASSERT b23 = (2, 3);
+ASSERT b23 IS_IN y;
+b24 : IntPair;
+ASSERT b24 = (2, 4);
+ASSERT b24 IS_IN y;
+b25 : IntPair;
+ASSERT b25 = (2, 5);
+ASSERT b25 IS_IN y;
+b26 : IntPair;
+ASSERT b26 = (2, 6);
+ASSERT b26 IS_IN y;
+b27 : IntPair;
+ASSERT b27 = (2, 7);
+ASSERT b27 IS_IN y;
+b28 : IntPair;
+ASSERT b28 = (2, 8);
+ASSERT b28 IS_IN y;
+b29 : IntPair;
+ASSERT b29 = (2, 9);
+ASSERT b29 IS_IN y;
+b210 : IntPair;
+ASSERT b210 = (2, 10);
+ASSERT b210 IS_IN y;
+b31 : IntPair;
+ASSERT b31 = (3, 1);
+ASSERT b31 IS_IN y;
+b32 : IntPair;
+ASSERT b32 = (3, 2);
+ASSERT b32 IS_IN y;
+b33 : IntPair;
+ASSERT b33 = (3, 3);
+ASSERT b33 IS_IN y;
+b34 : IntPair;
+ASSERT b34 = (3, 4);
+ASSERT b34 IS_IN y;
+b35 : IntPair;
+ASSERT b35 = (3, 5);
+ASSERT b35 IS_IN y;
+b36 : IntPair;
+ASSERT b36 = (3, 6);
+ASSERT b36 IS_IN y;
+b37 : IntPair;
+ASSERT b37 = (3, 7);
+ASSERT b37 IS_IN y;
+b38 : IntPair;
+ASSERT b38 = (3, 8);
+ASSERT b38 IS_IN y;
+b39 : IntPair;
+ASSERT b39 = (3, 9);
+ASSERT b39 IS_IN y;
+b310 : IntPair;
+ASSERT b310 = (3, 10);
+ASSERT b310 IS_IN y;
+b41 : IntPair;
+ASSERT b41 = (4, 1);
+ASSERT b41 IS_IN y;
+b42 : IntPair;
+ASSERT b42 = (4, 2);
+ASSERT b42 IS_IN y;
+b43 : IntPair;
+ASSERT b43 = (4, 3);
+ASSERT b43 IS_IN y;
+b44 : IntPair;
+ASSERT b44 = (4, 4);
+ASSERT b44 IS_IN y;
+b45 : IntPair;
+ASSERT b45 = (4, 5);
+ASSERT b45 IS_IN y;
+b46 : IntPair;
+ASSERT b46 = (4, 6);
+ASSERT b46 IS_IN y;
+b47 : IntPair;
+ASSERT b47 = (4, 7);
+ASSERT b47 IS_IN y;
+b48 : IntPair;
+ASSERT b48 = (4, 8);
+ASSERT b48 IS_IN y;
+b49 : IntPair;
+ASSERT b49 = (4, 9);
+ASSERT b49 IS_IN y;
+b410 : IntPair;
+ASSERT b410 = (4, 10);
+ASSERT b410 IS_IN y;
+b51 : IntPair;
+ASSERT b51 = (5, 1);
+ASSERT b51 IS_IN y;
+b52 : IntPair;
+ASSERT b52 = (5, 2);
+ASSERT b52 IS_IN y;
+b53 : IntPair;
+ASSERT b53 = (5, 3);
+ASSERT b53 IS_IN y;
+b54 : IntPair;
+ASSERT b54 = (5, 4);
+ASSERT b54 IS_IN y;
+b55 : IntPair;
+ASSERT b55 = (5, 5);
+ASSERT b55 IS_IN y;
+b56 : IntPair;
+ASSERT b56 = (5, 6);
+ASSERT b56 IS_IN y;
+b57 : IntPair;
+ASSERT b57 = (5, 7);
+ASSERT b57 IS_IN y;
+b58 : IntPair;
+ASSERT b58 = (5, 8);
+ASSERT b58 IS_IN y;
+b59 : IntPair;
+ASSERT b59 = (5, 9);
+ASSERT b59 IS_IN y;
+b510 : IntPair;
+ASSERT b510 = (5, 10);
+ASSERT b510 IS_IN y;
+b61 : IntPair;
+ASSERT b61 = (6, 1);
+ASSERT b61 IS_IN y;
+b62 : IntPair;
+ASSERT b62 = (6, 2);
+ASSERT b62 IS_IN y;
+b63 : IntPair;
+ASSERT b63 = (6, 3);
+ASSERT b63 IS_IN y;
+b64 : IntPair;
+ASSERT b64 = (6, 4);
+ASSERT b64 IS_IN y;
+b65 : IntPair;
+ASSERT b65 = (6, 5);
+ASSERT b65 IS_IN y;
+b66 : IntPair;
+ASSERT b66 = (6, 6);
+ASSERT b66 IS_IN y;
+b67 : IntPair;
+ASSERT b67 = (6, 7);
+ASSERT b67 IS_IN y;
+b68 : IntPair;
+ASSERT b68 = (6, 8);
+ASSERT b68 IS_IN y;
+b69 : IntPair;
+ASSERT b69 = (6, 9);
+ASSERT b69 IS_IN y;
+b610 : IntPair;
+ASSERT b610 = (6, 10);
+ASSERT b610 IS_IN y;
+b71 : IntPair;
+ASSERT b71 = (7, 1);
+ASSERT b71 IS_IN y;
+b72 : IntPair;
+ASSERT b72 = (7, 2);
+ASSERT b72 IS_IN y;
+b73 : IntPair;
+ASSERT b73 = (7, 3);
+ASSERT b73 IS_IN y;
+b74 : IntPair;
+ASSERT b74 = (7, 4);
+ASSERT b74 IS_IN y;
+b75 : IntPair;
+ASSERT b75 = (7, 5);
+ASSERT b75 IS_IN y;
+b76 : IntPair;
+ASSERT b76 = (7, 6);
+ASSERT b76 IS_IN y;
+b77 : IntPair;
+ASSERT b77 = (7, 7);
+ASSERT b77 IS_IN y;
+b78 : IntPair;
+ASSERT b78 = (7, 8);
+ASSERT b78 IS_IN y;
+b79 : IntPair;
+ASSERT b79 = (7, 9);
+ASSERT b79 IS_IN y;
+b710 : IntPair;
+ASSERT b710 = (7, 10);
+ASSERT b710 IS_IN y;
+b81 : IntPair;
+ASSERT b81 = (8, 1);
+ASSERT b81 IS_IN y;
+b82 : IntPair;
+ASSERT b82 = (8, 2);
+ASSERT b82 IS_IN y;
+b83 : IntPair;
+ASSERT b83 = (8, 3);
+ASSERT b83 IS_IN y;
+b84 : IntPair;
+ASSERT b84 = (8, 4);
+ASSERT b84 IS_IN y;
+b85 : IntPair;
+ASSERT b85 = (8, 5);
+ASSERT b85 IS_IN y;
+b86 : IntPair;
+ASSERT b86 = (8, 6);
+ASSERT b86 IS_IN y;
+b87 : IntPair;
+ASSERT b87 = (8, 7);
+ASSERT b87 IS_IN y;
+b88 : IntPair;
+ASSERT b88 = (8, 8);
+ASSERT b88 IS_IN y;
+b89 : IntPair;
+ASSERT b89 = (8, 9);
+ASSERT b89 IS_IN y;
+b810 : IntPair;
+ASSERT b810 = (8, 10);
+ASSERT b810 IS_IN y;
+b91 : IntPair;
+ASSERT b91 = (9, 1);
+ASSERT b91 IS_IN y;
+b92 : IntPair;
+ASSERT b92 = (9, 2);
+ASSERT b92 IS_IN y;
+b93 : IntPair;
+ASSERT b93 = (9, 3);
+ASSERT b93 IS_IN y;
+b94 : IntPair;
+ASSERT b94 = (9, 4);
+ASSERT b94 IS_IN y;
+b95 : IntPair;
+ASSERT b95 = (9, 5);
+ASSERT b95 IS_IN y;
+b96 : IntPair;
+ASSERT b96 = (9, 6);
+ASSERT b96 IS_IN y;
+b97 : IntPair;
+ASSERT b97 = (9, 7);
+ASSERT b97 IS_IN y;
+b98 : IntPair;
+ASSERT b98 = (9, 8);
+ASSERT b98 IS_IN y;
+b99 : IntPair;
+ASSERT b99 = (9, 9);
+ASSERT b99 IS_IN y;
+b910 : IntPair;
+ASSERT b910 = (9, 10);
+ASSERT b910 IS_IN y;
+b101 : IntPair;
+ASSERT b101 = (10, 1);
+ASSERT b101 IS_IN y;
+b102 : IntPair;
+ASSERT b102 = (10, 2);
+ASSERT b102 IS_IN y;
+b103 : IntPair;
+ASSERT b103 = (10, 3);
+ASSERT b103 IS_IN y;
+b104 : IntPair;
+ASSERT b104 = (10, 4);
+ASSERT b104 IS_IN y;
+b105 : IntPair;
+ASSERT b105 = (10, 5);
+ASSERT b105 IS_IN y;
+b106 : IntPair;
+ASSERT b106 = (10, 6);
+ASSERT b106 IS_IN y;
+b107 : IntPair;
+ASSERT b107 = (10, 7);
+ASSERT b107 IS_IN y;
+b108 : IntPair;
+ASSERT b108 = (10, 8);
+ASSERT b108 IS_IN y;
+b109 : IntPair;
+ASSERT b109 = (10, 9);
+ASSERT b109 IS_IN y;
+b1010 : IntPair;
+ASSERT b1010 = (10, 10);
+ASSERT b1010 IS_IN y;
+
+ASSERT (1, 9) IS_IN z;
+
+a : IntPair;
+ASSERT a = (9,1);
+ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc
new file mode 100644
index 000000000..082604dc2
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc
@@ -0,0 +1,21 @@
+% 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 = (1,3);
+ASSERT (1,3) 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_symbolic_3_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_3_1.cvc
new file mode 100644
index 000000000..b1720b50e
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_symbolic_3_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 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_transpose_5.cvc b/test/regress/regress0/sets/rels/rel_transpose_5.cvc
new file mode 100644
index 000000000..203e8b3d2
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_transpose_5.cvc
@@ -0,0 +1,22 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+ASSERT zt IS_IN y;
+
+w : IntPair;
+ASSERT w = (2, 2);
+ASSERT w IS_IN y;
+ASSERT z IS_IN x;
+
+ASSERT NOT (zt IS_IN (TRANSPOSE (x JOIN y)));
+
+CHECKSAT;