diff options
Diffstat (limited to 'test/regress/regress1/rels')
29 files changed, 342 insertions, 342 deletions
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) |