Added more benchmarks

Fixed the problem that duplicates and split facts were sent as lemmas
causing nontermination
Fixed the computation of join and product relations without simplication

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index de70e6a52b663517bb809e9af79630695a5e4a78..2b35fb077e8caf37440217822b69bb5fb5b6b7f1 100644 (file)
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -43,7 +43,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     Trace("rels-debug") << "[sets-rels] Start the relational solver..." << std::endl;
     collectRelationalInfo();
     check();
-//    doPendingFacts();
+    doPendingSplitFacts();
     doPendingLemmas();
     Assert(d_lemma_cache.empty());
     Assert(d_pending_facts.empty());
@@ -189,6 +189,28 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     d_terms_cache.clear();
   }
 
+  void TheorySetsRels::doPendingSplitFacts() {
+      std::map<Node, Node>::iterator map_it = d_pending_split_facts.begin();
+      while( !(*d_conflict) && map_it != d_pending_split_facts.end()) {
+
+        Node fact = map_it->first;
+        Node exp = d_pending_split_facts[ fact ];
+        if(fact.getKind() == kind::AND) {
+          for(size_t j=0; j<fact.getNumChildren(); j++) {
+            bool polarity = fact[j].getKind() != kind::NOT;
+            Node atom = polarity ? fact[j] : fact[j][0];
+            assertMembership(atom, exp, polarity);
+          }
+        } else {
+          bool polarity = fact.getKind() != kind::NOT;
+          Node atom = polarity ? fact : fact[0];
+          assertMembership(atom, exp, polarity);
+        }
+        map_it++;
+      }
+      d_pending_split_facts.clear();
+    }
+
   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;
@@ -266,11 +288,17 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     if(!polarity) {
       if(d_terms_cache[getRepresentative(fact[1])].find(kind::JOIN)
          != d_terms_cache[getRepresentative(fact[1])].end()) {
-        computeJoinOrProductRelations(fact[1]);
+        std::vector<Node> join_terms = d_terms_cache[getRepresentative(fact[1])][kind::JOIN];
+        for(unsigned int i = 0; i < join_terms.size(); i++) {
+          computeJoinOrProductRelations(join_terms[i]);
+        }
       }
       if(d_terms_cache[getRepresentative(fact[1])].find(kind::PRODUCT)
          != d_terms_cache[getRepresentative(fact[1])].end()) {
-        computeJoinOrProductRelations(fact[1]);
+        std::vector<Node> product_terms = d_terms_cache[getRepresentative(fact[1])][kind::PRODUCT];
+        for(unsigned int i = 0; i < product_terms.size(); i++) {
+          computeJoinOrProductRelations(product_terms[i]);
+        }
       }
       fact = fact.negate();
     }
@@ -278,13 +306,12 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
   }
 
   void TheorySetsRels::computeJoinOrProductRelations(Node n) {
+    Trace("rels-debug") << "\n[sets-rels] computeJoinOrProductRelations for relation  " << n << std::endl;
     switch(n[0].getKind()) {
-    case kind::JOIN:
-      computeJoinOrProductRelations(n[0]);
-      break;
     case kind::TRANSPOSE:
       computeTransposeRelations(n[0]);
       break;
+    case kind::JOIN:
     case kind::PRODUCT:
       computeJoinOrProductRelations(n[0]);
       break;
@@ -293,12 +320,10 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     }
 
     switch(n[1].getKind()) {
-    case kind::JOIN:
-      computeJoinOrProductRelations(n[1]);
-      break;
     case kind::TRANSPOSE:
       computeTransposeRelations(n[1]);
       break;
+    case kind::JOIN:
     case kind::PRODUCT:
       computeJoinOrProductRelations(n[1]);
       break;
@@ -349,9 +374,6 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
       rev_tuples.push_back(rev_tup);
       rev_exps.push_back(Rewriter::rewrite(reason));
       sendInfer(MEMBER(rev_tup, n_rep), Rewriter::rewrite(reason), "transpose-rule");
-//      if(std::find(rev_tuples.begin(), rev_tuples.end(), reverseTuple(tuples[i])) == rev_tuples.end()) {
-//
-//      }
     }
     d_membership_cache[n_rep] = rev_tuples;
     d_membership_exp_cache[n_rep] = rev_exps;
@@ -364,7 +386,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     Node r2 = n[1];
     Node r1_rep = getRepresentative(r1);
     Node r2_rep = getRepresentative(r2);
-    Trace("rels-debug") << "[sets-rels] start joining tuples in "
+    Trace("rels-debug") << "[sets-rels] start composing tuples in relations "
                        << r1 << " and " << r2
                        << "\n r1_rep: " << r1_rep
                        << "\n r2_rep: " << r2_rep << std::endl;
@@ -390,10 +412,6 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
       for(unsigned int j = 0; j < r2_elements.size(); j++) {
         std::vector<Node> joinedTuple;
         joinedTuple.push_back(Node::fromExpr(dt[0].getConstructor()));
-        Debug("rels-debug") << "areEqual(r1_elements[i][t1_len-1], r2_elements[j][0]):\n"
-                            << "   r1_elements[i][t1_len-1] = " << r1_elements[i][t1_len-1]
-                            << "   r2_elements[j][0]) = " << r2_elements[j][0]
-                            << "   are equal? " << areEqual(r1_elements[i][t1_len-1], r2_elements[j][0]) << std::endl;
         if((areEqual(r1_elements[i][t1_len-1], r2_elements[j][0]) && n.getKind() == kind::JOIN) ||
             n.getKind() == kind::PRODUCT) {
           unsigned int k = 0;
@@ -434,7 +452,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
           if(kind::JOIN == n.getKind())
             sendInfer(fact, reason, "join-compose");
           else if(kind::PRODUCT == n.getKind())
-            sendInfer(fact, reason, "product-compose");
+            sendInfer( fact, reason, "product-compose" );
         }
       }
     }
@@ -454,13 +472,18 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
   }
 
   void TheorySetsRels::doPendingLemmas() {
-    if( !(*d_conflict) && !d_lemma_cache.empty() ){
+    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;
         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;
+          continue;
+        }
+
         Trace("rels-debug") << "[sets-rels] Process pending fact as lemma : " << child_it->first << std::endl;
         d_sets.d_out->lemma(child_it->first);
       }
@@ -483,6 +506,10 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
 
   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;
+    }
     d_pending_facts[fact] = exp;
     d_infer.push_back( fact );
     d_infer_exp.push_back( exp );
@@ -522,12 +549,44 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
 
   bool TheorySetsRels::areEqual( Node a, Node b ){
     if( hasTerm( a ) && hasTerm( b ) ){
-//      Trace("rels-debug") << "has a and b " << a << " " << b << " are equal? "<<  d_eqEngine->areEqual( a, b ) << std::endl;
+      if( d_eqEngine->isTriggerTerm(a, THEORY_SETS) &&
+          d_eqEngine->isTriggerTerm(b, THEORY_SETS) ) {
+        // Get representative trigger terms
+          TNode x_shared = d_eqEngine->getTriggerTermRepresentative(a, THEORY_SETS);
+          TNode y_shared = d_eqEngine->getTriggerTermRepresentative(b, THEORY_SETS);
+          EqualityStatus eqStatusDomain = d_sets.d_valuation.getEqualityStatus(x_shared, y_shared);
+          switch (eqStatusDomain) {
+            case EQUALITY_TRUE_AND_PROPAGATED:
+              // Should have been propagated to us
+              Trace("rels-debug") << "EQUALITY_TRUE_AND_PROPAGATED ****  equality( a, b ) = true" << std::endl;
+              return true;
+              break;
+            case EQUALITY_TRUE:
+              // Missed propagation - need to add the pair so that theory engine can force propagation
+              Trace("rels-debug") << "EQUALITY_TRUE **** equality( a, b ) = true" << std::endl;
+              return true;
+              break;
+            case EQUALITY_FALSE_AND_PROPAGATED:
+              // Should have been propagated to us
+              Trace("rels-debug") << "EQUALITY_FALSE_AND_PROPAGATED ******** equality( a, b ) = false" << std::endl;
+              return false;
+              break;
+            case EQUALITY_FALSE:
+              Trace("rels-debug") << "EQUALITY_FALSE **** equality( a, b ) = false" << std::endl;
+              return false;
+              break;
+
+            default:
+              // Covers EQUALITY_TRUE_IN_MODEL (common case) and EQUALITY_UNKNOWN
+              break;
+          }
+      }
+      Trace("rels-debug") << "has a and b " << a << " " << b << " are equal? "<<  d_eqEngine->areEqual( a, b ) << std::endl;
       return d_eqEngine->areEqual( a, b );
     }else if( a.isConst() && b.isConst() ){
       return a == b;
     }else {
-//      Trace("rels-debug") << "to split a and b " << a << " " << b << std::endl;
+      Trace("rels-debug") << "to split a and b " << a << " " << b << std::endl;
       addSharedTerm(a);
       addSharedTerm(b);
       sendSplit(a, b, "tuple-element-equality");
@@ -545,6 +604,16 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     return std::find(v.begin(), v.end(), n) != v.end();
   }
 
+  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]) );
+    d_eqEngine->addTerm(atom_mod);
+    return areEqual(atom_mod, polarity_atom);
+  }
+
   TheorySetsRels::TheorySetsRels(context::Context* c,
                                  context::UserContext* u,
                                  eq::EqualityEngine* eq,

diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 4eb30ab12886f220519791aa703caeec187dff8e..d0d926e69bead5efde0ba844ec486dce2f2dbbb1 100644 (file)
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -54,6 +54,7 @@ private:
 
   // Facts and lemmas to be sent to EE
   std::map< Node, Node > d_pending_facts;
+  std::map< Node, Node > d_pending_split_facts;
   std::vector< Node > d_lemma_cache;
 
   /** inferences: maintained to ensure ref count for internally introduced nodes */
@@ -84,6 +85,7 @@ private:
   void sendLemma( Node fact, Node reason, bool polarity );
   void sendSplit( Node a, Node b, const char * c );
   void doPendingFacts();
+  void doPendingSplitFacts();
   void addSharedTerm( TNode n );
 
   // Helper functions
@@ -91,6 +93,7 @@ private:
   bool hasTerm( Node a );
   bool areEqual( Node a, Node b );
   bool exists( std::vector<Node>&, Node );
+  bool holds(Node);
 
 };
 

diff --git a/test/regress/regress0/sets/rels/rel_join_3.cvc b/test/regress/regress0/sets/rels/rel_join_3.cvc
new file mode 100644 (file)
index 0000000..6e190ce
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_3.cvc
@@ -0,0 +1,29 @@
+% 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);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN r);
+
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_join_3_1.cvc b/test/regress/regress0/sets/rels/rel_join_3_1.cvc
new file mode 100644 (file)
index 0000000..d4e666c
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_3_1.cvc
@@ -0,0 +1,29 @@
+% 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);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT a IS_IN r;
+
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_join_4.cvc b/test/regress/regress0/sets/rels/rel_join_4.cvc
new file mode 100644 (file)
index 0000000..030810f
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_4.cvc
@@ -0,0 +1,32 @@
+% 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);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+b : IntPair;
+ASSERT b = (7, 5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT b IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN r);
+
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_join_5.cvc b/test/regress/regress0/sets/rels/rel_join_5.cvc
new file mode 100644 (file)
index 0000000..5209d81
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_5.cvc
@@ -0,0 +1,19 @@
+% 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 (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+
+a : IntPair;
+ASSERT a = (1,4);
+ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT NOT (a IS_IN r);
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_product_0.cvc b/test/regress/regress0/sets/rels/rel_product_0.cvc
new file mode 100644 (file)
index 0000000..09981be
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_product_0.cvc
@@ -0,0 +1,20 @@
+% EXPECT: unsat
+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;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntTup;
+ASSERT v = (1,2,2,1);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (v IS_IN (x PRODUCT y));
+
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_product_0_1.cvc b/test/regress/regress0/sets/rels/rel_product_0_1.cvc
new file mode 100644 (file)
index 0000000..f141c7b
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_product_0_1.cvc
@@ -0,0 +1,20 @@
+% 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;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntTup;
+ASSERT v = (1,2,2,1);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT v IS_IN (x PRODUCT y);
+
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_product_1.cvc b/test/regress/regress0/sets/rels/rel_product_1.cvc
new file mode 100644 (file)
index 0000000..1826e5a
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_product_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT,INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2,3);
+zt : IntPair;
+ASSERT zt = (3,2,1);
+v : IntTup;
+ASSERT v = (1,2,3,3,2,1);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (v IS_IN (x PRODUCT y));
+
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_product_1_1.cvc b/test/regress/regress0/sets/rels/rel_product_1_1.cvc
new file mode 100644 (file)
index 0000000..3e5280c
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_product_1_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: SAT
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT,INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2,3);
+zt : IntPair;
+ASSERT zt = (3,2,1);
+v : IntTup;
+ASSERT v = (1,2,3,3,2,1);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT v IS_IN (x PRODUCT y);
+
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_tp_join_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_0.cvc
new file mode 100644 (file)
index 0000000..a03f0e3
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_0.cvc
@@ -0,0 +1,32 @@
+% 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);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (5,1);
+
+b : IntPair;
+ASSERT b = (7, 5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT b IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN (TRANSPOSE 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
new file mode 100644 (file)
index 0000000..dca0a3b
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc
@@ -0,0 +1,24 @@
+% 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 (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+
+
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) 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_2.cvc b/test/regress/regress0/sets/rels/rel_tp_join_2.cvc
new file mode 100644 (file)
index 0000000..cc851f6
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_2.cvc
@@ -0,0 +1,19 @@
+% 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 (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+
+a : IntPair;
+ASSERT a = (4,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_tp_join_2_1.cvc b/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc
new file mode 100644 (file)
index 0000000..04856d8
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc
@@ -0,0 +1,19 @@
+% 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 (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+a : IntPair;
+ASSERT a = (4,1);
+
+ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT a IS_IN (TRANSPOSE r);
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_tp_join_3.cvc b/test/regress/regress0/sets/rels/rel_tp_join_3.cvc
new file mode 100644 (file)
index 0000000..25277f4
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_3.cvc
@@ -0,0 +1,28 @@
+% 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;
+
+ASSERT (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+ASSERT (3, 3) IS_IN w;
+
+a : IntPair;
+ASSERT a = (4,1);
+%ASSERT r = (((TRANSPOSE x) JOIN y) JOIN (w JOIN z));
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+
+zz : SET OF IntPair;
+ASSERT zz = ((TRANSPOSE x) JOIN y);
+ASSERT NOT ((1,3) IS_IN w);
+ASSERT NOT ((1,3) IS_IN (w | zz) );
+
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc
new file mode 100644 (file)
index 0000000..b05026b
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc
@@ -0,0 +1,21 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntTup;
+
+ASSERT (2, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (2, 2) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+
+v : IntTup;
+ASSERT v = (4,3,2,1);
+
+ASSERT r = (((TRANSPOSE x) JOIN y) PRODUCT z);
+ASSERT NOT (v IS_IN (TRANSPOSE r));
+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
new file mode 100644 (file)
index 0000000..c7757bd
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc
@@ -0,0 +1,28 @@
+% EXPECT: unsat
+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));
+
+st : SET OF INT;
+su : SET OF INT;
+ASSERT t IS_IN st;
+ASSERT u IS_IN su;
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_transpose_2.cvc b/test/regress/regress0/sets/rels/rel_transpose_2.cvc
new file mode 100644 (file)
index 0000000..15a035b
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_transpose_2.cvc
@@ -0,0 +1,12 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntTup: TYPE = [INT];
+x : SET OF IntTup;
+y : SET OF IntTup;
+z : IntTup;
+ASSERT z = (1);
+zt : IntTup;
+ASSERT zt = (1);
+ASSERT z IS_IN x;
+ASSERT NOT (zt IS_IN (TRANSPOSE x));
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_transpose_3.cvc b/test/regress/regress0/sets/rels/rel_transpose_3.cvc
new file mode 100644 (file)
index 0000000..225f349
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_transpose_3.cvc
@@ -0,0 +1,14 @@
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+ASSERT (x = y);
+ASSERT z IS_IN x;
+ASSERT NOT (zt IS_IN (TRANSPOSE y));
+
+CHECKSAT;

diff --git a/test/regress/regress0/sets/rels/rel_transpose_4.cvc b/test/regress/regress0/sets/rels/rel_transpose_4.cvc
new file mode 100644 (file)
index 0000000..b260147
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_transpose_4.cvc
@@ -0,0 +1,13 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+
+ASSERT z IS_IN x;
+ASSERT NOT ((2, 1) IS_IN (TRANSPOSE x));
+
+CHECKSAT;