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