ros.c

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

pcube p;
pcube overexpanded_cube;
pcube *T;
int level;

{

    pcover BBl, BBr;
    pcube temp;
    pcube cl, cr;
    pcube *Tl, *Tr, *Temp;
    int best;
    bool was_taut;


    if (BB_dyn_special_cases(&BBl, p, overexpanded_cube, T, level)) {
	return(BBl);
    }
    else {

	cl = new_cube();
	cr = new_cube();

	best = binate_split_select(T, cl, cr, COMPL);

	if (best < cube.num_binary_vars) {

	    nc_bin_cof(T, &Tl, &Tr, cl, cr, best);
	    free_cubelist(T);

	    if (GETINPUT(p, best) == 0) {
		BBl = setupBB_dyn(p, overexpanded_cube, Tl, level+1);

		/* Use was_taut to temporarily hold is_taut */
		was_taut = is_taut;
		BBr = setupBB_dyn(p, overexpanded_cube, Tr, level+1);

		if (was_taut && is_taut) {
		    sf_free(BBr);
		} else {
		    nc_sf_multiply(BBl, cl, best);
		    nc_sf_multiply(BBr, cr, best);
		    BBl = sf_append(BBl, BBr);
		    is_taut = FALSE;
		}

		free_cube(cl);
		free_cube(cr);
		is_taut = FALSE;
		return(BBl);

	    }

	    /* Swap left and right sides if cl is not dist0 from p.
	       Since both left and right cannot be dist1 from p,
	       cl must be dist0 from p after swapping */

	    if (!cdist0bv(p, cl, best)) {
		temp = cl;
		cl = cr;
		cr = temp;

		Temp = Tl;
		Tl = Tr;
		Tr = Temp;
	    }

	    BBl = setupBB_dyn(p, overexpanded_cube, Tl, level+1);
	    free_cube(cl);

	    /* If BBl is a tautology, no need to evaluate BBr */
	    if (is_taut) {
		free_cubelist(Tr);
		free_cube(cr);
		return(BBl);
	    }

	    BBr = setupBB_dyn(p, overexpanded_cube, Tr, level+1);

	    if (cdist0bv(p, cr, best)) {
		if (is_taut) {
		    sf_free(BBl);
		    free_cube(cr);
		    return(BBr);
		}
		else {
		    BBl = sf_append(BBl, BBr);
		    free_cube(cr);
		    return(BBl);
		}
	    } else if (BBr->count == 0) {
		sf_free(BBr);
		free_cube(cr);
		return(BBl);
	    } else {
		is_taut = FALSE;
		nc_sf_multiply(BBr, cr, best);
		BBl = sf_append(BBl, BBr);
		free_cube(cr);
		return(BBl);
	    }
	}

	else { /* Splitting variable is multivalued */

	    Tl = scofactor(T, cl, best);
	    nc_cof_contain(Tl);
	    Tr = scofactor(T, cr, best);
	    nc_cof_contain(Tr);

	    free_cubelist(T);

	    BBl = setupBB_dyn(p, overexpanded_cube, Tl, level+1);
	    if (cdist0v(p, cl, best)) {
		free_cube(cl);
		if (is_taut) {
		    free_cube(cr);
		    return(BBl);
		}
	    }
	    else if (BBl->count != 0) {
		    nc_sf_multiply(BBl, cl, best);
		    free_cube(cl);
	    }
        else {
            free_cube(cl);  /* added by wjiang (5/1/03) */
        }

	    BBr = setupBB_dyn(p, overexpanded_cube, Tr, level+1);
	    if (cdist0v(p, cr, best)) {
		free_cube(cr);
		if (is_taut) {
		    sf_free(BBl);
		    return(BBr);
		}
		else {
		    BBl = sf_append(BBl, BBr);
		    return(BBl);
		}
	    } else if (BBr->count == 0) {
		sf_free(BBr);
		free_cube(cr);
		return(BBl);
	    } else {
		is_taut = FALSE;
		nc_sf_multiply(BBr, cr, best);
		free_cube(cr);
		BBl = sf_append(BBl, BBr);
		return(BBl);
	    }
	}

    }

}

/*
 * Special cases for setting up blocking matrix (reduced offset)
 * This routine uses global variable Num_act_vars declared in 
 * minimize.h
 */
bool
BB_dyn_special_cases(BB, p, overexpanded_cube, T, level)
pcover *BB;
pcube p;
pcube overexpanded_cube;
pcube *T;
int level;

{

    pcube temp;

    if (!(level%N_level)) {

	/* If the cofactoring cube is contained in p, the cofactor
	   is a tautology. In this case return an empty cover. */
	if (level > Num_act_vars) {
	    temp = set_diff(new_cube(), cube.fullset, T[0]);
	    if (setp_implies(temp, p)) {
		free_cube(temp);
		is_taut = FALSE;
		*BB = new_cover(0); 
		free_cubelist(T);
		return(TRUE);
	    }

	    free_cube(temp);
	}

	/* Remove unnecessary cubes from the cofactor */
	nc_rem_unnec_cubes(p, T);
    }

    /* Avoid massive count if there is no cube or only one cube in the cover */
    if ((T[2] == NULL) || (T[3] == NULL))
	cdata.vars_unate = cdata.vars_active = 1;
    else
	massive_count(T);

    /* Check for unate cover */
    if (cdata.vars_unate == cdata.vars_active) { /* T is unate */

	/* Remove those cubes from the cover that don't contain p */
	nc_rem_noncov_cubes(p, T);

	if (T[2] == (pcube) NULL) { /* Empty cubelist. Compl is tautology */
	    is_taut = TRUE;
	    *BB = sf_addset(new_cover(1), cube.fullset);
	    free_cubelist(T);
	    return(TRUE);
	}

	else {
	    is_taut = FALSE;
	}

	temp = new_cube();
	(void) set_or(T[0], T[0], set_diff(temp, cube.fullset, overexpanded_cube));

	nc_compl_special_cases(T, BB);

	free_cube(temp);
	return(TRUE);
    
    }

    /* Try to partition T */
    if (level % N_level)
	if (partition_ROS(p, overexpanded_cube, level, T, BB))
	    return(TRUE);

    return(FALSE);

}

/*
 * Find the overexpanded cube of cube p.
 *
 * This subroutine is used when the entire unate tree is stored
 * rather than only the leafs.
 */

void
find_overexpanded_cube(p, overexpanded_cube, pNode, dist_cube, dist, var, level)
pcube p;		/* Node to be expanded */
pcube overexpanded_cube;/* overexpanded cube so far */
pnc_node pNode;		/* The current node */
pcube dist_cube;	/* Node where distance changed from 0 to 1 */
int dist;		/* Distance so far between cofactoring cube and p */
int var;		/* Conflicting variable */
int level;		/* Level from the root of the tree */

{
    int k;

    if (find_oc_special_cases(p, overexpanded_cube, pNode, dist_cube, 
		dist, var, level)) {
	return;
    }

    else {

	if (dist == 0) {
	    for (k=0; k<=1; k++) {

		if (cdist0v(pNode->part_cube[k], p, pNode->var))
		    find_overexpanded_cube(p, overexpanded_cube,
				pNode->child[k], (pcube)NULL, 0, 0, level+1);

		else if (cdist0v(pNode->part_cube[k], overexpanded_cube,
			pNode->var)) {
		    d1_active = TRUE;
		    find_overexpanded_cube(p, overexpanded_cube,
			pNode->child[k], pNode->part_cube[1-k],
							1, pNode->var, level+1);
		}
	    }
	}

	else {  /* dist == 1 */

	    if (var == pNode->var) { /* Split is on the conflicting variable */
		find_overexpanded_cube(p, overexpanded_cube,
			    pNode->child[LEFT], dist_cube, 1, var, level+1);
		find_overexpanded_cube(p, overexpanded_cube,
			    pNode->child[RIGHT], dist_cube, 1, var, level+1);
	    }
	    else { /* Splitting variable is not the same as conflicting var */
		if (cdist0v(pNode->part_cube[LEFT], p, pNode->var))
		    find_overexpanded_cube(p, overexpanded_cube,
			    pNode->child[LEFT], dist_cube, 1, var, level+1);

		if ((cdist0v(pNode->part_cube[RIGHT], p, pNode->var))
		    && (d1_active))
		    find_overexpanded_cube(p, overexpanded_cube,
			    pNode->child[RIGHT], dist_cube, 1, var, level+1);
	    }
	}
    }
}

/*
 * Special cases for finding overexpanded cube.
 */
bool
find_oc_special_cases(p, overexpanded_cube, pNode, dist_cube, dist, var, level)
pcube p;		/* Node to be expanded */
pcube overexpanded_cube;/* overexpanded cube so far */
pnc_node pNode;		/* The current node */
pcube dist_cube;	/* Node where distance changed from 0 to 1 */
int dist;		/* Distance so far between cofactoring cube and p */
int var;		/* Conflicting variable */
int level;		/* Level from the root of the tree */

{

    pcube temp;
    pcube *T_d;
    pcube mask;
    int last_word, k;

    /* If all the literals present in p are either in overexpanded cube
       already or have been cofactored out, there is no need to continue */
    if (dist == 0) {
	temp = set_diff(new_cube(), overexpanded_cube, pNode->cof);
	if (setp_implies(temp, p)) {
	    free_cube(temp);
	    return(TRUE);
	}
	free_cube(temp);
    }

    if (pNode->cubelist != NULL) {
	if (level < Max_level) {  /* A unate leaf has been reached */

	    temp = new_cube();

	    if (dist == 0) {
		nc_or_unnec(p, pNode->cubelist, temp);
		(void) set_and(overexpanded_cube, overexpanded_cube, temp);
	    }

	    else { /* dist == 1 */
		if (var < cube.num_binary_vars) {
		    /* Conflicting variable is binary */

		    if (!nc_is_nec(p, pNode->cubelist)) {
			(void) set_and(overexpanded_cube,
					    overexpanded_cube, dist_cube);
			d1_active = FALSE;
		    }
		}

		else {
		    /* Conflicting variable is an mv.
		       Lower essential parts in overexpanded cube */

		    nc_or_unnec(p, pNode->cubelist, temp);
		    last_word = cube.last_word[var];
		    mask = cube.var_mask[var];
		    for (k=cube.first_word[var]; k<=last_word; k++)
			overexpanded_cube[k] &= temp[k] | ~mask[k];

		}
		    
	    }

	    free_cube(temp);

	    return(TRUE);
    
	}

	else {

	    /* The leaf is not necessarily unate. Switch to dynamic mode. */

	    /* Copy the cubelist because it will be disposed of by 
	       find_overexpanded_cube_dyn. */

	    temp = set_diff(new_cube(), cube.fullset, pNode->cubelist[0]);
	    if (setp_implies(temp, overexpanded_cube))
		T_d = nc_copy_cubelist(pNode->cubelist);
	    else {
		T_d = cofactor(pNode->cubelist, overexpanded_cube);
		nc_cof_contain(T_d);
	    }
	    free_cube(temp);

	    if (dist == 0)
		find_overexpanded_cube_dyn(p, overexpanded_cube, T_d,
						    (pcube)NULL, 0, 0, level+1);
	    else
		find_overexpanded_cube_dyn(p, overexpanded_cube, T_d,
						    dist_cube, 1, var, level+1);

	    free_cubelist(T_d);
	    return(TRUE);

	}
    }

    return(FALSE);
}

/*
 * Generate the blocking matrix for cube p.
 *
 * Compute the Blocking Matrix (reduced offset) recursively.
 */

pcover
setupBB(p, overexpanded_cube, pNode, level)
pcube p;
pcube overexpanded_cube;
pnc_node pNode;
int level;

{

    pset_family BBl, BBr;
    pcube cl, cr;
    int var;

    if (BB_special_cases(&BBl, p, overexpanded_cube, pNode, level)) {
	return(BBl);
    }

    else { /* Not quite at a leaf yet */

	 cl = pNode->part_cube[LEFT];
	 cr = pNode->part_cube[RIGHT];
	 var = pNode->var;

	/* Only those subtrees need to be considered that are not orthogonal 
	   to the overexpanded_cube */

	if (cdist0v(overexpanded_cube, cl, var)) {

	    BBl = setupBB(p, overexpanded_cube, pNode->child[LEFT], level+1);

	    if (cdist0v(p, cl, var)) {
		if (is_taut) return(BBl);
	    }
	    else {
		nc_sf_multiply(BBl, cl, var);
	    }

	    if (cdist0v(overexpanded_cube, cr, var)) {
		BBr = setupBB(p, overexpanded_cube, pNode->child[RIGHT], level+1);
		if (cdist0v(p, cr, var)) {
		    if (is_taut) {
			sf_free(BBl);
			return(BBr);
		    }
		    else {
			if (BBr->count == 0) {
			    sf_free(BBr);
			    return(BBl);
			}
			else {
			    BBl = sf_append(BBl, BBr);
			    return(BBl);
			}
		    }
		}
		else {
		    if (BBr->count == 0) {
			sf_free(BBr);
			return(BBl);
		    }
		    else {
			nc_sf_multiply(BBr, cr, var);
			BBl = sf_append(BBl, BBr);
			is_taut = FALSE;
			return(BBl);
		    }
		}
		
	    }
	    else {
		return(BBl);
	    }

	}

	/* Left subtree is distance 1 therefore right subtree must be
	   distance 0 from the overexpanded_cube */

	else {
		BBr = setupBB(p, overexpanded_cube, pNode->child[RIGHT], level+1);
		if ((cdist0v(p, cr, var)) || (BBr->count == 0)) return(BBr);

		is_taut = FALSE;
		nc_sf_multiply(BBr, cr, var);
		return(BBr);
	}

    }

}

/*
 * Special cases for setting up blocking matrix (reduced offset)
 * This routine uses global variable Num_act_vars declared in 
 * minimize.h
 */

bool
BB_special_cases(BB, p, overexpanded_cube, pNode, level)
pcover *BB;
pcube p;
pcube overexpanded_cube;
pnc_node pNode;
int level;

{

    pcube temp;
    pcube *T;

    if (!(level%N_level)) {

	/* If the cofactoring cube is contained in p, the cofactor
	   is a tautology. In this case return an empty cover. */
	if (level > Num_act_vars) {
	    temp = new_cube();
	    (void) set_diff(temp, cube.fullset, pNode->cof);
	    if (setp_implies(temp, p)) {
		free_cube(temp);
		is_taut = FALSE;
		*BB = new_cover(0); 
		return(TRUE);
	    }