ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
unate.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 * unate.c -- routines for dealing with unate functions
12 */
13
14#include "espresso.h"
15
17
18
19static pset_family abs_covered();
20static pset_family abs_covered_many();
21static int abs_select_restricted();
22
24pcube *T;
25{
26 register unsigned int word_test, word_set, bit_test, bit_set;
27 register pcube p, pA;
29 pcube *T1;
30 int ncol, i;
31
32 A = sf_new(CUBELISTSIZE(T), cdata.vars_unate);
33 A->count = CUBELISTSIZE(T);
34 foreachi_set(A, i, p) {
35 (void) set_clear(p, A->sf_size);
36 }
37 ncol = 0;
38
39 for(i = 0; i < cube.size; i++) {
40 if (cdata.part_zeros[i] > 0) {
41 assert(ncol <= cdata.vars_unate);
42
43 /* Copy a column from T to A */
44 word_test = WHICH_WORD(i);
45 bit_test = 1 << WHICH_BIT(i);
46 word_set = WHICH_WORD(ncol);
47 bit_set = 1 << WHICH_BIT(ncol);
48
49 pA = A->data;
50 for(T1 = T+2; (p = *T1++) != 0; ) {
51 if ((p[word_test] & bit_test) == 0) {
52 pA[word_set] |= bit_set;
53 }
54 pA += A->wsize;
55 }
56
57 ncol++;
58 }
59 }
60
61 return A;
62}
63
66{
67 register int i, ncol, lp;
68 register pcube p, pB;
69 int var, nunate, *unate;
70 pcube last;
72
73 B = sf_new(A->count, cube.size);
74 B->count = A->count;
75
76 /* Find the unate variables */
77 unate = ALLOC(int, cube.num_vars);
78 nunate = 0;
79 for(var = 0; var < cube.num_vars; var++) {
80 if (cdata.is_unate[var]) {
81 unate[nunate++] = var;
82 }
83 }
84
85 /* Loop for each set of A */
86 pB = B->data;
87 foreach_set(A, last, p) {
88
89 /* Initialize this set of B */
90 INLINEset_fill(pB, cube.size);
91
92 /* Now loop for the unate variables; if the part is in A,
93 * then this variable of B should be a single 1 in the unate
94 * part.
95 */
96 for(ncol = 0; ncol < nunate; ncol++) {
97 if (is_in_set(p, ncol)) {
98 lp = cube.last_part[unate[ncol]];
99 for(i = cube.first_part[unate[ncol]]; i <= lp; i++) {
100 if (cdata.part_zeros[i] == 0) {
101 set_remove(pB, i);
102 }
103 }
104 }
105 }
106 pB += B->wsize;
107 }
108
109 FREE(unate);
110 return B;
111}
112
113/*
114 * unate_compl
115 */
116
119{
120 register pset p, last;
121
122 /* Make sure A is single-cube containment minimal */
123/* A = sf_rev_contain(A);*/
124
125 foreach_set(A, last, p) {
126 PUTSIZE(p, set_ord(p));
127 }
128
129 /* Recursively find the complement */
130 A = unate_complement(A);
131
132 /* Now, we can guarantee a minimal result by containing the result */
133 A = sf_rev_contain(A);
134 return A;
135}
136
137
138/*
139 * Assume SIZE(p) records the size of each set
140 */
142pset_family A; /* disposes of A */
143{
144 pset_family Abar;
145 register pset p, p1, restrict;
146 register int i;
147 int max_i, min_set_ord, j;
148
149 /* Check for no sets in the matrix -- complement is the universe */
150 if (A->count == 0) {
151 sf_free(A);
152 Abar = sf_new(1, A->sf_size);
153 (void) set_clear(GETSET(Abar, Abar->count++), A->sf_size);
154
155 /* Check for a single set in the maxtrix -- compute de Morgan complement */
156 } else if (A->count == 1) {
157 p = A->data;
158 Abar = sf_new(A->sf_size, A->sf_size);
159 for(i = 0; i < A->sf_size; i++) {
160 if (is_in_set(p, i)) {
161 p1 = set_clear(GETSET(Abar, Abar->count++), A->sf_size);
162 set_insert(p1, i);
163 }
164 }
165 sf_free(A);
166
167 } else {
168
169 /* Select splitting variable as the variable which belongs to a set
170 * of the smallest size, and which has greatest column count
171 */
172 restrict = set_new(A->sf_size);
173 min_set_ord = A->sf_size + 1;
174 foreachi_set(A, i, p) {
175 if (SIZE(p) < min_set_ord) {
176 set_copy(restrict, p);
177 min_set_ord = SIZE(p);
178 } else if (SIZE(p) == min_set_ord) {
179 set_or(restrict, restrict, p);
180 }
181 }
182
183 /* Check for no data (shouldn't happen ?) */
184 if (min_set_ord == 0) {
185 A->count = 0;
186 Abar = A;
187
188 /* Check for "essential" columns */
189 } else if (min_set_ord == 1) {
190 Abar = unate_complement(abs_covered_many(A, restrict));
191 sf_free(A);
192 foreachi_set(Abar, i, p) {
193 set_or(p, p, restrict);
194 }
195
196 /* else, recur as usual */
197 } else {
198 max_i = abs_select_restricted(A, restrict);
199
200 /* Select those rows of A which are not covered by max_i,
201 * recursively find all minimal covers of these rows, and
202 * then add back in max_i
203 */
204 Abar = unate_complement(abs_covered(A, max_i));
205 foreachi_set(Abar, i, p) {
206 set_insert(p, max_i);
207 }
208
209 /* Now recur on A with all zero's on column max_i */
210 foreachi_set(A, i, p) {
211 if (is_in_set(p, max_i)) {
212 set_remove(p, max_i);
213 j = SIZE(p) - 1;
214 PUTSIZE(p, j);
215 }
216 }
217
218 Abar = sf_append(Abar, unate_complement(A));
219 }
220 set_free(restrict);
221 }
222
223 return Abar;
224}
225
228{
229 register pset p, last, p1;
230 register int i, n;
231 int lev, lvl;
232 pset nlast;
233 pset_family temp;
234 long start = ptime();
235 struct {
236 pset_family sf;
237 int level;
238 } stack[32]; /* 32 suffices for 2 ** 32 cubes ! */
239
240 if (T->count <= 0)
241 return sf_new(1, T->sf_size);
242 for(n = T->count, lev = 0; n != 0; n >>= 1, lev++) ;
243
244 /* A simple heuristic ordering */
245 T = lex_sort(sf_save(T));
246
247 /* Push a full set on the stack to get things started */
248 n = 1;
249 stack[0].sf = sf_new(1, T->sf_size);
250 stack[0].level = lev;
251 set_fill(GETSET(stack[0].sf, stack[0].sf->count++), T->sf_size);
252
253 nlast = GETSET(T, T->count - 1);
254 foreach_set(T, last, p) {
255
256 /* "unstack" the set into a family */
257 temp = sf_new(set_ord(p), T->sf_size);
258 for(i = 0; i < T->sf_size; i++)
259 if (is_in_set(p, i)) {
260 p1 = set_fill(GETSET(temp, temp->count++), T->sf_size);
261 set_remove(p1, i);
262 }
263 stack[n].sf = temp;
264 stack[n++].level = lev;
265
266 /* Pop the stack and perform (leveled) intersections */
267 while (n > 1 && (stack[n-1].level==stack[n-2].level || p == nlast)) {
268 temp = unate_intersect(stack[n-1].sf, stack[n-2].sf, FALSE);
269 lvl = MIN(stack[n-1].level, stack[n-2].level) - 1;
270 if (debug & MINCOV && lvl < 10) {
271 printf("# EXACT_MINCOV[%d]: %4d = %4d x %4d, time = %s\n",
272 lvl, temp->count, stack[n-1].sf->count,
273 stack[n-2].sf->count, print_time(ptime() - start));
274 (void) fflush(stdout);
275 }
276 sf_free(stack[n-2].sf);
277 sf_free(stack[n-1].sf);
278 stack[n-2].sf = temp;
279 stack[n-2].level = lvl;
280 n--;
281 }
282 }
283
284 temp = stack[0].sf;
285 p1 = set_fill(set_new(T->sf_size), T->sf_size);
286 foreach_set(temp, last, p)
287 INLINEset_diff(p, p1, p);
288 set_free(p1);
289 if (debug & MINCOV1) {
290 printf("MINCOV: family of all minimal coverings is\n");
291 sf_print(temp);
292 }
293 sf_free(T); /* this is the copy of T we made ... */
294 return temp;
295}
296
297/*
298 * unate_intersect -- intersect two unate covers
299 *
300 * If largest_only is TRUE, then only the largest cube(s) are returned
301 */
302
303#define MAGIC 500 /* save 500 cubes before containment */
304
305pset_family unate_intersect(A, B, largest_only)
306pset_family A, B;
307bool largest_only;
308{
309 register pset pi, pj, lasti, lastj, pt;
310 pset_family T, Tsave;
311 bool save;
312 int maxord, ord;
313
314 /* How large should each temporary result cover be ? */
315 T = sf_new(MAGIC, A->sf_size);
316 Tsave = NULL;
317 maxord = 0;
318 pt = T->data;
319
320 /* Form pairwise intersection of each set of A with each cube of B */
321 foreach_set(A, lasti, pi) {
322
323 foreach_set(B, lastj, pj) {
324
325 save = set_andp(pt, pi, pj);
326
327 /* Check if we want the largest only */
328 if (save && largest_only) {
329 if ((ord = set_ord(pt)) > maxord) {
330 /* discard Tsave and T */
331 if (Tsave != NULL) {
332 sf_free(Tsave);
333 Tsave = NULL;
334 }
335 pt = T->data;
336 T->count = 0;
337 /* Re-create pt (which was just thrown away) */
338 (void) set_and(pt, pi, pj);
339 maxord = ord;
340 } else if (ord < maxord) {
341 save = FALSE;
342 }
343 }
344
345 if (save) {
346 if (++T->count >= T->capacity) {
347 T = sf_contain(T);
348 Tsave = (Tsave == NULL) ? T : sf_union(Tsave, T);
349 T = sf_new(MAGIC, A->sf_size);
350 pt = T->data;
351 } else {
352 pt += T->wsize;
353 }
354 }
355 }
356 }
357
358
359 /* Contain the final result and merge it into Tsave */
360 T = sf_contain(T);
361 Tsave = (Tsave == NULL) ? T : sf_union(Tsave, T);
362
363 return Tsave;
364}
365
366/*
367 * abs_covered -- after selecting a new column for the selected set,
368 * create a new matrix which is only those rows which are still uncovered
369 */
370static pset_family
371abs_covered(A, pick)
373register int pick;
374{
375 register pset last, p, pdest;
376 register pset_family Aprime;
377
378 Aprime = sf_new(A->count, A->sf_size);
379 pdest = Aprime->data;
380 foreach_set(A, last, p)
381 if (! is_in_set(p, pick)) {
382 INLINEset_copy(pdest, p);
383 Aprime->count++;
384 pdest += Aprime->wsize;
385 }
386 return Aprime;
387}
388
389
390/*
391 * abs_covered_many -- after selecting many columns for ther selected set,
392 * create a new matrix which is only those rows which are still uncovered
393 */
394static pset_family
395abs_covered_many(A, pick_set)
397register pset pick_set;
398{
399 register pset last, p, pdest;
400 register pset_family Aprime;
401
402 Aprime = sf_new(A->count, A->sf_size);
403 pdest = Aprime->data;
404 foreach_set(A, last, p)
405 if (setp_disjoint(p, pick_set)) {
406 INLINEset_copy(pdest, p);
407 Aprime->count++;
408 pdest += Aprime->wsize;
409 }
410 return Aprime;
411}
412
413
414/*
415 * abs_select_restricted -- select the column of maximum column count which
416 * also belongs to the set "restrict"; weight each column of a set as
417 * 1 / (set_ord(p) - 1).
418 */
419static int
420abs_select_restricted(A, restrict)
422pset restrict;
423{
424 register int i, best_var, best_count, *count;
425
426 /* Sum the elements in these columns */
427 count = sf_count_restricted(A, restrict);
428
429 /* Find which variable has maximum weight */
430 best_var = -1;
431 best_count = 0;
432 for(i = 0; i < A->sf_size; i++) {
433 if (count[i] > best_count) {
434 best_var = i;
435 best_count = count[i];
436 }
437 }
438 FREE(count);
439
440 if (best_var == -1)
441 fatal("abs_select_restricted: should not have best_var == -1");
442
443 return best_var;
444}
446
#define FALSE
Definition abcBm.c:37
#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 pcover
Definition espresso.h:264
#define INLINEset_diff(r, a, b)
Definition espresso.h:208
pset_family unate_complement()
pcover map_unate_to_cover()
#define PUTSIZE(set, size)
Definition espresso.h:113
#define is_in_set(set, e)
Definition espresso.h:170
#define set_free(r)
Definition espresso.h:167
pset_family sf_new()
#define foreachi_set(R, i, p)
Definition espresso.h:143
#define set_new(size)
Definition espresso.h:164
#define MINCOV
Definition espresso.h:362
#define set_insert(set, e)
Definition espresso.h:172
bool setp_disjoint()
pset_family exact_minimum_cover()
pset set_and()
void sf_print()
pset_family sf_contain()
void fatal()
#define print_time(t)
Definition espresso.h:22
void sf_free()
#define pcube
Definition espresso.h:261
#define WHICH_WORD(element)
Definition espresso.h:87
#define GETSET(family, index)
Definition espresso.h:161
pset_family sf_union()
pcover map_cover_to_unate()
#define INLINEset_copy(r, a)
Definition espresso.h:195
pset_family sf_save()
#define set_remove(set, e)
Definition espresso.h:171
pset set_fill()
struct set_family * pset_family
#define MINCOV1
Definition espresso.h:363
#define foreach_set(R, last, p)
Definition espresso.h:135
pset_family unate_compl()
unsigned int debug
Definition globals.c:19
#define SIZE(set)
Definition espresso.h:112
int set_ord()
#define INLINEset_fill(r, size)
Definition espresso.h:199
pset_family sf_rev_contain()
#define IN
Definition espresso.h:332
pset set_clear()
pcover lex_sort()
#define WHICH_BIT(element)
Definition espresso.h:88
unsigned int * pset
Definition espresso.h:73
bool set_andp()
pset set_or()
pset_family unate_intersect()
pset_family sf_append()
pset set_copy()
int * sf_count_restricted()
#define CUBELISTSIZE(T)
Definition espresso.h:329
Cube * p
Definition exorList.c:222
#define MAGIC
Definition sharp.c:214
Definition exor.h:123
int count
Definition espresso.h:80
int capacity
Definition espresso.h:79
pset data
Definition espresso.h:82
int wsize
Definition espresso.h:77
int sf_size
Definition espresso.h:78
#define assert(ex)
Definition util_old.h:213
#define ptime()
Definition util_old.h:283
#define MIN(a, b)
Definition util_old.h:256