From: mudathirmahgoub Date: Wed, 13 Apr 2022 18:54:27 +0000 (-0500) Subject: Add Relation and Table types to SMTLib parser (#8605) X-Git-Tag: cvc5-1.0.1~266 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=12293a35d56ddefe51adba6d07f058f10b1dd20e;p=cvc5.git 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 f6e277329..b2d7245eb 100644 --- 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 s = solver.mkSetSort(cvc5::Sort tupleSort);`` | +| Relation Sort | ``(Relation , ..., )`` | ``Sort s = solver.mkSetSort(cvc5::Sort tupleSort);`` | +| | | | +| | which is a syntax sugar for | | +| | | | +| | ``(Set (Tuple , ..., ))`` | | +----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ | 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 2b0b23fa6..0b1c7989a 100644 --- 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 b1b4955f1..18cf25507 100644 --- 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 6bb806481..63dc823f2 100644 --- 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 323cd263b..7f5ed4315 100644 --- 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 971f1d832..145260bce 100644 --- 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 dd6bd004a..29262da32 100644 --- 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 0f22c5853..61d301074 100644 --- 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 00d9abc55..d6f16a79b 100644 --- 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 d1c93a45b..fd0b11fa7 100644 --- 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 +; 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 9bc85f268..aad0a3b15 100644 --- 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 11799ba79..c8aa67e73 100644 --- 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 +; 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 6db1e0e47..394c64609 100644 --- 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 75dc80d22..2ed094e25 100644 --- 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 64efc4aef..d6af1bb76 100644 --- 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 9dd334b5e..685bc60a6 100644 --- 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 652504a1a..b582f22f5 100644 --- 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 85d9cac6f..eb1c54e13 100644 --- 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 ee500f8ed..fc72055f6 100644 --- 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 0e9a61922..9f340a52f 100644 --- 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 6804a4df8..f5e493d9b 100644 --- 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 5a320b1d0..42f425db6 100644 --- 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 a72a26b9b..285dff123 100644 --- 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 389260e17..21d1a5d20 100644 --- 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 4b7fede6c..a7120a6c2 100644 --- 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 018b83e27..ba2045ab8 100644 --- 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 4489b1a16..e64c15c4d 100644 --- 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 638964931..60260fd7e 100644 --- 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 357f37922..e2ff7fa46 100644 --- 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 3359f2f62..05cc2ec11 100644 --- 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 5c1f114a5..553e6b08e 100644 --- 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 6459b9f03..b95dea83b 100644 --- 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 1fb714112..b62755e57 100644 --- 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 fc9fad09b..96824a5ea 100644 --- 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 cd256a476..702711b85 100644 --- 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 81ab335aa..9303725a8 100644 --- 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 a8b1fd3c0..04a6d039b 100644 --- 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 cdf337276..aa7c1f1af 100644 --- 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 a0469b3e9..ed431835a 100644 --- 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 544068b50..4a4f491ab 100644 --- 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 a3fb21eed..14fa852e3 100644 --- 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 178208ff7..e258db77f 100644 --- 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 7afe4e4a9..a8eaeae08 100644 --- 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 665513498..d29bac00e 100644 --- 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 183aff148..4eb6bb222 100644 --- 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 8a2dc2749..d0e49e7d9 100644 --- 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 7940e9898..73234c4a2 100644 --- 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 5de2d82d2..769d5489b 100644 --- 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 df9764a5c..7dc763f51 100644 --- 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 620f8d3d0..0687fe0b1 100644 --- 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 5e359b538..240e7c0e3 100644 --- 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 9f2dd1190..21fa6fa10 100644 --- 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 aed2badf7..7995765aa 100644 --- 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 213d75bdc..97506ece9 100644 --- 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 b66f1c6ed..20557bf7a 100644 --- 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 4ebd54b90..f9f143644 100644 --- 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 e67f5d59b..4c4e42685 100644 --- 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 7806c48ba..77d48e42a 100644 --- 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 d9120c398..3c7198ddc 100644 --- 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 c4cf0b43d..908d9a5e6 100644 --- 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 3cce80a4b..1af61fb9e 100644 --- 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 728b2b23c..e42db6001 100644 --- 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 4177d70e4..f21924bcd 100644 --- 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 24f1ca24c..8279ac04b 100644 --- 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 4013806de..80b43e759 100644 --- 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 fbb1d265c..db3a86e44 100644 --- 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 5924efd37..57d4d167d 100644 --- 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 a4e0c8a76..b9b55204d 100644 --- 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 3e6801102..809e95dd6 100644 --- 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 186374897..6cf085669 100644 --- 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 e0a5c19f0..fc8ad328f 100644 --- 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 2046b2fc9..c360c5ad4 100644 --- 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 4e37eb717..6a194d202 100644 --- 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 79ccc4b82..bd26067ef 100644 --- 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 c7968b274..7954ed476 100644 --- 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 a457bf9ae..9a7be04ab 100644 --- 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 926455710..92a6c4649 100644 --- 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 5b24b8d6e..67706f0a2 100644 --- 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 0674fad9c..1b88df727 100644 --- 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 2bcc024dd..8625f5e33 100644 --- 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 2f7f09058..00e223a7f 100644 --- 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 ee7d1712f..c230c8733 100644 --- 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 8e62f55ca..e2c2286aa 100644 --- 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 e5cc1a503..54e51e091 100644 --- 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 783c90b78..9358ad3f9 100644 --- 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 3f5c39b5d..8f12ab292 100644 --- 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 09858de24..a6096f1a6 100644 --- 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 cec025723..2c0b61ed2 100644 --- 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 c317baedf..06d43ebe3 100644 --- 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 367a44c11..50b03fc65 100644 --- 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 262826b3c..7c95d1472 100644 --- 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 9ea472819..3b67b0b5c 100644 --- 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 8406b4ab8..d45f7d6c2 100644 --- 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 55daa9a41..ab9d1766a 100644 --- 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 f4203e5ec..0ce18fc9b 100644 --- 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 bad15f3c8..f75859ff5 100644 --- 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 1918e2ad4..89a4efe41 100644 --- 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 6c822db5b..7f3f12602 100644 --- 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 457e66cef..ca698bee9 100644 --- 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 171623d19..c433c5906 100644 --- 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 56d45607f..d23509a48 100644 --- 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 a20218fc1..7b7627294 100644 --- 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 738ccf8e8..838fe683b 100644 --- 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 d9add50ad..b8e8c8bd9 100644 --- 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 dfb3b0750..fb02a5342 100644 --- 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 4e4f2d534..199ffeede 100644 --- 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 8269daf42..e09d8b794 100644 --- 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 134a99c73..b2bee7d6d 100644 --- 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 ed894518e..2d491c66a 100644 --- 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 77a5f38fd..aeb9ff1fa 100644 --- 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 e80fe01e2..98f8fbcec 100644 --- 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 9e49c2731..66ed16e27 100644 --- 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 1b2a6173d..fabdf3338 100644 --- 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 68ca97c2a..17ebc8f38 100644 --- 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 0caa98002..0bb4e4863 100644 --- 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 8e2e1cae2..fa0246289 100644 --- 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 02efe912b..5f805b403 100644 --- 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 ca8e1ba77..dd614cf46 100644 --- 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 32a520d13..63c778b9d 100644 --- 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 a509780ac..17960d47d 100644 --- 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 b65251ca7..da06ba1a9 100644 --- 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 c06a753e1..22a238b56 100644 --- 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 5e343156e..45e630acb 100644 --- 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 31d64cb49..1f8f72b26 100644 --- 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))