blob: a27be5b4bed7812ac90012ef7c7ec1d8ce7eb715 (
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
|
; EXPECT: unsat
(set-option :incremental false)
(set-logic ALL)
(declare-sort Atom 0)
(declare-fun Target () (Set (Tuple Atom)))
(declare-fun Name () (Set (Tuple Atom)))
(declare-fun Addr () (Set (Tuple Atom)))
(declare-fun Book () (Set (Tuple Atom)))
(declare-fun names () (Set (Tuple Atom Atom)))
(declare-fun addr () (Set (Tuple Atom Atom Atom)))
(declare-fun b1 () Atom)
(declare-fun b1_tup () (Tuple Atom))
(assert (= b1_tup (mkTuple b1)))
(assert (member b1_tup Book))
(declare-fun b2 () Atom)
(declare-fun b2_tup () (Tuple Atom))
(assert (= b2_tup (mkTuple b2)))
(assert (member b2_tup Book))
(declare-fun b3 () Atom)
(declare-fun b3_tup () (Tuple Atom))
(assert (= b3_tup (mkTuple b3)))
(assert (member b3_tup Book))
(declare-fun n () Atom)
(declare-fun n_tup () (Tuple Atom))
(assert (= n_tup (mkTuple n)))
(assert (member n_tup Name))
(declare-fun t () Atom)
(declare-fun t_tup () (Tuple Atom))
(assert (= t_tup (mkTuple t)))
(assert (member t_tup Target))
(assert (subset (join (join Book addr) Target) Name))
(assert (subset (join Book names) Name))
(assert (= (intersection Name Addr) (as emptyset (Set (Tuple Atom)))))
(assert (= (join (singleton n_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom)))))
(assert (let ((_let_1 (singleton n_tup))) (= (join _let_1 (join (singleton b2_tup) addr)) (union (join _let_1 (join (singleton b1_tup) addr)) (singleton t_tup)))))
(assert (let ((_let_1 (singleton n_tup))) (= (join _let_1 (join (singleton b3_tup) addr)) (setminus (join _let_1 (join (singleton b2_tup) addr)) (singleton t_tup)))))
(assert (let ((_let_1 (singleton n_tup))) (not (= (join _let_1 (join (singleton b1_tup) addr)) (join _let_1 (join (singleton b3_tup) addr))))))
(check-sat)
|
