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);
This page took 0.036684 seconds and 4 git commands to generate.