ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
compl.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 * module: compl.c
12 * purpose: compute the complement of a multiple-valued function
13 *
14 * The "unate recursive paradigm" is used. After a set of special
15 * cases are examined, the function is split on the "most active
16 * variable". These two halves are complemented recursively, and then
17 * the results are merged.
18 *
19 * Changes (from Version 2.1 to Version 2.2)
20 * 1. Minor bug in compl_lifting -- cubes in the left half were
21 * not marked as active, so that when merging a leaf from the left
22 * hand side, the active flags were essentially random. This led
23 * to minor impredictability problem, but never affected the
24 * accuracy of the results.
25 */
26
27#include "espresso.h"
28
30
31
32#define USE_COMPL_LIFT 0
33#define USE_COMPL_LIFT_ONSET 1
34#define USE_COMPL_LIFT_ONSET_COMPLEX 2
35#define NO_LIFTING 3
36
37static bool compl_special_cases();
38static pcover compl_merge();
39static void compl_d1merge();
40static pcover compl_cube();
41static void compl_lift();
42static void compl_lift_onset();
43static void compl_lift_onset_complex();
44static bool simp_comp_special_cases();
45static bool simplify_special_cases();
46
47
48/* complement -- compute the complement of T */
50pcube *T; /* T will be disposed of */
51{
52 register pcube cl, cr;
53 register int best;
54 pcover Tbar, Tl, Tr;
55 int lifting;
56 static int compl_level = 0;
57
58 if (debug & COMPL)
59 debug_print(T, "COMPLEMENT", compl_level++);
60
61 if (compl_special_cases(T, &Tbar) == MAYBE) {
62
63 /* Allocate space for the partition cubes */
64 cl = new_cube();
65 cr = new_cube();
66 best = binate_split_select(T, cl, cr, COMPL);
67
68 /* Complement the left and right halves */
69 Tl = complement(scofactor(T, cl, best));
70 Tr = complement(scofactor(T, cr, best));
71
72 if (Tr->count*Tl->count > (Tr->count+Tl->count)*CUBELISTSIZE(T)) {
73 lifting = USE_COMPL_LIFT_ONSET;
74 } else {
75 lifting = USE_COMPL_LIFT;
76 }
77 Tbar = compl_merge(T, Tl, Tr, cl, cr, best, lifting);
78
79 free_cube(cl);
80 free_cube(cr);
82 }
83
84 if (debug & COMPL)
85 debug1_print(Tbar, "exit COMPLEMENT", --compl_level);
86 return Tbar;
87}
88
89static bool compl_special_cases(T, Tbar)
90pcube *T; /* will be disposed if answer is determined */
91pcover *Tbar; /* returned only if answer determined */
92{
93 register pcube *T1, p, ceil, cof=T[0];
94 pcover A, ceil_compl;
95
96 /* Check for no cubes in the cover */
97 if (T[2] == NULL) {
98 *Tbar = sf_addset(new_cover(1), cube.fullset);
100 return TRUE;
101 }
102
103 /* Check for only a single cube in the cover */
104 if (T[3] == NULL) {
105 *Tbar = compl_cube(set_or(cof, cof, T[2]));
106 free_cubelist(T);
107 return TRUE;
108 }
109
110 /* Check for a row of all 1's (implies complement is null) */
111 for(T1 = T+2; (p = *T1++) != NULL; ) {
112 if (full_row(p, cof)) {
113 *Tbar = new_cover(0);
114 free_cubelist(T);
115 return TRUE;
116 }
117 }
118
119 /* Check for a column of all 0's which can be factored out */
120 ceil = set_save(cof);
121 for(T1 = T+2; (p = *T1++) != NULL; ) {
122 INLINEset_or(ceil, ceil, p);
123 }
124 if (! setp_equal(ceil, cube.fullset)) {
125 ceil_compl = compl_cube(ceil);
126 (void) set_or(cof, cof, set_diff(ceil, cube.fullset, ceil));
127 set_free(ceil);
128 *Tbar = sf_append(complement(T), ceil_compl);
129 return TRUE;
130 }
131 set_free(ceil);
132
133 /* Collect column counts, determine unate variables, etc. */
134 massive_count(T);
135
136 /* If single active variable not factored out above, then tautology ! */
137 if (cdata.vars_active == 1) {
138 *Tbar = new_cover(0);
139 free_cubelist(T);
140 return TRUE;
141
142 /* Check for unate cover */
143 } else if (cdata.vars_unate == cdata.vars_active) {
144 A = map_cover_to_unate(T);
145 free_cubelist(T);
146 A = unate_compl(A);
147 *Tbar = map_unate_to_cover(A);
148 sf_free(A);
149 return TRUE;
150
151 /* Not much we can do about it */
152 } else {
153 return MAYBE;
154 }
155}
156
157/*
158 * compl_merge -- merge the two cofactors around the splitting
159 * variable
160 *
161 * The merge operation involves intersecting each cube of the left
162 * cofactor with cl, and intersecting each cube of the right cofactor
163 * with cr. The union of these two covers is the merged result.
164 *
165 * In order to reduce the number of cubes, a distance-1 merge is
166 * performed (note that two cubes can only combine distance-1 in the
167 * splitting variable). Also, a simple expand is performed in the
168 * splitting variable (simple implies the covering check for the
169 * expansion is not full containment, but single-cube containment).
170 */
171
172static pcover compl_merge(T1, L, R, cl, cr, var, lifting)
173pcube *T1; /* Original ON-set */
174pcover L, R; /* Complement from each recursion branch */
175register pcube cl, cr; /* cubes used for cofactoring */
176int var; /* splitting variable */
177int lifting; /* whether to perform lifting or not */
178{
179 register pcube p, last, pt;
180 pcover T, Tbar;
181 pcube *L1, *R1;
182
183 if (debug & COMPL) {
184 (void) printf("compl_merge: left %d, right %d\n", L->count, R->count);
185 (void) printf("%s (cl)\n%s (cr)\nLeft is\n", pc1(cl), pc2(cr));
186 cprint(L);
187 (void) printf("Right is\n");
188 cprint(R);
189 }
190
191 /* Intersect each cube with the cofactored cube */
192 foreach_set(L, last, p) {
193 INLINEset_and(p, p, cl);
194 SET(p, ACTIVE);
195 }
196 foreach_set(R, last, p) {
197 INLINEset_and(p, p, cr);
198 SET(p, ACTIVE);
199 }
200
201 /* Sort the arrays for a distance-1 merge */
202 (void) set_copy(cube.temp[0], cube.var_mask[var]);
203 qsort((char *) (L1 = sf_list(L)), (size_t)L->count, sizeof(pset), (int (*)()) d1_order);
204 qsort((char *) (R1 = sf_list(R)), (size_t)R->count, sizeof(pset), (int (*)()) d1_order);
205
206 /* Perform distance-1 merge */
207 compl_d1merge(L1, R1);
208
209 /* Perform lifting */
210 switch(lifting) {
212 T = cubeunlist(T1);
213 compl_lift_onset(L1, T, cr, var);
214 compl_lift_onset(R1, T, cl, var);
215 free_cover(T);
216 break;
218 T = cubeunlist(T1);
219 compl_lift_onset_complex(L1, T, var);
220 compl_lift_onset_complex(R1, T, var);
221 free_cover(T);
222 break;
223 case USE_COMPL_LIFT:
224 compl_lift(L1, R1, cr, var);
225 compl_lift(R1, L1, cl, var);
226 break;
227 case NO_LIFTING:
228 break;
229 default:
230 ;
231 }
232 FREE(L1);
233 FREE(R1);
234
235 /* Re-create the merged cover */
236 Tbar = new_cover(L->count + R->count);
237 pt = Tbar->data;
238 foreach_set(L, last, p) {
239 INLINEset_copy(pt, p);
240 Tbar->count++;
241 pt += Tbar->wsize;
242 }
243 foreach_active_set(R, last, p) {
244 INLINEset_copy(pt, p);
245 Tbar->count++;
246 pt += Tbar->wsize;
247 }
248
249 if (debug & COMPL) {
250 (void) printf("Result %d\n", Tbar->count);
251 if (verbose_debug)
252 cprint(Tbar);
253 }
254
255 free_cover(L);
256 free_cover(R);
257 return Tbar;
258}
259
260/*
261 * compl_lift_simple -- expand in the splitting variable using single
262 * cube containment against the other recursion branch to check
263 * validity of the expansion, and expanding all (or none) of the
264 * splitting variable.
265 */
266static void compl_lift(A1, B1, bcube, var)
267pcube *A1, *B1, bcube;
268int var;
269{
270 register pcube a, b, *B2, lift=cube.temp[4], liftor=cube.temp[5];
271 pcube mask = cube.var_mask[var];
272
273 (void) set_and(liftor, bcube, mask);
274
275 /* for each cube in the first array ... */
276 for(; (a = *A1++) != NULL; ) {
277 if (TESTP(a, ACTIVE)) {
278
279 /* create a lift of this cube in the merging coord */
280 (void) set_merge(lift, bcube, a, mask);
281
282 /* for each cube in the second array */
283 for(B2 = B1; (b = *B2++) != NULL; ) {
284 INLINEsetp_implies(lift, b, /* when_false => */ continue);
285 /* when_true => fall through to next statement */
286
287 /* cube of A1 was contained by some cube of B1, so raise */
288 INLINEset_or(a, a, liftor);
289 break;
290 }
291 }
292 }
293}
294
295
296
297/*
298 * compl_lift_onset -- expand in the splitting variable using a
299 * distance-1 check against the original on-set; expand all (or
300 * none) of the splitting variable. Each cube of A1 is expanded
301 * against the original on-set T.
302 */
303static void compl_lift_onset(A1, T, bcube, var)
304pcube *A1;
305pcover T;
306pcube bcube;
307int var;
308{
309 register pcube a, last, p, lift=cube.temp[4], mask=cube.var_mask[var];
310
311 /* for each active cube from one branch of the complement */
312 for(; (a = *A1++) != NULL; ) {
313 if (TESTP(a, ACTIVE)) {
314
315 /* create a lift of this cube in the merging coord */
316 INLINEset_and(lift, bcube, mask); /* isolate parts to raise */
317 INLINEset_or(lift, a, lift); /* raise these parts in a */
318
319 /* for each cube in the ON-set, check for intersection */
320 foreach_set(T, last, p) {
321 if (cdist0(p, lift)) {
322 goto nolift;
323 }
324 }
325 INLINEset_copy(a, lift); /* save the raising */
326 SET(a, ACTIVE);
327nolift : ;
328 }
329 }
330}
331
332/*
333 * compl_lift_complex -- expand in the splitting variable, but expand all
334 * parts which can possibly expand.
335 * T is the original ON-set
336 * A1 is either the left or right cofactor
337 */
338static void compl_lift_onset_complex(A1, T, var)
339pcube *A1; /* array of pointers to new result */
340pcover T; /* original ON-set */
341int var; /* which variable we split on */
342{
343 register int dist;
344 register pcube last, p, a, xlower;
345
346 /* for each cube in the complement */
347 xlower = new_cube();
348 for(; (a = *A1++) != NULL; ) {
349
350 if (TESTP(a, ACTIVE)) {
351
352 /* Find which parts of the splitting variable are forced low */
353 INLINEset_clear(xlower, cube.size);
354 foreach_set(T, last, p) {
355 if ((dist = cdist01(p, a)) < 2) {
356 if (dist == 0) {
357 fatal("compl: ON-set and OFF-set are not orthogonal");
358 } else {
359 (void) force_lower(xlower, p, a);
360 }
361 }
362 }
363
364 (void) set_diff(xlower, cube.var_mask[var], xlower);
365 (void) set_or(a, a, xlower);
366 free_cube(xlower);
367 }
368 }
369}
370
371
372
373/*
374 * compl_d1merge -- distance-1 merge in the splitting variable
375 */
376static void compl_d1merge(L1, R1)
377register pcube *L1, *R1;
378{
379 register pcube pl, pr;
380
381 /* Find equal cubes between the two cofactors */
382 for(pl = *L1, pr = *R1; (pl != NULL) && (pr != NULL); )
383 switch (d1_order(L1, R1)) {
384 case 1:
385 pr = *(++R1); break; /* advance right pointer */
386 case -1:
387 pl = *(++L1); break; /* advance left pointer */
388 case 0:
389 RESET(pr, ACTIVE);
390 INLINEset_or(pl, pl, pr);
391 pr = *(++R1);
392 default:
393 ;
394 }
395}
396
397
398
399/* compl_cube -- return the complement of a single cube (De Morgan's law) */
400static pcover compl_cube(p)
401register pcube p;
402{
403 register pcube diff=cube.temp[7], pdest, mask, full=cube.fullset;
404 int var;
405 pcover R;
406
407 /* Allocate worst-case size cover (to avoid checking overflow) */
408 R = new_cover(cube.num_vars);
409
410 /* Compute bit-wise complement of the cube */
411 INLINEset_diff(diff, full, p);
412
413 for(var = 0; var < cube.num_vars; var++) {
414 mask = cube.var_mask[var];
415 /* If the bit-wise complement is not empty in var ... */
416 if (! setp_disjoint(diff, mask)) {
417 pdest = GETSET(R, R->count++);
418 INLINEset_merge(pdest, diff, full, mask);
419 }
420 }
421 return R;
422}
423
424/* simp_comp -- quick simplification of T */
425void simp_comp(T, Tnew, Tbar)
426pcube *T; /* T will be disposed of */
427pcover *Tnew;
428pcover *Tbar;
429{
430 register pcube cl, cr;
431 register int best;
432 pcover Tl, Tr, Tlbar, Trbar;
433 int lifting;
434 static int simplify_level = 0;
435
436 if (debug & COMPL)
437 debug_print(T, "SIMPCOMP", simplify_level++);
438
439 if (simp_comp_special_cases(T, Tnew, Tbar) == MAYBE) {
440
441 /* Allocate space for the partition cubes */
442 cl = new_cube();
443 cr = new_cube();
444 best = binate_split_select(T, cl, cr, COMPL);
445
446 /* Complement the left and right halves */
447 simp_comp(scofactor(T, cl, best), &Tl, &Tlbar);
448 simp_comp(scofactor(T, cr, best), &Tr, &Trbar);
449
450 lifting = USE_COMPL_LIFT;
451 *Tnew = compl_merge(T, Tl, Tr, cl, cr, best, lifting);
452
453 lifting = USE_COMPL_LIFT;
454 *Tbar = compl_merge(T, Tlbar, Trbar, cl, cr, best, lifting);
455
456 /* All of this work for nothing ? Let's hope not ... */
457 if ((*Tnew)->count > CUBELISTSIZE(T)) {
458 sf_free(*Tnew);
459 *Tnew = cubeunlist(T);
460 }
461
462 free_cube(cl);
463 free_cube(cr);
464 free_cubelist(T);
465 }
466
467 if (debug & COMPL) {
468 debug1_print(*Tnew, "exit SIMPCOMP (new)", simplify_level);
469 debug1_print(*Tbar, "exit SIMPCOMP (compl)", simplify_level);
470 simplify_level--;
471 }
472}
473
474static bool simp_comp_special_cases(T, Tnew, Tbar)
475pcube *T; /* will be disposed if answer is determined */
476pcover *Tnew; /* returned only if answer determined */
477pcover *Tbar; /* returned only if answer determined */
478{
479 register pcube *T1, p, ceil, cof=T[0];
480 pcube last;
481 pcover A;
482
483 /* Check for no cubes in the cover (function is empty) */
484 if (T[2] == NULL) {
485 *Tnew = new_cover(1);
486 *Tbar = sf_addset(new_cover(1), cube.fullset);
487 free_cubelist(T);
488 return TRUE;
489 }
490
491 /* Check for only a single cube in the cover */
492 if (T[3] == NULL) {
493 (void) set_or(cof, cof, T[2]);
494 *Tnew = sf_addset(new_cover(1), cof);
495 *Tbar = compl_cube(cof);
496 free_cubelist(T);
497 return TRUE;
498 }
499
500 /* Check for a row of all 1's (function is a tautology) */
501 for(T1 = T+2; (p = *T1++) != NULL; ) {
502 if (full_row(p, cof)) {
503 *Tnew = sf_addset(new_cover(1), cube.fullset);
504 *Tbar = new_cover(1);
505 free_cubelist(T);
506 return TRUE;
507 }
508 }
509
510 /* Check for a column of all 0's which can be factored out */
511 ceil = set_save(cof);
512 for(T1 = T+2; (p = *T1++) != NULL; ) {
513 INLINEset_or(ceil, ceil, p);
514 }
515 if (! setp_equal(ceil, cube.fullset)) {
516 p = new_cube();
517 (void) set_diff(p, cube.fullset, ceil);
518 (void) set_or(cof, cof, p);
519 set_free(p);
520 simp_comp(T, Tnew, Tbar);
521
522 /* Adjust the ON-set */
523 A = *Tnew;
524 foreach_set(A, last, p) {
525 INLINEset_and(p, p, ceil);
526 }
527
528 /* Compute the new complement */
529 *Tbar = sf_append(*Tbar, compl_cube(ceil));
530 set_free(ceil);
531 return TRUE;
532 }
533 set_free(ceil);
534
535 /* Collect column counts, determine unate variables, etc. */
536 massive_count(T);
537
538 /* If single active variable not factored out above, then tautology ! */
539 if (cdata.vars_active == 1) {
540 *Tnew = sf_addset(new_cover(1), cube.fullset);
541 *Tbar = new_cover(1);
542 free_cubelist(T);
543 return TRUE;
544
545 /* Check for unate cover */
546 } else if (cdata.vars_unate == cdata.vars_active) {
547 /* Make the cover minimum by single-cube containment */
548 A = cubeunlist(T);
549 *Tnew = sf_contain(A);
550
551 /* Now form a minimum representation of the complement */
552 A = map_cover_to_unate(T);
553 A = unate_compl(A);
554 *Tbar = map_unate_to_cover(A);
555 sf_free(A);
556 free_cubelist(T);
557 return TRUE;
558
559 /* Not much we can do about it */
560 } else {
561 return MAYBE;
562 }
563}
564
565/* simplify -- quick simplification of T */
567pcube *T; /* T will be disposed of */
568{
569 register pcube cl, cr;
570 register int best;
571 pcover Tbar, Tl, Tr;
572 int lifting;
573 static int simplify_level = 0;
574
575 if (debug & COMPL) {
576 debug_print(T, "SIMPLIFY", simplify_level++);
577 }
578
579 if (simplify_special_cases(T, &Tbar) == MAYBE) {
580
581 /* Allocate space for the partition cubes */
582 cl = new_cube();
583 cr = new_cube();
584
585 best = binate_split_select(T, cl, cr, COMPL);
586
587 /* Complement the left and right halves */
588 Tl = simplify(scofactor(T, cl, best));
589 Tr = simplify(scofactor(T, cr, best));
590
591 lifting = USE_COMPL_LIFT;
592 Tbar = compl_merge(T, Tl, Tr, cl, cr, best, lifting);
593
594 /* All of this work for nothing ? Let's hope not ... */
595 if (Tbar->count > CUBELISTSIZE(T)) {
596 sf_free(Tbar);
597 Tbar = cubeunlist(T);
598 }
599
600 free_cube(cl);
601 free_cube(cr);
602 free_cubelist(T);
603 }
604
605 if (debug & COMPL) {
606 debug1_print(Tbar, "exit SIMPLIFY", --simplify_level);
607 }
608 return Tbar;
609}
610
611static bool simplify_special_cases(T, Tnew)
612pcube *T; /* will be disposed if answer is determined */
613pcover *Tnew; /* returned only if answer determined */
614{
615 register pcube *T1, p, ceil, cof=T[0];
616 pcube last;
617 pcover A;
618
619 /* Check for no cubes in the cover */
620 if (T[2] == NULL) {
621 *Tnew = new_cover(0);
622 free_cubelist(T);
623 return TRUE;
624 }
625
626 /* Check for only a single cube in the cover */
627 if (T[3] == NULL) {
628 *Tnew = sf_addset(new_cover(1), set_or(cof, cof, T[2]));
629 free_cubelist(T);
630 return TRUE;
631 }
632
633 /* Check for a row of all 1's (implies function is a tautology) */
634 for(T1 = T+2; (p = *T1++) != NULL; ) {
635 if (full_row(p, cof)) {
636 *Tnew = sf_addset(new_cover(1), cube.fullset);
637 free_cubelist(T);
638 return TRUE;
639 }
640 }
641
642 /* Check for a column of all 0's which can be factored out */
643 ceil = set_save(cof);
644 for(T1 = T+2; (p = *T1++) != NULL; ) {
645 INLINEset_or(ceil, ceil, p);
646 }
647 if (! setp_equal(ceil, cube.fullset)) {
648 p = new_cube();
649 (void) set_diff(p, cube.fullset, ceil);
650 (void) set_or(cof, cof, p);
651 free_cube(p);
652
653 A = simplify(T);
654 foreach_set(A, last, p) {
655 INLINEset_and(p, p, ceil);
656 }
657 *Tnew = A;
658 set_free(ceil);
659 return TRUE;
660 }
661 set_free(ceil);
662
663 /* Collect column counts, determine unate variables, etc. */
664 massive_count(T);
665
666 /* If single active variable not factored out above, then tautology ! */
667 if (cdata.vars_active == 1) {
668 *Tnew = sf_addset(new_cover(1), cube.fullset);
669 free_cubelist(T);
670 return TRUE;
671
672 /* Check for unate cover */
673 } else if (cdata.vars_unate == cdata.vars_active) {
674 A = cubeunlist(T);
675 *Tnew = sf_contain(A);
676 free_cubelist(T);
677 return TRUE;
678
679 /* Not much we can do about it */
680 } else {
681 return MAYBE;
682 }
683}
685
#define TRUE
Definition abcBm.c:38
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define FREE(obj)
Definition avl.h:31
#define NO_LIFTING
Definition compl.c:35
#define USE_COMPL_LIFT
Definition compl.c:32
#define USE_COMPL_LIFT_ONSET
Definition compl.c:33
#define USE_COMPL_LIFT_ONSET_COMPLEX
Definition compl.c:34
#define pcover
Definition espresso.h:264
pset_family sf_addset()
#define new_cube()
Definition espresso.h:262
bool full_row()
char * pc1()
pset set_merge()
#define set_save(r)
Definition espresso.h:166
#define INLINEset_diff(r, a, b)
Definition espresso.h:208
#define INLINEset_or(r, a, b)
Definition espresso.h:205
pcube * scofactor()
#define COMPL
Definition espresso.h:351
int d1_order()
#define INLINEsetp_implies(a, b, when_false)
Definition espresso.h:228
pcover map_unate_to_cover()
void simp_comp()
#define set_free(r)
Definition espresso.h:167
void debug1_print()
#define TESTP(set, flag)
Definition espresso.h:124
bool setp_disjoint()
#define ACTIVE
Definition espresso.h:129
pset set_and()
#define INLINEset_clear(r, size)
Definition espresso.h:197
pset force_lower()
pset_family sf_contain()
void fatal()
#define foreach_active_set(R, last, p)
Definition espresso.h:139
void cprint()
void debug_print()
pcover cubeunlist()
void massive_count()
void sf_free()
#define pcube
Definition espresso.h:261
ABC_NAMESPACE_HEADER_END int binate_split_select()
#define free_cover(r)
Definition espresso.h:266
#define GETSET(family, index)
Definition espresso.h:161
pset set_diff()
pcover map_cover_to_unate()
#define free_cube(r)
Definition espresso.h:263
#define INLINEset_copy(r, a)
Definition espresso.h:195
char * pc2()
#define foreach_set(R, last, p)
Definition espresso.h:135
pset_family unate_compl()
unsigned int debug
Definition globals.c:19
#define INLINEset_merge(r, a, b, mask)
Definition espresso.h:225
#define SET(set, flag)
Definition espresso.h:122
bool verbose_debug
Definition globals.c:20
#define INLINEset_and(r, a, b)
Definition espresso.h:202
#define RESET(set, flag)
Definition espresso.h:123
unsigned int * pset
Definition espresso.h:73
int cdist01()
pset set_or()
pset_family sf_append()
bool setp_equal()
pset * sf_list()
pcover simplify()
bool cdist0()
pset set_copy()
#define free_cubelist(T)
Definition espresso.h:267
#define CUBELISTSIZE(T)
Definition espresso.h:329
#define MAYBE
Definition espresso.h:257
#define new_cover(i)
Definition espresso.h:265
pcover complement()
Cube * p
Definition exorList.c:222
unsigned short var
Definition giaNewBdd.h:35
Definition exor.h:123