diff options
Diffstat (limited to 'test/regress/regress0')
13 files changed, 16 insertions, 16 deletions
diff --git a/test/regress/regress0/rels/addr_book_0.cvc.smt2 b/test/regress/regress0/rels/addr_book_0.cvc.smt2 index 70488b4eb..9bc85f268 100644 --- a/test/regress/regress0/rels/addr_book_0.cvc.smt2 +++ b/test/regress/regress0/rels/addr_book_0.cvc.smt2 @@ -33,7 +33,7 @@ (assert (set.member t_tup Target)) (assert (set.subset (rel.join (rel.join Book addr) Target) Name)) (assert (set.subset (rel.join Book names) Name)) -(assert (= (set.intersection Name Addr) (as set.empty (Set (Tuple Atom))))) +(assert (= (set.inter Name Addr) (as set.empty (Set (Tuple Atom))))) (assert (= (rel.join (set.singleton n_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Set (Tuple Atom))))) (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.union (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (set.singleton t_tup))))) (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b3_tup) addr)) (set.minus (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.singleton t_tup))))) diff --git a/test/regress/regress0/rels/iden_0.cvc.smt2 b/test/regress/regress0/rels/iden_0.cvc.smt2 index 1cdeffbff..75dc80d22 100644 --- a/test/regress/regress0/rels/iden_0.cvc.smt2 +++ b/test/regress/regress0/rels/iden_0.cvc.smt2 @@ -21,5 +21,5 @@ (assert (set.member v x)) (assert (set.member a x)) (assert (= id (rel.iden t))) -(assert (not (set.member (tuple 1 1) (set.intersection id x)))) +(assert (not (set.member (tuple 1 1) (set.inter id x)))) (check-sat) diff --git a/test/regress/regress0/sets/complement3.cvc.smt2 b/test/regress/regress0/sets/complement3.cvc.smt2 index 20cfb36f8..2046b2fc9 100644 --- a/test/regress/regress0/sets/complement3.cvc.smt2 +++ b/test/regress/regress0/sets/complement3.cvc.smt2 @@ -8,7 +8,7 @@ (declare-fun C4 () (Set (Tuple Atom))) (declare-fun ATOM_UNIV () (Set (Tuple Atom))) (declare-fun V1 () Atom) -(assert (= C32 (set.intersection (set.complement C2) (set.complement C4)))) +(assert (= C32 (set.inter (set.complement C2) (set.complement C4)))) (assert (set.member (tuple V1) (set.complement C32))) (assert (= ATOM_UNIV (as set.universe (Set (Tuple Atom))))) (assert (set.member (tuple V1) ATOM_UNIV)) diff --git a/test/regress/regress0/sets/cvc-sample.cvc.smt2 b/test/regress/regress0/sets/cvc-sample.cvc.smt2 index 9ee199b43..9c89df0c6 100644 --- a/test/regress/regress0/sets/cvc-sample.cvc.smt2 +++ b/test/regress/regress0/sets/cvc-sample.cvc.smt2 @@ -20,12 +20,12 @@ (declare-fun e () Int) (assert (= a (set.singleton 5))) (assert (= c (set.union a b))) -(assert (not (= c (set.intersection a b)))) +(assert (not (= c (set.inter a b)))) (assert (= c (set.minus a b))) (assert (set.subset a b)) (assert (set.member e c)) (assert (set.member e a)) -(assert (set.member e (set.intersection a b))) +(assert (set.member e (set.inter a b))) (push 1) (assert true) diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2 index 0ecd32bf8..c93b18857 100644 --- a/test/regress/regress0/sets/eqtest.smt2 +++ b/test/regress/regress0/sets/eqtest.smt2 @@ -10,9 +10,9 @@ (declare-fun H () (Set Int) ) (declare-fun I () (Set Int) ) (declare-fun x () Int) -(assert (set.member x (set.intersection (set.union A B) C))) +(assert (set.member x (set.inter (set.union A B) C))) (assert (not (set.member x G))) (assert (= (set.union A B) D)) -(assert (= C (set.intersection E F))) +(assert (= C (set.inter E F))) (assert (and (= F H) (= G H) (= H I))) (check-sat) 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 7e2f627ae..76592a691 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 @@ -6,7 +6,7 @@ (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_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) 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 f6fd4bd53..b0172db39 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 @@ -6,7 +6,7 @@ (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_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (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))) 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 f70d59b16..1538a2e9f 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 @@ -66,7 +66,7 @@ (assert (! (= sk_?X_36$0 FP$0) :named precondition_of_rec_copy_loop_34_11_18)) -(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_38$0 sk_?X_37$0)) +(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_38$0 sk_?X_37$0)) :named precondition_of_rec_copy_loop_34_11_19)) (assert (! (= old_cp_2$0 cp$0) :named assign_41_4)) diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2 index 6857e5147..66f843c9d 100644 --- a/test/regress/regress0/sets/sets-inter.smt2 +++ b/test/regress/regress0/sets/sets-inter.smt2 @@ -5,7 +5,7 @@ (declare-fun b () (Set Int)) (declare-fun x () Int) ;(assert (not (set.member x a))) -(assert (set.member x (set.intersection a b))) +(assert (set.member x (set.inter a b))) (assert (not (set.member x b))) (check-sat) (exit) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index 4a49bef07..0020e5c55 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -8,7 +8,7 @@ (declare-fun x () Int) (assert (set.member x (set.union A B))) -(assert (not (set.member x (set.intersection A B)))) +(assert (not (set.member x (set.inter A B)))) (assert (not (set.member x (set.minus A B)))) ;(assert (not (set.member x (set.minus B A)))) ;(assert (set.member x B)) diff --git a/test/regress/regress0/sets/sets-poly-int-real.smt2 b/test/regress/regress0/sets/sets-poly-int-real.smt2 index 20832c573..00546eee2 100644 --- a/test/regress/regress0/sets/sets-poly-int-real.smt2 +++ b/test/regress/regress0/sets/sets-poly-int-real.smt2 @@ -11,7 +11,7 @@ (assert (= t1 (set.union s (set.singleton 2.5)))) (assert (= t2 (set.union s (set.singleton 2.0)))) (assert (= t3 (set.union r3 (set.singleton 2.5)))) -(assert (= (set.intersection r1 r2) (set.intersection s (set.singleton 0.0)))) +(assert (= (set.inter r1 r2) (set.inter s (set.singleton 0.0)))) (assert (not (= r1 (as set.empty (Set Real))))) (check-sat) diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 index 3dcafae08..4a11bcc78 100644 --- a/test/regress/regress0/sets/sets-sample.smt2 +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -15,12 +15,12 @@ (declare-fun e () Int) (assert (= a (set.singleton 5))) (assert (= c (set.union a b) )) -(assert (not (= c (set.intersection a b) ))) +(assert (not (= c (set.inter a b) ))) (assert (= c (set.minus a b) )) (assert (set.subset a b)) (assert (set.member e c)) (assert (set.member e a)) -(assert (set.member e (set.intersection a b))) +(assert (set.member e (set.inter a b))) (check-sat) (pop 1) diff --git a/test/regress/regress0/sets/sharing-simp.smt2 b/test/regress/regress0/sets/sharing-simp.smt2 index be746be1d..a591792cf 100644 --- a/test/regress/regress0/sets/sharing-simp.smt2 +++ b/test/regress/regress0/sets/sharing-simp.smt2 @@ -9,7 +9,7 @@ (assert (set.member x A)) (assert (set.member y B)) -(assert (or (= C (set.intersection A B)) (= D (set.intersection A B)))) +(assert (or (= C (set.inter A B)) (= D (set.inter A B)))) (check-sat) |