diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-30 13:28:09 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-30 13:28:09 -0400 |
| commit | b06d25a020240fa455798308418ad802f9f40ea3 (patch) | |
| tree | 8203c68da0861a823674b942595ae8cfbfeac256 /test | |
| parent | 7c009ac38ef5ccda070d8d7fb3955273574e94eb (diff) | |
| parent | fa53ae111cd314f455456a884f1247bb9b8e2c7b (diff) | |
Merge pull request #47 from kbansal/sets
Sets theory operators in SMTLIB2 and kinds to use from API have changed. They now are:
SMTLIB: emptyset, singleton*, insert*, union, intersection, setminus, member*, subset*
API: EMPTYSET, SINGLETON*, INSERT*, UNION, INTERSECTION, SETMINUS, MEMBER, SUBSET
(those marked with [*] have changed or been added, others are as earlier)
In the set-logic string use FS to enable sets.
A not-so-well-tested perl command for translating old benchmarks:
perl -pi -e 's/\(set-logic (.+)_SETS\)/\(set-logic \1FS\)/; s/\(in\b/\(member/g; s/\(setenum\b/\(singleton/g; s/\(subseteq\b/\(subset/g; '
Diffstat (limited to 'test')
49 files changed, 372 insertions, 364 deletions
diff --git a/test/regress/regress0/bug567.smt2 b/test/regress/regress0/bug567.smt2 index 265d456b6..109940090 100644 --- a/test/regress/regress0/bug567.smt2 +++ b/test/regress/regress0/bug567.smt2 @@ -27,7 +27,7 @@ (assert (forall ((l4 List0) (e1 Int)) (! (= (buggySortedIns e1 l4) (ite (is-Nil l4) (Cons e1 Nil) (ite (<= (head0 l4) e1) (Cons (head0 l4) (buggySortedIns e1 (tail0 l4))) (Cons e1 l4)))) :pattern ((buggySortedIns e1 l4))))) (assert (forall ((l3 List0) (e Int)) (! (= (sortedIns e l3) (ite (is-Nil l3) (Cons e Nil) (ite (<= (head0 l3) e) (Cons (head0 l3) (sortedIns e (tail0 l3))) (Cons e l3)))) :pattern ((sortedIns e l3))))) (assert (forall ((l5 List0)) (! (= (sort l5) (ite (is-Nil l5) Nil (sortedIns (head0 l5) (sort (tail0 l5))))) :pattern ((sort l5))))) -(assert (forall ((l1 List0)) (! (= (contents l1) (ite (is-Nil l1) (as emptyset (Set Int)) (union (contents (tail0 l1)) (setenum (head0 l1))))) :pattern ((contents l1))))) +(assert (forall ((l1 List0)) (! (= (contents l1) (ite (is-Nil l1) (as emptyset (Set Int)) (union (contents (tail0 l1)) (singleton (head0 l1))))) :pattern ((contents l1))))) @@ -42,7 +42,7 @@ (pop) (push) -(assert (forall ((l4 List0) (e1 Int)) (not (let ((result2 (ite (is-Nil l4) (Cons e1 Nil) (ite (<= (head0 l4) e1) (Cons (head0 l4) (buggySortedIns e1 (tail0 l4))) (Cons e1 l4))))) (and (= (contents result2) (union (contents l4) (setenum e1))) (isSorted result2) (= (size result2) (+ (size l4) 1))))))) +(assert (forall ((l4 List0) (e1 Int)) (not (let ((result2 (ite (is-Nil l4) (Cons e1 Nil) (ite (<= (head0 l4) e1) (Cons (head0 l4) (buggySortedIns e1 (tail0 l4))) (Cons e1 l4))))) (and (= (contents result2) (union (contents l4) (singleton e1))) (isSorted result2) (= (size result2) (+ (size l4) 1))))))) (check-sat) (pop) diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index ccedc7596..9536dfac1 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -44,6 +44,7 @@ TESTS = \ error1.smt2 \ error2.smt2 \ eqtest.smt2 \ + insert.smt2 \ fuzz14418.smt2 \ fuzz15201.smt2 \ fuzz31811.smt2 \ diff --git a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 index 9ba2d84d3..9af45c2dd 100644 --- a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 +++ b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --full-saturate-quant ; EXPECT: unsat (set-option :print-success false) -(set-logic AUFLIA_SETS) +(set-logic AUFLIAFS) (set-info :status unsat) (declare-sort Loc 0) (define-sort SetLoc () (Set Loc)) @@ -46,15 +46,15 @@ (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 (in l1 sk_?X_4$0)) - (not (in l2 sk_?X_4$0))))) + (not (Btwn$0 next$0 l1 l2 null$0)) (not (member l1 sk_?X_4$0)) + (not (member l2 sk_?X_4$0))))) :named sortedness_3)) (assert (! (= (read$1 next$0 null$0) null$0) :named read_null_1)) -(assert (! (not (in tmp_2$0 Alloc$0)) :named new_31_11)) +(assert (! (not (member tmp_2$0 Alloc$0)) :named new_31_11)) -(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_copy_23_11_2)) +(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_copy_23_11_2)) (assert (! (not (= lst$0 null$0)) :named if_else_26_6)) @@ -67,7 +67,7 @@ (assert (! (= cp_2$0 res_1$0) :named assign_32_4)) -(assert (! (= FP_1$0 (union FP$0 (setenum tmp_2$0))) :named assign_31_11)) +(assert (! (= FP_1$0 (union FP$0 (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) - (in l1 (slseg_domain$0 data$0 next$0 lst$0 null$0)) + (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 (in l1 (slseg_domain$0 data$0 next$0 lst$0 null$0)))))) + (not (member l1 (slseg_domain$0 data$0 next$0 lst$0 null$0)))))) :named slseg_footprint_2)) -(assert (! (not (in curr_2$0 FP_1$0)) :named check_heap_access_33_4)) +(assert (! (not (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)) @@ -99,7 +99,7 @@ (assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_26_2_1)) -(assert (! (= Alloc_1$0 (union Alloc$0 (setenum tmp_2$0))) :named assign_31_11_1)) +(assert (! (= Alloc_1$0 (union Alloc$0 (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/regress0/sets/emptyset.smt2 b/test/regress/regress0/sets/emptyset.smt2 index 47fc25661..2b2322d46 100644 --- a/test/regress/regress0/sets/emptyset.smt2 +++ b/test/regress/regress0/sets/emptyset.smt2 @@ -1,4 +1,4 @@ (set-logic ALL_SUPPORTED) (set-info :status unsat) -(assert (in 5 (as emptyset (Set Int) ))) +(assert (member 5 (as emptyset (Set Int) ))) (check-sat) diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2 index 02577b00a..cb816a306 100644 --- a/test/regress/regress0/sets/eqtest.smt2 +++ b/test/regress/regress0/sets/eqtest.smt2 @@ -10,8 +10,8 @@ (declare-fun H () (Set Int) ) (declare-fun I () (Set Int) ) (declare-fun x () Int) -(assert (in x (intersection (union A B) C))) -(assert (not (in x G))) +(assert (member x (intersection (union A B) C))) +(assert (not (member x G))) (assert (= (union A B) D)) (assert (= C (intersection E F))) (assert (and (= F H) (= G H) (= H I))) diff --git a/test/regress/regress0/sets/error1.smt2 b/test/regress/regress0/sets/error1.smt2 index 1241b117f..bf1822305 100644 --- a/test/regress/regress0/sets/error1.smt2 +++ b/test/regress/regress0/sets/error1.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFLIAFS) (set-info :status sat) (declare-fun A () (Set Int)) (declare-fun C () (Set Int)) diff --git a/test/regress/regress0/sets/error2.smt2 b/test/regress/regress0/sets/error2.smt2 index ac678c552..0b8c5ab65 100644 --- a/test/regress/regress0/sets/error2.smt2 +++ b/test/regress/regress0/sets/error2.smt2 @@ -1,4 +1,4 @@ (set-logic QF_ALL_SUPPORTED) (set-info :status unsat) -(assert (= (as emptyset (Set Int)) (setenum 5))) +(assert (= (as emptyset (Set Int)) (singleton 5))) (check-sat) diff --git a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 index 7a8661e4d..7b5294aec 100644 --- a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 +++ b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 @@ -4,14 +4,14 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus 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 (subseteq s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v58 () Int) (declare-fun z3v59 () Int) (assert (distinct z3v58 z3v59)) diff --git a/test/regress/regress0/sets/fuzz14418.smt2 b/test/regress/regress0/sets/fuzz14418.smt2 index d5a49c601..24679749c 100644 --- a/test/regress/regress0/sets/fuzz14418.smt2 +++ b/test/regress/regress0/sets/fuzz14418.smt2 @@ -11,7 +11,7 @@ (set-info :smt-lib-version 2.0) (set-info :category "random") (set-info :status sat) -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFLIAFS) (define-sort Element () Int) (declare-fun f0 ( Int) Int) (declare-fun f1 ( (Set Element) (Set Element) (Set Element)) (Set Element)) @@ -36,19 +36,19 @@ (let ((e16 (f1 e14 v1 v4))) (let ((e17 (intersection e16 e15))) (let ((e18 (f1 v4 e15 v2))) -(let ((e19 (ite (p1 e13) (setenum 1) (setenum 0)))) -(let ((e20 (in v0 e17))) -(let ((e21 (in e7 e16))) -(let ((e22 (in e10 e16))) -(let ((e23 (in e8 e17))) -(let ((e24 (in e9 e14))) -(let ((e25 (in e8 e16))) -(let ((e26 (in v0 e13))) -(let ((e27 (in e12 v4))) -(let ((e28 (in e8 e14))) -(let ((e29 (in e8 v1))) -(let ((e30 (in e10 e13))) -(let ((e31 (in e7 e13))) +(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 ((e32 (f1 e13 e13 e13))) (let ((e33 (f1 e18 v4 e17))) (let ((e34 (f1 v2 v2 e15))) diff --git a/test/regress/regress0/sets/fuzz15201.smt2 b/test/regress/regress0/sets/fuzz15201.smt2 index 8ddeb36d2..e12b74d18 100644 --- a/test/regress/regress0/sets/fuzz15201.smt2 +++ b/test/regress/regress0/sets/fuzz15201.smt2 @@ -4,7 +4,7 @@ (set-info :smt-lib-version 2.0) (set-info :category "random") (set-info :status sat) -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFLIAFS) (define-sort Element () Int) (declare-fun f0 ( Int) Int) (declare-fun f1 ( (Set Element)) (Set Element)) @@ -33,37 +33,37 @@ (let ((e20 (intersection e17 e18))) (let ((e21 (intersection v1 e16))) (let ((e22 (setminus e20 e16))) -(let ((e23 (ite (p1 v2 e18 e21) (setenum 1) (setenum 0)))) +(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) (setenum 1) (setenum 0)))) +(let ((e27 (ite (p1 e20 e19 e25) (singleton 1) (singleton 0)))) (let ((e28 (f1 e20))) -(let ((e29 (in e14 e17))) -(let ((e30 (in e13 e23))) -(let ((e31 (in e11 e25))) -(let ((e32 (in e6 v1))) -(let ((e33 (in e9 v1))) -(let ((e34 (in v0 e28))) -(let ((e35 (in e9 e16))) -(let ((e36 (in e4 e17))) -(let ((e37 (in e9 e18))) -(let ((e38 (in e14 e25))) -(let ((e39 (in e14 v2))) -(let ((e40 (in v0 v1))) -(let ((e41 (in e4 e16))) -(let ((e42 (in e15 e21))) -(let ((e43 (in e7 e22))) -(let ((e44 (in e11 v2))) -(let ((e45 (in e14 e22))) -(let ((e46 (in e11 e16))) -(let ((e47 (in e15 e22))) -(let ((e48 (in e10 e23))) -(let ((e49 (in e4 e21))) -(let ((e50 (in e5 e28))) -(let ((e51 (in e6 e28))) -(let ((e52 (in v0 e22))) -(let ((e53 (in e14 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 ((e54 (f1 e21))) (let ((e55 (f1 e28))) (let ((e56 (f1 e27))) diff --git a/test/regress/regress0/sets/fuzz31811.smt2 b/test/regress/regress0/sets/fuzz31811.smt2 index 799dda0e2..5e7c032ea 100644 --- a/test/regress/regress0/sets/fuzz31811.smt2 +++ b/test/regress/regress0/sets/fuzz31811.smt2 @@ -9,7 +9,7 @@ (set-info :smt-lib-version 2.0) (set-info :category "random") (set-info :status sat) -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFLIAFS) (define-sort Element () Int) (declare-fun f0 ( Int Int Int) Int) (declare-fun f1 ( (Set Element) (Set Element)) (Set Element)) @@ -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) (setenum 1) (setenum 0)))) +(let ((e11 (ite (p1 v1) (singleton 1) (singleton 0)))) (let ((e12 (union v3 v3))) (let ((e13 (intersection v3 v1))) -(let ((e14 (ite (p1 v3) (setenum 1) (setenum 0)))) +(let ((e14 (ite (p1 v3) (singleton 1) (singleton 0)))) (let ((e15 (intersection v2 e14))) -(let ((e16 (ite (p1 e11) (setenum 1) (setenum 0)))) -(let ((e17 (ite (p1 v4) (setenum 1) (setenum 0)))) +(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) (setenum 1) (setenum 0)))) +(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) (setenum 1) (setenum 0)))) +(let ((e26 (ite (p1 e15) (singleton 1) (singleton 0)))) (let ((e27 (setminus e17 e15))) (let ((e28 (f1 e23 e12))) -(let ((e29 (in e10 e16))) -(let ((e30 (in e10 v1))) -(let ((e31 (in e7 e19))) +(let ((e29 (member e10 e16))) +(let ((e30 (member e10 v1))) +(let ((e31 (member e7 e19))) (let ((e32 (f1 e12 e12))) (let ((e33 (f1 e16 e25))) (let ((e34 (f1 v1 e27))) diff --git a/test/regress/regress0/sets/insert.smt2 b/test/regress/regress0/sets/insert.smt2 new file mode 100644 index 000000000..b4936a32b --- /dev/null +++ b/test/regress/regress0/sets/insert.smt2 @@ -0,0 +1,7 @@ +(set-option :produce-models true) +(set-logic QF_UFLIAFS) +(set-info :status sat) +(declare-fun X () (Set Int)) +(assert (= X (insert 1 2 (singleton 3)))) +(check-sat) +;(get-model) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 index b90563199..71bb8a3e6 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 @@ -3,14 +3,14 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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 (subseteq s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v58 () Int) (declare-fun z3v59 () Int) (assert (distinct z3v58 z3v59)) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 index 204af2f2d..652307645 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 @@ -7,12 +7,12 @@ (declare-fun S () (Set Int)) (declare-fun T () (Set Int)) -(assert (in x S)) +(assert (member x S)) -(assert (= S (union T (setenum y)))) +(assert (= S (union T (singleton y)))) (assert (not (= x y))) -(assert (not (in x T))) +(assert (not (member x T))) (check-sat) diff --git a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 index ad0a7e464..2ef07f920 100644 --- a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 +++ b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 @@ -1,5 +1,5 @@ (set-option :print-success false) -(set-logic AUFLIA_SETS) +(set-logic AUFLIAFS) (set-info :status unsat) (declare-sort Loc 0) (define-sort SetLoc () (Set Loc)) @@ -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 (in l1 sk_?X$0)) - (not (in l2 sk_?X$0))))) + (not (Btwn$0 next$0 l1 l2 null$0)) (not (member l1 sk_?X$0)) + (not (member l2 sk_?X$0))))) :named strict_sortedness)) (assert (! (forall ((l1 Loc)) (or (= l1 null$0) - (in (read$0 data$0 l1) + (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) - (in (read$0 data$0 curr_2$0) + (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)))) - (in + (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 - (in (read$0 data$0 curr_2$0) + (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) - (in (read$0 data$0 prev_2$0) + (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)))) - (in + (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 - (in (read$0 data$0 prev_2$0) + (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) - (in (read$0 data$0 sk_l1$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l1$0) + (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) - (in (read$0 data$0 sk_l1_1$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l1_1$0) + (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) - (in (read$0 data$0 sk_l2$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l2$0) + (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) - (in (read$0 data$0 sk_l2_1$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l2_1$0) + (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) - (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (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)))) - (in + (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 (in sk_?e$0 (sorted_set_c$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))))) :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) - (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))) + (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)))) - (in + (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 (in sk_?e_3$0 (sorted_set_c$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))))) :named sorted_set_2_7)) (assert (! (forall ((l1 Loc)) (or (= l1 null$0) - (in (read$0 data$0 l1) + (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) - (in (read$0 data$0 l1) + (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) - (in (read$0 data$0 curr_2$0) + (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)))) - (in + (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 - (in (read$0 data$0 curr_2$0) + (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) - (in (read$0 data$0 prev_2$0) + (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)))) - (in + (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 - (in (read$0 data$0 prev_2$0) + (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) - (in (read$0 data$0 sk_l1$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l1$0) + (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) - (in (read$0 data$0 sk_l1_1$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l1_1$0) + (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) - (in (read$0 data$0 sk_l2$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l2$0) + (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) - (in (read$0 data$0 sk_l2_1$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l2_1$0) + (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) - (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (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)))) - (in + (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 (in sk_?e$0 (sorted_set_c$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))))) :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) - (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) + (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)))) - (in + (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 - (in sk_?e_3$0 + (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) - (in (read$0 data$0 curr_2$0) + (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)))) - (in + (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 - (in (read$0 data$0 curr_2$0) + (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) - (in (read$0 data$0 prev_2$0) + (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)))) - (in + (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 - (in (read$0 data$0 prev_2$0) + (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) - (in (read$0 data$0 sk_l1$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l1$0) + (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) - (in (read$0 data$0 sk_l1_1$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l1_1$0) + (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) - (in (read$0 data$0 sk_l2$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l2$0) + (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) - (in (read$0 data$0 sk_l2_1$0) + (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)))) - (in + (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 - (in (read$0 data$0 sk_l2_1$0) + (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) - (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (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)))) - (in + (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 (in sk_?e$0 (sorted_set_c$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))))) :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) - (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) + (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)))) - (in + (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 - (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + (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) - (in l1 (sorted_set_domain$0 data$0 next$0 lst$0 null$0)) + (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 - (in l1 + (member l1 (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))))) :named sorted_set_footprint)) -(assert (! (or (in sk_?e_3$0 c2_2$0) - (and (in sk_?e_2$0 sk_FP_1$0) (not (in sk_?e_2$0 FP$0))) - (and (in sk_?e_3$0 (union c1_2$0 c2_2$0)) - (not (in sk_?e_3$0 content$0))) - (and (in sk_?e_3$0 c1_2$0) +(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) (not - (in sk_?e_3$0 + (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (and (in sk_?e_3$0 content$0) - (not (in sk_?e_3$0 (union c1_2$0 c2_2$0)))) - (and (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (not (in sk_?e_3$0 c1_2$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 (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)) @@ -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) (in sk_l1$0 sk_?X_3$0) - (in 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) (member sk_l1$0 sk_?X_3$0) + (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) - (in l1 + (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 - (in l1 + (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) - (in l1 + (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 - (in l1 + (member l1 (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))))) :named sorted_set_footprint_2)) -(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1)) +(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1)) (assert (! (or (= prev_2$0 curr_2$0) - (in sk_?e_1$0 (intersection sk_?X_4$0 sk_?X_3$0)) - (and (in sk_?e_1$0 sk_FP$0) (not (in sk_?e_1$0 FP$0))) - (and (in sk_?e$0 (union c1_2$0 c2_2$0)) (not (in sk_?e$0 content$0))) - (and (in sk_?e$0 c1_2$0) - (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (and (in sk_?e$0 c2_2$0) - (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (and (in sk_?e$0 content$0) (not (in sk_?e$0 (union c1_2$0 c2_2$0)))) - (and (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (not (in sk_?e$0 c1_2$0))) - (and (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (not (in sk_?e$0 c2_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))) (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)) @@ -772,7 +772,7 @@ (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) - (in sk_l1_1$0 sk_?X_5$0) (in sk_l2_1$0 sk_?X_5$0) + (member sk_l1_1$0 sk_?X_5$0) (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/regress0/sets/jan24/remove_check_free_31_6.smt2 b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 index c1c65cea5..2bf2d4c62 100644 --- a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 +++ b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 @@ -1,5 +1,5 @@ (set-option :print-success false) -(set-logic AUFLIA_SETS) +(set-logic AUFLIAFS) (set-info :status unsat) (declare-sort Loc 0) (define-sort SetLoc () (Set Loc)) @@ -76,22 +76,22 @@ :named btwn_step_10)) (assert (! (forall ((?f FldLoc)) - (or (in (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0) + (or (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 (in (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0) + (or (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 (in (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0) + (or (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 (in (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0) + (or (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 (in ?y sk_?X_30$0)))) + (not (Btwn$0 ?f null$0 ?y ?y)) (not (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 (in ?y sk_?X_30$0)))) + (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (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 (in ?y sk_?X_30$0)))) + (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (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 (in ?y sk_?X_30$0)))) + (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (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 (in ?y sk_?X_30$0)) - (in (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0))) + (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))) :named entry-point2_10)) (assert (! (forall ((?f FldLoc) (?y Loc)) - (or (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (in ?y sk_?X_30$0)) - (in (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 (member ?y sk_?X_30$0)) + (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 (in ?y sk_?X_30$0)) - (in (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 (member ?y sk_?X_30$0)) + (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 (in ?y sk_?X_30$0)) - (in (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 (member ?y sk_?X_30$0)) + (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,28 +181,28 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst$0 l1 curr_2$0) - (in l1 (lseg_domain$0 next$0 lst$0 curr_2$0)) + (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 (in l1 (lseg_domain$0 next$0 lst$0 curr_2$0)))))) + (not (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) - (in l1 (lseg_domain$0 next$0 curr_3$0 null$0)) + (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 (in l1 (lseg_domain$0 next$0 curr_3$0 null$0)))))) + (not (member l1 (lseg_domain$0 next$0 curr_3$0 null$0)))))) :named lseg_footprint_21)) -(assert (! (not (in tmp_2$0 FP_2$0)) :named check_free_31_6)) +(assert (! (not (member tmp_2$0 FP_2$0)) :named check_free_31_6)) -(assert (! (not (in null$0 Alloc$0)) :named framecondition_of_remove_loop_18_4_15)) +(assert (! (not (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)) @@ -263,35 +263,35 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst_1$0 l1 curr_3$0) - (in l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) + (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 (in l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)))))) + (not (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) - (in l1 (lseg_domain$0 next$0 lst$0 null$0)) + (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 (in l1 (lseg_domain$0 next$0 lst$0 null$0)))))) + (not (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) - (in l1 (lseg_domain$0 next$0 curr_2$0 null$0)) + (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 (in l1 (lseg_domain$0 next$0 curr_2$0 null$0)))))) + (not (member l1 (lseg_domain$0 next$0 curr_2$0 null$0)))))) :named lseg_footprint_24)) -(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_remove_10_11_11)) +(assert (! (not (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)) diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 index 7fea3435e..eb48b023a 100644 --- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 @@ -3,14 +3,14 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus 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 (subseteq s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v54 () Int) (declare-fun z3f55 (Int) Int) (declare-fun z3v56 () Int) diff --git a/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 index 6c32bb578..3c0ef1dda 100644 --- a/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 +++ b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 @@ -9,14 +9,14 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus 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 (subseteq s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v56 () Int) (declare-fun z3v57 () Int) (assert (distinct z3v56 z3v57)) diff --git a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 index 0aa6c88ae..83dfe41e5 100644 --- a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 +++ b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -4,14 +4,14 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus 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 (subseteq s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v58 () Int) (declare-fun z3v59 () Int) (assert (distinct z3v58 z3v59)) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 index d0fda8b86..282325f14 100644 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -4,14 +4,14 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus 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 (subseteq s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v60 () Int) (declare-fun z3v61 () Int) (assert (distinct z3v60 z3v61)) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 index f37a8ccfe..10ed4be7c 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 @@ -3,12 +3,12 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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 (subseteq s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v66 () Int) (declare-fun z3v67 () Int) (assert (distinct z3v66 z3v67)) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 index 59cc1a00e..6165b98de 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 @@ -3,14 +3,14 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus 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 (subseteq s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v66 () Int) (declare-fun z3v67 () Int) (assert (distinct z3v66 z3v67)) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 index 5fa5101f0..df659f0fb 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 @@ -8,12 +8,12 @@ ; What was going on? ; ; The solver was unable to reason that (emptyset) cannot equal -; (setenum 0). There were no membership predicates anywhere, just +; (singleton 0). There were no membership predicates anywhere, just ; equalities. ; ; Fix ; -; Add the propagation rule: (true) => (in x (setenum x)) +; Add the propagation rule: (true) => (member x (singleton x)) (declare-fun z3f70 (Int) (Set Int)) (declare-fun z3v85 () Int) @@ -21,7 +21,7 @@ (declare-fun z3v87 () Int) (declare-fun z3v90 () Int) -(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (setenum z3v86))))) +(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (singleton z3v86))))) (assert (= (z3f70 z3v90) (z3f70 z3v87))) (assert (= (as emptyset (Set Int)) (z3f70 z3v87))) (check-sat) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 index d01b7468e..af67a69a7 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 @@ -9,10 +9,10 @@ (declare-fun T () (Set Int)) (declare-fun x () Int) -(assert (or (not (= S smt_set_emp)) (in x T))) +(assert (or (not (= S smt_set_emp)) (member x T))) (assert (= smt_set_emp - (ite (in x T) - (union (union smt_set_emp (setenum x)) S) + (ite (member x T) + (union (union smt_set_emp (singleton x)) S) S))) (check-sat) diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 index e6f187331..38477c46a 100644 --- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 +++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 @@ -3,12 +3,12 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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 (subseteq s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v66 () Int) (declare-fun z3v67 () Int) diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 index b8a27b967..e282e446e 100644 --- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 +++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 @@ -3,12 +3,12 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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 (subseteq s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (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 (subseteq (z3f70 z3v242) +(assert (subset (z3f70 z3v242) (z3f70 z3v244))) (assert (= (z3f72 z3v243) smt_set_emp)) (assert (= (z3f72 z3v244) diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 index 1ea3ea6b5..0fc8ca067 100644 --- a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 +++ b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 @@ -1,7 +1,7 @@ ; EXPECT: sat ; Observed behavior: -; --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143)) +; --check-model failed for set-term (union (z3f69 z3v151) (singleton z3v143)) ; with different set of elements in the model for representative and the node ; itself. ; @@ -24,14 +24,14 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus 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 (subseteq s1 s2)) +(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) (declare-fun z3v58 () Int) (declare-fun z3v59 () Int) @@ -69,16 +69,16 @@ (z3f69 z3v140)))) (assert (= (z3f69 z3v152) - (smt_set_cup (setenum z3v143) (z3f69 z3v151)))) + (smt_set_cup (singleton z3v143) (z3f69 z3v151)))) (assert (= (z3f70 z3v152) - (smt_set_cup (setenum z3v143) (z3f70 z3v151)))) + (smt_set_cup (singleton z3v143) (z3f70 z3v151)))) (assert (and (= (z3f69 z3v142) - (smt_set_cup (setenum z3v143) (z3f69 z3v141))) + (smt_set_cup (singleton z3v143) (z3f69 z3v141))) (= (z3f70 z3v142) - (smt_set_cup (setenum z3v143) (z3f70 z3v141))) + (smt_set_cup (singleton z3v143) (z3f70 z3v141))) (= z3v142 (z3f92 z3v143 z3v141)) (= z3v142 z3v144) (= (z3f62 z3v61) z3v61) diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 index dc42abfa2..d851ca35e 100644 --- a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 +++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 @@ -1,12 +1,12 @@ ; EXPECT: unsat -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFLIAFS) (set-info :status sat) (declare-fun a () Int) (declare-fun b () Int) (declare-fun x () (Set Int)) (declare-fun y () (Set Int)) -(assert (= x (setenum a))) -(assert (= y (setenum b))) +(assert (= x (singleton a))) +(assert (= y (singleton b))) (assert (not (= x y))) (assert (and (< 1 a) (< a 3) (< 1 b) (< b 3))) (check-sat) diff --git a/test/regress/regress0/sets/mar2014/small.smt2 b/test/regress/regress0/sets/mar2014/small.smt2 index 838a27919..635c7959d 100644 --- a/test/regress/regress0/sets/mar2014/small.smt2 +++ b/test/regress/regress0/sets/mar2014/small.smt2 @@ -4,15 +4,15 @@ ; demostrates core issue with UniqueZipper.hs.1030minimized.cvc4.smt2 ; unlike original benchmark, this is unsat. -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFLIAFS) (declare-fun x () Int) (declare-fun y () Int) (declare-fun z () Int) (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) -(assert (in x (union a b))) -(assert (not (in y a))) -(assert (not (in z b))) +(assert (member x (union a b))) +(assert (not (member y a))) +(assert (not (member z b))) (assert (= z y)) (assert (= x y)) (check-sat) diff --git a/test/regress/regress0/sets/mar2014/smaller.smt2 b/test/regress/regress0/sets/mar2014/smaller.smt2 index 876311de8..d6565205b 100644 --- a/test/regress/regress0/sets/mar2014/smaller.smt2 +++ b/test/regress/regress0/sets/mar2014/smaller.smt2 @@ -4,12 +4,12 @@ ; demostrates core issue with UniqueZipper.hs.1030minimized.cvc4.smt2 ; fails check-model, even though answer is correct -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFLIAFS) (declare-fun x () Int) (declare-fun y () Int) (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) -(assert (in x (union a b))) -(assert (not (in y a))) +(assert (member x (union a b))) +(assert (not (member y a))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 index 57d5d72ca..61fbee11d 100644 --- a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 +++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 @@ -1,5 +1,5 @@ (set-option :print-success false) -(set-logic AUFLIA_SETS) +(set-logic AUFLIAFS) (set-info :status unsat) (declare-sort Loc 0) (define-sort SetLoc () (Set Loc)) @@ -45,15 +45,15 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 curr$0 l1 null$0) - (in l1 (lseg_domain$0 next$0 curr$0 null$0)) + (member l1 (lseg_domain$0 next$0 curr$0 null$0)) (not (= l1 null$0))) (and (or (= l1 null$0) (not (Btwn$0 next$0 curr$0 l1 null$0))) - (not (in l1 (lseg_domain$0 next$0 curr$0 null$0)))))) + (not (member l1 (lseg_domain$0 next$0 curr$0 null$0)))))) :named lseg_footprint_14)) -(assert (! (not (in tmp_1$0 Alloc$0)) :named new_42_10)) +(assert (! (not (member tmp_1$0 Alloc$0)) :named new_42_10)) -(assert (! (not (in null$0 Alloc$0)) +(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_rec_copy_loop_34_11_4)) (assert (! (not (= curr$0 null$0)) :named if_else_37_6)) @@ -73,7 +73,7 @@ (assert (! (= FP_Caller_2$0 (setminus FP_Caller$0 FP$0)) :named assign_37_2_2)) -(assert (! (= Alloc_2$0 (union Alloc$0 (setenum tmp_1$0))) :named assign_42_10)) +(assert (! (= Alloc_2$0 (union Alloc$0 (singleton tmp_1$0))) :named assign_42_10)) (assert (! (or (Btwn$0 next$0 cp$0 null$0 null$0) (not (lseg_struct$0 sk_?X_38$0 next$0 cp$0 null$0))) @@ -82,13 +82,13 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 cp$0 l1 null$0) - (in l1 (lseg_domain$0 next$0 cp$0 null$0)) + (member l1 (lseg_domain$0 next$0 cp$0 null$0)) (not (= l1 null$0))) (and (or (= l1 null$0) (not (Btwn$0 next$0 cp$0 l1 null$0))) - (not (in l1 (lseg_domain$0 next$0 cp$0 null$0)))))) + (not (member l1 (lseg_domain$0 next$0 cp$0 null$0)))))) :named lseg_footprint_15)) -(assert (! (not (in cp_1$0 FP_3$0)) :named check_heap_access_43_4)) +(assert (! (not (member cp_1$0 FP_3$0)) :named check_heap_access_43_4)) (assert (! (not (= tmp_1$0 null$0)) :named new_42_10_1)) @@ -109,7 +109,7 @@ (assert (! (= cp_1$0 tmp_1$0) :named assign_42_4)) -(assert (! (= FP_3$0 (union FP$0 (setenum tmp_1$0))) :named assign_42_10_1)) +(assert (! (= FP_3$0 (union FP$0 (singleton tmp_1$0))) :named assign_42_10_1)) (assert (! (or (Btwn$0 next$0 curr$0 null$0 null$0) (not (lseg_struct$0 sk_?X_37$0 next$0 curr$0 null$0))) diff --git a/test/regress/regress0/sets/setel-eq.smt2 b/test/regress/regress0/sets/setel-eq.smt2 index 8ed9a2e57..b5d85c7e8 100644 --- a/test/regress/regress0/sets/setel-eq.smt2 +++ b/test/regress/regress0/sets/setel-eq.smt2 @@ -4,7 +4,7 @@ (declare-fun T () (Set Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (in y S)) -(assert (not (in x (union S T)))) +(assert (member y S)) +(assert (not (member x (union S T)))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress0/sets/setofsets-disequal.smt2 b/test/regress/regress0/sets/setofsets-disequal.smt2 index 907e074fe..1702aab27 100644 --- a/test/regress/regress0/sets/setofsets-disequal.smt2 +++ b/test/regress/regress0/sets/setofsets-disequal.smt2 @@ -1,7 +1,7 @@ ; On a production build (as of 2014-05-16), takes several minutes ; to finish (2967466 decisions). -(set-logic QF_BV_SETS) +(set-logic QF_BVFS) (set-info :status unsat) (define-sort myset () (Set (Set (_ BitVec 1)))) @@ -11,52 +11,52 @@ (assert (not (= S (as emptyset myset)))) ; 1 element is S -(assert (not (= S (setenum (as emptyset (Set (_ BitVec 1))))))) -(assert (not (= S (setenum (setenum (_ bv0 1)) )))) -(assert (not (= S (setenum (setenum (_ bv1 1)) )))) -(assert (not (= S (setenum (union (setenum (_ bv0 1)) - (setenum (_ bv1 1))))))) +(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))))))) ; 2 elements in S -(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1)))) - (setenum (setenum (_ bv0 1)))) ))) -(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1)))) - (setenum (setenum (_ bv1 1))))))) -(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1)))) - (setenum (union (setenum (_ bv0 1)) - (setenum (_ bv1 1)))))))) -(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) - (setenum (_ bv1 1)))) - (setenum (setenum (_ bv0 1)))) ))) -(assert (not (= S (union (setenum (setenum (_ bv0 1))) - (setenum (setenum (_ bv1 1)))) ))) -(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) - (setenum (_ bv1 1)))) - (setenum (setenum (_ bv1 1))))))) +(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))))))) ; 3 elements in S -(assert (not (= S (union (setenum (setenum (_ bv1 1))) - (union (setenum (as emptyset (Set (_ BitVec 1)))) - (setenum (setenum (_ bv0 1))))) ))) -(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) - (setenum (_ bv1 1)))) - (union (setenum (as emptyset (Set (_ BitVec 1)))) - (setenum (setenum (_ bv1 1))))) ))) -(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) - (setenum (_ bv1 1)))) - (union (setenum (setenum (_ bv0 1))) - (setenum (setenum (_ bv1 1))))) ))) -(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) - (setenum (_ bv1 1)))) - (union (setenum (as emptyset (Set (_ BitVec 1)))) - (setenum (setenum (_ bv0 1))))) ))) +(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))))) ))) ; 4 elements in S -(assert (not (= S (union (setenum (union (setenum (_ bv0 1)) - (setenum (_ bv1 1)))) - (union (setenum (setenum (_ bv1 1))) - (union (setenum (as emptyset (Set (_ BitVec 1)))) - (setenum (setenum (_ bv0 1)))))) ))) +(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)))))) ))) (check-sat) diff --git a/test/regress/regress0/sets/sets-disequal.smt2 b/test/regress/regress0/sets/sets-disequal.smt2 index 65f55f3a6..3acf77108 100644 --- a/test/regress/regress0/sets/sets-disequal.smt2 +++ b/test/regress/regress0/sets/sets-disequal.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat ; EXPECT: unsat ; EXIT: 0 -(set-logic QF_BV_SETS) +(set-logic QF_BVFS) (declare-fun S1 () (Set (_ BitVec 1))) (declare-fun S2 () (Set (_ BitVec 1))) (declare-fun S3 () (Set (_ BitVec 1))) diff --git a/test/regress/regress0/sets/sets-equal.smt2 b/test/regress/regress0/sets/sets-equal.smt2 index a2ce4b3c2..8fd29a244 100644 --- a/test/regress/regress0/sets/sets-equal.smt2 +++ b/test/regress/regress0/sets/sets-equal.smt2 @@ -6,9 +6,9 @@ (assert (= x y)) (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) -(assert (not (in x a))) -(assert (in y (union a b))) +(assert (not (member x a))) +(assert (member y (union a b))) (assert (= x z)) -(assert (not (in z a))) +(assert (not (member z a))) (assert (= a b)) (check-sat) diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2 index 0f5e41864..d3d8a9044 100644 --- a/test/regress/regress0/sets/sets-inter.smt2 +++ b/test/regress/regress0/sets/sets-inter.smt2 @@ -4,8 +4,8 @@ (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) (declare-fun x () Int) -;(assert (not (in x a))) -(assert (in x (intersection a b))) -(assert (not (in x b))) +;(assert (not (member x a))) +(assert (member x (intersection a b))) +(assert (not (member x b))) (check-sat) (exit) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index accb09799..0f43ee10d 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -6,11 +6,11 @@ (declare-fun A () SetInt) (declare-fun B () SetInt) (declare-fun x () Int) -(assert (in x (union A B))) +(assert (member x (union A B))) -(assert (not (in x (intersection A B)))) -(assert (not (in x (setminus A B)))) -;(assert (not (in x (setminus B A)))) -;(assert (in x B)) +(assert (not (member x (intersection A B)))) +(assert (not (member x (setminus A B)))) +;(assert (not (member x (setminus B A)))) +;(assert (member x B)) (check-sat) diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 index 1bd0eb396..a040b0bec 100644 --- a/test/regress/regress0/sets/sets-sample.smt2 +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -12,14 +12,14 @@ (declare-fun b () (Set Int)) (declare-fun c () (Set Int)) (declare-fun e () Int) -(assert (= a (setenum 5))) +(assert (= a (singleton 5))) (assert (= c (union a b) )) (assert (not (= c (intersection a b) ))) (assert (= c (setminus a b) )) -(assert (subseteq a b)) -(assert (in e c)) -(assert (in e a)) -(assert (in e (intersection a b))) +(assert (subset a b)) +(assert (member e c)) +(assert (member e a)) +(assert (member e (intersection a b))) (check-sat) (pop 1) @@ -41,8 +41,8 @@ (declare-fun e2 () Int) (assert (= x y)) (assert (= e1 e2)) -(assert (in e1 x)) -(assert (not (in e2 y))) +(assert (member e1 x)) +(assert (not (member e2 y))) (check-sat) (pop 1) @@ -55,8 +55,8 @@ (declare-fun e2 () Int) (assert (= x y)) (assert (= e1 e2)) -(assert (in e1 (union x z))) -(assert (not (in e2 (union y z)))) +(assert (member e1 (union x z))) +(assert (not (member e2 (union y z)))) (check-sat) (pop 1) diff --git a/test/regress/regress0/sets/sets-sharing.smt2 b/test/regress/regress0/sets/sets-sharing.smt2 index d2a94fdf4..caada9606 100644 --- a/test/regress/regress0/sets/sets-sharing.smt2 +++ b/test/regress/regress0/sets/sets-sharing.smt2 @@ -4,8 +4,8 @@ (declare-fun S () (Set Int)) (declare-fun x () Int) -(assert (in (+ 5 x) S)) -(assert (not (in 9 S))) +(assert (member (+ 5 x) S)) +(assert (not (member 9 S))) (assert (= x 4)) (check-sat) diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2 index 9dd257401..e68520cbf 100644 --- a/test/regress/regress0/sets/sets-testlemma-ints.smt2 +++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFLIAFS) (set-info :status sat) (declare-fun x () (Set Int)) (declare-fun y () (Set Int)) diff --git a/test/regress/regress0/sets/sets-testlemma-reals.smt2 b/test/regress/regress0/sets/sets-testlemma-reals.smt2 index 16e7780b4..bc18235f0 100644 --- a/test/regress/regress0/sets/sets-testlemma-reals.smt2 +++ b/test/regress/regress0/sets/sets-testlemma-reals.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_UFLRA_SETS) +(set-logic QF_UFLRAFS) (set-info :status sat) (declare-fun x () (Set Real)) (declare-fun y () (Set Real)) diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2 index 183f54242..aee8c5937 100644 --- a/test/regress/regress0/sets/sets-testlemma.smt2 +++ b/test/regress/regress0/sets/sets-testlemma.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_UFBV_SETS) +(set-logic QF_UFBVFS) (set-info :status sat) (declare-fun x () (Set (_ BitVec 2))) (declare-fun y () (Set (_ BitVec 2))) diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2 index 656a0bc88..56ba520dc 100644 --- a/test/regress/regress0/sets/sets-union.smt2 +++ b/test/regress/regress0/sets/sets-union.smt2 @@ -6,10 +6,10 @@ (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) (declare-fun x () Int) -(assert (not (in x a))) -(assert (in x (union a b))) +(assert (not (member x a))) +(assert (member x (union a b))) (check-sat) ;(get-model) -(assert (not (in x b))) +(assert (not (member x b))) (check-sat) (exit) diff --git a/test/regress/regress0/sets/sharingbug.smt2 b/test/regress/regress0/sets/sharingbug.smt2 index b2b61f739..b87579816 100644 --- a/test/regress/regress0/sets/sharingbug.smt2 +++ b/test/regress/regress0/sets/sharingbug.smt2 @@ -2,7 +2,7 @@ (set-info :smt-lib-version 2.0) (set-info :category "random") (set-info :status sat) -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFLIAFS) (define-sort Element () Int) (declare-fun f0 ( Int Int Int) Int) (declare-fun f1 ( (Set Element)) (Set Element)) @@ -23,9 +23,9 @@ (let ((e12 (* (- e4) e7))) (let ((e13 (- e10))) (let ((e14 (f0 e5 e7 e6))) -(let ((e15 (in v0 v1))) -(let ((e16 (in e12 v2))) -(let ((e17 (in e14 v1))) +(let ((e15 (member v0 v1))) +(let ((e16 (member e12 v2))) +(let ((e17 (member e14 v1))) (let ((e18 (f1 v3))) (let ((e19 (f1 v2))) (let ((e20 (f1 v1))) diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2 index 7bbe442e1..6a73c5b91 100644 --- a/test/regress/regress0/sets/union-1a-flip.smt2 +++ b/test/regress/regress0/sets/union-1a-flip.smt2 @@ -8,9 +8,9 @@ (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) (declare-fun x () Int) -(assert (in x A)) +(assert (member x A)) (push 1) -(assert (not (in x (union A B)))) +(assert (not (member x (union A B)))) (check-sat) (pop 1) (check-sat) diff --git a/test/regress/regress0/sets/union-1a.smt2 b/test/regress/regress0/sets/union-1a.smt2 index b594ac74d..8636cb220 100644 --- a/test/regress/regress0/sets/union-1a.smt2 +++ b/test/regress/regress0/sets/union-1a.smt2 @@ -8,9 +8,9 @@ (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) (declare-fun x () Int) -(assert (not (in x (union A B)))) +(assert (not (member x (union A B)))) (push 1) -(assert (in x A)) +(assert (member x A)) (check-sat) (pop 1) (check-sat) diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2 index 72c544553..e2b19b31a 100644 --- a/test/regress/regress0/sets/union-1b-flip.smt2 +++ b/test/regress/regress0/sets/union-1b-flip.smt2 @@ -8,9 +8,9 @@ (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) (declare-fun x () Int) -(assert (in x B)) +(assert (member x B)) (push 1) -(assert (not (in x (union A B)))) +(assert (not (member x (union A B)))) (check-sat) (pop 1) (check-sat) diff --git a/test/regress/regress0/sets/union-1b.smt2 b/test/regress/regress0/sets/union-1b.smt2 index 85fce759c..c354923c9 100644 --- a/test/regress/regress0/sets/union-1b.smt2 +++ b/test/regress/regress0/sets/union-1b.smt2 @@ -8,9 +8,9 @@ (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) (declare-fun x () Int) -(assert (not (in x (union A B)))) +(assert (not (member x (union A B)))) (push 1) -(assert (in x B)) +(assert (member x B)) (check-sat) (pop 1) (check-sat) diff --git a/test/regress/regress0/sets/union-2.smt2 b/test/regress/regress0/sets/union-2.smt2 index e5e96be5a..6e2933975 100644 --- a/test/regress/regress0/sets/union-2.smt2 +++ b/test/regress/regress0/sets/union-2.smt2 @@ -6,7 +6,7 @@ (declare-fun B () (Set Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (in x (union A B))) -(assert (not (in y A))) -(assert (not (in y B))) +(assert (member x (union A B))) +(assert (not (member y A))) +(assert (not (member y B))) (check-sat) |