blob: 5b1ecefd8ab152e926a19597c6e07f62dfd8ec39 (
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
43
44
45
46
47
48
49
|
% EXPECT: unsat
OPTION "logic" "ALL_SUPPORTED";
Atom : TYPE;
AtomTup : TYPE = [Atom];
AtomBinTup : TYPE = [Atom, Atom];
AtomTerTup : TYPE = [Atom, Atom, Atom];
Target: SET OF AtomTup;
Name: SET OF AtomTup;
Addr: SET OF AtomTup;
Book: SET OF AtomTup;
names: SET OF AtomBinTup;
addr: SET OF AtomTerTup;
b1: Atom;
b1_tup : AtomTup;
ASSERT b1_tup = TUPLE(b1);
ASSERT b1_tup IS_IN Book;
b2: Atom;
b2_tup : AtomTup;
ASSERT b2_tup = TUPLE(b2);
ASSERT b2_tup IS_IN Book;
b3: Atom;
b3_tup : AtomTup;
ASSERT b3_tup = TUPLE(b3);
ASSERT b3_tup IS_IN Book;
n: Atom;
n_tup : AtomTup;
ASSERT n_tup = TUPLE(n);
ASSERT n_tup IS_IN Name;
t: Atom;
t_tup : AtomTup;
ASSERT t_tup = TUPLE(t);
ASSERT t_tup IS_IN Target;
ASSERT ((Book JOIN addr) JOIN Target) <= Name;
ASSERT (Book JOIN names) <= Name;
ASSERT (Name & Addr) = {}::SET OF AtomTup;
ASSERT ({n_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup;
ASSERT ({n_tup} JOIN ({b2_tup} JOIN addr)) = ({n_tup} JOIN ({b1_tup} JOIN addr)) | {t_tup};
ASSERT ({n_tup} JOIN ({b3_tup} JOIN addr)) = ({n_tup} JOIN ({b2_tup} JOIN addr)) - {t_tup};
ASSERT NOT (({n_tup} JOIN ({b1_tup} JOIN addr)) = ({n_tup} JOIN ({b3_tup} JOIN addr)));
CHECKSAT;
|
