blob: 407e95d3c64ab0ae042186f03ad3c111ec1c5971 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(set-logic QF_UFLIRAFS)
(set-info :status sat)
(declare-fun s () (Set Real))
(declare-fun t1 () (Set Real))
(declare-fun t2 () (Set Real))
(declare-fun t3 () (Set Real))
(declare-fun r1 () (Set Int))
(declare-fun r2 () (Set Int))
(declare-fun r3 () (Set Int))
(assert (and (member 1.5 s) (member 0 s)))
(assert (= t1 (union s (singleton 2.5))))
(assert (= t2 (union s (singleton 2))))
(assert (= t3 (union r3 (singleton 2.5))))
(assert (= (intersection r1 r2) (intersection s (singleton 0))))
(assert (not (= r1 (as emptyset (Set Real)))))
(check-sat)
|
