blob: 7a6ac7d5bba29d98c7e790b2db6cad63d727296b (
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
|
; 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 m () Atom)
(declare-fun m_tup () (Tuple Atom))
(assert (= m_tup (mkTuple m)))
(assert (member m_tup Name))
(declare-fun t () Atom)
(declare-fun t_tup () (Tuple Atom))
(assert (= t_tup (mkTuple t)))
(assert (member t_tup Target))
(assert (= (join (singleton m_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom)))))
(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (mkTuple m t)))))
(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (mkTuple m t)))))
(assert (not (= (join (singleton b1_tup) addr) (join (singleton b3_tup) addr))))
(check-sat)
|
