diff options
Diffstat (limited to 'test/regress/regress1')
22 files changed, 41 insertions, 41 deletions
diff --git a/test/regress/regress1/bags/choose1.smt2 b/test/regress/regress1/bags/choose1.smt2 index b157bbc70..53cd7c771 100644 --- a/test/regress/regress1/bags/choose1.smt2 +++ b/test/regress/regress1/bags/choose1.smt2 @@ -3,7 +3,7 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (declare-fun a () Int) -(assert (not (= A (as emptybag (Bag Int))))) +(assert (not (= A (as bag.empty (Bag Int))))) (assert (= (bag.choose A) 10)) (assert (= a (bag.choose A))) (assert (exists ((x Int)) (and (= x (bag.choose A)) (= x a)))) diff --git a/test/regress/regress1/bags/choose3.smt2 b/test/regress/regress1/bags/choose3.smt2 index ffa9ae9a7..adf1a3e21 100644 --- a/test/regress/regress1/bags/choose3.smt2 +++ b/test/regress/regress1/bags/choose3.smt2 @@ -4,5 +4,5 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (assert (= (bag.choose A) 10)) -(assert (= A (as emptybag (Bag Int)))) +(assert (= A (as bag.empty (Bag Int)))) (check-sat) diff --git a/test/regress/regress1/bags/choose4.smt2 b/test/regress/regress1/bags/choose4.smt2 index a0290b90b..cdf4065d4 100644 --- a/test/regress/regress1/bags/choose4.smt2 +++ b/test/regress/regress1/bags/choose4.smt2 @@ -3,7 +3,7 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (declare-fun a () Int) -(assert (not (= A (as emptybag (Bag Int))))) +(assert (not (= A (as bag.empty (Bag Int))))) (assert (> (bag.count 10 A) 0)) (assert (= a (bag.choose A))) (check-sat) diff --git a/test/regress/regress1/bags/difference_remove1.smt2 b/test/regress/regress1/bags/difference_remove1.smt2 index f5a87c149..82f6ec53d 100644 --- a/test/regress/regress1/bags/difference_remove1.smt2 +++ b/test/regress/regress1/bags/difference_remove1.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress1/bags/duplicate_removal1.smt2 b/test/regress/regress1/bags/duplicate_removal1.smt2 index 2b662c6e5..27ce2360b 100644 --- a/test/regress/regress1/bags/duplicate_removal1.smt2 +++ b/test/regress/regress1/bags/duplicate_removal1.smt2 @@ -3,6 +3,6 @@ (set-option :produce-models true) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) -(assert (= B (duplicate_removal A))) -(assert (distinct (as emptybag (Bag String)) A B)) +(assert (= B (bag.duplicate_removal A))) +(assert (distinct (as bag.empty (Bag String)) A B)) (check-sat) diff --git a/test/regress/regress1/bags/duplicate_removal2.smt2 b/test/regress/regress1/bags/duplicate_removal2.smt2 index 7dacaae43..5382f773f 100644 --- a/test/regress/regress1/bags/duplicate_removal2.smt2 +++ b/test/regress/regress1/bags/duplicate_removal2.smt2 @@ -2,7 +2,7 @@ (set-info :status unsat) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) -(assert (= B (duplicate_removal A))) -(assert (distinct (as emptybag (Bag String)) A B)) -(assert (= B (union_max A B))) +(assert (= B (bag.duplicate_removal A))) +(assert (distinct (as bag.empty (Bag String)) A B)) +(assert (= B (bag.union_max A B))) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/emptybag1.smt2 b/test/regress/regress1/bags/emptybag1.smt2 index f7f92599d..61b29f414 100644 --- a/test/regress/regress1/bags/emptybag1.smt2 +++ b/test/regress/regress1/bags/emptybag1.smt2 @@ -4,7 +4,7 @@ (declare-fun x () String) (declare-fun y () Int) (assert (= x "x")) -(assert (= A (as emptybag (Bag String)))) +(assert (= A (as bag.empty (Bag String)))) (assert (= (bag.count x A) y)) (assert(> y 1)) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy1.smt2 b/test/regress/regress1/bags/fuzzy1.smt2 index f9fee0ec4..79ccc4b82 100644 --- a/test/regress/regress1/bags/fuzzy1.smt2 +++ b/test/regress/regress1/bags/fuzzy1.smt2 @@ -5,6 +5,6 @@ (declare-fun c () Int) ; c here is zero (assert (and - (= b (difference_subtract b a)) ; b is empty + (= b (bag.difference_subtract b a)) ; b is empty (= a (bag (tuple c 0) 1)))) ; a = {|(<0, 0>, 1)|} (check-sat) diff --git a/test/regress/regress1/bags/fuzzy2.smt2 b/test/regress/regress1/bags/fuzzy2.smt2 index 31da47f53..c7968b274 100644 --- a/test/regress/regress1/bags/fuzzy2.smt2 +++ b/test/regress/regress1/bags/fuzzy2.smt2 @@ -8,8 +8,8 @@ (let ((D (bag d c))) ; when c = zero, then D is empty (and (= a (bag (tuple 1 1) c)) ; when c = zero, then a is empty - (= a (union_max a D)) - (= a (difference_subtract a (bag d 1))) - (= a (union_disjoint a D)) - (= a (intersection_min a D))))) + (= a (bag.union_max a D)) + (= a (bag.difference_subtract a (bag d 1))) + (= a (bag.union_disjoint a D)) + (= a (bag.inter_min a D))))) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy3.smt2 b/test/regress/regress1/bags/fuzzy3.smt2 index dd6dd02dc..a457bf9ae 100644 --- a/test/regress/regress1/bags/fuzzy3.smt2 +++ b/test/regress/regress1/bags/fuzzy3.smt2 @@ -8,6 +8,6 @@ (assert (not (= - (= A (difference_remove (bag d c) A)) + (= A (bag.difference_remove (bag d c) A)) (= A (bag (tuple c c) c))))) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy4.smt2 b/test/regress/regress1/bags/fuzzy4.smt2 index b733a4862..5b24b8d6e 100644 --- a/test/regress/regress1/bags/fuzzy4.smt2 +++ b/test/regress/regress1/bags/fuzzy4.smt2 @@ -7,8 +7,8 @@ (assert (not (= - (= A (bag d (+ c (bag.count d (union_disjoint A A))))) - (= A (difference_remove (bag d c) A))))) + (= A (bag d (+ c (bag.count d (bag.union_disjoint A A))))) + (= A (bag.difference_remove (bag d c) A))))) (assert (= A (bag (tuple 0 0) 5))) (assert (= c (- 5))) (assert (= d (tuple 0 0))) diff --git a/test/regress/regress1/bags/fuzzy5.smt2 b/test/regress/regress1/bags/fuzzy5.smt2 index 2dea236a5..0674fad9c 100644 --- a/test/regress/regress1/bags/fuzzy5.smt2 +++ b/test/regress/regress1/bags/fuzzy5.smt2 @@ -10,7 +10,7 @@ (and (not (= (= A (bag (tuple 0 c) (+ c c))) - (= A (difference_remove (bag d c) A)))) + (= A (bag.difference_remove (bag d c) A)))) (not (= (= A (bag (tuple 0 1) c_plus_1)) (= A (bag (tuple c 1) c_plus_1))))))) diff --git a/test/regress/regress1/bags/intersection_min1.smt2 b/test/regress/regress1/bags/intersection_min1.smt2 index f5a515b9c..0ced4aa89 100644 --- a/test/regress/regress1/bags/intersection_min1.smt2 +++ b/test/regress/regress1/bags/intersection_min1.smt2 @@ -4,7 +4,7 @@ (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) (declare-fun C () (Bag String)) -(assert (= C (intersection_min A B))) -(assert (distinct (as emptybag (Bag String)) C)) +(assert (= C (bag.inter_min A B))) +(assert (distinct (as bag.empty (Bag String)) C)) (assert (distinct A B C)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/intersection_min2.smt2 b/test/regress/regress1/bags/intersection_min2.smt2 index 66afa2f3a..119f34665 100644 --- a/test/regress/regress1/bags/intersection_min2.smt2 +++ b/test/regress/regress1/bags/intersection_min2.smt2 @@ -3,7 +3,7 @@ (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) (declare-fun C () (Bag String)) -(assert (= C (intersection_min A B))) -(assert (= C (union_disjoint A B))) -(assert (distinct (as emptybag (Bag String)) C)) +(assert (= C (bag.inter_min A B))) +(assert (= C (bag.union_disjoint A B))) +(assert (distinct (as bag.empty (Bag String)) C)) (check-sat) diff --git a/test/regress/regress1/bags/issue5759.smt2 b/test/regress/regress1/bags/issue5759.smt2 index ba3752e09..1c29afea6 100644 --- a/test/regress/regress1/bags/issue5759.smt2 +++ b/test/regress/regress1/bags/issue5759.smt2 @@ -4,7 +4,7 @@ (declare-fun A () (Bag Int)) (declare-fun B () (Bag Int)) (declare-fun x () Int) -(assert (not (= A (union_max (bag x 1) (bag 0 1))))) -(assert (= A (union_disjoint B (bag 0 1)))) +(assert (not (= A (bag.union_max (bag x 1) (bag 0 1))))) +(assert (= A (bag.union_disjoint B (bag 0 1)))) (assert (= x 1)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/map1.smt2 b/test/regress/regress1/bags/map1.smt2 index 54d671415..c7dc3d636 100644 --- a/test/regress/regress1/bags/map1.smt2 +++ b/test/regress/regress1/bags/map1.smt2 @@ -5,8 +5,8 @@ (declare-fun x () Int) (declare-fun y () Int) (declare-fun f (Int) Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) (assert (= B (bag.map f A))) (assert (distinct (f x) (f y) x y)) (check-sat) diff --git a/test/regress/regress1/bags/map3.smt2 b/test/regress/regress1/bags/map3.smt2 index 637815fa5..ae0184008 100644 --- a/test/regress/regress1/bags/map3.smt2 +++ b/test/regress/regress1/bags/map3.smt2 @@ -6,5 +6,5 @@ (define-fun f ((x Int)) Int (+ x 1)) (assert (= B (bag.map f A))) (assert (= (bag.count (- 2) B) 57)) -(assert (= A (as emptybag (Bag Int)) )) +(assert (= A (as bag.empty (Bag Int)) )) (check-sat) diff --git a/test/regress/regress1/bags/subbag1.smt2 b/test/regress/regress1/bags/subbag1.smt2 index 055e47a17..7a6bf66d7 100644 --- a/test/regress/regress1/bags/subbag1.smt2 +++ b/test/regress/regress1/bags/subbag1.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (assert (= x 1)) -(assert (subbag A B)) -(assert (subbag B A)) +(assert (bag.subbag A B)) +(assert (bag.subbag B A)) (assert (= (bag.count x A) 5)) (assert (= (bag.count x B) 10)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/subbag2.smt2 b/test/regress/regress1/bags/subbag2.smt2 index 6d5cde362..abdb3b7d9 100644 --- a/test/regress/regress1/bags/subbag2.smt2 +++ b/test/regress/regress1/bags/subbag2.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (subbag A B)) -(assert (subbag B A)) +(assert (bag.subbag A B)) +(assert (bag.subbag B A)) (assert (= (bag.count x A) x)) (assert (= (bag.count y A) x)) (assert (distinct x y)) diff --git a/test/regress/regress1/bags/union_disjoint.smt2 b/test/regress/regress1/bags/union_disjoint.smt2 index d30ed4b14..fdb9d16d3 100644 --- a/test/regress/regress1/bags/union_disjoint.smt2 +++ b/test/regress/regress1/bags/union_disjoint.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_disjoint (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_disjoint (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress1/bags/union_max1.smt2 b/test/regress/regress1/bags/union_max1.smt2 index d278527b9..d41e1425a 100644 --- a/test/regress/regress1/bags/union_max1.smt2 +++ b/test/regress/regress1/bags/union_max1.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bags/union_max2.smt2 b/test/regress/regress1/bags/union_max2.smt2 index dd4bceff5..1366130bf 100644 --- a/test/regress/regress1/bags/union_max2.smt2 +++ b/test/regress/regress1/bags/union_max2.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) -(assert (distinct (as emptybag (Bag Int)) B)) +(assert (distinct (as bag.empty (Bag Int)) B)) (check-sat)
\ No newline at end of file |