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
|
% EXPECT: sat
OPTION "logic" "ALL_SUPPORTED";
IntPair: TYPE = [INT, INT];
IntPairPair: TYPE = [INT, INT, INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
z : SET OF IntPairPair;
z1 : SET OF IntPair;
w1 : SET OF IntPair;
z2 : SET OF IntPair;
w2 : SET OF IntPair;
%ASSERT NOT (0,1,2,3) IS_IN (x PRODUCT y);
ASSERT NOT( z = (x PRODUCT y) );
ASSERT (0,1,2,3) IS_IN z;
ASSERT (0,1) IS_IN z1;
ASSERT (0,1) IS_IN z2;
ASSERT (2,3) IS_IN w1;
ASSERT (2,3) IS_IN w2;
ASSERT ( x = z1 AND y = w1 ) OR ( x = z2 AND y = w2 );
CHECKSAT;
|
