irred.c File Reference

#include "espresso.h"

Include dependency graph for irred.c:

Go to the source code of this file.

Functions
pcover	irredundant (pcover F, pcover D)
void	mark_irredundant (pcover F, pcover D)
void	irred_split_cover (pcover F, pcover D, pcover *E, pcover *Rt, pcover *Rp)
sm_matrix *	irred_derive_table (pcover D, pcover E, pcover Rp)
bool	cube_is_covered (pcube *T, pcube c)
bool	tautology (pcube *T)
bool	taut_special_cases (pcube *T)

Function Documentation

cube_is_covered()

bool cube_is_covered	(	pcube *	T,
		pcube	c )

Definition at line 207 of file irred.c.

{
    return tautology(cofactor(T,c));
}

Here is the call graph for this function:

irred_derive_table()

sm_matrix * irred_derive_table	(	pcover	D,
		pcover	E,
		pcover	Rp )

Definition at line 155 of file irred.c.

{
    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;
}

Here is the call graph for this function:

irred_split_cover()

void irred_split_cover	(	pcover	F,
		pcover	D,
		pcover *	E,
		pcover *	Rt,
		pcover *	Rp )

Definition at line 92 of file irred.c.

{
    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);
}

Here is the call graph for this function:

irredundant()

pcover irredundant	(	pcover	F,
		pcover	D )

Definition at line 27 of file irred.c.

{
    mark_irredundant(F, D);
    return sf_inactive(F);
}

Here is the call graph for this function:

mark_irredundant()

void mark_irredundant	(	pcover	F,
		pcover	D )

Definition at line 40 of file irred.c.

{
    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);
}

Here is the call graph for this function:

taut_special_cases()

bool taut_special_cases

(

pcube *

T

)

Definition at line 250 of file irred.c.

{
    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",
        (int)cdata.vars_unate, (int)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;
}

Here is the call graph for this function:

tautology()

bool tautology

(

pcube *

T

)

Definition at line 217 of file irred.c.

{
    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;
}

Here is the call graph for this function: