diff options
Diffstat (limited to 'test/regress/regress0')
140 files changed, 541 insertions, 541 deletions
diff --git a/test/regress/regress0/bug586.cvc.smt2 b/test/regress/regress0/bug586.cvc.smt2 index be5feea1c..88375e3e5 100644 --- a/test/regress/regress0/bug586.cvc.smt2 +++ b/test/regress/regress0/bug586.cvc.smt2 @@ -7,9 +7,9 @@ (declare-fun emptyRoleSet () (Set role)) -(assert (= emptyRoleSet (as emptyset (Set role)))) +(assert (= emptyRoleSet (as set.empty (Set role)))) (declare-fun d () (Array role |__cvc5_record_pos_(Set role)_neg_(Set role)|)) -(assert (= (pos (select d r3)) (singleton r1))) -(assert (= (pos (select d r2)) (union (singleton r2) (singleton r3)))) -(assert (= (neg (select d r2)) (singleton r1))) +(assert (= (pos (select d r3)) (set.singleton r1))) +(assert (= (pos (select d r2)) (set.union (set.singleton r2) (set.singleton r3)))) +(assert (= (neg (select d r2)) (set.singleton r1))) (check-sat) diff --git a/test/regress/regress0/bug605.cvc.smt2 b/test/regress/regress0/bug605.cvc.smt2 index eb8b92454..920a53158 100644 --- a/test/regress/regress0/bug605.cvc.smt2 +++ b/test/regress/regress0/bug605.cvc.smt2 @@ -13,10 +13,10 @@ (declare-fun a () (Array Int |__cvc5_record_s_f____cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__|)) (define-fun p1 () __cvc5_record_longitude_Int_latitude_Int (__cvc5_record_longitude_Int_latitude_Int_ctor 0 0)) -(define-fun s1 () |__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)| (|__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_ctor| (singleton (__cvc5_record_longitude_Int_latitude_Int_ctor 0 0)))) -(define-fun f0 () |__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_| (|__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__ctor| (|__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_ctor| (singleton (__cvc5_record_longitude_Int_latitude_Int_ctor 0 0))))) +(define-fun s1 () |__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)| (|__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_ctor| (set.singleton (__cvc5_record_longitude_Int_latitude_Int_ctor 0 0)))) +(define-fun f0 () |__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_| (|__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__ctor| (|__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_ctor| (set.singleton (__cvc5_record_longitude_Int_latitude_Int_ctor 0 0))))) (define-fun init ((v (Array Int |__cvc5_record_s_f____cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__|)) (i Int) (f |__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_|)) Bool (= (s_f (select v 0)) f)) -(assert (init a 2 (|__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__ctor| (|__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_ctor| (singleton (__cvc5_record_longitude_Int_latitude_Int_ctor 0 0)))))) +(assert (init a 2 (|__cvc5_record_base____cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)__ctor| (|__cvc5_record_geoLoc_(Set __cvc5_record_longitude_Int_latitude_Int)_ctor| (set.singleton (__cvc5_record_longitude_Int_latitude_Int_ctor 0 0)))))) (push 1) (assert true) diff --git a/test/regress/regress0/cores/issue4971-1.smt2 b/test/regress/regress0/cores/issue4971-1.smt2 index 2ac70735c..011b7432e 100644 --- a/test/regress/regress0/cores/issue4971-1.smt2 +++ b/test/regress/regress0/cores/issue4971-1.smt2 @@ -8,9 +8,9 @@ (declare-fun st4 () (Set Int)) (declare-fun st9 () (Set Int)) (declare-const v6 Bool) -(assert (! (forall ((q12 Int) (q13 Bool)) (xor false true true false true true v6 (<= 5 i5 93 417 i2) true (subset st2 st4) true)) :named IP_4)) +(assert (! (forall ((q12 Int) (q13 Bool)) (xor false true true false true true v6 (<= 5 i5 93 417 i2) true (set.subset st2 st4) true)) :named IP_4)) (declare-const i11 Int) -(assert (< (card st9) i11)) +(assert (< (set.card st9) i11)) (assert (! (not (<= 5 i5 93 417 i2)) :named IP_46)) (check-sat) (check-sat-assuming ((! (or v6 v6 v6) :named IP_12) (! (or false v6 v6) :named IP_56)))
\ No newline at end of file diff --git a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 index bbc25da68..c4e4b76f6 100644 --- a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 +++ b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 @@ -63,11 +63,11 @@ (declare-fun isTip!5 (ConQ!6) Bool) -(assert (=> start!13 (and (not (isTip!5 (evalLazyConQ2!7 lt!14))) (member lt!14 st!3)))) +(assert (=> start!13 (and (not (isTip!5 (evalLazyConQ2!7 lt!14))) (set.member lt!14 st!3)))) (assert (=> start!13 (= lt!14 e!42))) -(assert (=> start!13 (= b!40 (member l!2 st!3)))) +(assert (=> start!13 (= b!40 (set.member l!2 st!3)))) (assert (=> start!13 (or (not b!40) (not b!42)))) diff --git a/test/regress/regress0/datatypes/dt-2.6.smt2 b/test/regress/regress0/datatypes/dt-2.6.smt2 index 07dc0169e..07f01a1f5 100644 --- a/test/regress/regress0/datatypes/dt-2.6.smt2 +++ b/test/regress/regress0/datatypes/dt-2.6.smt2 @@ -3,7 +3,7 @@ (set-logic ALL) (set-info :status sat) (declare-datatypes ((IntList 0)) ( -((empty) (insert ( head Int ) ( tail IntList ) )) +((empty) (set.insert ( head Int ) ( tail IntList ) )) )) (declare-fun x () IntList) diff --git a/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 b/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 index 430b22c59..2dba04bb1 100644 --- a/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 +++ b/test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2 @@ -4,12 +4,12 @@ (set-info :status sat) (declare-datatypes ( ( Tree 0) ( TreeList 0) ) ( ( ( node ( value Int ) ( children TreeList) )) -( ( empty ) ( insert ( head Tree) ( tail TreeList)) ) +( ( empty ) ( set.insert ( head Tree) ( tail TreeList)) ) )) (declare-fun t () TreeList) -(assert (<= 100 (match t ((empty (- 1)) ((insert x1 x2) (value x1)))))) +(assert (<= 100 (match t ((empty (- 1)) ((set.insert x1 x2) (value x1)))))) (declare-datatypes ( ( PTree 1) ( PTreeList 1) ) ( diff --git a/test/regress/regress0/datatypes/dt-param-2.6.smt2 b/test/regress/regress0/datatypes/dt-param-2.6.smt2 index f6d1cd58d..010b55feb 100644 --- a/test/regress/regress0/datatypes/dt-param-2.6.smt2 +++ b/test/regress/regress0/datatypes/dt-param-2.6.smt2 @@ -2,7 +2,7 @@ (set-info :status sat) (declare-datatypes ( (Tree 1) (TreeList 1) ) ( (par ( X ) ( ( node ( value X ) ( children ( TreeList X )) ))) -(par ( Y ) ( ( empty ) ( insert ( head ( Tree Y )) ( tail ( TreeList Y ))) )) +(par ( Y ) ( ( empty ) ( set.insert ( head ( Tree Y )) ( tail ( TreeList Y ))) )) )) @@ -13,7 +13,7 @@ (assert (distinct x y z)) (assert (= (value x) 5)) -(assert ((_ is insert) (children y))) +(assert ((_ is set.insert) (children y))) (assert (= (value (head (children y))) 7)) (declare-sort U 0) @@ -23,7 +23,7 @@ (assert (distinct a b c)) -(assert ((_ is insert) (children a))) +(assert ((_ is set.insert) (children a))) (declare-fun d () (Tree (Tree Int))) diff --git a/test/regress/regress0/datatypes/dt-sel-2.6.smt2 b/test/regress/regress0/datatypes/dt-sel-2.6.smt2 index ae290a5ba..0fdc05471 100644 --- a/test/regress/regress0/datatypes/dt-sel-2.6.smt2 +++ b/test/regress/regress0/datatypes/dt-sel-2.6.smt2 @@ -3,7 +3,7 @@ (set-logic ALL) (set-info :status unsat) (declare-datatypes ((IntList 0)) ( -((empty) (insert ( head Int ) ( tail IntList ) )) +((empty) (set.insert ( head Int ) ( tail IntList ) )) )) (declare-fun x () IntList) @@ -12,7 +12,7 @@ (assert (distinct x y z)) -(assert (not ((_ is insert) x))) -(assert (not ((_ is insert) y))) +(assert (not ((_ is set.insert) x))) +(assert (not ((_ is set.insert) y))) (check-sat) diff --git a/test/regress/regress0/datatypes/issue5280-no-nrec.smt2 b/test/regress/regress0/datatypes/issue5280-no-nrec.smt2 index f80a6796a..283fcdc26 100644 --- a/test/regress/regress0/datatypes/issue5280-no-nrec.smt2 +++ b/test/regress/regress0/datatypes/issue5280-no-nrec.smt2 @@ -4,5 +4,5 @@ (declare-datatype ty0 ((Emp) (Container (v2 (Set ty0))))) (declare-fun v1 () ty0) (assert (not ((_ is Emp) v1))) -(assert (= (v2 v1) (singleton v1))) +(assert (= (v2 v1) (set.singleton v1))) (check-sat) diff --git a/test/regress/regress0/fmf/bounded_sets.smt2 b/test/regress/regress0/fmf/bounded_sets.smt2 index b06c3636f..363512fa1 100644 --- a/test/regress/regress0/fmf/bounded_sets.smt2 +++ b/test/regress/regress0/fmf/bounded_sets.smt2 @@ -6,13 +6,13 @@ (declare-fun S () (Set Int)) (declare-fun P (Int) Bool) (declare-fun a () Int) -(assert (member a S)) -(assert (forall ((y Int)) (=> (member y S) (P y)))) +(assert (set.member a S)) +(assert (forall ((y Int)) (=> (set.member y S) (P y)))) (declare-fun T () (Set Int)) (declare-fun b () Int) -(assert (member b T)) -(assert (forall ((y Int)) (=> (member y T) (not (P y))))) +(assert (set.member b T)) +(assert (forall ((y Int)) (=> (set.member y T) (not (P y))))) (check-sat) diff --git a/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2 b/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2 index 1e289d94f..e110c4e46 100644 --- a/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2 +++ b/test/regress/regress0/fmf/fmf-strange-bounds-2.smt2 @@ -10,12 +10,12 @@ (declare-fun f (U) U) (assert (forall ((x Int) (z U)) -(=> (member x (S (f z))) +(=> (set.member x (S (f z))) (P x z)))) ; need model of U size 2 to satisfy these (declare-fun a () U) -(assert (member 77 (S a))) +(assert (set.member 77 (S a))) (assert (not (P 77 a))) ; unsat diff --git a/test/regress/regress0/fmf/quant_real_univ.cvc.smt2 b/test/regress/regress0/fmf/quant_real_univ.cvc.smt2 index 68fee3f21..d1c93a45b 100644 --- a/test/regress/regress0/fmf/quant_real_univ.cvc.smt2 +++ b/test/regress/regress0/fmf/quant_real_univ.cvc.smt2 @@ -6,8 +6,8 @@ (declare-sort Atom 0) (declare-fun REAL_UNIVERSE () (Set (Tuple Real))) (declare-fun ATOM_UNIVERSE () (Set (Tuple Atom))) -(assert (= REAL_UNIVERSE (as univset (Set (Tuple Real))))) -(assert (= ATOM_UNIVERSE (as univset (Set (Tuple Atom))))) +(assert (= REAL_UNIVERSE (as set.universe (Set (Tuple Real))))) +(assert (= ATOM_UNIVERSE (as set.universe (Set (Tuple Atom))))) (declare-fun levelVal () (Set (Tuple Atom Real))) -(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))))) +(assert (forall ((s Atom) (v1 Real) (v2 Real)) (=> (and (and (set.member (tuple s) ATOM_UNIVERSE) (set.member (tuple v1) REAL_UNIVERSE)) (set.member (tuple v2) REAL_UNIVERSE)) (=> (and (set.member (tuple s v1) levelVal) (set.member (tuple s v2) levelVal)) (= v1 v2))))) (check-sat) diff --git a/test/regress/regress0/ho/fta0144-alpha-eq.smt2 b/test/regress/regress0/ho/fta0144-alpha-eq.smt2 index 747bfd48e..c3b0e7387 100644 --- a/test/regress/regress0/ho/fta0144-alpha-eq.smt2 +++ b/test/regress/regress0/ho/fta0144-alpha-eq.smt2 @@ -13,7 +13,7 @@ (declare-fun minus$ (Complex$ Complex$) Complex$) (declare-fun norm$a (Real) Real) (declare-fun zero$a () Nat$) -(declare-fun member$ (Real Real_set$) Bool) +(declare-fun set.member$ (Real Real_set$) Bool) (declare-fun minus$a (Nat$ Nat$) Nat$) (declare-fun thesis$ () Bool) (declare-fun collect$ ((-> Real Bool)) Real_set$) diff --git a/test/regress/regress0/parser/declarefun-emptyset-uf.smt2 b/test/regress/regress0/parser/declarefun-emptyset-uf.smt2 index a6e514407..8f004b8f3 100644 --- a/test/regress/regress0/parser/declarefun-emptyset-uf.smt2 +++ b/test/regress/regress0/parser/declarefun-emptyset-uf.smt2 @@ -2,6 +2,6 @@ (set-logic QF_UF) (declare-sort T 0) (declare-fun union () T) -(declare-fun emptyset () T) -(assert (= union emptyset)) +(declare-fun set.empty () T) +(assert (= union set.empty)) (check-sat) diff --git a/test/regress/regress0/rels/addr_book_0.cvc.smt2 b/test/regress/regress0/rels/addr_book_0.cvc.smt2 index 00fc33d56..70488b4eb 100644 --- a/test/regress/regress0/rels/addr_book_0.cvc.smt2 +++ b/test/regress/regress0/rels/addr_book_0.cvc.smt2 @@ -14,28 +14,28 @@ (declare-fun b1 () Atom) (declare-fun b1_tup () (Tuple Atom)) (assert (= b1_tup (tuple b1))) -(assert (member b1_tup Book)) +(assert (set.member b1_tup Book)) (declare-fun b2 () Atom) (declare-fun b2_tup () (Tuple Atom)) (assert (= b2_tup (tuple b2))) -(assert (member b2_tup Book)) +(assert (set.member b2_tup Book)) (declare-fun b3 () Atom) (declare-fun b3_tup () (Tuple Atom)) (assert (= b3_tup (tuple b3))) -(assert (member b3_tup Book)) +(assert (set.member b3_tup Book)) (declare-fun n () Atom) (declare-fun n_tup () (Tuple Atom)) (assert (= n_tup (tuple n))) -(assert (member n_tup Name)) +(assert (set.member n_tup Name)) (declare-fun t () Atom) (declare-fun t_tup () (Tuple Atom)) (assert (= t_tup (tuple t))) -(assert (member t_tup Target)) -(assert (subset (join (join Book addr) Target) Name)) -(assert (subset (join Book names) Name)) -(assert (= (intersection Name Addr) (as emptyset (Set (Tuple Atom))))) -(assert (= (join (singleton n_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom))))) -(assert (let ((_let_1 (singleton n_tup))) (= (join _let_1 (join (singleton b2_tup) addr)) (union (join _let_1 (join (singleton b1_tup) addr)) (singleton t_tup))))) -(assert (let ((_let_1 (singleton n_tup))) (= (join _let_1 (join (singleton b3_tup) addr)) (setminus (join _let_1 (join (singleton b2_tup) addr)) (singleton t_tup))))) -(assert (let ((_let_1 (singleton n_tup))) (not (= (join _let_1 (join (singleton b1_tup) addr)) (join _let_1 (join (singleton b3_tup) addr)))))) +(assert (set.member t_tup Target)) +(assert (set.subset (rel.join (rel.join Book addr) Target) Name)) +(assert (set.subset (rel.join Book names) Name)) +(assert (= (set.intersection Name Addr) (as set.empty (Set (Tuple Atom))))) +(assert (= (rel.join (set.singleton n_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Set (Tuple Atom))))) +(assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.union (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (set.singleton t_tup))))) +(assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b3_tup) addr)) (set.minus (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.singleton t_tup))))) +(assert (let ((_let_1 (set.singleton n_tup))) (not (= (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (rel.join _let_1 (rel.join (set.singleton b3_tup) addr)))))) (check-sat) diff --git a/test/regress/regress0/rels/atom_univ2.cvc.smt2 b/test/regress/regress0/rels/atom_univ2.cvc.smt2 index ad7d5ec4b..11799ba79 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 (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)))))) +(assert (set.member (tuple y) a)) +(assert (set.member (tuple x y) b)) +(assert (= (as set.universe (Set (Tuple Atom Atom))) (rel.product (as set.universe (Set (Tuple Atom))) (as set.universe (Set (Tuple Atom)))))) (declare-fun u () (Set (Tuple Atom Atom))) -(assert (= u (as univset (Set (Tuple Atom Atom))))) -(assert (not (member (tuple x y) u))) +(assert (= u (as set.universe (Set (Tuple Atom Atom))))) +(assert (not (set.member (tuple x y) u))) (check-sat) diff --git a/test/regress/regress0/rels/card_transpose.cvc.smt2 b/test/regress/regress0/rels/card_transpose.cvc.smt2 index 8356eca41..6db1e0e47 100644 --- a/test/regress/regress0/rels/card_transpose.cvc.smt2 +++ b/test/regress/regress0/rels/card_transpose.cvc.smt2 @@ -3,5 +3,5 @@ (set-logic ALL) (declare-fun x () (Set (Tuple Int Int))) -(assert (> (card (transpose x)) 0)) +(assert (> (set.card (rel.transpose x)) 0)) (check-sat) diff --git a/test/regress/regress0/rels/iden_0.cvc.smt2 b/test/regress/regress0/rels/iden_0.cvc.smt2 index d2d091e60..1cdeffbff 100644 --- a/test/regress/regress0/rels/iden_0.cvc.smt2 +++ b/test/regress/regress0/rels/iden_0.cvc.smt2 @@ -14,12 +14,12 @@ (assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) (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 (tuple 1 1) (intersection id x)))) +(assert (set.member (tuple 1) t)) +(assert (set.member (tuple 2) t)) +(assert (set.member z x)) +(assert (set.member zt x)) +(assert (set.member v x)) +(assert (set.member a x)) +(assert (= id (rel.iden t))) +(assert (not (set.member (tuple 1 1) (set.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 c2de24558..64efc4aef 100644 --- a/test/regress/regress0/rels/iden_1.cvc.smt2 +++ b/test/regress/regress0/rels/iden_1.cvc.smt2 @@ -11,9 +11,9 @@ (declare-fun b () Atom) (declare-fun c () Atom) (declare-fun d () Atom) -(assert (= univ (as univset (Set (Tuple Atom))))) -(assert (member (tuple a b) x)) -(assert (member (tuple c d) x)) +(assert (= univ (as set.universe (Set (Tuple Atom))))) +(assert (set.member (tuple a b) x)) +(assert (set.member (tuple c d) x)) (assert (not (= a b))) -(assert (= (iden (join x univ)) x)) +(assert (= (rel.iden (rel.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 37af1b418..9dd334b5e 100644 --- a/test/regress/regress0/rels/join-eq-u-sat.cvc.smt2 +++ b/test/regress/regress0/rels/join-eq-u-sat.cvc.smt2 @@ -9,10 +9,10 @@ (declare-fun w () (Set (Tuple Int unit))) (declare-fun z () (Set (Tuple unit Int))) -(assert (= (join x y) (join w z))) -(assert (member (tuple 0 1) (join x y))) -(assert (member (tuple 0 u) w)) +(assert (= (rel.join x y) (rel.join w z))) +(assert (set.member (tuple 0 1) (rel.join x y))) +(assert (set.member (tuple 0 u) w)) (declare-fun t () Int) (assert (and (> t 0) (< t 3))) -(assert (not (member (tuple u t) z))) +(assert (not (set.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 92514a3be..652504a1a 100644 --- a/test/regress/regress0/rels/join-eq-u.cvc.smt2 +++ b/test/regress/regress0/rels/join-eq-u.cvc.smt2 @@ -9,10 +9,10 @@ (declare-fun w () (Set (Tuple Int unit))) (declare-fun z () (Set (Tuple unit Int))) -(assert (= (join x y) (join w z))) -(assert (member (tuple 0 1) (join x y))) -(assert (member (tuple 0 u) w)) +(assert (= (rel.join x y) (rel.join w z))) +(assert (set.member (tuple 0 1) (rel.join x y))) +(assert (set.member (tuple 0 u) w)) (declare-fun t () Int) (assert (and (> t 0) (< t 2))) -(assert (not (member (tuple u t) z))) +(assert (not (set.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 76a13b645..85d9cac6f 100644 --- a/test/regress/regress0/rels/joinImg_0.cvc.smt2 +++ b/test/regress/regress0/rels/joinImg_0.cvc.smt2 @@ -15,12 +15,12 @@ (assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 1 5))) -(assert (member (tuple 1 7) x)) -(assert (member z x)) -(assert (member (tuple 7 5) y)) -(assert (= t (join_image x 2))) -(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))) +(assert (set.member (tuple 1 7) x)) +(assert (set.member z x)) +(assert (set.member (tuple 7 5) y)) +(assert (= t (rel.join_image x 2))) +(assert (set.member (tuple 3) (rel.join_image x 2))) +(assert (not (set.member (tuple 1) (rel.join_image x 2)))) +(assert (set.member (tuple 4) (rel.join_image x 2))) +(assert (set.member (tuple 1) (rel.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 c04aa7985..ee500f8ed 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 (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)))) +(assert (let ((_let_1 (set.singleton (tuple a)))) (= (rel.join _let_1 t) (J _let_1 t)))) +(assert (let ((_let_1 (set.singleton (tuple c)))) (not (= (rel.join _let_1 (rel.tclosure t)) _let_1)))) (check-sat) diff --git a/test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2 b/test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2 index 52ee0b1c0..0e9a61922 100644 --- a/test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2 +++ b/test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2 @@ -1,5 +1,5 @@ (set-logic ALL) (set-info :status sat) (declare-fun d () (Tuple Int Int)) -(assert (= (as emptyset (Set (Tuple Int Int))) (join (singleton (tuple 1 0)) (singleton d)))) +(assert (= (as set.empty (Set (Tuple Int Int))) (rel.join (set.singleton (tuple 1 0)) (set.singleton d)))) (check-sat) diff --git a/test/regress/regress0/rels/qgu-fuzz-relations-1.smt2 b/test/regress/regress0/rels/qgu-fuzz-relations-1.smt2 index b489ce65b..6804a4df8 100644 --- a/test/regress/regress0/rels/qgu-fuzz-relations-1.smt2 +++ b/test/regress/regress0/rels/qgu-fuzz-relations-1.smt2 @@ -4,5 +4,5 @@ (declare-fun b () (Set (Tuple Int Int))) (declare-fun c () Int) (declare-fun d () (Tuple Int Int)) -(assert (and (= b (singleton (tuple 1 0))) (= a (join b (transpose a))) (= a (join b (tclosure a))) (= a (join b (singleton d))))) +(assert (and (= b (set.singleton (tuple 1 0))) (= a (rel.join b (rel.transpose a))) (= a (rel.join b (rel.tclosure a))) (= a (rel.join b (set.singleton d))))) (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 4210a5486..5a320b1d0 100644 --- a/test/regress/regress0/rels/rel_1tup_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_1tup_0.cvc.smt2 @@ -8,12 +8,12 @@ (declare-fun z () (Set (Tuple Int))) (declare-fun b () (Tuple Int Int)) (assert (= b (tuple 2 1))) -(assert (member b x)) +(assert (set.member b x)) (declare-fun a () (Tuple Int)) (assert (= a (tuple 1))) -(assert (member a y)) +(assert (set.member a y)) (declare-fun c () (Tuple Int)) (assert (= c (tuple 2))) -(assert (= z (join x y))) -(assert (not (member c z))) +(assert (= z (rel.join x y))) +(assert (not (set.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 2f4aea539..a72a26b9b 100644 --- a/test/regress/regress0/rels/rel_complex_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_complex_0.cvc.smt2 @@ -10,14 +10,14 @@ (declare-fun g () Int) (declare-fun e () (Tuple Int Int)) (assert (= e (tuple 4 f))) -(assert (member e x)) +(assert (set.member e x)) (declare-fun d () (Tuple Int Int)) (assert (= d (tuple g 3))) -(assert (member d y)) -(assert (= z (union (singleton f) (singleton g)))) +(assert (set.member d y)) +(assert (= z (set.union (set.singleton f) (set.singleton g)))) (assert (= 0 (- f g))) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 4 3))) -(assert (= r (join x y))) -(assert (not (member a r))) +(assert (= r (rel.join x y))) +(assert (not (set.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 e8ccfb070..389260e17 100644 --- a/test/regress/regress0/rels/rel_complex_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_complex_1.cvc.smt2 @@ -11,17 +11,17 @@ (declare-fun r2 () (Set (Tuple Int Int))) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 3 1))) -(assert (member a x)) +(assert (set.member a x)) (declare-fun d () (Tuple Int Int)) (assert (= d (tuple 1 3))) -(assert (member d y)) +(assert (set.member d y)) (declare-fun e () (Tuple Int Int)) (assert (= e (tuple 4 3))) -(assert (= r (join x y))) -(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 (tuple 3 3) r2))) +(assert (= r (rel.join x y))) +(assert (set.member (tuple 1) w)) +(assert (set.member (tuple 2) z)) +(assert (= r2 (rel.product w z))) +(assert (not (set.member e r))) +(assert (set.subset r r2)) +(assert (not (set.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 e074778c5..4b7fede6c 100644 --- a/test/regress/regress0/rels/rel_conflict_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_conflict_0.cvc.smt2 @@ -5,6 +5,6 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun e () (Tuple Int Int)) (assert (= e (tuple 4 4))) -(assert (member e x)) -(assert (not (member (tuple 4 4) x))) +(assert (set.member e x)) +(assert (not (set.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 3c36d36e8..018b83e27 100644 --- a/test/regress/regress0/rels/rel_join_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_0.cvc.smt2 @@ -13,9 +13,9 @@ (assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) (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)))) +(assert (set.member (tuple 1 7) x)) +(assert (set.member (tuple 7 5) y)) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (not (set.member a (rel.join x y)))) (check-sat) 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 6af8429d3..4489b1a16 100644 --- a/test/regress/regress0/rels/rel_join_0_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_0_1.cvc.smt2 @@ -13,10 +13,10 @@ (assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) (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))) +(assert (set.member (tuple 1 7) x)) +(assert (set.member (tuple 4 3) x)) +(assert (set.member (tuple 7 5) y)) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (set.member a (rel.join x y))) (check-sat) diff --git a/test/regress/regress0/rels/rel_join_1.cvc.smt2 b/test/regress/regress0/rels/rel_join_1.cvc.smt2 index 88f8c73f3..638964931 100644 --- a/test/regress/regress0/rels/rel_join_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_1.cvc.smt2 @@ -13,13 +13,13 @@ (assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) (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)))) +(assert (set.member (tuple 1 7) x)) +(assert (set.member (tuple 2 3) x)) +(assert (set.member (tuple 3 4) x)) +(assert (set.member (tuple 7 5) y)) +(assert (set.member (tuple 7 3) y)) +(assert (set.member (tuple 4 7) y)) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (not (set.member a (rel.join x y)))) (check-sat) 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 e1556149c..357f37922 100644 --- a/test/regress/regress0/rels/rel_join_1_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_1_1.cvc.smt2 @@ -13,13 +13,13 @@ (assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) (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))) +(assert (set.member (tuple 1 7) x)) +(assert (set.member (tuple 2 3) x)) +(assert (set.member (tuple 3 4) x)) +(assert (set.member (tuple 7 5) y)) +(assert (set.member (tuple 7 3) y)) +(assert (set.member (tuple 4 7) y)) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (= r (rel.join x y))) (check-sat) diff --git a/test/regress/regress0/rels/rel_join_2.cvc.smt2 b/test/regress/regress0/rels/rel_join_2.cvc.smt2 index 5c8f0ea91..3359f2f62 100644 --- a/test/regress/regress0/rels/rel_join_2.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_2.cvc.smt2 @@ -11,7 +11,7 @@ (assert (= zt (tuple 2 1 3))) (declare-fun a () (Tuple Int Int Int)) (assert (= a (tuple 1 1 3))) -(assert (member z x)) -(assert (member zt y)) -(assert (not (member a (join x y)))) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (not (set.member a (rel.join x y)))) (check-sat) 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 82433cc1b..5c1f114a5 100644 --- a/test/regress/regress0/rels/rel_join_2_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_2_1.cvc.smt2 @@ -11,7 +11,7 @@ (assert (= zt (tuple 2 1 3))) (declare-fun a () (Tuple Int Int Int)) (assert (= a (tuple 1 1 3))) -(assert (member z x)) -(assert (member zt y)) -(assert (member a (join x y))) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (set.member a (rel.join x y))) (check-sat) diff --git a/test/regress/regress0/rels/rel_join_3.cvc.smt2 b/test/regress/regress0/rels/rel_join_3.cvc.smt2 index 4a3358526..6459b9f03 100644 --- a/test/regress/regress0/rels/rel_join_3.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_3.cvc.smt2 @@ -13,14 +13,14 @@ (assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) (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)) -(assert (not (member a r))) +(assert (set.member (tuple 1 7) x)) +(assert (set.member (tuple 2 3) x)) +(assert (set.member (tuple 3 4) x)) +(assert (set.member (tuple 7 5) y)) +(assert (set.member (tuple 7 3) y)) +(assert (set.member (tuple 4 7) y)) +(assert (= r (rel.join x y))) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (not (set.member a r))) (check-sat) 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 7b66ab443..1fb714112 100644 --- a/test/regress/regress0/rels/rel_join_3_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_3_1.cvc.smt2 @@ -13,14 +13,14 @@ (assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) (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)) -(assert (member a r)) +(assert (set.member (tuple 1 7) x)) +(assert (set.member (tuple 2 3) x)) +(assert (set.member (tuple 3 4) x)) +(assert (set.member (tuple 7 5) y)) +(assert (set.member (tuple 7 3) y)) +(assert (set.member (tuple 4 7) y)) +(assert (= r (rel.join x y))) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (set.member a r)) (check-sat) diff --git a/test/regress/regress0/rels/rel_join_4.cvc.smt2 b/test/regress/regress0/rels/rel_join_4.cvc.smt2 index bc4f16513..fc9fad09b 100644 --- a/test/regress/regress0/rels/rel_join_4.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_4.cvc.smt2 @@ -15,14 +15,14 @@ (assert (= a (tuple 1 5))) (declare-fun b () (Tuple Int Int)) (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 (tuple 7 3) y)) -(assert (member (tuple 4 7) y)) -(assert (= r (join x y))) -(assert (member z x)) -(assert (member zt y)) -(assert (not (member a r))) +(assert (set.member (tuple 1 7) x)) +(assert (set.member (tuple 2 3) x)) +(assert (set.member (tuple 3 4) x)) +(assert (set.member b y)) +(assert (set.member (tuple 7 3) y)) +(assert (set.member (tuple 4 7) y)) +(assert (= r (rel.join x y))) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (not (set.member a r))) (check-sat) diff --git a/test/regress/regress0/rels/rel_join_5.cvc.smt2 b/test/regress/regress0/rels/rel_join_5.cvc.smt2 index 227395fe6..cd256a476 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 (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 (set.member (tuple 7 1) x)) +(assert (set.member (tuple 2 3) x)) +(assert (set.member (tuple 7 3) y)) +(assert (set.member (tuple 4 7) y)) +(assert (set.member (tuple 3 4) z)) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 1 4))) -(assert (= r (join (join (transpose x) y) z))) -(assert (not (member a r))) +(assert (= r (rel.join (rel.join (rel.transpose x) y) z))) +(assert (not (set.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 547430c19..81ab335aa 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 (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))) +(assert (= x (set.union (set.singleton (tuple 1 2)) (set.singleton (tuple 3 4))))) +(assert (= y (rel.join x (set.union (set.singleton (tuple 2 1)) (set.singleton (tuple 4 3)))))) +(assert (not (set.member (tuple 1 1) y))) (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 3956af748..a8b1fd3c0 100644 --- a/test/regress/regress0/rels/rel_join_7.cvc.smt2 +++ b/test/regress/regress0/rels/rel_join_7.cvc.smt2 @@ -14,10 +14,10 @@ (assert (= v (tuple 1 1))) (declare-fun a () (Tuple Int Int)) (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)))) -(assert (not (member a w))) +(assert (set.member (tuple 1 7) x)) +(assert (set.member (tuple 7 5) y)) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (= w (set.union r (rel.join x y)))) +(assert (not (set.member a w))) (check-sat) diff --git a/test/regress/regress0/rels/rel_product_0.cvc.smt2 b/test/regress/regress0/rels/rel_product_0.cvc.smt2 index 890c6f5d6..cdf337276 100644 --- a/test/regress/regress0/rels/rel_product_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_product_0.cvc.smt2 @@ -12,7 +12,7 @@ (assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int Int Int)) (assert (= v (tuple 1 2 2 1))) -(assert (member z x)) -(assert (member zt y)) -(assert (not (member v (product x y)))) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (not (set.member v (rel.product x y)))) (check-sat) 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 1958036d2..a0469b3e9 100644 --- a/test/regress/regress0/rels/rel_product_0_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_product_0_1.cvc.smt2 @@ -12,7 +12,7 @@ (assert (= zt (tuple 2 1))) (declare-fun v () (Tuple Int Int Int Int)) (assert (= v (tuple 1 2 2 1))) -(assert (member z x)) -(assert (member zt y)) -(assert (member v (product x y))) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (set.member v (rel.product x y))) (check-sat) diff --git a/test/regress/regress0/rels/rel_product_1.cvc.smt2 b/test/regress/regress0/rels/rel_product_1.cvc.smt2 index 6711cfd6f..544068b50 100644 --- a/test/regress/regress0/rels/rel_product_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_product_1.cvc.smt2 @@ -12,7 +12,7 @@ (assert (= zt (tuple 3 2 1))) (declare-fun v () (Tuple Int Int Int Int Int Int)) (assert (= v (tuple 1 2 3 3 2 1))) -(assert (member z x)) -(assert (member zt y)) -(assert (not (member v (product x y)))) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (not (set.member v (rel.product x y)))) (check-sat) 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 5d8c2dbf2..a3fb21eed 100644 --- a/test/regress/regress0/rels/rel_product_1_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_product_1_1.cvc.smt2 @@ -10,8 +10,8 @@ (assert (= z (tuple 1 2 3))) (declare-fun zt () (Tuple Int Int Int)) (assert (= zt (tuple 3 2 1))) -(assert (member z x)) -(assert (member zt y)) -(assert (member (tuple 1 1 1 1 1 1) r)) -(assert (= r (product x y))) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (set.member (tuple 1 1 1 1 1 1) r)) +(assert (= r (rel.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 0c8188f1f..178208ff7 100644 --- a/test/regress/regress0/rels/rel_symbolic_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_symbolic_1.cvc.smt2 @@ -8,12 +8,12 @@ (declare-fun f () Int) (declare-fun d () (Tuple Int Int)) (assert (= d (tuple f 3))) -(assert (member d y)) +(assert (set.member d y)) (declare-fun e () (Tuple Int Int)) (assert (= e (tuple 4 f))) -(assert (member e x)) +(assert (set.member e x)) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 4 3))) -(assert (= r (join x y))) -(assert (not (member a r))) +(assert (= r (rel.join x y))) +(assert (not (set.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 2e10e76ad..7afe4e4a9 100644 --- a/test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2 @@ -6,11 +6,11 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun r () (Set (Tuple Int Int))) (declare-fun d () (Tuple Int Int)) -(assert (member d y)) +(assert (set.member d y)) (declare-fun a () (Tuple Int Int)) -(assert (member a x)) +(assert (set.member a x)) (declare-fun e () (Tuple Int Int)) (assert (= e (tuple 4 3))) -(assert (= r (join x y))) -(assert (not (member e r))) +(assert (= r (rel.join x y))) +(assert (not (set.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 2615112c2..665513498 100644 --- a/test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2 @@ -7,11 +7,11 @@ (declare-fun r () (Set (Tuple Int Int))) (declare-fun d () (Tuple Int Int)) (assert (= d (tuple 1 3))) -(assert (member (tuple 1 3) y)) +(assert (set.member (tuple 1 3) y)) (declare-fun a () (Tuple Int Int)) -(assert (member a x)) +(assert (set.member a x)) (declare-fun e () (Tuple Int Int)) (assert (= e (tuple 4 3))) -(assert (= r (join x y))) -(assert (not (member e r))) +(assert (= r (rel.join x y))) +(assert (not (set.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 c170fd7a0..183aff148 100644 --- a/test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2 @@ -7,12 +7,12 @@ (declare-fun r () (Set (Tuple Int Int))) (declare-fun f () Int) (declare-fun d () (Tuple Int Int)) -(assert (member d y)) +(assert (set.member d y)) (declare-fun e () (Tuple Int Int)) (assert (= e (tuple 4 f))) -(assert (member e x)) +(assert (set.member e x)) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 4 3))) -(assert (= r (join x y))) -(assert (not (member a r))) +(assert (= r (rel.join x y))) +(assert (not (set.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 5398cf388..8a2dc2749 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 (tuple 2 3) x)) -(assert (member (tuple 5 3) x)) -(assert (member (tuple 3 9) x)) -(assert (= z (product x 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 (tuple 1 2) y))) +(assert (set.member (tuple 2 3) x)) +(assert (set.member (tuple 5 3) x)) +(assert (set.member (tuple 3 9) x)) +(assert (= z (rel.product x y))) +(assert (set.member (tuple 1 2 3 4) z)) +(assert (not (set.member (tuple 5 9) x))) +(assert (set.member (tuple 3 8) y)) +(assert (= y (rel.tclosure x))) +(assert (not (set.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 07c60c562..7940e9898 100644 --- a/test/regress/regress0/rels/rel_tc_2_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tc_2_1.cvc.smt2 @@ -9,15 +9,15 @@ (assert (= a (tuple 1 e))) (declare-fun d () (Tuple Int Int)) (assert (= d (tuple e 5))) -(assert (member a x)) -(assert (member d 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 (tuple 1 5) y)) +(assert (set.member a x)) +(assert (set.member d x)) +(assert (not (set.member (tuple 1 1) x))) +(assert (not (set.member (tuple 1 2) x))) +(assert (not (set.member (tuple 1 3) x))) +(assert (not (set.member (tuple 1 4) x))) +(assert (not (set.member (tuple 1 5) x))) +(assert (not (set.member (tuple 1 6) x))) +(assert (not (set.member (tuple 1 7) x))) +(assert (= y (rel.tclosure x))) +(assert (set.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 9af4c2490..5de2d82d2 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 (tuple 1 a) x)) -(assert (member (tuple 1 c) x)) -(assert (member (tuple 1 d) x)) -(assert (member (tuple b 1) x)) +(assert (set.member (tuple 1 a) x)) +(assert (set.member (tuple 1 c) x)) +(assert (set.member (tuple 1 d) x)) +(assert (set.member (tuple b 1) x)) (assert (= b d)) (assert (> b (- d 1))) (assert (< b (+ d 1))) -(assert (= y (tclosure x))) -(assert (not (member (tuple 1 1) y))) +(assert (= y (rel.tclosure x))) +(assert (not (set.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 4041735f9..df9764a5c 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 (tuple 1 a) x)) -(assert (member (tuple 1 c) x)) -(assert (member (tuple 1 d) x)) -(assert (member (tuple b 1) x)) +(assert (set.member (tuple 1 a) x)) +(assert (set.member (tuple 1 c) x)) +(assert (set.member (tuple 1 d) x)) +(assert (set.member (tuple b 1) x)) (assert (= b d)) -(assert (= y (tclosure x))) +(assert (= y (rel.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 b7200a9ef..620f8d3d0 100644 --- a/test/regress/regress0/rels/rel_tc_7.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tc_7.cvc.smt2 @@ -4,7 +4,7 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int))) -(assert (= y (join (tclosure x) x))) -(assert (member (tuple 1 2) (join (join x x) x))) -(assert (not (subset y (tclosure x)))) +(assert (= y (rel.join (rel.tclosure x) x))) +(assert (set.member (tuple 1 2) (rel.join (rel.join x x) x))) +(assert (not (set.subset y (rel.tclosure x)))) (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 0485a06e9..5e359b538 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 (tuple 2 2) (tclosure x))) -(assert (= x (as emptyset (Set (Tuple Int Int))))) +(assert (set.member (tuple 2 2) (rel.tclosure x))) +(assert (= x (as set.empty (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 4e7a33e04..9f2dd1190 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 (tuple 1 3) x)) -(assert (or (member (tuple 2 3) z) (member (tuple 2 1) z))) -(assert (= y (transpose x))) -(assert (not (member (tuple 1 2) y))) +(assert (set.member (tuple 1 3) x)) +(assert (or (set.member (tuple 2 3) z) (set.member (tuple 2 1) z))) +(assert (= y (rel.transpose x))) +(assert (not (set.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 05761030c..aed2badf7 100644 --- a/test/regress/regress0/rels/rel_tp_join_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tp_join_0.cvc.smt2 @@ -15,14 +15,14 @@ (assert (= a (tuple 5 1))) (declare-fun b () (Tuple Int Int)) (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 (tuple 7 3) y)) -(assert (member (tuple 4 7) y)) -(assert (= r (join x y))) -(assert (member z x)) -(assert (member zt y)) -(assert (not (member a (transpose r)))) +(assert (set.member (tuple 1 7) x)) +(assert (set.member (tuple 2 3) x)) +(assert (set.member (tuple 3 4) x)) +(assert (set.member b y)) +(assert (set.member (tuple 7 3) y)) +(assert (set.member (tuple 4 7) y)) +(assert (= r (rel.join x y))) +(assert (set.member z x)) +(assert (set.member zt y)) +(assert (not (set.member a (rel.transpose r)))) (check-sat) 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 f1faefaeb..213d75bdc 100644 --- a/test/regress/regress0/rels/rel_tp_join_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_tp_join_1.cvc.smt2 @@ -10,17 +10,17 @@ (assert (= b (tuple 1 7))) (declare-fun c () (Tuple Int Int)) (assert (= c (tuple 2 3))) -(assert (member b x)) -(assert (member c x)) +(assert (set.member b x)) +(assert (set.member c x)) (declare-fun d () (Tuple Int Int)) (assert (= d (tuple 7 3))) (declare-fun e () (Tuple Int Int)) (assert (= e (tuple 4 7))) -(assert (member d y)) -(assert (member e y)) -(assert (member (tuple 3 4) z)) +(assert (set.member d y)) +(assert (set.member e y)) +(assert (set.member (tuple 3 4) z)) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 4 1))) -(assert (= r (join (join x y) z))) -(assert (not (member a (transpose r)))) +(assert (= r (rel.join (rel.join x y) z))) +(assert (not (set.member a (rel.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 0f3d124ae..b66f1c6ed 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 (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 (set.member (tuple 7 1) x)) +(assert (set.member (tuple 2 3) x)) +(assert (set.member (tuple 7 3) y)) +(assert (set.member (tuple 4 7) y)) +(assert (set.member (tuple 3 4) z)) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 4 1))) -(assert (= r (join (join (transpose x) y) z))) -(assert (not (member a (transpose r)))) +(assert (= r (rel.join (rel.join (rel.transpose x) y) z))) +(assert (not (set.member a (rel.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 1443c9ca3..4ebd54b90 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 (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)) +(assert (set.member (tuple 7 1) x)) +(assert (set.member (tuple 2 3) x)) +(assert (set.member (tuple 7 3) y)) +(assert (set.member (tuple 4 7) y)) +(assert (set.member (tuple 3 4) z)) +(assert (set.member (tuple 3 3) w)) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 4 1))) -(assert (not (member a (transpose r)))) +(assert (not (set.member a (rel.transpose r)))) (declare-fun zz () (Set (Tuple Int Int))) -(assert (= zz (join (transpose x) y))) -(assert (not (member (tuple 1 3) w))) -(assert (not (member (tuple 1 3) (union w zz)))) +(assert (= zz (rel.join (rel.transpose x) y))) +(assert (not (set.member (tuple 1 3) w))) +(assert (not (set.member (tuple 1 3) (set.union w zz)))) (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 1dcfc0eb6..e67f5d59b 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 (tuple 1 7)) (singleton (tuple 2 3))))) +(assert (= x (set.union (set.singleton (tuple 1 7)) (set.singleton (tuple 2 3))))) (declare-fun d () (Tuple Int Int)) (assert (= d (tuple 7 3))) (declare-fun e () (Tuple Int Int)) (assert (= e (tuple 4 7))) -(assert (member d y)) -(assert (member e y)) -(assert (member (tuple 3 4) z)) +(assert (set.member d y)) +(assert (set.member e y)) +(assert (set.member (tuple 3 4) z)) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 4 1))) -(assert (= r (join (join x y) z))) -(assert (not (member a (transpose r)))) +(assert (= r (rel.join (rel.join x y) z))) +(assert (not (set.member a (rel.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 82f6a0238..7806c48ba 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 (tuple 1 u) x)) -(assert (member (tuple t 3) y)) +(assert (set.member (tuple 1 u) x)) +(assert (set.member (tuple t 3) y)) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 1 3))) -(assert (not (member a (join x y)))) +(assert (not (set.member a (rel.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 d7d89d3a4..d9120c398 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 (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)) +(assert (set.member (tuple 2 1) x)) +(assert (set.member (tuple 2 3) x)) +(assert (set.member (tuple 2 2) y)) +(assert (set.member (tuple 4 7) y)) +(assert (set.member (tuple 3 4) z)) (declare-fun v () (Tuple Int Int Int Int)) (assert (= v (tuple 4 3 2 1))) -(assert (= r (product (join (transpose x) y) z))) -(assert (not (member v (transpose r)))) +(assert (= r (rel.product (rel.join (rel.transpose x) y) z))) +(assert (not (set.member v (rel.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 80b359e8b..c4cf0b43d 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,13 +11,13 @@ (declare-fun u () Int) (assert (and (< 4 t) (< t 6))) (assert (and (< 4 u) (< u 6))) -(assert (member (tuple 1 t) x)) -(assert (member (tuple u 3) y)) +(assert (set.member (tuple 1 t) x)) +(assert (set.member (tuple u 3) y)) (declare-fun a () (Tuple Int Int)) (assert (= a (tuple 1 3))) -(assert (not (member a (join x y)))) +(assert (not (set.member a (rel.join x y)))) (declare-fun st () (Set Int)) (declare-fun su () (Set Int)) -(assert (member t st)) -(assert (member u su)) +(assert (set.member t st)) +(assert (set.member u su)) (check-sat) diff --git a/test/regress/regress0/rels/rel_transpose_0.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_0.cvc.smt2 index 280f78ea2..3cce80a4b 100644 --- a/test/regress/regress0/rels/rel_transpose_0.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_0.cvc.smt2 @@ -9,7 +9,7 @@ (assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) (assert (= zt (tuple 2 1))) -(assert (member z x)) -(assert (not (member zt (transpose x)))) -(assert (= y (transpose x))) +(assert (set.member z x)) +(assert (not (set.member zt (rel.transpose x)))) +(assert (= y (rel.transpose x))) (check-sat) diff --git a/test/regress/regress0/rels/rel_transpose_1.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_1.cvc.smt2 index fb7070e82..728b2b23c 100644 --- a/test/regress/regress0/rels/rel_transpose_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_1.cvc.smt2 @@ -8,6 +8,6 @@ (assert (= z (tuple 1 2 3))) (declare-fun zt () (Tuple Int Int Int)) (assert (= zt (tuple 3 2 1))) -(assert (member z x)) -(assert (not (member zt (transpose x)))) +(assert (set.member z x)) +(assert (not (set.member zt (rel.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 0d9f6d028..4177d70e4 100644 --- a/test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2 @@ -9,7 +9,7 @@ (assert (= z (tuple 1 2 a))) (declare-fun zt () (Tuple Int Int Int)) (assert (= zt (tuple 3 2 2))) -(assert (member z x)) -(assert (member zt (transpose x))) -(assert (= y (transpose x))) +(assert (set.member z x)) +(assert (set.member zt (rel.transpose x))) +(assert (= y (rel.transpose x))) (check-sat) diff --git a/test/regress/regress0/rels/rel_transpose_3.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_3.cvc.smt2 index ea737919e..24f1ca24c 100644 --- a/test/regress/regress0/rels/rel_transpose_3.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_3.cvc.smt2 @@ -9,6 +9,6 @@ (declare-fun zt () (Tuple Int Int)) (assert (= zt (tuple 2 1))) (assert (= x y)) -(assert (member z x)) -(assert (not (member zt (transpose y)))) +(assert (set.member z x)) +(assert (not (set.member zt (rel.transpose y)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_transpose_4.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_4.cvc.smt2 index 5ba3cc2c6..4013806de 100644 --- a/test/regress/regress0/rels/rel_transpose_4.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_4.cvc.smt2 @@ -6,6 +6,6 @@ (declare-fun y () (Set (Tuple Int Int))) (declare-fun z () (Tuple Int Int)) (assert (= z (tuple 1 2))) -(assert (member z x)) -(assert (not (member (tuple 2 1) (transpose x)))) +(assert (set.member z x)) +(assert (not (set.member (tuple 2 1) (rel.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 8a58ca763..fbb1d265c 100644 --- a/test/regress/regress0/rels/rel_transpose_5.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_5.cvc.smt2 @@ -9,10 +9,10 @@ (assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) (assert (= zt (tuple 2 1))) -(assert (member zt y)) +(assert (set.member zt y)) (declare-fun w () (Tuple Int Int)) (assert (= w (tuple 2 2))) -(assert (member w y)) -(assert (member z x)) -(assert (not (member zt (transpose (join x y))))) +(assert (set.member w y)) +(assert (set.member z x)) +(assert (not (set.member zt (rel.transpose (rel.join x y))))) (check-sat) diff --git a/test/regress/regress0/rels/rel_transpose_6.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_6.cvc.smt2 index 1dc932a81..5924efd37 100644 --- a/test/regress/regress0/rels/rel_transpose_6.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_6.cvc.smt2 @@ -8,12 +8,12 @@ (assert (= z (tuple 1 2))) (declare-fun zt () (Tuple Int Int)) (assert (= zt (tuple 2 1))) -(assert (member z 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)) -(assert (not (member zt (transpose y)))) +(assert (set.member z x)) +(assert (set.member (tuple 3 4) x)) +(assert (set.member (tuple 3 5) x)) +(assert (set.member (tuple 3 3) x)) +(assert (= x (rel.transpose y))) +(assert (not (set.member zt y))) +(assert (set.member z y)) +(assert (not (set.member zt (rel.transpose y)))) (check-sat) diff --git a/test/regress/regress0/rels/rel_transpose_7.cvc.smt2 b/test/regress/regress0/rels/rel_transpose_7.cvc.smt2 index 7debeaa87..a4e0c8a76 100644 --- a/test/regress/regress0/rels/rel_transpose_7.cvc.smt2 +++ b/test/regress/regress0/rels/rel_transpose_7.cvc.smt2 @@ -5,5 +5,5 @@ (declare-fun x () (Set (Tuple Int Int))) (declare-fun y () (Set (Tuple Int Int))) (assert (= x y)) -(assert (not (= (transpose x) (transpose y)))) +(assert (not (= (rel.transpose x) (rel.transpose y)))) (check-sat) diff --git a/test/regress/regress0/rels/relations-ops.smt2 b/test/regress/regress0/rels/relations-ops.smt2 index e68eb49bb..3e6801102 100644 --- a/test/regress/regress0/rels/relations-ops.smt2 +++ b/test/regress/regress0/rels/relations-ops.smt2 @@ -11,13 +11,13 @@ (declare-fun lt2 () (Set (Tuple Int Int))) (declare-fun i () Int) -(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 (tuple 1 2) (tuple 2 3) (tuple 3 4) (singleton (tuple 4 5))))) -(assert (= lt2 (tclosure lt1))) -(assert (= i (card t))) +(assert (= r1 (set.insert (tuple "a" 1) (tuple "b" 2) (tuple "c" 3) (set.singleton (tuple "d" 4))))) +(assert (= r2 (set.insert (tuple 1 "1") (tuple 2 "2") (tuple 3 "3") (set.singleton (tuple 17 "17"))))) +(assert (= r (rel.join r1 r2))) +(assert (= s (rel.transpose r))) +(assert (= t (rel.product r1 r2))) +(assert (= lt1 (set.insert (tuple 1 2) (tuple 2 3) (tuple 3 4) (set.singleton (tuple 4 5))))) +(assert (= lt2 (rel.tclosure lt1))) +(assert (= i (set.card t))) (check-sat) diff --git a/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2 b/test/regress/regress0/rels/rels-sharing-simp.cvc.smt2 index 2ba92270a..186374897 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 (tuple 1 x) w)) -(assert (member (tuple y 2) z)) -(assert (not (member (tuple 1 2) (join w z)))) +(assert (set.member (tuple 1 x) w)) +(assert (set.member (tuple y 2) z)) +(assert (not (set.member (tuple 1 2) (rel.join w z)))) (check-sat) diff --git a/test/regress/regress0/sets/abt-min.smt2 b/test/regress/regress0/sets/abt-min.smt2 index 3bf1a9b6a..ceb97a781 100644 --- a/test/regress/regress0/sets/abt-min.smt2 +++ b/test/regress/regress0/sets/abt-min.smt2 @@ -12,11 +12,11 @@ (declare-fun b2 () Atom) (assert (forall ((b Atom)) (or -(member v (k t0 b)) -(member v (k t1 b)) +(set.member v (k t0 b)) +(set.member v (k t1 b)) ) )) -(assert (not (member v (k t2 b2)))) +(assert (not (set.member v (k t2 b2)))) (check-sat) diff --git a/test/regress/regress0/sets/abt-te-exh.smt2 b/test/regress/regress0/sets/abt-te-exh.smt2 index f87429fc2..c4c92aa50 100644 --- a/test/regress/regress0/sets/abt-te-exh.smt2 +++ b/test/regress/regress0/sets/abt-te-exh.smt2 @@ -7,7 +7,7 @@ (declare-fun kk (Atom (Set Atom)) (Set Atom)) (declare-fun n () (Set Atom)) -(assert (forall ((b Atom)) (= (as emptyset (Set Atom)) (kk (j (singleton b)) n)))) +(assert (forall ((b Atom)) (= (as set.empty (Set Atom)) (kk (j (set.singleton b)) n)))) (check-sat) diff --git a/test/regress/regress0/sets/abt-te-exh2.smt2 b/test/regress/regress0/sets/abt-te-exh2.smt2 index 9ff80e14c..ebd22b83f 100644 --- a/test/regress/regress0/sets/abt-te-exh2.smt2 +++ b/test/regress/regress0/sets/abt-te-exh2.smt2 @@ -14,8 +14,8 @@ (assert (forall ((b Atom) (c Atom)) (or -(member v (k (singleton n) (j (singleton b) a))) -(= (as emptyset (Set Atom)) (d (j (singleton b) a) (singleton n))) +(set.member v (k (set.singleton n) (j (set.singleton b) a))) +(= (as set.empty (Set Atom)) (d (j (set.singleton b) a) (set.singleton n))) ) ) ) diff --git a/test/regress/regress0/sets/card-2.smt2 b/test/regress/regress0/sets/card-2.smt2 index bc460fb4a..1bdfbb5ce 100644 --- a/test/regress/regress0/sets/card-2.smt2 +++ b/test/regress/regress0/sets/card-2.smt2 @@ -4,8 +4,8 @@ (declare-fun s () (Set E)) (declare-fun t () (Set E)) (declare-fun u () (Set E)) -(assert (>= (card s) 5)) -(assert (>= (card t) 5)) -(assert (<= (card u) 6)) -(assert (= u (union s t))) +(assert (>= (set.card s) 5)) +(assert (>= (set.card t) 5)) +(assert (<= (set.card u) 6)) +(assert (= u (set.union s t))) (check-sat) diff --git a/test/regress/regress0/sets/card-3sets.cvc.smt2 b/test/regress/regress0/sets/card-3sets.cvc.smt2 index 6c4bdd8ca..9f1a6552a 100644 --- a/test/regress/regress0/sets/card-3sets.cvc.smt2 +++ b/test/regress/regress0/sets/card-3sets.cvc.smt2 @@ -4,5 +4,5 @@ (declare-fun x () (Set Int)) (declare-fun y () (Set Int)) (declare-fun z () (Set Int)) -(assert (let ((_let_1 (card y))) (and (> (card x) _let_1) (> _let_1 (card z))))) +(assert (let ((_let_1 (set.card y))) (and (> (set.card x) _let_1) (> _let_1 (set.card z))))) (check-sat) diff --git a/test/regress/regress0/sets/card.smt2 b/test/regress/regress0/sets/card.smt2 index d42bf6f55..4c0fdbb56 100644 --- a/test/regress/regress0/sets/card.smt2 +++ b/test/regress/regress0/sets/card.smt2 @@ -3,7 +3,7 @@ (declare-sort E 0) (declare-fun s () (Set E)) (declare-fun t () (Set E)) -(assert (>= (card s) 5)) -(assert (>= (card t) 5)) -(assert (<= (card (union s t)) 4)) +(assert (>= (set.card s) 5)) +(assert (>= (set.card t) 5)) +(assert (<= (set.card (set.union s t)) 4)) (check-sat) diff --git a/test/regress/regress0/sets/card3-ground.smt2 b/test/regress/regress0/sets/card3-ground.smt2 index 7b42b8a8a..b6c66c0dd 100644 --- a/test/regress/regress0/sets/card3-ground.smt2 +++ b/test/regress/regress0/sets/card3-ground.smt2 @@ -1,6 +1,6 @@ (set-logic ALL) (set-info :status sat) (declare-fun S () (Set Int)) -(assert (>= (card S) 3)) -(assert (not (member 1 S))) +(assert (>= (set.card S) 3)) +(assert (not (set.member 1 S))) (check-sat) diff --git a/test/regress/regress0/sets/comp-qf-error.smt2 b/test/regress/regress0/sets/comp-qf-error.smt2 index 81e4d7411..ae9052dd4 100644 --- a/test/regress/regress0/sets/comp-qf-error.smt2 +++ b/test/regress/regress0/sets/comp-qf-error.smt2 @@ -9,6 +9,6 @@ (declare-fun x () (Set U)) -(assert (subset x (comprehension ((z U)) (not (= z a)) z))) +(assert (set.subset x (set.comprehension ((z U)) (not (= z a)) z))) (check-sat) diff --git a/test/regress/regress0/sets/complement.cvc.smt2 b/test/regress/regress0/sets/complement.cvc.smt2 index e86dcf107..e0a5c19f0 100644 --- a/test/regress/regress0/sets/complement.cvc.smt2 +++ b/test/regress/regress0/sets/complement.cvc.smt2 @@ -5,5 +5,5 @@ (declare-sort Atom 0) (declare-fun a () (Set (Tuple Atom))) (declare-fun b () (Set (Tuple Atom))) -(assert (= a (complement b))) +(assert (= a (set.complement b))) (check-sat) diff --git a/test/regress/regress0/sets/complement2.cvc.smt2 b/test/regress/regress0/sets/complement2.cvc.smt2 index 582156067..ecf8080db 100644 --- a/test/regress/regress0/sets/complement2.cvc.smt2 +++ b/test/regress/regress0/sets/complement2.cvc.smt2 @@ -6,6 +6,6 @@ (declare-fun a () (Set Atom)) (declare-fun b () (Set Atom)) (declare-fun c () Atom) -(assert (= a (complement a))) -(assert (member c a)) +(assert (= a (set.complement a))) +(assert (set.member c a)) (check-sat) diff --git a/test/regress/regress0/sets/complement3.cvc.smt2 b/test/regress/regress0/sets/complement3.cvc.smt2 index b81843871..20cfb36f8 100644 --- a/test/regress/regress0/sets/complement3.cvc.smt2 +++ b/test/regress/regress0/sets/complement3.cvc.smt2 @@ -8,9 +8,9 @@ (declare-fun C4 () (Set (Tuple Atom))) (declare-fun ATOM_UNIV () (Set (Tuple Atom))) (declare-fun V1 () Atom) -(assert (= C32 (intersection (complement C2) (complement C4)))) -(assert (member (tuple V1) (complement C32))) -(assert (= ATOM_UNIV (as univset (Set (Tuple Atom))))) -(assert (member (tuple V1) ATOM_UNIV)) -(assert (member (tuple V1) (complement C2))) +(assert (= C32 (set.intersection (set.complement C2) (set.complement C4)))) +(assert (set.member (tuple V1) (set.complement C32))) +(assert (= ATOM_UNIV (as set.universe (Set (Tuple Atom))))) +(assert (set.member (tuple V1) ATOM_UNIV)) +(assert (set.member (tuple V1) (set.complement C2))) (check-sat) diff --git a/test/regress/regress0/sets/cvc-sample.cvc.smt2 b/test/regress/regress0/sets/cvc-sample.cvc.smt2 index e0ea07a78..9ee199b43 100644 --- a/test/regress/regress0/sets/cvc-sample.cvc.smt2 +++ b/test/regress/regress0/sets/cvc-sample.cvc.smt2 @@ -18,14 +18,14 @@ (declare-fun b () (Set Int)) (declare-fun c () (Set Int)) (declare-fun e () Int) -(assert (= a (singleton 5))) -(assert (= c (union a b))) -(assert (not (= c (intersection a b)))) -(assert (= c (setminus a b))) -(assert (subset a b)) -(assert (member e c)) -(assert (member e a)) -(assert (member e (intersection a b))) +(assert (= a (set.singleton 5))) +(assert (= c (set.union a b))) +(assert (not (= c (set.intersection a b)))) +(assert (= c (set.minus a b))) +(assert (set.subset a b)) +(assert (set.member e c)) +(assert (set.member e a)) +(assert (set.member e (set.intersection a b))) (push 1) (assert true) @@ -37,7 +37,7 @@ (pop 1) (push 1) (assert (= x y)) -(assert (not (= (union x z) (union y z)))) +(assert (not (= (set.union x z) (set.union y z)))) (push 1) (assert true) @@ -50,8 +50,8 @@ (push 1) (assert (= x y)) (assert (= e1 e2)) -(assert (member e1 x)) -(assert (not (member e2 y))) +(assert (set.member e1 x)) +(assert (not (set.member e2 y))) (push 1) (assert true) @@ -64,8 +64,8 @@ (push 1) (assert (= x y)) (assert (= e1 e2)) -(assert (member e1 (union x z))) -(assert (not (member e2 (union y z)))) +(assert (set.member e1 (set.union x z))) +(assert (not (set.member e2 (set.union y z)))) (push 1) (assert true) @@ -76,8 +76,8 @@ (pop 1) (push 1) -(assert (member 5 (union (union (union (union (singleton 1) (singleton 2)) (singleton 3)) (singleton 4)) (singleton 5)))) -(assert (member 5 (union (union (union (union (singleton 1) (singleton 2)) (singleton 3)) (singleton 4)) (as emptyset (Set Int))))) +(assert (set.member 5 (set.union (set.union (set.union (set.union (set.singleton 1) (set.singleton 2)) (set.singleton 3)) (set.singleton 4)) (set.singleton 5)))) +(assert (set.member 5 (set.union (set.union (set.union (set.union (set.singleton 1) (set.singleton 2)) (set.singleton 3)) (set.singleton 4)) (as set.empty (Set Int))))) (push 1) (assert true) @@ -87,4 +87,4 @@ (pop 1) (pop 1) -(check-sat-assuming ( (not (let ((_let_1 (member e1 z))) (and _let_1 (not _let_1)))) )) +(check-sat-assuming ( (not (let ((_let_1 (set.member e1 z))) (and _let_1 (not _let_1)))) )) diff --git a/test/regress/regress0/sets/dt-simp-mem.smt2 b/test/regress/regress0/sets/dt-simp-mem.smt2 index 47bc7aa58..c7b2a3ee4 100644 --- a/test/regress/regress0/sets/dt-simp-mem.smt2 +++ b/test/regress/regress0/sets/dt-simp-mem.smt2 @@ -4,6 +4,6 @@ (declare-fun x1 () D) (declare-fun S () (Set D)) (declare-fun P (D) Bool) -(assert (member x1 S)) -(assert (=> (member (A 0) S) (P x1))) +(assert (set.member x1 S)) +(assert (=> (set.member (A 0) S) (P x1))) (check-sat) diff --git a/test/regress/regress0/sets/emptyset.smt2 b/test/regress/regress0/sets/emptyset.smt2 index 7296fcc28..0b5b561cd 100644 --- a/test/regress/regress0/sets/emptyset.smt2 +++ b/test/regress/regress0/sets/emptyset.smt2 @@ -1,4 +1,4 @@ (set-logic ALL) (set-info :status unsat) -(assert (member 5 (as emptyset (Set Int) ))) +(assert (set.member 5 (as set.empty (Set Int) ))) (check-sat) diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2 index 06f86ae3c..0ecd32bf8 100644 --- a/test/regress/regress0/sets/eqtest.smt2 +++ b/test/regress/regress0/sets/eqtest.smt2 @@ -10,9 +10,9 @@ (declare-fun H () (Set Int) ) (declare-fun I () (Set Int) ) (declare-fun x () Int) -(assert (member x (intersection (union A B) C))) -(assert (not (member x G))) -(assert (= (union A B) D)) -(assert (= C (intersection E F))) +(assert (set.member x (set.intersection (set.union A B) C))) +(assert (not (set.member x G))) +(assert (= (set.union A B) D)) +(assert (= C (set.intersection E F))) (assert (and (= F H) (= G H) (= H I))) (check-sat) diff --git a/test/regress/regress0/sets/error1.smt2 b/test/regress/regress0/sets/error1.smt2 index bf1822305..193d6d1cf 100644 --- a/test/regress/regress0/sets/error1.smt2 +++ b/test/regress/regress0/sets/error1.smt2 @@ -7,7 +7,7 @@ (declare-fun E () (Set Int)) (set-info :status sat) -(assert (= A (union D C))) -(assert (not (= A (union E A)))) +(assert (= A (set.union D C))) +(assert (not (= A (set.union E A)))) (check-sat) diff --git a/test/regress/regress0/sets/error2.smt2 b/test/regress/regress0/sets/error2.smt2 index 7b8f78218..d41e2b3b8 100644 --- a/test/regress/regress0/sets/error2.smt2 +++ b/test/regress/regress0/sets/error2.smt2 @@ -1,4 +1,4 @@ (set-logic QF_ALL) (set-info :status unsat) -(assert (= (as emptyset (Set Int)) (singleton 5))) +(assert (= (as set.empty (Set Int)) (set.singleton 5))) (check-sat) diff --git a/test/regress/regress0/sets/insert.smt2 b/test/regress/regress0/sets/insert.smt2 index b4936a32b..0e5f815f6 100644 --- a/test/regress/regress0/sets/insert.smt2 +++ b/test/regress/regress0/sets/insert.smt2 @@ -2,6 +2,6 @@ (set-logic QF_UFLIAFS) (set-info :status sat) (declare-fun X () (Set Int)) -(assert (= X (insert 1 2 (singleton 3)))) +(assert (= X (set.insert 1 2 (set.singleton 3)))) (check-sat) ;(get-model) diff --git a/test/regress/regress0/sets/int-real-univ-unsat.smt2 b/test/regress/regress0/sets/int-real-univ-unsat.smt2 index 19b5850fa..3267dcccf 100644 --- a/test/regress/regress0/sets/int-real-univ-unsat.smt2 +++ b/test/regress/regress0/sets/int-real-univ-unsat.smt2 @@ -7,9 +7,9 @@ (declare-fun x () Real) -(assert (= (as univset (Set Real)) (as univset (Set Real)))) +(assert (= (as set.universe (Set Real)) (as set.universe (Set Real)))) -(assert (member x a)) +(assert (set.member x a)) (assert (and (<= 5.5 x) (< x 5.8))) diff --git a/test/regress/regress0/sets/int-real-univ.smt2 b/test/regress/regress0/sets/int-real-univ.smt2 index e7d79bbf6..78bf88be9 100644 --- a/test/regress/regress0/sets/int-real-univ.smt2 +++ b/test/regress/regress0/sets/int-real-univ.smt2 @@ -7,9 +7,9 @@ (declare-fun x () Real) -(assert (= (as univset (Set Real)) (as univset (Set Real)))) +(assert (= (as set.universe (Set Real)) (as set.universe (Set Real)))) -(assert (member x a)) +(assert (set.member x a)) (assert (and (<= 5.5 x) (< x 6.1))) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 index 448022a2e..7e2f627ae 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 @@ -2,15 +2,15 @@ (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) -(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x))) -(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) +(define-fun smt_set_emp () mySet (as set.empty mySet)) +(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) +(define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) +(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) -(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) +(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) (declare-fun z3v58 () Int) (declare-fun z3v59 () Int) (assert (distinct z3v58 z3v59)) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 index a7c2bec8d..8fbed5572 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 @@ -7,12 +7,12 @@ (declare-fun S () (Set Int)) (declare-fun T () (Set Int)) -(assert (member x S)) +(assert (set.member x S)) -(assert (= S (union T (singleton y)))) +(assert (= S (set.union T (set.singleton y)))) (assert (not (= x y))) -(assert (not (member x T))) +(assert (not (set.member x T))) (check-sat) diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 index ff83b0fb5..b93a379ac 100644 --- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 @@ -2,13 +2,13 @@ (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) +(define-fun smt_set_emp () mySet (as set.empty mySet)) (declare-fun S () (Set Int)) (declare-fun T () (Set Int)) (assert (not (= S T))) -(assert (= T (union smt_set_emp S))) +(assert (= T (set.union smt_set_emp S))) (check-sat) ; What was the bug? diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 index 90d3a6372..f6fd4bd53 100644 --- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 @@ -2,15 +2,15 @@ (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) -(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x))) -(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) +(define-fun smt_set_emp () mySet (as set.empty mySet)) +(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) +(define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) +(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) -(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) +(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) (declare-fun z3v54 () Int) (declare-fun z3f55 (Int) Int) (declare-fun z3v56 () Int) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 index b20fb4f3d..882c67091 100644 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 @@ -22,12 +22,12 @@ (declare-fun T () mySet) (assert (= (f x) - (union S T))) + (set.union S T))) (assert (= (f x) - (union T (f y)))) + (set.union T (f y)))) (assert (not (= (f y) - (union T (f y))))) + (set.union T (f y))))) (check-sat) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 index 1c28759b6..99a67f7e7 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 @@ -7,13 +7,13 @@ ; ; What was going on? ; -; The solver was unable to reason that (emptyset) cannot equal -; (singleton 0). There were no membership predicates anywhere, just +; The solver was unable to reason that (set.empty) cannot equal +; (set.singleton 0). There were no membership predicates anywhere, just ; equalities. ; ; Fix ; -; Add the propagation rule: (true) => (member x (singleton x)) +; Add the propagation rule: (true) => (set.member x (set.singleton x)) (declare-fun z3f70 (Int) (Set Int)) (declare-fun z3v85 () Int) @@ -21,7 +21,7 @@ (declare-fun z3v87 () Int) (declare-fun z3v90 () Int) -(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (singleton z3v86))))) +(assert (= (z3f70 z3v90) (set.union (z3f70 z3v85) (set.union (as set.empty (Set Int)) (set.singleton z3v86))))) (assert (= (z3f70 z3v90) (z3f70 z3v87))) -(assert (= (as emptyset (Set Int)) (z3f70 z3v87))) +(assert (= (as set.empty (Set Int)) (z3f70 z3v87))) (check-sat) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 index 8b879b3ec..50f51a13f 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 @@ -3,16 +3,16 @@ (define-sort Elt () Int) (define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) +(define-fun smt_set_emp () mySet (as set.empty mySet)) (declare-fun S () (Set Int)) (declare-fun T () (Set Int)) (declare-fun x () Int) -(assert (or (not (= S smt_set_emp)) (member x T))) +(assert (or (not (= S smt_set_emp)) (set.member x T))) (assert (= smt_set_emp - (ite (member x T) - (union (union smt_set_emp (singleton x)) S) + (ite (set.member x T) + (set.union (set.union smt_set_emp (set.singleton x)) S) S))) (check-sat) diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 index e3e88c65f..6655713cf 100644 --- a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 +++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 @@ -4,8 +4,8 @@ (declare-fun b () Int) (declare-fun x () (Set Int)) (declare-fun y () (Set Int)) -(assert (= x (singleton a))) -(assert (= y (singleton b))) +(assert (= x (set.singleton a))) +(assert (= y (set.singleton b))) (assert (not (= x y))) (assert (and (< 1 a) (< a 3) (< 1 b) (< b 3))) (check-sat) diff --git a/test/regress/regress0/sets/mar2014/small.smt2 b/test/regress/regress0/sets/mar2014/small.smt2 index 635c7959d..f984aca53 100644 --- a/test/regress/regress0/sets/mar2014/small.smt2 +++ b/test/regress/regress0/sets/mar2014/small.smt2 @@ -10,9 +10,9 @@ (declare-fun z () Int) (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) -(assert (member x (union a b))) -(assert (not (member y a))) -(assert (not (member z b))) +(assert (set.member x (set.union a b))) +(assert (not (set.member y a))) +(assert (not (set.member z b))) (assert (= z y)) (assert (= x y)) (check-sat) diff --git a/test/regress/regress0/sets/mar2014/smaller.smt2 b/test/regress/regress0/sets/mar2014/smaller.smt2 index d6565205b..5a02cbe53 100644 --- a/test/regress/regress0/sets/mar2014/smaller.smt2 +++ b/test/regress/regress0/sets/mar2014/smaller.smt2 @@ -9,7 +9,7 @@ (declare-fun y () Int) (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) -(assert (member x (union a b))) -(assert (not (member y a))) +(assert (set.member x (set.union a b))) +(assert (not (set.member y a))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress0/sets/nonvar-univ.smt2 b/test/regress/regress0/sets/nonvar-univ.smt2 index 5c3bc567c..695e87ec3 100644 --- a/test/regress/regress0/sets/nonvar-univ.smt2 +++ b/test/regress/regress0/sets/nonvar-univ.smt2 @@ -6,8 +6,8 @@ (declare-fun P ((Set Int)) Bool) (assert (P x)) -(assert (not (P (singleton 0)))) -(assert (member 1 x)) -(assert (not (member 0 (as univset (Set Int))))) +(assert (not (P (set.singleton 0)))) +(assert (set.member 1 x)) +(assert (not (set.member 0 (as set.universe (Set Int))))) (check-sat) diff --git a/test/regress/regress0/sets/pre-proc-univ.smt2 b/test/regress/regress0/sets/pre-proc-univ.smt2 index f184ebf92..f01ad747b 100644 --- a/test/regress/regress0/sets/pre-proc-univ.smt2 +++ b/test/regress/regress0/sets/pre-proc-univ.smt2 @@ -4,8 +4,8 @@ (set-info :status unsat) (declare-fun x () (Set Int)) -(assert (= x (union (singleton 0) (singleton 1)))) +(assert (= x (set.union (set.singleton 0) (set.singleton 1)))) -(assert (not (member 0 (as univset (Set Int))))) +(assert (not (set.member 0 (as set.universe (Set Int))))) (check-sat) diff --git a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 index 61fbee11d..f70d59b16 100644 --- a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 +++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 @@ -45,15 +45,15 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 curr$0 l1 null$0) - (member l1 (lseg_domain$0 next$0 curr$0 null$0)) + (set.member l1 (lseg_domain$0 next$0 curr$0 null$0)) (not (= l1 null$0))) (and (or (= l1 null$0) (not (Btwn$0 next$0 curr$0 l1 null$0))) - (not (member l1 (lseg_domain$0 next$0 curr$0 null$0)))))) + (not (set.member l1 (lseg_domain$0 next$0 curr$0 null$0)))))) :named lseg_footprint_14)) -(assert (! (not (member tmp_1$0 Alloc$0)) :named new_42_10)) +(assert (! (not (set.member tmp_1$0 Alloc$0)) :named new_42_10)) -(assert (! (not (member null$0 Alloc$0)) +(assert (! (not (set.member null$0 Alloc$0)) :named initial_footprint_of_rec_copy_loop_34_11_4)) (assert (! (not (= curr$0 null$0)) :named if_else_37_6)) @@ -66,14 +66,14 @@ (assert (! (= sk_?X_36$0 FP$0) :named precondition_of_rec_copy_loop_34_11_18)) -(assert (! (= (as emptyset SetLoc) (intersection sk_?X_38$0 sk_?X_37$0)) +(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_38$0 sk_?X_37$0)) :named precondition_of_rec_copy_loop_34_11_19)) (assert (! (= old_cp_2$0 cp$0) :named assign_41_4)) -(assert (! (= FP_Caller_2$0 (setminus FP_Caller$0 FP$0)) :named assign_37_2_2)) +(assert (! (= FP_Caller_2$0 (set.minus FP_Caller$0 FP$0)) :named assign_37_2_2)) -(assert (! (= Alloc_2$0 (union Alloc$0 (singleton tmp_1$0))) :named assign_42_10)) +(assert (! (= Alloc_2$0 (set.union Alloc$0 (set.singleton tmp_1$0))) :named assign_42_10)) (assert (! (or (Btwn$0 next$0 cp$0 null$0 null$0) (not (lseg_struct$0 sk_?X_38$0 next$0 cp$0 null$0))) @@ -82,34 +82,34 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 cp$0 l1 null$0) - (member l1 (lseg_domain$0 next$0 cp$0 null$0)) + (set.member l1 (lseg_domain$0 next$0 cp$0 null$0)) (not (= l1 null$0))) (and (or (= l1 null$0) (not (Btwn$0 next$0 cp$0 l1 null$0))) - (not (member l1 (lseg_domain$0 next$0 cp$0 null$0)))))) + (not (set.member l1 (lseg_domain$0 next$0 cp$0 null$0)))))) :named lseg_footprint_15)) -(assert (! (not (member cp_1$0 FP_3$0)) :named check_heap_access_43_4)) +(assert (! (not (set.member cp_1$0 FP_3$0)) :named check_heap_access_43_4)) (assert (! (not (= tmp_1$0 null$0)) :named new_42_10_1)) (assert (! (lseg_struct$0 sk_?X_38$0 next$0 cp$0 null$0) :named precondition_of_rec_copy_loop_34_11_20)) -(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) +(assert (! (= FP_Caller$0 (set.union FP$0 FP_Caller$0)) :named precondition_of_rec_copy_loop_34_11_21)) (assert (! (= sk_?X_37$0 (lseg_domain$0 next$0 curr$0 null$0)) :named precondition_of_rec_copy_loop_34_11_22)) -(assert (! (= sk_?X_36$0 (union sk_?X_37$0 sk_?X_38$0)) +(assert (! (= sk_?X_36$0 (set.union sk_?X_37$0 sk_?X_38$0)) :named precondition_of_rec_copy_loop_34_11_23)) -(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) +(assert (! (= Alloc$0 (set.union FP_Caller$0 Alloc$0)) :named initial_footprint_of_rec_copy_loop_34_11_5)) (assert (! (= cp_1$0 tmp_1$0) :named assign_42_4)) -(assert (! (= FP_3$0 (union FP$0 (singleton tmp_1$0))) :named assign_42_10_1)) +(assert (! (= FP_3$0 (set.union FP$0 (set.singleton tmp_1$0))) :named assign_42_10_1)) (assert (! (or (Btwn$0 next$0 curr$0 null$0 null$0) (not (lseg_struct$0 sk_?X_37$0 next$0 curr$0 null$0))) diff --git a/test/regress/regress0/sets/setel-eq.smt2 b/test/regress/regress0/sets/setel-eq.smt2 index 35b89645a..ec8756896 100644 --- a/test/regress/regress0/sets/setel-eq.smt2 +++ b/test/regress/regress0/sets/setel-eq.smt2 @@ -4,7 +4,7 @@ (declare-fun T () (Set Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (member y S)) -(assert (not (member x (union S T)))) +(assert (set.member y S)) +(assert (not (set.member x (set.union S T)))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress0/sets/sets-deq-dd.smt2 b/test/regress/regress0/sets/sets-deq-dd.smt2 index 17ca1fce2..ccb0452a4 100644 --- a/test/regress/regress0/sets/sets-deq-dd.smt2 +++ b/test/regress/regress0/sets/sets-deq-dd.smt2 @@ -4,5 +4,5 @@ (set-logic ALL) (set-info :status sat) (declare-fun S () (Set (_ BitVec 1))) -(assert (not (= S (as emptyset (Set (_ BitVec 1)))))) +(assert (not (= S (as set.empty (Set (_ BitVec 1)))))) (check-sat) diff --git a/test/regress/regress0/sets/sets-equal.smt2 b/test/regress/regress0/sets/sets-equal.smt2 index adccd51c5..c643c8b78 100644 --- a/test/regress/regress0/sets/sets-equal.smt2 +++ b/test/regress/regress0/sets/sets-equal.smt2 @@ -6,9 +6,9 @@ (assert (= x y)) (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) -(assert (not (member x a))) -(assert (member y (union a b))) +(assert (not (set.member x a))) +(assert (set.member y (set.union a b))) (assert (= x z)) -(assert (not (member z a))) +(assert (not (set.member z a))) (assert (= a b)) (check-sat) diff --git a/test/regress/regress0/sets/sets-extr.smt2 b/test/regress/regress0/sets/sets-extr.smt2 index c497ff189..1cbe0de9c 100644 --- a/test/regress/regress0/sets/sets-extr.smt2 +++ b/test/regress/regress0/sets/sets-extr.smt2 @@ -9,7 +9,7 @@ (declare-fun S () (Set Atom)) -(assert (= S (union (singleton a) (union (singleton c) (singleton b))))) +(assert (= S (set.union (set.singleton a) (set.union (set.singleton c) (set.singleton b))))) (check-sat) diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2 index 2faf72768..6857e5147 100644 --- a/test/regress/regress0/sets/sets-inter.smt2 +++ b/test/regress/regress0/sets/sets-inter.smt2 @@ -4,8 +4,8 @@ (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) (declare-fun x () Int) -;(assert (not (member x a))) -(assert (member x (intersection a b))) -(assert (not (member x b))) +;(assert (not (set.member x a))) +(assert (set.member x (set.intersection a b))) +(assert (not (set.member x b))) (check-sat) (exit) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index 8ac414829..4a49bef07 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -6,11 +6,11 @@ (declare-fun A () SetInt) (declare-fun B () SetInt) (declare-fun x () Int) -(assert (member x (union A B))) +(assert (set.member x (set.union A B))) -(assert (not (member x (intersection A B)))) -(assert (not (member x (setminus A B)))) -;(assert (not (member x (setminus B A)))) -;(assert (member x B)) +(assert (not (set.member x (set.intersection A B)))) +(assert (not (set.member x (set.minus A B)))) +;(assert (not (set.member x (set.minus B A)))) +;(assert (set.member x B)) (check-sat) diff --git a/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 index e8c98e09c..2af676f8b 100644 --- a/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 +++ b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 @@ -7,8 +7,8 @@ (declare-fun x () (Set Real)) (declare-fun y () (Set Real)) -(assert (member 0.5 y)) -(assert (member y s)) -(assert (or (= s t) (= s (singleton (singleton 1.0))) (= s (singleton (singleton 0.0))))) +(assert (set.member 0.5 y)) +(assert (set.member y s)) +(assert (or (= s t) (= s (set.singleton (set.singleton 1.0))) (= s (set.singleton (set.singleton 0.0))))) (check-sat) diff --git a/test/regress/regress0/sets/sets-poly-int-real.smt2 b/test/regress/regress0/sets/sets-poly-int-real.smt2 index df79a39b0..20832c573 100644 --- a/test/regress/regress0/sets/sets-poly-int-real.smt2 +++ b/test/regress/regress0/sets/sets-poly-int-real.smt2 @@ -7,11 +7,11 @@ (declare-fun r1 () (Set Real)) (declare-fun r2 () (Set Real)) (declare-fun r3 () (Set Real)) -(assert (and (member 1.5 s) (member 0.0 s))) -(assert (= t1 (union s (singleton 2.5)))) -(assert (= t2 (union s (singleton 2.0)))) -(assert (= t3 (union r3 (singleton 2.5)))) -(assert (= (intersection r1 r2) (intersection s (singleton 0.0)))) -(assert (not (= r1 (as emptyset (Set Real))))) +(assert (and (set.member 1.5 s) (set.member 0.0 s))) +(assert (= t1 (set.union s (set.singleton 2.5)))) +(assert (= t2 (set.union s (set.singleton 2.0)))) +(assert (= t3 (set.union r3 (set.singleton 2.5)))) +(assert (= (set.intersection r1 r2) (set.intersection s (set.singleton 0.0)))) +(assert (not (= r1 (as set.empty (Set Real))))) (check-sat) diff --git a/test/regress/regress0/sets/sets-poly-nonint.smt2 b/test/regress/regress0/sets/sets-poly-nonint.smt2 index 58ff563bc..f572fafc7 100644 --- a/test/regress/regress0/sets/sets-poly-nonint.smt2 +++ b/test/regress/regress0/sets/sets-poly-nonint.smt2 @@ -4,8 +4,8 @@ (declare-fun t () (Set Real)) (declare-fun r () (Set Real)) (declare-fun u () (Set Real)) -(assert (member 1.5 t)) -(assert (member 2.5 r)) -(assert (member 3.5 u)) +(assert (set.member 1.5 t)) +(assert (set.member 2.5 r)) +(assert (set.member 3.5 u)) (assert (or (= s t) (= s r) (= s u))) (check-sat) diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 index b92c4b2cf..3dcafae08 100644 --- a/test/regress/regress0/sets/sets-sample.smt2 +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -13,24 +13,24 @@ (declare-fun b () (Set Int)) (declare-fun c () (Set Int)) (declare-fun e () Int) -(assert (= a (singleton 5))) -(assert (= c (union a b) )) -(assert (not (= c (intersection a b) ))) -(assert (= c (setminus a b) )) -(assert (subset a b)) -(assert (member e c)) -(assert (member e a)) -(assert (member e (intersection a b))) +(assert (= a (set.singleton 5))) +(assert (= c (set.union a b) )) +(assert (not (= c (set.intersection a b) ))) +(assert (= c (set.minus a b) )) +(assert (set.subset a b)) +(assert (set.member e c)) +(assert (set.member e a)) +(assert (set.member e (set.intersection a b))) (check-sat) (pop 1) -; UF can tell that this is UNSAT (union) +; UF can tell that this is UNSAT (set.union) (push 1) (declare-fun x () (Set Int)) (declare-fun y () (Set Int)) (declare-fun z () (Set Int)) (assert (= x y)) -(assert (not (= (union x z) (union y z)))) +(assert (not (= (set.union x z) (set.union y z)))) (check-sat) (pop 1) @@ -42,12 +42,12 @@ (declare-fun e2 () Int) (assert (= x y)) (assert (= e1 e2)) -(assert (member e1 x)) -(assert (not (member e2 y))) +(assert (set.member e1 x)) +(assert (not (set.member e2 y))) (check-sat) (pop 1) -; UF can tell that this is UNSAT (merge union + containment examples) +; UF can tell that this is UNSAT (merge set.union + containment examples) (push 1) (declare-fun x () (Set Int)) (declare-fun y () (Set Int)) @@ -56,15 +56,15 @@ (declare-fun e2 () Int) (assert (= x y)) (assert (= e1 e2)) -(assert (member e1 (union x z))) -(assert (not (member e2 (union y z)))) +(assert (set.member e1 (set.union x z))) +(assert (not (set.member e2 (set.union y z)))) (check-sat) (pop 1) ; test all the other kinds for completeness (push 1) -(assert (member 5 (insert 1 2 3 4 (singleton 5)))) -(assert (member 5 (insert 1 2 3 4 (as emptyset (Set Int))))) +(assert (set.member 5 (set.insert 1 2 3 4 (set.singleton 5)))) +(assert (set.member 5 (set.insert 1 2 3 4 (as set.empty (Set Int))))) (check-sat) (exit) diff --git a/test/regress/regress0/sets/sets-sharing.smt2 b/test/regress/regress0/sets/sets-sharing.smt2 index 1ac2e1603..37ad90017 100644 --- a/test/regress/regress0/sets/sets-sharing.smt2 +++ b/test/regress/regress0/sets/sets-sharing.smt2 @@ -4,8 +4,8 @@ (declare-fun S () (Set Int)) (declare-fun x () Int) -(assert (member (+ 5 x) S)) -(assert (not (member 9 S))) +(assert (set.member (+ 5 x) S)) +(assert (not (set.member 9 S))) (assert (= x 4)) (check-sat) diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2 index b794633e3..8dbe5ffa5 100644 --- a/test/regress/regress0/sets/sets-union.smt2 +++ b/test/regress/regress0/sets/sets-union.smt2 @@ -6,10 +6,10 @@ (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) (declare-fun x () Int) -(assert (not (member x a))) -(assert (member x (union a b))) +(assert (not (set.member x a))) +(assert (set.member x (set.union a b))) (check-sat) ;(get-model) -(assert (not (member x b))) +(assert (not (set.member x b))) (check-sat) (exit) diff --git a/test/regress/regress0/sets/sharing-simp.smt2 b/test/regress/regress0/sets/sharing-simp.smt2 index 761428fde..be746be1d 100644 --- a/test/regress/regress0/sets/sharing-simp.smt2 +++ b/test/regress/regress0/sets/sharing-simp.smt2 @@ -7,9 +7,9 @@ (declare-fun C () (Set Int)) (declare-fun D () (Set Int)) -(assert (member x A)) -(assert (member y B)) -(assert (or (= C (intersection A B)) (= D (intersection A B)))) +(assert (set.member x A)) +(assert (set.member y B)) +(assert (or (= C (set.intersection A B)) (= D (set.intersection A B)))) (check-sat) diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2 index bb969f866..ea936c730 100644 --- a/test/regress/regress0/sets/union-1a-flip.smt2 +++ b/test/regress/regress0/sets/union-1a-flip.smt2 @@ -8,9 +8,9 @@ (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) (declare-fun x () Int) -(assert (member x A)) +(assert (set.member x A)) (push 1) -(assert (not (member x (union A B)))) +(assert (not (set.member x (set.union A B)))) (check-sat) (pop 1) (check-sat) diff --git a/test/regress/regress0/sets/union-1a.smt2 b/test/regress/regress0/sets/union-1a.smt2 index ad684070f..007d64d4e 100644 --- a/test/regress/regress0/sets/union-1a.smt2 +++ b/test/regress/regress0/sets/union-1a.smt2 @@ -8,9 +8,9 @@ (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) (declare-fun x () Int) -(assert (not (member x (union A B)))) +(assert (not (set.member x (set.union A B)))) (push 1) -(assert (member x A)) +(assert (set.member x A)) (check-sat) (pop 1) (check-sat) diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2 index 228452f54..92d241dd7 100644 --- a/test/regress/regress0/sets/union-1b-flip.smt2 +++ b/test/regress/regress0/sets/union-1b-flip.smt2 @@ -8,9 +8,9 @@ (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) (declare-fun x () Int) -(assert (member x B)) +(assert (set.member x B)) (push 1) -(assert (not (member x (union A B)))) +(assert (not (set.member x (set.union A B)))) (check-sat) (pop 1) (check-sat) diff --git a/test/regress/regress0/sets/union-1b.smt2 b/test/regress/regress0/sets/union-1b.smt2 index 8829b6152..5be785079 100644 --- a/test/regress/regress0/sets/union-1b.smt2 +++ b/test/regress/regress0/sets/union-1b.smt2 @@ -8,9 +8,9 @@ (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) (declare-fun x () Int) -(assert (not (member x (union A B)))) +(assert (not (set.member x (set.union A B)))) (push 1) -(assert (member x B)) +(assert (set.member x B)) (check-sat) (pop 1) (check-sat) diff --git a/test/regress/regress0/sets/union-2.smt2 b/test/regress/regress0/sets/union-2.smt2 index 52d2e7e8c..12a1fe8ff 100644 --- a/test/regress/regress0/sets/union-2.smt2 +++ b/test/regress/regress0/sets/union-2.smt2 @@ -6,7 +6,7 @@ (declare-fun B () (Set Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (member x (union A B))) -(assert (not (member y A))) -(assert (not (member y B))) +(assert (set.member x (set.union A B))) +(assert (not (set.member y A))) +(assert (not (set.member y B))) (check-sat) diff --git a/test/regress/regress0/sets/univset-simp.smt2 b/test/regress/regress0/sets/univset-simp.smt2 index a8875cc41..04f413399 100644 --- a/test/regress/regress0/sets/univset-simp.smt2 +++ b/test/regress/regress0/sets/univset-simp.smt2 @@ -12,12 +12,12 @@ (declare-fun x () Int) -(assert (not (member 0 a))) -(assert (member 0 b)) -(assert (not (member 1 c))) -(assert (member 2 d)) -(assert (= e (as univset (Set Int)))) -(assert (= f (complement d))) -(assert (not (member x (as univset (Set Int))))) +(assert (not (set.member 0 a))) +(assert (set.member 0 b)) +(assert (not (set.member 1 c))) +(assert (set.member 2 d)) +(assert (= e (as set.universe (Set Int)))) +(assert (= f (set.complement d))) +(assert (not (set.member x (as set.universe (Set Int))))) (check-sat) diff --git a/test/regress/regress0/tptp/Axioms/BOO004-0.ax b/test/regress/regress0/tptp/Axioms/BOO004-0.ax index e02b4c2f8..7a36794df 100644 --- a/test/regress/regress0/tptp/Axioms/BOO004-0.ax +++ b/test/regress/regress0/tptp/Axioms/BOO004-0.ax @@ -15,7 +15,7 @@ % Maximal clause size : 1 ( 1 average) % Number of predicates : 1 ( 0 propositional; 2-2 arity) % Number of functors : 5 ( 2 constant; 0-2 arity) -% Number of variables : 14 ( 0 singleton) +% Number of variables : 14 ( 0 set.singleton) % Maximal term depth : 3 ( 2 average) % SPC : diff --git a/test/regress/regress0/tptp/Axioms/SYN000+0.ax b/test/regress/regress0/tptp/Axioms/SYN000+0.ax index 24ef682b7..136a70b3c 100644 --- a/test/regress/regress0/tptp/Axioms/SYN000+0.ax +++ b/test/regress/regress0/tptp/Axioms/SYN000+0.ax @@ -18,7 +18,7 @@ % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 3 ( 3 propositional; 0-0 arity) % Number of functors : 0 ( 0 constant; --- arity) -% Number of variables : 0 ( 0 singleton; 0 !; 0 ?) +% Number of variables : 0 ( 0 set.singleton; 0 !; 0 ?) % Maximal term depth : 0 ( 0 average) % SPC : diff --git a/test/regress/regress0/tptp/Axioms/SYN000-0.ax b/test/regress/regress0/tptp/Axioms/SYN000-0.ax index d67e61aee..01a6d9ba0 100644 --- a/test/regress/regress0/tptp/Axioms/SYN000-0.ax +++ b/test/regress/regress0/tptp/Axioms/SYN000-0.ax @@ -15,7 +15,7 @@ % Maximal clause size : 1 ( 1 average) % Number of predicates : 3 ( 3 propositional; 0-0 arity) % Number of functors : 0 ( 0 constant; --- arity) -% Number of variables : 0 ( 0 singleton) +% Number of variables : 0 ( 0 set.singleton) % Maximal term depth : 0 ( 0 average) % SPC : diff --git a/test/regress/regress0/tptp/BOO003-4.p b/test/regress/regress0/tptp/BOO003-4.p index 0ea15fefc..5391e0689 100644 --- a/test/regress/regress0/tptp/BOO003-4.p +++ b/test/regress/regress0/tptp/BOO003-4.p @@ -16,7 +16,7 @@ % Maximal clause size : 1 ( 1 average) % Number of predicates : 1 ( 0 propositional; 2-2 arity) % Number of functors : 6 ( 3 constant; 0-2 arity) -% Number of variables : 14 ( 0 singleton) +% Number of variables : 14 ( 0 set.singleton) % Maximal term depth : 3 ( 2 average) % SPC : CNF_UNS_RFO_PEQ_UEQ diff --git a/test/regress/regress0/tptp/BOO027-1.p b/test/regress/regress0/tptp/BOO027-1.p index a3cd4224c..3b5297e16 100644 --- a/test/regress/regress0/tptp/BOO027-1.p +++ b/test/regress/regress0/tptp/BOO027-1.p @@ -18,7 +18,7 @@ % Maximal clause size : 1 ( 1 average) % Number of predicates : 1 ( 0 propositional; 2-2 arity) % Number of functors : 5 ( 2 constant; 0-2 arity) -% Number of variables : 10 ( 0 singleton) +% Number of variables : 10 ( 0 set.singleton) % Maximal term depth : 5 ( 3 average) % SPC : CNF_SAT_RFO_PEQ_UEQ diff --git a/test/regress/regress0/tptp/KRS018+1.p b/test/regress/regress0/tptp/KRS018+1.p index 8d0bbe25c..969c1c6f4 100644 --- a/test/regress/regress0/tptp/KRS018+1.p +++ b/test/regress/regress0/tptp/KRS018+1.p @@ -22,7 +22,7 @@ % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 6 ( 0 propositional; 1-2 arity) % Number of functors : 0 ( 0 constant; --- arity) -% Number of variables : 6 ( 0 singleton; 4 !; 2 ?) +% Number of variables : 6 ( 0 set.singleton; 4 !; 2 ?) % Maximal term depth : 1 ( 1 average) % SPC : FOF_SAT_RFO_NEQ diff --git a/test/regress/regress0/tptp/KRS063+1.p b/test/regress/regress0/tptp/KRS063+1.p index 737741dee..dca3edbca 100644 --- a/test/regress/regress0/tptp/KRS063+1.p +++ b/test/regress/regress0/tptp/KRS063+1.p @@ -20,7 +20,7 @@ % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 11 ( 0 propositional; 1-2 arity) % Number of functors : 7 ( 7 constant; 0-0 arity) -% Number of variables : 37 ( 0 singleton; 36 !; 1 ?) +% Number of variables : 37 ( 0 set.singleton; 36 !; 1 ?) % Maximal term depth : 1 ( 1 average) % SPC : FOF_UNS_RFO_SEQ diff --git a/test/regress/regress0/tptp/MGT019+2.p b/test/regress/regress0/tptp/MGT019+2.p index e6a2ffe74..7bebdc095 100644 --- a/test/regress/regress0/tptp/MGT019+2.p +++ b/test/regress/regress0/tptp/MGT019+2.p @@ -25,7 +25,7 @@ % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 7 ( 0 propositional; 1-4 arity) % Number of functors : 5 ( 2 constant; 0-2 arity) -% Number of variables : 11 ( 0 singleton; 9 !; 2 ?) +% Number of variables : 11 ( 0 set.singleton; 9 !; 2 ?) % Maximal term depth : 2 ( 1 average) % SPC : FOF_CSA_RFO_SEQ diff --git a/test/regress/regress0/tptp/MGT031-1.p b/test/regress/regress0/tptp/MGT031-1.p index f5cd1937e..14fb64d63 100644 --- a/test/regress/regress0/tptp/MGT031-1.p +++ b/test/regress/regress0/tptp/MGT031-1.p @@ -18,7 +18,7 @@ % Maximal clause size : 5 ( 3 average) % Number of predicates : 6 ( 0 propositional; 1-3 arity) % Number of functors : 10 ( 6 constant; 0-2 arity) -% Number of variables : 23 ( 0 singleton) +% Number of variables : 23 ( 0 set.singleton) % Maximal term depth : 3 ( 1 average) % SPC : CNF_SAT_RFO_EQU_NUE diff --git a/test/regress/regress0/tptp/MGT041-2.p b/test/regress/regress0/tptp/MGT041-2.p index a10a2f42d..7735b39a8 100644 --- a/test/regress/regress0/tptp/MGT041-2.p +++ b/test/regress/regress0/tptp/MGT041-2.p @@ -19,7 +19,7 @@ % Maximal clause size : 4 ( 2 average) % Number of predicates : 6 ( 0 propositional; 1-3 arity) % Number of functors : 4 ( 4 constant; 0-0 arity) -% Number of variables : 8 ( 1 singleton) +% Number of variables : 8 ( 1 set.singleton) % Maximal term depth : 1 ( 1 average) % SPC : CNF_UNS_EPR diff --git a/test/regress/regress0/tptp/NLP114-1.p b/test/regress/regress0/tptp/NLP114-1.p index cf5bd272a..23221232a 100644 --- a/test/regress/regress0/tptp/NLP114-1.p +++ b/test/regress/regress0/tptp/NLP114-1.p @@ -19,7 +19,7 @@ % Maximal clause size : 18 ( 3 average) % Number of predicates : 18 ( 1 propositional; 0-3 arity) % Number of functors : 11 ( 11 constant; 0-0 arity) -% Number of variables : 11 ( 0 singleton) +% Number of variables : 11 ( 0 set.singleton) % Maximal term depth : 1 ( 1 average) % SPC : CNF_SAT_EPR diff --git a/test/regress/regress0/tptp/SYN000-1.p b/test/regress/regress0/tptp/SYN000-1.p index b6a68ec95..f32940536 100644 --- a/test/regress/regress0/tptp/SYN000-1.p +++ b/test/regress/regress0/tptp/SYN000-1.p @@ -16,7 +16,7 @@ % Maximal clause size : 5 ( 2 average) % Number of predicates : 16 ( 10 propositional; 0-3 arity) % Number of functors : 8 ( 5 constant; 0-3 arity) -% Number of variables : 11 ( 5 singleton) +% Number of variables : 11 ( 5 set.singleton) % Maximal term depth : 4 ( 2 average) % SPC : CNF_UNS_RFO_SEQ_NHN diff --git a/test/regress/regress0/tptp/SYN075+1.p b/test/regress/regress0/tptp/SYN075+1.p index 7ef40217c..20720a552 100644 --- a/test/regress/regress0/tptp/SYN075+1.p +++ b/test/regress/regress0/tptp/SYN075+1.p @@ -20,7 +20,7 @@ % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 2 ( 0 propositional; 2-2 arity) % Number of functors : 0 ( 0 constant; --- arity) -% Number of variables : 8 ( 0 singleton; 4 !; 4 ?) +% Number of variables : 8 ( 0 set.singleton; 4 !; 4 ?) % Maximal term depth : 1 ( 1 average) % SPC : FOF_THM_RFO_SEQ diff --git a/test/regress/regress0/tptp/SYN075-1.p b/test/regress/regress0/tptp/SYN075-1.p index 85ac2d278..2a1a10783 100644 --- a/test/regress/regress0/tptp/SYN075-1.p +++ b/test/regress/regress0/tptp/SYN075-1.p @@ -18,7 +18,7 @@ % Maximal clause size : 4 ( 3 average) % Number of predicates : 2 ( 0 propositional; 2-2 arity) % Number of functors : 5 ( 2 constant; 0-2 arity) -% Number of variables : 23 ( 2 singleton) +% Number of variables : 23 ( 2 set.singleton) % Maximal term depth : 2 ( 1 average) % SPC : CNF_UNS_RFO_SEQ_NHN |