blob: fc2d73235d6e93fe48fce31cbf132301bc839fab (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
; EXPECT: unsat
(set-option :incremental true)
(set-logic ALL)
(declare-fun x () (Set (Tuple Int Int)))
(declare-fun y () (Set (Tuple Int Int)))
(declare-fun z () (Set (Tuple Int Int)))
(declare-fun r () (Set (Tuple Int Int)))
(declare-fun w () (Set (Tuple Int Int)))
(declare-fun f () (Tuple Int Int))
(assert (= f (tuple 3 1)))
(assert (set.member f x))
(declare-fun g () (Tuple Int Int))
(assert (= g (tuple 1 3)))
(assert (set.member g y))
(declare-fun h () (Tuple Int Int))
(assert (= h (tuple 3 5)))
(assert (set.member h x))
(assert (set.member h y))
(assert (= r (rel.join x y)))
(declare-fun a () (Tuple Int))
(assert (= a (tuple 1)))
(declare-fun e () (Tuple Int Int))
(assert (= e (tuple 1 1)))
(assert (let ((_let_1 (set.singleton a))) (= w (rel.product _let_1 _let_1))))
(assert (set.subset (rel.transpose w) y))
(assert (not (set.member e r)))
(assert (not (= z (set.intersection x y))))
(assert (= z (set.minus x y)))
(assert (set.subset x y))
(assert (set.member e (rel.join r z)))
(assert (set.member e x))
(assert (set.member e (set.intersection x y)))
(push 1)
(assert true)
(check-sat)
(pop 1)
|
