compl.c

主要进行大规模的电路综合

    /* 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;
    }
}