diff options
Diffstat (limited to 'test/regress/regress1/sets')
72 files changed, 596 insertions, 596 deletions
diff --git a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 index 666d16367..144566fc5 100644 --- a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 +++ b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 @@ -8,15 +8,15 @@ (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 z3v56 () Int) (declare-fun z3v57 () Int) (assert (distinct z3v56 z3v57)) diff --git a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 index 4863baa64..9a2521520 100644 --- a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 +++ b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 @@ -3,15 +3,15 @@ (set-info :status sat) (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 z3v58 () Int) (declare-fun z3v59 () Int) (assert (distinct z3v58 z3v59)) diff --git a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 index dcfd13521..b2732dbd2 100644 --- a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 +++ b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -3,15 +3,15 @@ (set-info :status sat) (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 z3v60 () Int) (declare-fun z3v61 () Int) (assert (distinct z3v60 z3v61)) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 index 9e5962a24..ee24367c3 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 @@ -2,13 +2,13 @@ (set-logic QF_ALL) (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_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset 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 (set.minus s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) (declare-fun z3v66 () Int) (declare-fun z3v67 () Int) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 index 88cf21aa8..b0cfe4888 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 @@ -2,13 +2,13 @@ (set-logic QF_ALL) (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_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset 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 (set.minus s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) (declare-fun z3f70 (Int) mySet) (declare-fun z3f72 (Int) mySet) @@ -177,7 +177,7 @@ (z3f70 z3v270)))) (assert (= z3v242 (z3f77 z3v271 z3v270))) (assert (= z3v242 z3v243)) -(assert (subset (z3f70 z3v242) +(assert (set.subset (z3f70 z3v242) (z3f70 z3v244))) (assert (= (z3f72 z3v243) smt_set_emp)) (assert (= (z3f72 z3v244) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 index 1967497da..9ac15e9a4 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.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_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_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset 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 (set.minus s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) (declare-fun z3v66 () Int) (declare-fun z3v67 () Int) (assert (distinct z3v66 z3v67)) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 index cb1dfc842..68ed72a93 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.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 z3v66 () Int) (declare-fun z3v67 () Int) (assert (distinct z3v66 z3v67)) diff --git a/test/regress/regress1/sets/arjun-set-univ.cvc.smt2 b/test/regress/regress1/sets/arjun-set-univ.cvc.smt2 index b76b48f2d..8e851bb7f 100644 --- a/test/regress/regress1/sets/arjun-set-univ.cvc.smt2 +++ b/test/regress/regress1/sets/arjun-set-univ.cvc.smt2 @@ -6,11 +6,11 @@ (declare-fun x () (Set Bool)) (declare-fun y () (Set Bool)) (declare-fun z () (Set Bool)) -(assert (= x (singleton true))) -(assert (= y (singleton false))) +(assert (= x (set.singleton true))) +(assert (= y (set.singleton false))) (push 1) -(assert (= z (complement y))) +(assert (= z (set.complement y))) (check-sat) diff --git a/test/regress/regress1/sets/card-3.smt2 b/test/regress/regress1/sets/card-3.smt2 index 0e96b0231..383395b0d 100644 --- a/test/regress/regress1/sets/card-3.smt2 +++ b/test/regress/regress1/sets/card-3.smt2 @@ -4,9 +4,9 @@ (declare-fun s () (Set E)) (declare-fun t () (Set E)) (declare-fun u () (Set E)) -(assert (>= (card (union s t)) 8)) -(assert (>= (card (union s u)) 8)) -(assert (<= (card (union t u)) 5)) -(assert (<= (card s) 5)) -(assert (= (as emptyset (Set E)) (intersection t u))) +(assert (>= (set.card (set.union s t)) 8)) +(assert (>= (set.card (set.union s u)) 8)) +(assert (<= (set.card (set.union t u)) 5)) +(assert (<= (set.card s) 5)) +(assert (= (as set.empty (Set E)) (set.intersection t u))) (check-sat) diff --git a/test/regress/regress1/sets/card-4.smt2 b/test/regress/regress1/sets/card-4.smt2 index 456e24ca7..019b16a09 100644 --- a/test/regress/regress1/sets/card-4.smt2 +++ b/test/regress/regress1/sets/card-4.smt2 @@ -4,21 +4,21 @@ (declare-fun s () (Set E)) (declare-fun t () (Set E)) (declare-fun u () (Set E)) -(assert (>= (card (union s t)) 8)) -(assert (>= (card (union s u)) 8)) -;(assert (<= (card (union t u)) 5)) -(assert (<= (card s) 5)) -(assert (= (as emptyset (Set E)) (intersection t u))) +(assert (>= (set.card (set.union s t)) 8)) +(assert (>= (set.card (set.union s u)) 8)) +;(assert (<= (set.card (set.union t u)) 5)) +(assert (<= (set.card s) 5)) +(assert (= (as set.empty (Set E)) (set.intersection t u))) (declare-fun x1 () E) (declare-fun x2 () E) (declare-fun x3 () E) (declare-fun x4 () E) (declare-fun x5 () E) (declare-fun x6 () E) -(assert (member x1 s)) -(assert (member x2 s)) -(assert (member x3 s)) -(assert (member x4 s)) -(assert (member x5 s)) -(assert (member x6 s)) +(assert (set.member x1 s)) +(assert (set.member x2 s)) +(assert (set.member x3 s)) +(assert (set.member x4 s)) +(assert (set.member x5 s)) +(assert (set.member x6 s)) (check-sat) diff --git a/test/regress/regress1/sets/card-5.smt2 b/test/regress/regress1/sets/card-5.smt2 index 4135a0c16..c24ca974a 100644 --- a/test/regress/regress1/sets/card-5.smt2 +++ b/test/regress/regress1/sets/card-5.smt2 @@ -4,22 +4,22 @@ (declare-fun s () (Set E)) (declare-fun t () (Set E)) (declare-fun u () (Set E)) -(assert (>= (card (union s t)) 8)) -(assert (>= (card (union s u)) 8)) -;(assert (<= (card (union t u)) 5)) -(assert (<= (card s) 5)) -(assert (= (as emptyset (Set E)) (intersection t u))) +(assert (>= (set.card (set.union s t)) 8)) +(assert (>= (set.card (set.union s u)) 8)) +;(assert (<= (set.card (set.union t u)) 5)) +(assert (<= (set.card s) 5)) +(assert (= (as set.empty (Set E)) (set.intersection t u))) (declare-fun x1 () E) (declare-fun x2 () E) (declare-fun x3 () E) (declare-fun x4 () E) (declare-fun x5 () E) (declare-fun x6 () E) -(assert (member x1 s)) -(assert (member x2 s)) -(assert (member x3 s)) -(assert (member x4 s)) -(assert (member x5 s)) -(assert (member x6 s)) +(assert (set.member x1 s)) +(assert (set.member x2 s)) +(assert (set.member x3 s)) +(assert (set.member x4 s)) +(assert (set.member x5 s)) +(assert (set.member x6 s)) (assert (distinct x1 x2 x3 x4 x5 x6)) (check-sat) diff --git a/test/regress/regress1/sets/card-6.smt2 b/test/regress/regress1/sets/card-6.smt2 index 87d87c03b..b0ef3a3b9 100644 --- a/test/regress/regress1/sets/card-6.smt2 +++ b/test/regress/regress1/sets/card-6.smt2 @@ -6,12 +6,12 @@ (declare-fun C () (Set E)) (assert (and - (= (as emptyset (Set E)) - (intersection A B)) - (subset C (union A B)) - (>= (card C) 5) - (<= (card A) 2) - (<= (card B) 2) + (= (as set.empty (Set E)) + (set.intersection A B)) + (set.subset C (set.union A B)) + (>= (set.card C) 5) + (<= (set.card A) 2) + (<= (set.card B) 2) ) ) (check-sat) diff --git a/test/regress/regress1/sets/card-7.smt2 b/test/regress/regress1/sets/card-7.smt2 index df1867c63..30595218c 100644 --- a/test/regress/regress1/sets/card-7.smt2 +++ b/test/regress/regress1/sets/card-7.smt2 @@ -22,26 +22,26 @@ (declare-fun A19 () (Set E)) (declare-fun A20 () (Set E)) (assert (and - (= (card A1) 1) - (= (card A2) 1) - (= (card A3) 1) - (= (card A4) 1) - (= (card A5) 1) - (= (card A6) 1) - (= (card A7) 1) - (= (card A8) 1) - (= (card A9) 1) - (= (card A10) 1) - (= (card A11) 1) - (= (card A12) 1) - (= (card A13) 1) - (= (card A14) 1) - (= (card A15) 1) - (= (card A16) 1) - (= (card A17) 1) - (= (card A18) 1) - (= (card A19) 1) - (= (card A20) 1) + (= (set.card A1) 1) + (= (set.card A2) 1) + (= (set.card A3) 1) + (= (set.card A4) 1) + (= (set.card A5) 1) + (= (set.card A6) 1) + (= (set.card A7) 1) + (= (set.card A8) 1) + (= (set.card A9) 1) + (= (set.card A10) 1) + (= (set.card A11) 1) + (= (set.card A12) 1) + (= (set.card A13) 1) + (= (set.card A14) 1) + (= (set.card A15) 1) + (= (set.card A16) 1) + (= (set.card A17) 1) + (= (set.card A18) 1) + (= (set.card A19) 1) + (= (set.card A20) 1) )) -(assert (= 20 (+ (card A1) (card A2) (card A3) (card A4) (card A5) (card A6) (card A7) (card A8) (card A9) (card A10) (card A11) (card A12) (card A13) (card A14) (card A15) (card A16) (card A17) (card A18) (card A19) (card A20)))) +(assert (= 20 (+ (set.card A1) (set.card A2) (set.card A3) (set.card A4) (set.card A5) (set.card A6) (set.card A7) (set.card A8) (set.card A9) (set.card A10) (set.card A11) (set.card A12) (set.card A13) (set.card A14) (set.card A15) (set.card A16) (set.card A17) (set.card A18) (set.card A19) (set.card A20)))) (check-sat) diff --git a/test/regress/regress1/sets/card-vc6-minimized.smt2 b/test/regress/regress1/sets/card-vc6-minimized.smt2 index d7f4bdf1e..4f589cad7 100644 --- a/test/regress/regress1/sets/card-vc6-minimized.smt2 +++ b/test/regress/regress1/sets/card-vc6-minimized.smt2 @@ -6,10 +6,10 @@ (declare-fun alloc1 () (Set Int)) (declare-fun alloc2 () (Set Int)) (assert -(and (member x c) - (<= (card (setminus alloc1 alloc0)) 1) - (<= (card (setminus alloc2 alloc1)) - (card (setminus c (singleton x)))) - (> (card (setminus alloc2 alloc0)) (card c)) +(and (set.member x c) + (<= (set.card (set.minus alloc1 alloc0)) 1) + (<= (set.card (set.minus alloc2 alloc1)) + (set.card (set.minus c (set.singleton x)))) + (> (set.card (set.minus alloc2 alloc0)) (set.card c)) )) (check-sat) diff --git a/test/regress/regress1/sets/choose.cvc.smt2 b/test/regress/regress1/sets/choose.cvc.smt2 index 8c3be2f99..18a89334f 100644 --- a/test/regress/regress1/sets/choose.cvc.smt2 +++ b/test/regress/regress1/sets/choose.cvc.smt2 @@ -4,7 +4,7 @@ (set-option :incremental false) (declare-fun A () (Set Int)) (declare-fun a () Int) -(assert (not (= A (as emptyset (Set Int))))) -(assert (= (choose A) 10)) -(assert (= (choose A) a)) +(assert (not (= A (as set.empty (Set Int))))) +(assert (= (set.choose A) 10)) +(assert (= (set.choose A) a)) (check-sat) diff --git a/test/regress/regress1/sets/choose1.smt2 b/test/regress/regress1/sets/choose1.smt2 index 0e937169e..a96daa9d5 100644 --- a/test/regress/regress1/sets/choose1.smt2 +++ b/test/regress/regress1/sets/choose1.smt2 @@ -4,8 +4,8 @@ (set-option :produce-models true) (declare-fun A () (Set Int)) (declare-fun a () Int) -(assert (not (= A (as emptyset (Set Int))))) -(assert (= (choose A) 10)) -(assert (= a (choose A))) -(assert (exists ((x Int)) (and (= x (choose A)) (= x a)))) +(assert (not (= A (as set.empty (Set Int))))) +(assert (= (set.choose A) 10)) +(assert (= a (set.choose A))) +(assert (exists ((x Int)) (and (= x (set.choose A)) (= x a)))) (check-sat) diff --git a/test/regress/regress1/sets/choose2.smt2 b/test/regress/regress1/sets/choose2.smt2 index 85a5d18d3..494a74f0b 100644 --- a/test/regress/regress1/sets/choose2.smt2 +++ b/test/regress/regress1/sets/choose2.smt2 @@ -2,5 +2,5 @@ (set-info :status unsat) (set-option :produce-models true) (declare-fun A () (Set Int)) -(assert (distinct (choose A) (choose A))) +(assert (distinct (set.choose A) (set.choose A))) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/sets/choose3.smt2 b/test/regress/regress1/sets/choose3.smt2 index 2a844efeb..284d3c9e9 100644 --- a/test/regress/regress1/sets/choose3.smt2 +++ b/test/regress/regress1/sets/choose3.smt2 @@ -4,6 +4,6 @@ (set-info :status sat) (set-option :produce-models true) (declare-fun A () (Set Int)) -(assert (= (choose A) 10)) -(assert (= A (as emptyset (Set Int)))) +(assert (= (set.choose A) 10)) +(assert (= A (as set.empty (Set Int)))) (check-sat) diff --git a/test/regress/regress1/sets/choose4.smt2 b/test/regress/regress1/sets/choose4.smt2 index 6cb97c3e3..5590a0d5f 100644 --- a/test/regress/regress1/sets/choose4.smt2 +++ b/test/regress/regress1/sets/choose4.smt2 @@ -4,8 +4,8 @@ (set-option :produce-models true) (declare-fun A () (Set Int)) (declare-fun a () Int) -(assert (not (= A (as emptyset (Set Int))))) -(assert (member 10 A)) -(assert (= a (choose A))) -;(assert (exists ((x Int)) (and (= x (choose A)) (= x a)))) +(assert (not (= A (as set.empty (Set Int))))) +(assert (set.member 10 A)) +(assert (= a (set.choose A))) +;(assert (exists ((x Int)) (and (= x (set.choose A)) (= x a)))) (check-sat) diff --git a/test/regress/regress1/sets/comp-intersect.smt2 b/test/regress/regress1/sets/comp-intersect.smt2 index ab3206343..60d9046bd 100644 --- a/test/regress/regress1/sets/comp-intersect.smt2 +++ b/test/regress/regress1/sets/comp-intersect.smt2 @@ -6,9 +6,9 @@ (declare-fun x () (Set Int)) (declare-fun y () (Set Int)) -(assert (= x (comprehension ((z Int)) (> z 4) (* 5 z)))) -(assert (= y (comprehension ((z Int)) (< z 10) (+ (* 5 z) 1)))) +(assert (= x (set.comprehension ((z Int)) (> z 4) (* 5 z)))) +(assert (= y (set.comprehension ((z Int)) (< z 10) (+ (* 5 z) 1)))) -(assert (not (= (intersection x y) (as emptyset (Set Int))))) +(assert (not (= (set.intersection x y) (as set.empty (Set Int))))) (check-sat) diff --git a/test/regress/regress1/sets/comp-odd.smt2 b/test/regress/regress1/sets/comp-odd.smt2 index 1b1a13b34..5d2a65619 100644 --- a/test/regress/regress1/sets/comp-odd.smt2 +++ b/test/regress/regress1/sets/comp-odd.smt2 @@ -5,12 +5,12 @@ (declare-fun x () (Set Int)) -(assert (subset x (comprehension ((z Int)) true (* 2 z)))) +(assert (set.subset x (set.comprehension ((z Int)) true (* 2 z)))) (declare-fun a () Int) (declare-fun b () Int) (assert (= a (+ (* 8 b) 1))) -(assert (member a x)) +(assert (set.member a x)) (check-sat) diff --git a/test/regress/regress1/sets/comp-pos-member.smt2 b/test/regress/regress1/sets/comp-pos-member.smt2 index aeba4cadc..fdd5926b6 100644 --- a/test/regress/regress1/sets/comp-pos-member.smt2 +++ b/test/regress/regress1/sets/comp-pos-member.smt2 @@ -5,15 +5,15 @@ (declare-fun x () (Set Int)) -(assert (subset (comprehension ((z Int)) (>= z 0) (* 3 z)) x)) +(assert (set.subset (set.comprehension ((z Int)) (>= z 0) (* 3 z)) x)) (declare-fun a () Int) (declare-fun b () Int) (declare-fun c () Int) -(assert (not (member a x))) -(assert (not (member b x))) -(assert (not (member c x))) +(assert (not (set.member a x))) +(assert (not (set.member b x))) +(assert (not (set.member c x))) (assert (<= 0 a)) (assert (<= a b)) (assert (<= b c)) diff --git a/test/regress/regress1/sets/comp-positive.smt2 b/test/regress/regress1/sets/comp-positive.smt2 index af75230b3..6f8e3e1ab 100644 --- a/test/regress/regress1/sets/comp-positive.smt2 +++ b/test/regress/regress1/sets/comp-positive.smt2 @@ -5,8 +5,8 @@ (declare-fun x () (Set Int)) -(assert (subset x (comprehension ((z Int)) (> z 0) z))) +(assert (set.subset x (set.comprehension ((z Int)) (> z 0) z))) -(assert (member 0 x)) +(assert (set.member 0 x)) (check-sat) diff --git a/test/regress/regress1/sets/copy_check_heap_access_33_4.smt2 b/test/regress/regress1/sets/copy_check_heap_access_33_4.smt2 index 9af45c2dd..991470d30 100644 --- a/test/regress/regress1/sets/copy_check_heap_access_33_4.smt2 +++ b/test/regress/regress1/sets/copy_check_heap_access_33_4.smt2 @@ -46,19 +46,19 @@ (assert (! (forall ((l1 Loc) (l2 Loc)) (or (not Axiom_1$0) (or (<= (read$0 data$0 l1) (read$0 data$0 l2)) - (not (Btwn$0 next$0 l1 l2 null$0)) (not (member l1 sk_?X_4$0)) - (not (member l2 sk_?X_4$0))))) + (not (Btwn$0 next$0 l1 l2 null$0)) (not (set.member l1 sk_?X_4$0)) + (not (set.member l2 sk_?X_4$0))))) :named sortedness_3)) (assert (! (= (read$1 next$0 null$0) null$0) :named read_null_1)) -(assert (! (not (member tmp_2$0 Alloc$0)) :named new_31_11)) +(assert (! (not (set.member tmp_2$0 Alloc$0)) :named new_31_11)) -(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_copy_23_11_2)) +(assert (! (not (set.member null$0 Alloc$0)) :named initial_footprint_of_copy_23_11_2)) (assert (! (not (= lst$0 null$0)) :named if_else_26_6)) -(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) +(assert (! (= FP_Caller$0 (set.union FP$0 FP_Caller$0)) :named precondition_of_copy_23_11_4)) (assert (! (= sk_?X_4$0 FP$0) :named precondition_of_copy_23_11_5)) @@ -67,7 +67,7 @@ (assert (! (= cp_2$0 res_1$0) :named assign_32_4)) -(assert (! (= FP_1$0 (union FP$0 (singleton tmp_2$0))) :named assign_31_11)) +(assert (! (= FP_1$0 (set.union FP$0 (set.singleton tmp_2$0))) :named assign_31_11)) (assert (! (or (and (Btwn$0 next$0 lst$0 null$0 null$0) Axiom_1$0) (not (slseg_struct$0 sk_?X_4$0 data$0 next$0 lst$0 null$0))) @@ -76,13 +76,13 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst$0 l1 null$0) - (member l1 (slseg_domain$0 data$0 next$0 lst$0 null$0)) + (set.member l1 (slseg_domain$0 data$0 next$0 lst$0 null$0)) (not (= l1 null$0))) (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0))) - (not (member l1 (slseg_domain$0 data$0 next$0 lst$0 null$0)))))) + (not (set.member l1 (slseg_domain$0 data$0 next$0 lst$0 null$0)))))) :named slseg_footprint_2)) -(assert (! (not (member curr_2$0 FP_1$0)) :named check_heap_access_33_4)) +(assert (! (not (set.member curr_2$0 FP_1$0)) :named check_heap_access_33_4)) (assert (! (not (= tmp_2$0 null$0)) :named new_31_11_1)) @@ -92,14 +92,14 @@ (assert (! (= sk_?X_4$0 (slseg_domain$0 data$0 next$0 lst$0 null$0)) :named precondition_of_copy_23_11_7)) -(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) +(assert (! (= Alloc$0 (set.union FP_Caller$0 Alloc$0)) :named initial_footprint_of_copy_23_11_3)) (assert (! (= curr_2$0 lst$0) :named assign_30_4)) -(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_26_2_1)) +(assert (! (= FP_Caller_1$0 (set.minus FP_Caller$0 FP$0)) :named assign_26_2_1)) -(assert (! (= Alloc_1$0 (union Alloc$0 (singleton tmp_2$0))) :named assign_31_11_1)) +(assert (! (= Alloc_1$0 (set.union Alloc$0 (set.singleton tmp_2$0))) :named assign_31_11_1)) (assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_1)) diff --git a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 index 426661ba2..7c5e09b5a 100644 --- a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 +++ b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -3,15 +3,15 @@ (set-info :status sat) (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 z3v58 () Int) (declare-fun z3v59 () Int) (assert (distinct z3v58 z3v59)) diff --git a/test/regress/regress1/sets/finite-type/bug3663.smt2 b/test/regress/regress1/sets/finite-type/bug3663.smt2 index 5aef5d15d..8a696e129 100644 --- a/test/regress/regress1/sets/finite-type/bug3663.smt2 +++ b/test/regress/regress1/sets/finite-type/bug3663.smt2 @@ -4,5 +4,5 @@ (set-option :fmf-fun true) (declare-sort a 0) (declare-const b (Set a)) -(assert (= (card b) 0)) +(assert (= (set.card b) 0)) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 b/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 index 2c7acf282..25724a31e 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 @@ -5,7 +5,7 @@ (declare-datatype Color ((Red) (Green) (Blue))) (declare-fun A () (Set (Array Color Color))) (declare-fun B () (Set (Array Color Color))) -(assert (> (card A) 25)) -(assert (> (card B) 25)) +(assert (> (set.card A) 25)) +(assert (> (set.card B) 25)) (assert (distinct A B)) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 b/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 index 95d363397..d774e3b8e 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 @@ -5,6 +5,6 @@ (declare-fun S () (Set (Array Int Unit))) -(assert (> (card S) 1)) +(assert (> (set.card S) 1)) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 index eded56674..aa5b62d09 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 @@ -5,8 +5,8 @@ (declare-fun A () (Set Bool)) (declare-fun B () (Set Bool)) (declare-fun universe () (Set Bool)) -(assert (= (card A) 2)) -(assert (= (card B) 2)) -(assert (= (intersection A B) (as emptyset (Set Bool)))) -(assert (= universe (as univset (Set Bool)))) +(assert (= (set.card A) 2)) +(assert (= (set.card B) 2)) +(assert (= (set.intersection A B) (as set.empty (Set Bool)))) +(assert (= universe (as set.universe (Set Bool)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 index 7d3421463..161312cab 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 @@ -4,7 +4,7 @@ (set-option :sets-ext true) (declare-fun A () (Set Bool)) (declare-fun universe () (Set Bool)) -(assert (= (card A) 2)) -(assert (= universe (as univset (Set Bool)))) +(assert (= (set.card A) 2)) +(assert (= universe (as set.universe (Set Bool)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 index 4c83655ed..89daac5c7 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 @@ -5,8 +5,8 @@ (declare-fun A () (Set Bool)) (declare-fun B () (Set Bool)) (declare-fun universe () (Set Bool)) -(assert (= (card A) 2)) -(assert (= (card B) 2)) -(assert (= universe (as univset (Set Bool)))) +(assert (= (set.card A) 2)) +(assert (= (set.card B) 2)) +(assert (= universe (as set.universe (Set Bool)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 index 1e18597dc..90bd422b5 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 @@ -4,6 +4,6 @@ (set-option :produce-models true) (declare-fun A () (Set Bool)) (declare-fun x () Bool) -(assert (member (member x A) A)) -(assert (> (card A) 1)) +(assert (set.member (set.member x A) A)) +(assert (> (set.card A) 1)) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 index 150dd5cff..9849ea211 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 @@ -3,8 +3,8 @@ (set-option :sets-ext true) (declare-fun A () (Set Bool)) (declare-fun x () Bool) -(assert (member (member x A) A)) -(assert (> (card A) 1)) +(assert (set.member (set.member x A) A)) +(assert (> (set.card A) 1)) (declare-fun U () (Set Bool)) -(assert (= U (as univset (Set Bool)))) +(assert (= U (as set.universe (Set Bool)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 index 535646c7b..9ecc6a3aa 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 @@ -4,7 +4,7 @@ (set-option :sets-ext true) (declare-fun A () (Set (_ BitVec 3))) (declare-fun universe () (Set (_ BitVec 3))) -(assert (= (card A) 3)) -(assert (= universe (as univset (Set (_ BitVec 3))))) +(assert (= (set.card A) 3)) +(assert (= universe (as set.universe (Set (_ BitVec 3))))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 index 4eb8fc269..91bf1905a 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 @@ -5,12 +5,12 @@ (declare-fun A () (Set (_ BitVec 3))) (declare-fun B () (Set (_ BitVec 3))) (declare-fun universe () (Set (_ BitVec 3))) -(assert (= (card A) 5)) -(assert (= (card B) 5)) +(assert (= (set.card A) 5)) +(assert (= (set.card B) 5)) (assert (not (= A B))) -(assert (= (card (intersection A B)) 2)) -(assert (= (card (setminus A B)) 3)) -(assert (= (card (setminus B A)) 3)) -(assert (= universe (as univset (Set (_ BitVec 3))))) +(assert (= (set.card (set.intersection A B)) 2)) +(assert (= (set.card (set.minus A B)) 3)) +(assert (= (set.card (set.minus B A)) 3)) +(assert (= universe (as set.universe (Set (_ BitVec 3))))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 index 6e26ef4c7..adbe51507 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 @@ -6,14 +6,14 @@ (declare-fun B () (Set (_ BitVec 3))) (declare-fun universe () (Set (_ BitVec 3))) (declare-fun x () (_ BitVec 3)) -(assert (= (card A) 3)) -(assert (= (card B) 3)) +(assert (= (set.card A) 3)) +(assert (= (set.card B) 3)) (assert (not (= A B))) -(assert (= (card (intersection A B)) 1)) -(assert (= (card (setminus A B)) 2)) -(assert (= (card (setminus B A)) 2)) -(assert (not (member x A))) -(assert (not (member x B))) -(assert (= universe (as univset (Set (_ BitVec 3))))) +(assert (= (set.card (set.intersection A B)) 1)) +(assert (= (set.card (set.minus A B)) 2)) +(assert (= (set.card (set.minus B A)) 2)) +(assert (not (set.member x A))) +(assert (not (set.member x B))) +(assert (= universe (as set.universe (Set (_ BitVec 3))))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 index 4fc6b7347..2ccbc8a58 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 @@ -6,13 +6,13 @@ (declare-fun B () (Set (_ BitVec 3))) (declare-fun universe () (Set (_ BitVec 3))) (declare-fun x () (_ BitVec 3)) -(assert (= (card A) 5)) -(assert (= (card B) 5)) +(assert (= (set.card A) 5)) +(assert (= (set.card B) 5)) (assert (not (= A B))) -(assert (= (card (intersection A B)) 2)) -(assert (= (card (setminus A B)) 3)) -(assert (= (card (setminus B A)) 3)) -(assert (= universe (as univset (Set (_ BitVec 3))))) -(assert (not (member x A))) -(assert (not (member x B))) +(assert (= (set.card (set.intersection A B)) 2)) +(assert (= (set.card (set.minus A B)) 3)) +(assert (= (set.card (set.minus B A)) 3)) +(assert (= universe (as set.universe (Set (_ BitVec 3))))) +(assert (not (set.member x A))) +(assert (not (set.member x B))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 b/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 index ca8015622..c2d2e0724 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 @@ -5,10 +5,10 @@ (declare-datatype Color ((Red) (Green) (Blue) (Purple))) (declare-fun A () (Set Color)) (declare-fun B () (Set Color)) -(assert (> (card A) (card B) )) -(assert (member Red B)) +(assert (> (set.card A) (set.card B) )) +(assert (set.member Red B)) (declare-fun d () Color) (assert (not (= d Red))) -(assert (member d B)) -(assert (not (member Green A))) +(assert (set.member d B)) +(assert (not (set.member Green A))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-color.smt2 b/test/regress/regress1/sets/finite-type/sets-card-color.smt2 index 4fe3f0428..73db8105d 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-color.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-color.smt2 @@ -5,10 +5,10 @@ (declare-datatype Color ((Red) (Green) (Blue))) (declare-fun A () (Set Color)) (declare-fun B () (Set Color)) -(assert (> (card A) (card B) )) -(assert (member Red B)) +(assert (> (set.card A) (set.card B) )) +(assert (set.member Red B)) (declare-fun d () Color) (assert (not (= d Red))) -(assert (member d B)) -(assert (not (member Green A))) +(assert (set.member d B)) +(assert (not (set.member Green A))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 index 681033794..4c113c84b 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 @@ -7,8 +7,8 @@ (declare-fun B () (Set Rec)) (declare-fun universe () (Set Rec)) (declare-fun x () Rec) -(assert (= (card A) 5)) -(assert (= (card B) 5)) -(assert (= (card (intersection A B)) 1)) -(assert (= universe (as univset (Set Rec)))) +(assert (= (set.card A) 5)) +(assert (= (set.card B) 5)) +(assert (= (set.card (set.intersection A B)) 1)) +(assert (= universe (as set.universe (Set Rec)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 index eb45d9ef9..4c9bdadd5 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 @@ -6,8 +6,8 @@ (declare-fun A () (Set Rec)) (declare-fun B () (Set Rec)) (declare-fun universe () (Set Rec)) -(assert (= (card A) 9)) -(assert (= (card B) 9)) -(assert (= (card (intersection A B)) 1)) -(assert (= universe (as univset (Set Rec)))) +(assert (= (set.card A) 9)) +(assert (= (set.card B) 9)) +(assert (= (set.card (set.intersection A B)) 1)) +(assert (= universe (as set.universe (Set Rec)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 index b4bd97f1d..0999c6569 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 @@ -8,23 +8,23 @@ (declare-fun D () (Set (_ BitVec 2))) (declare-fun x () (_ BitVec 2)) -(assert (not (member x A))) -(assert (not (member x B))) -(assert (not (member x C))) -(assert (not (member x D))) +(assert (not (set.member x A))) +(assert (not (set.member x B))) +(assert (not (set.member x C))) +(assert (not (set.member x D))) (declare-fun y () (_ BitVec 2)) -(assert (not (member y A))) -(assert (not (member y B))) -(assert (not (member y C))) -(assert (not (member y D))) +(assert (not (set.member y A))) +(assert (not (set.member y B))) +(assert (not (set.member y C))) +(assert (not (set.member y D))) (declare-fun z () (_ BitVec 2)) -(assert (not (member z A))) -(assert (not (member z B))) -(assert (not (member z C))) -(assert (not (member z D))) +(assert (not (set.member z A))) +(assert (not (set.member z B))) +(assert (not (set.member z C))) +(assert (not (set.member z D))) (assert (distinct x y z)) -(assert (= (card (union A (union B (union C D)))) 2)) +(assert (= (set.card (set.union A (set.union B (set.union C D)))) 2)) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 index 88825a600..73781a91a 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 @@ -8,23 +8,23 @@ (declare-fun D () (Set (_ BitVec 3))) (declare-fun x () (_ BitVec 3)) -(assert (not (member x A))) -(assert (not (member x B))) -(assert (not (member x C))) -(assert (not (member x D))) +(assert (not (set.member x A))) +(assert (not (set.member x B))) +(assert (not (set.member x C))) +(assert (not (set.member x D))) (declare-fun y () (_ BitVec 3)) -(assert (not (member y A))) -(assert (not (member y B))) -(assert (not (member y C))) -(assert (not (member y D))) +(assert (not (set.member y A))) +(assert (not (set.member y B))) +(assert (not (set.member y C))) +(assert (not (set.member y D))) (declare-fun z () (_ BitVec 3)) -(assert (not (member z A))) -(assert (not (member z B))) -(assert (not (member z C))) -(assert (not (member z D))) +(assert (not (set.member z A))) +(assert (not (set.member z B))) +(assert (not (set.member z C))) +(assert (not (set.member z D))) (assert (distinct x y z)) -(assert (= (card (union A (union B (union C D)))) 6)) +(assert (= (set.card (set.union A (set.union B (set.union C D)))) 6)) (check-sat) diff --git a/test/regress/regress1/sets/fuzz14418.smt2 b/test/regress/regress1/sets/fuzz14418.smt2 index 9b65102a6..2fb60cb72 100644 --- a/test/regress/regress1/sets/fuzz14418.smt2 +++ b/test/regress/regress1/sets/fuzz14418.smt2 @@ -30,25 +30,25 @@ (let ((e10 (f0 v0))) (let ((e11 (* (- e5) e10))) (let ((e12 (ite (p0 e7 e6) 1 0))) -(let ((e13 (union v3 v4))) -(let ((e14 (setminus v2 v2))) +(let ((e13 (set.union v3 v4))) +(let ((e14 (set.minus v2 v2))) (let ((e15 (f1 v1 v4 v1))) (let ((e16 (f1 e14 v1 v4))) -(let ((e17 (intersection e16 e15))) +(let ((e17 (set.intersection e16 e15))) (let ((e18 (f1 v4 e15 v2))) -(let ((e19 (ite (p1 e13) (singleton 1) (singleton 0)))) -(let ((e20 (member v0 e17))) -(let ((e21 (member e7 e16))) -(let ((e22 (member e10 e16))) -(let ((e23 (member e8 e17))) -(let ((e24 (member e9 e14))) -(let ((e25 (member e8 e16))) -(let ((e26 (member v0 e13))) -(let ((e27 (member e12 v4))) -(let ((e28 (member e8 e14))) -(let ((e29 (member e8 v1))) -(let ((e30 (member e10 e13))) -(let ((e31 (member e7 e13))) +(let ((e19 (ite (p1 e13) (set.singleton 1) (set.singleton 0)))) +(let ((e20 (set.member v0 e17))) +(let ((e21 (set.member e7 e16))) +(let ((e22 (set.member e10 e16))) +(let ((e23 (set.member e8 e17))) +(let ((e24 (set.member e9 e14))) +(let ((e25 (set.member e8 e16))) +(let ((e26 (set.member v0 e13))) +(let ((e27 (set.member e12 v4))) +(let ((e28 (set.member e8 e14))) +(let ((e29 (set.member e8 v1))) +(let ((e30 (set.member e10 e13))) +(let ((e31 (set.member e7 e13))) (let ((e32 (f1 e13 e13 e13))) (let ((e33 (f1 e18 v4 e17))) (let ((e34 (f1 v2 v2 e15))) diff --git a/test/regress/regress1/sets/fuzz15201.smt2 b/test/regress/regress1/sets/fuzz15201.smt2 index f9dbaeb75..3094a8d84 100644 --- a/test/regress/regress1/sets/fuzz15201.smt2 +++ b/test/regress/regress1/sets/fuzz15201.smt2 @@ -1,5 +1,5 @@ ; symptom: unsat instead of sat -; issue/fix: buggy rewriter for setminus +; issue/fix: buggy rewriter for set.minus (set-info :source |fuzzsmt|) (set-info :smt-lib-version 2.6) (set-info :category "random") @@ -26,44 +26,44 @@ (let ((e13 (* e7 (- e3)))) (let ((e14 (f0 e7))) (let ((e15 (ite (p0 e9) 1 0))) -(let ((e16 (setminus v2 v1))) -(let ((e17 (setminus v1 v2))) -(let ((e18 (union e17 e17))) -(let ((e19 (intersection e17 v1))) -(let ((e20 (intersection e17 e18))) -(let ((e21 (intersection v1 e16))) -(let ((e22 (setminus e20 e16))) -(let ((e23 (ite (p1 v2 e18 e21) (singleton 1) (singleton 0)))) -(let ((e24 (setminus e17 e23))) -(let ((e25 (union v2 e22))) -(let ((e26 (union e24 e18))) -(let ((e27 (ite (p1 e20 e19 e25) (singleton 1) (singleton 0)))) +(let ((e16 (set.minus v2 v1))) +(let ((e17 (set.minus v1 v2))) +(let ((e18 (set.union e17 e17))) +(let ((e19 (set.intersection e17 v1))) +(let ((e20 (set.intersection e17 e18))) +(let ((e21 (set.intersection v1 e16))) +(let ((e22 (set.minus e20 e16))) +(let ((e23 (ite (p1 v2 e18 e21) (set.singleton 1) (set.singleton 0)))) +(let ((e24 (set.minus e17 e23))) +(let ((e25 (set.union v2 e22))) +(let ((e26 (set.union e24 e18))) +(let ((e27 (ite (p1 e20 e19 e25) (set.singleton 1) (set.singleton 0)))) (let ((e28 (f1 e20))) -(let ((e29 (member e14 e17))) -(let ((e30 (member e13 e23))) -(let ((e31 (member e11 e25))) -(let ((e32 (member e6 v1))) -(let ((e33 (member e9 v1))) -(let ((e34 (member v0 e28))) -(let ((e35 (member e9 e16))) -(let ((e36 (member e4 e17))) -(let ((e37 (member e9 e18))) -(let ((e38 (member e14 e25))) -(let ((e39 (member e14 v2))) -(let ((e40 (member v0 v1))) -(let ((e41 (member e4 e16))) -(let ((e42 (member e15 e21))) -(let ((e43 (member e7 e22))) -(let ((e44 (member e11 v2))) -(let ((e45 (member e14 e22))) -(let ((e46 (member e11 e16))) -(let ((e47 (member e15 e22))) -(let ((e48 (member e10 e23))) -(let ((e49 (member e4 e21))) -(let ((e50 (member e5 e28))) -(let ((e51 (member e6 e28))) -(let ((e52 (member v0 e22))) -(let ((e53 (member e14 e20))) +(let ((e29 (set.member e14 e17))) +(let ((e30 (set.member e13 e23))) +(let ((e31 (set.member e11 e25))) +(let ((e32 (set.member e6 v1))) +(let ((e33 (set.member e9 v1))) +(let ((e34 (set.member v0 e28))) +(let ((e35 (set.member e9 e16))) +(let ((e36 (set.member e4 e17))) +(let ((e37 (set.member e9 e18))) +(let ((e38 (set.member e14 e25))) +(let ((e39 (set.member e14 v2))) +(let ((e40 (set.member v0 v1))) +(let ((e41 (set.member e4 e16))) +(let ((e42 (set.member e15 e21))) +(let ((e43 (set.member e7 e22))) +(let ((e44 (set.member e11 v2))) +(let ((e45 (set.member e14 e22))) +(let ((e46 (set.member e11 e16))) +(let ((e47 (set.member e15 e22))) +(let ((e48 (set.member e10 e23))) +(let ((e49 (set.member e4 e21))) +(let ((e50 (set.member e5 e28))) +(let ((e51 (set.member e6 e28))) +(let ((e52 (set.member v0 e22))) +(let ((e53 (set.member e14 e20))) (let ((e54 (f1 e21))) (let ((e55 (f1 e28))) (let ((e56 (f1 e27))) diff --git a/test/regress/regress1/sets/fuzz31811.smt2 b/test/regress/regress1/sets/fuzz31811.smt2 index 9a7a7510a..e86901f9a 100644 --- a/test/regress/regress1/sets/fuzz31811.smt2 +++ b/test/regress/regress1/sets/fuzz31811.smt2 @@ -26,27 +26,27 @@ (let ((e8 (* e6 (- e5)))) (let ((e9 (ite (p0 e7 v0 e6) 1 0))) (let ((e10 (f0 v0 e8 e8))) -(let ((e11 (ite (p1 v1) (singleton 1) (singleton 0)))) -(let ((e12 (union v3 v3))) -(let ((e13 (intersection v3 v1))) -(let ((e14 (ite (p1 v3) (singleton 1) (singleton 0)))) -(let ((e15 (intersection v2 e14))) -(let ((e16 (ite (p1 e11) (singleton 1) (singleton 0)))) -(let ((e17 (ite (p1 v4) (singleton 1) (singleton 0)))) -(let ((e18 (union e15 v2))) -(let ((e19 (ite (p1 e16) (singleton 1) (singleton 0)))) -(let ((e20 (intersection e18 v3))) -(let ((e21 (setminus v4 e12))) -(let ((e22 (union v3 v2))) -(let ((e23 (setminus e12 v4))) -(let ((e24 (setminus v3 e16))) -(let ((e25 (intersection e19 e20))) -(let ((e26 (ite (p1 e15) (singleton 1) (singleton 0)))) -(let ((e27 (setminus e17 e15))) +(let ((e11 (ite (p1 v1) (set.singleton 1) (set.singleton 0)))) +(let ((e12 (set.union v3 v3))) +(let ((e13 (set.intersection v3 v1))) +(let ((e14 (ite (p1 v3) (set.singleton 1) (set.singleton 0)))) +(let ((e15 (set.intersection v2 e14))) +(let ((e16 (ite (p1 e11) (set.singleton 1) (set.singleton 0)))) +(let ((e17 (ite (p1 v4) (set.singleton 1) (set.singleton 0)))) +(let ((e18 (set.union e15 v2))) +(let ((e19 (ite (p1 e16) (set.singleton 1) (set.singleton 0)))) +(let ((e20 (set.intersection e18 v3))) +(let ((e21 (set.minus v4 e12))) +(let ((e22 (set.union v3 v2))) +(let ((e23 (set.minus e12 v4))) +(let ((e24 (set.minus v3 e16))) +(let ((e25 (set.intersection e19 e20))) +(let ((e26 (ite (p1 e15) (set.singleton 1) (set.singleton 0)))) +(let ((e27 (set.minus e17 e15))) (let ((e28 (f1 e23 e12))) -(let ((e29 (member e10 e16))) -(let ((e30 (member e10 v1))) -(let ((e31 (member e7 e19))) +(let ((e29 (set.member e10 e16))) +(let ((e30 (set.member e10 v1))) +(let ((e31 (set.member e7 e19))) (let ((e32 (f1 e12 e12))) (let ((e33 (f1 e16 e25))) (let ((e34 (f1 v1 e27))) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 index ee697065f..f6d032f11 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 @@ -4,9 +4,9 @@ (declare-const universe (Set (Array Int Int))) (declare-const A (Set (Array Int Int))) (declare-const B (Set (Array Int Int))) -(assert (= (card universe) 3)) -(assert (= (card A) 2)) -(assert (= (card B) 2)) -(assert (= (intersection A B) (as emptyset (Set (Array Int Int))))) -(assert (= universe (as univset (Set (Array Int Int))))) +(assert (= (set.card universe) 3)) +(assert (= (set.card A) 2)) +(assert (= (set.card B) 2)) +(assert (= (set.intersection A B) (as set.empty (Set (Array Int Int))))) +(assert (= universe (as set.universe (Set (Array Int Int))))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 index fe8ce9142..d7e6a758c 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 @@ -4,9 +4,9 @@ (declare-const universe (Set (Array Int Int))) (declare-const A (Set (Array Int Int))) (declare-const B (Set (Array Int Int))) -(assert (= (card universe) 3)) -(assert (= (card A) 1)) -(assert (= (card B) 2)) -(assert (= (intersection A B) (as emptyset (Set (Array Int Int))))) -(assert (= universe (as univset (Set (Array Int Int))))) +(assert (= (set.card universe) 3)) +(assert (= (set.card A) 1)) +(assert (= (set.card B) 2)) +(assert (= (set.intersection A B) (as set.empty (Set (Array Int Int))))) +(assert (= universe (as set.universe (Set (Array Int Int))))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 index 573ff56da..c649c9be2 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 @@ -1,12 +1,12 @@ (set-logic QF_ALL) (set-option :sets-ext true) (set-info :status unsat) -(assert (= (card (as univset (Set Int))) 10)) +(assert (= (set.card (as set.universe (Set Int))) 10)) (declare-const universe (Set Int)) (declare-const A (Set Int)) (declare-const B (Set Int)) -(assert (= (card A) 6)) -(assert (= (card B) 5)) -(assert (= (intersection A B) (as emptyset (Set Int)))) -(assert (= universe (as univset (Set Int)))) +(assert (= (set.card A) 6)) +(assert (= (set.card B) 5)) +(assert (= (set.intersection A B) (as set.empty (Set Int)))) +(assert (= universe (as set.universe (Set Int)))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 index 9d8fee7c3..b3958e79e 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 @@ -1,12 +1,12 @@ (set-logic QF_ALL) (set-option :sets-ext true) (set-info :status sat) -(assert (= (card (as univset (Set Int))) 10)) +(assert (= (set.card (as set.universe (Set Int))) 10)) (declare-const universe (Set Int)) (declare-const A (Set Int)) (declare-const B (Set Int)) -(assert (= (card A) 5)) -(assert (= (card B) 5)) -(assert (= (intersection A B) (as emptyset (Set Int)))) -(assert (= universe (as univset (Set Int)))) +(assert (= (set.card A) 5)) +(assert (= (set.card B) 5)) +(assert (= (set.intersection A B) (as set.empty (Set Int)))) +(assert (= universe (as set.universe (Set Int)))) (check-sat) diff --git a/test/regress/regress1/sets/insert_invariant_37_2.smt2 b/test/regress/regress1/sets/insert_invariant_37_2.smt2 index 2ef07f920..cac805531 100644 --- a/test/regress/regress1/sets/insert_invariant_37_2.smt2 +++ b/test/regress/regress1/sets/insert_invariant_37_2.smt2 @@ -61,13 +61,13 @@ (assert (! (forall ((l1 Loc) (l2 Loc)) (or (not Axiom$0) (or (= l1 l2) (< (read$0 data$0 l1) (read$0 data$0 l2)) - (not (Btwn$0 next$0 l1 l2 null$0)) (not (member l1 sk_?X$0)) - (not (member l2 sk_?X$0))))) + (not (Btwn$0 next$0 l1 l2 null$0)) (not (set.member l1 sk_?X$0)) + (not (set.member l2 sk_?X$0))))) :named strict_sortedness)) (assert (! (forall ((l1 Loc)) (or (= l1 null$0) - (member (read$0 data$0 l1) + (set.member (read$0 data$0 l1) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) (not (Btwn$0 next$0 lst$0 l1 null$0)))) :named sorted_set_1)) @@ -78,7 +78,7 @@ (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (member (read$0 data$0 curr_2$0) + (set.member (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -86,12 +86,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) (not - (member (read$0 data$0 curr_2$0) + (set.member (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) :named sorted_set_2)) @@ -101,7 +101,7 @@ (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (member (read$0 data$0 prev_2$0) + (set.member (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -109,12 +109,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) (not - (member (read$0 data$0 prev_2$0) + (set.member (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) :named sorted_set_2_1)) @@ -124,7 +124,7 @@ (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (member (read$0 data$0 sk_l1$0) + (set.member (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -132,12 +132,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) (not - (member (read$0 data$0 sk_l1$0) + (set.member (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) :named sorted_set_2_2)) @@ -147,7 +147,7 @@ (witness$0 (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (member (read$0 data$0 sk_l1_1$0) + (set.member (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -155,12 +155,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) (not - (member (read$0 data$0 sk_l1_1$0) + (set.member (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) :named sorted_set_2_3)) @@ -170,7 +170,7 @@ (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (member (read$0 data$0 sk_l2$0) + (set.member (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -178,12 +178,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) (not - (member (read$0 data$0 sk_l2$0) + (set.member (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) :named sorted_set_2_4)) @@ -193,7 +193,7 @@ (witness$0 (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (member (read$0 data$0 sk_l2_1$0) + (set.member (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -201,12 +201,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) (not - (member (read$0 data$0 sk_l2_1$0) + (set.member (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) :named sorted_set_2_5)) @@ -215,18 +215,18 @@ (= (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (set.member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and (= sk_?e$0 (read$0 data$0 (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member + (set.member (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)) (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) - (not (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) + (not (set.member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) :named sorted_set_2_6)) (assert (! (and @@ -235,30 +235,30 @@ (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (set.member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and (= sk_?e_3$0 (read$0 data$0 (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member + (set.member (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)) (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) - (not (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) + (not (set.member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) :named sorted_set_2_7)) (assert (! (forall ((l1 Loc)) (or (= l1 null$0) - (member (read$0 data$0 l1) + (set.member (read$0 data$0 l1) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) (not (Btwn$0 next$0 curr_2$0 l1 null$0)))) :named sorted_set_1_1)) (assert (! (forall ((l1 Loc)) (or (= l1 curr_2$0) - (member (read$0 data$0 l1) + (set.member (read$0 data$0 l1) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) (not (Btwn$0 next$0 lst$0 l1 curr_2$0)))) :named sorted_set_1_2)) @@ -269,7 +269,7 @@ (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (member (read$0 data$0 curr_2$0) + (set.member (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and @@ -277,12 +277,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) (not - (member (read$0 data$0 curr_2$0) + (set.member (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) :named sorted_set_2_8)) @@ -292,7 +292,7 @@ (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (member (read$0 data$0 prev_2$0) + (set.member (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and @@ -300,12 +300,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) (not - (member (read$0 data$0 prev_2$0) + (set.member (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) :named sorted_set_2_9)) @@ -315,7 +315,7 @@ (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (member (read$0 data$0 sk_l1$0) + (set.member (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and @@ -323,12 +323,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) (not - (member (read$0 data$0 sk_l1$0) + (set.member (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) :named sorted_set_2_10)) @@ -338,7 +338,7 @@ (witness$0 (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (member (read$0 data$0 sk_l1_1$0) + (set.member (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and @@ -346,12 +346,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) (not - (member (read$0 data$0 sk_l1_1$0) + (set.member (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) :named sorted_set_2_11)) @@ -361,7 +361,7 @@ (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (member (read$0 data$0 sk_l2$0) + (set.member (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and @@ -369,12 +369,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) (not - (member (read$0 data$0 sk_l2$0) + (set.member (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) :named sorted_set_2_12)) @@ -384,7 +384,7 @@ (witness$0 (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (member (read$0 data$0 sk_l2_1$0) + (set.member (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and @@ -392,12 +392,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) (not - (member (read$0 data$0 sk_l2_1$0) + (set.member (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) :named sorted_set_2_13)) @@ -407,18 +407,18 @@ (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (set.member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and (= sk_?e$0 (read$0 data$0 (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member + (set.member (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) - (not (member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) + (not (set.member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) :named sorted_set_2_14)) (assert (! (and @@ -427,19 +427,19 @@ (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (set.member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and (= sk_?e_3$0 (read$0 data$0 (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member + (set.member (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) (not - (member sk_?e_3$0 + (set.member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) :named sorted_set_2_15)) @@ -449,7 +449,7 @@ (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (member (read$0 data$0 curr_2$0) + (set.member (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and @@ -457,12 +457,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member + (set.member (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) (not - (member (read$0 data$0 curr_2$0) + (set.member (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) :named sorted_set_2_16)) @@ -472,7 +472,7 @@ (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (member (read$0 data$0 prev_2$0) + (set.member (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and @@ -480,12 +480,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member + (set.member (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) (not - (member (read$0 data$0 prev_2$0) + (set.member (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) :named sorted_set_2_17)) @@ -495,7 +495,7 @@ (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (member (read$0 data$0 sk_l1$0) + (set.member (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and @@ -503,12 +503,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) (not - (member (read$0 data$0 sk_l1$0) + (set.member (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) :named sorted_set_2_18)) @@ -518,7 +518,7 @@ (witness$0 (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (member (read$0 data$0 sk_l1_1$0) + (set.member (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and @@ -526,12 +526,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) (not - (member (read$0 data$0 sk_l1_1$0) + (set.member (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) :named sorted_set_2_19)) @@ -541,7 +541,7 @@ (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (member (read$0 data$0 sk_l2$0) + (set.member (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and @@ -549,12 +549,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) (not - (member (read$0 data$0 sk_l2$0) + (set.member (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) :named sorted_set_2_20)) @@ -564,7 +564,7 @@ (witness$0 (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (member (read$0 data$0 sk_l2_1$0) + (set.member (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and @@ -572,12 +572,12 @@ (read$0 data$0 (witness$0 (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member + (set.member (witness$0 (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) (not - (member (read$0 data$0 sk_l2_1$0) + (set.member (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) :named sorted_set_2_21)) @@ -587,18 +587,18 @@ (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (set.member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and (= sk_?e$0 (read$0 data$0 (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member + (set.member (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) - (not (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + (not (set.member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) :named sorted_set_2_22)) (assert (! (and @@ -607,19 +607,19 @@ (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (set.member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and (= sk_?e_3$0 (read$0 data$0 (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member + (set.member (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) (not - (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + (set.member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) :named sorted_set_2_23)) (assert (! (= (read$1 next$0 null$0) null$0) :named read_null)) @@ -627,26 +627,26 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst$0 l1 null$0) - (member l1 (sorted_set_domain$0 data$0 next$0 lst$0 null$0)) + (set.member l1 (sorted_set_domain$0 data$0 next$0 lst$0 null$0)) (not (= l1 null$0))) (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0))) (not - (member l1 + (set.member l1 (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))))) :named sorted_set_footprint)) -(assert (! (or (member sk_?e_3$0 c2_2$0) - (and (member sk_?e_2$0 sk_FP_1$0) (not (member sk_?e_2$0 FP$0))) - (and (member sk_?e_3$0 (union c1_2$0 c2_2$0)) - (not (member sk_?e_3$0 content$0))) - (and (member sk_?e_3$0 c1_2$0) +(assert (! (or (set.member sk_?e_3$0 c2_2$0) + (and (set.member sk_?e_2$0 sk_FP_1$0) (not (set.member sk_?e_2$0 FP$0))) + (and (set.member sk_?e_3$0 (set.union c1_2$0 c2_2$0)) + (not (set.member sk_?e_3$0 content$0))) + (and (set.member sk_?e_3$0 c1_2$0) (not - (member sk_?e_3$0 + (set.member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (and (member sk_?e_3$0 content$0) - (not (member sk_?e_3$0 (union c1_2$0 c2_2$0)))) - (and (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (not (member sk_?e_3$0 c1_2$0))) + (and (set.member sk_?e_3$0 content$0) + (not (set.member sk_?e_3$0 (set.union c1_2$0 c2_2$0)))) + (and (set.member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (not (set.member sk_?e_3$0 c1_2$0))) (and (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0)) (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0)))) (not (= curr_2$0 lst$0)) (not (= prev_2$0 null$0)) @@ -663,14 +663,14 @@ (assert (! (= sk_?X_3$0 (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)) :named invariant_37_2_3)) -(assert (! (= sk_?X_1$0 (union sk_?X_3$0 sk_?X_4$0)) :named invariant_37_2_4)) +(assert (! (= sk_?X_1$0 (set.union sk_?X_3$0 sk_?X_4$0)) :named invariant_37_2_4)) -(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) +(assert (! (= FP_Caller$0 (set.union FP$0 FP_Caller$0)) :named precondition_of_insert_27_11)) (assert (! (= sk_?X$0 FP$0) :named precondition_of_insert_27_11_1)) -(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) +(assert (! (= Alloc$0 (set.union FP_Caller$0 Alloc$0)) :named initial_footprint_of_insert_27_11)) (assert (! (= curr_2$0 lst$0) :named assign_31_2)) @@ -685,8 +685,8 @@ (assert (! (or (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0 c1_2$0) (not (Btwn$0 next$0 curr_2$0 null$0 null$0)) - (! (and (Btwn$0 next$0 sk_l1$0 sk_l2$0 null$0) (member sk_l1$0 sk_?X_3$0) - (member sk_l2$0 sk_?X_3$0) (not (= sk_l1$0 sk_l2$0)) + (! (and (Btwn$0 next$0 sk_l1$0 sk_l2$0 null$0) (set.member sk_l1$0 sk_?X_3$0) + (set.member sk_l2$0 sk_?X_3$0) (not (= sk_l1$0 sk_l2$0)) (not (< (read$0 data$0 sk_l1$0) (read$0 data$0 sk_l2$0)))) :named strict_sortedness_1)) :named unnamed_1)) @@ -694,47 +694,47 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst$0 l1 curr_2$0) - (member l1 + (set.member l1 (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)) (not (= l1 curr_2$0))) (and (or (= l1 curr_2$0) (not (Btwn$0 next$0 lst$0 l1 curr_2$0))) (not - (member l1 + (set.member l1 (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))))) :named sorted_set_footprint_1)) (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 curr_2$0 l1 null$0) - (member l1 + (set.member l1 (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)) (not (= l1 null$0))) (and (or (= l1 null$0) (not (Btwn$0 next$0 curr_2$0 l1 null$0))) (not - (member l1 + (set.member l1 (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))))) :named sorted_set_footprint_2)) -(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1)) +(assert (! (not (set.member null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1)) (assert (! (or (= prev_2$0 curr_2$0) - (member sk_?e_1$0 (intersection sk_?X_4$0 sk_?X_3$0)) - (and (member sk_?e_1$0 sk_FP$0) (not (member sk_?e_1$0 FP$0))) - (and (member sk_?e$0 (union c1_2$0 c2_2$0)) (not (member sk_?e$0 content$0))) - (and (member sk_?e$0 c1_2$0) - (not (member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (and (member sk_?e$0 c2_2$0) - (not (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (and (member sk_?e$0 content$0) (not (member sk_?e$0 (union c1_2$0 c2_2$0)))) - (and (member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (not (member sk_?e$0 c1_2$0))) - (and (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (not (member sk_?e$0 c2_2$0))) + (set.member sk_?e_1$0 (set.intersection sk_?X_4$0 sk_?X_3$0)) + (and (set.member sk_?e_1$0 sk_FP$0) (not (set.member sk_?e_1$0 FP$0))) + (and (set.member sk_?e$0 (set.union c1_2$0 c2_2$0)) (not (set.member sk_?e$0 content$0))) + (and (set.member sk_?e$0 c1_2$0) + (not (set.member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) + (and (set.member sk_?e$0 c2_2$0) + (not (set.member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) + (and (set.member sk_?e$0 content$0) (not (set.member sk_?e$0 (set.union c1_2$0 c2_2$0)))) + (and (set.member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) + (not (set.member sk_?e$0 c1_2$0))) + (and (set.member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) + (not (set.member sk_?e$0 c2_2$0))) (and (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0)) (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0)))) (not (= (read$1 next$0 prev_2$0) curr_2$0)) @@ -765,14 +765,14 @@ (assert (! (= prev_2$0 null$0) :named assign_32_2)) -(assert (! (= c2_2$0 (as emptyset SetInt)) :named assign_35_2)) +(assert (! (= c2_2$0 (as set.empty SetInt)) :named assign_35_2)) -(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_29_0)) +(assert (! (= FP_Caller_1$0 (set.minus FP_Caller$0 FP$0)) :named assign_29_0)) (assert (! (or (sorted_set_struct$0 sk_?X_5$0 data$0 next$0 lst$0 curr_2$0 c2_2$0) (not (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0)) (! (and (Btwn$0 next$0 sk_l1_1$0 sk_l2_1$0 curr_2$0) - (member sk_l1_1$0 sk_?X_5$0) (member sk_l2_1$0 sk_?X_5$0) + (set.member sk_l1_1$0 sk_?X_5$0) (set.member sk_l2_1$0 sk_?X_5$0) (not (= sk_l1_1$0 sk_l2_1$0)) (not (< (read$0 data$0 sk_l1_1$0) (read$0 data$0 sk_l2_1$0)))) :named strict_sortedness_2)) diff --git a/test/regress/regress1/sets/is_singleton1.smt2 b/test/regress/regress1/sets/is_singleton1.smt2 index a6f1961cd..b641e8ef9 100644 --- a/test/regress/regress1/sets/is_singleton1.smt2 +++ b/test/regress/regress1/sets/is_singleton1.smt2 @@ -4,8 +4,8 @@ (set-info :status sat) (declare-fun S () (Set Int)) (declare-fun x () Int) -(assert (= (choose (singleton x)) 5)) -(assert (= (singleton x) S)) -(assert (is_singleton S)) -(assert (is_singleton (singleton 3))) +(assert (= (set.choose (set.singleton x)) 5)) +(assert (= (set.singleton x) S)) +(assert (set.is_singleton S)) +(assert (set.is_singleton (set.singleton 3))) (check-sat) diff --git a/test/regress/regress1/sets/issue2568.smt2 b/test/regress/regress1/sets/issue2568.smt2 index 17a05c876..80bcf1619 100644 --- a/test/regress/regress1/sets/issue2568.smt2 +++ b/test/regress/regress1/sets/issue2568.smt2 @@ -10,7 +10,7 @@ (declare-fun s () (Set Int)) (declare-fun u () Unit) -(assert (= s (insert y s))) +(assert (= s (set.insert y s))) (assert (=> b (= uu u))) (push 1) diff --git a/test/regress/regress1/sets/issue2904.smt2 b/test/regress/regress1/sets/issue2904.smt2 index 49268953d..c39ea09ba 100644 --- a/test/regress/regress1/sets/issue2904.smt2 +++ b/test/regress/regress1/sets/issue2904.smt2 @@ -9,18 +9,18 @@ (declare-fun b () (Set Int)) (declare-fun c () (Set Int)) (declare-fun UNIVERALSET () (Set Int)) -(assert (subset b UNIVERALSET)) -(assert (subset c UNIVERALSET)) +(assert (set.subset b UNIVERALSET)) +(assert (set.subset c UNIVERALSET)) (assert (> n 0)) -(assert (= (card UNIVERALSET) n)) -(assert (= (card b) m)) -(assert (= (card c) (- f m))) +(assert (= (set.card UNIVERALSET) n)) +(assert (= (set.card b) m)) +(assert (= (set.card c) (- f m))) (assert (>= m 0)) (assert (>= f m)) (assert (> n (+ (* 2 f) m))) -(assert (>= (card (setminus UNIVERALSET (intersection (setminus UNIVERALSET b) (setminus UNIVERALSET c)))) n)) +(assert (>= (set.card (set.minus UNIVERALSET (set.intersection (set.minus UNIVERALSET b) (set.minus UNIVERALSET c)))) n)) (check-sat) diff --git a/test/regress/regress1/sets/issue4124-need-check.smt2 b/test/regress/regress1/sets/issue4124-need-check.smt2 index 46507df2a..c06a753e1 100644 --- a/test/regress/regress1/sets/issue4124-need-check.smt2 +++ b/test/regress/regress1/sets/issue4124-need-check.smt2 @@ -6,8 +6,8 @@ (declare-fun d () (Set (Tuple String String))) (declare-fun f () (Set Int)) (declare-fun e () Int) -(assert (= b (insert (tuple "" 1) (tuple "" 2) (singleton (tuple "" 4))))) -(assert (= c (insert (tuple 1 "1") (tuple 2 "2") (singleton (tuple 7 ""))))) -(assert (= d (join b c))) -(assert (= e (card f))) +(assert (= b (set.insert (tuple "" 1) (tuple "" 2) (set.singleton (tuple "" 4))))) +(assert (= c (set.insert (tuple 1 "1") (tuple 2 "2") (set.singleton (tuple 7 ""))))) +(assert (= d (rel.join b c))) +(assert (= e (set.card f))) (check-sat) diff --git a/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 b/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 index aa7349261..fd3bd62eb 100644 --- a/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 +++ b/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 @@ -2,6 +2,6 @@ (set-info :status unsat) (declare-fun st1 () (Set Int)) (declare-fun st7 () (Set Int)) -(assert (> 0 (card (intersection st1 (union st7 st1))))) -(assert (subset st1 st7)) +(assert (> 0 (set.card (set.intersection st1 (set.union st7 st1))))) +(assert (set.subset st1 st7)) (check-sat) diff --git a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 index 95425709d..bc2f103d2 100644 --- a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 +++ b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 @@ -2,7 +2,7 @@ (set-info :status unsat) (declare-fun st3 () (Set String)) (declare-fun st9 () (Set String)) -(assert (is_singleton (intersection st3 st9))) -(assert (< 1 (card (intersection st3 st9)))) -(assert (is_singleton st9)) +(assert (set.is_singleton (set.intersection st3 st9))) +(assert (< 1 (set.card (set.intersection st3 st9)))) +(assert (set.is_singleton st9)) (check-sat) diff --git a/test/regress/regress1/sets/issue4391-card-lasso.smt2 b/test/regress/regress1/sets/issue4391-card-lasso.smt2 index a8a0cb62d..f7a720436 100644 --- a/test/regress/regress1/sets/issue4391-card-lasso.smt2 +++ b/test/regress/regress1/sets/issue4391-card-lasso.smt2 @@ -7,10 +7,10 @@ (declare-fun c () (Set Int)) (declare-fun e () (Set Int)) -(assert (= e (union b e))) -(assert (= (card b) d)) -(assert (= (card c) 0)) +(assert (= e (set.union b e))) +(assert (= (set.card b) d)) +(assert (= (set.card c) 0)) (assert (= 0 (mod 0 d))) -(assert (> (card (setminus e (intersection (intersection e b) (setminus e c)))) 1)) +(assert (> (set.card (set.minus e (set.intersection (set.intersection e b) (set.minus e c)))) 1)) (check-sat) diff --git a/test/regress/regress1/sets/issue5271.smt2 b/test/regress/regress1/sets/issue5271.smt2 index 3c64e1d30..b8f4f3e85 100644 --- a/test/regress/regress1/sets/issue5271.smt2 +++ b/test/regress/regress1/sets/issue5271.smt2 @@ -3,6 +3,6 @@ (set-logic ALL) (set-info :status sat) (declare-fun s () (Set Int)) -(assert (> (card s) 1)) -(assert (and (member 0 s) (exists ((x Int)) (member (mod x 1) s)))) +(assert (> (set.card s) 1)) +(assert (and (set.member 0 s) (exists ((x Int)) (set.member (mod x 1) s)))) (check-sat) diff --git a/test/regress/regress1/sets/issue5309.smt2 b/test/regress/regress1/sets/issue5309.smt2 index 383b1263e..f9f8efbc9 100644 --- a/test/regress/regress1/sets/issue5309.smt2 +++ b/test/regress/regress1/sets/issue5309.smt2 @@ -2,6 +2,6 @@ (set-info :status sat) (declare-const zero Int) (declare-fun A () (Set Int)) -(assert (exists ((x Int)) (= A (singleton x)))) -(assert (member (- zero) A)) +(assert (exists ((x Int)) (= A (set.singleton x)))) +(assert (set.member (- zero) A)) (check-sat) diff --git a/test/regress/regress1/sets/issue5342.smt2 b/test/regress/regress1/sets/issue5342.smt2 index e5e7ed65d..1b4943535 100644 --- a/test/regress/regress1/sets/issue5342.smt2 +++ b/test/regress/regress1/sets/issue5342.smt2 @@ -2,6 +2,6 @@ (set-logic ALL) (set-info :status unsat) (declare-fun S () (Set Int)) -(assert (is_singleton (complement (complement S)))) -(assert (= 2 (card S))) +(assert (set.is_singleton (set.complement (set.complement S)))) +(assert (= 2 (set.card S))) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/sets/issue5342_difference_version.smt2 b/test/regress/regress1/sets/issue5342_difference_version.smt2 index 143ac56c2..31b28824c 100644 --- a/test/regress/regress1/sets/issue5342_difference_version.smt2 +++ b/test/regress/regress1/sets/issue5342_difference_version.smt2 @@ -2,6 +2,6 @@ (set-logic ALL) (set-info :status unsat) (declare-fun S () (Set Int)) -(assert (is_singleton (setminus (as univset (Set Int)) (setminus (as univset (Set Int)) S)))) -(assert (= 2 (card S))) +(assert (set.is_singleton (set.minus (as set.universe (Set Int)) (set.minus (as set.universe (Set Int)) S)))) +(assert (= 2 (set.card S))) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/sets/issue5705-cg-subtyping.smt2 b/test/regress/regress1/sets/issue5705-cg-subtyping.smt2 index df5b2246c..27d014e53 100644 --- a/test/regress/regress1/sets/issue5705-cg-subtyping.smt2 +++ b/test/regress/regress1/sets/issue5705-cg-subtyping.smt2 @@ -2,6 +2,6 @@ (set-info :status sat) (declare-fun s () (Set Real)) (declare-fun t3 () (Set Real)) -(assert (or (member 1.0 t3) (member 0.0 s))) -(assert (not (= t3 (setminus s (singleton 1.0))))) +(assert (or (set.member 1.0 t3) (set.member 0.0 s))) +(assert (not (= t3 (set.minus s (set.singleton 1.0))))) (check-sat) diff --git a/test/regress/regress1/sets/issue5942-witness.smt2 b/test/regress/regress1/sets/issue5942-witness.smt2 index 901f60edb..efe02117f 100644 --- a/test/regress/regress1/sets/issue5942-witness.smt2 +++ b/test/regress/regress1/sets/issue5942-witness.smt2 @@ -5,5 +5,5 @@ (declare-fun r1 () Real) (declare-fun st9 () (Set String)) (declare-fun str2 () String) -(assert (is_singleton (ite (= str2 (str.substr str2 0 (to_int r1))) st9 (as emptyset (Set String))))) +(assert (set.is_singleton (ite (= str2 (str.substr str2 0 (to_int r1))) st9 (as set.empty (Set String))))) (check-sat) diff --git a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 index be1e36a97..ae71a1edb 100644 --- a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 +++ b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 @@ -1,7 +1,7 @@ ; EXPECT: sat ; Observed behavior: -; --check-model failed for set-term (union (z3f69 z3v151) (singleton z3v143)) +; --check-model failed for set-term (set.union (z3f69 z3v151) (set.singleton z3v143)) ; with different set of elements in the model for representative and the node ; itself. ; @@ -23,15 +23,15 @@ (set-info :status sat) (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 z3v58 () Int) (declare-fun z3v59 () Int) @@ -69,16 +69,16 @@ (z3f69 z3v140)))) (assert (= (z3f69 z3v152) - (smt_set_cup (singleton z3v143) (z3f69 z3v151)))) + (smt_set_cup (set.singleton z3v143) (z3f69 z3v151)))) (assert (= (z3f70 z3v152) - (smt_set_cup (singleton z3v143) (z3f70 z3v151)))) + (smt_set_cup (set.singleton z3v143) (z3f70 z3v151)))) (assert (and (= (z3f69 z3v142) - (smt_set_cup (singleton z3v143) (z3f69 z3v141))) + (smt_set_cup (set.singleton z3v143) (z3f69 z3v141))) (= (z3f70 z3v142) - (smt_set_cup (singleton z3v143) (z3f70 z3v141))) + (smt_set_cup (set.singleton z3v143) (z3f70 z3v141))) (= z3v142 (z3f92 z3v143 z3v141)) (= z3v142 z3v144) (= (z3f62 z3v61) z3v61) diff --git a/test/regress/regress1/sets/remove_check_free_31_6.smt2 b/test/regress/regress1/sets/remove_check_free_31_6.smt2 index 2bf2d4c62..c2ff1da23 100644 --- a/test/regress/regress1/sets/remove_check_free_31_6.smt2 +++ b/test/regress/regress1/sets/remove_check_free_31_6.smt2 @@ -76,22 +76,22 @@ :named btwn_step_10)) (assert (! (forall ((?f FldLoc)) - (or (member (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0) + (or (set.member (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0) (= null$0 (ep$0 ?f sk_?X_30$0 null$0)))) :named entry-point3_10)) (assert (! (forall ((?f FldLoc)) - (or (member (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0) + (or (set.member (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0) (= lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0)))) :named entry-point3_11)) (assert (! (forall ((?f FldLoc)) - (or (member (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0) + (or (set.member (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0) (= curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0)))) :named entry-point3_12)) (assert (! (forall ((?f FldLoc)) - (or (member (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0) + (or (set.member (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0) (= tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0)))) :named entry-point3_13)) @@ -117,42 +117,42 @@ (assert (! (forall ((?f FldLoc) (?y Loc)) (or (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0) ?y) - (not (Btwn$0 ?f null$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) + (not (Btwn$0 ?f null$0 ?y ?y)) (not (set.member ?y sk_?X_30$0)))) :named entry-point4_10)) (assert (! (forall ((?f FldLoc) (?y Loc)) (or (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0) ?y) - (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) + (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (set.member ?y sk_?X_30$0)))) :named entry-point4_11)) (assert (! (forall ((?f FldLoc) (?y Loc)) (or (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0) ?y) - (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) + (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (set.member ?y sk_?X_30$0)))) :named entry-point4_12)) (assert (! (forall ((?f FldLoc) (?y Loc)) (or (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0) ?y) - (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) + (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (set.member ?y sk_?X_30$0)))) :named entry-point4_13)) (assert (! (forall ((?f FldLoc) (?y Loc)) - (or (not (Btwn$0 ?f null$0 ?y ?y)) (not (member ?y sk_?X_30$0)) - (member (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0))) + (or (not (Btwn$0 ?f null$0 ?y ?y)) (not (set.member ?y sk_?X_30$0)) + (set.member (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0))) :named entry-point2_10)) (assert (! (forall ((?f FldLoc) (?y Loc)) - (or (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (member ?y sk_?X_30$0)) - (member (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0))) + (or (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (set.member ?y sk_?X_30$0)) + (set.member (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0))) :named entry-point2_11)) (assert (! (forall ((?f FldLoc) (?y Loc)) - (or (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (member ?y sk_?X_30$0)) - (member (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0))) + (or (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (set.member ?y sk_?X_30$0)) + (set.member (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0))) :named entry-point2_12)) (assert (! (forall ((?f FldLoc) (?y Loc)) - (or (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (member ?y sk_?X_30$0)) - (member (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0))) + (or (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (set.member ?y sk_?X_30$0)) + (set.member (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0))) :named entry-point2_13)) (assert (! (= (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0) @@ -181,59 +181,59 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst$0 l1 curr_2$0) - (member l1 (lseg_domain$0 next$0 lst$0 curr_2$0)) + (set.member l1 (lseg_domain$0 next$0 lst$0 curr_2$0)) (not (= l1 curr_2$0))) (and (or (= l1 curr_2$0) (not (Btwn$0 next$0 lst$0 l1 curr_2$0))) - (not (member l1 (lseg_domain$0 next$0 lst$0 curr_2$0)))))) + (not (set.member l1 (lseg_domain$0 next$0 lst$0 curr_2$0)))))) :named lseg_footprint_20)) (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 curr_3$0 l1 null$0) - (member l1 (lseg_domain$0 next$0 curr_3$0 null$0)) + (set.member l1 (lseg_domain$0 next$0 curr_3$0 null$0)) (not (= l1 null$0))) (and (or (= l1 null$0) (not (Btwn$0 next$0 curr_3$0 l1 null$0))) - (not (member l1 (lseg_domain$0 next$0 curr_3$0 null$0)))))) + (not (set.member l1 (lseg_domain$0 next$0 curr_3$0 null$0)))))) :named lseg_footprint_21)) -(assert (! (not (member tmp_2$0 FP_2$0)) :named check_free_31_6)) +(assert (! (not (set.member tmp_2$0 FP_2$0)) :named check_free_31_6)) -(assert (! (not (member null$0 Alloc$0)) :named framecondition_of_remove_loop_18_4_15)) +(assert (! (not (set.member null$0 Alloc$0)) :named framecondition_of_remove_loop_18_4_15)) (assert (! (not (= lst$0 null$0)) :named if_else_13_6_4)) -(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) +(assert (! (= FP_Caller$0 (set.union FP$0 FP_Caller$0)) :named precondition_of_remove_10_11_20)) (assert (! (= sk_?X_33$0 FP$0) :named precondition_of_remove_10_11_21)) (assert (! (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0) :named invariant_18_4_62)) -(assert (! (= FP$0 (union FP_1$0 FP$0)) :named invariant_18_4_63)) +(assert (! (= FP$0 (set.union FP_1$0 FP$0)) :named invariant_18_4_63)) (assert (! (= sk_?X_31$0 (lseg_domain$0 next$0 curr_2$0 null$0)) :named invariant_18_4_64)) -(assert (! (= sk_?X_30$0 (union sk_?X_31$0 sk_?X_32$0)) :named invariant_18_4_65)) +(assert (! (= sk_?X_30$0 (set.union sk_?X_31$0 sk_?X_32$0)) :named invariant_18_4_65)) -(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_66)) +(assert (! (= (as set.empty SetLoc) (as set.empty SetLoc)) :named invariant_18_4_66)) (assert (! (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0) :named invariant_18_4_67)) -(assert (! (= sk_?X_29$0 (union sk_?X_28$0 sk_?X_27$0)) :named invariant_18_4_68)) +(assert (! (= sk_?X_29$0 (set.union sk_?X_28$0 sk_?X_27$0)) :named invariant_18_4_68)) (assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0)) :named invariant_18_4_69)) -(assert (! (= (as emptyset SetLoc) (intersection sk_?X_27$0 sk_?X_28$0)) +(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_27$0 sk_?X_28$0)) :named invariant_18_4_70)) -(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) +(assert (! (= Alloc$0 (set.union FP_Caller$0 Alloc$0)) :named initial_footprint_of_remove_10_11_10)) (assert (! (Frame$0 FP_1$0 Alloc$0 next$0 next$0) @@ -245,8 +245,8 @@ (assert (! (= curr_2$0 lst$0) :named assign_17_4_4)) (assert (! (= FP_2$0 - (union (setminus FP$0 FP_1$0) - (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0)))) + (set.union (set.minus FP$0 FP_1$0) + (set.union (set.intersection Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0)))) :named framecondition_of_remove_loop_18_4_17)) (assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0) @@ -263,35 +263,35 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst_1$0 l1 curr_3$0) - (member l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) + (set.member l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) (not (= l1 curr_3$0))) (and (or (= l1 curr_3$0) (not (Btwn$0 next$0 lst_1$0 l1 curr_3$0))) - (not (member l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)))))) + (not (set.member l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)))))) :named lseg_footprint_22)) (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst$0 l1 null$0) - (member l1 (lseg_domain$0 next$0 lst$0 null$0)) + (set.member l1 (lseg_domain$0 next$0 lst$0 null$0)) (not (= l1 null$0))) (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0))) - (not (member l1 (lseg_domain$0 next$0 lst$0 null$0)))))) + (not (set.member l1 (lseg_domain$0 next$0 lst$0 null$0)))))) :named lseg_footprint_23)) (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 curr_2$0 l1 null$0) - (member l1 (lseg_domain$0 next$0 curr_2$0 null$0)) + (set.member l1 (lseg_domain$0 next$0 curr_2$0 null$0)) (not (= l1 null$0))) (and (or (= l1 null$0) (not (Btwn$0 next$0 curr_2$0 l1 null$0))) - (not (member l1 (lseg_domain$0 next$0 curr_2$0 null$0)))))) + (not (set.member l1 (lseg_domain$0 next$0 curr_2$0 null$0)))))) :named lseg_footprint_24)) -(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_remove_10_11_11)) +(assert (! (not (set.member null$0 Alloc$0)) :named initial_footprint_of_remove_10_11_11)) (assert (! (not (= tmp_2$0 null$0)) :named if_else_28_8_2)) @@ -311,7 +311,7 @@ (assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74)) -(assert (! (= (as emptyset SetLoc) (intersection sk_?X_32$0 sk_?X_31$0)) +(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_32$0 sk_?X_31$0)) :named invariant_18_4_75)) (assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76)) @@ -320,22 +320,22 @@ :named invariant_18_4_77)) (assert (! (= sk_?X_29$0 - (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0))) + (set.union (set.intersection Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0))) :named invariant_18_4_78)) (assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) :named invariant_18_4_79)) -(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_80)) +(assert (! (= (as set.empty SetLoc) (as set.empty SetLoc)) :named invariant_18_4_80)) -(assert (! (= Alloc$0 (union FP_2$0 Alloc$0)) +(assert (! (= Alloc$0 (set.union FP_2$0 Alloc$0)) :named framecondition_of_remove_loop_18_4_18)) (assert (! (= tmp_2$0 (read$0 next$0 curr_3$0)) :named assign_27_4_2)) (assert (! (= lst_1$0 lst$0) :named framecondition_of_remove_loop_18_4_19)) -(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_13_2_5)) +(assert (! (= FP_Caller_1$0 (set.minus FP_Caller$0 FP$0)) :named assign_13_2_5)) (assert (! (or (Btwn$0 next$0 lst_1$0 curr_3$0 curr_3$0) (not (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0))) diff --git a/test/regress/regress1/sets/set-comp-sat.smt2 b/test/regress/regress1/sets/set-comp-sat.smt2 index d6a64c36e..b8c2c1cfd 100644 --- a/test/regress/regress1/sets/set-comp-sat.smt2 +++ b/test/regress/regress1/sets/set-comp-sat.smt2 @@ -10,9 +10,9 @@ (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))) -(assert (not (member b x))) -(assert (member c x)) +(assert (not (set.member b x))) +(assert (set.member c x)) (check-sat) diff --git a/test/regress/regress1/sets/setofsets-disequal.smt2 b/test/regress/regress1/sets/setofsets-disequal.smt2 index 1702aab27..f137ed7dd 100644 --- a/test/regress/regress1/sets/setofsets-disequal.smt2 +++ b/test/regress/regress1/sets/setofsets-disequal.smt2 @@ -8,55 +8,55 @@ (declare-fun S () myset) ; 0 elements -(assert (not (= S (as emptyset myset)))) +(assert (not (= S (as set.empty myset)))) ; 1 element is S -(assert (not (= S (singleton (as emptyset (Set (_ BitVec 1))))))) -(assert (not (= S (singleton (singleton (_ bv0 1)) )))) -(assert (not (= S (singleton (singleton (_ bv1 1)) )))) -(assert (not (= S (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1))))))) +(assert (not (= S (set.singleton (as set.empty (Set (_ BitVec 1))))))) +(assert (not (= S (set.singleton (set.singleton (_ bv0 1)) )))) +(assert (not (= S (set.singleton (set.singleton (_ bv1 1)) )))) +(assert (not (= S (set.singleton (set.union (set.singleton (_ bv0 1)) + (set.singleton (_ bv1 1))))))) ; 2 elements in S -(assert (not (= S (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv0 1)))) ))) -(assert (not (= S (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv1 1))))))) -(assert (not (= S (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))))))) -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (singleton (singleton (_ bv0 1)))) ))) -(assert (not (= S (union (singleton (singleton (_ bv0 1))) - (singleton (singleton (_ bv1 1)))) ))) -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (singleton (singleton (_ bv1 1))))))) +(assert (not (= S (set.union (set.singleton (as set.empty (Set (_ BitVec 1)))) + (set.singleton (set.singleton (_ bv0 1)))) ))) +(assert (not (= S (set.union (set.singleton (as set.empty (Set (_ BitVec 1)))) + (set.singleton (set.singleton (_ bv1 1))))))) +(assert (not (= S (set.union (set.singleton (as set.empty (Set (_ BitVec 1)))) + (set.singleton (set.union (set.singleton (_ bv0 1)) + (set.singleton (_ bv1 1)))))))) +(assert (not (= S (set.union (set.singleton (set.union (set.singleton (_ bv0 1)) + (set.singleton (_ bv1 1)))) + (set.singleton (set.singleton (_ bv0 1)))) ))) +(assert (not (= S (set.union (set.singleton (set.singleton (_ bv0 1))) + (set.singleton (set.singleton (_ bv1 1)))) ))) +(assert (not (= S (set.union (set.singleton (set.union (set.singleton (_ bv0 1)) + (set.singleton (_ bv1 1)))) + (set.singleton (set.singleton (_ bv1 1))))))) ; 3 elements in S -(assert (not (= S (union (singleton (singleton (_ bv1 1))) - (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv0 1))))) ))) -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv1 1))))) ))) -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (union (singleton (singleton (_ bv0 1))) - (singleton (singleton (_ bv1 1))))) ))) -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv0 1))))) ))) +(assert (not (= S (set.union (set.singleton (set.singleton (_ bv1 1))) + (set.union (set.singleton (as set.empty (Set (_ BitVec 1)))) + (set.singleton (set.singleton (_ bv0 1))))) ))) +(assert (not (= S (set.union (set.singleton (set.union (set.singleton (_ bv0 1)) + (set.singleton (_ bv1 1)))) + (set.union (set.singleton (as set.empty (Set (_ BitVec 1)))) + (set.singleton (set.singleton (_ bv1 1))))) ))) +(assert (not (= S (set.union (set.singleton (set.union (set.singleton (_ bv0 1)) + (set.singleton (_ bv1 1)))) + (set.union (set.singleton (set.singleton (_ bv0 1))) + (set.singleton (set.singleton (_ bv1 1))))) ))) +(assert (not (= S (set.union (set.singleton (set.union (set.singleton (_ bv0 1)) + (set.singleton (_ bv1 1)))) + (set.union (set.singleton (as set.empty (Set (_ BitVec 1)))) + (set.singleton (set.singleton (_ bv0 1))))) ))) ; 4 elements in S -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (union (singleton (singleton (_ bv1 1))) - (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv0 1)))))) ))) +(assert (not (= S (set.union (set.singleton (set.union (set.singleton (_ bv0 1)) + (set.singleton (_ bv1 1)))) + (set.union (set.singleton (set.singleton (_ bv1 1))) + (set.union (set.singleton (as set.empty (Set (_ BitVec 1)))) + (set.singleton (set.singleton (_ bv0 1)))))) ))) (check-sat) diff --git a/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2 b/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2 index d75b9c3ae..64a2306c4 100644 --- a/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2 +++ b/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2 @@ -7,7 +7,7 @@ (declare-fun b () (Set (Tuple Int Real))) (declare-fun x () (Tuple Real Real)) (assert (let ((_let_1 0.0)) (not (= x (tuple _let_1 _let_1))))) -(assert (member (tuple ((_ tuple_select 0) x) (to_int ((_ tuple_select 1) x))) a)) -(assert (member (tuple (to_int ((_ tuple_select 0) x)) ((_ tuple_select 1) x)) b)) +(assert (set.member (tuple ((_ tuple_select 0) x) (to_int ((_ tuple_select 1) x))) a)) +(assert (set.member (tuple (to_int ((_ tuple_select 0) x)) ((_ tuple_select 1) x)) b)) (assert (not (= ((_ tuple_select 0) x) ((_ tuple_select 1) x)))) (check-sat) diff --git a/test/regress/regress1/sets/sets-uc-wrong.smt2 b/test/regress/regress1/sets/sets-uc-wrong.smt2 index e8b768d36..73588db4d 100644 --- a/test/regress/regress1/sets/sets-uc-wrong.smt2 +++ b/test/regress/regress1/sets/sets-uc-wrong.smt2 @@ -5,8 +5,8 @@ (declare-fun t () (Set Int)) (declare-fun s () (Set Int)) (declare-const v Bool) -(assert (forall ((q Bool)) (distinct v (subset s t)))) -(assert (= 1 (card t))) +(assert (forall ((q Bool)) (distinct v (set.subset s t)))) +(assert (= 1 (set.card t))) (check-sat) (assert v) (check-sat) diff --git a/test/regress/regress1/sets/sharingbug.smt2 b/test/regress/regress1/sets/sharingbug.smt2 index 82c6eb8f0..a050e9d0e 100644 --- a/test/regress/regress1/sets/sharingbug.smt2 +++ b/test/regress/regress1/sets/sharingbug.smt2 @@ -23,9 +23,9 @@ (let ((e12 (* (- e4) e7))) (let ((e13 (- e10))) (let ((e14 (f0 e5 e7 e6))) -(let ((e15 (member v0 v1))) -(let ((e16 (member e12 v2))) -(let ((e17 (member e14 v1))) +(let ((e15 (set.member v0 v1))) +(let ((e16 (set.member e12 v2))) +(let ((e17 (set.member e14 v1))) (let ((e18 (f1 v3))) (let ((e19 (f1 v2))) (let ((e20 (f1 v1))) diff --git a/test/regress/regress1/sets/univ-set-uf-elim.smt2 b/test/regress/regress1/sets/univ-set-uf-elim.smt2 index f02788a72..548deca05 100644 --- a/test/regress/regress1/sets/univ-set-uf-elim.smt2 +++ b/test/regress/regress1/sets/univ-set-uf-elim.smt2 @@ -6,12 +6,12 @@ (declare-fun f ((Set Bool)) Int) (declare-fun s () (Set Bool)) -(assert (member true s)) -(assert (member false s)) -(assert (= a (f (as univset (Set Bool))))) +(assert (set.member true s)) +(assert (set.member false s)) +(assert (= a (f (as set.universe (Set Bool))))) -(assert (= (f (as emptyset (Set Bool))) 1)) -(assert (= (f (singleton true)) 2)) -(assert (= (f (singleton false)) 3)) -(assert (= (f (union (singleton true) (singleton false))) 4)) +(assert (= (f (as set.empty (Set Bool))) 1)) +(assert (= (f (set.singleton true)) 2)) +(assert (= (f (set.singleton false)) 3)) +(assert (= (f (set.union (set.singleton true) (set.singleton false))) 4)) (check-sat) |