From: Paul Meng <baolmeng@gmail.com>
Date: Tue, 13 Sep 2016 16:05:25 +0000 (-0500)
Subject: refactored the code, added more benchmarks and minor fixes
X-Git-Tag: cvc5-1.0.0~6032
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=680e0d843eced443e9d484c441b895abb403d4e0;p=cvc5.git

refactored the code, added more benchmarks and minor fixes
---

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index b3b49493c..a1e6951cd 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -85,7 +85,8 @@ int TheorySetsRels::EqcInfo::counter        = 0;
           if(kind_terms.find(kind::JOIN) != kind_terms.end()) {
             std::vector<Node> join_terms = kind_terms[kind::JOIN];
             // exp is a membership term and join_terms contains all
-            // terms involving "join" operator that are in the same equivalence class with the right hand side of exp
+            // terms involving "join" operator that are in the same
+            // equivalence class with the right hand side of exp
             for(unsigned int j = 0; j < join_terms.size(); j++) {
               applyJoinRule(exp, join_terms[j]);
             }
@@ -258,7 +259,7 @@ int TheorySetsRels::EqcInfo::counter        = 0;
     TC_PAIR_IT tc_mem_it = d_tc_membership_db.find(tc_term);
 
     if( tc_mem_it != d_tc_membership_db.end() ) {
-      for(std::hash_set<Node>::iterator pair_it = tc_mem_it->second.begin();
+      for(std::hash_set<Node, NodeHashFunction>::iterator pair_it = tc_mem_it->second.begin();
           pair_it != tc_mem_it->second.end(); pair_it++) {
         Node            fst_rep         = getRepresentative(RelsUtils::nthElementOfTuple(*pair_it, 0));
         Node            snd_rep         = getRepresentative(RelsUtils::nthElementOfTuple(*pair_it, 1));
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index b785dba9c..f756930c4 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -158,6 +158,7 @@ private:
 
   /** Mapping between transitive closure TC(r)'s representative and TC(r) */
   std::map< Node, Node > d_tc_rep_term;
+  std::map< Node, EqcInfo* > d_eqc_info;
 
 public:
   void eqNotifyNewClass(Node t);
@@ -166,33 +167,36 @@ public:
 private:
 
   void doPendingMerge();
-  std::map< Node, EqcInfo* > d_eqc_info;
-  EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false );
-  void mergeTransposeEqcs(Node t1, Node t2);
-  void mergeProductEqcs(Node t1, Node t2);
-  void mergeTCEqcs(Node t1, Node t2);
-  void sendInferTranspose(bool, Node, Node, Node, bool reverseOnly = false);
-  void sendInferProduct(bool, Node, Node, Node);
-  void sendTCInference(EqcInfo* tc_ei, std::hash_set<int> in_reachable, std::hash_set<int> out_reachable, Node mem_rep, Node fst_rep, Node snd_rep, int id1, int id2);
-  void addTCMemAndSendInfer(EqcInfo* tc_ei, Node mem, Node exp, bool fromRel = false);
   Node findTCMemExp(EqcInfo*, Node);
-  void mergeTCEqcExp(EqcInfo*, EqcInfo*);
   void buildTCAndExp(Node, EqcInfo*);
+  void mergeTCEqcs(Node t1, Node t2);
+  void mergeTCEqcExp(EqcInfo*, EqcInfo*);
+  void mergeProductEqcs(Node t1, Node t2);
   int getOrMakeElementRepId(EqcInfo*, Node);
+  void mergeTransposeEqcs(Node t1, Node t2);
+  Node explainTCMem(EqcInfo*, Node, Node, Node);
+  void sendInferProduct(bool, Node, Node, Node);
+  EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false );
+  void sendInferTranspose(bool, Node, Node, Node, bool reverseOnly = false);
+  void addTCMemAndSendInfer(EqcInfo* tc_ei, Node mem, Node exp, bool fromRel = false);
   void collectInReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set<int>& in_reachable, bool firstRound  = true);
   void collectOutReachableNodes(EqcInfo* tc_ei, int start_id, std::hash_set<int>& out_reachable, bool firstRound  = true);
-  Node explainTCMem(EqcInfo*, Node, Node, Node);
+  void sendTCInference(EqcInfo* tc_ei, std::hash_set<int> in_reachable, std::hash_set<int> out_reachable, Node mem_rep, Node fst_rep, Node snd_rep, int id1, int id2);
+
 
 
   void check();
+  Node explain(Node);
   void collectRelsInfo();
-  void assertMembership( Node fact, Node reason, bool polarity );
-  void composeTupleMemForRel( Node );
-  void applyTransposeRule( Node, Node, bool tp_occur_rule = false );
+  void applyTCRule( Node, Node );
   void applyJoinRule( Node, Node );
   void applyProductRule( Node, Node );
-  void applyTCRule( Node, Node );
-  std::map< Node, std::hash_set< Node, NodeHashFunction > > constructTCGraph( Node, Node, Node );
+  void composeTupleMemForRel( Node );
+  void assertMembership( Node fact, Node reason, bool polarity );
+  void applyTransposeRule( Node, Node, bool tp_occur_rule = false );
+
+
+
   void computeMembersForRel( Node );
   void computeMembersForTpRel( Node );
   void finalizeTCInference();
@@ -201,35 +205,36 @@ private:
                 Node, Node, std::hash_set< Node, NodeHashFunction >&);
   void isTCReachable(Node fst, Node snd, std::hash_set<Node, NodeHashFunction>& hasSeen,
                       std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool&);
+  std::map< Node, std::hash_set< Node, NodeHashFunction > > constructTCGraph( Node, Node, Node );
 
-  Node explain(Node);
 
   void doTCLemmas();
+  void addSharedTerm( TNode n );
   void sendInfer( Node fact, Node exp, const char * c );
   void sendLemma( Node fact, Node reason, const char * c );
-  void addSharedTerm( TNode n );
   void checkTCGraphForConflict( Node, Node, Node, Node, Node, std::map< Node, std::hash_set< Node, NodeHashFunction > >& );
 
   // Helper functions
-  bool insertIntoIdList(IdList&, int);
-  inline Node getReason(Node tc_rep, Node tc_term, Node tc_r_rep, Node tc_r);
-  inline Node constructPair(Node tc_rep, Node a, Node b);
-  Node findMemExp(Node r, Node pair);
-  bool safelyAddToMap( std::map< Node, std::vector<Node> >&, Node, Node );
-  void addToMap( std::map< Node, std::vector<Node> >&, Node, Node );
-  bool hasMember( 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 );
-  void computeTupleReps( Node );
+  bool hasTerm( Node a );
   void makeSharedTerm( Node );
   void reduceTupleVar( Node );
-  inline void addToMembershipDB( Node, Node, Node  );
-  bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();}
+  bool hasMember( Node, Node );
+  void computeTupleReps( Node );
+  bool areEqual( Node a, Node b );
+  Node getRepresentative( Node t );
+  Node findMemExp(Node r, Node pair);
+  bool insertIntoIdList(IdList&, int);
+  bool exists( std::vector<Node>&, Node );
   Node mkAnd( std::vector< TNode >& assumptions );
+  inline void addToMembershipDB( Node, Node, Node  );
   void printNodeMap(char* fst, char* snd, NodeMap map);
+  inline Node constructPair(Node tc_rep, Node a, Node b);
+  void addToMap( std::map< Node, std::vector<Node> >&, Node, Node );
+  bool safelyAddToMap( std::map< Node, std::vector<Node> >&, Node, Node );
+  inline Node getReason(Node tc_rep, Node tc_term, Node tc_r_rep, Node tc_r);
+  bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();}
+
 
 };
 
diff --git a/test/regress/regress0/sets/rels/addr_book_0.cvc b/test/regress/regress0/sets/rels/addr_book_0.cvc
new file mode 100644
index 000000000..fbe782ab2
--- /dev/null
+++ b/test/regress/regress0/sets/rels/addr_book_0.cvc
@@ -0,0 +1,49 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom : TYPE;
+AtomTup : TYPE = [Atom];
+AtomBinTup : TYPE = [Atom, Atom];
+AtomTerTup : TYPE = [Atom, Atom, Atom];
+Target: SET OF AtomTup;
+
+Name: SET OF AtomTup;
+Addr: SET OF AtomTup;
+Book: SET OF AtomTup;
+names: SET OF AtomBinTup;
+addr: SET OF AtomTerTup;
+
+b1: Atom;
+b1_tup : AtomTup;
+ASSERT b1_tup = TUPLE(b1);
+ASSERT b1_tup IS_IN Book;
+
+b2: Atom;
+b2_tup : AtomTup;
+ASSERT b2_tup = TUPLE(b2);
+ASSERT b2_tup IS_IN Book;
+
+b3: Atom;
+b3_tup : AtomTup;
+ASSERT b3_tup = TUPLE(b3);
+ASSERT b3_tup IS_IN Book;
+
+n: Atom;
+n_tup : AtomTup;
+ASSERT n_tup = TUPLE(n);
+ASSERT n_tup IS_IN Name;
+
+t: Atom;
+t_tup : AtomTup;
+ASSERT t_tup = TUPLE(t);
+ASSERT t_tup IS_IN Target;
+
+ASSERT ((Book JOIN  addr) JOIN Target) = Name;
+ASSERT (Book JOIN names) = Name;
+ASSERT (Name & Addr) = {}::SET OF AtomTup;
+
+ASSERT ({n_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup;
+ASSERT ({n_tup} JOIN ({b2_tup} JOIN addr)) = ({n_tup} JOIN ({b1_tup} JOIN addr)) | {t_tup};
+ASSERT ({n_tup} JOIN ({b3_tup} JOIN addr)) = ({n_tup} JOIN ({b2_tup} JOIN addr)) - {t_tup};
+ASSERT NOT (({n_tup} JOIN ({b1_tup} JOIN addr)) = ({n_tup} JOIN ({b3_tup} JOIN addr)));
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/sets/rels/addr_book_1.cvc b/test/regress/regress0/sets/rels/addr_book_1.cvc
new file mode 100644
index 000000000..34176f274
--- /dev/null
+++ b/test/regress/regress0/sets/rels/addr_book_1.cvc
@@ -0,0 +1,45 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom : TYPE;
+AtomTup : TYPE = [Atom];
+AtomBinTup : TYPE = [Atom, Atom];
+AtomTerTup : TYPE = [Atom, Atom, Atom];
+Target: SET OF AtomTup;
+
+Name: SET OF AtomTup;
+Addr: SET OF AtomTup;
+Book: SET OF AtomTup;
+names: SET OF AtomBinTup;
+addr: SET OF AtomTerTup;
+
+b1: Atom;
+b1_tup : AtomTup;
+ASSERT b1_tup = TUPLE(b1);
+ASSERT b1_tup IS_IN Book;
+
+b2: Atom;
+b2_tup : AtomTup;
+ASSERT b2_tup = TUPLE(b2);
+ASSERT b2_tup IS_IN Book;
+
+b3: Atom;
+b3_tup : AtomTup;
+ASSERT b3_tup = TUPLE(b3);
+ASSERT b3_tup IS_IN Book;
+
+m: Atom;
+m_tup : AtomTup;
+ASSERT m_tup = TUPLE(m);
+ASSERT m_tup IS_IN Name;
+
+t: Atom;
+t_tup : AtomTup;
+ASSERT t_tup = TUPLE(t);
+ASSERT t_tup IS_IN Target;
+
+ASSERT ({m_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup;
+ASSERT ({b2_tup} JOIN addr) = ({b1_tup} JOIN addr) | {(m,t)};
+ASSERT ({b3_tup} JOIN addr) = ({b2_tup} JOIN addr) - {(m,t)};
+ASSERT NOT (({b1_tup} JOIN addr) = ({b3_tup} JOIN addr));
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/sets/rels/addr_book_1_1.cvc b/test/regress/regress0/sets/rels/addr_book_1_1.cvc
new file mode 100644
index 000000000..74e29eaee
--- /dev/null
+++ b/test/regress/regress0/sets/rels/addr_book_1_1.cvc
@@ -0,0 +1,45 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom : TYPE;
+AtomTup : TYPE = [Atom];
+AtomBinTup : TYPE = [Atom, Atom];
+AtomTerTup : TYPE = [Atom, Atom, Atom];
+Target: SET OF AtomTup;
+
+Name: SET OF AtomTup;
+Addr: SET OF AtomTup;
+Book: SET OF AtomTup;
+names: SET OF AtomBinTup;
+addr: SET OF AtomTerTup;
+
+b1: Atom;
+b1_tup : AtomTup;
+ASSERT b1_tup = TUPLE(b1);
+ASSERT b1_tup IS_IN Book;
+
+b2: Atom;
+b2_tup : AtomTup;
+ASSERT b2_tup = TUPLE(b2);
+ASSERT b2_tup IS_IN Book;
+
+b3: Atom;
+b3_tup : AtomTup;
+ASSERT b3_tup = TUPLE(b3);
+ASSERT b3_tup IS_IN Book;
+
+m: Atom;
+m_tup : AtomTup;
+ASSERT m_tup = TUPLE(m);
+ASSERT m_tup IS_IN Name;
+
+t: Atom;
+t_tup : AtomTup;
+ASSERT t_tup = TUPLE(t);
+ASSERT t_tup IS_IN Target;
+
+ASSERT ({m_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup;
+ASSERT ({b2_tup} JOIN addr) = ({b1_tup} JOIN addr) | {(m,t)};
+ASSERT ({b3_tup} JOIN addr) = ({b2_tup} JOIN addr) - {(m,t)};
+ASSERT (({b1_tup} JOIN addr) = ({b3_tup} JOIN addr));
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/sets/rels/tobesolved/garbage_collect.cvc b/test/regress/regress0/sets/rels/tobesolved/garbage_collect.cvc
new file mode 100644
index 000000000..dd5995c42
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/garbage_collect.cvc
@@ -0,0 +1,59 @@
+H_TYPE: TYPE;
+H: TYPE = [H_TYPE];
+Obj: TYPE;
+Obj_Tup: TYPE = [Obj];
+MARK_TYPE: TYPE = [H_TYPE, Obj];
+RELATE: TYPE = [Obj, Obj];
+REF_TYPE: TYPE = [H_TYPE, Obj, Obj];
+
+% Symbols h0 to h3 are constants of type H that represents the system state;
+h0: SET OF H;
+h1: SET OF H;
+h2: SET OF H;
+h3: SET OF H;
+s0: H_TYPE;
+s1: H_TYPE;
+s2: H_TYPE;
+s3: H_TYPE;
+ASSERT h0 = {TUPLE(s0)};
+ASSERT h1 = {TUPLE(s1)};
+ASSERT h2 = {TUPLE(s2)};
+ASSERT h3 = {TUPLE(s3)};
+
+% ref ⊆ H × Obj × Obj represents references between objects in each state;
+ref : SET OF REF_TYPE;
+
+% mark ⊆ H × Obj represents the marked objects in each state
+mark: SET OF MARK_TYPE;
+
+empty_obj_set: SET OF Obj_Tup;
+ASSERT empty_obj_set = {}:: SET OF Obj_Tup;
+
+% root and live are two constants of type Obj that represents objects;
+root: Obj;
+live: Obj;
+
+% The state transition (h0–h1) resets all the marks
+ASSERT (h1 JOIN mark) = empty_obj_set;
+ASSERT (h0 JOIN ref) <= (h1 JOIN ref);
+
+% (h1–h2) marks objects reachable from root
+ASSERT FORALL (n : Obj) : ((root, n) IS_IN TCLOSURE(h1 JOIN ref)) 
+										  => (TUPLE(n) IS_IN (h2 JOIN mark));
+ASSERT (h1 JOIN ref) <= (h2 JOIN ref);
+
+% (h2–h3) sweeps references of non-marked objects										  
+
+ASSERT FORALL (n: Obj) : (NOT (TUPLE(n) IS_IN (h2 JOIN mark))) 
+										  => ({TUPLE(n)} JOIN (h3 JOIN ref)) = empty_obj_set;										  
+
+ASSERT FORALL (n: Obj) : (TUPLE(n) IS_IN (h2 JOIN mark))
+										  => ({TUPLE(n)} JOIN (h3 JOIN ref)) = ({TUPLE(n)} JOIN (h2 JOIN ref));	
+
+%The safety property is negated, thus it checks if
+%in the final state, there is a live object that was originally reachable from root
+%in the beginning state, but some of its references have been swept 										  
+ASSERT (root, live) IS_IN TCLOSURE(h0 JOIN ref);
+ASSERT NOT (({TUPLE(live)} JOIN (h0 JOIN ref)) <= ({TUPLE(live)} JOIN (h3 JOIN ref)));										  
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_1tup_syntax.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_1tup_syntax.cvc
new file mode 100644
index 000000000..0b4a13d09
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_1tup_syntax.cvc
@@ -0,0 +1,24 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntTup: TYPE = [INT];
+IntPair: TYPE = [INT, INT];
+x : SET OF IntTup;
+y : SET OF IntTup;
+z: SET OF IntTup;
+
+b : IntTup;
+ASSERT b = TUPLE(2);
+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/tobesolved/rel_complex_2.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_complex_2.cvc
new file mode 100644
index 000000000..5dfe957ca
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_complex_2.cvc
@@ -0,0 +1,34 @@
+% 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;
+
+
+f : IntPair;
+ASSERT f = (3,1);
+ASSERT f IS_IN x;
+
+g : IntPair;
+ASSERT g = (1,3);
+ASSERT g IS_IN y;
+
+h : IntPair;
+ASSERT h = (4,3);
+ASSERT h IS_IN x;
+ASSERT h IS_IN y;
+
+ASSERT r = (x JOIN y);
+
+e : IntPair;
+
+ASSERT r = (x | y);
+ASSERT NOT(z = (x & y));
+ASSERT z = (x - y);
+ASSERT x <= y;
+ASSERT e IS_IN (z JOIN x);
+ASSERT e IS_IN x;
+ASSERT e IS_IN (x & y);
+CHECKSAT TRUE;
\ No newline at end of file
diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_complex_4.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_complex_4.cvc
new file mode 100644
index 000000000..60e39a5b2
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_complex_4.cvc
@@ -0,0 +1,652 @@
+% 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;
+w : 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;
+
+f : IntPair;
+ASSERT f = (3,1);
+ASSERT f IS_IN x;
+
+g : IntPair;
+ASSERT g = (1,3);
+ASSERT g IS_IN y;
+
+h : IntPair;
+ASSERT h = (3,5);
+ASSERT h IS_IN x;
+ASSERT h IS_IN y;
+
+ASSERT r = (x JOIN y);
+a:INT;
+e : IntPair;
+ASSERT e = (a,a);
+ASSERT w = {e};
+ASSERT TRANSPOSE(w) <= y;
+
+ASSERT NOT (e IS_IN r);
+ASSERT NOT(z = (x & y));
+ASSERT z = (x - y);
+ASSERT x <= y;
+ASSERT e IS_IN (r JOIN z);
+ASSERT e IS_IN x;
+ASSERT e IS_IN (x & y);
+CHECKSAT TRUE;
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_join_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_0.cvc
new file mode 100644
index 000000000..034eebd22
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_join_0.cvc
@@ -0,0 +1,18 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+
+ASSERT (1, 2) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN z;
+
+ASSERT ((1, 1) IS_IN (x JOIN x));
+
+%ASSERT y = (x JOIN x);
+
+ASSERT (NOT (1,4) IS_IN ((x JOIN x) JOIN z));
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_join_com.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_com.cvc
new file mode 100644
index 000000000..5fce37ef4
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_join_com.cvc
@@ -0,0 +1,13 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+a: INT;
+b: INT;
+
+ASSERT (1, b) IS_IN x;
+ASSERT (a, 3) IS_IN y;
+
+ASSERT NOT ((1,3) IS_IN (x JOIN y));
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_0.cvc
new file mode 100644
index 000000000..ca6369087
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_0.cvc
@@ -0,0 +1,35 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT];
+w : SET OF IntPair;
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+
+r : SET OF IntPair;
+r2 : SET OF IntPair;
+
+d : IntPair;
+ASSERT d = (3,1);
+ASSERT (1,3) IS_IN y;
+ASSERT d IS_IN y;
+
+ASSERT (3,1) IS_IN y;
+ASSERT (4,1) IS_IN y;
+ASSERT (1,3) IS_IN z;
+
+a : IntPair;
+ASSERT a IS_IN x;
+
+e : IntPair;
+ASSERT e = (4,3);
+ASSERT e IS_IN x;
+
+ASSERT r = (x JOIN y);
+ASSERT r2 = (y JOIN z);
+ASSERT (1,3) IS_IN r;
+ASSERT r = r2;
+ASSERT NOT (e IS_IN r);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_1.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_1.cvc
new file mode 100644
index 000000000..32d529df3
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_1.cvc
@@ -0,0 +1,31 @@
+% EXPECT: sat
+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;
+r2 : SET OF IntPair;
+
+d : IntPair;
+ASSERT d = (3,1);
+ASSERT (1,3) IS_IN y;
+ASSERT d IS_IN y;
+
+ASSERT (3,1) IS_IN y;
+ASSERT (4,1) IS_IN y;
+ASSERT (1,3) IS_IN z;
+
+a : IntPair;
+ASSERT a IS_IN x;
+
+e : IntPair;
+ASSERT e = (4,3);
+ASSERT e IS_IN x;
+
+ASSERT y = ((x JOIN y) JOIN z);
+
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_pt_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_pt_0.cvc
new file mode 100644
index 000000000..7257d5a0d
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_pt_0.cvc
@@ -0,0 +1,25 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+w : SET OF IntTup;
+
+z : IntPair;
+ASSERT z = (1,3);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntTup;
+ASSERT v = (1,2,2,1);
+
+ASSERT zt IS_IN y;
+ASSERT v IS_IN (x PRODUCT y);
+ASSERT (4, 4, 5, 5) IS_IN w;
+ASSERT  z IS_IN x;
+
+ASSERT w = (x PRODUCT y);
+ASSERT NOT (4,4) IS_IN x;
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tc_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tc_0.cvc
new file mode 100644
index 000000000..0a2ec79be
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_tc_0.cvc
@@ -0,0 +1,23 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+a : IntPair;
+ASSERT a = (1,2);
+b : IntPair;
+ASSERT b = (2,1);
+c: IntPair;
+ASSERT c = (1,1);
+d : IntPair;
+ASSERT d = (1,5);
+
+ASSERT a IS_IN x;
+ASSERT b IS_IN x;
+ASSERT c IS_IN x;
+ASSERT d IS_IN x;
+ASSERT y = (TCLOSURE x);
+ASSERT NOT ((1, 1) IS_IN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tc_1.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tc_1.cvc
new file mode 100644
index 000000000..b8ab773b1
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_tc_1.cvc
@@ -0,0 +1,19 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+e: INT;
+a : IntPair;
+ASSERT a = (1,e);
+b : IntPair;
+ASSERT b = (e,1);
+
+
+ASSERT a IS_IN x;
+ASSERT b IS_IN x;
+
+ASSERT y = (TCLOSURE x);
+ASSERT NOT ((1, 1) IS_IN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tp_3.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tp_3.cvc
new file mode 100644
index 000000000..f074011ce
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_tp_3.cvc
@@ -0,0 +1,14 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z: SET OF IntPair;
+
+ASSERT (1, 3) IS_IN x;
+ASSERT ((2,3) IS_IN z OR (2,1) IS_IN z);
+ASSERT y = (TRANSPOSE x);
+ASSERT NOT (1,2) IS_IN y;
+ASSERT NOT (3,2) IS_IN y;
+ASSERT x = z;
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tp_4.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tp_4.cvc
new file mode 100644
index 000000000..183be8d9b
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/rel_tp_4.cvc
@@ -0,0 +1,10 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+ASSERT (2, 2) IS_IN (TCLOSURE x);
+ASSERT NOT (2,1) IS_IN x;
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/tobesolved/test.cvc b/test/regress/regress0/sets/rels/tobesolved/test.cvc
new file mode 100644
index 000000000..aa4e17eab
--- /dev/null
+++ b/test/regress/regress0/sets/rels/tobesolved/test.cvc
@@ -0,0 +1,11 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+ASSERT (y JOIN x) = x;
+
+ASSERT (1,2) IS_IN x;
+
+CHECKSAT;