0b55f123 |
1 | /***** tl_spin: tl_rewrt.c *****/ |
2 | |
3 | /* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories. */ |
4 | /* All Rights Reserved. This software is for educational purposes only. */ |
5 | /* No guarantee whatsoever is expressed or implied by the distribution of */ |
6 | /* this code. Permission is given to distribute this code provided that */ |
7 | /* this introductory message is not removed and no monies are exchanged. */ |
8 | /* Software written by Gerard J. Holzmann. For tool documentation see: */ |
9 | /* http://spinroot.com/ */ |
10 | /* Send all bug-reports and/or questions to: bugs@spinroot.com */ |
11 | |
12 | /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */ |
13 | /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */ |
14 | |
15 | #include "tl.h" |
16 | |
17 | extern int tl_verbose; |
18 | |
19 | static Node *can = ZN; |
20 | |
21 | Node * |
22 | right_linked(Node *n) |
23 | { |
24 | if (!n) return n; |
25 | |
26 | if (n->ntyp == AND || n->ntyp == OR) |
27 | while (n->lft && n->lft->ntyp == n->ntyp) |
28 | { Node *tmp = n->lft; |
29 | n->lft = tmp->rgt; |
30 | tmp->rgt = n; |
31 | n = tmp; |
32 | } |
33 | |
34 | n->lft = right_linked(n->lft); |
35 | n->rgt = right_linked(n->rgt); |
36 | |
37 | return n; |
38 | } |
39 | |
40 | Node * |
41 | canonical(Node *n) |
42 | { Node *m; /* assumes input is right_linked */ |
43 | |
44 | if (!n) return n; |
45 | if ((m = in_cache(n)) != ZN) |
46 | return m; |
47 | |
48 | n->rgt = canonical(n->rgt); |
49 | n->lft = canonical(n->lft); |
50 | |
51 | return cached(n); |
52 | } |
53 | |
54 | Node * |
55 | push_negation(Node *n) |
56 | { Node *m; |
57 | |
58 | Assert(n->ntyp == NOT, n->ntyp); |
59 | |
60 | switch (n->lft->ntyp) { |
61 | case TRUE: |
62 | Debug("!true => false\n"); |
63 | releasenode(0, n->lft); |
64 | n->lft = ZN; |
65 | n->ntyp = FALSE; |
66 | break; |
67 | case FALSE: |
68 | Debug("!false => true\n"); |
69 | releasenode(0, n->lft); |
70 | n->lft = ZN; |
71 | n->ntyp = TRUE; |
72 | break; |
73 | case NOT: |
74 | Debug("!!p => p\n"); |
75 | m = n->lft->lft; |
76 | releasenode(0, n->lft); |
77 | n->lft = ZN; |
78 | releasenode(0, n); |
79 | n = m; |
80 | break; |
81 | case V_OPER: |
82 | Debug("!(p V q) => (!p U !q)\n"); |
83 | n->ntyp = U_OPER; |
84 | goto same; |
85 | case U_OPER: |
86 | Debug("!(p U q) => (!p V !q)\n"); |
87 | n->ntyp = V_OPER; |
88 | goto same; |
89 | #ifdef NXT |
90 | case NEXT: |
91 | Debug("!X -> X!\n"); |
92 | n->ntyp = NEXT; |
93 | n->lft->ntyp = NOT; |
94 | n->lft = push_negation(n->lft); |
95 | break; |
96 | #endif |
97 | case AND: |
98 | Debug("!(p && q) => !p || !q\n"); |
99 | n->ntyp = OR; |
100 | goto same; |
101 | case OR: |
102 | Debug("!(p || q) => !p && !q\n"); |
103 | n->ntyp = AND; |
104 | |
105 | same: m = n->lft->rgt; |
106 | n->lft->rgt = ZN; |
107 | |
108 | n->rgt = Not(m); |
109 | n->lft->ntyp = NOT; |
110 | m = n->lft; |
111 | n->lft = push_negation(m); |
112 | break; |
113 | } |
114 | |
115 | return rewrite(n); |
116 | } |
117 | |
118 | static void |
119 | addcan(int tok, Node *n) |
120 | { Node *m, *prev = ZN; |
121 | Node **ptr; |
122 | Node *N; |
123 | Symbol *s, *t; int cmp; |
124 | |
125 | if (!n) return; |
126 | |
127 | if (n->ntyp == tok) |
128 | { addcan(tok, n->rgt); |
129 | addcan(tok, n->lft); |
130 | return; |
131 | } |
132 | |
133 | N = dupnode(n); |
134 | if (!can) |
135 | { can = N; |
136 | return; |
137 | } |
138 | |
139 | s = DoDump(N); |
140 | if (can->ntyp != tok) /* only one element in list so far */ |
141 | { ptr = &can; |
142 | goto insert; |
143 | } |
144 | |
145 | /* there are at least 2 elements in list */ |
146 | prev = ZN; |
147 | for (m = can; m->ntyp == tok && m->rgt; prev = m, m = m->rgt) |
148 | { t = DoDump(m->lft); |
149 | if (t != ZS) |
150 | cmp = strcmp(s->name, t->name); |
151 | else |
152 | cmp = 0; |
153 | if (cmp == 0) /* duplicate */ |
154 | return; |
155 | if (cmp < 0) |
156 | { if (!prev) |
157 | { can = tl_nn(tok, N, can); |
158 | return; |
159 | } else |
160 | { ptr = &(prev->rgt); |
161 | goto insert; |
162 | } } } |
163 | |
164 | /* new entry goes at the end of the list */ |
165 | ptr = &(prev->rgt); |
166 | insert: |
167 | t = DoDump(*ptr); |
168 | cmp = strcmp(s->name, t->name); |
169 | if (cmp == 0) /* duplicate */ |
170 | return; |
171 | if (cmp < 0) |
172 | *ptr = tl_nn(tok, N, *ptr); |
173 | else |
174 | *ptr = tl_nn(tok, *ptr, N); |
175 | } |
176 | |
177 | static void |
178 | marknode(int tok, Node *m) |
179 | { |
180 | if (m->ntyp != tok) |
181 | { releasenode(0, m->rgt); |
182 | m->rgt = ZN; |
183 | } |
184 | m->ntyp = -1; |
185 | } |
186 | |
187 | Node * |
188 | Canonical(Node *n) |
189 | { Node *m, *p, *k1, *k2, *prev, *dflt = ZN; |
190 | int tok; |
191 | |
192 | if (!n) return n; |
193 | |
194 | tok = n->ntyp; |
195 | if (tok != AND && tok != OR) |
196 | return n; |
197 | |
198 | can = ZN; |
199 | addcan(tok, n); |
200 | #if 0 |
201 | Debug("\nA0: "); Dump(can); |
202 | Debug("\nA1: "); Dump(n); Debug("\n"); |
203 | #endif |
204 | releasenode(1, n); |
205 | |
206 | /* mark redundant nodes */ |
207 | if (tok == AND) |
208 | { for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN) |
209 | { k1 = (m->ntyp == AND) ? m->lft : m; |
210 | if (k1->ntyp == TRUE) |
211 | { marknode(AND, m); |
212 | dflt = True; |
213 | continue; |
214 | } |
215 | if (k1->ntyp == FALSE) |
216 | { releasenode(1, can); |
217 | can = False; |
218 | goto out; |
219 | } } |
220 | for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN) |
221 | for (p = can; p; p = (p->ntyp == AND) ? p->rgt : ZN) |
222 | { if (p == m |
223 | || p->ntyp == -1 |
224 | || m->ntyp == -1) |
225 | continue; |
226 | k1 = (m->ntyp == AND) ? m->lft : m; |
227 | k2 = (p->ntyp == AND) ? p->lft : p; |
228 | |
229 | if (isequal(k1, k2)) |
230 | { marknode(AND, p); |
231 | continue; |
232 | } |
233 | if (anywhere(OR, k1, k2)) |
234 | { marknode(AND, p); |
235 | continue; |
236 | } |
237 | } } |
238 | if (tok == OR) |
239 | { for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN) |
240 | { k1 = (m->ntyp == OR) ? m->lft : m; |
241 | if (k1->ntyp == FALSE) |
242 | { marknode(OR, m); |
243 | dflt = False; |
244 | continue; |
245 | } |
246 | if (k1->ntyp == TRUE) |
247 | { releasenode(1, can); |
248 | can = True; |
249 | goto out; |
250 | } } |
251 | for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN) |
252 | for (p = can; p; p = (p->ntyp == OR) ? p->rgt : ZN) |
253 | { if (p == m |
254 | || p->ntyp == -1 |
255 | || m->ntyp == -1) |
256 | continue; |
257 | k1 = (m->ntyp == OR) ? m->lft : m; |
258 | k2 = (p->ntyp == OR) ? p->lft : p; |
259 | |
260 | if (isequal(k1, k2)) |
261 | { marknode(OR, p); |
262 | continue; |
263 | } |
264 | if (anywhere(AND, k1, k2)) |
265 | { marknode(OR, p); |
266 | continue; |
267 | } |
268 | } } |
269 | for (m = can, prev = ZN; m; ) /* remove marked nodes */ |
270 | { if (m->ntyp == -1) |
271 | { k2 = m->rgt; |
272 | releasenode(0, m); |
273 | if (!prev) |
274 | { m = can = can->rgt; |
275 | } else |
276 | { m = prev->rgt = k2; |
277 | /* if deleted the last node in a chain */ |
278 | if (!prev->rgt && prev->lft |
279 | && (prev->ntyp == AND || prev->ntyp == OR)) |
280 | { k1 = prev->lft; |
281 | prev->ntyp = prev->lft->ntyp; |
282 | prev->sym = prev->lft->sym; |
283 | prev->rgt = prev->lft->rgt; |
284 | prev->lft = prev->lft->lft; |
285 | releasenode(0, k1); |
286 | } |
287 | } |
288 | continue; |
289 | } |
290 | prev = m; |
291 | m = m->rgt; |
292 | } |
293 | out: |
294 | #if 0 |
295 | Debug("A2: "); Dump(can); Debug("\n"); |
296 | #endif |
297 | if (!can) |
298 | { if (!dflt) |
299 | fatal("cannot happen, Canonical", (char *) 0); |
300 | return dflt; |
301 | } |
302 | |
303 | return can; |
304 | } |