diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
commit | 4812c90424dfc40d26725244723887a2d16ddfd9 (patch) | |
tree | b32ace96e7e2d84d586e09ba605463b6f49c3271 /src/misc/espresso/irred.c | |
parent | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (diff) | |
download | abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.gz abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.bz2 abc-4812c90424dfc40d26725244723887a2d16ddfd9.zip |
Version abc71001
Diffstat (limited to 'src/misc/espresso/irred.c')
-rw-r--r-- | src/misc/espresso/irred.c | 440 |
1 files changed, 440 insertions, 0 deletions
diff --git a/src/misc/espresso/irred.c b/src/misc/espresso/irred.c new file mode 100644 index 00000000..384e698f --- /dev/null +++ b/src/misc/espresso/irred.c @@ -0,0 +1,440 @@ +/* + * Revision Control Information + * + * $Source$ + * $Author$ + * $Revision$ + * $Date$ + * + */ +#include "espresso.h" + +static void fcube_is_covered(); +static void ftautology(); +static bool ftaut_special_cases(); + + +static int Rp_current; + +/* + * irredundant -- Return a minimal subset of F + */ + +pcover +irredundant(F, D) +pcover F, D; +{ + mark_irredundant(F, D); + return sf_inactive(F); +} + + +/* + * mark_irredundant -- find redundant cubes, and mark them "INACTIVE" + */ + +void +mark_irredundant(F, D) +pcover F, D; +{ + pcover E, Rt, Rp; + pset p, p1, last; + sm_matrix *table; + sm_row *cover; + sm_element *pe; + + /* extract a minimum cover */ + irred_split_cover(F, D, &E, &Rt, &Rp); + table = irred_derive_table(D, E, Rp); + cover = sm_minimum_cover(table, NIL(int), /* heuristic */ 1, /* debug */ 0); + + /* mark the cubes for the result */ + foreach_set(F, last, p) { + RESET(p, ACTIVE); + RESET(p, RELESSEN); + } + foreach_set(E, last, p) { + p1 = GETSET(F, SIZE(p)); + assert(setp_equal(p1, p)); + SET(p1, ACTIVE); + SET(p1, RELESSEN); /* for essen(), mark as rel. ess. */ + } + sm_foreach_row_element(cover, pe) { + p1 = GETSET(F, pe->col_num); + SET(p1, ACTIVE); + } + + if (debug & IRRED) { + printf("# IRRED: F=%d E=%d R=%d Rt=%d Rp=%d Rc=%d Final=%d Bound=%d\n", + F->count, E->count, Rt->count+Rp->count, Rt->count, Rp->count, + cover->length, E->count + cover->length, 0); + } + + free_cover(E); + free_cover(Rt); + free_cover(Rp); + sm_free(table); + sm_row_free(cover); +} + +/* + * irred_split_cover -- find E, Rt, and Rp from the cover F, D + * + * E -- relatively essential cubes + * Rt -- totally redundant cubes + * Rp -- partially redundant cubes + */ + +void +irred_split_cover(F, D, E, Rt, Rp) +pcover F, D; +pcover *E, *Rt, *Rp; +{ + register pcube p, last; + register int index; + pcover R; + pcube *FD, *ED; + + /* number the cubes of F -- these numbers track into E, Rp, Rt, etc. */ + index = 0; + foreach_set(F, last, p) { + PUTSIZE(p, index); + index++; + } + + *E = new_cover(10); + *Rt = new_cover(10); + *Rp = new_cover(10); + R = new_cover(10); + + /* Split F into E and R */ + FD = cube2list(F, D); + foreach_set(F, last, p) { + if (cube_is_covered(FD, p)) { + R = sf_addset(R, p); + } else { + *E = sf_addset(*E, p); + } + if (debug & IRRED1) { + (void) printf("IRRED1: zr=%d ze=%d to-go=%d time=%s\n", + R->count, (*E)->count, F->count - (R->count + (*E)->count), + print_time(ptime())); + } + } + free_cubelist(FD); + + /* Split R into Rt and Rp */ + ED = cube2list(*E, D); + foreach_set(R, last, p) { + if (cube_is_covered(ED, p)) { + *Rt = sf_addset(*Rt, p); + } else { + *Rp = sf_addset(*Rp, p); + } + if (debug & IRRED1) { + (void) printf("IRRED1: zr=%d zrt=%d to-go=%d time=%s\n", + (*Rp)->count, (*Rt)->count, + R->count - ((*Rp)->count +(*Rt)->count), print_time(ptime())); + } + } + free_cubelist(ED); + + free_cover(R); +} + +/* + * irred_derive_table -- given the covers D, E and the set of + * partially redundant primes Rp, build a covering table showing + * possible selections of primes to cover Rp. + */ + +sm_matrix * +irred_derive_table(D, E, Rp) +pcover D, E, Rp; +{ + register pcube last, p, *list; + sm_matrix *table; + int size_last_dominance, i; + + /* Mark each cube in DE as not part of the redundant set */ + foreach_set(D, last, p) { + RESET(p, REDUND); + } + foreach_set(E, last, p) { + RESET(p, REDUND); + } + + /* Mark each cube in Rp as partially redundant */ + foreach_set(Rp, last, p) { + SET(p, REDUND); /* belongs to redundant set */ + } + + /* For each cube in Rp, find ways to cover its minterms */ + list = cube3list(D, E, Rp); + table = sm_alloc(); + size_last_dominance = 0; + i = 0; + foreach_set(Rp, last, p) { + Rp_current = SIZE(p); + fcube_is_covered(list, p, table); + RESET(p, REDUND); /* can now consider this cube redundant */ + if (debug & IRRED1) { + (void) printf("IRRED1: %d of %d to-go=%d, table=%dx%d time=%s\n", + i, Rp->count, Rp->count - i, + table->nrows, table->ncols, print_time(ptime())); + } + /* try to keep memory limits down by reducing table as we go along */ + if (table->nrows - size_last_dominance > 1000) { + (void) sm_row_dominance(table); + size_last_dominance = table->nrows; + if (debug & IRRED1) { + (void) printf("IRRED1: delete redundant rows, now %dx%d\n", + table->nrows, table->ncols); + } + } + i++; + } + free_cubelist(list); + + return table; +} + +/* cube_is_covered -- determine if a cubelist "covers" a single cube */ +bool +cube_is_covered(T, c) +pcube *T, c; +{ + return tautology(cofactor(T,c)); +} + + + +/* tautology -- answer the tautology question for T */ +bool +tautology(T) +pcube *T; /* T will be disposed of */ +{ + register pcube cl, cr; + register int best, result; + static int taut_level = 0; + + if (debug & TAUT) { + debug_print(T, "TAUTOLOGY", taut_level++); + } + + if ((result = taut_special_cases(T)) == MAYBE) { + cl = new_cube(); + cr = new_cube(); + best = binate_split_select(T, cl, cr, TAUT); + result = tautology(scofactor(T, cl, best)) && + tautology(scofactor(T, cr, best)); + free_cubelist(T); + free_cube(cl); + free_cube(cr); + } + + if (debug & TAUT) { + printf("exit TAUTOLOGY[%d]: %s\n", --taut_level, print_bool(result)); + } + return result; +} + +/* + * taut_special_cases -- check special cases for tautology + */ + +bool +taut_special_cases(T) +pcube *T; /* will be disposed if answer is determined */ +{ + register pcube *T1, *Tsave, p, ceil=cube.temp[0], temp=cube.temp[1]; + pcube *A, *B; + int var; + + /* Check for a row of all 1's which implies tautology */ + for(T1 = T+2; (p = *T1++) != NULL; ) { + if (full_row(p, T[0])) { + free_cubelist(T); + return TRUE; + } + } + + /* Check for a column of all 0's which implies no tautology */ +start: + INLINEset_copy(ceil, T[0]); + for(T1 = T+2; (p = *T1++) != NULL; ) { + INLINEset_or(ceil, ceil, p); + } + if (! setp_equal(ceil, cube.fullset)) { + free_cubelist(T); + return FALSE; + } + + /* Collect column counts, determine unate variables, etc. */ + massive_count(T); + + /* If function is unate (and no row of all 1's), then no tautology */ + if (cdata.vars_unate == cdata.vars_active) { + free_cubelist(T); + return FALSE; + + /* If active in a single variable (and no column of 0's) then tautology */ + } else if (cdata.vars_active == 1) { + free_cubelist(T); + return TRUE; + + /* Check for unate variables, and reduce cover if there are any */ + } else if (cdata.vars_unate != 0) { + /* Form a cube "ceil" with full variables in the unate variables */ + (void) set_copy(ceil, cube.emptyset); + for(var = 0; var < cube.num_vars; var++) { + if (cdata.is_unate[var]) { + INLINEset_or(ceil, ceil, cube.var_mask[var]); + } + } + + /* Save only those cubes that are "full" in all unate variables */ + for(Tsave = T1 = T+2; (p = *T1++) != 0; ) { + if (setp_implies(ceil, set_or(temp, p, T[0]))) { + *Tsave++ = p; + } + } + *Tsave++ = NULL; + T[1] = (pcube) Tsave; + + if (debug & TAUT) { + printf("UNATE_REDUCTION: %d unate variables, reduced to %d\n", + cdata.vars_unate, CUBELISTSIZE(T)); + } + goto start; + + /* Check for component reduction */ + } else if (cdata.var_zeros[cdata.best] < CUBELISTSIZE(T) / 2) { + if (cubelist_partition(T, &A, &B, debug & TAUT) == 0) { + return MAYBE; + } else { + free_cubelist(T); + if (tautology(A)) { + free_cubelist(B); + return TRUE; + } else { + return tautology(B); + } + } + } + + /* We tried as hard as we could, but must recurse from here on */ + return MAYBE; +} + +/* fcube_is_covered -- determine exactly how a cubelist "covers" a cube */ +static void +fcube_is_covered(T, c, table) +pcube *T, c; +sm_matrix *table; +{ + ftautology(cofactor(T,c), table); +} + + +/* ftautology -- find ways to make a tautology */ +static void +ftautology(T, table) +pcube *T; /* T will be disposed of */ +sm_matrix *table; +{ + register pcube cl, cr; + register int best; + static int ftaut_level = 0; + + if (debug & TAUT) { + debug_print(T, "FIND_TAUTOLOGY", ftaut_level++); + } + + if (ftaut_special_cases(T, table) == MAYBE) { + cl = new_cube(); + cr = new_cube(); + best = binate_split_select(T, cl, cr, TAUT); + + ftautology(scofactor(T, cl, best), table); + ftautology(scofactor(T, cr, best), table); + + free_cubelist(T); + free_cube(cl); + free_cube(cr); + } + + if (debug & TAUT) { + (void) printf("exit FIND_TAUTOLOGY[%d]: table is %d by %d\n", + --ftaut_level, table->nrows, table->ncols); + } +} + +static bool +ftaut_special_cases(T, table) +pcube *T; /* will be disposed if answer is determined */ +sm_matrix *table; +{ + register pcube *T1, *Tsave, p, temp = cube.temp[0], ceil = cube.temp[1]; + int var, rownum; + + /* Check for a row of all 1's in the essential cubes */ + for(T1 = T+2; (p = *T1++) != 0; ) { + if (! TESTP(p, REDUND)) { + if (full_row(p, T[0])) { + /* subspace is covered by essentials -- no new rows for table */ + free_cubelist(T); + return TRUE; + } + } + } + + /* Collect column counts, determine unate variables, etc. */ +start: + massive_count(T); + + /* If function is unate, find the rows of all 1's */ + if (cdata.vars_unate == cdata.vars_active) { + /* find which nonessentials cover this subspace */ + rownum = table->last_row ? table->last_row->row_num+1 : 0; + (void) sm_insert(table, rownum, Rp_current); + for(T1 = T+2; (p = *T1++) != 0; ) { + if (TESTP(p, REDUND)) { + /* See if a redundant cube covers this leaf */ + if (full_row(p, T[0])) { + (void) sm_insert(table, rownum, (int) SIZE(p)); + } + } + } + free_cubelist(T); + return TRUE; + + /* Perform unate reduction if there are any unate variables */ + } else if (cdata.vars_unate != 0) { + /* Form a cube "ceil" with full variables in the unate variables */ + (void) set_copy(ceil, cube.emptyset); + for(var = 0; var < cube.num_vars; var++) { + if (cdata.is_unate[var]) { + INLINEset_or(ceil, ceil, cube.var_mask[var]); + } + } + + /* Save only those cubes that are "full" in all unate variables */ + for(Tsave = T1 = T+2; (p = *T1++) != 0; ) { + if (setp_implies(ceil, set_or(temp, p, T[0]))) { + *Tsave++ = p; + } + } + *Tsave++ = 0; + T[1] = (pcube) Tsave; + + if (debug & TAUT) { + printf("UNATE_REDUCTION: %d unate variables, reduced to %d\n", + cdata.vars_unate, CUBELISTSIZE(T)); + } + goto start; + } + + /* Not much we can do about it */ + return MAYBE; +} |