pair.c

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

/*
 * Revision Control Information
 *
 * $Source: /projects/mvsis/Repository/mvsis-1.3/src/sis/espresso/pair.c,v $
 * $Author: wjiang $
 * $Revision: 1.1.1.1 $
 * $Date: 2003/02/24 22:24:08 $
 *
 */
#include "espresso.h"

void set_pair(PLA)
pPLA PLA;
{
    set_pair1(PLA, TRUE);
}

void set_pair1(PLA, adjust_labels)
pPLA PLA;
bool adjust_labels;
{
    int i, var, *paired, newvar;
    int old_num_vars, old_num_binary_vars, old_size, old_mv_start;
    int *new_part_size, new_num_vars, new_num_binary_vars, new_mv_start;
    ppair pair = PLA->pair;
    char scratch[1000], **oldlabel, *var1, *var1bar, *var2, *var2bar;

    if (adjust_labels)
	makeup_labels(PLA);

    /* Check the pair structure for valid entries and see which binary
	variables are left unpaired
    */
    paired = ALLOC(bool, cube.num_binary_vars);
    for(var = 0; var < cube.num_binary_vars; var++)
	paired[var] = FALSE;
    for(i = 0; i < pair->cnt; i++)
	if ((pair->var1[i] > 0 && pair->var1[i] <= cube.num_binary_vars) &&
	     (pair->var2[i] > 0 && pair->var2[i] <= cube.num_binary_vars)) {
	    paired[pair->var1[i]-1] = TRUE;
	    paired[pair->var2[i]-1] = TRUE;
	} else
	    fatal("can only pair binary-valued variables");

    PLA->F = delvar(pairvar(PLA->F, pair), paired);
    PLA->R = delvar(pairvar(PLA->R, pair), paired);
    PLA->D = delvar(pairvar(PLA->D, pair), paired);

    /* Now painfully adjust the cube size */
    old_size = cube.size;
    old_num_vars = cube.num_vars;
    old_num_binary_vars = cube.num_binary_vars;
    old_mv_start = cube.first_part[cube.num_binary_vars];
    /* Create the new cube.part_size vector and setup the cube structure */
    new_num_binary_vars = 0;
    for(var = 0; var < old_num_binary_vars; var++)
	new_num_binary_vars += (paired[var] == FALSE);
    new_num_vars = new_num_binary_vars + pair->cnt;
    new_num_vars += old_num_vars - old_num_binary_vars;
    new_part_size = ALLOC(int, new_num_vars);
    for(var = 0; var < pair->cnt; var++)
	new_part_size[new_num_binary_vars + var] = 4;
    for(var = 0; var < old_num_vars - old_num_binary_vars; var++)
	new_part_size[new_num_binary_vars + pair->cnt + var] =
	    cube.part_size[old_num_binary_vars + var];
    setdown_cube();
    FREE(cube.part_size);
    cube.num_vars = new_num_vars;
    cube.num_binary_vars = new_num_binary_vars;
    cube.part_size = new_part_size;
    cube_setup();

    /* hack with the labels to get them correct */
    if (adjust_labels) {
	oldlabel = PLA->label;
	PLA->label = ALLOC(char *, cube.size);
	for(var = 0; var < pair->cnt; var++) {
	    newvar = cube.num_binary_vars*2 + var*4;
	    var1 = oldlabel[ (pair->var1[var]-1) * 2 + 1];
	    var2 = oldlabel[ (pair->var2[var]-1) * 2 + 1];
	    var1bar = oldlabel[ (pair->var1[var]-1) * 2];
	    var2bar = oldlabel[ (pair->var2[var]-1) * 2];
	    (void) sprintf(scratch, "%s+%s", var1bar, var2bar);
	    PLA->label[newvar] = util_strsav(scratch);
	    (void) sprintf(scratch, "%s+%s", var1bar, var2);
	    PLA->label[newvar+1] = util_strsav(scratch);
	    (void) sprintf(scratch, "%s+%s", var1, var2bar);
	    PLA->label[newvar+2] = util_strsav(scratch);
	    (void) sprintf(scratch, "%s+%s", var1, var2);
	    PLA->label[newvar+3] = util_strsav(scratch);
	}
	/* Copy the old labels for the unpaired binary vars */
	i = 0;
	for(var = 0; var < old_num_binary_vars; var++) {
	    if (paired[var] == FALSE) {
		PLA->label[2*i] = oldlabel[2*var];
		PLA->label[2*i+1] = oldlabel[2*var+1];
		oldlabel[2*var] = oldlabel[2*var+1] = (char *) NULL;
		i++;
	    }
	}
	/* Copy the old labels for the remaining unpaired vars */
	new_mv_start = cube.num_binary_vars*2 + pair->cnt*4;
	for(i = old_mv_start; i < old_size; i++) {
	    PLA->label[new_mv_start + i - old_mv_start] = oldlabel[i];
	    oldlabel[i] = (char *) NULL;
	}
	/* free remaining entries in oldlabel */
	for(i = 0; i < old_size; i++)
	    if (oldlabel[i] != (char *) NULL)
		FREE(oldlabel[i]);
	FREE(oldlabel);
    }

    /* the paired variables should not be sparse (cf. mv_reduce/raise_in)*/
    for(var = 0; var < pair->cnt; var++)
	cube.sparse[cube.num_binary_vars + var] = 0;
    FREE(paired);
}

pcover pairvar(A, pair)
pcover A;
ppair pair;
{
    register pcube last, p;
    register int val, p1, p2, b1, b0;
    int insert_col, pairnum;

    insert_col = cube.first_part[cube.num_vars - 1];

    /* stretch the cover matrix to make room for the paired variables */
    A = sf_delcol(A, insert_col, -4*pair->cnt);

    /* compute the paired values */
    foreach_set(A, last, p) {
	for(pairnum = 0; pairnum < pair->cnt; pairnum++) {
	    p1 = cube.first_part[pair->var1[pairnum] - 1];
	    p2 = cube.first_part[pair->var2[pairnum] - 1];
	    b1 = is_in_set(p, p2+1);
	    b0 = is_in_set(p, p2);
	    val = insert_col + pairnum * 4;
	    if (/* a0 */ is_in_set(p, p1)) {
		if (b0)
		    set_insert(p, val + 3);
		if (b1)
		    set_insert(p, val + 2);
	    }
	    if (/* a1 */ is_in_set(p, p1+1)) {
		if (b0)
		    set_insert(p, val + 1);
		if (b1)
		    set_insert(p, val);
	    }
	}
    }
    return A;
}


/* delvar -- delete variables from A, minimize the number of column shifts */
pcover delvar(A, paired)
pcover A;
bool paired[];
{
    bool run;
    int first_run, run_length, var, offset = 0;

    run = FALSE; run_length = 0;
    for(var = 0; var < cube.num_binary_vars; var++)
	if (paired[var])
	    if (run)
		run_length += cube.part_size[var];
	    else {
		run = TRUE;
		first_run = cube.first_part[var];
		run_length = cube.part_size[var];
	    }
	else
	    if (run) {
		A = sf_delcol(A, first_run-offset, run_length);
		run = FALSE;
		offset += run_length;
	    }
    if (run)
	A = sf_delcol(A, first_run-offset, run_length);
    return A;
}

/*
    find_optimal_pairing -- find which binary variables should be paired
    to maximally reduce the number of terms

    This is essentially the technique outlined by T. Sasao in the
    Trans. on Comp., Oct 1984.  We estimate the cost of pairing each
    pair individually using 1 of 4 strategies: (1) algebraic division
    of F by the pair (exactly T. Sasao technique); (2) strong division
    of F by the paired variables (using REDUCE/EXPAND/ IRREDUNDANT from
    espresso); (3) full minimization using espresso; (4) exact
    minimization.  These are in order of both increasing accuracy and
    increasing difficulty (!)

    Once the n squared pairs have been evaluated, T. Sasao proposes a
    graph covering of nodes by disjoint edges.  For now, I solve this
    problem exhaustively (complexity = (n-1)*(n-3)*...*3*1 for n
    variables when n is even).  Note that solving this problem exactly
    is the same as evaluating the cost function for all possible
    pairings.

			       n       pairs

			     1, 2           1
			     3, 4           3
			     5, 6          15
			     7, 8         105
			     9,10         945
			    11,12      10,395
			    13,14     135,135
			    15,16   2,027,025
			    17,18  34,459,425
			    19,20 654,729,075
*/
void find_optimal_pairing(PLA, strategy)
pPLA PLA;
int strategy;
{
    int i, j, **cost_array;

    cost_array = find_pairing_cost(PLA, strategy);

    if (summary) {
	(void) printf("    ");
	for(i = 0; i < cube.num_binary_vars; i++)
	    (void) printf("%3d ", i+1);
	(void) printf("\n");
	for(i = 0; i < cube.num_binary_vars; i++) {
	    (void) printf("%3d ", i+1);
	    for(j = 0; j < cube.num_binary_vars; j++)
		(void) printf("%3d ", cost_array[i][j]);
	    (void) printf("\n");
	}
    }

    if (cube.num_binary_vars <= 14) {
	PLA->pair = pair_best_cost(cost_array);
    } else {
	(void) greedy_best_cost(cost_array, &(PLA->pair));
    }
    (void) printf("# ");
    print_pair(PLA->pair);
	
    for(i = 0; i < cube.num_binary_vars; i++)
	FREE(cost_array[i]);
    FREE(cost_array);

    set_pair(PLA);
    EXEC_S(PLA->F=espresso(PLA->F,PLA->D,PLA->R),"ESPRESSO  ",PLA->F);
}

int **find_pairing_cost(PLA, strategy)
pPLA PLA;
int strategy;
{
    int var1, var2, **cost_array;
    int i, j, xnum_binary_vars, xnum_vars, *xpart_size, cost;
    pcover T, Fsave, Dsave, Rsave;
    pset mask;
/*    char *s;*/

    /* data is returned in the cost array */
    cost_array = ALLOC(int *, cube.num_binary_vars);
    for(i = 0; i < cube.num_binary_vars; i++)
	cost_array[i] = ALLOC(int, cube.num_binary_vars);
    for(i = 0; i < cube.num_binary_vars; i++)
	for(j = 0; j < cube.num_binary_vars; j++)
	    cost_array[i][j] = 0;

    /* Setup the pair structure for pairing variables together */
    PLA->pair = pair_new(1);
    PLA->pair->cnt = 1;

    for(var1 = 0; var1 < cube.num_binary_vars-1; var1++) {
	for(var2 = var1+1; var2 < cube.num_binary_vars; var2++) {
	    /* if anything but simple strategy, perform setup */
	    if (strategy > 0) {
		/* save the original covers */
		Fsave = sf_save(PLA->F);
		Dsave = sf_save(PLA->D);
		Rsave = sf_save(PLA->R);

		/* save the original cube structure */
		xnum_binary_vars = cube.num_binary_vars;
		xnum_vars = cube.num_vars;
		xpart_size = ALLOC(int, cube.num_vars);
		for(i = 0; i < cube.num_vars; i++)
		    xpart_size[i] = cube.part_size[i];

		/* pair two variables together */
		PLA->pair->var1[0] = var1 + 1;
		PLA->pair->var2[0] = var2 + 1;
		set_pair1(PLA, /* adjust_labels */ FALSE);
	    }


	    /* decide how to best estimate worth of this pairing */
	    switch(strategy) {
		case 3:
		    /*s = "exact minimization";*/
		    PLA->F = minimize_exact(PLA->F, PLA->D, PLA->R, 1);
		    cost = Fsave->count - PLA->F->count;
		    break;
		case 2:
		    /*s = "full minimization";*/
		    PLA->F = espresso(PLA->F, PLA->D, PLA->R);
		    cost = Fsave->count - PLA->F->count;
		    break;
		case 1:
		    /*s = "strong division";*/
		    PLA->F = reduce(PLA->F, PLA->D);
		    PLA->F = expand(PLA->F, PLA->R, FALSE);
		    PLA->F = irredundant(PLA->F, PLA->D);
		    cost = Fsave->count - PLA->F->count;
		    break;
		case 0:
		    /*s = "weak division";*/
		    mask = new_cube();
		    (void) set_or(mask, cube.var_mask[var1], cube.var_mask[var2]);
		    T = dist_merge(sf_save(PLA->F), mask);
		    cost = PLA->F->count - T->count;
		    sf_free(T);
		    set_free(mask);
	    }

	    cost_array[var1][var2] = cost;

	    if (strategy > 0) {
		/* restore the original cube structure -- free the new ones */
		setdown_cube();
		FREE(cube.part_size);