test/regress/regress0/quantifiers/refcount24.cvc


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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112

% Preamble  --------------
DATATYPE UNIT = Unit END;
DATATYPE BOOL = Truth | Falsity END;

% Decls     --------------
resource$type: TYPE;
process$type: TYPE;
null: resource$type;
S$elem$type: TYPE = process$type;
S$t$type: TYPE;
S$empty: S$t$type;
S$mem:(S$elem$type, S$t$type) -> BOOL;
S$add:(S$elem$type, S$t$type) -> S$t$type;
S$remove:(S$elem$type, S$t$type) -> S$t$type;
S$cardinality:(S$t$type) -> INT;
S$mem_empty: BOOLEAN = (FORALL (e: S$elem$type): (NOT ((S$mem((e), (S$empty))) = 
                                                      (Truth))));
ASSERT S$mem_empty;
S$mem_add: BOOLEAN = (FORALL (x: S$elem$type, y: S$elem$type, s: S$t$type): 
                     ((S$mem((x), (S$add((y), (s))))) = (IF (((x) = (y)) OR 
                                                            ((S$mem((x), (s))) = 
                                                            (Truth))) THEN 
                                                        (Truth) ELSE 
                                                        (Falsity) ENDIF)));
ASSERT S$mem_add;
S$mem_remove: BOOLEAN = (FORALL (x: S$elem$type, y: S$elem$type, s: S$t$type): 
                        ((S$mem((x), (S$remove((y), (s))))) = (IF ((NOT 
                                                                   ((x) = 
                                                                   (y))) AND 
                                                                  ((S$mem(
                                                                   (x), (s))) = 
                                                                  (Truth))) THEN 
                                                              (Truth) ELSE 
                                                              (Falsity) ENDIF)));
ASSERT S$mem_remove;
S$card_empty: BOOLEAN = ((S$cardinality((S$empty))) = (0));
ASSERT S$card_empty;
S$card_zero: BOOLEAN = (FORALL (s: S$t$type): (((S$cardinality((s))) = (0)) => 
                                              ((s) = (S$empty))));
ASSERT S$card_zero;
S$card_non_negative: BOOLEAN = (FORALL (s: S$t$type): ((S$cardinality((s))) >= 
                               (0)));
ASSERT S$card_non_negative;
S$card_add: BOOLEAN = (FORALL (x: S$elem$type, s: S$t$type): ((S$cardinality(
                                                              (S$add(
                                                              (x), (s))))) = 
                                                             (IF ((S$mem(
                                                                  (x), (s))) = 
                                                                 (Truth)) THEN 
                                                             (S$cardinality(
                                                             (s))) ELSE (
                                                             (S$cardinality(
                                                             (s))) + 
                                                             (1)) ENDIF)));
ASSERT S$card_add;
S$card_remove: BOOLEAN = (FORALL (x: S$elem$type, s: S$t$type): ((S$cardinality(
                                                                 (S$remove(
                                                                 (x), (s))))) = 
                                                                (IF (
                                                                    (S$mem(
                                                                    (x), (s))) = 
                                                                    (Truth)) THEN (
                                                                (S$cardinality(
                                                                (s))) - 
                                                                (1)) ELSE 
                                                                (S$cardinality(
                                                                (s))) ENDIF)));
ASSERT S$card_remove;

% Var Decls --------------
count: ARRAY resource$type OF INT;
ref: ARRAY process$type OF resource$type;
valid: ARRAY resource$type OF BOOL;
destroy$r: resource$type;
valid$1: ARRAY resource$type OF BOOL;

% Asserts   --------------
ASSERT (NOT ((FORALL (p: process$type): ((NOT 
                                                                    (
                                                                    (
                                                                    (ref)[
                                                                    (p)]) = 
                                                                    (null))) => 
                                                                   ((
                                                                    (valid)[
                                                                    (
                                                                    (ref)[
                                                                    (p)])]) = 
                                                                   (Truth)))) => 
                                       ((NOT ((destroy$r) = (null))) => 
                                       ((((valid)[(destroy$r)]) = (Truth)) => 
                                       ((((count)[(destroy$r)]) = (0)) => 
                                       (((valid$1) = ((valid) WITH [(destroy$r)] := 
                                                     (Falsity))) => (FORALL 
                                                                    (
                                                                    p: process$type): 
                                                                    (
                                                                    (NOT 
                                                                    (
                                                                    (
                                                                    (ref)[
                                                                    (p)]) = 
                                                                    (null))) => 
                                                                    (
                                                                    (
                                                                    (valid$1)[
                                                                    (
                                                                    (ref)[
                                                                    (p)])]) = 
                                                                    (Truth))))))))));
                           
CHECKSAT;