ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
contain.c
Go to the documentation of this file.
1/*
2 * Revision Control Information
3 *
4 * $Source$
5 * $Author$
6 * $Revision$
7 * $Date$
8 *
9 */
10/*
11 contain.c -- set containment routines
12
13 These are complex routines for performing containment over a
14 family of sets, but they have the advantage of being much faster
15 than a straightforward n*n routine.
16
17 First the cubes are sorted by size, and as a secondary key they are
18 sorted so that if two cubes are equal they end up adjacent. We can
19 than quickly remove equal cubes from further consideration by
20 comparing each cube to its neighbor. Finally, because the cubes
21 are sorted by size, we need only check cubes which are larger (or
22 smaller) than a given cube for containment.
23*/
24
25#include "espresso.h"
26
28
29
30
31/*
32 sf_contain -- perform containment on a set family (delete sets which
33 are contained by some larger set in the family). No assumptions are
34 made about A, and the result will be returned in decreasing order of
35 set size.
36*/
38INOUT pset_family A; /* disposes of A */
39{
40 int cnt;
41 pset *A1;
43
44 A1 = sf_sort(A, descend); /* sort into descending order */
45 cnt = rm_equal(A1, descend); /* remove duplicates */
46 cnt = rm_contain(A1); /* remove contained sets */
47 R = sf_unlist(A1, cnt, A->sf_size); /* recreate the set family */
48 sf_free(A);
49 return R;
50}
51
52
53/*
54 sf_rev_contain -- perform containment on a set family (delete sets which
55 contain some smaller set in the family). No assumptions are made about
56 A, and the result will be returned in increasing order of set size
57*/
59INOUT pset_family A; /* disposes of A */
60{
61 int cnt;
62 pset *A1;
64
65 A1 = sf_sort(A, ascend); /* sort into ascending order */
66 cnt = rm_equal(A1, ascend); /* remove duplicates */
67 cnt = rm_rev_contain(A1); /* remove containing sets */
68 R = sf_unlist(A1, cnt, A->sf_size); /* recreate the set family */
69 sf_free(A);
70 return R;
71}
72
73
74/*
75 sf_ind_contain -- perform containment on a set family (delete sets which
76 are contained by some larger set in the family). No assumptions are
77 made about A, and the result will be returned in decreasing order of
78 set size. Also maintains a set of row_indices to track which rows
79 disappear and how the rows end up permuted.
80*/
82INOUT pset_family A; /* disposes of A */
83INOUT int *row_indices; /* updated with the new values */
84{
85 int cnt;
86 pset *A1;
88
89 A1 = sf_sort(A, descend); /* sort into descending order */
90 cnt = rm_equal(A1, descend); /* remove duplicates */
91 cnt = rm_contain(A1); /* remove contained sets */
92 R = sf_ind_unlist(A1, cnt, A->sf_size, row_indices, A->data);
93 sf_free(A);
94 return R;
95}
96
97
98/* sf_dupl -- delete duplicate sets in a set family */
100INOUT pset_family A; /* disposes of A */
101{
102 register int cnt;
103 register pset *A1;
104 pset_family R;
105
106 A1 = sf_sort(A, descend); /* sort the set family */
107 cnt = rm_equal(A1, descend); /* remove duplicates */
108 R = sf_unlist(A1, cnt, A->sf_size); /* recreate the set family */
109 sf_free(A);
110 return R;
111}
112
113
114/*
115 sf_union -- form the contained union of two set families (delete
116 sets which are contained by some larger set in the family). A and
117 B are assumed already sorted in decreasing order of set size (and
118 the SIZE field is assumed to contain the set size), and the result
119 will be returned sorted likewise.
120*/
122INOUT pset_family A, B; /* disposes of A and B */
123{
124 int cnt;
125 pset_family R;
126 pset *A1 = sf_list(A), *B1 = sf_list(B), *E1;
127
128 E1 = ALLOC(pset, MAX(A->count, B->count) + 1);
129 cnt = rm2_equal(A1, B1, E1, descend);
130 cnt += rm2_contain(A1, B1) + rm2_contain(B1, A1);
131 R = sf_merge(A1, B1, E1, cnt, A->sf_size);
132 sf_free(A); sf_free(B);
133 return R;
134}
135
136
137/*
138 dist_merge -- consider all sets to be "or"-ed with "mask" and then
139 delete duplicates from the set family.
140*/
142INOUT pset_family A; /* disposes of A */
143IN pset mask; /* defines variables to mask out */
144{
145 pset *A1;
146 int cnt;
147 pset_family R;
148
149 (void) set_copy(cube.temp[0], mask);
150 A1 = sf_sort(A, d1_order);
151 cnt = d1_rm_equal(A1, d1_order);
152 R = sf_unlist(A1, cnt, A->sf_size);
153 sf_free(A);
154 return R;
155}
156
157
158/*
159 d1merge -- perform an efficient distance-1 merge of cubes of A
160*/
162INOUT pset_family A; /* disposes of A */
163IN int var;
164{
165 return dist_merge(A, cube.var_mask[var]);
166}
167
168
169
170/* d1_rm_equal -- distance-1 merge (merge cubes which are equal under a mask) */
171int d1_rm_equal(A1, compare)
172register pset *A1; /* array of set pointers */
173int (*compare)(); /* comparison function */
174{
175 register int i, j, dest;
176
177 dest = 0;
178 if (A1[0] != (pcube) NULL) {
179 for(i = 0, j = 1; A1[j] != (pcube) NULL; j++)
180 if ( (*compare)(&A1[i], &A1[j]) == 0) {
181 /* if sets are equal (under the mask) merge them */
182 (void) set_or(A1[i], A1[i], A1[j]);
183 } else {
184 /* sets are unequal, so save the set i */
185 A1[dest++] = A1[i];
186 i = j;
187 }
188 A1[dest++] = A1[i];
189 }
190 A1[dest] = (pcube) NULL;
191 return dest;
192}
193
194
195/* rm_equal -- scan a sorted array of set pointers for duplicate sets */
196int rm_equal(A1, compare)
197INOUT pset *A1; /* updated in place */
198IN int (*compare)();
199{
200 register pset *p, *pdest = A1;
201
202 if (*A1 != NULL) { /* If more than one set */
203 for(p = A1+1; *p != NULL; p++)
204 if ((*compare)(p, p-1) != 0)
205 *pdest++ = *(p-1);
206 *pdest++ = *(p-1);
207 *pdest = NULL;
208 }
209 return pdest - A1;
210}
211
212
213/* rm_contain -- perform containment over a sorted array of set pointers */
215INOUT pset *A1; /* updated in place */
216{
217 register pset *pa, *pb;
218 register pset *pcheck = NULL; // Suppress "might be used uninitialized"
219 register pset a, b;
220 pset *pdest = A1;
221 int last_size = -1;
222
223 /* Loop for all cubes of A1 */
224 for(pa = A1; (a = *pa++) != NULL; ) {
225 /* Update the check pointer if the size has changed */
226 if (SIZE(a) != last_size)
227 last_size = SIZE(a), pcheck = pdest;
228 for(pb = A1; pb != pcheck; ) {
229 b = *pb++;
230 INLINEsetp_implies(a, b, /* when_false => */ continue);
231 goto lnext1;
232 }
233 /* set a was not contained by some larger set, so save it */
234 *pdest++ = a;
235 lnext1: ;
236 }
237
238 *pdest = NULL;
239 return pdest - A1;
240}
241
242
243/* rm_rev_contain -- perform rcontainment over a sorted array of set pointers */
245INOUT pset *A1; /* updated in place */
246{
247 register pset *pa, *pb;
248 register pset *pcheck = NULL; // Suppress "might be used uninitialized"
249 register pset a, b;
250 pset *pdest = A1;
251 int last_size = -1;
252
253 /* Loop for all cubes of A1 */
254 for(pa = A1; (a = *pa++) != NULL; ) {
255 /* Update the check pointer if the size has changed */
256 if (SIZE(a) != last_size)
257 last_size = SIZE(a), pcheck = pdest;
258 for(pb = A1; pb != pcheck; ) {
259 b = *pb++;
260 INLINEsetp_implies(b, a, /* when_false => */ continue);
261 goto lnext1;
262 }
263 /* the set a did not contain some smaller set, so save it */
264 *pdest++ = a;
265 lnext1: ;
266 }
267
268 *pdest = NULL;
269 return pdest - A1;
270}
271
272
273/* rm2_equal -- check two sorted arrays of set pointers for equal cubes */
274int rm2_equal(A1, B1, E1, compare)
275INOUT register pset *A1, *B1; /* updated in place */
276OUT pset *E1;
277IN int (*compare)();
278{
279 register pset *pda = A1, *pdb = B1, *pde = E1;
280
281 /* Walk through the arrays advancing pointer to larger cube */
282 for(; *A1 != NULL && *B1 != NULL; )
283 switch((*compare)(A1, B1)) {
284 case -1: /* "a" comes before "b" */
285 *pda++ = *A1++; break;
286 case 0: /* equal cubes */
287 *pde++ = *A1++; B1++; break;
288 case 1: /* "a" is to follow "b" */
289 *pdb++ = *B1++; break;
290 }
291
292 /* Finish moving down the pointers of A and B */
293 while (*A1 != NULL)
294 *pda++ = *A1++;
295 while (*B1 != NULL)
296 *pdb++ = *B1++;
297 *pda = *pdb = *pde = NULL;
298
299 return pde - E1;
300}
301
302
303/* rm2_contain -- perform containment between two arrays of set pointers */
304int rm2_contain(A1, B1)
305INOUT pset *A1; /* updated in place */
306IN pset *B1; /* unchanged */
307{
308 register pset *pa, *pb, a, b, *pdest = A1;
309
310 /* for each set in the first array ... */
311 for(pa = A1; (a = *pa++) != NULL; ) {
312 /* for each set in the second array which is larger ... */
313 for(pb = B1; (b = *pb++) != NULL && SIZE(b) > SIZE(a); ) {
314 INLINEsetp_implies(a, b, /* when_false => */ continue);
315 /* set was contained in some set of B, so don't save pointer */
316 goto lnext1;
317 }
318 /* set wasn't contained in any set of B, so save the pointer */
319 *pdest++ = a;
320 lnext1: ;
321 }
322
323 *pdest = NULL; /* sentinel */
324 return pdest - A1; /* # elements in A1 */
325}
326
327
328
329/* sf_sort -- sort the sets of A */
330pset *sf_sort(A, compare)
332IN int (*compare)();
333{
334 register pset p, last, *pdest, *A1;
335
336 /* Create a single array pointing to each cube of A */
337 pdest = A1 = ALLOC(pset, A->count + 1);
338 foreach_set(A, last, p) {
339 PUTSIZE(p, set_ord(p)); /* compute the set size */
340 *pdest++ = p; /* save the pointer */
341 }
342 *pdest = NULL; /* Sentinel -- never seen by sort */
343
344 /* Sort cubes by size */
345 qsort((char *) A1, (size_t)A->count, sizeof(pset), compare);
346 return A1;
347}
348
349
350/* sf_list -- make a list of pointers to the sets in a set family */
352IN register pset_family A;
353{
354 register pset p, last, *pdest, *A1;
355
356 /* Create a single array pointing to each cube of A */
357 pdest = A1 = ALLOC(pset, A->count + 1);
358 foreach_set(A, last, p)
359 *pdest++ = p; /* save the pointer */
360 *pdest = NULL; /* Sentinel */
361 return A1;
362}
363
364
365/* sf_unlist -- make a set family out of a list of pointers to sets */
366pset_family sf_unlist(A1, totcnt, size)
367IN pset *A1;
368IN int totcnt, size;
369{
370 register pset pr, p, *pa;
371 pset_family R = sf_new(totcnt, size);
372
373 R->count = totcnt;
374 for(pr = R->data, pa = A1; (p = *pa++) != NULL; pr += R->wsize)
375 INLINEset_copy(pr, p);
376 FREE(A1);
377 return R;
378}
379
380
381/* sf_ind_unlist -- make a set family out of a list of pointers to sets */
382pset_family sf_ind_unlist(A1, totcnt, size, row_indices, pfirst)
383IN pset *A1;
384IN int totcnt, size;
385INOUT int *row_indices;
386IN register pset pfirst;
387{
388 register pset pr, p, *pa;
389 register int i, *new_row_indices;
390 pset_family R = sf_new(totcnt, size);
391
392 R->count = totcnt;
393 new_row_indices = ALLOC(int, totcnt);
394 for(pr = R->data, pa = A1, i=0; (p = *pa++) != NULL; pr += R->wsize, i++) {
395 INLINEset_copy(pr, p);
396 new_row_indices[i] = row_indices[(p - pfirst)/R->wsize];
397 }
398 for(i = 0; i < totcnt; i++)
399 row_indices[i] = new_row_indices[i];
400 FREE(new_row_indices);
401 FREE(A1);
402 return R;
403}
404
405
406/* sf_merge -- merge three sorted lists of set pointers */
407pset_family sf_merge(A1, B1, E1, totcnt, size)
408INOUT pset *A1, *B1, *E1; /* will be disposed of */
409IN int totcnt, size;
410{
411 register pset pr, ps, *pmin, *pmid, *pmax;
412 pset_family R;
413 pset *temp[3], *swap;
414 int i, j, n;
415
416 /* Allocate the result set_family */
417 R = sf_new(totcnt, size);
418 R->count = totcnt;
419 pr = R->data;
420
421 /* Quick bubble sort to order the top member of the three arrays */
422 n = 3; temp[0] = A1; temp[1] = B1; temp[2] = E1;
423 for(i = 0; i < n-1; i++)
424 for(j = i+1; j < n; j++)
425 if (desc1(*temp[i], *temp[j]) > 0) {
426 swap = temp[j];
427 temp[j] = temp[i];
428 temp[i] = swap;
429 }
430 pmin = temp[0]; pmid = temp[1]; pmax = temp[2];
431
432 /* Save the minimum element, then update pmin, pmid, pmax */
433 while (*pmin != (pset) NULL) {
434 ps = *pmin++;
435 INLINEset_copy(pr, ps);
436 pr += R->wsize;
437 if (desc1(*pmin, *pmax) > 0) {
438 swap = pmax; pmax = pmin; pmin = pmid; pmid = swap;
439 } else if (desc1(*pmin, *pmid) > 0) {
440 swap = pmin; pmin = pmid; pmid = swap;
441 }
442 }
443
444 FREE(A1);
445 FREE(B1);
446 FREE(E1);
447 return R;
448}
450
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define ALLOC(type, num)
Definition avl.h:27
#define FREE(obj)
Definition avl.h:31
#define MAX(a, b)
Definition avl.h:23
int ascend()
int d1_order()
#define INLINEsetp_implies(a, b, when_false)
Definition espresso.h:228
#define PUTSIZE(set, size)
Definition espresso.h:113
pset_family sf_new()
pset_family sf_contain()
pset_family d1merge()
pset_family sf_ind_unlist()
#define INOUT
Definition espresso.h:334
pset_family sf_dupl()
void sf_free()
#define pcube
Definition espresso.h:261
pset_family sf_unlist()
int rm_equal()
int desc1()
pset_family sf_union()
#define INLINEset_copy(r, a)
Definition espresso.h:195
int rm_contain()
pset_family sf_ind_contain()
struct set_family * pset_family
#define foreach_set(R, last, p)
Definition espresso.h:135
pset_family dist_merge()
#define SIZE(set)
Definition espresso.h:112
int rm2_contain()
pset_family sf_merge()
int rm2_equal()
int set_ord()
pset_family sf_rev_contain()
#define IN
Definition espresso.h:332
unsigned int * pset
Definition espresso.h:73
pset set_or()
int rm_rev_contain()
pset * sf_sort()
int d1_rm_equal()
pset * sf_list()
pset set_copy()
#define OUT
Definition espresso.h:333
Cube * p
Definition exorList.c:222
Definition exor.h:123
int count
Definition espresso.h:80
pset data
Definition espresso.h:82
int wsize
Definition espresso.h:77