blob: 20832c573264bc59236113a13fcd69501f7e2a63 (
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 Real))
(declare-fun r2 () (Set Real))
(declare-fun r3 () (Set Real))
(assert (and (set.member 1.5 s) (set.member 0.0 s)))
(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 (not (= r1 (as set.empty (Set Real)))))
(check-sat)
|
