Add Relation and Table types to SMTLib parser (#8605)

diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst
index f6e27732917a8e72ca249499d4ea6caafc45cb29..b2d7245eb5b0fa6cc9667db1ac48fd3652be2f87 100644 (file)
--- a/docs/theories/sets-and-relations.rst
+++ b/docs/theories/sets-and-relations.rst
@@ -171,7 +171,11 @@ More details can be found in :cite:`MengRTB17`.
 |                      |                                              |                                                                                    |
 |                      |                                              | ``Term t = solver.mkTerm(Kind::APPLY_SELECTOR, {s, t});``                          |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
-| Relation Sort        | ``(Set (Tuple <Sort_1>, ..., <Sort_n>))``    | ``Sort s = solver.mkSetSort(cvc5::Sort tupleSort);``                               |
+| Relation Sort        | ``(Relation <Sort_1>, ..., <Sort_n>)``       | ``Sort s = solver.mkSetSort(cvc5::Sort tupleSort);``                               |
+|                      |                                              |                                                                                    |
+|                      | which is a syntax sugar for                  |                                                                                    |
+|                      |                                              |                                                                                    |
+|                      | ``(Set (Tuple <Sort_1>, ..., <Sort_n>))``    |                                                                                    |
 +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+
 | Constants            | ``(declare-const X (Set (Tuple Int Int)``    | ``Sort s = solver.mkSetSort(solver.mkTupleSort({s_int, s_int});``                  |
 |                      |                                              |                                                                                    |

diff --git a/examples/api/cpp/relations.cpp b/examples/api/cpp/relations.cpp
index 2b0b23fa6f1e47be008a1cacca9bfaa3af186f70..0b1c7989a1ad38318f4c19a5c2c448e00d0d554b 100644 (file)
--- a/examples/api/cpp/relations.cpp
+++ b/examples/api/cpp/relations.cpp
@@ -39,12 +39,12 @@ int main()
 
   // (Tuple Person)
   Sort tupleArity1 = solver.mkTupleSort({personSort});
-  // (Set (Tuple Person))
+  // (Relation Person)
   Sort relationArity1 = solver.mkSetSort(tupleArity1);
 
   // (Tuple Person Person)
   Sort tupleArity2 = solver.mkTupleSort({personSort, personSort});
-  // (Set (Tuple Person Person))
+  // (Relation Person Person)
   Sort relationArity2 = solver.mkSetSort(tupleArity2);
 
   // empty set
@@ -69,21 +69,21 @@ int main()
   Term isEmpty1 = solver.mkTerm(EQUAL, {males, emptySetTerm});
   Term isEmpty2 = solver.mkTerm(EQUAL, {females, emptySetTerm});
 
-  // (assert (= people (as set.universe (Set (Tuple Person)))))
+  // (assert (= people (as set.universe (Relation Person))))
   Term peopleAreTheUniverse = solver.mkTerm(EQUAL, {people, universeSet});
-  // (assert (not (= males (as set.empty (Set (Tuple Person))))))
+  // (assert (not (= males (as set.empty (Relation Person)))))
   Term maleSetIsNotEmpty = solver.mkTerm(NOT, {isEmpty1});
-  // (assert (not (= females (as set.empty (Set (Tuple Person))))))
+  // (assert (not (= females (as set.empty (Relation Person)))))
   Term femaleSetIsNotEmpty = solver.mkTerm(NOT, {isEmpty2});
 
   // (assert (= (set.inter males females)
-  //            (as set.empty (Set (Tuple Person)))))
+  //            (as set.empty (Relation Person))))
   Term malesFemalesIntersection = solver.mkTerm(SET_INTER, {males, females});
   Term malesAndFemalesAreDisjoint =
       solver.mkTerm(EQUAL, {malesFemalesIntersection, emptySetTerm});
 
-  // (assert (not (= father (as set.empty (Set (Tuple Person Person))))))
-  // (assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
+  // (assert (not (= father (as set.empty (Relation Person Person)))))
+  // (assert (not (= mother (as set.empty (Relation Person Person)))))
   Term isEmpty3 = solver.mkTerm(EQUAL, {father, emptyRelationTerm});
   Term isEmpty4 = solver.mkTerm(EQUAL, {mother, emptyRelationTerm});
   Term fatherIsNotEmpty = solver.mkTerm(NOT, {isEmpty3});

diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java
index b1b4955f17ee674abb113cd1bbfbc3f19eef0eef..18cf255072e7a4e6b95841db62c956a9e3f0cf53 100644 (file)
--- a/examples/api/java/Relations.java
+++ b/examples/api/java/Relations.java
@@ -39,12 +39,12 @@ public class Relations
 
       // (Tuple Person)
       Sort tupleArity1 = solver.mkTupleSort(new Sort[] {personSort});
-      // (Set (Tuple Person))
+      // (Relation Person)
       Sort relationArity1 = solver.mkSetSort(tupleArity1);
 
       // (Tuple Person Person)
       Sort tupleArity2 = solver.mkTupleSort(new Sort[] {personSort, personSort});
-      // (Set (Tuple Person Person))
+      // (Relation Person Person)
       Sort relationArity2 = solver.mkSetSort(tupleArity2);
 
       // empty set
@@ -69,21 +69,21 @@ public class Relations
       Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm);
       Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm);
 
-      // (assert (= people (as set.universe (Set (Tuple Person)))))
+      // (assert (= people (as set.universe (Relation Person))))
       Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet);
-      // (assert (not (= males (as set.empty (Set (Tuple Person))))))
+      // (assert (not (= males (as set.empty (Relation Person)))))
       Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1);
-      // (assert (not (= females (as set.empty (Set (Tuple Person))))))
+      // (assert (not (= females (as set.empty (Relation Person)))))
       Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2);
 
       // (assert (= (set.inter males females)
-      //            (as set.empty (Set (Tuple Person)))))
+      //            (as set.empty (Relation Person))))
       Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females);
       Term malesAndFemalesAreDisjoint =
           solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
 
-      // (assert (not (= father (as set.empty (Set (Tuple Person Person))))))
-      // (assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
+      // (assert (not (= father (as set.empty (Relation Person Person)))))
+      // (assert (not (= mother (as set.empty (Relation Person Person)))))
       Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm);
       Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm);
       Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3);

diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java
index 6bb806481b13c28c7ffc1973c9b465d7ce6026b8..63dc823f2375e66e99c102fdd3da94f97b0d493d 100644 (file)
--- a/examples/api/java/Statistics.java
+++ b/examples/api/java/Statistics.java
@@ -128,12 +128,12 @@ public class Statistics
 
     // (Tuple Person)
     Sort tupleArity1 = solver.mkTupleSort(new Sort[] {personSort});
-    // (Set (Tuple Person))
+    // (Relation Person)
     Sort relationArity1 = solver.mkSetSort(tupleArity1);
 
     // (Tuple Person Person)
     Sort tupleArity2 = solver.mkTupleSort(new Sort[] {personSort, personSort});
-    // (Set (Tuple Person Person))
+    // (Relation Person Person)
     Sort relationArity2 = solver.mkSetSort(tupleArity2);
 
     // empty set
@@ -158,11 +158,11 @@ public class Statistics
     Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm);
     Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm);
 
-    // (assert (= people (as set.universe (Set (Tuple Person)))))
+    // (assert (= people (as set.universe (Relation Person))))
     Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet);
-    // (assert (not (= males (as set.empty (Set (Tuple Person))))))
+    // (assert (not (= males (as set.empty (Relation Person)))))
     Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1);
-    // (assert (not (= females (as set.empty (Set (Tuple Person))))))
+    // (assert (not (= females (as set.empty (Relation Person)))))
     Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2);
 
     // (assert (= (set.inter males females) (as set.empty (Set (Tuple
@@ -170,8 +170,8 @@ public class Statistics
     Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females);
     Term malesAndFemalesAreDisjoint = solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
 
-    // (assert (not (= father (as set.empty (Set (Tuple Person Person))))))
-    // (assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
+    // (assert (not (= father (as set.empty (Relation Person Person)))))
+    // (assert (not (= mother (as set.empty (Relation Person Person)))))
     Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm);
     Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm);
     Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3);

diff --git a/examples/api/python/relations.py b/examples/api/python/relations.py
index 323cd263bcf5e66a9b1189ac385edd46c849c0e1..7f5ed4315ca7905a22722ac3e37a4abd25e0359f 100644 (file)
--- a/examples/api/python/relations.py
+++ b/examples/api/python/relations.py
@@ -43,12 +43,12 @@ if __name__ == "__main__":
 
     # (Tuple Person)
     tupleArity1 = solver.mkTupleSort(personSort)
-    # (Set (Tuple Person))
+    # (Relation Person)
     relationArity1 = solver.mkSetSort(tupleArity1)
 
     # (Tuple Person Person)
     tupleArity2 = solver.mkTupleSort(personSort, personSort)
-    # (Set (Tuple Person Person))
+    # (Relation Person Person)
     relationArity2 = solver.mkSetSort(tupleArity2)
 
     # empty set
@@ -73,21 +73,21 @@ if __name__ == "__main__":
     isEmpty1 = solver.mkTerm(Kind.EQUAL, males, emptySetTerm)
     isEmpty2 = solver.mkTerm(Kind.EQUAL, females, emptySetTerm)
 
-    # (assert (= people (as set.universe (Set (Tuple Person)))))
+    # (assert (= people (as set.universe (Relation Person))))
     peopleAreTheUniverse = solver.mkTerm(Kind.EQUAL, people, universeSet)
-    # (assert (not (= males (as set.empty (Set (Tuple Person))))))
+    # (assert (not (= males (as set.empty (Relation Person)))))
     maleSetIsNotEmpty = solver.mkTerm(Kind.NOT, isEmpty1)
-    # (assert (not (= females (as set.empty (Set (Tuple Person))))))
+    # (assert (not (= females (as set.empty (Relation Person)))))
     femaleSetIsNotEmpty = solver.mkTerm(Kind.NOT, isEmpty2)
 
     # (assert (= (set.inter males females)
-    #            (as set.empty (Set (Tuple Person)))))
+    #            (as set.empty (Relation Person))))
     malesFemalesIntersection = solver.mkTerm(Kind.SET_INTER, males, females)
     malesAndFemalesAreDisjoint = \
             solver.mkTerm(Kind.EQUAL, malesFemalesIntersection, emptySetTerm)
 
-    # (assert (not (= father (as set.empty (Set (Tuple Person Person))))))
-    # (assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
+    # (assert (not (= father (as set.empty (Relation Person Person)))))
+    # (assert (not (= mother (as set.empty (Relation Person Person)))))
     isEmpty3 = solver.mkTerm(Kind.EQUAL, father, emptyRelationTerm)
     isEmpty4 = solver.mkTerm(Kind.EQUAL, mother, emptyRelationTerm)
     fatherIsNotEmpty = solver.mkTerm(Kind.NOT, isEmpty3)

diff --git a/examples/api/smtlib/relations.smt2 b/examples/api/smtlib/relations.smt2
index 971f1d8320527cbc3d0b3342b0c72e75f32a2682..145260bce2b23f070ced94406244913079f0cb1f 100644 (file)
--- a/examples/api/smtlib/relations.smt2
+++ b/examples/api/smtlib/relations.smt2
@@ -9,24 +9,24 @@
 
 (declare-sort Person 0)
 
-(declare-fun people () (Set (Tuple Person)))
-(declare-fun males () (Set (Tuple Person)))
-(declare-fun females () (Set (Tuple Person)))
-(declare-fun father () (Set (Tuple Person Person)))
-(declare-fun mother () (Set (Tuple Person Person)))
-(declare-fun parent () (Set (Tuple Person Person)))
-(declare-fun ancestor () (Set (Tuple Person Person)))
-(declare-fun descendant () (Set (Tuple Person Person)))
+(declare-fun people () (Relation Person))
+(declare-fun males () (Relation Person))
+(declare-fun females () (Relation Person))
+(declare-fun father () (Relation Person Person))
+(declare-fun mother () (Relation Person Person))
+(declare-fun parent () (Relation Person Person))
+(declare-fun ancestor () (Relation Person Person))
+(declare-fun descendant () (Relation Person Person))
 
-(assert (= people (as set.universe (Set (Tuple Person)))))
-(assert (not (= males (as set.empty (Set (Tuple Person))))))
-(assert (not (= females (as set.empty (Set (Tuple Person))))))
-(assert (= (set.inter males females) (as set.empty (Set (Tuple Person)))))
+(assert (= people (as set.universe (Relation Person))))
+(assert (not (= males (as set.empty (Relation Person)))))
+(assert (not (= females (as set.empty (Relation Person)))))
+(assert (= (set.inter males females) (as set.empty (Relation Person))))
 
 ; father relation is not empty
-(assert (not (= father (as set.empty (Set (Tuple Person Person))))))
+(assert (not (= father (as set.empty (Relation Person Person)))))
 ; mother relation is not empty
-(assert (not (= mother (as set.empty (Set (Tuple Person Person))))))
+(assert (not (= mother (as set.empty (Relation Person Person)))))
 ; fathers are males
 (assert (set.subset (rel.join father people) males))
 ; mothers are females

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dd6bd004ac9a05dc9086b8e9202aa5cc8c4a4107..29262da320d50192041f2ecbb7adc8246e295da0 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2031,6 +2031,12 @@ sortSymbol[cvc5::Sort& t]
           t = SOLVER->mkSequenceSort( args[0] );
         } else if (name == "Tuple" && !PARSER_STATE->strictModeEnabled()) {
           t = SOLVER->mkTupleSort(args);
+        } else if (name == "Relation" && !PARSER_STATE->strictModeEnabled()) {
+          cvc5::Sort tupleSort = SOLVER->mkTupleSort(args);
+          t = SOLVER->mkSetSort(tupleSort);
+        } else if (name == "Table" && !PARSER_STATE->strictModeEnabled()) {
+          cvc5::Sort tupleSort = SOLVER->mkTupleSort(args);
+          t = SOLVER->mkBagSort(tupleSort);
         } else {
           t = PARSER_STATE->getSort(name, args);
         }

diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index 0f22c5853f65aa737585dff3c98413b938f905cf..61d3010741241960e034e3d38ed78a6d8d469b10 100644 (file)
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -29,7 +29,7 @@ class RelsUtils
    * compute the transitive closure of a binary relation
    * @param members constant nodes of type (Tuple E E) that are known to in the
    * relation rel
-   * @param rel a binary relation of type (Set (Tuple E E))
+   * @param rel a binary relation of type (Relation E E)
    * @pre all members need to be constants
    * @return the transitive closure of the relation
    */
@@ -38,7 +38,7 @@ class RelsUtils
   /**
    * add all pairs (a, c) to the transitive closures where c is reachable from b
    * in the transitive relation in a depth first search manner.
-   * @param rel a binary relation of type (Set (Tuple E E))
+   * @param rel a binary relation of type (Relation E E)
    * @param members constant nodes of type (Tuple E E) that are known to be in
    * the relation rel
    * @param a a node of type E where (a,b) is an element in the transitive
@@ -58,7 +58,7 @@ class RelsUtils
 
   /**
    * construct a pair from two elements
-   * @param rel a node of type (Set (Tuple E E))
+   * @param rel a node of type (Relation E E)
    * @param a a node of type E
    * @param b a node of type E
    * @return  a tuple (tuple a b)

diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 00d9abc553d4a19157001d0d7c2fa5841c1ed178..d6f16a79b61894872afc2fb8716e19d2d3870d95 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -143,11 +143,11 @@ struct SetMapTypeRule
 /**
  * Type rule for binary operators (rel.join, rel.product) to check
  * if the two arguments are relations (set of tuples).
- * For arguments A of type (Set (Tuple A1 ... Am)) and B of type
- * (Set (Tuple B1 ... Bn)):
- * - (rel.product A B): it computes the type (Set (Tuple (A1 ... Am B1 ... Bn)).
+ * For arguments A of type (Relation A1 ... Am) and B of type
+ * (Relation B1 ... Bn):
+ * - (rel.product A B): it computes the type (Relation (A1 ... Am B1 ... Bn).
  * - (rel.join A B) it checks that m, n > 1 and Am = B1 and computes the type
- *   (Set (Tuple (A1 ... Am-1 B2 ... Bn)).
+ *   (Relation (A1 ... Am-1 B2 ... Bn).
  */
 struct RelBinaryOperatorTypeRule
 {
@@ -156,8 +156,8 @@ struct RelBinaryOperatorTypeRule
 
 /**
  * Type rule for unary operator (rel.transpose A) to check that A is a relation
- * (set of Tuples). For an argument A of type (Set (Tuple A1 ... An))
- * it reveres A1 ... An and computes the type (Set (Tuple An ... A1)).
+ * (set of Tuples). For an argument A of type (Relation A1 ... An)
+ * it reveres A1 ... An and computes the type (Relation An ... A1).
  */
 struct RelTransposeTypeRule
 {
@@ -166,7 +166,7 @@ struct RelTransposeTypeRule
 
 /**
  * Type rule for unary operator (rel.tclosure A) to check that A is a binary
- * relation of type (Set (Tuple T T)), where T is a type
+ * relation of type (Relation T T), where T is a type
  */
 struct RelTransClosureTypeRule
 {
@@ -175,7 +175,7 @@ struct RelTransClosureTypeRule
 
 /**
  * Type rule for operator (rel.join_image A c) that checks A is a binary
- * relation of type (Set (Tuple T T)), where T is a type, and c is an integer
+ * relation of type (Relation T T), where T is a type, and c is an integer
  * term (in fact c should be a non-negative constant, otherwise a logic
  * exception is thrown TheorySetsPrivate::preRegisterTerm).
  */
@@ -186,7 +186,7 @@ struct JoinImageTypeRule
 
 /**
  * Type rule for unary operator (rel.iden A) to check that A is a unary relation
- * of type (Set (Tuple T)) and computes the type (Set (Tuple T T)) for the
+ * of type (Relation T) and computes the type (Relation T T) for the
  * identity
  */
 struct RelIdenTypeRule

diff --git a/test/regress/cli/regress0/fmf/quant_real_univ.cvc.smt2 b/test/regress/cli/regress0/fmf/quant_real_univ.cvc.smt2
index d1c93a45b1162f24d9ef3e225adb0e6e9226248b..fd0b11fa73dfe31a1fd3f9fe52dd8aa518275c42 100644 (file)
--- a/test/regress/cli/regress0/fmf/quant_real_univ.cvc.smt2
+++ b/test/regress/cli/regress0/fmf/quant_real_univ.cvc.smt2
@@ -1,13 +1,13 @@
-; EXPECT: sat\r
+; EXPECT: sat
 (set-logic ALL)
 (set-option :incremental false)
 (set-option :fmf-bound true)
 (set-option :sets-ext true)
 (declare-sort Atom 0)
-(declare-fun REAL_UNIVERSE () (Set (Tuple Real)))
-(declare-fun ATOM_UNIVERSE () (Set (Tuple Atom)))
-(assert (= REAL_UNIVERSE (as set.universe (Set (Tuple Real)))))
-(assert (= ATOM_UNIVERSE (as set.universe (Set (Tuple Atom)))))
-(declare-fun levelVal () (Set (Tuple Atom Real)))
+(declare-fun REAL_UNIVERSE () (Relation Real))
+(declare-fun ATOM_UNIVERSE () (Relation Atom))
+(assert (= REAL_UNIVERSE (as set.universe (Relation Real))))
+(assert (= ATOM_UNIVERSE (as set.universe (Relation Atom))))
+(declare-fun levelVal () (Relation Atom Real))
 (assert (forall ((s Atom) (v1 Real) (v2 Real)) (=> (and (and (set.member (tuple s) ATOM_UNIVERSE) (set.member (tuple v1) REAL_UNIVERSE)) (set.member (tuple v2) REAL_UNIVERSE)) (=> (and (set.member (tuple s v1) levelVal) (set.member (tuple s v2) levelVal)) (= v1 v2)))))
 (check-sat)

diff --git a/test/regress/cli/regress0/rels/addr_book_0.cvc.smt2 b/test/regress/cli/regress0/rels/addr_book_0.cvc.smt2
index 9bc85f268da50d564b29cf6a7a9d37d3128435e5..aad0a3b1563b81d151e67f823bbf27a69d55078a 100644 (file)
--- a/test/regress/cli/regress0/rels/addr_book_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/addr_book_0.cvc.smt2
@@ -5,12 +5,12 @@
 
 
 
-(declare-fun Target () (Set (Tuple Atom)))
-(declare-fun Name () (Set (Tuple Atom)))
-(declare-fun Addr () (Set (Tuple Atom)))
-(declare-fun Book () (Set (Tuple Atom)))
-(declare-fun names () (Set (Tuple Atom Atom)))
-(declare-fun addr () (Set (Tuple Atom Atom Atom)))
+(declare-fun Target () (Relation Atom))
+(declare-fun Name () (Relation Atom))
+(declare-fun Addr () (Relation Atom))
+(declare-fun Book () (Relation Atom))
+(declare-fun names () (Relation Atom Atom))
+(declare-fun addr () (Relation Atom Atom Atom))
 (declare-fun b1 () Atom)
 (declare-fun b1_tup () (Tuple Atom))
 (assert (= b1_tup (tuple b1)))
@@ -33,8 +33,8 @@
 (assert (set.member t_tup Target))
 (assert (set.subset (rel.join (rel.join Book addr) Target) Name))
 (assert (set.subset (rel.join Book names) Name))
-(assert (= (set.inter Name Addr) (as set.empty (Set (Tuple Atom)))))
-(assert (= (rel.join (set.singleton n_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Set (Tuple Atom)))))
+(assert (= (set.inter Name Addr) (as set.empty (Relation Atom))))
+(assert (= (rel.join (set.singleton n_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Relation Atom))))
 (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.union (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (set.singleton t_tup)))))
 (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b3_tup) addr)) (set.minus (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.singleton t_tup)))))
 (assert (let ((_let_1 (set.singleton n_tup))) (not (= (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (rel.join _let_1 (rel.join (set.singleton b3_tup) addr))))))

diff --git a/test/regress/cli/regress0/rels/atom_univ2.cvc.smt2 b/test/regress/cli/regress0/rels/atom_univ2.cvc.smt2
index 11799ba793d343f1f2fdf6b4eb184f3aa4046304..c8aa67e735a751413dd84244247e1051e32bcbc1 100644 (file)
--- a/test/regress/cli/regress0/rels/atom_univ2.cvc.smt2
+++ b/test/regress/cli/regress0/rels/atom_univ2.cvc.smt2
@@ -1,17 +1,17 @@
-; EXPECT: unsat\r
+; EXPECT: unsat
 (set-option :incremental false)
 (set-option :sets-ext true)
 (set-logic ALL)
 (declare-sort Atom 0)
-(declare-fun a () (Set (Tuple Atom)))
-(declare-fun b () (Set (Tuple Atom Atom)))
+(declare-fun a () (Relation Atom))
+(declare-fun b () (Relation Atom Atom))
 (declare-fun x () Atom)
 (declare-fun y () Atom)
 (assert (not (= x y)))
 (assert (set.member (tuple y) a))
 (assert (set.member (tuple x y) b))
-(assert (= (as set.universe (Set (Tuple Atom Atom))) (rel.product (as set.universe (Set (Tuple Atom))) (as set.universe (Set (Tuple Atom))))))
-(declare-fun u () (Set (Tuple Atom Atom)))
-(assert (= u (as set.universe (Set (Tuple Atom Atom)))))
+(assert (= (as set.universe (Relation Atom Atom)) (rel.product (as set.universe (Relation Atom)) (as set.universe (Relation Atom)))))
+(declare-fun u () (Relation Atom Atom))
+(assert (= u (as set.universe (Relation Atom Atom))))
 (assert (not (set.member (tuple x y) u)))
 (check-sat)

diff --git a/test/regress/cli/regress0/rels/card_transpose.cvc.smt2 b/test/regress/cli/regress0/rels/card_transpose.cvc.smt2
index 6db1e0e473e85812738d752739917e81aad3a8d0..394c64609dcd7cf9c569445ab9b3bd3a9e72e7be 100644 (file)
--- a/test/regress/cli/regress0/rels/card_transpose.cvc.smt2
+++ b/test/regress/cli/regress0/rels/card_transpose.cvc.smt2
@@ -2,6 +2,6 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
 (assert (> (set.card (rel.transpose x)) 0))
 (check-sat)

diff --git a/test/regress/cli/regress0/rels/iden_0.cvc.smt2 b/test/regress/cli/regress0/rels/iden_0.cvc.smt2
index 75dc80d227ddb03a136e496c65a17af0f9c1cbfd..2ed094e25a4261ae2e4480666f48660fa1416e32 100644 (file)
--- a/test/regress/cli/regress0/rels/iden_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/iden_0.cvc.smt2
@@ -3,9 +3,9 @@
 (set-logic ALL)
 (declare-sort Atom 0)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun id () (Set (Tuple Int Int)))
-(declare-fun t () (Set (Tuple Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun id () (Relation Int Int))
+(declare-fun t () (Relation Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/iden_1.cvc.smt2 b/test/regress/cli/regress0/rels/iden_1.cvc.smt2
index 64efc4aef47b1b69d99bc6f4d3d6bdff59059aea..d6af1bb764e3230448da6757140213265c31f7d1 100644 (file)
--- a/test/regress/cli/regress0/rels/iden_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/iden_1.cvc.smt2
@@ -4,14 +4,14 @@
 (set-logic ALL)
 (declare-sort Atom 0)
 
-(declare-fun x () (Set (Tuple Atom Atom)))
-(declare-fun t () (Set (Tuple Atom)))
-(declare-fun univ () (Set (Tuple Atom)))
+(declare-fun x () (Relation Atom Atom))
+(declare-fun t () (Relation Atom))
+(declare-fun univ () (Relation Atom))
 (declare-fun a () Atom)
 (declare-fun b () Atom)
 (declare-fun c () Atom)
 (declare-fun d () Atom)
-(assert (= univ (as set.universe (Set (Tuple Atom)))))
+(assert (= univ (as set.universe (Relation Atom))))
 (assert (set.member (tuple a b) x))
 (assert (set.member (tuple c d) x))
 (assert (not (= a b)))

diff --git a/test/regress/cli/regress0/rels/join-eq-u-sat.cvc.smt2 b/test/regress/cli/regress0/rels/join-eq-u-sat.cvc.smt2
index 9dd334b5e8a9ccf65e416482b90613351474ea25..685bc60a61e2381496d349efd1d4efad5d713b63 100644 (file)
--- a/test/regress/cli/regress0/rels/join-eq-u-sat.cvc.smt2
+++ b/test/regress/cli/regress0/rels/join-eq-u-sat.cvc.smt2
@@ -2,13 +2,13 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-datatypes ((unit 0)) (((u))))
 
 
-(declare-fun w () (Set (Tuple Int unit)))
-(declare-fun z () (Set (Tuple unit Int)))
+(declare-fun w () (Relation Int unit))
+(declare-fun z () (Relation unit Int))
 (assert (= (rel.join x y) (rel.join w z)))
 (assert (set.member (tuple 0 1) (rel.join x y)))
 (assert (set.member (tuple 0 u) w))

diff --git a/test/regress/cli/regress0/rels/join-eq-u.cvc.smt2 b/test/regress/cli/regress0/rels/join-eq-u.cvc.smt2
index 652504a1a4c29f60feec7c5390d56870550b3951..b582f22f58f1d21d54f3169564a81102675a0c54 100644 (file)
--- a/test/regress/cli/regress0/rels/join-eq-u.cvc.smt2
+++ b/test/regress/cli/regress0/rels/join-eq-u.cvc.smt2
@@ -2,13 +2,13 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-datatypes ((unit 0)) (((u))))
 
 
-(declare-fun w () (Set (Tuple Int unit)))
-(declare-fun z () (Set (Tuple unit Int)))
+(declare-fun w () (Relation Int unit))
+(declare-fun z () (Relation unit Int))
 (assert (= (rel.join x y) (rel.join w z)))
 (assert (set.member (tuple 0 1) (rel.join x y)))
 (assert (set.member (tuple 0 u) w))

diff --git a/test/regress/cli/regress0/rels/joinImg_0.cvc.smt2 b/test/regress/cli/regress0/rels/joinImg_0.cvc.smt2
index 85d9cac6f66af692cc857e78fc8bc5e3a11bd1b8..eb1c54e1355f05f6a38dc0944e07c67707a73fd1 100644 (file)
--- a/test/regress/cli/regress0/rels/joinImg_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/joinImg_0.cvc.smt2
@@ -3,10 +3,10 @@
 (set-logic ALL)
 (set-option :sets-ext true)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
-(declare-fun t () (Set (Tuple Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
+(declare-fun t () (Relation Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2 b/test/regress/cli/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2
index ee500f8edb2644fdb125857acc07e2bd7dbd20c5..fc72055f604675222fa33d94ce801dd521b0ce4b 100644 (file)
--- a/test/regress/cli/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2
@@ -2,12 +2,12 @@
 (set-option :incremental false)
 (set-logic QF_UFDTFS)
 (declare-datatypes ((Atom 0)) (((atom))))
-(declare-fun t () (Set (Tuple Atom Atom)))
+(declare-fun t () (Relation Atom Atom))
 (declare-fun b () Atom)
 (declare-fun a () Atom)
 (declare-fun c () Atom)
-(declare-fun J ((Set (Tuple Atom)) (Set (Tuple Atom Atom))) (Set (Tuple Atom)))
-(declare-fun T ((Set (Tuple Atom Atom))) (Set (Tuple Atom Atom)))
+(declare-fun J ((Relation Atom) (Relation Atom Atom)) (Relation Atom))
+(declare-fun T ((Relation Atom Atom)) (Relation Atom Atom))
 (assert (let ((_let_1 (set.singleton (tuple a)))) (= (rel.join _let_1 t) (J _let_1 t))))
 (assert (let ((_let_1 (set.singleton (tuple c)))) (not (= (rel.join _let_1 (rel.tclosure t)) _let_1))))
 (check-sat)

diff --git a/test/regress/cli/regress0/rels/qgu-fuzz-relations-1-dd.smt2 b/test/regress/cli/regress0/rels/qgu-fuzz-relations-1-dd.smt2
index 0e9a61922918d31c06d104e098c89a50c826b591..9f340a52f60e799f8bb9da6bc30e8625f31e6829 100644 (file)
--- a/test/regress/cli/regress0/rels/qgu-fuzz-relations-1-dd.smt2
+++ b/test/regress/cli/regress0/rels/qgu-fuzz-relations-1-dd.smt2
@@ -1,5 +1,5 @@
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun d () (Tuple Int Int))
-(assert (= (as set.empty (Set (Tuple Int Int))) (rel.join (set.singleton (tuple 1 0)) (set.singleton d))))
+(assert (= (as set.empty (Relation Int Int)) (rel.join (set.singleton (tuple 1 0)) (set.singleton d))))
 (check-sat)

diff --git a/test/regress/cli/regress0/rels/qgu-fuzz-relations-1.smt2 b/test/regress/cli/regress0/rels/qgu-fuzz-relations-1.smt2
index 6804a4df87e7c5ecfee72c874a3b98c059923ed8..f5e493d9b5d7beb0c7ec026aba4681c77eddb45f 100644 (file)
--- a/test/regress/cli/regress0/rels/qgu-fuzz-relations-1.smt2
+++ b/test/regress/cli/regress0/rels/qgu-fuzz-relations-1.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL)
 (set-info :status sat)
-(declare-fun a () (Set (Tuple Int Int)))
-(declare-fun b () (Set (Tuple Int Int)))
+(declare-fun a () (Relation Int Int))
+(declare-fun b () (Relation Int Int))
 (declare-fun c () Int)
 (declare-fun d () (Tuple Int Int))
 (assert (and (= b (set.singleton (tuple 1 0))) (= a (rel.join b (rel.transpose a))) (= a (rel.join b (rel.tclosure a))) (= a (rel.join b (set.singleton d)))))

diff --git a/test/regress/cli/regress0/rels/rel_1tup_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_1tup_0.cvc.smt2
index 5a320b1d0503e52e3714f77427c64aed6ecb51ec..42f425db6be0c9390d3b81c1956ede6f663b3ec4 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_1tup_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_1tup_0.cvc.smt2
@@ -3,9 +3,9 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int)))
-(declare-fun z () (Set (Tuple Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int))
+(declare-fun z () (Relation Int))
 (declare-fun b () (Tuple Int Int))
 (assert (= b (tuple 2 1)))
 (assert (set.member b x))

diff --git a/test/regress/cli/regress0/rels/rel_complex_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_complex_0.cvc.smt2
index a72a26b9b803b353d00afe8e39a687afe938e361..285dff1236c39851c7d611835fcf59103bd5c008 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_complex_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_complex_0.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Set Int))
 (declare-fun f () Int)
 (declare-fun g () Int)

diff --git a/test/regress/cli/regress0/rels/rel_complex_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_complex_1.cvc.smt2
index 389260e17e191f9488db4dcc6d09c80bbd1cfe8d..21d1a5d205b1f19978689391d8a31399a4f6d07a 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_complex_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_complex_1.cvc.smt2
@@ -3,12 +3,12 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
-(declare-fun w () (Set (Tuple Int)))
-(declare-fun z () (Set (Tuple Int)))
-(declare-fun r2 () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
+(declare-fun w () (Relation Int))
+(declare-fun z () (Relation Int))
+(declare-fun r2 () (Relation Int Int))
 (declare-fun a () (Tuple Int Int))
 (assert (= a (tuple 3 1)))
 (assert (set.member a x))

diff --git a/test/regress/cli/regress0/rels/rel_conflict_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_conflict_0.cvc.smt2
index 4b7fede6cd2fb69479fae361d42cd8855f12664c..a7120a6c2c8cee515d633d57486482ee7b543aac 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_conflict_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_conflict_0.cvc.smt2
@@ -2,7 +2,7 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
 (declare-fun e () (Tuple Int Int))
 (assert (= e (tuple 4 4)))
 (assert (set.member e x))

diff --git a/test/regress/cli/regress0/rels/rel_join_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_0.cvc.smt2
index 018b83e27703fe44f014ec479a15e64ef1a23108..ba2045ab8e707e3dcf6095a49110d4d2e2593109 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_0.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_join_0_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_0_1.cvc.smt2
index 4489b1a16bf4b8c92206dc71f52dff3137ec459f..e64c15c4d767d37999a5c7797939ebea758c7ff9 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_0_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_0_1.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_join_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_1.cvc.smt2
index 638964931150ba49775e03ba205a2b7d71d1604a..60260fd7e8eb922951ec79545c9ab00662f55981 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_1.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_join_1_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_1_1.cvc.smt2
index 357f37922f0f20c32a09d8ce9523dbb214b465e5..e2ff7fa46f813861358c2c30d1d0997065985968 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_1_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_1_1.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_join_2.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_2.cvc.smt2
index 3359f2f625d65da9d527b98e13d87c5e276cb445..05cc2ec11721fd1241962031687adfc166e7c04c 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_2.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_2.cvc.smt2
@@ -3,8 +3,8 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_join_2_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_2_1.cvc.smt2
index 5c1f114a51423c213e1cfbee804a44fcc1c39495..553e6b08e2512c843dfa60c3ee8fea6a20e8b7a8 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_2_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_2_1.cvc.smt2
@@ -3,8 +3,8 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_join_3.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_3.cvc.smt2
index 6459b9f032abf655fae89512af9eb0338b1bc030..b95dea83bef5ab6f7589e36737187dc04872b1b2 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_3.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_3.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_join_3_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_3_1.cvc.smt2
index 1fb714112771bd4106f453c943477acab41efaa0..b62755e57bdc4600654d58393d6b3f59f540ac8f 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_3_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_3_1.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_join_4.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_4.cvc.smt2
index fc9fad09bf923836e5fc5d3bc94fa7e979c1d9e8..96824a5ea200bbdeb54b635344f7f076b3501f34 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_4.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_4.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_join_5.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_5.cvc.smt2
index cd256a476f431eb9e685a3c38a7f944fdd9317d2..702711b856a73275974d4929574898a4def1413a 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_5.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_5.cvc.smt2
@@ -2,10 +2,10 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (assert (set.member (tuple 7 1) x))
 (assert (set.member (tuple 2 3) x))
 (assert (set.member (tuple 7 3) y))

diff --git a/test/regress/cli/regress0/rels/rel_join_6.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_6.cvc.smt2
index 81ab335aa205bc2c55dc513973fa82ccb342cfe7..9303725a884fa0a640e0024e2098b259ecc2c0d1 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_6.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_6.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (assert (= x (set.union (set.singleton (tuple 1 2)) (set.singleton (tuple 3 4)))))
 (assert (= y (rel.join x (set.union (set.singleton (tuple 2 1)) (set.singleton (tuple 4 3))))))
 (assert (not (set.member (tuple 1 1) y)))

diff --git a/test/regress/cli/regress0/rels/rel_join_7.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_7.cvc.smt2
index a8b1fd3c0246034873d46f17eb82bd53056fd77f..04a6d039ba3ccbfb2e784c88b9f7302260793f28 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_join_7.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_join_7.cvc.smt2
@@ -2,10 +2,10 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
-(declare-fun w () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
+(declare-fun w () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_product_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_product_0.cvc.smt2
index cdf3372763a4c5c5d2bd5a8a66ae3d14116b6783..aa7c1f1afeeb0fef5b4a8f3ad2a590dad545e4ac 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_product_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_product_0.cvc.smt2
@@ -3,9 +3,9 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_product_0_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_product_0_1.cvc.smt2
index a0469b3e95b3ba955b43692573feb494901f9e13..ed431835ad76087ac648ec917744de223b3b9693 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_product_0_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_product_0_1.cvc.smt2
@@ -3,9 +3,9 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_product_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_product_1.cvc.smt2
index 544068b5032a2f2a7c1202fb3297df83fa125e23..4a4f491ab93453cf1cfeebab36b625819ccb22bc 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_product_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_product_1.cvc.smt2
@@ -3,9 +3,9 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int Int)))
-(declare-fun y () (Set (Tuple Int Int Int)))
-(declare-fun r () (Set (Tuple Int Int Int)))
+(declare-fun x () (Relation Int Int Int))
+(declare-fun y () (Relation Int Int Int))
+(declare-fun r () (Relation Int Int Int))
 (declare-fun z () (Tuple Int Int Int))
 (assert (= z (tuple 1 2 3)))
 (declare-fun zt () (Tuple Int Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_product_1_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_product_1_1.cvc.smt2
index a3fb21eedbdb7b2c670b2f227a5c993ee0580f1a..14fa852e33f7a8cb20467e956783b810abcf54c3 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_product_1_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_product_1_1.cvc.smt2
@@ -3,9 +3,9 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int Int)))
-(declare-fun y () (Set (Tuple Int Int Int)))
-(declare-fun r () (Set (Tuple Int Int Int Int Int Int)))
+(declare-fun x () (Relation Int Int Int))
+(declare-fun y () (Relation Int Int Int))
+(declare-fun r () (Relation Int Int Int Int Int Int))
 (declare-fun z () (Tuple Int Int Int))
 (assert (= z (tuple 1 2 3)))
 (declare-fun zt () (Tuple Int Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_symbolic_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_symbolic_1.cvc.smt2
index 178208ff76cc9c150ad4596657ca264a666d5626..e258db77fd3bd6665451b333630d58afe0c6f8ed 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_symbolic_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_symbolic_1.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun f () Int)
 (declare-fun d () (Tuple Int Int))
 (assert (= d (tuple f 3)))

diff --git a/test/regress/cli/regress0/rels/rel_symbolic_1_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_symbolic_1_1.cvc.smt2
index 7afe4e4a9f5557790f9e7224cc4d1038f818f36a..a8eaeae08ed561e51126438b346da097bf40c18f 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_symbolic_1_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_symbolic_1_1.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun d () (Tuple Int Int))
 (assert (set.member d y))
 (declare-fun a () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_symbolic_2_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_symbolic_2_1.cvc.smt2
index 66551349856efab1bb6299a1ea570b3bec1b0064..d29bac00e17d84541e08aa7d39c7ef68ccb9ab1a 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_symbolic_2_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_symbolic_2_1.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun d () (Tuple Int Int))
 (assert (= d (tuple 1 3)))
 (assert (set.member (tuple 1 3) y))

diff --git a/test/regress/cli/regress0/rels/rel_symbolic_3_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_symbolic_3_1.cvc.smt2
index 183aff148e66cb043f05c8e5268977674e93af6c..4eb6bb2222a2609e1ff88c52a9c396747a868337 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_symbolic_3_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_symbolic_3_1.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun f () Int)
 (declare-fun d () (Tuple Int Int))
 (assert (set.member d y))

diff --git a/test/regress/cli/regress0/rels/rel_tc_11.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tc_11.cvc.smt2
index 8a2dc27496510d7ac153b084188914d5399a535c..d0e49e7d9c2f81e8a8371e3433158090372883e0 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tc_11.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tc_11.cvc.smt2
@@ -3,9 +3,9 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int Int Int))
 (assert (set.member (tuple 2 3) x))
 (assert (set.member (tuple 5 3) x))
 (assert (set.member (tuple 3 9) x))

diff --git a/test/regress/cli/regress0/rels/rel_tc_2_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tc_2_1.cvc.smt2
index 7940e989837fd100281fbdfd6fc57428503a9450..73234c4a2b6785bd9eb35acd7b7dd9d271bceeff 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tc_2_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tc_2_1.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-fun e () Int)
 (declare-fun a () (Tuple Int Int))
 (assert (= a (tuple 1 e)))

diff --git a/test/regress/cli/regress0/rels/rel_tc_3.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tc_3.cvc.smt2
index 5de2d82d2b55d47d47a3f27d04ef8f4ce71de6bf..769d5489b5bd9f31ff0a8fb8d35792237925f35b 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tc_3.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tc_3.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-fun a () Int)
 (declare-fun b () Int)
 (declare-fun c () Int)

diff --git a/test/regress/cli/regress0/rels/rel_tc_3_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tc_3_1.cvc.smt2
index df9764a5c2b8d5a68b9991deb73b6900a262c704..7dc763f517d55f31fe6d372605b4695aa7c5e5c6 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tc_3_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tc_3_1.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-fun a () Int)
 (declare-fun b () Int)
 (declare-fun c () Int)

diff --git a/test/regress/cli/regress0/rels/rel_tc_7.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tc_7.cvc.smt2
index 620f8d3d067d403109a6c81da2ebe3c12bebf5b0..0687fe0b1988f53c9b8606fd30262bd7620dc79d 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tc_7.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tc_7.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (assert (= y (rel.join (rel.tclosure x) x)))
 (assert (set.member (tuple 1 2) (rel.join (rel.join x x) x)))
 (assert (not (set.subset y (rel.tclosure x))))

diff --git a/test/regress/cli/regress0/rels/rel_tc_8.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tc_8.cvc.smt2
index 5e359b538dafbea860c5750a8c3686bc2b3428c8..240e7c0e385c1d50c94b57afb284f0b4abd574d7 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tc_8.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tc_8.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (assert (set.member (tuple 2 2) (rel.tclosure x)))
-(assert (= x (as set.empty (Set (Tuple Int Int)))))
+(assert (= x (as set.empty (Relation Int Int))))
 (check-sat)

diff --git a/test/regress/cli/regress0/rels/rel_tp_3_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_3_1.cvc.smt2
index 9f2dd11901704f9e5fc4d1a7e1f8b5b55b1e2ed8..21fa6fa10b0776a1b68052fcb7742fdb8d74bf64 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tp_3_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tp_3_1.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
 (assert (set.member (tuple 1 3) x))
 (assert (or (set.member (tuple 2 3) z) (set.member (tuple 2 1) z)))
 (assert (= y (rel.transpose x)))

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_0.cvc.smt2
index aed2badf77c8cfaa4799d6d3cabca9cc45a02f87..7995765aaaabceb13766724b844a0af138052b17 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tp_join_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tp_join_0.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_1.cvc.smt2
index 213d75bdcc9e04612969370ab64b7d220152d0bb..97506ece915a8d7ffd03b237faac9173d6449851 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tp_join_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tp_join_1.cvc.smt2
@@ -2,10 +2,10 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun b () (Tuple Int Int))
 (assert (= b (tuple 1 7)))
 (declare-fun c () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_2.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_2.cvc.smt2
index b66f1c6edea378a58449639dc486772863bbe26f..20557bf7adfde5e85f5f0905086ef46f9eee8552 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tp_join_2.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tp_join_2.cvc.smt2
@@ -2,10 +2,10 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (assert (set.member (tuple 7 1) x))
 (assert (set.member (tuple 2 3) x))
 (assert (set.member (tuple 7 3) y))

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_3.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_3.cvc.smt2
index 4ebd54b90169734d10b11e9e979682b8ecbc472c..f9f143644a081a17c1a17a6bb9478bb7cb4e7bfe 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tp_join_3.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tp_join_3.cvc.smt2
@@ -2,11 +2,11 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun w () (Set (Tuple Int Int)))
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun w () (Relation Int Int))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (assert (set.member (tuple 7 1) x))
 (assert (set.member (tuple 2 3) x))
 (assert (set.member (tuple 7 3) y))
@@ -16,7 +16,7 @@
 (declare-fun a () (Tuple Int Int))
 (assert (= a (tuple 4 1)))
 (assert (not (set.member a (rel.transpose r))))
-(declare-fun zz () (Set (Tuple Int Int)))
+(declare-fun zz () (Relation Int Int))
 (assert (= zz (rel.join (rel.transpose x) y)))
 (assert (not (set.member (tuple 1 3) w)))
 (assert (not (set.member (tuple 1 3) (set.union w zz))))

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_eq_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_eq_0.cvc.smt2
index e67f5d59ba976e07b94126ac56b9ee9b82ce9bd4..4c4e4268504c6e8b128c7387d2c8ef7a55cb8832 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tp_join_eq_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tp_join_eq_0.cvc.smt2
@@ -2,10 +2,10 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (assert (= x (set.union (set.singleton (tuple 1 7)) (set.singleton (tuple 2 3)))))
 (declare-fun d () (Tuple Int Int))
 (assert (= d (tuple 7 3)))

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_int_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_int_0.cvc.smt2
index 7806c48baa9ca18be0e117f0fefd91919f2c3141..77d48e42a90546acd4b2c6942f984f4788e857cb 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tp_join_int_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tp_join_int_0.cvc.smt2
@@ -2,11 +2,11 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun w () (Set (Tuple Int Int)))
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun w () (Relation Int Int))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun t () Int)
 (declare-fun u () Int)
 (assert (and (< 4 t) (< t 6)))

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_pro_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_pro_0.cvc.smt2
index d9120c398ef3cc65915e77d392d0148be400ceb2..3c7198ddc1b353dbae4e2128397fb59119c23cf9 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tp_join_pro_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tp_join_pro_0.cvc.smt2
@@ -3,10 +3,10 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int Int Int))
 (assert (set.member (tuple 2 1) x))
 (assert (set.member (tuple 2 3) x))
 (assert (set.member (tuple 2 2) y))

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_var_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_var_0.cvc.smt2
index c4cf0b43db398163ae629649216284e757f2d818..908d9a5e6710a4116e093a25413b28728937a3ad 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_tp_join_var_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_tp_join_var_0.cvc.smt2
@@ -2,11 +2,11 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun w () (Set (Tuple Int Int)))
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun w () (Relation Int Int))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun t () Int)
 (declare-fun u () Int)
 (assert (and (< 4 t) (< t 6)))

diff --git a/test/regress/cli/regress0/rels/rel_transpose_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_transpose_0.cvc.smt2
index 3cce80a4b22f888988fcc671fdbed45af67e1cc4..1af61fb9e8f9a94782de953d94988bc3f0c1e537 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_transpose_0.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_transpose_0.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-fun a () Int)
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))

diff --git a/test/regress/cli/regress0/rels/rel_transpose_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_transpose_1.cvc.smt2
index 728b2b23c2c56c10c71d3040e42bbdb1c79b4c42..e42db60012a7de50c1aaf15dfd6e36e74d344806 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_transpose_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_transpose_1.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int Int)))
-(declare-fun y () (Set (Tuple Int Int Int)))
+(declare-fun x () (Relation Int Int Int))
+(declare-fun y () (Relation Int Int Int))
 (declare-fun z () (Tuple Int Int Int))
 (assert (= z (tuple 1 2 3)))
 (declare-fun zt () (Tuple Int Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_transpose_1_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_transpose_1_1.cvc.smt2
index 4177d70e43b5ff2955f84281329aa582186b216f..f21924bcdd78bc7f645a6575045dc408924bc96b 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_transpose_1_1.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_transpose_1_1.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int Int)))
-(declare-fun y () (Set (Tuple Int Int Int)))
+(declare-fun x () (Relation Int Int Int))
+(declare-fun y () (Relation Int Int Int))
 (declare-fun z () (Tuple Int Int Int))
 (declare-fun a () Int)
 (assert (= z (tuple 1 2 a)))

diff --git a/test/regress/cli/regress0/rels/rel_transpose_3.cvc.smt2 b/test/regress/cli/regress0/rels/rel_transpose_3.cvc.smt2
index 24f1ca24c35227262efa68d2b569737b05473b31..8279ac04bec2f3f73801ea009ebb775a9d020694 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_transpose_3.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_transpose_3.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_transpose_4.cvc.smt2 b/test/regress/cli/regress0/rels/rel_transpose_4.cvc.smt2
index 4013806deb9f00ea3bf70df61ebae04f6c4272a2..80b43e759b0929f1f74b89e3961e5e348741f432 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_transpose_4.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_transpose_4.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (assert (set.member z x))

diff --git a/test/regress/cli/regress0/rels/rel_transpose_5.cvc.smt2 b/test/regress/cli/regress0/rels/rel_transpose_5.cvc.smt2
index fbb1d265ca984b3ad3eedffc6df21671370434a3..db3a86e44b5afbddedf8cbef6fc1154802428a73 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_transpose_5.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_transpose_5.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_transpose_6.cvc.smt2 b/test/regress/cli/regress0/rels/rel_transpose_6.cvc.smt2
index 5924efd37e1856da8680736429cabda628215a03..57d4d167ded559d9f98c9b2754f21221b5a76b26 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_transpose_6.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_transpose_6.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress0/rels/rel_transpose_7.cvc.smt2 b/test/regress/cli/regress0/rels/rel_transpose_7.cvc.smt2
index a4e0c8a76d049a1705f906561534ae558fea8c1c..b9b55204da54d502bf96a99413a62f92ddcffb96 100644 (file)
--- a/test/regress/cli/regress0/rels/rel_transpose_7.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rel_transpose_7.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (assert (= x y))
 (assert (not (= (rel.transpose x) (rel.transpose y))))
 (check-sat)

diff --git a/test/regress/cli/regress0/rels/relations-ops.smt2 b/test/regress/cli/regress0/rels/relations-ops.smt2
index 3e68011020ee20e1c1cdca8a48f0842c111898ea..809e95dd6b671a7ba1823c3d21b6931d48797f75 100644 (file)
--- a/test/regress/cli/regress0/rels/relations-ops.smt2
+++ b/test/regress/cli/regress0/rels/relations-ops.smt2
@@ -2,13 +2,13 @@
 (set-logic ALL)
 (set-info :status sat)
 
-(declare-fun r1 () (Set (Tuple String Int)))
-(declare-fun r2 () (Set (Tuple Int String)))
-(declare-fun r () (Set (Tuple String String)))
-(declare-fun s () (Set (Tuple String String)))
-(declare-fun t () (Set (Tuple String Int Int String)))
-(declare-fun lt1 () (Set (Tuple Int Int)))
-(declare-fun lt2 () (Set (Tuple Int Int)))
+(declare-fun r1 () (Relation String Int))
+(declare-fun r2 () (Relation Int String))
+(declare-fun r () (Relation String String))
+(declare-fun s () (Relation String String))
+(declare-fun t () (Relation String Int Int String))
+(declare-fun lt1 () (Relation Int Int))
+(declare-fun lt2 () (Relation Int Int))
 (declare-fun i () Int)
 
 (assert (= r1 (set.insert (tuple "a" 1) (tuple "b" 2) (tuple "c" 3) (set.singleton (tuple "d" 4)))))

diff --git a/test/regress/cli/regress0/rels/rels-sharing-simp.cvc.smt2 b/test/regress/cli/regress0/rels/rels-sharing-simp.cvc.smt2
index 186374897590d44956ddcaffe0c3b0a409d600ec..6cf085669812fcc26f0086594f4ac3291bdfacf4 100644 (file)
--- a/test/regress/cli/regress0/rels/rels-sharing-simp.cvc.smt2
+++ b/test/regress/cli/regress0/rels/rels-sharing-simp.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun w () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
+(declare-fun w () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
 (declare-fun x () Int)
 (declare-fun y () Int)
 (assert (set.member (tuple 1 x) w))

diff --git a/test/regress/cli/regress0/sets/complement.cvc.smt2 b/test/regress/cli/regress0/sets/complement.cvc.smt2
index e0a5c19f08194e02877c3d3e01f77e1e7dd6f938..fc8ad328fd84392aa85f5eb7a99b044da1a77c04 100644 (file)
--- a/test/regress/cli/regress0/sets/complement.cvc.smt2
+++ b/test/regress/cli/regress0/sets/complement.cvc.smt2
@@ -3,7 +3,7 @@
 (set-option :sets-ext true)
 (set-logic ALL)
 (declare-sort Atom 0)
-(declare-fun a () (Set (Tuple Atom)))
-(declare-fun b () (Set (Tuple Atom)))
+(declare-fun a () (Relation Atom))
+(declare-fun b () (Relation Atom))
 (assert (= a (set.complement b)))
 (check-sat)

diff --git a/test/regress/cli/regress0/sets/complement3.cvc.smt2 b/test/regress/cli/regress0/sets/complement3.cvc.smt2
index 2046b2fc9601bde1bf9a802b3d4fd622c87c8e45..c360c5ad4b1027dd5ed57df37024f02e17c6e4eb 100644 (file)
--- a/test/regress/cli/regress0/sets/complement3.cvc.smt2
+++ b/test/regress/cli/regress0/sets/complement3.cvc.smt2
@@ -3,14 +3,14 @@
 (set-option :sets-ext true)
 (set-logic ALL)
 (declare-sort Atom 0)
-(declare-fun C32 () (Set (Tuple Atom)))
-(declare-fun C2 () (Set (Tuple Atom)))
-(declare-fun C4 () (Set (Tuple Atom)))
-(declare-fun ATOM_UNIV () (Set (Tuple Atom)))
+(declare-fun C32 () (Relation Atom))
+(declare-fun C2 () (Relation Atom))
+(declare-fun C4 () (Relation Atom))
+(declare-fun ATOM_UNIV () (Relation Atom))
 (declare-fun V1 () Atom)
 (assert (= C32 (set.inter (set.complement C2) (set.complement C4))))
 (assert (set.member (tuple V1) (set.complement C32)))
-(assert (= ATOM_UNIV (as set.universe (Set (Tuple Atom)))))
+(assert (= ATOM_UNIV (as set.universe (Relation Atom))))
 (assert (set.member (tuple V1) ATOM_UNIV))
 (assert (set.member (tuple V1) (set.complement C2)))
 (check-sat)

diff --git a/test/regress/cli/regress1/bags/card3.smt2 b/test/regress/cli/regress1/bags/card3.smt2
index 4e37eb7177ef7bb7d724d914bdc2625bd62b3751..6a194d20211a87c264be7771a4d88ebd723f0d4b 100644 (file)
--- a/test/regress/cli/regress1/bags/card3.smt2
+++ b/test/regress/cli/regress1/bags/card3.smt2
@@ -1,9 +1,9 @@
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :fmf-bound true)
-(declare-fun B () (Bag (Tuple Int Int)))
+(declare-fun B () (Table Int Int))
 (declare-fun x () (Tuple Int Int))
 (assert
- (and (= (as bag.empty (Bag (Tuple Int Int))) (bag x (bag.card B)))
-      (not (= (as bag.empty (Bag (Tuple Int Int))) B))))
+ (and (= (as bag.empty (Table Int Int)) (bag x (bag.card B)))
+      (not (= (as bag.empty (Table Int Int)) B))))
 (check-sat)

diff --git a/test/regress/cli/regress1/bags/fuzzy1.smt2 b/test/regress/cli/regress1/bags/fuzzy1.smt2
index 79ccc4b82ba9f8a78d75120958ad5fd3701f547b..bd26067efcfef45182439ec9af3e19cabe79ac81 100644 (file)
--- a/test/regress/cli/regress1/bags/fuzzy1.smt2
+++ b/test/regress/cli/regress1/bags/fuzzy1.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL)
 (set-info :status sat)
-(declare-fun a () (Bag (Tuple Int Int)))
-(declare-fun b () (Bag (Tuple Int Int)))
+(declare-fun a () (Table Int Int))
+(declare-fun b () (Table Int Int))
 (declare-fun c () Int) ; c here is zero
 (assert
   (and

diff --git a/test/regress/cli/regress1/bags/fuzzy2.smt2 b/test/regress/cli/regress1/bags/fuzzy2.smt2
index c7968b27423f14404432311c0b6a4b380a5f902f..7954ed4765fd48b2dd16d205fe832d0c0c211b28 100644 (file)
--- a/test/regress/cli/regress1/bags/fuzzy2.smt2
+++ b/test/regress/cli/regress1/bags/fuzzy2.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL)
 (set-info :status sat)
-(declare-fun a () (Bag (Tuple Int Int)))
-(declare-fun b () (Bag (Tuple Int Int)))
+(declare-fun a () (Table Int Int))
+(declare-fun b () (Table Int Int))
 (declare-fun c () Int)
 (declare-fun d () (Tuple Int Int))
 (assert

diff --git a/test/regress/cli/regress1/bags/fuzzy3.smt2 b/test/regress/cli/regress1/bags/fuzzy3.smt2
index a457bf9ae87ea8ea8502a8eeba48ff699ab1aeeb..9a7be04abd64c558ec36296af77dba69b21bd7e2 100644 (file)
--- a/test/regress/cli/regress1/bags/fuzzy3.smt2
+++ b/test/regress/cli/regress1/bags/fuzzy3.smt2
@@ -1,8 +1,8 @@
 (set-logic ALL)
 (set-info :status sat)
 (set-option :produce-models true)
-(declare-fun A () (Bag (Tuple Int Int)))
-(declare-fun B () (Bag (Tuple Int Int)))
+(declare-fun A () (Table Int Int))
+(declare-fun B () (Table Int Int))
 (declare-fun c () Int)
 (declare-fun d () (Tuple Int Int))
 (assert

diff --git a/test/regress/cli/regress1/bags/fuzzy3b.smt2 b/test/regress/cli/regress1/bags/fuzzy3b.smt2
index 926455710db7ba48b7aab8b7296846bfbf471fa7..92a6c4649c11e20d29be992eac63b278d57e4709 100644 (file)
--- a/test/regress/cli/regress1/bags/fuzzy3b.smt2
+++ b/test/regress/cli/regress1/bags/fuzzy3b.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL)
 (set-info :status sat)
 (set-option :produce-models true)
-(declare-fun A () (Bag (Tuple Int Int)))
+(declare-fun A () (Table Int Int))
 (declare-fun d () (Tuple Int Int))
 (assert (= A (bag.difference_remove A (bag d 1))))
 (check-sat)

diff --git a/test/regress/cli/regress1/bags/fuzzy4.smt2 b/test/regress/cli/regress1/bags/fuzzy4.smt2
index 5b24b8d6e0d02b2afc5499cf6df4bc3081ad0de2..67706f0a216c12de4b8a2ec3a10c1e3d97d9924b 100644 (file)
--- a/test/regress/cli/regress1/bags/fuzzy4.smt2
+++ b/test/regress/cli/regress1/bags/fuzzy4.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL)
 (set-option :produce-models true)
 (set-info :status sat)
-(declare-fun A () (Bag (Tuple Int Int)))
+(declare-fun A () (Table Int Int))
 (declare-fun c () Int)
 (declare-fun d () (Tuple Int Int))
 (assert

diff --git a/test/regress/cli/regress1/bags/fuzzy5.smt2 b/test/regress/cli/regress1/bags/fuzzy5.smt2
index 0674fad9c06a5a737bf0f100a501d2a2e94c6535..1b88df7274d0190b595f92cded7e10e191560b20 100644 (file)
--- a/test/regress/cli/regress1/bags/fuzzy5.smt2
+++ b/test/regress/cli/regress1/bags/fuzzy5.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL)
 (set-option :produce-models true)
 (set-info :status sat)
-(declare-fun A () (Bag (Tuple Int Int)))
+(declare-fun A () (Table Int Int))
 (declare-fun c () Int)
 (declare-fun d () (Tuple Int Int))
 

diff --git a/test/regress/cli/regress1/bags/fuzzy6.smt2 b/test/regress/cli/regress1/bags/fuzzy6.smt2
index 2bcc024dd5afdc983c6c6e66f1bdef50b7e32e35..8625f5e33f4012a11d54acb537dc613ec5ef6431 100644 (file)
--- a/test/regress/cli/regress1/bags/fuzzy6.smt2
+++ b/test/regress/cli/regress1/bags/fuzzy6.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL)
 (set-info :status sat)
 (set-option :produce-models true)
-(declare-fun A () (Bag (Tuple Int Int)))
+(declare-fun A () (Table Int Int))
 (declare-fun c () Int)
 (declare-fun d () (Tuple Int Int))
 (assert

diff --git a/test/regress/cli/regress1/bags/product1.smt2 b/test/regress/cli/regress1/bags/product1.smt2
index 2f7f09058cfa3c4b59c55778f727131e752e982e..00e223a7fe597aee7413dd0e52b7b77434f2dd7f 100644 (file)
--- a/test/regress/cli/regress1/bags/product1.smt2
+++ b/test/regress/cli/regress1/bags/product1.smt2
@@ -1,8 +1,8 @@
 (set-logic ALL)
 (set-info :status sat)
-(declare-fun A () (Bag (Tuple String)))
-(declare-fun B () (Bag (Tuple Bool)))
-(declare-fun C () (Bag (Tuple String Bool)))
+(declare-fun A () (Table String))
+(declare-fun B () (Table Bool))
+(declare-fun C () (Table String Bool))
 (declare-fun x () (Tuple String))
 (declare-fun y () (Tuple Bool))
 (assert (= (bag.count x A) 5))

diff --git a/test/regress/cli/regress1/bags/product2.smt2 b/test/regress/cli/regress1/bags/product2.smt2
index ee7d1712feff4449af83d8ef95eb0607f9e00cb1..c230c8733962a423093beb6474364b7b0c16adb6 100644 (file)
--- a/test/regress/cli/regress1/bags/product2.smt2
+++ b/test/regress/cli/regress1/bags/product2.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL)
 (set-info :status unsat)
-(declare-fun A () (Bag (Tuple Int Int Int)))
-(declare-fun B () (Bag (Tuple Int Int Int)))
+(declare-fun A () (Table Int Int Int))
+(declare-fun B () (Table Int Int Int))
 (declare-fun x () (Tuple Int Int Int))
 (assert (= x (tuple 1 2 3)))
 (declare-fun y () (Tuple Int Int Int))

diff --git a/test/regress/cli/regress1/bags/product3.smt2 b/test/regress/cli/regress1/bags/product3.smt2
index 8e62f55ca6503aec47d60223b6ff8ddd18287229..e2c2286aad4d4e0e3368ca99f6f693400b4ef6ee 100644 (file)
--- a/test/regress/cli/regress1/bags/product3.smt2
+++ b/test/regress/cli/regress1/bags/product3.smt2
@@ -2,9 +2,9 @@
 
 (set-info :status sat)
 
-(declare-fun A () (Bag (Tuple Int Int Int)))
-(declare-fun B () (Bag (Tuple Int Int Int)))
-(declare-fun C () (Bag (Tuple Int Int Int Int Int Int)))
+(declare-fun A () (Table Int Int Int))
+(declare-fun B () (Table Int Int Int))
+(declare-fun C () (Table Int Int Int Int Int Int))
 
 (assert (= C (table.product A B)))
 

diff --git a/test/regress/cli/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2 b/test/regress/cli/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2
index e5cc1a503a7d5289db2f89501ca155cfc1d04551..54e51e091e53ce0481fa2a717ceb088851bfbebb 100644 (file)
--- a/test/regress/cli/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2
+++ b/test/regress/cli/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2
@@ -15,7 +15,7 @@
 (declare-datatypes ((|__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE| 0)) (((|__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_ctor| (O MOPERATION) (T TEAR_TYPE) (RR ORDER) (A ATOM) (B SDBLOCK_TYPE) (M (Set BINT)) (V VALUE_TYPE)))))
 
 
-(declare-datatypes ((|__cvc5_record_E_(Set ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_)_PO_(Set (Tuple ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_ ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_))| 0)) (((|__cvc5_record_E_(Set ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_)_PO_(Set (Tuple ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_ ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_))_ctor| (E (Set |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)) (PO (Set (Tuple |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE| |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)))))))
+(declare-datatypes ((|__cvc5_record_E_(Set ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_)_PO_(Relation ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_ ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_)| 0)) (((|__cvc5_record_E_(Set ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_)_PO_(Relation ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_ ___cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE_)_ctor| (E (Set |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)) (PO (Relation |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE| |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|))))))
 
 (declare-fun m1 () SDBLOCK_TYPE)
 (declare-fun ow1 () |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)
@@ -26,6 +26,6 @@
 (assert (and (and (and (and (and (and (= (O or2) R) (= (T or2) TEAR_FALSE)) (= (RR or2) U)) (= (A or2) NA)) (= (B or2) m1)) (= (M or2) (set.singleton I0))) (= (V or2) v2)))
 (declare-fun ev_set () (Set |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|))
 (assert (= ev_set (set.union (set.singleton ow1) (set.singleton or2))))
-(declare-fun RF () (Set (Tuple |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE| |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)))
+(declare-fun RF () (Relation |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE| |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|))
 (assert (forall ((r |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|) (w |__cvc5_record_O_MOPERATION_T_TEAR_TYPE_R_ORDER_A_ATOM_B_SDBLOCK_TYPE_M_(Set BINT)_V_VALUE_TYPE|)) (=> (and (set.member r ev_set) (set.member w ev_set)) (= (set.member (tuple r w) RF) (and (= (O r) R) (= (O w) W))))))
 (check-sat)

diff --git a/test/regress/cli/regress1/rels/addr_book_1.cvc.smt2 b/test/regress/cli/regress1/rels/addr_book_1.cvc.smt2
index 783c90b780758467084056b06ff14732201d4df5..9358ad3f96525c811fabc543f32d046e7c9f19d7 100644 (file)
--- a/test/regress/cli/regress1/rels/addr_book_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/addr_book_1.cvc.smt2
@@ -5,12 +5,12 @@
 
 
 
-(declare-fun Target () (Set (Tuple Atom)))
-(declare-fun Name () (Set (Tuple Atom)))
-(declare-fun Addr () (Set (Tuple Atom)))
-(declare-fun Book () (Set (Tuple Atom)))
-(declare-fun names () (Set (Tuple Atom Atom)))
-(declare-fun addr () (Set (Tuple Atom Atom Atom)))
+(declare-fun Target () (Relation Atom))
+(declare-fun Name () (Relation Atom))
+(declare-fun Addr () (Relation Atom))
+(declare-fun Book () (Relation Atom))
+(declare-fun names () (Relation Atom Atom))
+(declare-fun addr () (Relation Atom Atom Atom))
 (declare-fun b1 () Atom)
 (declare-fun b1_tup () (Tuple Atom))
 (assert (= b1_tup (tuple b1)))
@@ -31,7 +31,7 @@
 (declare-fun t_tup () (Tuple Atom))
 (assert (= t_tup (tuple t)))
 (assert (set.member t_tup Target))
-(assert (= (rel.join (set.singleton m_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Set (Tuple Atom)))))
+(assert (= (rel.join (set.singleton m_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Relation Atom))))
 (assert (= (rel.join (set.singleton b2_tup) addr) (set.union (rel.join (set.singleton b1_tup) addr) (set.singleton (tuple m t)))))
 (assert (= (rel.join (set.singleton b3_tup) addr) (set.minus (rel.join (set.singleton b2_tup) addr) (set.singleton (tuple m t)))))
 (assert (not (= (rel.join (set.singleton b1_tup) addr) (rel.join (set.singleton b3_tup) addr))))

diff --git a/test/regress/cli/regress1/rels/addr_book_1_1.cvc.smt2 b/test/regress/cli/regress1/rels/addr_book_1_1.cvc.smt2
index 3f5c39b5d37cbe034b6056f4d0da5a13c3836993..8f12ab292a836d75d408512b0b38b3fe16374c6f 100644 (file)
--- a/test/regress/cli/regress1/rels/addr_book_1_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/addr_book_1_1.cvc.smt2
@@ -5,12 +5,12 @@
 
 
 
-(declare-fun Target () (Set (Tuple Atom)))
-(declare-fun Name () (Set (Tuple Atom)))
-(declare-fun Addr () (Set (Tuple Atom)))
-(declare-fun Book () (Set (Tuple Atom)))
-(declare-fun names () (Set (Tuple Atom Atom)))
-(declare-fun addr () (Set (Tuple Atom Atom Atom)))
+(declare-fun Target () (Relation Atom))
+(declare-fun Name () (Relation Atom))
+(declare-fun Addr () (Relation Atom))
+(declare-fun Book () (Relation Atom))
+(declare-fun names () (Relation Atom Atom))
+(declare-fun addr () (Relation Atom Atom Atom))
 (declare-fun b1 () Atom)
 (declare-fun b1_tup () (Tuple Atom))
 (assert (= b1_tup (tuple b1)))
@@ -31,7 +31,7 @@
 (declare-fun t_tup () (Tuple Atom))
 (assert (= t_tup (tuple t)))
 (assert (set.member t_tup Target))
-(assert (= (rel.join (set.singleton m_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Set (Tuple Atom)))))
+(assert (= (rel.join (set.singleton m_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Relation Atom))))
 (assert (= (rel.join (set.singleton b2_tup) addr) (set.union (rel.join (set.singleton b1_tup) addr) (set.singleton (tuple m t)))))
 (assert (= (rel.join (set.singleton b3_tup) addr) (set.minus (rel.join (set.singleton b2_tup) addr) (set.singleton (tuple m t)))))
 (assert (= (rel.join (set.singleton b1_tup) addr) (rel.join (set.singleton b3_tup) addr)))

diff --git a/test/regress/cli/regress1/rels/bv1-unit.cvc.smt2 b/test/regress/cli/regress1/rels/bv1-unit.cvc.smt2
index 09858de2414695bbd0e6be41db81c72c3a0477e9..a6096f1a6c7668868cbef1ca1b633f1fb3365448 100644 (file)
--- a/test/regress/cli/regress1/rels/bv1-unit.cvc.smt2
+++ b/test/regress/cli/regress1/rels/bv1-unit.cvc.smt2
@@ -3,8 +3,8 @@
 (set-logic ALL)
 (declare-datatypes ((unit 0)) (((u))))
 
-(declare-fun x () (Set (Tuple (_ BitVec 1) unit (_ BitVec 1))))
-(declare-fun y () (Set (Tuple (_ BitVec 1) unit (_ BitVec 1))))
+(declare-fun x () (Relation (_ BitVec 1) unit (_ BitVec 1)))
+(declare-fun y () (Relation (_ BitVec 1) unit (_ BitVec 1)))
 (declare-fun a () (_ BitVec 1))
 (declare-fun b () (_ BitVec 1))
 (declare-fun c () (_ BitVec 1))

diff --git a/test/regress/cli/regress1/rels/bv1-unitb.cvc.smt2 b/test/regress/cli/regress1/rels/bv1-unitb.cvc.smt2
index cec025723740e00bba57ab603c96c4389f215e70..2c0b61ed20b676aeda9b5b79130bd5d5d4b27f30 100644 (file)
--- a/test/regress/cli/regress1/rels/bv1-unitb.cvc.smt2
+++ b/test/regress/cli/regress1/rels/bv1-unitb.cvc.smt2
@@ -3,8 +3,8 @@
 (set-logic ALL)
 (declare-datatypes ((unitb 0)) (((ub (data (_ BitVec 1))))))
 
-(declare-fun x () (Set (Tuple (_ BitVec 1) unitb (_ BitVec 1))))
-(declare-fun y () (Set (Tuple (_ BitVec 1) unitb (_ BitVec 1))))
+(declare-fun x () (Relation (_ BitVec 1) unitb (_ BitVec 1)))
+(declare-fun y () (Relation (_ BitVec 1) unitb (_ BitVec 1)))
 (declare-fun a () (_ BitVec 1))
 (declare-fun b () (_ BitVec 1))
 (declare-fun c () (_ BitVec 1))

diff --git a/test/regress/cli/regress1/rels/bv1.cvc.smt2 b/test/regress/cli/regress1/rels/bv1.cvc.smt2
index c317baedf0fd793f257925f2a5994bba2ecb0c2e..06d43ebe3952df3bae3d2cc9f300b2194cf043a6 100644 (file)
--- a/test/regress/cli/regress1/rels/bv1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/bv1.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple (_ BitVec 1) (_ BitVec 1))))
-(declare-fun y () (Set (Tuple (_ BitVec 1) (_ BitVec 1))))
+(declare-fun x () (Relation (_ BitVec 1) (_ BitVec 1)))
+(declare-fun y () (Relation (_ BitVec 1) (_ BitVec 1)))
 (declare-fun a () (_ BitVec 1))
 (declare-fun b () (_ BitVec 1))
 (declare-fun c () (_ BitVec 1))

diff --git a/test/regress/cli/regress1/rels/bv1p-sat.cvc.smt2 b/test/regress/cli/regress1/rels/bv1p-sat.cvc.smt2
index 367a44c11f26a3c49ef104d5ed1dab588c9cd512..50b03fc655cd6cfb106400e00f42ac5fae3577dd 100644 (file)
--- a/test/regress/cli/regress1/rels/bv1p-sat.cvc.smt2
+++ b/test/regress/cli/regress1/rels/bv1p-sat.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple (_ BitVec 1) (_ BitVec 1))))
-(declare-fun y () (Set (Tuple (_ BitVec 1) (_ BitVec 1))))
+(declare-fun x () (Relation (_ BitVec 1) (_ BitVec 1)))
+(declare-fun y () (Relation (_ BitVec 1) (_ BitVec 1)))
 (declare-fun a () (Tuple (_ BitVec 1) (_ BitVec 1)))
 (declare-fun b () (Tuple (_ BitVec 1) (_ BitVec 1)))
 (declare-fun c () (Tuple (_ BitVec 1) (_ BitVec 1)))

diff --git a/test/regress/cli/regress1/rels/bv1p.cvc.smt2 b/test/regress/cli/regress1/rels/bv1p.cvc.smt2
index 262826b3cc0578dd4e52e1ac22470ca979e3cb61..7c95d1472d7c98f9368218f7fc527707e9b1f31b 100644 (file)
--- a/test/regress/cli/regress1/rels/bv1p.cvc.smt2
+++ b/test/regress/cli/regress1/rels/bv1p.cvc.smt2
@@ -3,8 +3,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple (_ BitVec 1) (_ BitVec 1))))
-(declare-fun y () (Set (Tuple (_ BitVec 1) (_ BitVec 1))))
+(declare-fun x () (Relation (_ BitVec 1) (_ BitVec 1)))
+(declare-fun y () (Relation (_ BitVec 1) (_ BitVec 1)))
 (declare-fun a () (Tuple (_ BitVec 1) (_ BitVec 1)))
 (declare-fun b () (Tuple (_ BitVec 1) (_ BitVec 1)))
 (declare-fun c () (Tuple (_ BitVec 1) (_ BitVec 1)))

diff --git a/test/regress/cli/regress1/rels/bv2.cvc.smt2 b/test/regress/cli/regress1/rels/bv2.cvc.smt2
index 9ea472819f665d5a44d5460991bf356d8730e63c..3b67b0b5c738c0f7f54390aaedc08653b3fb5f73 100644 (file)
--- a/test/regress/cli/regress1/rels/bv2.cvc.smt2
+++ b/test/regress/cli/regress1/rels/bv2.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple (_ BitVec 2) (_ BitVec 2))))
-(declare-fun y () (Set (Tuple (_ BitVec 2) (_ BitVec 2))))
+(declare-fun x () (Relation (_ BitVec 2) (_ BitVec 2)))
+(declare-fun y () (Relation (_ BitVec 2) (_ BitVec 2)))
 (declare-fun a () (_ BitVec 2))
 (declare-fun b () (_ BitVec 2))
 (declare-fun c () (_ BitVec 2))

diff --git a/test/regress/cli/regress1/rels/garbage_collect.cvc.smt2 b/test/regress/cli/regress1/rels/garbage_collect.cvc.smt2
index 8406b4ab8154b1b36960010c86601fa53ff2ee75..d45f7d6c22315aad92f5b0219c6cb8469e7c3c77 100644 (file)
--- a/test/regress/cli/regress1/rels/garbage_collect.cvc.smt2
+++ b/test/regress/cli/regress1/rels/garbage_collect.cvc.smt2
@@ -8,10 +8,10 @@
 
 
 
-(declare-fun h0 () (Set (Tuple H_TYPE)))
-(declare-fun h1 () (Set (Tuple H_TYPE)))
-(declare-fun h2 () (Set (Tuple H_TYPE)))
-(declare-fun h3 () (Set (Tuple H_TYPE)))
+(declare-fun h0 () (Relation H_TYPE))
+(declare-fun h1 () (Relation H_TYPE))
+(declare-fun h2 () (Relation H_TYPE))
+(declare-fun h3 () (Relation H_TYPE))
 (declare-fun s0 () H_TYPE)
 (declare-fun s1 () H_TYPE)
 (declare-fun s2 () H_TYPE)
@@ -20,10 +20,10 @@
 (assert (= h1 (set.singleton (tuple s1))))
 (assert (= h2 (set.singleton (tuple s2))))
 (assert (= h3 (set.singleton (tuple s3))))
-(declare-fun ref () (Set (Tuple H_TYPE Obj Obj)))
-(declare-fun mark () (Set (Tuple H_TYPE Obj)))
-(declare-fun empty_obj_set () (Set (Tuple Obj)))
-(assert (= empty_obj_set (as set.empty (Set (Tuple Obj)))))
+(declare-fun ref () (Relation H_TYPE Obj Obj))
+(declare-fun mark () (Relation H_TYPE Obj))
+(declare-fun empty_obj_set () (Relation Obj))
+(assert (= empty_obj_set (as set.empty (Relation Obj))))
 (declare-fun root () Obj)
 (declare-fun live () Obj)
 (assert (= (rel.join h1 mark) empty_obj_set))

diff --git a/test/regress/cli/regress1/rels/iden_1_1.cvc.smt2 b/test/regress/cli/regress1/rels/iden_1_1.cvc.smt2
index 55daa9a41217e1bd66545e906d36d21b46f046a5..ab9d1766afed9c1d0a28699750c1ed1b01727c51 100644 (file)
--- a/test/regress/cli/regress1/rels/iden_1_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/iden_1_1.cvc.smt2
@@ -4,16 +4,16 @@
 (set-logic ALL)
 (declare-sort Atom 0)
 
-(declare-fun x () (Set (Tuple Atom Atom)))
-(declare-fun t () (Set (Tuple Atom)))
-(declare-fun univ () (Set (Tuple Atom)))
-(declare-fun univ2 () (Set (Tuple Atom Atom)))
+(declare-fun x () (Relation Atom Atom))
+(declare-fun t () (Relation Atom))
+(declare-fun univ () (Relation Atom))
+(declare-fun univ2 () (Relation Atom Atom))
 (declare-fun a () Atom)
 (declare-fun b () Atom)
 (declare-fun c () Atom)
 (declare-fun d () Atom)
-(assert (= univ (as set.universe (Set (Tuple Atom)))))
-(assert (= univ2 (as set.universe (Set (Tuple Atom Atom)))))
+(assert (= univ (as set.universe (Relation Atom))))
+(assert (= univ2 (as set.universe (Relation Atom Atom))))
 (assert (= univ2 (rel.product univ univ)))
 (assert (set.member (tuple a b) x))
 (assert (set.member (tuple c d) x))

diff --git a/test/regress/cli/regress1/rels/join-eq-structure-and.cvc.smt2 b/test/regress/cli/regress1/rels/join-eq-structure-and.cvc.smt2
index f4203e5eca40758b3d849f57ac246efb5d2bdd64..0ce18fc9b255b01ec9eee081f57d08bf9ab49288 100644 (file)
--- a/test/regress/cli/regress1/rels/join-eq-structure-and.cvc.smt2
+++ b/test/regress/cli/regress1/rels/join-eq-structure-and.cvc.smt2
@@ -2,13 +2,13 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-datatypes ((unit 0)) (((u))))
 
 
-(declare-fun w () (Set (Tuple Int unit)))
-(declare-fun z () (Set (Tuple unit Int)))
+(declare-fun w () (Relation Int unit))
+(declare-fun z () (Relation unit Int))
 (assert (let ((_let_1 (rel.join w z))) (let ((_let_2 (rel.join x y))) (and (= _let_2 _let_1) (= _let_2 (rel.transpose _let_1))))))
 (assert (set.member (tuple 0 1) (rel.join x y)))
 (declare-fun t () Int)

diff --git a/test/regress/cli/regress1/rels/join-eq-structure.cvc.smt2 b/test/regress/cli/regress1/rels/join-eq-structure.cvc.smt2
index bad15f3c88ba29e85fc801f4cab6eaa80eb8a9b0..f75859ff589562520e85e82f1a548d4f71cde594 100644 (file)
--- a/test/regress/cli/regress1/rels/join-eq-structure.cvc.smt2
+++ b/test/regress/cli/regress1/rels/join-eq-structure.cvc.smt2
@@ -2,13 +2,13 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-datatypes ((unit 0)) (((u))))
 
 
-(declare-fun w () (Set (Tuple Int unit)))
-(declare-fun z () (Set (Tuple unit Int)))
+(declare-fun w () (Relation Int unit))
+(declare-fun z () (Relation unit Int))
 (assert (let ((_let_1 (rel.join w z))) (let ((_let_2 (rel.join x y))) (or (= _let_2 _let_1) (= _let_2 (rel.transpose _let_1))))))
 (assert (set.member (tuple 0 1) (rel.join x y)))
 (declare-fun t () Int)

diff --git a/test/regress/cli/regress1/rels/joinImg_0_1.cvc.smt2 b/test/regress/cli/regress1/rels/joinImg_0_1.cvc.smt2
index 1918e2ad46c917d77b6574294377eb87c8c1ac92..89a4efe41b7c7c48bf0c9ecee245bd42186ba2b5 100644 (file)
--- a/test/regress/cli/regress1/rels/joinImg_0_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/joinImg_0_1.cvc.smt2
@@ -3,11 +3,11 @@
 (set-logic ALL)
 (set-option :sets-ext true)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
-(declare-fun t () (Set (Tuple Int)))
-(declare-fun u () (Set (Tuple Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
+(declare-fun t () (Relation Int))
+(declare-fun u () (Relation Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress1/rels/joinImg_0_2.cvc.smt2 b/test/regress/cli/regress1/rels/joinImg_0_2.cvc.smt2
index 6c822db5b8c1de3533e68f3f37e835708006c04b..7f3f12602a6346f3ab03c60c7a2499906161e58f 100644 (file)
--- a/test/regress/cli/regress1/rels/joinImg_0_2.cvc.smt2
+++ b/test/regress/cli/regress1/rels/joinImg_0_2.cvc.smt2
@@ -3,12 +3,12 @@
 (set-option :sets-ext true)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
-(declare-fun t () (Set (Tuple Int)))
-(declare-fun u () (Set (Tuple Int)))
-(declare-fun univ () (Set (Tuple Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
+(declare-fun t () (Relation Int))
+(declare-fun u () (Relation Int))
+(declare-fun univ () (Relation Int))
 (declare-fun z () (Tuple Int Int))
 (assert (= z (tuple 1 2)))
 (declare-fun zt () (Tuple Int Int))

diff --git a/test/regress/cli/regress1/rels/joinImg_1.cvc.smt2 b/test/regress/cli/regress1/rels/joinImg_1.cvc.smt2
index 457e66cef51d7dbf903ad3f8edb0572469050e4f..ca698bee9b1e61e2c1f187c73705e5662ebf60f7 100644 (file)
--- a/test/regress/cli/regress1/rels/joinImg_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/joinImg_1.cvc.smt2
@@ -3,10 +3,10 @@
 (set-logic ALL)
 (set-option :sets-ext true)
 (declare-sort Atom 0)
-(declare-fun x () (Set (Tuple Atom Atom)))
-(declare-fun y () (Set (Tuple Atom Atom)))
-(declare-fun r () (Set (Tuple Atom Atom)))
-(declare-fun t () (Set (Tuple Atom)))
+(declare-fun x () (Relation Atom Atom))
+(declare-fun y () (Relation Atom Atom))
+(declare-fun r () (Relation Atom Atom))
+(declare-fun t () (Relation Atom))
 (declare-fun a () Atom)
 (declare-fun b () Atom)
 (declare-fun c () Atom)

diff --git a/test/regress/cli/regress1/rels/joinImg_1_1.cvc.smt2 b/test/regress/cli/regress1/rels/joinImg_1_1.cvc.smt2
index 171623d194bbfa3fd48688a9bbba1289dca24e2e..c433c5906175cc242e93f66ce576e0459b778b15 100644 (file)
--- a/test/regress/cli/regress1/rels/joinImg_1_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/joinImg_1_1.cvc.smt2
@@ -3,10 +3,10 @@
 (set-logic ALL)
 (set-option :sets-ext true)
 (declare-sort Atom 0)
-(declare-fun x () (Set (Tuple Atom Atom)))
-(declare-fun y () (Set (Tuple Atom Atom)))
-(declare-fun r () (Set (Tuple Atom Atom)))
-(declare-fun t () (Set (Tuple Atom)))
+(declare-fun x () (Relation Atom Atom))
+(declare-fun y () (Relation Atom Atom))
+(declare-fun r () (Relation Atom Atom))
+(declare-fun t () (Relation Atom))
 (declare-fun a () Atom)
 (declare-fun b () Atom)
 (declare-fun c () Atom)

diff --git a/test/regress/cli/regress1/rels/joinImg_2.cvc.smt2 b/test/regress/cli/regress1/rels/joinImg_2.cvc.smt2
index 56d45607f531f9df668264c2e50df0eff122bd74..d23509a487589a04de72c360bd838cdb0228584e 100644 (file)
--- a/test/regress/cli/regress1/rels/joinImg_2.cvc.smt2
+++ b/test/regress/cli/regress1/rels/joinImg_2.cvc.smt2
@@ -3,10 +3,10 @@
 (set-logic ALL)
 (set-option :sets-ext true)
 (declare-sort Atom 0)
-(declare-fun x () (Set (Tuple Atom Atom)))
-(declare-fun y () (Set (Tuple Atom Atom)))
-(declare-fun r () (Set (Tuple Atom Atom)))
-(declare-fun t () (Set (Tuple Atom)))
+(declare-fun x () (Relation Atom Atom))
+(declare-fun y () (Relation Atom Atom))
+(declare-fun r () (Relation Atom Atom))
+(declare-fun t () (Relation Atom))
 (declare-fun a () Atom)
 (declare-fun b () Atom)
 (declare-fun c () Atom)

diff --git a/test/regress/cli/regress1/rels/joinImg_2_1.cvc.smt2 b/test/regress/cli/regress1/rels/joinImg_2_1.cvc.smt2
index a20218fc16bea9ca6ca17bb0ea5c024425c56649..7b762729437e5864cae46ecd07785d22a6cf5a99 100644 (file)
--- a/test/regress/cli/regress1/rels/joinImg_2_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/joinImg_2_1.cvc.smt2
@@ -3,10 +3,10 @@
 (set-logic ALL)
 (set-option :sets-ext true)
 (declare-sort Atom 0)
-(declare-fun x () (Set (Tuple Atom Atom)))
-(declare-fun y () (Set (Tuple Atom Atom)))
-(declare-fun r () (Set (Tuple Atom Atom)))
-(declare-fun t () (Set (Tuple Atom)))
+(declare-fun x () (Relation Atom Atom))
+(declare-fun y () (Relation Atom Atom))
+(declare-fun r () (Relation Atom Atom))
+(declare-fun t () (Relation Atom))
 (declare-fun a () Atom)
 (declare-fun b () Atom)
 (declare-fun c () Atom)

diff --git a/test/regress/cli/regress1/rels/prod-mod-eq.cvc.smt2 b/test/regress/cli/regress1/rels/prod-mod-eq.cvc.smt2
index 738ccf8e8c92ee5fd9fd6b3d5e3e10f42bd1f166..838fe683bf51ee8205ab4580c03d8f1eb5140f4c 100644 (file)
--- a/test/regress/cli/regress1/rels/prod-mod-eq.cvc.smt2
+++ b/test/regress/cli/regress1/rels/prod-mod-eq.cvc.smt2
@@ -3,13 +3,13 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int Int Int)))
-(declare-fun z1 () (Set (Tuple Int Int)))
-(declare-fun w1 () (Set (Tuple Int Int)))
-(declare-fun z2 () (Set (Tuple Int Int)))
-(declare-fun w2 () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int Int Int))
+(declare-fun z1 () (Relation Int Int))
+(declare-fun w1 () (Relation Int Int))
+(declare-fun z2 () (Relation Int Int))
+(declare-fun w2 () (Relation Int Int))
 (assert (not (= z (rel.product x y))))
 (assert (set.member (tuple 0 1 2 3) z))
 (assert (set.member (tuple 0 1) z1))

diff --git a/test/regress/cli/regress1/rels/prod-mod-eq2.cvc.smt2 b/test/regress/cli/regress1/rels/prod-mod-eq2.cvc.smt2
index d9add50adbf02710462c425040cb8d628ea0c021..b8e8c8bd99e207a69461f42b9a286c19f7e3ca27 100644 (file)
--- a/test/regress/cli/regress1/rels/prod-mod-eq2.cvc.smt2
+++ b/test/regress/cli/regress1/rels/prod-mod-eq2.cvc.smt2
@@ -3,14 +3,14 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int Int Int)))
-(declare-fun z1 () (Set (Tuple Int Int)))
-(declare-fun w1 () (Set (Tuple Int Int)))
-(declare-fun z2 () (Set (Tuple Int Int)))
-(declare-fun w2 () (Set (Tuple Int Int)))
-(declare-fun P ((Set (Tuple Int Int Int Int))) Bool)
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int Int Int))
+(declare-fun z1 () (Relation Int Int))
+(declare-fun w1 () (Relation Int Int))
+(declare-fun z2 () (Relation Int Int))
+(declare-fun w2 () (Relation Int Int))
+(declare-fun P ((Relation Int Int Int Int)) Bool)
 (assert (= z (rel.product x y)))
 (assert (P z))
 (assert (not (P (set.singleton (tuple 0 1 2 3)))))

diff --git a/test/regress/cli/regress1/rels/qgu-fuzz-relations-2.smt2 b/test/regress/cli/regress1/rels/qgu-fuzz-relations-2.smt2
index dfb3b0750a30621b9d217e01e9764ac88f39c1d4..fb02a5342bc8728f1ef5b959d100c8458f4d956f 100644 (file)
--- a/test/regress/cli/regress1/rels/qgu-fuzz-relations-2.smt2
+++ b/test/regress/cli/regress1/rels/qgu-fuzz-relations-2.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL)
 (set-info :status sat)
-(declare-fun a () (Set (Tuple Int Int)))
-(declare-fun b () (Set (Tuple Int Int)))
+(declare-fun a () (Relation Int Int))
+(declare-fun b () (Relation Int Int))
 (declare-fun c () Int)
 (declare-fun d () (Tuple Int Int))
 (assert (and (= a (set.singleton (tuple (+ c 1) 1))) (= (rel.tclosure b) (rel.join a a))))

diff --git a/test/regress/cli/regress1/rels/qgu-fuzz-relations-3-upwards.smt2 b/test/regress/cli/regress1/rels/qgu-fuzz-relations-3-upwards.smt2
index 4e4f2d534554ab58b0e9baf84b6448ba197c06e3..199ffeede1d8a1ef4a89636c8216aad7cd6e85f7 100644 (file)
--- a/test/regress/cli/regress1/rels/qgu-fuzz-relations-3-upwards.smt2
+++ b/test/regress/cli/regress1/rels/qgu-fuzz-relations-3-upwards.smt2
@@ -1,11 +1,11 @@
 (set-logic ALL)
 (set-info :status sat)
-(declare-fun b () (Set (Tuple Int Int)))
+(declare-fun b () (Relation Int Int))
 (assert 
-(= (rel.join b (rel.tclosure (rel.join b b))) (as set.empty (Set (Tuple Int Int))))
+(= (rel.join b (rel.tclosure (rel.join b b))) (as set.empty (Relation Int Int)))
 )
 (assert
-(distinct b (as set.empty (Set (Tuple Int Int))))
+(distinct b (as set.empty (Relation Int Int)))
 )
-(assert (= (rel.join b b) (as set.empty (Set (Tuple Int Int)))))
+(assert (= (rel.join b b) (as set.empty (Relation Int Int))))
 (check-sat)

diff --git a/test/regress/cli/regress1/rels/rel_complex_3.cvc.smt2 b/test/regress/cli/regress1/rels/rel_complex_3.cvc.smt2
index 8269daf426aa91a4c6165bcc7a5bf13a21ac6f12..e09d8b79402faa189ff539a46d758df7071806ee 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_complex_3.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_complex_3.cvc.smt2
@@ -2,11 +2,11 @@
 (set-option :incremental true)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
-(declare-fun w () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
+(declare-fun w () (Relation Int Int))
 (declare-fun f () (Tuple Int Int))
 (assert (= f (tuple 3 1)))
 (assert (set.member f x))

diff --git a/test/regress/cli/regress1/rels/rel_complex_4.cvc.smt2 b/test/regress/cli/regress1/rels/rel_complex_4.cvc.smt2
index 134a99c73371b4e50b8ed2a8751f2450ae6aa20f..b2bee7d6dc00521397626a2a5545e0bf480acde0 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_complex_4.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_complex_4.cvc.smt2
@@ -2,11 +2,11 @@
 (set-option :incremental true)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
-(declare-fun w () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
+(declare-fun w () (Relation Int Int))
 (declare-fun f () (Tuple Int Int))
 (assert (= f (tuple 3 1)))
 (assert (set.member f x))

diff --git a/test/regress/cli/regress1/rels/rel_complex_5.cvc.smt2 b/test/regress/cli/regress1/rels/rel_complex_5.cvc.smt2
index ed894518e8c8b8727ca123c5e9d86a0c4da60948..2d491c66a57dc6325993e27a7ae4b9add3154e7c 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_complex_5.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_complex_5.cvc.smt2
@@ -3,11 +3,11 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
-(declare-fun w () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
+(declare-fun w () (Relation Int Int))
 (declare-fun f () (Tuple Int Int))
 (assert (= f (tuple 3 1)))
 (assert (set.member f x))

diff --git a/test/regress/cli/regress1/rels/rel_mix_0_1.cvc.smt2 b/test/regress/cli/regress1/rels/rel_mix_0_1.cvc.smt2
index 77a5f38fde39ee73826c9441e4185de0b85f9f8e..aeb9ff1faca379813718acf5b27aa386875f132c 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_mix_0_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_mix_0_1.cvc.smt2
@@ -3,12 +3,12 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
-(declare-fun w () (Set (Tuple Int)))
-(declare-fun z () (Set (Tuple Int)))
-(declare-fun r2 () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
+(declare-fun w () (Relation Int))
+(declare-fun z () (Relation Int))
+(declare-fun r2 () (Relation Int Int))
 (declare-fun d () (Tuple Int Int))
 (assert (= d (tuple 1 3)))
 (assert (set.member (tuple 1 3) y))

diff --git a/test/regress/cli/regress1/rels/rel_pressure_0.cvc.smt2 b/test/regress/cli/regress1/rels/rel_pressure_0.cvc.smt2
index e80fe01e2555ac138e34f2c5bcceeee2f52b7401..98f8fbcec2e261a20419ce6070c2195757bf2f92 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_pressure_0.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_pressure_0.cvc.smt2
@@ -2,10 +2,10 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (declare-fun a11 () (Tuple Int Int))
 (assert (= a11 (tuple 1 1)))
 (assert (set.member a11 x))

diff --git a/test/regress/cli/regress1/rels/rel_tc_10_1.cvc.smt2 b/test/regress/cli/regress1/rels/rel_tc_10_1.cvc.smt2
index 9e49c27317255688e1da24410eef46e1877a4be2..66ed16e2723f98b6fb32c3cd53a9e88e30fb729a 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_tc_10_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_tc_10_1.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-fun a () Int)
 (declare-fun b () Int)
 (declare-fun c () Int)

diff --git a/test/regress/cli/regress1/rels/rel_tc_4.cvc.smt2 b/test/regress/cli/regress1/rels/rel_tc_4.cvc.smt2
index 1b2a6173da65165ec57106ac8c02c08a482957eb..fabdf3338fc5ae0b8d642c67a7c962c550caba1a 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_tc_4.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_tc_4.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (declare-fun a () Int)
 (declare-fun b () Int)
 (declare-fun c () Int)

diff --git a/test/regress/cli/regress1/rels/rel_tc_4_1.cvc.smt2 b/test/regress/cli/regress1/rels/rel_tc_4_1.cvc.smt2
index 68ca97c2af649a7857863926f9bc4106845c3381..17ebc8f38a164ac927043f6899996cf172db1315 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_tc_4_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_tc_4_1.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
 (assert (= y (rel.join (rel.tclosure x) x)))
 (assert (not (= y (rel.tclosure x))))
 (check-sat)

diff --git a/test/regress/cli/regress1/rels/rel_tc_5_1.cvc.smt2 b/test/regress/cli/regress1/rels/rel_tc_5_1.cvc.smt2
index 0caa98002233ef1e7546b70a430c56a69613b717..0bb4e486360af986e52fe4204d3f7e29ff67c704 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_tc_5_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_tc_5_1.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (assert (= y (rel.tclosure x)))
 (assert (not (= y (rel.join (rel.join x x) x))))
 (check-sat)

diff --git a/test/regress/cli/regress1/rels/rel_tc_6.cvc.smt2 b/test/regress/cli/regress1/rels/rel_tc_6.cvc.smt2
index 8e2e1cae2b9c2f0c52eaa21aacc31cea3a265140..fa0246289229f86e9197d2216d3b352a010ea8f3 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_tc_6.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_tc_6.cvc.smt2
@@ -2,8 +2,8 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
 (assert (= y (rel.tclosure x)))
 (assert (not (set.subset (rel.join (rel.join x x) x) y)))
 (check-sat)

diff --git a/test/regress/cli/regress1/rels/rel_tc_9_1.cvc.smt2 b/test/regress/cli/regress1/rels/rel_tc_9_1.cvc.smt2
index 02efe912bea02bc2575d53b46de07cf72f215577..5f805b403607aef56501ff33c3d166b1568e4aca 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_tc_9_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_tc_9_1.cvc.smt2
@@ -2,10 +2,10 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun w () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun w () (Relation Int Int))
 (assert (= z (rel.tclosure x)))
 (assert (= w (rel.join x y)))
 (assert (set.member (tuple 2 2) z))

diff --git a/test/regress/cli/regress1/rels/rel_tp_2.cvc.smt2 b/test/regress/cli/regress1/rels/rel_tp_2.cvc.smt2
index ca8e1ba775246885f8b332a0c6655d26f17f8d79..dd614cf46b14b6dabe029d41c295f82f53e4b517 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_tp_2.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_tp_2.cvc.smt2
@@ -2,9 +2,9 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
 (assert (or (= z (rel.transpose y)) (= z (rel.transpose x))))
 (assert (not (= (rel.transpose z) y)))
 (assert (not (= (rel.transpose z) x)))

diff --git a/test/regress/cli/regress1/rels/rel_tp_join_2_1.cvc.smt2 b/test/regress/cli/regress1/rels/rel_tp_join_2_1.cvc.smt2
index 32a520d13e6c0e4f57b8f341b431be96577c692e..63c778b9d33109b5177337e20a1cdceca0e4b099 100644 (file)
--- a/test/regress/cli/regress1/rels/rel_tp_join_2_1.cvc.smt2
+++ b/test/regress/cli/regress1/rels/rel_tp_join_2_1.cvc.smt2
@@ -2,10 +2,10 @@
 (set-option :incremental false)
 (set-logic ALL)
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun z () (Relation Int Int))
+(declare-fun r () (Relation Int Int))
 (assert (set.member (tuple 7 1) x))
 (assert (set.member (tuple 2 3) x))
 (assert (set.member (tuple 7 3) y))

diff --git a/test/regress/cli/regress1/rels/set-strat.cvc.smt2 b/test/regress/cli/regress1/rels/set-strat.cvc.smt2
index a509780acebd0741e9789e18ed9f2cbcbd77469d..17960d47db212ed64bd68d179140e2a0d0277fb0 100644 (file)
--- a/test/regress/cli/regress1/rels/set-strat.cvc.smt2
+++ b/test/regress/cli/regress1/rels/set-strat.cvc.smt2
@@ -3,10 +3,10 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple Int Int)))
-(declare-fun y () (Set (Tuple Int Int)))
-(declare-fun w () (Set (Tuple Int Int)))
-(declare-fun z () (Set (Tuple (Set (Tuple Int Int)) (Set (Tuple Int Int)))))
+(declare-fun x () (Relation Int Int))
+(declare-fun y () (Relation Int Int))
+(declare-fun w () (Relation Int Int))
+(declare-fun z () (Relation (Relation Int Int) (Relation Int Int)))
 (declare-fun a () (Tuple Int Int))
 (declare-fun b () (Tuple Int Int))
 (assert (not (= a b)))

diff --git a/test/regress/cli/regress1/rels/strat.cvc.smt2 b/test/regress/cli/regress1/rels/strat.cvc.smt2
index b65251ca7997fa6c8f6016ae7730f57b3966085a..da06ba1a9ca10542b86766a549bb47a882ac115a 100644 (file)
--- a/test/regress/cli/regress1/rels/strat.cvc.smt2
+++ b/test/regress/cli/regress1/rels/strat.cvc.smt2
@@ -3,10 +3,10 @@
 (set-logic ALL)
 
 
-(declare-fun x () (Set (Tuple (Tuple Int Int) (Tuple Int Int))))
-(declare-fun y () (Set (Tuple (Tuple Int Int) (Tuple Int Int))))
-(declare-fun z () (Set (Tuple Int Int)))
-(declare-fun w () (Set (Tuple Int Int)))
+(declare-fun x () (Relation (Tuple Int Int) (Tuple Int Int)))
+(declare-fun y () (Relation (Tuple Int Int) (Tuple Int Int)))
+(declare-fun z () (Relation Int Int))
+(declare-fun w () (Relation Int Int))
 (declare-fun a () (Tuple Int Int))
 (declare-fun b () (Tuple Int Int))
 (declare-fun c () (Tuple (Tuple Int Int) (Tuple Int Int)))

diff --git a/test/regress/cli/regress1/sets/issue4124-need-check.smt2 b/test/regress/cli/regress1/sets/issue4124-need-check.smt2
index c06a753e1087726fc07442a82bc5a409f0d0ec68..22a238b56a36aeaae4877ee6184448cae5e8f607 100644 (file)
--- a/test/regress/cli/regress1/sets/issue4124-need-check.smt2
+++ b/test/regress/cli/regress1/sets/issue4124-need-check.smt2
@@ -1,9 +1,9 @@
 ; COMMAND-LINE: --sets-infer-as-lemmas --simplification=none
 ; EXPECT: sat
 (set-logic ALL)
-(declare-fun b () (Set (Tuple String Int))) 
-(declare-fun c () (Set (Tuple Int String))) 
-(declare-fun d () (Set (Tuple String String))) 
+(declare-fun b () (Relation String Int))
+(declare-fun c () (Relation Int String))
+(declare-fun d () (Relation String String))
 (declare-fun f () (Set Int)) 
 (declare-fun e () Int) 
 (assert (= b (set.insert (tuple "" 1)  (tuple "" 2) (set.singleton (tuple "" 4))))) 

diff --git a/test/regress/cli/regress1/sets/proj-issue164.smt2 b/test/regress/cli/regress1/sets/proj-issue164.smt2
index 5e343156eccc37e2f5413a8a09d828740a3b78ff..45e630acb2f43af6d61f4ede2484a0f179d154b9 100644 (file)
--- a/test/regress/cli/regress1/sets/proj-issue164.smt2
+++ b/test/regress/cli/regress1/sets/proj-issue164.smt2
@@ -1,8 +1,8 @@
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun b () (Set String))
-(declare-fun c () (Set (Tuple Int Int)))
-(declare-fun d () (Set (Tuple Int Int)))
+(declare-fun c () (Relation Int Int))
+(declare-fun d () (Relation Int Int))
 (declare-fun e () Int)
 (assert (distinct c (set.insert (tuple 0 0) (set.singleton (tuple 1 1)))))
 (assert (distinct d (rel.tclosure c)))

diff --git a/test/regress/cli/regress1/sets/sets-tuple-poly.cvc.smt2 b/test/regress/cli/regress1/sets/sets-tuple-poly.cvc.smt2
index 31d64cb49b42d843a3b13abbdab59077c173ae09..1f8f72b261f981eb2cb2ee9cb9f5a56f0c0a1bb2 100644 (file)
--- a/test/regress/cli/regress1/sets/sets-tuple-poly.cvc.smt2
+++ b/test/regress/cli/regress1/sets/sets-tuple-poly.cvc.smt2
@@ -3,8 +3,8 @@
 (set-option :incremental false)
 (set-option :sets-ext true)
 (set-logic ALL)
-(declare-fun a () (Set (Tuple Real Int)))
-(declare-fun b () (Set (Tuple Int Real)))
+(declare-fun a () (Relation Real Int))
+(declare-fun b () (Relation Int Real))
 (declare-fun x () (Tuple Real Real))
 (assert (let ((_let_1 0.0)) (not (= x (tuple _let_1 _let_1)))))
 (assert (set.member (tuple ((_ tuple.select 0) x) (to_int ((_ tuple.select 1) x))) a))