1 /***** tl_spin: tl_rewrt.c *****/
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
8 * Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
9 * presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
14 extern int tl_verbose;
16 static Node *can = ZN;
29 if (n->ntyp == AND || n->ntyp == OR)
30 while (n->lft && n->lft->ntyp == n->ntyp)
37 n->lft = right_linked(n->lft);
38 n->rgt = right_linked(n->rgt);
45 { Node *m; /* assumes input is right_linked */
48 if ((m = in_cache(n)) != ZN)
51 n->rgt = canonical(n->rgt);
52 n->lft = canonical(n->lft);
58 push_negation(Node *n)
61 Assert(n->ntyp == NOT, n->ntyp);
63 switch (n->lft->ntyp) {
65 Debug("!true => false\n");
66 releasenode(0, n->lft);
71 Debug("!false => true\n");
72 releasenode(0, n->lft);
79 releasenode(0, n->lft);
85 Debug("!(p V q) => (!p U !q)\n");
89 Debug("!(p U q) => (!p V !q)\n");
97 n->lft = push_negation(n->lft);
101 Debug("!(p && q) => !p || !q\n");
105 Debug("!(p || q) => !p && !q\n");
108 same: m = n->lft->rgt;
114 n->lft = push_negation(m);
122 addcan(int tok, Node *n)
123 { Node *m, *prev = ZN;
126 Symbol *s, *t; int cmp;
131 { addcan(tok, n->rgt);
144 { fatal("unexpected error 6", (char *) 0);
146 if (can->ntyp != tok) /* only one element in list so far */
151 /* there are at least 2 elements in list */
153 for (m = can; m->ntyp == tok && m->rgt; prev = m, m = m->rgt)
154 { t = DoDump(m->lft);
156 cmp = strcmp(s->name, t->name);
159 if (cmp == 0) /* duplicate */
163 { can = tl_nn(tok, N, can);
166 { ptr = &(prev->rgt);
170 /* new entry goes at the end of the list */
174 cmp = strcmp(s->name, t->name);
175 if (cmp == 0) /* duplicate */
178 *ptr = tl_nn(tok, N, *ptr);
180 *ptr = tl_nn(tok, *ptr, N);
184 marknode(int tok, Node *m)
187 { releasenode(0, m->rgt);
195 { Node *m, *p, *k1, *k2, *prev, *dflt = ZN;
201 if (tok != AND && tok != OR)
207 Debug("\nA0: "); Dump(can);
208 Debug("\nA1: "); Dump(n); Debug("\n");
212 /* mark redundant nodes */
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)
221 if (k1->ntyp == FALSE)
222 { releasenode(1, can);
226 for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN)
227 for (p = can; p; p = (p->ntyp == AND) ? p->rgt : ZN)
232 k1 = (m->ntyp == AND) ? m->lft : m;
233 k2 = (p->ntyp == AND) ? p->lft : p;
239 if (anywhere(OR, k1, k2))
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)
252 if (k1->ntyp == TRUE)
253 { releasenode(1, can);
257 for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN)
258 for (p = can; p; p = (p->ntyp == OR) ? p->rgt : ZN)
263 k1 = (m->ntyp == OR) ? m->lft : m;
264 k2 = (p->ntyp == OR) ? p->lft : p;
270 if (anywhere(AND, k1, k2))
275 for (m = can, prev = ZN; m; ) /* remove marked nodes */
280 { m = can = can->rgt;
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))
287 prev->ntyp = prev->lft->ntyp;
288 prev->sym = prev->lft->sym;
289 prev->rgt = prev->lft->rgt;
290 prev->lft = prev->lft->lft;
301 Debug("A2: "); Dump(can); Debug("\n");
305 fatal("cannot happen, Canonical", (char *) 0);