1 /***** tl_spin: tl_cache.c *****/
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 */
12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
17 typedef struct Cache {
24 static Cache *stored = (Cache *) 0;
25 static unsigned long Caches, CacheHits;
27 static int ismatch(Node *, Node *);
28 extern void fatal(char *, char *);
29 int sameform(Node *, Node *);
36 printf("\nCACHE DUMP:\n");
37 for (d = stored; d; d = d->nxt, nr++)
38 { if (d->same) continue;
39 printf("B%3d: ", nr); dump(d->before); printf("\n");
40 printf("A%3d: ", nr); dump(d->after); printf("\n");
42 printf("============\n");
50 for (d = stored; d; d = d->nxt, nr++)
51 if (isequal(d->before, n))
53 if (d->same && ismatch(n, d->before)) return n;
54 return dupnode(d->after);
65 if ((m = in_cache(n)) != ZN)
69 d = (Cache *) tl_emalloc(sizeof(Cache));
70 d->before = dupnode(n);
71 d->after = Canonical(n); /* n is released */
73 if (ismatch(d->before, d->after))
75 releasenode(1, d->after);
80 return dupnode(d->after);
86 printf("cache stores : %9ld\n", Caches);
87 printf("cache hits : %9ld\n", CacheHits);
91 releasenode(int all_levels, Node *n)
96 { releasenode(1, n->lft);
98 releasenode(1, n->rgt);
105 tl_nn(int t, Node *ll, Node *rl)
106 { Node *n = (Node *) tl_emalloc(sizeof(Node));
121 n = (Node *) tl_emalloc(sizeof(Node));
123 n->sym = p->sym; /* same name */
136 d->lft = dupnode(n->lft);
137 d->rgt = dupnode(n->rgt);
142 one_lft(int ntyp, Node *x, Node *in)
150 if (in->ntyp != ntyp)
153 if (one_lft(ntyp, x, in->lft))
156 return one_lft(ntyp, x, in->rgt);
160 all_lfts(int ntyp, Node *from, Node *in)
164 if (from->ntyp != ntyp)
165 return one_lft(ntyp, from, in);
167 if (!one_lft(ntyp, from->lft, in))
170 return all_lfts(ntyp, from->rgt, in);
174 sametrees(int ntyp, Node *a, Node *b)
175 { /* toplevel is an AND or OR */
176 /* both trees are right-linked, but the leafs */
177 /* can be in different places in the two trees */
179 if (!all_lfts(ntyp, a, b))
182 return all_lfts(ntyp, b, a);
185 int /* a better isequal() */
186 sameform(Node *a, Node *b)
188 if (!a && !b) return 1;
189 if (!a || !b) return 0;
190 if (a->ntyp != b->ntyp) return 0;
194 && strcmp(a->sym->name, b->sym->name) != 0)
202 if (!a->sym || !b->sym) fatal("sameform...", (char *) 0);
203 return !strcmp(a->sym->name, b->sym->name);
209 return sameform(a->lft, b->lft);
212 if (!sameform(a->lft, b->lft))
214 if (!sameform(a->rgt, b->rgt))
219 case OR: /* the hard case */
220 return sametrees(a->ntyp, a, b);
223 printf("type: %d\n", a->ntyp);
224 fatal("cannot happen, sameform", (char *) 0);
231 isequal(Node *a, Node *b)
238 { if (b->ntyp == TRUE)
241 { if (a->ntyp == TRUE)
246 if (a->ntyp != b->ntyp)
251 && strcmp(a->sym->name, b->sym->name) != 0)
254 if (isequal(a->lft, b->lft)
255 && isequal(a->rgt, b->rgt))
258 return sameform(a, b);
262 ismatch(Node *a, Node *b)
264 if (!a && !b) return 1;
265 if (!a || !b) return 0;
266 if (a->ntyp != b->ntyp) return 0;
270 && strcmp(a->sym->name, b->sym->name) != 0)
273 if (ismatch(a->lft, b->lft)
274 && ismatch(a->rgt, b->rgt))
281 any_term(Node *srch, Node *in)
286 return any_term(srch, in->lft) ||
287 any_term(srch, in->rgt);
289 return isequal(in, srch);
293 any_and(Node *srch, Node *in)
297 if (srch->ntyp == AND)
298 return any_and(srch->lft, in) &&
299 any_and(srch->rgt, in);
301 return any_term(srch, in);
305 any_lor(Node *srch, Node *in)
310 return any_lor(srch, in->lft) ||
311 any_lor(srch, in->rgt);
313 return isequal(in, srch);
317 anywhere(int tok, Node *srch, Node *in)
322 case AND: return any_and(srch, in);
323 case OR: return any_lor(srch, in);
324 case 0: return any_term(srch, in);
326 fatal("cannot happen, anywhere", (char *) 0);