blob: 9bc85f268da50d564b29cf6a7a9d37d3128435e5 (
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 (tuple b1)))
(assert (set.member b1_tup Book))
(declare-fun b2 () Atom)
(declare-fun b2_tup () (Tuple Atom))
(assert (= b2_tup (tuple b2)))
(assert (set.member b2_tup Book))
(declare-fun b3 () Atom)
(declare-fun b3_tup () (Tuple Atom))
(assert (= b3_tup (tuple b3)))
(assert (set.member b3_tup Book))
(declare-fun n () Atom)
(declare-fun n_tup () (Tuple Atom))
(assert (= n_tup (tuple n)))
(assert (set.member n_tup Name))
(declare-fun t () Atom)
(declare-fun t_tup () (Tuple Atom))
(assert (= t_tup (tuple t)))
(assert (set.member t_tup Target))
(assert (set.subset (rel.join (rel.join Book addr) Target) Name))
(assert (set.subset (rel.join Book names) Name))
(assert (= (set.inter Name Addr) (as set.empty (Set (Tuple Atom)))))
(assert (= (rel.join (set.singleton n_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Set (Tuple Atom)))))
(assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.union (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (set.singleton t_tup)))))
(assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b3_tup) addr)) (set.minus (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.singleton t_tup)))))
(assert (let ((_let_1 (set.singleton n_tup))) (not (= (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (rel.join _let_1 (rel.join (set.singleton b3_tup) addr))))))
(check-sat)
|
