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 void
ini_rewrt(void)22 ini_rewrt(void)
23 {
24 can = ZN;
25 }
26
27 Node *
right_linked(Node * n)28 right_linked(Node *n)
29 {
30 if (!n) return n;
31
32 if (n->ntyp == AND || n->ntyp == OR)
33 while (n->lft && n->lft->ntyp == n->ntyp)
34 { Node *tmp = n->lft;
35 n->lft = tmp->rgt;
36 tmp->rgt = n;
37 n = tmp;
38 }
39
40 n->lft = right_linked(n->lft);
41 n->rgt = right_linked(n->rgt);
42
43 return n;
44 }
45
46 Node *
canonical(Node * n)47 canonical(Node *n)
48 { Node *m; /* assumes input is right_linked */
49
50 if (!n) return n;
51 if ((m = in_cache(n)) != ZN)
52 return m;
53
54 n->rgt = canonical(n->rgt);
55 n->lft = canonical(n->lft);
56
57 return cached(n);
58 }
59
60 Node *
push_negation(Node * n)61 push_negation(Node *n)
62 { Node *m;
63
64 Assert(n->ntyp == NOT, n->ntyp);
65
66 switch (n->lft->ntyp) {
67 case TRUE:
68 Debug("!true => false\n");
69 releasenode(0, n->lft);
70 n->lft = ZN;
71 n->ntyp = FALSE;
72 break;
73 case FALSE:
74 Debug("!false => true\n");
75 releasenode(0, n->lft);
76 n->lft = ZN;
77 n->ntyp = TRUE;
78 break;
79 case NOT:
80 Debug("!!p => p\n");
81 m = n->lft->lft;
82 releasenode(0, n->lft);
83 n->lft = ZN;
84 releasenode(0, n);
85 n = m;
86 break;
87 case V_OPER:
88 Debug("!(p V q) => (!p U !q)\n");
89 n->ntyp = U_OPER;
90 goto same;
91 case U_OPER:
92 Debug("!(p U q) => (!p V !q)\n");
93 n->ntyp = V_OPER;
94 goto same;
95 #ifdef NXT
96 case NEXT:
97 Debug("!X -> X!\n");
98 n->ntyp = NEXT;
99 n->lft->ntyp = NOT;
100 n->lft = push_negation(n->lft);
101 break;
102 #endif
103 case AND:
104 Debug("!(p && q) => !p || !q\n");
105 n->ntyp = OR;
106 goto same;
107 case OR:
108 Debug("!(p || q) => !p && !q\n");
109 n->ntyp = AND;
110
111 same: m = n->lft->rgt;
112 n->lft->rgt = ZN;
113
114 n->rgt = Not(m);
115 n->lft->ntyp = NOT;
116 m = n->lft;
117 n->lft = push_negation(m);
118 break;
119 }
120
121 return rewrite(n);
122 }
123
124 static void
addcan(int tok,Node * n)125 addcan(int tok, Node *n)
126 { Node *m, *prev = ZN;
127 Node **ptr;
128 Node *N;
129 Symbol *s, *t; int cmp;
130
131 if (!n) return;
132
133 if (n->ntyp == tok)
134 { addcan(tok, n->rgt);
135 addcan(tok, n->lft);
136 return;
137 }
138
139 N = dupnode(n);
140 if (!can)
141 { can = N;
142 return;
143 }
144
145 s = DoDump(N);
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