diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-29 13:40:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-29 13:40:08 -0500 |
| commit | e86726da4cf3883888a765aacf81ae76c7611c54 (patch) | |
| tree | f0565d3bac2bcc04ebe45a948e8032892a25d329 /test | |
| parent | a6e09da79c31d9f7cf783f17072239a44e538162 (diff) | |
Update the syntax for tuples in smt2 (#7265)
This changes mkTuple -> tuple and tupSel -> tuple_select.
This is in line with the most recent syntax for tuples in preparation for the theory of tables in smt2.
Diffstat (limited to 'test')
104 files changed, 639 insertions, 639 deletions
diff --git a/test/regress/regress0/bug596b.cvc.smt2 b/test/regress/regress0/bug596b.cvc.smt2 index 120966bf0..3482f6a37 100644 --- a/test/regress/regress0/bug596b.cvc.smt2 +++ b/test/regress/regress0/bug596b.cvc.smt2 @@ -3,5 +3,5 @@ (set-option :incremental false) (declare-fun f (Int) (Tuple Int Bool)) (declare-fun a () Int) -(assert (not (= (f a) (mkTuple 0 false)))) +(assert (not (= (f a) (tuple 0 false)))) (check-sat) diff --git a/test/regress/regress0/datatypes/4482-unc-simp-one.smt2 b/test/regress/regress0/datatypes/4482-unc-simp-one.smt2 index 265aeef23..a48b68535 100644 --- a/test/regress/regress0/datatypes/4482-unc-simp-one.smt2 +++ b/test/regress/regress0/datatypes/4482-unc-simp-one.smt2 @@ -1,5 +1,5 @@ (set-logic ALL) (set-info :status unsat) (declare-fun a () Tuple) -(assert (distinct a mkTuple)) +(assert (distinct a tuple)) (check-sat) diff --git a/test/regress/regress0/datatypes/Test1-tup-mp.cvc.smt2 b/test/regress/regress0/datatypes/Test1-tup-mp.cvc.smt2 index 87847d635..f4ac5f7e5 100644 --- a/test/regress/regress0/datatypes/Test1-tup-mp.cvc.smt2 +++ b/test/regress/regress0/datatypes/Test1-tup-mp.cvc.smt2 @@ -3,6 +3,6 @@ (set-option :incremental false) (declare-fun test (Int) (Tuple Int Int)) -(assert (= (test 5) (mkTuple 2 3))) -(assert (= (test 7) (mkTuple 3 4))) +(assert (= (test 5) (tuple 2 3))) +(assert (= (test 7) (tuple 3 4))) (check-sat) diff --git a/test/regress/regress0/datatypes/boolean-terms-tuple.cvc.smt2 b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc.smt2 index 7f391b719..7f666db79 100644 --- a/test/regress/regress0/datatypes/boolean-terms-tuple.cvc.smt2 +++ b/test/regress/regress0/datatypes/boolean-terms-tuple.cvc.smt2 @@ -2,5 +2,5 @@ (set-logic ALL) (set-option :incremental false) (declare-fun x () (Tuple Int Bool)) -(assert (not (= x (mkTuple 0 false)))) +(assert (not (= x (tuple 0 false)))) (check-sat) diff --git a/test/regress/regress0/datatypes/some-boolean-tests.cvc.smt2 b/test/regress/regress0/datatypes/some-boolean-tests.cvc.smt2 index d581b37b9..e05a65ad0 100644 --- a/test/regress/regress0/datatypes/some-boolean-tests.cvc.smt2 +++ b/test/regress/regress0/datatypes/some-boolean-tests.cvc.smt2 @@ -4,7 +4,7 @@ (declare-datatypes ((list 1)) ((par (T)((cons (car T) (care Bool) (cdr (list T))) (nil))))) (declare-fun x () (list Real)) (declare-fun y () (Tuple Int Bool Int)) -(assert (= y (mkTuple 5 true 4))) -(assert ((_ tupSel 1) y)) +(assert (= y (tuple 5 true 4))) +(assert ((_ tuple_select 1) y)) (assert (= x ((as cons (list Real)) (/ 11 10) true (as nil (list Real))))) (check-sat) diff --git a/test/regress/regress0/datatypes/tuple-model.cvc.smt2 b/test/regress/regress0/datatypes/tuple-model.cvc.smt2 index dcd68d03a..7f063a499 100644 --- a/test/regress/regress0/datatypes/tuple-model.cvc.smt2 +++ b/test/regress/regress0/datatypes/tuple-model.cvc.smt2 @@ -2,5 +2,5 @@ (set-logic ALL) (set-option :incremental false) (declare-fun x () (Tuple Int Int)) -(assert (= ((_ tupSel 0) x) 5)) +(assert (= ((_ tuple_select 0) x) 5)) (check-sat) diff --git a/test/regress/regress0/datatypes/tuple-no-clash.cvc.smt2 b/test/regress/regress0/datatypes/tuple-no-clash.cvc.smt2 index 1d05489b3..0c9479f07 100644 --- a/test/regress/regress0/datatypes/tuple-no-clash.cvc.smt2 +++ b/test/regress/regress0/datatypes/tuple-no-clash.cvc.smt2 @@ -4,6 +4,6 @@ (declare-fun x () (Tuple Real Real)) (declare-fun y () Real) (declare-fun z () Real) -(assert (or (= x (mkTuple y z)) (= x (mkTuple z y)))) -(assert (let ((_let_1 1.0)) (let ((_let_2 0.0)) (or (= x (mkTuple _let_2 _let_2)) (= x (mkTuple _let_1 _let_1)))))) +(assert (or (= x (tuple y z)) (= x (tuple z y)))) +(assert (let ((_let_1 1.0)) (let ((_let_2 0.0)) (or (= x (tuple _let_2 _let_2)) (= x (tuple _let_1 _let_1)))))) (check-sat) diff --git a/test/regress/regress0/datatypes/tuple-record-bug.cvc.smt2 b/test/regress/regress0/datatypes/tuple-record-bug.cvc.smt2 index 433a79797..f26769ccc 100644 --- a/test/regress/regress0/datatypes/tuple-record-bug.cvc.smt2 +++ b/test/regress/regress0/datatypes/tuple-record-bug.cvc.smt2 @@ -7,5 +7,5 @@ (declare-fun x () Int) (define-fun foo ((x |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)|)) |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| ((_ update int) x (int x))) (declare-fun m () |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)|) -(define-fun w () (Tuple |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| Int) (ite (= x 0) (mkTuple (foo m) 0) (mkTuple m 0))) -(check-sat-assuming ( (not (= ((_ tupSel 1) (ite (= x 0) (mkTuple (foo m) 0) (mkTuple m 0))) 1)) )) +(define-fun w () (Tuple |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| Int) (ite (= x 0) (tuple (foo m) 0) (tuple m 0))) +(check-sat-assuming ( (not (= ((_ tuple_select 1) (ite (= x 0) (tuple (foo m) 0) (tuple m 0))) 1)) )) diff --git a/test/regress/regress0/datatypes/tuple.cvc.smt2 b/test/regress/regress0/datatypes/tuple.cvc.smt2 index 2b0959968..9e6e83c2b 100644 --- a/test/regress/regress0/datatypes/tuple.cvc.smt2 +++ b/test/regress/regress0/datatypes/tuple.cvc.smt2 @@ -1,10 +1,10 @@ ; EXPECT: unsat (set-logic ALL) (set-option :incremental false) -(define-fun x () (Tuple Real Int Real) (mkTuple (/ 4 5) 9 (/ 11 9))) -(define-fun first_elem () Real ((_ tupSel 0) (mkTuple (/ 4 5) 9 (/ 11 9)))) -(define-fun third_elem () Real ((_ tupSel 2) (mkTuple (/ 4 5) 9 (/ 11 9)))) +(define-fun x () (Tuple Real Int Real) (tuple (/ 4 5) 9 (/ 11 9))) +(define-fun first_elem () Real ((_ tuple_select 0) (tuple (/ 4 5) 9 (/ 11 9)))) +(define-fun third_elem () Real ((_ tuple_select 2) (tuple (/ 4 5) 9 (/ 11 9)))) -(define-fun y () (Tuple Real Int Real) (mkTuple (/ 4 5) 9 (/ 11 9))) -(define-fun y1 () (Tuple Real Int Real) ((_ tuple_update 1) (mkTuple (/ 4 5) 9 (/ 11 9)) 3)) -(check-sat-assuming ( (not (let ((_let_1 (mkTuple (/ 4 5) 9 (/ 11 9)))) (let ((_let_2 ((_ tuple_update 1) _let_1 3))) (and (and (and (= _let_1 _let_1) (= ((_ tupSel 0) _let_1) ((_ tupSel 0) _let_2))) (= ((_ tupSel 2) _let_1) ((_ tupSel 2) _let_2))) (= ((_ tupSel 1) _let_2) 3))))) )) +(define-fun y () (Tuple Real Int Real) (tuple (/ 4 5) 9 (/ 11 9))) +(define-fun y1 () (Tuple Real Int Real) ((_ tuple_update 1) (tuple (/ 4 5) 9 (/ 11 9)) 3)) +(check-sat-assuming ( (not (let ((_let_1 (tuple (/ 4 5) 9 (/ 11 9)))) (let ((_let_2 ((_ tuple_update 1) _let_1 3))) (and (and (and (= _let_1 _let_1) (= ((_ tuple_select 0) _let_1) ((_ tuple_select 0) _let_2))) (= ((_ tuple_select 2) _let_1) ((_ tuple_select 2) _let_2))) (= ((_ tuple_select 1) _let_2) 3))))) )) diff --git a/test/regress/regress0/datatypes/tuples-empty.smt2 b/test/regress/regress0/datatypes/tuples-empty.smt2 index ec7e36ca8..125548499 100644 --- a/test/regress/regress0/datatypes/tuples-empty.smt2 +++ b/test/regress/regress0/datatypes/tuples-empty.smt2 @@ -7,8 +7,8 @@ (declare-fun t1 () (Tuple (Tuple Int Int) (Tuple Int String Int))) (declare-fun t2 () (Tuple (Tuple Bool Int) String)) -(assert (= t1 (mkTuple (mkTuple 12 99) (mkTuple 5 "xyz" 17)))) -(assert (= t2 (mkTuple (mkTuple true 14) "abc"))) -(assert (= t mkTuple)) +(assert (= t1 (tuple (tuple 12 99) (tuple 5 "xyz" 17)))) +(assert (= t2 (tuple (tuple true 14) "abc"))) +(assert (= t tuple)) (check-sat) diff --git a/test/regress/regress0/datatypes/tuples-multitype.smt2 b/test/regress/regress0/datatypes/tuples-multitype.smt2 index 8e412f2ed..c6555c5df 100644 --- a/test/regress/regress0/datatypes/tuples-multitype.smt2 +++ b/test/regress/regress0/datatypes/tuples-multitype.smt2 @@ -5,7 +5,7 @@ (declare-fun t () (Tuple Int String)) (declare-fun i () String) -(assert (= t (mkTuple 0 "0"))) -(assert (= i ((_ tupSel 1) t))) +(assert (= t (tuple 0 "0"))) +(assert (= i ((_ tuple_select 1) t))) (check-sat) diff --git a/test/regress/regress0/fmf/quant_real_univ.cvc.smt2 b/test/regress/regress0/fmf/quant_real_univ.cvc.smt2 index f4724355b..68fee3f21 100644 --- a/test/regress/regress0/fmf/quant_real_univ.cvc.smt2 +++ b/test/regress/regress0/fmf/quant_real_univ.cvc.smt2 @@ -9,5 +9,5 @@ (assert (= REAL_UNIVERSE (as univset (Set (Tuple Real))))) (assert (= ATOM_UNIVERSE (as univset (Set (Tuple Atom))))) (declare-fun levelVal () (Set (Tuple Atom Real))) -(assert (forall ((s Atom) (v1 Real) (v2 Real)) (=> (and (and (member (mkTuple s) ATOM_UNIVERSE) (member (mkTuple v1) REAL_UNIVERSE)) (member (mkTuple v2) REAL_UNIVERSE)) (=> (and (member (mkTuple s v1) levelVal) (member (mkTuple s v2) levelVal)) (= v1 v2))))) +(assert (forall ((s Atom) (v1 Real) (v2 Real)) (=> (and (and (member (tuple s) ATOM_UNIVERSE) (member (tuple v1) REAL_UNIVERSE)) (member (tuple v2) REAL_UNIVERSE)) (=> (and (member (tuple s v1) levelVal) (member (tuple s v2) levelVal)) (= v1 v2))))) (check-sat) diff --git a/test/regress/regress0/printer/tuples_and_records.cvc.smt2 b/test/regress/regress0/printer/tuples_and_records.cvc.smt2 index 49d12d1c0..0c54f5f49 100644 --- a/test/regress/regress0/printer/tuples_and_records.cvc.smt2 +++ b/test/regress/regress0/printer/tuples_and_records.cvc.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat ; EXPECT: (((a r) "active")) -; EXPECT: ((((_ tupSel 1) y) 9)) +; EXPECT: ((((_ tuple_select 1) y) 9)) (set-logic ALL) (set-option :incremental false) (set-option :produce-models true) @@ -9,7 +9,7 @@ (declare-fun r () __cvc5_record_a_String_b_String) (declare-fun y () (Tuple Real Int Real)) (assert (= r (__cvc5_record_a_String_b_String_ctor "active" "who knows?"))) -(assert (= y (mkTuple (/ 4 5) 9 (/ 11 9)))) +(assert (= y (tuple (/ 4 5) 9 (/ 11 9)))) (check-sat-assuming ( (not (= (a r) "what?")) )) (get-value ( (a r) )) -(get-value ( ((_ tupSel 1) y) )) +(get-value ( ((_ tuple_select 1) y) )) diff --git a/test/regress/regress0/rels/addr_book_0.cvc.smt2 b/test/regress/regress0/rels/addr_book_0.cvc.smt2 index a27be5b4b..00fc33d56 100644 --- a/test/regress/regress0/rels/addr_book_0.cvc.smt2 +++ b/test/regress/regress0/rels/addr_book_0.cvc.smt2 @@ -13,23 +13,23 @@ (declare-fun addr () (Set (Tuple Atom Atom Atom))) (declare-fun b1 () Atom) (declare-fun b1_tup () (Tuple Atom)) -(assert (= b1_tup (mkTuple b1))) +(assert (= b1_tup (tuple b1))) (assert (member b1_tup Book)) (declare-fun b2 () Atom) (declare-fun b2_tup () (Tuple Atom)) -(assert (= b2_tup (mkTuple b2))) +(assert (= b2_tup (tuple b2))) (assert (member b2_tup Book)) (declare-fun b3 () Atom) (declare-fun b3_tup () (Tuple Atom)) -(assert (= b3_tup (mkTuple b3))) +(assert (= b3_tup (tuple b3))) (assert (member b3_tup Book)) (declare-fun n () Atom) (declare-fun n_tup () (Tuple Atom)) -(assert (= n_tup (mkTuple n))) +(assert (= n_tup (tuple n))) (assert (member n_tup Name)) (declare-fun t () Atom) (declare-fun t_tup () (Tuple Atom)) -(assert (= t_tup (mkTuple t))) +(assert (= t_tup (tuple t))) (assert (member t_tup Target)) (assert (subset (join (join Book addr) Target) Name)) (assert (subset (join Book names) Name)) diff --git a/test/regress/regress0/rels/atom_univ2.cvc.smt2 b/test/regress/regress0/rels/atom_univ2.cvc.smt2 index 0fba2f00c..ad7d5ec4b 100644 --- a/test/regress/regress0/rels/atom_univ2.cvc.smt2 +++ b/test/regress/regress0/rels/atom_univ2.cvc.smt2 @@ -8,10 +8,10 @@ (declare-fun x () Atom) (declare-fun y () Atom) (assert (not (= x y))) -(assert (member (mkTuple y) a)) -(assert (member (mkTuple x y) b)) +(assert (member (tuple y) a)) +(assert (member (tuple x y) b)) (assert (= (as univset (Set (Tuple Atom Atom))) (product (as univset (Set (Tuple Atom))) (as univset (Set (Tuple Atom)))))) (declare-fun u () (Set (Tuple Atom Atom))) (assert (= u (as univset (Set (Tuple Atom Atom))))) -(assert (not (member (mkTuple x y) u))) +(assert (not (member (tuple x y) u))) (check-sat) diff --git a/test/regress/regress0/rels/iden_0.cvc.smt2 b/test/regress/regress0/rels/iden_0.cvc.smt2 index fca943912..d2d091e60 100644 --- a/test/regress/regress0/rels/iden_0.cvc.smt2 +++ b/test/regress/regress0/rels/iden_0.cvc.smt2 @@ -7,19 +7,19 @@ (declare-fun id () (Set (Tuple Int Int))) (declare-fun t () (Set (Tuple Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) -(assert (member (mkTuple 1) t)) -(assert (member (mkTuple 2) t)) +(assert (= a (tuple 1 5))) +(assert (member (tuple 1) t)) +(assert (member (tuple 2) t)) (assert (member z x)) (assert (member zt x)) (assert (member v x)) (assert (member a x)) (assert (= id (iden t))) -(assert (not (member (mkTuple 1 1) (intersection id x)))) +(assert (not (member (tuple 1 1) (intersection id x)))) (check-sat) diff --git a/test/regress/regress0/rels/iden_1.cvc.smt2 b/test/regress/regress0/rels/iden_1.cvc.smt2 index 5a59eda53..c2de24558 100644 --- a/test/regress/regress0/rels/iden_1.cvc.smt2 +++ b/test/regress/regress0/rels/iden_1.cvc.smt2 @@ -12,8 +12,8 @@ (declare-fun c () Atom) (declare-fun d () Atom) (assert (= univ (as univset (Set (Tuple Atom))))) -(assert (member (mkTuple a b) x)) -(assert (member (mkTuple c d) x)) +(assert (member (tuple a b) x)) +(assert (member (tuple c d) x)) (assert (not (= a b))) (assert (= (iden (join x univ)) x)) (check-sat) diff --git a/test/regress/regress0/rels/join-eq-u-sat.cvc.smt2 b/test/regress/regress0/rels/join-eq-u-sat.cvc.smt2 index 3801be252..37af1b418 100644 --- a/test/regress/regress0/rels/join-eq-u-sat.cvc.smt2 +++ b/test/regress/regress0/rels/join-eq-u-sat.cvc.smt2 @@ -10,9 +10,9 @@ (declare-fun w () (Set (Tuple Int unit))) (declare-fun z () (Set (Tuple unit Int))) (assert (= (join x y) (join w z))) -(assert (member (mkTuple 0 1) (join x y))) -(assert (member (mkTuple 0 u) w)) +(assert (member (tuple 0 1) (join x y))) +(assert (member (tuple 0 u) w)) (declare-fun t () Int) (assert (and (> t 0) (< t 3))) -(assert (not (member (mkTuple u t) z))) +(assert (not (member (tuple u t) z))) (check-sat) diff --git a/test/regress/regress0/rels/join-eq-u.cvc.smt2 b/test/regress/regress0/rels/join-eq-u.cvc.smt2 index a455e1d36..92514a3be 100644 --- a/test/regress/regress0/rels/join-eq-u.cvc.smt2 +++ b/test/regress/regress0/rels/join-eq-u.cvc.smt2 @@ -10,9 +10,9 @@ (declare-fun w () (Set (Tuple Int unit))) (declare-fun z () (Set (Tuple unit Int))) (assert (= (join x y) (join w z))) -(assert (member (mkTuple 0 1) (join x y))) -(assert (member (mkTuple 0 u) w)) +(assert (member (tuple 0 1) (join x y))) +(assert (member (tuple 0 u) w)) (declare-fun t () Int) (assert (and (> t 0) (< t 2))) -(assert (not (member (mkTuple u t) z))) +(assert (not (member (tuple u t) z))) (check-sat) diff --git a/test/regress/regress0/rels/joinImg_0.cvc.smt2 b/test/regress/regress0/rels/joinImg_0.cvc.smt2 index a2ae87de9..76a13b645 100644 --- a/test/regress/regress0/rels/joinImg_0.cvc.smt2 +++ b/test/regress/regress0/rels/joinImg_0.cvc.smt2 @@ -8,19 +8,19 @@ (declare-fun r () (Set (Tuple Int Int))) (declare-fun t () (Set (Tuple Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) -(assert (member (mkTuple 1 7) x)) +(assert (= a (tuple 1 5))) +(assert (member (tuple 1 7) x)) (assert (member z x)) -(assert (member (mkTuple 7 5) y)) +(assert (member (tuple 7 5) y)) (assert (= t (join_image x 2))) -(assert (member (mkTuple 3) (join_image x 2))) -(assert (not (member (mkTuple 1) (join_image x 2)))) -(assert (member (mkTuple 4) (join_image x 2))) -(assert (member (mkTuple 1) (join_image x 1))) +(assert (member (tuple 3) (join_image x 2))) +(assert (not (member (tuple 1) (join_image x 2)))) +(assert (member (tuple 4) (join_image x 2))) +(assert (member (tuple 1) (join_image x 1))) (check-sat) diff --git a/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2 b/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2 index 4beb03a76..c04aa7985 100644 --- a/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2 +++ b/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2 @@ -8,6 +8,6 @@ (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))) -(assert (let ((_let_1 (singleton (mkTuple a)))) (= (join _let_1 t) (J _let_1 t)))) -(assert (let ((_let_1 (singleton (mkTuple c)))) (not (= (join _let_1 (tclosure t)) _let_1)))) +(assert (let ((_let_1 (singleton (tuple a)))) (= (join _let_1 t) (J _let_1 t)))) +(assert (let ((_let_1 (singleton (tuple c)))) (not (= (join _let_1 (tclosure t)) _let_1)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_1tup_0.cvc.smt2 b/test/regress/regress0/rels/rel_1tup_0.cvc.smt2 index 0d0ccbfdc..4210a5486 100644 --- a/test/regress/regress0/rels/rel_1tup_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_1tup_0.cvc.smt2 @@ -7,13 +7,13 @@ (declare-fun y () (Set (Tuple Int))) (declare-fun z () (Set (Tuple Int))) (declare-fun b () (Tuple Int Int)) -(assert (= b (mkTuple 2 1))) +(assert (= b (tuple 2 1))) (assert (member b x)) (declare-fun a () (Tuple Int)) -(assert (= a (mkTuple 1))) +(assert (= a (tuple 1))) (assert (member a y)) (declare-fun c () (Tuple Int)) -(assert (= c (mkTuple 2))) +(assert (= c (tuple 2))) (assert (= z (join x y))) (assert (not (member c z))) (check-sat) diff --git a/test/regress/regress0/rels/rel_complex_0.cvc.smt2 b/test/regress/regress0/rels/rel_complex_0.cvc.smt2 index f7705987d..2f4aea539 100644 --- a/test/regress/regress0/rels/rel_complex_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_complex_0.cvc.smt2 @@ -9,15 +9,15 @@ (declare-fun f () Int) (declare-fun g () Int) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple 4 f))) +(assert (= e (tuple 4 f))) (assert (member e x)) (declare-fun d () (Tuple Int Int)) -(assert (= d (mkTuple g 3))) +(assert (= d (tuple g 3))) (assert (member d y)) (assert (= z (union (singleton f) (singleton g)))) (assert (= 0 (- f g))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 4 3))) +(assert (= a (tuple 4 3))) (assert (= r (join x y))) (assert (not (member a r))) (check-sat) diff --git a/test/regress/regress0/rels/rel_complex_1.cvc.smt2 b/test/regress/regress0/rels/rel_complex_1.cvc.smt2 index 823fb7ed1..e8ccfb070 100644 --- a/test/regress/regress0/rels/rel_complex_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_complex_1.cvc.smt2 @@ -10,18 +10,18 @@ (declare-fun z () (Set (Tuple Int))) (declare-fun r2 () (Set (Tuple Int Int))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 3 1))) +(assert (= a (tuple 3 1))) (assert (member a x)) (declare-fun d () (Tuple Int Int)) -(assert (= d (mkTuple 1 3))) +(assert (= d (tuple 1 3))) (assert (member d y)) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple 4 3))) +(assert (= e (tuple 4 3))) (assert (= r (join x y))) -(assert (member (mkTuple 1) w)) -(assert (member (mkTuple 2) z)) +(assert (member (tuple 1) w)) +(assert (member (tuple 2) z)) (assert (= r2 (product w z))) (assert (not (member e r))) (assert (subset r r2)) -(assert (not (member (mkTuple 3 3) r2))) +(assert (not (member (tuple 3 3) r2))) (check-sat) diff --git a/test/regress/regress0/rels/rel_conflict_0.cvc.smt2 b/test/regress/regress0/rels/rel_conflict_0.cvc.smt2 index 4af1f8530..e074778c5 100644 --- a/test/regress/regress0/rels/rel_conflict_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_conflict_0.cvc.smt2 @@ -4,7 +4,7 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple 4 4))) +(assert (= e (tuple 4 4))) (assert (member e x)) -(assert (not (member (mkTuple 4 4) x))) +(assert (not (member (tuple 4 4) x))) (check-sat) diff --git a/test/regress/regress0/rels/rel_join_0.cvc.smt2 b/test/regress/regress0/rels/rel_join_0.cvc.smt2 index 3e4a68377..3c36d36e8 100644 --- a/test/regress/regress0/rels/rel_join_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_0.cvc.smt2 @@ -6,15 +6,15 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) -(assert (member (mkTuple 1 7) x)) -(assert (member (mkTuple 7 5) y)) +(assert (= a (tuple 1 5))) +(assert (member (tuple 1 7) x)) +(assert (member (tuple 7 5) y)) (assert (member z x)) (assert (member zt y)) (assert (not (member a (join x y)))) diff --git a/test/regress/regress0/rels/rel_join_0_1.cvc.smt2 b/test/regress/regress0/rels/rel_join_0_1.cvc.smt2 index 1c8f7b472..6af8429d3 100644 --- a/test/regress/regress0/rels/rel_join_0_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_0_1.cvc.smt2 @@ -6,16 +6,16 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) -(assert (member (mkTuple 1 7) x)) -(assert (member (mkTuple 4 3) x)) -(assert (member (mkTuple 7 5) y)) +(assert (= a (tuple 1 5))) +(assert (member (tuple 1 7) x)) +(assert (member (tuple 4 3) x)) +(assert (member (tuple 7 5) y)) (assert (member z x)) (assert (member zt y)) (assert (member a (join x y))) diff --git a/test/regress/regress0/rels/rel_join_1.cvc.smt2 b/test/regress/regress0/rels/rel_join_1.cvc.smt2 index 22e5e7f8f..88f8c73f3 100644 --- a/test/regress/regress0/rels/rel_join_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_1.cvc.smt2 @@ -6,19 +6,19 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) -(assert (member (mkTuple 1 7) x)) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 3 4) x)) -(assert (member (mkTuple 7 5) y)) -(assert (member (mkTuple 7 3) y)) -(assert (member (mkTuple 4 7) y)) +(assert (= a (tuple 1 5))) +(assert (member (tuple 1 7) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 3 4) x)) +(assert (member (tuple 7 5) y)) +(assert (member (tuple 7 3) y)) +(assert (member (tuple 4 7) y)) (assert (member z x)) (assert (member zt y)) (assert (not (member a (join x y)))) diff --git a/test/regress/regress0/rels/rel_join_1_1.cvc.smt2 b/test/regress/regress0/rels/rel_join_1_1.cvc.smt2 index 54e51cfe6..e1556149c 100644 --- a/test/regress/regress0/rels/rel_join_1_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_1_1.cvc.smt2 @@ -6,19 +6,19 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) -(assert (member (mkTuple 1 7) x)) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 3 4) x)) -(assert (member (mkTuple 7 5) y)) -(assert (member (mkTuple 7 3) y)) -(assert (member (mkTuple 4 7) y)) +(assert (= a (tuple 1 5))) +(assert (member (tuple 1 7) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 3 4) x)) +(assert (member (tuple 7 5) y)) +(assert (member (tuple 7 3) y)) +(assert (member (tuple 4 7) y)) (assert (member z x)) (assert (member zt y)) (assert (= r (join x y))) diff --git a/test/regress/regress0/rels/rel_join_2.cvc.smt2 b/test/regress/regress0/rels/rel_join_2.cvc.smt2 index 0ab915f7e..5c8f0ea91 100644 --- a/test/regress/regress0/rels/rel_join_2.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_2.cvc.smt2 @@ -6,11 +6,11 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int Int)) -(assert (= zt (mkTuple 2 1 3))) +(assert (= zt (tuple 2 1 3))) (declare-fun a () (Tuple Int Int Int)) -(assert (= a (mkTuple 1 1 3))) +(assert (= a (tuple 1 1 3))) (assert (member z x)) (assert (member zt y)) (assert (not (member a (join x y)))) diff --git a/test/regress/regress0/rels/rel_join_2_1.cvc.smt2 b/test/regress/regress0/rels/rel_join_2_1.cvc.smt2 index 47269ef64..82433cc1b 100644 --- a/test/regress/regress0/rels/rel_join_2_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_2_1.cvc.smt2 @@ -6,11 +6,11 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int Int)) -(assert (= zt (mkTuple 2 1 3))) +(assert (= zt (tuple 2 1 3))) (declare-fun a () (Tuple Int Int Int)) -(assert (= a (mkTuple 1 1 3))) +(assert (= a (tuple 1 1 3))) (assert (member z x)) (assert (member zt y)) (assert (member a (join x y))) diff --git a/test/regress/regress0/rels/rel_join_3.cvc.smt2 b/test/regress/regress0/rels/rel_join_3.cvc.smt2 index e726271d1..4a3358526 100644 --- a/test/regress/regress0/rels/rel_join_3.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_3.cvc.smt2 @@ -6,19 +6,19 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) -(assert (member (mkTuple 1 7) x)) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 3 4) x)) -(assert (member (mkTuple 7 5) y)) -(assert (member (mkTuple 7 3) y)) -(assert (member (mkTuple 4 7) y)) +(assert (= a (tuple 1 5))) +(assert (member (tuple 1 7) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 3 4) x)) +(assert (member (tuple 7 5) y)) +(assert (member (tuple 7 3) y)) +(assert (member (tuple 4 7) y)) (assert (= r (join x y))) (assert (member z x)) (assert (member zt y)) diff --git a/test/regress/regress0/rels/rel_join_3_1.cvc.smt2 b/test/regress/regress0/rels/rel_join_3_1.cvc.smt2 index 3b06bfb38..7b66ab443 100644 --- a/test/regress/regress0/rels/rel_join_3_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_3_1.cvc.smt2 @@ -6,19 +6,19 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) -(assert (member (mkTuple 1 7) x)) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 3 4) x)) -(assert (member (mkTuple 7 5) y)) -(assert (member (mkTuple 7 3) y)) -(assert (member (mkTuple 4 7) y)) +(assert (= a (tuple 1 5))) +(assert (member (tuple 1 7) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 3 4) x)) +(assert (member (tuple 7 5) y)) +(assert (member (tuple 7 3) y)) +(assert (member (tuple 4 7) y)) (assert (= r (join x y))) (assert (member z x)) (assert (member zt y)) diff --git a/test/regress/regress0/rels/rel_join_4.cvc.smt2 b/test/regress/regress0/rels/rel_join_4.cvc.smt2 index 76ad33633..bc4f16513 100644 --- a/test/regress/regress0/rels/rel_join_4.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_4.cvc.smt2 @@ -6,21 +6,21 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) +(assert (= a (tuple 1 5))) (declare-fun b () (Tuple Int Int)) -(assert (= b (mkTuple 7 5))) -(assert (member (mkTuple 1 7) x)) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 3 4) x)) +(assert (= b (tuple 7 5))) +(assert (member (tuple 1 7) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 3 4) x)) (assert (member b y)) -(assert (member (mkTuple 7 3) y)) -(assert (member (mkTuple 4 7) y)) +(assert (member (tuple 7 3) y)) +(assert (member (tuple 4 7) y)) (assert (= r (join x y))) (assert (member z x)) (assert (member zt y)) diff --git a/test/regress/regress0/rels/rel_join_5.cvc.smt2 b/test/regress/regress0/rels/rel_join_5.cvc.smt2 index 1d138befa..227395fe6 100644 --- a/test/regress/regress0/rels/rel_join_5.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_5.cvc.smt2 @@ -6,13 +6,13 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) -(assert (member (mkTuple 7 1) x)) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 7 3) y)) -(assert (member (mkTuple 4 7) y)) -(assert (member (mkTuple 3 4) z)) +(assert (member (tuple 7 1) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 7 3) y)) +(assert (member (tuple 4 7) y)) +(assert (member (tuple 3 4) z)) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 4))) +(assert (= a (tuple 1 4))) (assert (= r (join (join (transpose x) y) z))) (assert (not (member a r))) (check-sat) diff --git a/test/regress/regress0/rels/rel_join_6.cvc.smt2 b/test/regress/regress0/rels/rel_join_6.cvc.smt2 index 391bd0fad..547430c19 100644 --- a/test/regress/regress0/rels/rel_join_6.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_6.cvc.smt2 @@ -5,7 +5,7 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) -(assert (= x (union (singleton (mkTuple 1 2)) (singleton (mkTuple 3 4))))) -(assert (= y (join x (union (singleton (mkTuple 2 1)) (singleton (mkTuple 4 3)))))) -(assert (not (member (mkTuple 1 1) y))) +(assert (= x (union (singleton (tuple 1 2)) (singleton (tuple 3 4))))) +(assert (= y (join x (union (singleton (tuple 2 1)) (singleton (tuple 4 3)))))) +(assert (not (member (tuple 1 1) y))) (check-sat) diff --git a/test/regress/regress0/rels/rel_join_7.cvc.smt2 b/test/regress/regress0/rels/rel_join_7.cvc.smt2 index 6488df50e..3956af748 100644 --- a/test/regress/regress0/rels/rel_join_7.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_7.cvc.smt2 @@ -7,15 +7,15 @@ (declare-fun r () (Set (Tuple Int Int))) (declare-fun w () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) -(assert (member (mkTuple 1 7) x)) -(assert (member (mkTuple 7 5) y)) +(assert (= a (tuple 1 5))) +(assert (member (tuple 1 7) x)) +(assert (member (tuple 7 5) y)) (assert (member z x)) (assert (member zt y)) (assert (= w (union r (join x y)))) diff --git a/test/regress/regress0/rels/rel_product_0.cvc.smt2 b/test/regress/regress0/rels/rel_product_0.cvc.smt2 index 1b9f4e369..890c6f5d6 100644 --- a/test/regress/regress0/rels/rel_product_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_product_0.cvc.smt2 @@ -7,11 +7,11 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int Int Int)) -(assert (= v (mkTuple 1 2 2 1))) +(assert (= v (tuple 1 2 2 1))) (assert (member z x)) (assert (member zt y)) (assert (not (member v (product x y)))) diff --git a/test/regress/regress0/rels/rel_product_0_1.cvc.smt2 b/test/regress/regress0/rels/rel_product_0_1.cvc.smt2 index 2929a51ee..1958036d2 100644 --- a/test/regress/regress0/rels/rel_product_0_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_product_0_1.cvc.smt2 @@ -7,11 +7,11 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int Int Int)) -(assert (= v (mkTuple 1 2 2 1))) +(assert (= v (tuple 1 2 2 1))) (assert (member z x)) (assert (member zt y)) (assert (member v (product x y))) diff --git a/test/regress/regress0/rels/rel_product_1.cvc.smt2 b/test/regress/regress0/rels/rel_product_1.cvc.smt2 index 93d2eb725..6711cfd6f 100644 --- a/test/regress/regress0/rels/rel_product_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_product_1.cvc.smt2 @@ -7,11 +7,11 @@ (declare-fun y () (Set (Tuple Int Int Int))) (declare-fun r () (Set (Tuple Int Int Int))) (declare-fun z () (Tuple Int Int Int)) -(assert (= z (mkTuple 1 2 3))) +(assert (= z (tuple 1 2 3))) (declare-fun zt () (Tuple Int Int Int)) -(assert (= zt (mkTuple 3 2 1))) +(assert (= zt (tuple 3 2 1))) (declare-fun v () (Tuple Int Int Int Int Int Int)) -(assert (= v (mkTuple 1 2 3 3 2 1))) +(assert (= v (tuple 1 2 3 3 2 1))) (assert (member z x)) (assert (member zt y)) (assert (not (member v (product x y)))) diff --git a/test/regress/regress0/rels/rel_product_1_1.cvc.smt2 b/test/regress/regress0/rels/rel_product_1_1.cvc.smt2 index 696ae31ba..5d8c2dbf2 100644 --- a/test/regress/regress0/rels/rel_product_1_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_product_1_1.cvc.smt2 @@ -7,11 +7,11 @@ (declare-fun y () (Set (Tuple Int Int Int))) (declare-fun r () (Set (Tuple Int Int Int Int Int Int))) (declare-fun z () (Tuple Int Int Int)) -(assert (= z (mkTuple 1 2 3))) +(assert (= z (tuple 1 2 3))) (declare-fun zt () (Tuple Int Int Int)) -(assert (= zt (mkTuple 3 2 1))) +(assert (= zt (tuple 3 2 1))) (assert (member z x)) (assert (member zt y)) -(assert (member (mkTuple 1 1 1 1 1 1) r)) +(assert (member (tuple 1 1 1 1 1 1) r)) (assert (= r (product x y))) (check-sat) diff --git a/test/regress/regress0/rels/rel_symbolic_1.cvc.smt2 b/test/regress/regress0/rels/rel_symbolic_1.cvc.smt2 index 9952b64ec..0c8188f1f 100644 --- a/test/regress/regress0/rels/rel_symbolic_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_symbolic_1.cvc.smt2 @@ -7,13 +7,13 @@ (declare-fun r () (Set (Tuple Int Int))) (declare-fun f () Int) (declare-fun d () (Tuple Int Int)) -(assert (= d (mkTuple f 3))) +(assert (= d (tuple f 3))) (assert (member d y)) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple 4 f))) +(assert (= e (tuple 4 f))) (assert (member e x)) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 4 3))) +(assert (= a (tuple 4 3))) (assert (= r (join x y))) (assert (not (member a r))) (check-sat) diff --git a/test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2 b/test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2 index b677ddb0e..2e10e76ad 100644 --- a/test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2 @@ -10,7 +10,7 @@ (declare-fun a () (Tuple Int Int)) (assert (member a x)) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple 4 3))) +(assert (= e (tuple 4 3))) (assert (= r (join x y))) (assert (not (member e r))) (check-sat) diff --git a/test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2 b/test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2 index 21f7c6d89..2615112c2 100644 --- a/test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2 @@ -6,12 +6,12 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun d () (Tuple Int Int)) -(assert (= d (mkTuple 1 3))) -(assert (member (mkTuple 1 3) y)) +(assert (= d (tuple 1 3))) +(assert (member (tuple 1 3) y)) (declare-fun a () (Tuple Int Int)) (assert (member a x)) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple 4 3))) +(assert (= e (tuple 4 3))) (assert (= r (join x y))) (assert (not (member e r))) (check-sat) diff --git a/test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2 b/test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2 index 7302a53b1..c170fd7a0 100644 --- a/test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2 @@ -9,10 +9,10 @@ (declare-fun d () (Tuple Int Int)) (assert (member d y)) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple 4 f))) +(assert (= e (tuple 4 f))) (assert (member e x)) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 4 3))) +(assert (= a (tuple 4 3))) (assert (= r (join x y))) (assert (not (member a r))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tc_11.cvc.smt2 b/test/regress/regress0/rels/rel_tc_11.cvc.smt2 index 0b0cd0d07..5398cf388 100644 --- a/test/regress/regress0/rels/rel_tc_11.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tc_11.cvc.smt2 @@ -6,13 +6,13 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Set (Tuple Int Int Int Int))) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 5 3) x)) -(assert (member (mkTuple 3 9) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 5 3) x)) +(assert (member (tuple 3 9) x)) (assert (= z (product x y))) -(assert (member (mkTuple 1 2 3 4) z)) -(assert (not (member (mkTuple 5 9) x))) -(assert (member (mkTuple 3 8) y)) +(assert (member (tuple 1 2 3 4) z)) +(assert (not (member (tuple 5 9) x))) +(assert (member (tuple 3 8) y)) (assert (= y (tclosure x))) -(assert (not (member (mkTuple 1 2) y))) +(assert (not (member (tuple 1 2) y))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tc_2_1.cvc.smt2 b/test/regress/regress0/rels/rel_tc_2_1.cvc.smt2 index 689390402..07c60c562 100644 --- a/test/regress/regress0/rels/rel_tc_2_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tc_2_1.cvc.smt2 @@ -6,18 +6,18 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun e () Int) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 e))) +(assert (= a (tuple 1 e))) (declare-fun d () (Tuple Int Int)) -(assert (= d (mkTuple e 5))) +(assert (= d (tuple e 5))) (assert (member a x)) (assert (member d x)) -(assert (not (member (mkTuple 1 1) x))) -(assert (not (member (mkTuple 1 2) x))) -(assert (not (member (mkTuple 1 3) x))) -(assert (not (member (mkTuple 1 4) x))) -(assert (not (member (mkTuple 1 5) x))) -(assert (not (member (mkTuple 1 6) x))) -(assert (not (member (mkTuple 1 7) x))) +(assert (not (member (tuple 1 1) x))) +(assert (not (member (tuple 1 2) x))) +(assert (not (member (tuple 1 3) x))) +(assert (not (member (tuple 1 4) x))) +(assert (not (member (tuple 1 5) x))) +(assert (not (member (tuple 1 6) x))) +(assert (not (member (tuple 1 7) x))) (assert (= y (tclosure x))) -(assert (member (mkTuple 1 5) y)) +(assert (member (tuple 1 5) y)) (check-sat) diff --git a/test/regress/regress0/rels/rel_tc_3.cvc.smt2 b/test/regress/regress0/rels/rel_tc_3.cvc.smt2 index 46b7cff5b..9af4c2490 100644 --- a/test/regress/regress0/rels/rel_tc_3.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tc_3.cvc.smt2 @@ -8,13 +8,13 @@ (declare-fun b () Int) (declare-fun c () Int) (declare-fun d () Int) -(assert (member (mkTuple 1 a) x)) -(assert (member (mkTuple 1 c) x)) -(assert (member (mkTuple 1 d) x)) -(assert (member (mkTuple b 1) x)) +(assert (member (tuple 1 a) x)) +(assert (member (tuple 1 c) x)) +(assert (member (tuple 1 d) x)) +(assert (member (tuple b 1) x)) (assert (= b d)) (assert (> b (- d 1))) (assert (< b (+ d 1))) (assert (= y (tclosure x))) -(assert (not (member (mkTuple 1 1) y))) +(assert (not (member (tuple 1 1) y))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tc_3_1.cvc.smt2 b/test/regress/regress0/rels/rel_tc_3_1.cvc.smt2 index 4d44f31a5..4041735f9 100644 --- a/test/regress/regress0/rels/rel_tc_3_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tc_3_1.cvc.smt2 @@ -8,10 +8,10 @@ (declare-fun b () Int) (declare-fun c () Int) (declare-fun d () Int) -(assert (member (mkTuple 1 a) x)) -(assert (member (mkTuple 1 c) x)) -(assert (member (mkTuple 1 d) x)) -(assert (member (mkTuple b 1) x)) +(assert (member (tuple 1 a) x)) +(assert (member (tuple 1 c) x)) +(assert (member (tuple 1 d) x)) +(assert (member (tuple b 1) x)) (assert (= b d)) (assert (= y (tclosure x))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tc_7.cvc.smt2 b/test/regress/regress0/rels/rel_tc_7.cvc.smt2 index f5abb8eef..b7200a9ef 100644 --- a/test/regress/regress0/rels/rel_tc_7.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tc_7.cvc.smt2 @@ -5,6 +5,6 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int))) (assert (= y (join (tclosure x) x))) -(assert (member (mkTuple 1 2) (join (join x x) x))) +(assert (member (tuple 1 2) (join (join x x) x))) (assert (not (subset y (tclosure x)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tc_8.cvc.smt2 b/test/regress/regress0/rels/rel_tc_8.cvc.smt2 index 9dc3f9f50..0485a06e9 100644 --- a/test/regress/regress0/rels/rel_tc_8.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tc_8.cvc.smt2 @@ -4,6 +4,6 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int))) -(assert (member (mkTuple 2 2) (tclosure x))) +(assert (member (tuple 2 2) (tclosure x))) (assert (= x (as emptyset (Set (Tuple Int Int))))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tp_3_1.cvc.smt2 b/test/regress/regress0/rels/rel_tp_3_1.cvc.smt2 index 5db2710d8..4e7a33e04 100644 --- a/test/regress/regress0/rels/rel_tp_3_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tp_3_1.cvc.smt2 @@ -5,9 +5,9 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Set (Tuple Int Int))) -(assert (member (mkTuple 1 3) x)) -(assert (or (member (mkTuple 2 3) z) (member (mkTuple 2 1) z))) +(assert (member (tuple 1 3) x)) +(assert (or (member (tuple 2 3) z) (member (tuple 2 1) z))) (assert (= y (transpose x))) -(assert (not (member (mkTuple 1 2) y))) +(assert (not (member (tuple 1 2) y))) (assert (= x z)) (check-sat) diff --git a/test/regress/regress0/rels/rel_tp_join_0.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_0.cvc.smt2 index 594e0c52f..05761030c 100644 --- a/test/regress/regress0/rels/rel_tp_join_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tp_join_0.cvc.smt2 @@ -6,21 +6,21 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 5 1))) +(assert (= a (tuple 5 1))) (declare-fun b () (Tuple Int Int)) -(assert (= b (mkTuple 7 5))) -(assert (member (mkTuple 1 7) x)) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 3 4) x)) +(assert (= b (tuple 7 5))) +(assert (member (tuple 1 7) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 3 4) x)) (assert (member b y)) -(assert (member (mkTuple 7 3) y)) -(assert (member (mkTuple 4 7) y)) +(assert (member (tuple 7 3) y)) +(assert (member (tuple 4 7) y)) (assert (= r (join x y))) (assert (member z x)) (assert (member zt y)) diff --git a/test/regress/regress0/rels/rel_tp_join_1.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_1.cvc.smt2 index fe2f9f2db..f1faefaeb 100644 --- a/test/regress/regress0/rels/rel_tp_join_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tp_join_1.cvc.smt2 @@ -7,20 +7,20 @@ (declare-fun z () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun b () (Tuple Int Int)) -(assert (= b (mkTuple 1 7))) +(assert (= b (tuple 1 7))) (declare-fun c () (Tuple Int Int)) -(assert (= c (mkTuple 2 3))) +(assert (= c (tuple 2 3))) (assert (member b x)) (assert (member c x)) (declare-fun d () (Tuple Int Int)) -(assert (= d (mkTuple 7 3))) +(assert (= d (tuple 7 3))) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple 4 7))) +(assert (= e (tuple 4 7))) (assert (member d y)) (assert (member e y)) -(assert (member (mkTuple 3 4) z)) +(assert (member (tuple 3 4) z)) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 4 1))) +(assert (= a (tuple 4 1))) (assert (= r (join (join x y) z))) (assert (not (member a (transpose r)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tp_join_2.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_2.cvc.smt2 index fb402a909..0f3d124ae 100644 --- a/test/regress/regress0/rels/rel_tp_join_2.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tp_join_2.cvc.smt2 @@ -6,13 +6,13 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) -(assert (member (mkTuple 7 1) x)) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 7 3) y)) -(assert (member (mkTuple 4 7) y)) -(assert (member (mkTuple 3 4) z)) +(assert (member (tuple 7 1) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 7 3) y)) +(assert (member (tuple 4 7) y)) +(assert (member (tuple 3 4) z)) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 4 1))) +(assert (= a (tuple 4 1))) (assert (= r (join (join (transpose x) y) z))) (assert (not (member a (transpose r)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tp_join_3.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_3.cvc.smt2 index 23c235be6..1443c9ca3 100644 --- a/test/regress/regress0/rels/rel_tp_join_3.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tp_join_3.cvc.smt2 @@ -7,17 +7,17 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) -(assert (member (mkTuple 7 1) x)) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 7 3) y)) -(assert (member (mkTuple 4 7) y)) -(assert (member (mkTuple 3 4) z)) -(assert (member (mkTuple 3 3) w)) +(assert (member (tuple 7 1) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 7 3) y)) +(assert (member (tuple 4 7) y)) +(assert (member (tuple 3 4) z)) +(assert (member (tuple 3 3) w)) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 4 1))) +(assert (= a (tuple 4 1))) (assert (not (member a (transpose r)))) (declare-fun zz () (Set (Tuple Int Int))) (assert (= zz (join (transpose x) y))) -(assert (not (member (mkTuple 1 3) w))) -(assert (not (member (mkTuple 1 3) (union w zz)))) +(assert (not (member (tuple 1 3) w))) +(assert (not (member (tuple 1 3) (union w zz)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tp_join_eq_0.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc.smt2 index 672844f08..1dcfc0eb6 100644 --- a/test/regress/regress0/rels/rel_tp_join_eq_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc.smt2 @@ -6,16 +6,16 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) -(assert (= x (union (singleton (mkTuple 1 7)) (singleton (mkTuple 2 3))))) +(assert (= x (union (singleton (tuple 1 7)) (singleton (tuple 2 3))))) (declare-fun d () (Tuple Int Int)) -(assert (= d (mkTuple 7 3))) +(assert (= d (tuple 7 3))) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple 4 7))) +(assert (= e (tuple 4 7))) (assert (member d y)) (assert (member e y)) -(assert (member (mkTuple 3 4) z)) +(assert (member (tuple 3 4) z)) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 4 1))) +(assert (= a (tuple 4 1))) (assert (= r (join (join x y) z))) (assert (not (member a (transpose r)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tp_join_int_0.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_int_0.cvc.smt2 index 83b6ab904..82f6a0238 100644 --- a/test/regress/regress0/rels/rel_tp_join_int_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tp_join_int_0.cvc.smt2 @@ -11,9 +11,9 @@ (declare-fun u () Int) (assert (and (< 4 t) (< t 6))) (assert (and (< 4 u) (< u 6))) -(assert (member (mkTuple 1 u) x)) -(assert (member (mkTuple t 3) y)) +(assert (member (tuple 1 u) x)) +(assert (member (tuple t 3) y)) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 3))) +(assert (= a (tuple 1 3))) (assert (not (member a (join x y)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tp_join_pro_0.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc.smt2 index f3bcad8a1..d7d89d3a4 100644 --- a/test/regress/regress0/rels/rel_tp_join_pro_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc.smt2 @@ -7,13 +7,13 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int Int Int))) -(assert (member (mkTuple 2 1) x)) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 2 2) y)) -(assert (member (mkTuple 4 7) y)) -(assert (member (mkTuple 3 4) z)) +(assert (member (tuple 2 1) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 2 2) y)) +(assert (member (tuple 4 7) y)) +(assert (member (tuple 3 4) z)) (declare-fun v () (Tuple Int Int Int Int)) -(assert (= v (mkTuple 4 3 2 1))) +(assert (= v (tuple 4 3 2 1))) (assert (= r (product (join (transpose x) y) z))) (assert (not (member v (transpose r)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_tp_join_var_0.cvc.smt2 b/test/regress/regress0/rels/rel_tp_join_var_0.cvc.smt2 index 0fee2c136..80b359e8b 100644 --- a/test/regress/regress0/rels/rel_tp_join_var_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tp_join_var_0.cvc.smt2 @@ -11,10 +11,10 @@ (declare-fun u () Int) (assert (and (< 4 t) (< t 6))) (assert (and (< 4 u) (< u 6))) -(assert (member (mkTuple 1 t) x)) -(assert (member (mkTuple u 3) y)) +(assert (member (tuple 1 t) x)) +(assert (member (tuple u 3) y)) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 3))) +(assert (= a (tuple 1 3))) (assert (not (member a (join x y)))) (declare-fun st () (Set Int)) (declare-fun su () (Set Int)) diff --git a/test/regress/regress0/rels/rel_transpose_0.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_0.cvc.smt2 index 9996209b8..280f78ea2 100644 --- a/test/regress/regress0/rels/rel_transpose_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_0.cvc.smt2 @@ -6,9 +6,9 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun a () Int) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (assert (member z x)) (assert (not (member zt (transpose x)))) (assert (= y (transpose x))) diff --git a/test/regress/regress0/rels/rel_transpose_1.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_1.cvc.smt2 index 3d21e17a9..fb7070e82 100644 --- a/test/regress/regress0/rels/rel_transpose_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_1.cvc.smt2 @@ -5,9 +5,9 @@ (declare-fun x () (Set (Tuple Int Int Int))) (declare-fun y () (Set (Tuple Int Int Int))) (declare-fun z () (Tuple Int Int Int)) -(assert (= z (mkTuple 1 2 3))) +(assert (= z (tuple 1 2 3))) (declare-fun zt () (Tuple Int Int Int)) -(assert (= zt (mkTuple 3 2 1))) +(assert (= zt (tuple 3 2 1))) (assert (member z x)) (assert (not (member zt (transpose x)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2 index d54b8c608..0d9f6d028 100644 --- a/test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2 @@ -6,9 +6,9 @@ (declare-fun y () (Set (Tuple Int Int Int))) (declare-fun z () (Tuple Int Int Int)) (declare-fun a () Int) -(assert (= z (mkTuple 1 2 a))) +(assert (= z (tuple 1 2 a))) (declare-fun zt () (Tuple Int Int Int)) -(assert (= zt (mkTuple 3 2 2))) +(assert (= zt (tuple 3 2 2))) (assert (member z x)) (assert (member zt (transpose x))) (assert (= y (transpose x))) diff --git a/test/regress/regress0/rels/rel_transpose_3.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_3.cvc.smt2 index 3109186f1..ea737919e 100644 --- a/test/regress/regress0/rels/rel_transpose_3.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_3.cvc.smt2 @@ -5,9 +5,9 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (assert (= x y)) (assert (member z x)) (assert (not (member zt (transpose y)))) diff --git a/test/regress/regress0/rels/rel_transpose_4.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_4.cvc.smt2 index d75d64b64..5ba3cc2c6 100644 --- a/test/regress/regress0/rels/rel_transpose_4.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_4.cvc.smt2 @@ -5,7 +5,7 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (assert (member z x)) -(assert (not (member (mkTuple 2 1) (transpose x)))) +(assert (not (member (tuple 2 1) (transpose x)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_transpose_5.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_5.cvc.smt2 index 927a5f07f..8a58ca763 100644 --- a/test/regress/regress0/rels/rel_transpose_5.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_5.cvc.smt2 @@ -6,12 +6,12 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (assert (member zt y)) (declare-fun w () (Tuple Int Int)) -(assert (= w (mkTuple 2 2))) +(assert (= w (tuple 2 2))) (assert (member w y)) (assert (member z x)) (assert (not (member zt (transpose (join x y))))) diff --git a/test/regress/regress0/rels/rel_transpose_6.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_6.cvc.smt2 index 7c097fc46..1dc932a81 100644 --- a/test/regress/regress0/rels/rel_transpose_6.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_6.cvc.smt2 @@ -5,13 +5,13 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (assert (member z x)) -(assert (member (mkTuple 3 4) x)) -(assert (member (mkTuple 3 5) x)) -(assert (member (mkTuple 3 3) x)) +(assert (member (tuple 3 4) x)) +(assert (member (tuple 3 5) x)) +(assert (member (tuple 3 3) x)) (assert (= x (transpose y))) (assert (not (member zt y))) (assert (member z y)) diff --git a/test/regress/regress0/rels/relations-ops.smt2 b/test/regress/regress0/rels/relations-ops.smt2 index abb7faf10..e68eb49bb 100644 --- a/test/regress/regress0/rels/relations-ops.smt2 +++ b/test/regress/regress0/rels/relations-ops.smt2 @@ -11,12 +11,12 @@ (declare-fun lt2 () (Set (Tuple Int Int))) (declare-fun i () Int) -(assert (= r1 (insert (mkTuple "a" 1) (mkTuple "b" 2) (mkTuple "c" 3) (singleton (mkTuple "d" 4))))) -(assert (= r2 (insert (mkTuple 1 "1") (mkTuple 2 "2") (mkTuple 3 "3") (singleton (mkTuple 17 "17"))))) +(assert (= r1 (insert (tuple "a" 1) (tuple "b" 2) (tuple "c" 3) (singleton (tuple "d" 4))))) +(assert (= r2 (insert (tuple 1 "1") (tuple 2 "2") (tuple 3 "3") (singleton (tuple 17 "17"))))) (assert (= r (join r1 r2))) (assert (= s (transpose r))) (assert (= t (product r1 r2))) -(assert (= lt1 (insert (mkTuple 1 2) (mkTuple 2 3) (mkTuple 3 4) (singleton (mkTuple 4 5))))) +(assert (= lt1 (insert (tuple 1 2) (tuple 2 3) (tuple 3 4) (singleton (tuple 4 5))))) (assert (= lt2 (tclosure lt1))) (assert (= i (card t))) diff --git a/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2 b/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2 index dff78fbd8..2ba92270a 100644 --- a/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2 +++ b/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2 @@ -6,7 +6,7 @@ (declare-fun z () (Set (Tuple Int Int))) (declare-fun x () Int) (declare-fun y () Int) -(assert (member (mkTuple 1 x) w)) -(assert (member (mkTuple y 2) z)) -(assert (not (member (mkTuple 1 2) (join w z)))) +(assert (member (tuple 1 x) w)) +(assert (member (tuple y 2) z)) +(assert (not (member (tuple 1 2) (join w z)))) (check-sat) diff --git a/test/regress/regress0/sets/complement3.cvc.smt2 b/test/regress/regress0/sets/complement3.cvc.smt2 index 3e7239774..b81843871 100644 --- a/test/regress/regress0/sets/complement3.cvc.smt2 +++ b/test/regress/regress0/sets/complement3.cvc.smt2 @@ -9,8 +9,8 @@ (declare-fun ATOM_UNIV () (Set (Tuple Atom))) (declare-fun V1 () Atom) (assert (= C32 (intersection (complement C2) (complement C4)))) -(assert (member (mkTuple V1) (complement C32))) +(assert (member (tuple V1) (complement C32))) (assert (= ATOM_UNIV (as univset (Set (Tuple Atom))))) -(assert (member (mkTuple V1) ATOM_UNIV)) -(assert (member (mkTuple V1) (complement C2))) +(assert (member (tuple V1) ATOM_UNIV)) +(assert (member (tuple V1) (complement C2))) (check-sat) diff --git a/test/regress/regress1/datatypes/tuple_projection.smt2 b/test/regress/regress1/datatypes/tuple_projection.smt2 index bdd9d5458..dfe37a9d0 100644 --- a/test/regress/regress1/datatypes/tuple_projection.smt2 +++ b/test/regress/regress1/datatypes/tuple_projection.smt2 @@ -4,8 +4,8 @@ (declare-fun u () (Tuple String String)) (declare-fun v () Tuple) (declare-fun x () String) -(assert (= t (mkTuple "a" "b" "c" "d"))) -(assert (= x ((_ tupSel 0) t))) +(assert (= t (tuple "a" "b" "c" "d"))) +(assert (= x ((_ tuple_select 0) t))) (assert (= u ((_ tuple_project 2 3) t))) (assert (= v (tuple_project t))) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2 b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2 index b099c7914..433c1f102 100644 --- a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2 +++ b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2 @@ -27,5 +27,5 @@ (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 (union (singleton ow1) (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|))) -(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 (member r ev_set) (member w ev_set)) (= (member (mkTuple r w) RF) (and (= (O r) R) (= (O w) W)))))) +(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 (member r ev_set) (member w ev_set)) (= (member (tuple r w) RF) (and (= (O r) R) (= (O w) W)))))) (check-sat) diff --git a/test/regress/regress1/rels/addr_book_1.cvc.smt2 b/test/regress/regress1/rels/addr_book_1.cvc.smt2 index 7a6ac7d5b..591303875 100644 --- a/test/regress/regress1/rels/addr_book_1.cvc.smt2 +++ b/test/regress/regress1/rels/addr_book_1.cvc.smt2 @@ -13,26 +13,26 @@ (declare-fun addr () (Set (Tuple Atom Atom Atom))) (declare-fun b1 () Atom) (declare-fun b1_tup () (Tuple Atom)) -(assert (= b1_tup (mkTuple b1))) +(assert (= b1_tup (tuple b1))) (assert (member b1_tup Book)) (declare-fun b2 () Atom) (declare-fun b2_tup () (Tuple Atom)) -(assert (= b2_tup (mkTuple b2))) +(assert (= b2_tup (tuple b2))) (assert (member b2_tup Book)) (declare-fun b3 () Atom) (declare-fun b3_tup () (Tuple Atom)) -(assert (= b3_tup (mkTuple b3))) +(assert (= b3_tup (tuple b3))) (assert (member b3_tup Book)) (declare-fun m () Atom) (declare-fun m_tup () (Tuple Atom)) -(assert (= m_tup (mkTuple m))) +(assert (= m_tup (tuple m))) (assert (member m_tup Name)) (declare-fun t () Atom) (declare-fun t_tup () (Tuple Atom)) -(assert (= t_tup (mkTuple t))) +(assert (= t_tup (tuple t))) (assert (member t_tup Target)) (assert (= (join (singleton m_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom))))) -(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (mkTuple m t))))) -(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (mkTuple m t))))) +(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (tuple m t))))) +(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (tuple m t))))) (assert (not (= (join (singleton b1_tup) addr) (join (singleton b3_tup) addr)))) (check-sat) diff --git a/test/regress/regress1/rels/addr_book_1_1.cvc.smt2 b/test/regress/regress1/rels/addr_book_1_1.cvc.smt2 index 29eb2106d..a7cfcaf38 100644 --- a/test/regress/regress1/rels/addr_book_1_1.cvc.smt2 +++ b/test/regress/regress1/rels/addr_book_1_1.cvc.smt2 @@ -13,26 +13,26 @@ (declare-fun addr () (Set (Tuple Atom Atom Atom))) (declare-fun b1 () Atom) (declare-fun b1_tup () (Tuple Atom)) -(assert (= b1_tup (mkTuple b1))) +(assert (= b1_tup (tuple b1))) (assert (member b1_tup Book)) (declare-fun b2 () Atom) (declare-fun b2_tup () (Tuple Atom)) -(assert (= b2_tup (mkTuple b2))) +(assert (= b2_tup (tuple b2))) (assert (member b2_tup Book)) (declare-fun b3 () Atom) (declare-fun b3_tup () (Tuple Atom)) -(assert (= b3_tup (mkTuple b3))) +(assert (= b3_tup (tuple b3))) (assert (member b3_tup Book)) (declare-fun m () Atom) (declare-fun m_tup () (Tuple Atom)) -(assert (= m_tup (mkTuple m))) +(assert (= m_tup (tuple m))) (assert (member m_tup Name)) (declare-fun t () Atom) (declare-fun t_tup () (Tuple Atom)) -(assert (= t_tup (mkTuple t))) +(assert (= t_tup (tuple t))) (assert (member t_tup Target)) (assert (= (join (singleton m_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom))))) -(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (mkTuple m t))))) -(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (mkTuple m t))))) +(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (tuple m t))))) +(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (tuple m t))))) (assert (= (join (singleton b1_tup) addr) (join (singleton b3_tup) addr))) (check-sat) diff --git a/test/regress/regress1/rels/bv1-unit.cvc.smt2 b/test/regress/regress1/rels/bv1-unit.cvc.smt2 index b61b9403f..ba4dac386 100644 --- a/test/regress/regress1/rels/bv1-unit.cvc.smt2 +++ b/test/regress/regress1/rels/bv1-unit.cvc.smt2 @@ -11,8 +11,8 @@ (declare-fun d () (_ BitVec 1)) (declare-fun e () (_ BitVec 1)) (assert (not (= b c))) -(assert (member (mkTuple a u b) x)) -(assert (member (mkTuple a u c) x)) -(assert (member (mkTuple d u a) y)) -(assert (not (member (mkTuple a u u a) (join x y)))) +(assert (member (tuple a u b) x)) +(assert (member (tuple a u c) x)) +(assert (member (tuple d u a) y)) +(assert (not (member (tuple a u u a) (join x y)))) (check-sat) diff --git a/test/regress/regress1/rels/bv1-unitb.cvc.smt2 b/test/regress/regress1/rels/bv1-unitb.cvc.smt2 index c1db4195f..696c8919e 100644 --- a/test/regress/regress1/rels/bv1-unitb.cvc.smt2 +++ b/test/regress/regress1/rels/bv1-unitb.cvc.smt2 @@ -12,8 +12,8 @@ (declare-fun e () (_ BitVec 1)) (declare-fun u () unitb) (assert (not (= b c))) -(assert (member (mkTuple a u b) x)) -(assert (member (mkTuple a u c) x)) -(assert (member (mkTuple d u a) y)) -(assert (not (member (mkTuple a u u a) (join x y)))) +(assert (member (tuple a u b) x)) +(assert (member (tuple a u c) x)) +(assert (member (tuple d u a) y)) +(assert (not (member (tuple a u u a) (join x y)))) (check-sat) diff --git a/test/regress/regress1/rels/bv1.cvc.smt2 b/test/regress/regress1/rels/bv1.cvc.smt2 index 93fa6a296..1df5ee38b 100644 --- a/test/regress/regress1/rels/bv1.cvc.smt2 +++ b/test/regress/regress1/rels/bv1.cvc.smt2 @@ -10,8 +10,8 @@ (declare-fun d () (_ BitVec 1)) (declare-fun e () (_ BitVec 1)) (assert (not (= b c))) -(assert (member (mkTuple a b) x)) -(assert (member (mkTuple a c) x)) -(assert (member (mkTuple d a) y)) -(assert (not (member (mkTuple a a) (join x y)))) +(assert (member (tuple a b) x)) +(assert (member (tuple a c) x)) +(assert (member (tuple d a) y)) +(assert (not (member (tuple a a) (join x y)))) (check-sat) diff --git a/test/regress/regress1/rels/bv2.cvc.smt2 b/test/regress/regress1/rels/bv2.cvc.smt2 index 824e7e125..005737b36 100644 --- a/test/regress/regress1/rels/bv2.cvc.smt2 +++ b/test/regress/regress1/rels/bv2.cvc.smt2 @@ -10,8 +10,8 @@ (declare-fun d () (_ BitVec 2)) (declare-fun e () (_ BitVec 2)) (assert (not (= b c))) -(assert (member (mkTuple a b) x)) -(assert (member (mkTuple a c) x)) -(assert (member (mkTuple d a) y)) -(assert (not (member (mkTuple a a) (join x y)))) +(assert (member (tuple a b) x)) +(assert (member (tuple a c) x)) +(assert (member (tuple d a) y)) +(assert (not (member (tuple a a) (join x y)))) (check-sat) diff --git a/test/regress/regress1/rels/garbage_collect.cvc.smt2 b/test/regress/regress1/rels/garbage_collect.cvc.smt2 index c4bba2cd3..55f181acd 100644 --- a/test/regress/regress1/rels/garbage_collect.cvc.smt2 +++ b/test/regress/regress1/rels/garbage_collect.cvc.smt2 @@ -16,10 +16,10 @@ (declare-fun s1 () H_TYPE) (declare-fun s2 () H_TYPE) (declare-fun s3 () H_TYPE) -(assert (= h0 (singleton (mkTuple s0)))) -(assert (= h1 (singleton (mkTuple s1)))) -(assert (= h2 (singleton (mkTuple s2)))) -(assert (= h3 (singleton (mkTuple s3)))) +(assert (= h0 (singleton (tuple s0)))) +(assert (= h1 (singleton (tuple s1)))) +(assert (= h2 (singleton (tuple s2)))) +(assert (= h3 (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))) @@ -28,10 +28,10 @@ (declare-fun live () Obj) (assert (= (join h1 mark) empty_obj_set)) (assert (subset (join h0 ref) (join h1 ref))) -(assert (forall ((n Obj)) (=> (member (mkTuple root n) (tclosure (join h1 ref))) (member (mkTuple n) (join h2 mark))))) +(assert (forall ((n Obj)) (=> (member (tuple root n) (tclosure (join h1 ref))) (member (tuple n) (join h2 mark))))) (assert (subset (join h1 ref) (join h2 ref))) -(assert (forall ((n Obj)) (let ((_let_1 (mkTuple n))) (=> (not (member _let_1 (join h2 mark))) (= (join (singleton _let_1) (join h3 ref)) empty_obj_set))))) -(assert (forall ((n Obj)) (let ((_let_1 (mkTuple n))) (let ((_let_2 (singleton _let_1))) (=> (member _let_1 (join h2 mark)) (= (join _let_2 (join h3 ref)) (join _let_2 (join h2 ref)))))))) -(assert (member (mkTuple root live) (tclosure (join h0 ref)))) -(assert (let ((_let_1 (singleton (mkTuple live)))) (not (subset (join _let_1 (join h0 ref)) (join _let_1 (join h3 ref)))))) +(assert (forall ((n Obj)) (let ((_let_1 (tuple n))) (=> (not (member _let_1 (join h2 mark))) (= (join (singleton _let_1) (join h3 ref)) empty_obj_set))))) +(assert (forall ((n Obj)) (let ((_let_1 (tuple n))) (let ((_let_2 (singleton _let_1))) (=> (member _let_1 (join h2 mark)) (= (join _let_2 (join h3 ref)) (join _let_2 (join h2 ref)))))))) +(assert (member (tuple root live) (tclosure (join h0 ref)))) +(assert (let ((_let_1 (singleton (tuple live)))) (not (subset (join _let_1 (join h0 ref)) (join _let_1 (join h3 ref)))))) (check-sat) diff --git a/test/regress/regress1/rels/iden_1_1.cvc.smt2 b/test/regress/regress1/rels/iden_1_1.cvc.smt2 index eb09d698f..305476798 100644 --- a/test/regress/regress1/rels/iden_1_1.cvc.smt2 +++ b/test/regress/regress1/rels/iden_1_1.cvc.smt2 @@ -15,8 +15,8 @@ (assert (= univ (as univset (Set (Tuple Atom))))) (assert (= univ2 (as univset (Set (Tuple Atom Atom))))) (assert (= univ2 (product univ univ))) -(assert (member (mkTuple a b) x)) -(assert (member (mkTuple c d) x)) +(assert (member (tuple a b) x)) +(assert (member (tuple c d) x)) (assert (not (= a b))) (assert (subset (iden univ) x)) (check-sat) diff --git a/test/regress/regress1/rels/join-eq-structure-and.cvc.smt2 b/test/regress/regress1/rels/join-eq-structure-and.cvc.smt2 index 1eb1419c8..60696f706 100644 --- a/test/regress/regress1/rels/join-eq-structure-and.cvc.smt2 +++ b/test/regress/regress1/rels/join-eq-structure-and.cvc.smt2 @@ -10,12 +10,12 @@ (declare-fun w () (Set (Tuple Int unit))) (declare-fun z () (Set (Tuple unit Int))) (assert (let ((_let_1 (join w z))) (let ((_let_2 (join x y))) (and (= _let_2 _let_1) (= _let_2 (transpose _let_1)))))) -(assert (member (mkTuple 0 1) (join x y))) +(assert (member (tuple 0 1) (join x y))) (declare-fun t () Int) (assert (and (>= t 0) (<= t 1))) (declare-fun s () Int) (assert (and (>= s 0) (<= s 1))) (assert (= (+ s t) 1)) -(assert (member (mkTuple s u) w)) -(assert (not (member (mkTuple u t) z))) +(assert (member (tuple s u) w)) +(assert (not (member (tuple u t) z))) (check-sat) diff --git a/test/regress/regress1/rels/join-eq-structure.cvc.smt2 b/test/regress/regress1/rels/join-eq-structure.cvc.smt2 index 5144ac4c2..0e510c77a 100644 --- a/test/regress/regress1/rels/join-eq-structure.cvc.smt2 +++ b/test/regress/regress1/rels/join-eq-structure.cvc.smt2 @@ -10,12 +10,12 @@ (declare-fun w () (Set (Tuple Int unit))) (declare-fun z () (Set (Tuple unit Int))) (assert (let ((_let_1 (join w z))) (let ((_let_2 (join x y))) (or (= _let_2 _let_1) (= _let_2 (transpose _let_1)))))) -(assert (member (mkTuple 0 1) (join x y))) +(assert (member (tuple 0 1) (join x y))) (declare-fun t () Int) (assert (and (>= t 0) (<= t 1))) (declare-fun s () Int) (assert (and (>= s 0) (<= s 1))) (assert (= (+ s t) 1)) -(assert (member (mkTuple s u) w)) -(assert (not (member (mkTuple u t) z))) +(assert (member (tuple s u) w)) +(assert (not (member (tuple u t) z))) (check-sat) diff --git a/test/regress/regress1/rels/joinImg_0_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_0_1.cvc.smt2 index 8a28b74ae..ae33348bd 100644 --- a/test/regress/regress1/rels/joinImg_0_1.cvc.smt2 +++ b/test/regress/regress1/rels/joinImg_0_1.cvc.smt2 @@ -9,20 +9,20 @@ (declare-fun t () (Set (Tuple Int))) (declare-fun u () (Set (Tuple Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int)) -(assert (= v (mkTuple 1 1))) +(assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) +(assert (= a (tuple 1 5))) (declare-fun b () Int) -(assert (member (mkTuple 1 7) x)) +(assert (member (tuple 1 7) x)) (assert (member z x)) -(assert (member (mkTuple 7 5) y)) +(assert (member (tuple 7 5) y)) (assert (= t (join_image x 2))) -(assert (member (mkTuple 3) (join_image x 2))) +(assert (member (tuple 3) (join_image x 2))) (assert (= u (join_image x 1))) -(assert (member (mkTuple 4) (join_image x 2))) -(assert (member (mkTuple b) (join_image x 1))) +(assert (member (tuple 4) (join_image x 2))) +(assert (member (tuple b) (join_image x 1))) (check-sat) diff --git a/test/regress/regress1/rels/joinImg_0_2.cvc.smt2 b/test/regress/regress1/rels/joinImg_0_2.cvc.smt2 index 8f1954c10..86fc76670 100644 --- a/test/regress/regress1/rels/joinImg_0_2.cvc.smt2 +++ b/test/regress/regress1/rels/joinImg_0_2.cvc.smt2 @@ -10,22 +10,22 @@ (declare-fun u () (Set (Tuple Int))) (declare-fun univ () (Set (Tuple Int))) (declare-fun z () (Tuple Int Int)) -(assert (= z (mkTuple 1 2))) +(assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) -(assert (= zt (mkTuple 2 1))) +(assert (= zt (tuple 2 1))) (declare-fun s () (Tuple Int Int)) -(assert (= s (mkTuple 1 1))) +(assert (= s (tuple 1 1))) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 1 5))) +(assert (= a (tuple 1 5))) (declare-fun b () Int) -(assert (member (mkTuple 1 7) x)) +(assert (member (tuple 1 7) x)) (assert (member z x)) -(assert (member (mkTuple 7 5) y)) +(assert (member (tuple 7 5) y)) (assert (= t (join_image x 2))) (assert (= univ (join_image x 0))) -(assert (member (mkTuple 100) t)) -(assert (not (member (mkTuple 3) univ))) +(assert (member (tuple 100) t)) +(assert (not (member (tuple 3) univ))) (assert (= u (join_image x 1))) -(assert (member (mkTuple 4) (join_image x 2))) -(assert (member (mkTuple b) (join_image x 1))) +(assert (member (tuple 4) (join_image x 2))) +(assert (member (tuple b) (join_image x 1))) (check-sat) diff --git a/test/regress/regress1/rels/joinImg_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_1.cvc.smt2 index 3c5664d76..4d7c56000 100644 --- a/test/regress/regress1/rels/joinImg_1.cvc.smt2 +++ b/test/regress/regress1/rels/joinImg_1.cvc.smt2 @@ -12,7 +12,7 @@ (declare-fun c () Atom) (declare-fun d () Atom) (declare-fun e () Atom) -(assert (member (mkTuple a) (join_image x 2))) -(assert (= x (union (union (singleton (mkTuple b c)) (singleton (mkTuple d e))) (singleton (mkTuple c e))))) +(assert (member (tuple a) (join_image x 2))) +(assert (= x (union (union (singleton (tuple b c)) (singleton (tuple d e))) (singleton (tuple c e))))) (assert (not (= a b))) (check-sat) diff --git a/test/regress/regress1/rels/joinImg_1_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_1_1.cvc.smt2 index c8e228f1b..dc940a43b 100644 --- a/test/regress/regress1/rels/joinImg_1_1.cvc.smt2 +++ b/test/regress/regress1/rels/joinImg_1_1.cvc.smt2 @@ -12,8 +12,8 @@ (declare-fun c () Atom) (declare-fun d () Atom) (declare-fun e () Atom) -(assert (member (mkTuple a) (join_image x 2))) +(assert (member (tuple a) (join_image x 2))) (assert (= t (join_image x 2))) -(assert (= x (union (union (singleton (mkTuple b c)) (singleton (mkTuple d e))) (singleton (mkTuple c e))))) -(assert (member (mkTuple c) t)) +(assert (= x (union (union (singleton (tuple b c)) (singleton (tuple d e))) (singleton (tuple c e))))) +(assert (member (tuple c) t)) (check-sat) diff --git a/test/regress/regress1/rels/joinImg_2.cvc.smt2 b/test/regress/regress1/rels/joinImg_2.cvc.smt2 index 9f8efdfff..527770994 100644 --- a/test/regress/regress1/rels/joinImg_2.cvc.smt2 +++ b/test/regress/regress1/rels/joinImg_2.cvc.smt2 @@ -14,13 +14,13 @@ (declare-fun e () Atom) (declare-fun f () Atom) (declare-fun g () Atom) -(assert (member (mkTuple a) (join_image x 2))) -(assert (member (mkTuple a) (join_image y 3))) -(assert (= x (union (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e))) (singleton (mkTuple f b))))) -(assert (member (mkTuple a f) x)) -(assert (member (mkTuple a f) y)) +(assert (member (tuple a) (join_image x 2))) +(assert (member (tuple a) (join_image y 3))) +(assert (= x (union (union (union (union (singleton (tuple f g)) (singleton (tuple b c))) (singleton (tuple d e))) (singleton (tuple c e))) (singleton (tuple f b))))) +(assert (member (tuple a f) x)) +(assert (member (tuple a f) y)) (assert (= x y)) (assert (not (= a b))) -(assert (not (member (mkTuple d) (join_image x 2)))) +(assert (not (member (tuple d) (join_image x 2)))) (assert (= f d)) (check-sat) diff --git a/test/regress/regress1/rels/joinImg_2_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_2_1.cvc.smt2 index 797e7b35b..0d563415b 100644 --- a/test/regress/regress1/rels/joinImg_2_1.cvc.smt2 +++ b/test/regress/regress1/rels/joinImg_2_1.cvc.smt2 @@ -14,9 +14,9 @@ (declare-fun e () Atom) (declare-fun f () Atom) (declare-fun g () Atom) -(assert (member (mkTuple a) (join_image x 2))) -(assert (member (mkTuple a) (join_image y 1))) -(assert (= y (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e))))) -(assert (= x (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e))))) +(assert (member (tuple a) (join_image x 2))) +(assert (member (tuple a) (join_image y 1))) +(assert (= y (union (union (union (singleton (tuple f g)) (singleton (tuple b c))) (singleton (tuple d e))) (singleton (tuple c e))))) +(assert (= x (union (union (union (singleton (tuple f g)) (singleton (tuple b c))) (singleton (tuple d e))) (singleton (tuple c e))))) (assert (or (not (= a b)) (not (= a f)))) (check-sat) diff --git a/test/regress/regress1/rels/prod-mod-eq.cvc.smt2 b/test/regress/regress1/rels/prod-mod-eq.cvc.smt2 index 7d9147a8b..088976c2b 100644 --- a/test/regress/regress1/rels/prod-mod-eq.cvc.smt2 +++ b/test/regress/regress1/rels/prod-mod-eq.cvc.smt2 @@ -11,10 +11,10 @@ (declare-fun z2 () (Set (Tuple Int Int))) (declare-fun w2 () (Set (Tuple Int Int))) (assert (not (= z (product x y)))) -(assert (member (mkTuple 0 1 2 3) z)) -(assert (member (mkTuple 0 1) z1)) -(assert (member (mkTuple 0 1) z2)) -(assert (member (mkTuple 2 3) w1)) -(assert (member (mkTuple 2 3) w2)) +(assert (member (tuple 0 1 2 3) z)) +(assert (member (tuple 0 1) z1)) +(assert (member (tuple 0 1) z2)) +(assert (member (tuple 2 3) w1)) +(assert (member (tuple 2 3) w2)) (assert (or (and (= x z1) (= y w1)) (and (= x z2) (= y w2)))) (check-sat) diff --git a/test/regress/regress1/rels/prod-mod-eq2.cvc.smt2 b/test/regress/regress1/rels/prod-mod-eq2.cvc.smt2 index b2bee8b3f..e54259778 100644 --- a/test/regress/regress1/rels/prod-mod-eq2.cvc.smt2 +++ b/test/regress/regress1/rels/prod-mod-eq2.cvc.smt2 @@ -13,10 +13,10 @@ (declare-fun P ((Set (Tuple Int Int Int Int))) Bool) (assert (= z (product x y))) (assert (P z)) -(assert (not (P (singleton (mkTuple 0 1 2 3))))) -(assert (member (mkTuple 0 1) z1)) -(assert (member (mkTuple 0 1) z2)) -(assert (member (mkTuple 2 3) w1)) -(assert (member (mkTuple 2 3) w2)) +(assert (not (P (singleton (tuple 0 1 2 3))))) +(assert (member (tuple 0 1) z1)) +(assert (member (tuple 0 1) z2)) +(assert (member (tuple 2 3) w1)) +(assert (member (tuple 2 3) w2)) (assert (or (and (= x z1) (= y w1)) (and (= x z2) (= y w2)))) (check-sat) diff --git a/test/regress/regress1/rels/rel_complex_3.cvc.smt2 b/test/regress/regress1/rels/rel_complex_3.cvc.smt2 index ccd152268..7955cf532 100644 --- a/test/regress/regress1/rels/rel_complex_3.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_3.cvc.smt2 @@ -8,13 +8,13 @@ (declare-fun r () (Set (Tuple Int Int))) (declare-fun w () (Set (Tuple Int Int))) (declare-fun f () (Tuple Int Int)) -(assert (= f (mkTuple 3 1))) +(assert (= f (tuple 3 1))) (assert (member f x)) (declare-fun g () (Tuple Int Int)) -(assert (= g (mkTuple 1 3))) +(assert (= g (tuple 1 3))) (assert (member g y)) (declare-fun h () (Tuple Int Int)) -(assert (= h (mkTuple 3 5))) +(assert (= h (tuple 3 5))) (assert (member h x)) (assert (member h y)) (assert (= r (join x y))) diff --git a/test/regress/regress1/rels/rel_complex_4.cvc.smt2 b/test/regress/regress1/rels/rel_complex_4.cvc.smt2 index 1f99668ac..865105a1b 100644 --- a/test/regress/regress1/rels/rel_complex_4.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_4.cvc.smt2 @@ -8,19 +8,19 @@ (declare-fun r () (Set (Tuple Int Int))) (declare-fun w () (Set (Tuple Int Int))) (declare-fun f () (Tuple Int Int)) -(assert (= f (mkTuple 3 1))) +(assert (= f (tuple 3 1))) (assert (member f x)) (declare-fun g () (Tuple Int Int)) -(assert (= g (mkTuple 1 3))) +(assert (= g (tuple 1 3))) (assert (member g y)) (declare-fun h () (Tuple Int Int)) -(assert (= h (mkTuple 3 5))) +(assert (= h (tuple 3 5))) (assert (member h x)) (assert (member h y)) (assert (= r (join x y))) (declare-fun a () Int) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple a a))) +(assert (= e (tuple a a))) (assert (= w (singleton e))) (assert (subset (transpose w) y)) (assert (not (member e r))) diff --git a/test/regress/regress1/rels/rel_complex_5.cvc.smt2 b/test/regress/regress1/rels/rel_complex_5.cvc.smt2 index dfbc23c8e..69ec8046e 100644 --- a/test/regress/regress1/rels/rel_complex_5.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_5.cvc.smt2 @@ -9,20 +9,20 @@ (declare-fun r () (Set (Tuple Int Int))) (declare-fun w () (Set (Tuple Int Int))) (declare-fun f () (Tuple Int Int)) -(assert (= f (mkTuple 3 1))) +(assert (= f (tuple 3 1))) (assert (member f x)) (declare-fun g () (Tuple Int Int)) -(assert (= g (mkTuple 1 3))) +(assert (= g (tuple 1 3))) (assert (member g y)) (declare-fun h () (Tuple Int Int)) -(assert (= h (mkTuple 3 5))) +(assert (= h (tuple 3 5))) (assert (member h x)) (assert (member h y)) (assert (= r (join x y))) (declare-fun a () (Tuple Int)) -(assert (= a (mkTuple 1))) +(assert (= a (tuple 1))) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple 1 1))) +(assert (= e (tuple 1 1))) (assert (let ((_let_1 (singleton a))) (= w (product _let_1 _let_1)))) (assert (subset (transpose w) y)) (assert (not (member e r))) diff --git a/test/regress/regress1/rels/rel_mix_0_1.cvc.smt2 b/test/regress/regress1/rels/rel_mix_0_1.cvc.smt2 index 08323ed5a..79cfc078f 100644 --- a/test/regress/regress1/rels/rel_mix_0_1.cvc.smt2 +++ b/test/regress/regress1/rels/rel_mix_0_1.cvc.smt2 @@ -10,12 +10,12 @@ (declare-fun z () (Set (Tuple Int))) (declare-fun r2 () (Set (Tuple Int Int))) (declare-fun d () (Tuple Int Int)) -(assert (= d (mkTuple 1 3))) -(assert (member (mkTuple 1 3) y)) +(assert (= d (tuple 1 3))) +(assert (member (tuple 1 3) y)) (declare-fun a () (Tuple Int Int)) (assert (member a x)) (declare-fun e () (Tuple Int Int)) -(assert (= e (mkTuple 4 3))) +(assert (= e (tuple 4 3))) (assert (= r (join x y))) (assert (= r2 (product w z))) (assert (not (member e r))) diff --git a/test/regress/regress1/rels/rel_pressure_0.cvc.smt2 b/test/regress/regress1/rels/rel_pressure_0.cvc.smt2 index 698f2f5d9..d56f72e77 100644 --- a/test/regress/regress1/rels/rel_pressure_0.cvc.smt2 +++ b/test/regress/regress1/rels/rel_pressure_0.cvc.smt2 @@ -7,608 +7,608 @@ (declare-fun z () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun a11 () (Tuple Int Int)) -(assert (= a11 (mkTuple 1 1))) +(assert (= a11 (tuple 1 1))) (assert (member a11 x)) (declare-fun a12 () (Tuple Int Int)) -(assert (= a12 (mkTuple 1 2))) +(assert (= a12 (tuple 1 2))) (assert (member a12 x)) (declare-fun a13 () (Tuple Int Int)) -(assert (= a13 (mkTuple 1 3))) +(assert (= a13 (tuple 1 3))) (assert (member a13 x)) (declare-fun a14 () (Tuple Int Int)) -(assert (= a14 (mkTuple 1 4))) +(assert (= a14 (tuple 1 4))) (assert (member a14 x)) (declare-fun a15 () (Tuple Int Int)) -(assert (= a15 (mkTuple 1 5))) +(assert (= a15 (tuple 1 5))) (assert (member a15 x)) (declare-fun a16 () (Tuple Int Int)) -(assert (= a16 (mkTuple 1 6))) +(assert (= a16 (tuple 1 6))) (assert (member a16 x)) (declare-fun a17 () (Tuple Int Int)) -(assert (= a17 (mkTuple 1 7))) +(assert (= a17 (tuple 1 7))) (assert (member a17 x)) (declare-fun a18 () (Tuple Int Int)) -(assert (= a18 (mkTuple 1 8))) +(assert (= a18 (tuple 1 8))) (assert (member a18 x)) (declare-fun a19 () (Tuple Int Int)) -(assert (= a19 (mkTuple 1 9))) +(assert (= a19 (tuple 1 9))) (assert (member a19 x)) (declare-fun a110 () (Tuple Int Int)) -(assert (= a110 (mkTuple 1 10))) +(assert (= a110 (tuple 1 10))) (assert (member a110 x)) (declare-fun a21 () (Tuple Int Int)) -(assert (= a21 (mkTuple 2 1))) +(assert (= a21 (tuple 2 1))) (assert (member a21 x)) (declare-fun a22 () (Tuple Int Int)) -(assert (= a22 (mkTuple 2 2))) +(assert (= a22 (tuple 2 2))) (assert (member a22 x)) (declare-fun a23 () (Tuple Int Int)) -(assert (= a23 (mkTuple 2 3))) +(assert (= a23 (tuple 2 3))) (assert (member a23 x)) (declare-fun a24 () (Tuple Int Int)) -(assert (= a24 (mkTuple 2 4))) +(assert (= a24 (tuple 2 4))) (assert (member a24 x)) (declare-fun a25 () (Tuple Int Int)) -(assert (= a25 (mkTuple 2 5))) +(assert (= a25 (tuple 2 5))) (assert (member a25 x)) (declare-fun a26 () (Tuple Int Int)) -(assert (= a26 (mkTuple 2 6))) +(assert (= a26 (tuple 2 6))) (assert (member a26 x)) (declare-fun a27 () (Tuple Int Int)) -(assert (= a27 (mkTuple 2 7))) +(assert (= a27 (tuple 2 7))) (assert (member a27 x)) (declare-fun a28 () (Tuple Int Int)) -(assert (= a28 (mkTuple 2 8))) +(assert (= a28 (tuple 2 8))) (assert (member a28 x)) (declare-fun a29 () (Tuple Int Int)) -(assert (= a29 (mkTuple 2 9))) +(assert (= a29 (tuple 2 9))) (assert (member a29 x)) (declare-fun a210 () (Tuple Int Int)) -(assert (= a210 (mkTuple 2 10))) +(assert (= a210 (tuple 2 10))) (assert (member a210 x)) (declare-fun a31 () (Tuple Int Int)) -(assert (= a31 (mkTuple 3 1))) +(assert (= a31 (tuple 3 1))) (assert (member a31 x)) (declare-fun a32 () (Tuple Int Int)) -(assert (= a32 (mkTuple 3 2))) +(assert (= a32 (tuple 3 2))) (assert (member a32 x)) (declare-fun a33 () (Tuple Int Int)) -(assert (= a33 (mkTuple 3 3))) +(assert (= a33 (tuple 3 3))) (assert (member a33 x)) (declare-fun a34 () (Tuple Int Int)) -(assert (= a34 (mkTuple 3 4))) +(assert (= a34 (tuple 3 4))) (assert (member a34 x)) (declare-fun a35 () (Tuple Int Int)) -(assert (= a35 (mkTuple 3 5))) +(assert (= a35 (tuple 3 5))) (assert (member a35 x)) (declare-fun a36 () (Tuple Int Int)) -(assert (= a36 (mkTuple 3 6))) +(assert (= a36 (tuple 3 6))) (assert (member a36 x)) (declare-fun a37 () (Tuple Int Int)) -(assert (= a37 (mkTuple 3 7))) +(assert (= a37 (tuple 3 7))) (assert (member a37 x)) (declare-fun a38 () (Tuple Int Int)) -(assert (= a38 (mkTuple 3 8))) +(assert (= a38 (tuple 3 8))) (assert (member a38 x)) (declare-fun a39 () (Tuple Int Int)) -(assert (= a39 (mkTuple 3 9))) +(assert (= a39 (tuple 3 9))) (assert (member a39 x)) (declare-fun a310 () (Tuple Int Int)) -(assert (= a310 (mkTuple 3 10))) +(assert (= a310 (tuple 3 10))) (assert (member a310 x)) (declare-fun a41 () (Tuple Int Int)) -(assert (= a41 (mkTuple 4 1))) +(assert (= a41 (tuple 4 1))) (assert (member a41 x)) (declare-fun a42 () (Tuple Int Int)) -(assert (= a42 (mkTuple 4 2))) +(assert (= a42 (tuple 4 2))) (assert (member a42 x)) (declare-fun a43 () (Tuple Int Int)) -(assert (= a43 (mkTuple 4 3))) +(assert (= a43 (tuple 4 3))) (assert (member a43 x)) (declare-fun a44 () (Tuple Int Int)) -(assert (= a44 (mkTuple 4 4))) +(assert (= a44 (tuple 4 4))) (assert (member a44 x)) (declare-fun a45 () (Tuple Int Int)) -(assert (= a45 (mkTuple 4 5))) +(assert (= a45 (tuple 4 5))) (assert (member a45 x)) (declare-fun a46 () (Tuple Int Int)) -(assert (= a46 (mkTuple 4 6))) +(assert (= a46 (tuple 4 6))) (assert (member a46 x)) (declare-fun a47 () (Tuple Int Int)) -(assert (= a47 (mkTuple 4 7))) +(assert (= a47 (tuple 4 7))) (assert (member a47 x)) (declare-fun a48 () (Tuple Int Int)) -(assert (= a48 (mkTuple 4 8))) +(assert (= a48 (tuple 4 8))) (assert (member a48 x)) (declare-fun a49 () (Tuple Int Int)) -(assert (= a49 (mkTuple 4 9))) +(assert (= a49 (tuple 4 9))) (assert (member a49 x)) (declare-fun a410 () (Tuple Int Int)) -(assert (= a410 (mkTuple 4 10))) +(assert (= a410 (tuple 4 10))) (assert (member a410 x)) (declare-fun a51 () (Tuple Int Int)) -(assert (= a51 (mkTuple 5 1))) +(assert (= a51 (tuple 5 1))) (assert (member a51 x)) (declare-fun a52 () (Tuple Int Int)) -(assert (= a52 (mkTuple 5 2))) +(assert (= a52 (tuple 5 2))) (assert (member a52 x)) (declare-fun a53 () (Tuple Int Int)) -(assert (= a53 (mkTuple 5 3))) +(assert (= a53 (tuple 5 3))) (assert (member a53 x)) (declare-fun a54 () (Tuple Int Int)) -(assert (= a54 (mkTuple 5 4))) +(assert (= a54 (tuple 5 4))) (assert (member a54 x)) (declare-fun a55 () (Tuple Int Int)) -(assert (= a55 (mkTuple 5 5))) +(assert (= a55 (tuple 5 5))) (assert (member a55 x)) (declare-fun a56 () (Tuple Int Int)) -(assert (= a56 (mkTuple 5 6))) +(assert (= a56 (tuple 5 6))) (assert (member a56 x)) (declare-fun a57 () (Tuple Int Int)) -(assert (= a57 (mkTuple 5 7))) +(assert (= a57 (tuple 5 7))) (assert (member a57 x)) (declare-fun a58 () (Tuple Int Int)) -(assert (= a58 (mkTuple 5 8))) +(assert (= a58 (tuple 5 8))) (assert (member a58 x)) (declare-fun a59 () (Tuple Int Int)) -(assert (= a59 (mkTuple 5 9))) +(assert (= a59 (tuple 5 9))) (assert (member a59 x)) (declare-fun a510 () (Tuple Int Int)) -(assert (= a510 (mkTuple 5 10))) +(assert (= a510 (tuple 5 10))) (assert (member a510 x)) (declare-fun a61 () (Tuple Int Int)) -(assert (= a61 (mkTuple 6 1))) +(assert (= a61 (tuple 6 1))) (assert (member a61 x)) (declare-fun a62 () (Tuple Int Int)) -(assert (= a62 (mkTuple 6 2))) +(assert (= a62 (tuple 6 2))) (assert (member a62 x)) (declare-fun a63 () (Tuple Int Int)) -(assert (= a63 (mkTuple 6 3))) +(assert (= a63 (tuple 6 3))) (assert (member a63 x)) (declare-fun a64 () (Tuple Int Int)) -(assert (= a64 (mkTuple 6 4))) +(assert (= a64 (tuple 6 4))) (assert (member a64 x)) (declare-fun a65 () (Tuple Int Int)) -(assert (= a65 (mkTuple 6 5))) +(assert (= a65 (tuple 6 5))) (assert (member a65 x)) (declare-fun a66 () (Tuple Int Int)) -(assert (= a66 (mkTuple 6 6))) +(assert (= a66 (tuple 6 6))) (assert (member a66 x)) (declare-fun a67 () (Tuple Int Int)) -(assert (= a67 (mkTuple 6 7))) +(assert (= a67 (tuple 6 7))) (assert (member a67 x)) (declare-fun a68 () (Tuple Int Int)) -(assert (= a68 (mkTuple 6 8))) +(assert (= a68 (tuple 6 8))) (assert (member a68 x)) (declare-fun a69 () (Tuple Int Int)) -(assert (= a69 (mkTuple 6 9))) +(assert (= a69 (tuple 6 9))) (assert (member a69 x)) (declare-fun a610 () (Tuple Int Int)) -(assert (= a610 (mkTuple 6 10))) +(assert (= a610 (tuple 6 10))) (assert (member a610 x)) (declare-fun a71 () (Tuple Int Int)) -(assert (= a71 (mkTuple 7 1))) +(assert (= a71 (tuple 7 1))) (assert (member a71 x)) (declare-fun a72 () (Tuple Int Int)) -(assert (= a72 (mkTuple 7 2))) +(assert (= a72 (tuple 7 2))) (assert (member a72 x)) (declare-fun a73 () (Tuple Int Int)) -(assert (= a73 (mkTuple 7 3))) +(assert (= a73 (tuple 7 3))) (assert (member a73 x)) (declare-fun a74 () (Tuple Int Int)) -(assert (= a74 (mkTuple 7 4))) +(assert (= a74 (tuple 7 4))) (assert (member a74 x)) (declare-fun a75 () (Tuple Int Int)) -(assert (= a75 (mkTuple 7 5))) +(assert (= a75 (tuple 7 5))) (assert (member a75 x)) (declare-fun a76 () (Tuple Int Int)) -(assert (= a76 (mkTuple 7 6))) +(assert (= a76 (tuple 7 6))) (assert (member a76 x)) (declare-fun a77 () (Tuple Int Int)) -(assert (= a77 (mkTuple 7 7))) +(assert (= a77 (tuple 7 7))) (assert (member a77 x)) (declare-fun a78 () (Tuple Int Int)) -(assert (= a78 (mkTuple 7 8))) +(assert (= a78 (tuple 7 8))) (assert (member a78 x)) (declare-fun a79 () (Tuple Int Int)) -(assert (= a79 (mkTuple 7 9))) +(assert (= a79 (tuple 7 9))) (assert (member a79 x)) (declare-fun a710 () (Tuple Int Int)) -(assert (= a710 (mkTuple 7 10))) +(assert (= a710 (tuple 7 10))) (assert (member a710 x)) (declare-fun a81 () (Tuple Int Int)) -(assert (= a81 (mkTuple 8 1))) +(assert (= a81 (tuple 8 1))) (assert (member a81 x)) (declare-fun a82 () (Tuple Int Int)) -(assert (= a82 (mkTuple 8 2))) +(assert (= a82 (tuple 8 2))) (assert (member a82 x)) (declare-fun a83 () (Tuple Int Int)) -(assert (= a83 (mkTuple 8 3))) +(assert (= a83 (tuple 8 3))) (assert (member a83 x)) (declare-fun a84 () (Tuple Int Int)) -(assert (= a84 (mkTuple 8 4))) +(assert (= a84 (tuple 8 4))) (assert (member a84 x)) (declare-fun a85 () (Tuple Int Int)) -(assert (= a85 (mkTuple 8 5))) +(assert (= a85 (tuple 8 5))) (assert (member a85 x)) (declare-fun a86 () (Tuple Int Int)) -(assert (= a86 (mkTuple 8 6))) +(assert (= a86 (tuple 8 6))) (assert (member a86 x)) (declare-fun a87 () (Tuple Int Int)) -(assert (= a87 (mkTuple 8 7))) +(assert (= a87 (tuple 8 7))) (assert (member a87 x)) (declare-fun a88 () (Tuple Int Int)) -(assert (= a88 (mkTuple 8 8))) +(assert (= a88 (tuple 8 8))) (assert (member a88 x)) (declare-fun a89 () (Tuple Int Int)) -(assert (= a89 (mkTuple 8 9))) +(assert (= a89 (tuple 8 9))) (assert (member a89 x)) (declare-fun a810 () (Tuple Int Int)) -(assert (= a810 (mkTuple 8 10))) +(assert (= a810 (tuple 8 10))) (assert (member a810 x)) (declare-fun a91 () (Tuple Int Int)) -(assert (= a91 (mkTuple 9 1))) +(assert (= a91 (tuple 9 1))) (assert (member a91 x)) (declare-fun a92 () (Tuple Int Int)) -(assert (= a92 (mkTuple 9 2))) +(assert (= a92 (tuple 9 2))) (assert (member a92 x)) (declare-fun a93 () (Tuple Int Int)) -(assert (= a93 (mkTuple 9 3))) +(assert (= a93 (tuple 9 3))) (assert (member a93 x)) (declare-fun a94 () (Tuple Int Int)) -(assert (= a94 (mkTuple 9 4))) +(assert (= a94 (tuple 9 4))) (assert (member a94 x)) (declare-fun a95 () (Tuple Int Int)) -(assert (= a95 (mkTuple 9 5))) +(assert (= a95 (tuple 9 5))) (assert (member a95 x)) (declare-fun a96 () (Tuple Int Int)) -(assert (= a96 (mkTuple 9 6))) +(assert (= a96 (tuple 9 6))) (assert (member a96 x)) (declare-fun a97 () (Tuple Int Int)) -(assert (= a97 (mkTuple 9 7))) +(assert (= a97 (tuple 9 7))) (assert (member a97 x)) (declare-fun a98 () (Tuple Int Int)) -(assert (= a98 (mkTuple 9 8))) +(assert (= a98 (tuple 9 8))) (assert (member a98 x)) (declare-fun a99 () (Tuple Int Int)) -(assert (= a99 (mkTuple 9 9))) +(assert (= a99 (tuple 9 9))) (assert (member a99 x)) (declare-fun a910 () (Tuple Int Int)) -(assert (= a910 (mkTuple 9 10))) +(assert (= a910 (tuple 9 10))) (assert (member a910 x)) (declare-fun a101 () (Tuple Int Int)) -(assert (= a101 (mkTuple 10 1))) +(assert (= a101 (tuple 10 1))) (assert (member a101 x)) (declare-fun a102 () (Tuple Int Int)) -(assert (= a102 (mkTuple 10 2))) +(assert (= a102 (tuple 10 2))) (assert (member a102 x)) (declare-fun a103 () (Tuple Int Int)) -(assert (= a103 (mkTuple 10 3))) +(assert (= a103 (tuple 10 3))) (assert (member a103 x)) (declare-fun a104 () (Tuple Int Int)) -(assert (= a104 (mkTuple 10 4))) +(assert (= a104 (tuple 10 4))) (assert (member a104 x)) (declare-fun a105 () (Tuple Int Int)) -(assert (= a105 (mkTuple 10 5))) +(assert (= a105 (tuple 10 5))) (assert (member a105 x)) (declare-fun a106 () (Tuple Int Int)) -(assert (= a106 (mkTuple 10 6))) +(assert (= a106 (tuple 10 6))) (assert (member a106 x)) (declare-fun a107 () (Tuple Int Int)) -(assert (= a107 (mkTuple 10 7))) +(assert (= a107 (tuple 10 7))) (assert (member a107 x)) (declare-fun a108 () (Tuple Int Int)) -(assert (= a108 (mkTuple 10 8))) +(assert (= a108 (tuple 10 8))) (assert (member a108 x)) (declare-fun a109 () (Tuple Int Int)) -(assert (= a109 (mkTuple 10 9))) +(assert (= a109 (tuple 10 9))) (assert (member a109 x)) (declare-fun a1010 () (Tuple Int Int)) -(assert (= a1010 (mkTuple 10 10))) +(assert (= a1010 (tuple 10 10))) (assert (member a1010 x)) (declare-fun b11 () (Tuple Int Int)) -(assert (= b11 (mkTuple 1 1))) +(assert (= b11 (tuple 1 1))) (assert (member b11 y)) (declare-fun b12 () (Tuple Int Int)) -(assert (= b12 (mkTuple 1 2))) +(assert (= b12 (tuple 1 2))) (assert (member b12 y)) (declare-fun b13 () (Tuple Int Int)) -(assert (= b13 (mkTuple 1 3))) +(assert (= b13 (tuple 1 3))) (assert (member b13 y)) (declare-fun b14 () (Tuple Int Int)) -(assert (= b14 (mkTuple 1 4))) +(assert (= b14 (tuple 1 4))) (assert (member b14 y)) (declare-fun b15 () (Tuple Int Int)) -(assert (= b15 (mkTuple 1 5))) +(assert (= b15 (tuple 1 5))) (assert (member b15 y)) (declare-fun b16 () (Tuple Int Int)) -(assert (= b16 (mkTuple 1 6))) +(assert (= b16 (tuple 1 6))) (assert (member b16 y)) (declare-fun b17 () (Tuple Int Int)) -(assert (= b17 (mkTuple 1 7))) +(assert (= b17 (tuple 1 7))) (assert (member b17 y)) (declare-fun b18 () (Tuple Int Int)) -(assert (= b18 (mkTuple 1 8))) +(assert (= b18 (tuple 1 8))) (assert (member b18 y)) (declare-fun b19 () (Tuple Int Int)) -(assert (= b19 (mkTuple 1 9))) +(assert (= b19 (tuple 1 9))) (assert (member b19 y)) (declare-fun b110 () (Tuple Int Int)) -(assert (= b110 (mkTuple 1 10))) +(assert (= b110 (tuple 1 10))) (assert (member b110 y)) (declare-fun b21 () (Tuple Int Int)) -(assert (= b21 (mkTuple 2 1))) +(assert (= b21 (tuple 2 1))) (assert (member b21 y)) (declare-fun b22 () (Tuple Int Int)) -(assert (= b22 (mkTuple 2 2))) +(assert (= b22 (tuple 2 2))) (assert (member b22 y)) (declare-fun b23 () (Tuple Int Int)) -(assert (= b23 (mkTuple 2 3))) +(assert (= b23 (tuple 2 3))) (assert (member b23 y)) (declare-fun b24 () (Tuple Int Int)) -(assert (= b24 (mkTuple 2 4))) +(assert (= b24 (tuple 2 4))) (assert (member b24 y)) (declare-fun b25 () (Tuple Int Int)) -(assert (= b25 (mkTuple 2 5))) +(assert (= b25 (tuple 2 5))) (assert (member b25 y)) (declare-fun b26 () (Tuple Int Int)) -(assert (= b26 (mkTuple 2 6))) +(assert (= b26 (tuple 2 6))) (assert (member b26 y)) (declare-fun b27 () (Tuple Int Int)) -(assert (= b27 (mkTuple 2 7))) +(assert (= b27 (tuple 2 7))) (assert (member b27 y)) (declare-fun b28 () (Tuple Int Int)) -(assert (= b28 (mkTuple 2 8))) +(assert (= b28 (tuple 2 8))) (assert (member b28 y)) (declare-fun b29 () (Tuple Int Int)) -(assert (= b29 (mkTuple 2 9))) +(assert (= b29 (tuple 2 9))) (assert (member b29 y)) (declare-fun b210 () (Tuple Int Int)) -(assert (= b210 (mkTuple 2 10))) +(assert (= b210 (tuple 2 10))) (assert (member b210 y)) (declare-fun b31 () (Tuple Int Int)) -(assert (= b31 (mkTuple 3 1))) +(assert (= b31 (tuple 3 1))) (assert (member b31 y)) (declare-fun b32 () (Tuple Int Int)) -(assert (= b32 (mkTuple 3 2))) +(assert (= b32 (tuple 3 2))) (assert (member b32 y)) (declare-fun b33 () (Tuple Int Int)) -(assert (= b33 (mkTuple 3 3))) +(assert (= b33 (tuple 3 3))) (assert (member b33 y)) (declare-fun b34 () (Tuple Int Int)) -(assert (= b34 (mkTuple 3 4))) +(assert (= b34 (tuple 3 4))) (assert (member b34 y)) (declare-fun b35 () (Tuple Int Int)) -(assert (= b35 (mkTuple 3 5))) +(assert (= b35 (tuple 3 5))) (assert (member b35 y)) (declare-fun b36 () (Tuple Int Int)) -(assert (= b36 (mkTuple 3 6))) +(assert (= b36 (tuple 3 6))) (assert (member b36 y)) (declare-fun b37 () (Tuple Int Int)) -(assert (= b37 (mkTuple 3 7))) +(assert (= b37 (tuple 3 7))) (assert (member b37 y)) (declare-fun b38 () (Tuple Int Int)) -(assert (= b38 (mkTuple 3 8))) +(assert (= b38 (tuple 3 8))) (assert (member b38 y)) (declare-fun b39 () (Tuple Int Int)) -(assert (= b39 (mkTuple 3 9))) +(assert (= b39 (tuple 3 9))) (assert (member b39 y)) (declare-fun b310 () (Tuple Int Int)) -(assert (= b310 (mkTuple 3 10))) +(assert (= b310 (tuple 3 10))) (assert (member b310 y)) (declare-fun b41 () (Tuple Int Int)) -(assert (= b41 (mkTuple 4 1))) +(assert (= b41 (tuple 4 1))) (assert (member b41 y)) (declare-fun b42 () (Tuple Int Int)) -(assert (= b42 (mkTuple 4 2))) +(assert (= b42 (tuple 4 2))) (assert (member b42 y)) (declare-fun b43 () (Tuple Int Int)) -(assert (= b43 (mkTuple 4 3))) +(assert (= b43 (tuple 4 3))) (assert (member b43 y)) (declare-fun b44 () (Tuple Int Int)) -(assert (= b44 (mkTuple 4 4))) +(assert (= b44 (tuple 4 4))) (assert (member b44 y)) (declare-fun b45 () (Tuple Int Int)) -(assert (= b45 (mkTuple 4 5))) +(assert (= b45 (tuple 4 5))) (assert (member b45 y)) (declare-fun b46 () (Tuple Int Int)) -(assert (= b46 (mkTuple 4 6))) +(assert (= b46 (tuple 4 6))) (assert (member b46 y)) (declare-fun b47 () (Tuple Int Int)) -(assert (= b47 (mkTuple 4 7))) +(assert (= b47 (tuple 4 7))) (assert (member b47 y)) (declare-fun b48 () (Tuple Int Int)) -(assert (= b48 (mkTuple 4 8))) +(assert (= b48 (tuple 4 8))) (assert (member b48 y)) (declare-fun b49 () (Tuple Int Int)) -(assert (= b49 (mkTuple 4 9))) +(assert (= b49 (tuple 4 9))) (assert (member b49 y)) (declare-fun b410 () (Tuple Int Int)) -(assert (= b410 (mkTuple 4 10))) +(assert (= b410 (tuple 4 10))) (assert (member b410 y)) (declare-fun b51 () (Tuple Int Int)) -(assert (= b51 (mkTuple 5 1))) +(assert (= b51 (tuple 5 1))) (assert (member b51 y)) (declare-fun b52 () (Tuple Int Int)) -(assert (= b52 (mkTuple 5 2))) +(assert (= b52 (tuple 5 2))) (assert (member b52 y)) (declare-fun b53 () (Tuple Int Int)) -(assert (= b53 (mkTuple 5 3))) +(assert (= b53 (tuple 5 3))) (assert (member b53 y)) (declare-fun b54 () (Tuple Int Int)) -(assert (= b54 (mkTuple 5 4))) +(assert (= b54 (tuple 5 4))) (assert (member b54 y)) (declare-fun b55 () (Tuple Int Int)) -(assert (= b55 (mkTuple 5 5))) +(assert (= b55 (tuple 5 5))) (assert (member b55 y)) (declare-fun b56 () (Tuple Int Int)) -(assert (= b56 (mkTuple 5 6))) +(assert (= b56 (tuple 5 6))) (assert (member b56 y)) (declare-fun b57 () (Tuple Int Int)) -(assert (= b57 (mkTuple 5 7))) +(assert (= b57 (tuple 5 7))) (assert (member b57 y)) (declare-fun b58 () (Tuple Int Int)) -(assert (= b58 (mkTuple 5 8))) +(assert (= b58 (tuple 5 8))) (assert (member b58 y)) (declare-fun b59 () (Tuple Int Int)) -(assert (= b59 (mkTuple 5 9))) +(assert (= b59 (tuple 5 9))) (assert (member b59 y)) (declare-fun b510 () (Tuple Int Int)) -(assert (= b510 (mkTuple 5 10))) +(assert (= b510 (tuple 5 10))) (assert (member b510 y)) (declare-fun b61 () (Tuple Int Int)) -(assert (= b61 (mkTuple 6 1))) +(assert (= b61 (tuple 6 1))) (assert (member b61 y)) (declare-fun b62 () (Tuple Int Int)) -(assert (= b62 (mkTuple 6 2))) +(assert (= b62 (tuple 6 2))) (assert (member b62 y)) (declare-fun b63 () (Tuple Int Int)) -(assert (= b63 (mkTuple 6 3))) +(assert (= b63 (tuple 6 3))) (assert (member b63 y)) (declare-fun b64 () (Tuple Int Int)) -(assert (= b64 (mkTuple 6 4))) +(assert (= b64 (tuple 6 4))) (assert (member b64 y)) (declare-fun b65 () (Tuple Int Int)) -(assert (= b65 (mkTuple 6 5))) +(assert (= b65 (tuple 6 5))) (assert (member b65 y)) (declare-fun b66 () (Tuple Int Int)) -(assert (= b66 (mkTuple 6 6))) +(assert (= b66 (tuple 6 6))) (assert (member b66 y)) (declare-fun b67 () (Tuple Int Int)) -(assert (= b67 (mkTuple 6 7))) +(assert (= b67 (tuple 6 7))) (assert (member b67 y)) (declare-fun b68 () (Tuple Int Int)) -(assert (= b68 (mkTuple 6 8))) +(assert (= b68 (tuple 6 8))) (assert (member b68 y)) (declare-fun b69 () (Tuple Int Int)) -(assert (= b69 (mkTuple 6 9))) +(assert (= b69 (tuple 6 9))) (assert (member b69 y)) (declare-fun b610 () (Tuple Int Int)) -(assert (= b610 (mkTuple 6 10))) +(assert (= b610 (tuple 6 10))) (assert (member b610 y)) (declare-fun b71 () (Tuple Int Int)) -(assert (= b71 (mkTuple 7 1))) +(assert (= b71 (tuple 7 1))) (assert (member b71 y)) (declare-fun b72 () (Tuple Int Int)) -(assert (= b72 (mkTuple 7 2))) +(assert (= b72 (tuple 7 2))) (assert (member b72 y)) (declare-fun b73 () (Tuple Int Int)) -(assert (= b73 (mkTuple 7 3))) +(assert (= b73 (tuple 7 3))) (assert (member b73 y)) (declare-fun b74 () (Tuple Int Int)) -(assert (= b74 (mkTuple 7 4))) +(assert (= b74 (tuple 7 4))) (assert (member b74 y)) (declare-fun b75 () (Tuple Int Int)) -(assert (= b75 (mkTuple 7 5))) +(assert (= b75 (tuple 7 5))) (assert (member b75 y)) (declare-fun b76 () (Tuple Int Int)) -(assert (= b76 (mkTuple 7 6))) +(assert (= b76 (tuple 7 6))) (assert (member b76 y)) (declare-fun b77 () (Tuple Int Int)) -(assert (= b77 (mkTuple 7 7))) +(assert (= b77 (tuple 7 7))) (assert (member b77 y)) (declare-fun b78 () (Tuple Int Int)) -(assert (= b78 (mkTuple 7 8))) +(assert (= b78 (tuple 7 8))) (assert (member b78 y)) (declare-fun b79 () (Tuple Int Int)) -(assert (= b79 (mkTuple 7 9))) +(assert (= b79 (tuple 7 9))) (assert (member b79 y)) (declare-fun b710 () (Tuple Int Int)) -(assert (= b710 (mkTuple 7 10))) +(assert (= b710 (tuple 7 10))) (assert (member b710 y)) (declare-fun b81 () (Tuple Int Int)) -(assert (= b81 (mkTuple 8 1))) +(assert (= b81 (tuple 8 1))) (assert (member b81 y)) (declare-fun b82 () (Tuple Int Int)) -(assert (= b82 (mkTuple 8 2))) +(assert (= b82 (tuple 8 2))) (assert (member b82 y)) (declare-fun b83 () (Tuple Int Int)) -(assert (= b83 (mkTuple 8 3))) +(assert (= b83 (tuple 8 3))) (assert (member b83 y)) (declare-fun b84 () (Tuple Int Int)) -(assert (= b84 (mkTuple 8 4))) +(assert (= b84 (tuple 8 4))) (assert (member b84 y)) (declare-fun b85 () (Tuple Int Int)) -(assert (= b85 (mkTuple 8 5))) +(assert (= b85 (tuple 8 5))) (assert (member b85 y)) (declare-fun b86 () (Tuple Int Int)) -(assert (= b86 (mkTuple 8 6))) +(assert (= b86 (tuple 8 6))) (assert (member b86 y)) (declare-fun b87 () (Tuple Int Int)) -(assert (= b87 (mkTuple 8 7))) +(assert (= b87 (tuple 8 7))) (assert (member b87 y)) (declare-fun b88 () (Tuple Int Int)) -(assert (= b88 (mkTuple 8 8))) +(assert (= b88 (tuple 8 8))) (assert (member b88 y)) (declare-fun b89 () (Tuple Int Int)) -(assert (= b89 (mkTuple 8 9))) +(assert (= b89 (tuple 8 9))) (assert (member b89 y)) (declare-fun b810 () (Tuple Int Int)) -(assert (= b810 (mkTuple 8 10))) +(assert (= b810 (tuple 8 10))) (assert (member b810 y)) (declare-fun b91 () (Tuple Int Int)) -(assert (= b91 (mkTuple 9 1))) +(assert (= b91 (tuple 9 1))) (assert (member b91 y)) (declare-fun b92 () (Tuple Int Int)) -(assert (= b92 (mkTuple 9 2))) +(assert (= b92 (tuple 9 2))) (assert (member b92 y)) (declare-fun b93 () (Tuple Int Int)) -(assert (= b93 (mkTuple 9 3))) +(assert (= b93 (tuple 9 3))) (assert (member b93 y)) (declare-fun b94 () (Tuple Int Int)) -(assert (= b94 (mkTuple 9 4))) +(assert (= b94 (tuple 9 4))) (assert (member b94 y)) (declare-fun b95 () (Tuple Int Int)) -(assert (= b95 (mkTuple 9 5))) +(assert (= b95 (tuple 9 5))) (assert (member b95 y)) (declare-fun b96 () (Tuple Int Int)) -(assert (= b96 (mkTuple 9 6))) +(assert (= b96 (tuple 9 6))) (assert (member b96 y)) (declare-fun b97 () (Tuple Int Int)) -(assert (= b97 (mkTuple 9 7))) +(assert (= b97 (tuple 9 7))) (assert (member b97 y)) (declare-fun b98 () (Tuple Int Int)) -(assert (= b98 (mkTuple 9 8))) +(assert (= b98 (tuple 9 8))) (assert (member b98 y)) (declare-fun b99 () (Tuple Int Int)) -(assert (= b99 (mkTuple 9 9))) +(assert (= b99 (tuple 9 9))) (assert (member b99 y)) (declare-fun b910 () (Tuple Int Int)) -(assert (= b910 (mkTuple 9 10))) +(assert (= b910 (tuple 9 10))) (assert (member b910 y)) (declare-fun b101 () (Tuple Int Int)) -(assert (= b101 (mkTuple 10 1))) +(assert (= b101 (tuple 10 1))) (assert (member b101 y)) (declare-fun b102 () (Tuple Int Int)) -(assert (= b102 (mkTuple 10 2))) +(assert (= b102 (tuple 10 2))) (assert (member b102 y)) (declare-fun b103 () (Tuple Int Int)) -(assert (= b103 (mkTuple 10 3))) +(assert (= b103 (tuple 10 3))) (assert (member b103 y)) (declare-fun b104 () (Tuple Int Int)) -(assert (= b104 (mkTuple 10 4))) +(assert (= b104 (tuple 10 4))) (assert (member b104 y)) (declare-fun b105 () (Tuple Int Int)) -(assert (= b105 (mkTuple 10 5))) +(assert (= b105 (tuple 10 5))) (assert (member b105 y)) (declare-fun b106 () (Tuple Int Int)) -(assert (= b106 (mkTuple 10 6))) +(assert (= b106 (tuple 10 6))) (assert (member b106 y)) (declare-fun b107 () (Tuple Int Int)) -(assert (= b107 (mkTuple 10 7))) +(assert (= b107 (tuple 10 7))) (assert (member b107 y)) (declare-fun b108 () (Tuple Int Int)) -(assert (= b108 (mkTuple 10 8))) +(assert (= b108 (tuple 10 8))) (assert (member b108 y)) (declare-fun b109 () (Tuple Int Int)) -(assert (= b109 (mkTuple 10 9))) +(assert (= b109 (tuple 10 9))) (assert (member b109 y)) (declare-fun b1010 () (Tuple Int Int)) -(assert (= b1010 (mkTuple 10 10))) +(assert (= b1010 (tuple 10 10))) (assert (member b1010 y)) -(assert (member (mkTuple 1 9) z)) +(assert (member (tuple 1 9) z)) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 9 1))) +(assert (= a (tuple 9 1))) (assert (= r (join (join (transpose x) y) z))) (assert (not (member a (transpose r)))) (check-sat) diff --git a/test/regress/regress1/rels/rel_tc_10_1.cvc.smt2 b/test/regress/regress1/rels/rel_tc_10_1.cvc.smt2 index 32d670b25..af871781e 100644 --- a/test/regress/regress1/rels/rel_tc_10_1.cvc.smt2 +++ b/test/regress/regress1/rels/rel_tc_10_1.cvc.smt2 @@ -10,9 +10,9 @@ (declare-fun d () Int) (assert (= a c)) (assert (= a d)) -(assert (member (mkTuple 1 c) x)) -(assert (member (mkTuple 2 d) x)) -(assert (member (mkTuple a 5) y)) +(assert (member (tuple 1 c) x)) +(assert (member (tuple 2 d) x)) +(assert (member (tuple a 5) y)) (assert (= y (tclosure x))) -(assert (member (mkTuple 2 5) y)) +(assert (member (tuple 2 5) y)) (check-sat) diff --git a/test/regress/regress1/rels/rel_tc_4.cvc.smt2 b/test/regress/regress1/rels/rel_tc_4.cvc.smt2 index 29cb0609f..5de402d3b 100644 --- a/test/regress/regress1/rels/rel_tc_4.cvc.smt2 +++ b/test/regress/regress1/rels/rel_tc_4.cvc.smt2 @@ -8,11 +8,11 @@ (declare-fun b () Int) (declare-fun c () Int) (declare-fun d () Int) -(assert (member (mkTuple 1 a) x)) -(assert (member (mkTuple 1 c) x)) -(assert (member (mkTuple 1 d) x)) -(assert (member (mkTuple b 1) x)) +(assert (member (tuple 1 a) x)) +(assert (member (tuple 1 c) x)) +(assert (member (tuple 1 d) x)) +(assert (member (tuple b 1) x)) (assert (= b d)) -(assert (member (mkTuple 2 b) (join (join x x) x))) -(assert (not (member (mkTuple 2 1) (tclosure x)))) +(assert (member (tuple 2 b) (join (join x x) x))) +(assert (not (member (tuple 2 1) (tclosure x)))) (check-sat) diff --git a/test/regress/regress1/rels/rel_tc_9_1.cvc.smt2 b/test/regress/regress1/rels/rel_tc_9_1.cvc.smt2 index 599d30946..0cfacd14a 100644 --- a/test/regress/regress1/rels/rel_tc_9_1.cvc.smt2 +++ b/test/regress/regress1/rels/rel_tc_9_1.cvc.smt2 @@ -8,15 +8,15 @@ (declare-fun w () (Set (Tuple Int Int))) (assert (= z (tclosure x))) (assert (= w (join x y))) -(assert (member (mkTuple 2 2) z)) -(assert (member (mkTuple 0 3) y)) -(assert (member (mkTuple (- 1) 3) y)) -(assert (member (mkTuple 1 3) y)) -(assert (member (mkTuple (- 2) 3) y)) -(assert (member (mkTuple 2 3) y)) -(assert (member (mkTuple 3 3) y)) -(assert (member (mkTuple 4 3) y)) -(assert (member (mkTuple 5 3) y)) -(assert (not (member (mkTuple 2 3) (join x y)))) -(assert (not (member (mkTuple 2 1) x))) +(assert (member (tuple 2 2) z)) +(assert (member (tuple 0 3) y)) +(assert (member (tuple (- 1) 3) y)) +(assert (member (tuple 1 3) y)) +(assert (member (tuple (- 2) 3) y)) +(assert (member (tuple 2 3) y)) +(assert (member (tuple 3 3) y)) +(assert (member (tuple 4 3) y)) +(assert (member (tuple 5 3) y)) +(assert (not (member (tuple 2 3) (join x y)))) +(assert (not (member (tuple 2 1) x))) (check-sat) diff --git a/test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2 b/test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2 index 1a71721ac..698d29081 100644 --- a/test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2 +++ b/test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2 @@ -6,13 +6,13 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) -(assert (member (mkTuple 7 1) x)) -(assert (member (mkTuple 2 3) x)) -(assert (member (mkTuple 7 3) y)) -(assert (member (mkTuple 4 7) y)) -(assert (member (mkTuple 3 4) z)) +(assert (member (tuple 7 1) x)) +(assert (member (tuple 2 3) x)) +(assert (member (tuple 7 3) y)) +(assert (member (tuple 4 7) y)) +(assert (member (tuple 3 4) z)) (declare-fun a () (Tuple Int Int)) -(assert (= a (mkTuple 4 1))) +(assert (= a (tuple 4 1))) (assert (= r (join (join (transpose x) y) z))) (assert (member a (transpose r))) (check-sat) diff --git a/test/regress/regress1/rels/set-strat.cvc.smt2 b/test/regress/regress1/rels/set-strat.cvc.smt2 index e1c82de24..53e5588a9 100644 --- a/test/regress/regress1/rels/set-strat.cvc.smt2 +++ b/test/regress/regress1/rels/set-strat.cvc.smt2 @@ -13,8 +13,8 @@ (assert (member a x)) (assert (member b y)) (assert (member b w)) -(assert (member (mkTuple x y) z)) -(assert (member (mkTuple w x) z)) -(assert (not (member (mkTuple x x) (join z z)))) -(assert (member (mkTuple x (singleton (mkTuple 0 0))) (join z z))) +(assert (member (tuple x y) z)) +(assert (member (tuple w x) z)) +(assert (not (member (tuple x x) (join z z)))) +(assert (member (tuple x (singleton (tuple 0 0))) (join z z))) (check-sat) diff --git a/test/regress/regress1/rels/strat.cvc.smt2 b/test/regress/regress1/rels/strat.cvc.smt2 index 0cc6905f2..42850d283 100644 --- a/test/regress/regress1/rels/strat.cvc.smt2 +++ b/test/regress/regress1/rels/strat.cvc.smt2 @@ -13,8 +13,8 @@ (assert (not (= a b))) (assert (member a z)) (assert (member b z)) -(assert (member (mkTuple a b) x)) -(assert (member (mkTuple b a) x)) +(assert (member (tuple a b) x)) +(assert (member (tuple b a) x)) (assert (member c x)) -(assert (and (not (= c (mkTuple a b))) (not (= c (mkTuple b a))))) +(assert (and (not (= c (tuple a b))) (not (= c (tuple b a))))) (check-sat) diff --git a/test/regress/regress1/sets/issue4124-need-check.smt2 b/test/regress/regress1/sets/issue4124-need-check.smt2 index 3ad43ea98..46507df2a 100644 --- a/test/regress/regress1/sets/issue4124-need-check.smt2 +++ b/test/regress/regress1/sets/issue4124-need-check.smt2 @@ -6,8 +6,8 @@ (declare-fun d () (Set (Tuple String String))) (declare-fun f () (Set Int)) (declare-fun e () Int) -(assert (= b (insert (mkTuple "" 1) (mkTuple "" 2) (singleton (mkTuple "" 4))))) -(assert (= c (insert (mkTuple 1 "1") (mkTuple 2 "2") (singleton (mkTuple 7 ""))))) +(assert (= b (insert (tuple "" 1) (tuple "" 2) (singleton (tuple "" 4))))) +(assert (= c (insert (tuple 1 "1") (tuple 2 "2") (singleton (tuple 7 ""))))) (assert (= d (join b c))) (assert (= e (card f))) (check-sat) diff --git a/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2 b/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2 index d15aa3030..d75b9c3ae 100644 --- a/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2 +++ b/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2 @@ -6,8 +6,8 @@ (declare-fun a () (Set (Tuple Real Int))) (declare-fun b () (Set (Tuple Int Real))) (declare-fun x () (Tuple Real Real)) -(assert (let ((_let_1 0.0)) (not (= x (mkTuple _let_1 _let_1))))) -(assert (member (mkTuple ((_ tupSel 0) x) (to_int ((_ tupSel 1) x))) a)) -(assert (member (mkTuple (to_int ((_ tupSel 0) x)) ((_ tupSel 1) x)) b)) -(assert (not (= ((_ tupSel 0) x) ((_ tupSel 1) x)))) +(assert (let ((_let_1 0.0)) (not (= x (tuple _let_1 _let_1))))) +(assert (member (tuple ((_ tuple_select 0) x) (to_int ((_ tuple_select 1) x))) a)) +(assert (member (tuple (to_int ((_ tuple_select 0) x)) ((_ tuple_select 1) x)) b)) +(assert (not (= ((_ tuple_select 0) x) ((_ tuple_select 1) x)))) (check-sat) diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 63556fa8a..19113ae13 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -2520,7 +2520,7 @@ TEST_F(TestApiBlackSolver, tupleProject) } ASSERT_EQ( - "((_ tuple_project 0 3 2 0 1 2) (mkTuple true 3 \"C\" (singleton " + "((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (singleton " "\"Z\")))", projection.toString()); } |