diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-09-30 08:01:00 -0700 |
commit | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (patch) | |
tree | de3ffe87c3e17950351e3b7d97fa18318bd5ea9a /src/misc/espresso/compl.c | |
parent | 7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 (diff) | |
download | abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.gz abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.bz2 abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.zip |
Version abc70930
Diffstat (limited to 'src/misc/espresso/compl.c')
-rw-r--r-- | src/misc/espresso/compl.c | 680 |
1 files changed, 0 insertions, 680 deletions
diff --git a/src/misc/espresso/compl.c b/src/misc/espresso/compl.c deleted file mode 100644 index 8f1c6606..00000000 --- a/src/misc/espresso/compl.c +++ /dev/null @@ -1,680 +0,0 @@ -/* - * Revision Control Information - * - * $Source$ - * $Author$ - * $Revision$ - * $Date$ - * - */ -/* - * module: compl.c - * purpose: compute the complement of a multiple-valued function - * - * The "unate recursive paradigm" is used. After a set of special - * cases are examined, the function is split on the "most active - * variable". These two halves are complemented recursively, and then - * the results are merged. - * - * Changes (from Version 2.1 to Version 2.2) - * 1. Minor bug in compl_lifting -- cubes in the left half were - * not marked as active, so that when merging a leaf from the left - * hand side, the active flags were essentially random. This led - * to minor impredictability problem, but never affected the - * accuracy of the results. - */ - -#include "espresso.h" - -#define USE_COMPL_LIFT 0 -#define USE_COMPL_LIFT_ONSET 1 -#define USE_COMPL_LIFT_ONSET_COMPLEX 2 -#define NO_LIFTING 3 - -static bool compl_special_cases(); -static pcover compl_merge(); -static void compl_d1merge(); -static pcover compl_cube(); -static void compl_lift(); -static void compl_lift_onset(); -static void compl_lift_onset_complex(); -static bool simp_comp_special_cases(); -static bool simplify_special_cases(); - - -/* complement -- compute the complement of T */ -pcover complement(T) -pcube *T; /* T will be disposed of */ -{ - register pcube cl, cr; - register int best; - pcover Tbar, Tl, Tr; - int lifting; - static int compl_level = 0; - - if (debug & COMPL) - debug_print(T, "COMPLEMENT", compl_level++); - - if (compl_special_cases(T, &Tbar) == MAYBE) { - - /* Allocate space for the partition cubes */ - cl = new_cube(); - cr = new_cube(); - best = binate_split_select(T, cl, cr, COMPL); - - /* Complement the left and right halves */ - Tl = complement(scofactor(T, cl, best)); - Tr = complement(scofactor(T, cr, best)); - - if (Tr->count*Tl->count > (Tr->count+Tl->count)*CUBELISTSIZE(T)) { - lifting = USE_COMPL_LIFT_ONSET; - } else { - lifting = USE_COMPL_LIFT; - } - Tbar = compl_merge(T, Tl, Tr, cl, cr, best, lifting); - - free_cube(cl); - free_cube(cr); - free_cubelist(T); - } - - if (debug & COMPL) - debug1_print(Tbar, "exit COMPLEMENT", --compl_level); - return Tbar; -} - -static bool compl_special_cases(T, Tbar) -pcube *T; /* will be disposed if answer is determined */ -pcover *Tbar; /* returned only if answer determined */ -{ - register pcube *T1, p, ceil, cof=T[0]; - pcover A, ceil_compl; - - /* Check for no cubes in the cover */ - if (T[2] == NULL) { - *Tbar = sf_addset(new_cover(1), cube.fullset); - free_cubelist(T); - return TRUE; - } - - /* Check for only a single cube in the cover */ - if (T[3] == NULL) { - *Tbar = compl_cube(set_or(cof, cof, T[2])); - free_cubelist(T); - return TRUE; - } - - /* Check for a row of all 1's (implies complement is null) */ - for(T1 = T+2; (p = *T1++) != NULL; ) { - if (full_row(p, cof)) { - *Tbar = new_cover(0); - free_cubelist(T); - return TRUE; - } - } - - /* Check for a column of all 0's which can be factored out */ - ceil = set_save(cof); - for(T1 = T+2; (p = *T1++) != NULL; ) { - INLINEset_or(ceil, ceil, p); - } - if (! setp_equal(ceil, cube.fullset)) { - ceil_compl = compl_cube(ceil); - (void) set_or(cof, cof, set_diff(ceil, cube.fullset, ceil)); - set_free(ceil); - *Tbar = sf_append(complement(T), ceil_compl); - return TRUE; - } - set_free(ceil); - - /* Collect column counts, determine unate variables, etc. */ - massive_count(T); - - /* If single active variable not factored out above, then tautology ! */ - if (cdata.vars_active == 1) { - *Tbar = new_cover(0); - free_cubelist(T); - return TRUE; - - /* Check for unate cover */ - } else if (cdata.vars_unate == cdata.vars_active) { - A = map_cover_to_unate(T); - free_cubelist(T); - A = unate_compl(A); - *Tbar = map_unate_to_cover(A); - sf_free(A); - return TRUE; - - /* Not much we can do about it */ - } else { - return MAYBE; - } -} - -/* - * compl_merge -- merge the two cofactors around the splitting - * variable - * - * The merge operation involves intersecting each cube of the left - * cofactor with cl, and intersecting each cube of the right cofactor - * with cr. The union of these two covers is the merged result. - * - * In order to reduce the number of cubes, a distance-1 merge is - * performed (note that two cubes can only combine distance-1 in the - * splitting variable). Also, a simple expand is performed in the - * splitting variable (simple implies the covering check for the - * expansion is not full containment, but single-cube containment). - */ - -static pcover compl_merge(T1, L, R, cl, cr, var, lifting) -pcube *T1; /* Original ON-set */ -pcover L, R; /* Complement from each recursion branch */ -register pcube cl, cr; /* cubes used for cofactoring */ -int var; /* splitting variable */ -int lifting; /* whether to perform lifting or not */ -{ - register pcube p, last, pt; - pcover T, Tbar; - pcube *L1, *R1; - - if (debug & COMPL) { - (void) printf("compl_merge: left %d, right %d\n", L->count, R->count); - (void) printf("%s (cl)\n%s (cr)\nLeft is\n", pc1(cl), pc2(cr)); - cprint(L); - (void) printf("Right is\n"); - cprint(R); - } - - /* Intersect each cube with the cofactored cube */ - foreach_set(L, last, p) { - INLINEset_and(p, p, cl); - SET(p, ACTIVE); - } - foreach_set(R, last, p) { - INLINEset_and(p, p, cr); - SET(p, ACTIVE); - } - - /* Sort the arrays for a distance-1 merge */ - (void) set_copy(cube.temp[0], cube.var_mask[var]); - qsort((char *) (L1 = sf_list(L)), L->count, sizeof(pset), (int (*)()) d1_order); - qsort((char *) (R1 = sf_list(R)), R->count, sizeof(pset), (int (*)()) d1_order); - - /* Perform distance-1 merge */ - compl_d1merge(L1, R1); - - /* Perform lifting */ - switch(lifting) { - case USE_COMPL_LIFT_ONSET: - T = cubeunlist(T1); - compl_lift_onset(L1, T, cr, var); - compl_lift_onset(R1, T, cl, var); - free_cover(T); - break; - case USE_COMPL_LIFT_ONSET_COMPLEX: - T = cubeunlist(T1); - compl_lift_onset_complex(L1, T, var); - compl_lift_onset_complex(R1, T, var); - free_cover(T); - break; - case USE_COMPL_LIFT: - compl_lift(L1, R1, cr, var); - compl_lift(R1, L1, cl, var); - break; - case NO_LIFTING: - break; - default: - ; - } - FREE(L1); - FREE(R1); - - /* Re-create the merged cover */ - Tbar = new_cover(L->count + R->count); - pt = Tbar->data; - foreach_set(L, last, p) { - INLINEset_copy(pt, p); - Tbar->count++; - pt += Tbar->wsize; - } - foreach_active_set(R, last, p) { - INLINEset_copy(pt, p); - Tbar->count++; - pt += Tbar->wsize; - } - - if (debug & COMPL) { - (void) printf("Result %d\n", Tbar->count); - if (verbose_debug) - cprint(Tbar); - } - - free_cover(L); - free_cover(R); - return Tbar; -} - -/* - * compl_lift_simple -- expand in the splitting variable using single - * cube containment against the other recursion branch to check - * validity of the expansion, and expanding all (or none) of the - * splitting variable. - */ -static void compl_lift(A1, B1, bcube, var) -pcube *A1, *B1, bcube; -int var; -{ - register pcube a, b, *B2, lift=cube.temp[4], liftor=cube.temp[5]; - pcube mask = cube.var_mask[var]; - - (void) set_and(liftor, bcube, mask); - - /* for each cube in the first array ... */ - for(; (a = *A1++) != NULL; ) { - if (TESTP(a, ACTIVE)) { - - /* create a lift of this cube in the merging coord */ - (void) set_merge(lift, bcube, a, mask); - - /* for each cube in the second array */ - for(B2 = B1; (b = *B2++) != NULL; ) { - INLINEsetp_implies(lift, b, /* when_false => */ continue); - /* when_true => fall through to next statement */ - - /* cube of A1 was contained by some cube of B1, so raise */ - INLINEset_or(a, a, liftor); - break; - } - } - } -} - - - -/* - * compl_lift_onset -- expand in the splitting variable using a - * distance-1 check against the original on-set; expand all (or - * none) of the splitting variable. Each cube of A1 is expanded - * against the original on-set T. - */ -static void compl_lift_onset(A1, T, bcube, var) -pcube *A1; -pcover T; -pcube bcube; -int var; -{ - register pcube a, last, p, lift=cube.temp[4], mask=cube.var_mask[var]; - - /* for each active cube from one branch of the complement */ - for(; (a = *A1++) != NULL; ) { - if (TESTP(a, ACTIVE)) { - - /* create a lift of this cube in the merging coord */ - INLINEset_and(lift, bcube, mask); /* isolate parts to raise */ - INLINEset_or(lift, a, lift); /* raise these parts in a */ - - /* for each cube in the ON-set, check for intersection */ - foreach_set(T, last, p) { - if (cdist0(p, lift)) { - goto nolift; - } - } - INLINEset_copy(a, lift); /* save the raising */ - SET(a, ACTIVE); -nolift : ; - } - } -} - -/* - * compl_lift_complex -- expand in the splitting variable, but expand all - * parts which can possibly expand. - * T is the original ON-set - * A1 is either the left or right cofactor - */ -static void compl_lift_onset_complex(A1, T, var) -pcube *A1; /* array of pointers to new result */ -pcover T; /* original ON-set */ -int var; /* which variable we split on */ -{ - register int dist; - register pcube last, p, a, xlower; - - /* for each cube in the complement */ - xlower = new_cube(); - for(; (a = *A1++) != NULL; ) { - - if (TESTP(a, ACTIVE)) { - - /* Find which parts of the splitting variable are forced low */ - INLINEset_clear(xlower, cube.size); - foreach_set(T, last, p) { - if ((dist = cdist01(p, a)) < 2) { - if (dist == 0) { - fatal("compl: ON-set and OFF-set are not orthogonal"); - } else { - (void) force_lower(xlower, p, a); - } - } - } - - (void) set_diff(xlower, cube.var_mask[var], xlower); - (void) set_or(a, a, xlower); - free_cube(xlower); - } - } -} - - - -/* - * compl_d1merge -- distance-1 merge in the splitting variable - */ -static void compl_d1merge(L1, R1) -register pcube *L1, *R1; -{ - register pcube pl, pr; - - /* Find equal cubes between the two cofactors */ - for(pl = *L1, pr = *R1; (pl != NULL) && (pr != NULL); ) - switch (d1_order(L1, R1)) { - case 1: - pr = *(++R1); break; /* advance right pointer */ - case -1: - pl = *(++L1); break; /* advance left pointer */ - case 0: - RESET(pr, ACTIVE); - INLINEset_or(pl, pl, pr); - pr = *(++R1); - default: - ; - } -} - - - -/* compl_cube -- return the complement of a single cube (De Morgan's law) */ -static pcover compl_cube(p) -register pcube p; -{ - register pcube diff=cube.temp[7], pdest, mask, full=cube.fullset; - int var; - pcover R; - - /* Allocate worst-case size cover (to avoid checking overflow) */ - R = new_cover(cube.num_vars); - - /* Compute bit-wise complement of the cube */ - INLINEset_diff(diff, full, p); - - for(var = 0; var < cube.num_vars; var++) { - mask = cube.var_mask[var]; - /* If the bit-wise complement is not empty in var ... */ - if (! setp_disjoint(diff, mask)) { - pdest = GETSET(R, R->count++); - INLINEset_merge(pdest, diff, full, mask); - } - } - return R; -} - -/* simp_comp -- quick simplification of T */ -void simp_comp(T, Tnew, Tbar) -pcube *T; /* T will be disposed of */ -pcover *Tnew; -pcover *Tbar; -{ - register pcube cl, cr; - register int best; - pcover Tl, Tr, Tlbar, Trbar; - int lifting; - static int simplify_level = 0; - - if (debug & COMPL) - debug_print(T, "SIMPCOMP", simplify_level++); - - if (simp_comp_special_cases(T, Tnew, Tbar) == MAYBE) { - - /* Allocate space for the partition cubes */ - cl = new_cube(); - cr = new_cube(); - best = binate_split_select(T, cl, cr, COMPL); - - /* Complement the left and right halves */ - simp_comp(scofactor(T, cl, best), &Tl, &Tlbar); - simp_comp(scofactor(T, cr, best), &Tr, &Trbar); - - lifting = USE_COMPL_LIFT; - *Tnew = compl_merge(T, Tl, Tr, cl, cr, best, lifting); - - lifting = USE_COMPL_LIFT; - *Tbar = compl_merge(T, Tlbar, Trbar, cl, cr, best, lifting); - - /* All of this work for nothing ? Let's hope not ... */ - if ((*Tnew)->count > CUBELISTSIZE(T)) { - sf_free(*Tnew); - *Tnew = cubeunlist(T); - } - - free_cube(cl); - free_cube(cr); - free_cubelist(T); - } - - if (debug & COMPL) { - debug1_print(*Tnew, "exit SIMPCOMP (new)", simplify_level); - debug1_print(*Tbar, "exit SIMPCOMP (compl)", simplify_level); - simplify_level--; - } -} - -static bool simp_comp_special_cases(T, Tnew, Tbar) -pcube *T; /* will be disposed if answer is determined */ -pcover *Tnew; /* returned only if answer determined */ -pcover *Tbar; /* returned only if answer determined */ -{ - register pcube *T1, p, ceil, cof=T[0]; - pcube last; - pcover A; - - /* Check for no cubes in the cover (function is empty) */ - if (T[2] == NULL) { - *Tnew = new_cover(1); - *Tbar = sf_addset(new_cover(1), cube.fullset); - free_cubelist(T); - return TRUE; - } - - /* Check for only a single cube in the cover */ - if (T[3] == NULL) { - (void) set_or(cof, cof, T[2]); - *Tnew = sf_addset(new_cover(1), cof); - *Tbar = compl_cube(cof); - free_cubelist(T); - return TRUE; - } - - /* Check for a row of all 1's (function is a tautology) */ - for(T1 = T+2; (p = *T1++) != NULL; ) { - if (full_row(p, cof)) { - *Tnew = sf_addset(new_cover(1), cube.fullset); - *Tbar = new_cover(1); - free_cubelist(T); - return TRUE; - } - } - - /* Check for a column of all 0's which can be factored out */ - ceil = set_save(cof); - for(T1 = T+2; (p = *T1++) != NULL; ) { - INLINEset_or(ceil, ceil, p); - } - if (! setp_equal(ceil, cube.fullset)) { - p = new_cube(); - (void) set_diff(p, cube.fullset, ceil); - (void) set_or(cof, cof, p); - set_free(p); - simp_comp(T, Tnew, Tbar); - - /* Adjust the ON-set */ - A = *Tnew; - foreach_set(A, last, p) { - INLINEset_and(p, p, ceil); - } - - /* Compute the new complement */ - *Tbar = sf_append(*Tbar, compl_cube(ceil)); - set_free(ceil); - return TRUE; - } - set_free(ceil); - - /* Collect column counts, determine unate variables, etc. */ - massive_count(T); - - /* If single active variable not factored out above, then tautology ! */ - if (cdata.vars_active == 1) { - *Tnew = sf_addset(new_cover(1), cube.fullset); - *Tbar = new_cover(1); - free_cubelist(T); - return TRUE; - - /* Check for unate cover */ - } else if (cdata.vars_unate == cdata.vars_active) { - /* Make the cover minimum by single-cube containment */ - A = cubeunlist(T); - *Tnew = sf_contain(A); - - /* Now form a minimum representation of the complement */ - A = map_cover_to_unate(T); - A = unate_compl(A); - *Tbar = map_unate_to_cover(A); - sf_free(A); - free_cubelist(T); - return TRUE; - - /* Not much we can do about it */ - } else { - return MAYBE; - } -} - -/* simplify -- quick simplification of T */ -pcover simplify(T) -pcube *T; /* T will be disposed of */ -{ - register pcube cl, cr; - register int best; - pcover Tbar, Tl, Tr; - int lifting; - static int simplify_level = 0; - - if (debug & COMPL) { - debug_print(T, "SIMPLIFY", simplify_level++); - } - - if (simplify_special_cases(T, &Tbar) == MAYBE) { - - /* Allocate space for the partition cubes */ - cl = new_cube(); - cr = new_cube(); - - best = binate_split_select(T, cl, cr, COMPL); - - /* Complement the left and right halves */ - Tl = simplify(scofactor(T, cl, best)); - Tr = simplify(scofactor(T, cr, best)); - - lifting = USE_COMPL_LIFT; - Tbar = compl_merge(T, Tl, Tr, cl, cr, best, lifting); - - /* All of this work for nothing ? Let's hope not ... */ - if (Tbar->count > CUBELISTSIZE(T)) { - sf_free(Tbar); - Tbar = cubeunlist(T); - } - - free_cube(cl); - free_cube(cr); - free_cubelist(T); - } - - if (debug & COMPL) { - debug1_print(Tbar, "exit SIMPLIFY", --simplify_level); - } - return Tbar; -} - -static bool simplify_special_cases(T, Tnew) -pcube *T; /* will be disposed if answer is determined */ -pcover *Tnew; /* returned only if answer determined */ -{ - register pcube *T1, p, ceil, cof=T[0]; - pcube last; - pcover A; - - /* Check for no cubes in the cover */ - if (T[2] == NULL) { - *Tnew = new_cover(0); - free_cubelist(T); - return TRUE; - } - - /* Check for only a single cube in the cover */ - if (T[3] == NULL) { - *Tnew = sf_addset(new_cover(1), set_or(cof, cof, T[2])); - free_cubelist(T); - return TRUE; - } - - /* Check for a row of all 1's (implies function is a tautology) */ - for(T1 = T+2; (p = *T1++) != NULL; ) { - if (full_row(p, cof)) { - *Tnew = sf_addset(new_cover(1), cube.fullset); - free_cubelist(T); - return TRUE; - } - } - - /* Check for a column of all 0's which can be factored out */ - ceil = set_save(cof); - for(T1 = T+2; (p = *T1++) != NULL; ) { - INLINEset_or(ceil, ceil, p); - } - if (! setp_equal(ceil, cube.fullset)) { - p = new_cube(); - (void) set_diff(p, cube.fullset, ceil); - (void) set_or(cof, cof, p); - free_cube(p); - - A = simplify(T); - foreach_set(A, last, p) { - INLINEset_and(p, p, ceil); - } - *Tnew = A; - set_free(ceil); - return TRUE; - } - set_free(ceil); - - /* Collect column counts, determine unate variables, etc. */ - massive_count(T); - - /* If single active variable not factored out above, then tautology ! */ - if (cdata.vars_active == 1) { - *Tnew = sf_addset(new_cover(1), cube.fullset); - free_cubelist(T); - return TRUE; - - /* Check for unate cover */ - } else if (cdata.vars_unate == cdata.vars_active) { - A = cubeunlist(T); - *Tnew = sf_contain(A); - free_cubelist(T); - return TRUE; - - /* Not much we can do about it */ - } else { - return MAYBE; - } -} |