blob: 9e1ae5a6222d8fd1e112d47ec9309b8fe000c59e (
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
|
% COMMAND-LINE: --enable-miplib-trick
% EXPECT: sat
tmp1, tmp2, tmp3, tmp4 : INT;
x, y, z : BOOLEAN;
% x = {0, 1}, (NOT x) = 1 - x
% i*Nx + j*Ny + k = 0
% i*x + j*Ny + k = 4
% i*Nx + j*y + k = 6
% i*x + j*y + k = 10
ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0;
ASSERT x AND (NOT y AND TRUE) => tmp1 = 4;
ASSERT NOT x AND ( y AND TRUE) => tmp1 = 6;
ASSERT x AND ( y AND TRUE) => tmp1 = 10;
ASSERT NOT x AND (NOT z AND TRUE) => tmp2 = 0;
ASSERT x AND (NOT z AND TRUE) => tmp2 = 2;
ASSERT NOT x AND ( z AND TRUE) => tmp2 = 9;
ASSERT x AND ( z AND TRUE) => tmp2 = 11;
ASSERT NOT y AND (NOT z AND TRUE) => tmp3 = 0;
ASSERT y AND (NOT z AND TRUE) => tmp3 = 5;
ASSERT NOT y AND ( z AND TRUE) => tmp3 = 16;
ASSERT y AND ( z AND TRUE) => tmp3 = 21;
ASSERT NOT x AND (NOT y AND TRUE) => tmp4 = 0;
ASSERT x AND (NOT y AND TRUE) => tmp4 = 4;
ASSERT NOT x AND ( y AND TRUE) => tmp4 = 6;
ASSERT x AND ( y AND TRUE) => tmp4 = 10;
CHECKSAT;
|
