bin_mincov.c

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

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

typedef struct _value_t {
    sm_element * elem;
    double value;
} value_t;

static int is_unate;
static int (*g_record_fun) ();    /* called at the recursion end (if non-nil) */
static int verify_cover();

static sm_matrix *A;    /* reordered matrix */
static int *weights;    /* column weights */

/* expanded[row_num] points to the element currently expanded;
 * it is 0 if rule 3 was applied at the corresponding row level 
 */
static sm_element ** expanded;

/* order[row_num] is an array of pointers to elements; the row should
 * be expanded in that order.
 */
static sm_element *** order;

/* partial prime currently generated, in set form, and its cost */
static bin_solution_t *sol;    
/* best prime up to now, in set form, and its cost */
static bin_solution_t *best;

/* stop at first leaf if true */
static int g_heu;
static int ended;

/* debugging and statistics variables */
static int leaves_count, r1, r2, r3, r4, r5;
static int g_debug, g_option, got_best;
static long start_time;
int call_count, cc;

static int compare (), compare_rev ();
static char * literal_name ();
static sm_matrix * reorder_rows ();
static sm_row * mat_minimum_cover ();

/* get the index of the complement of the current literal */
#define GETBAR(v) (((v)&1)?((v)-1):((v)+1))

/* flags stored in the user_word of each element */
#define EXPANDED    1
#define MARKED        2

/* do the binate covering of matrix M with weights w (might be NULL);
 * if heuristic != 0, terminate as soon as the first result is obtained;
 * g_debug gives the amount of debugging information;
 * ubound, if > 0, gives the best possible estimate of the covering cost.
 * Any row can be missing from M, but at least one column for each odd-even 
 * pair should be present.
 */

sm_row *
sm_mat_bin_minimum_cover (M, weights, heuristic, debug, ubound, option, record_fun)

sm_matrix *M;
int *weights;
int heuristic, debug, ubound, option;
int (*record_fun) ();

{
    is_unate = 0;
    return mat_minimum_cover (M, weights, heuristic, debug, ubound, 
        option, record_fun);
}

sm_row *
sm_mat_minimum_cover (M, weights, heuristic, debug, ubound, option, record_fun)

sm_matrix *M;
int *weights;
int heuristic, debug, ubound, option;
int (*record_fun) ();

{
    is_unate = 1;
    return mat_minimum_cover (M, weights, heuristic, debug, ubound, 
        option, record_fun);
}

static sm_row *
mat_minimum_cover (M, w, heuristic, l_debug, ubound, l_option, record_fun)

sm_matrix *M;
int *w;
int heuristic, l_debug, ubound, l_option;
int (*record_fun) ();

{
    int nelem, i, row, col, cost, added, toadd;
    double sparsity, *col_value_save;
    sm_row *prow, *result;
    sm_col *pcol;
    sm_matrix *M_save, *temp1, *temp;
    sm_element *elem;
    value_t * col_value;
    pset unate;

    g_debug = l_debug;
    g_record_fun = record_fun;
    g_option = l_option;
    g_heu = heuristic;
    weights = w;
    ended = 0;
    M_save = NIL(sm_matrix);

    if (M->nrows <= 0) {
        return sm_row_alloc();
    }

    if (g_debug > 0) {
        start_time = util_cpu_time();

        /* Check the matrix sparsity */
        nelem = 0;
        sm_foreach_row(M, prow) {
            nelem += prow->length;
        }
        sparsity = (double) nelem / (double) (M->nrows * M->ncols);
        (void) fprintf(misout, "matrix     = %d by %d with %d elements (%4.3f%%)\n",
            M->nrows, M->ncols, nelem, sparsity * 100.0); 
    }
    if (g_debug > 3) {
        (void) fprintf (misout, "Weights:\n");
        for (i = 0; i < M->last_col->col_num + 1; i++) {
            (void) fprintf (misout, "%d ", WEIGHT(w, i));
        }
        (void) fprintf (misout, "\n");
        (void) fprintf (misout, "Matrix:\n");
        sm_print(misout, M);
        (void) fprintf (misout, "\n");
    }

    if (g_option & 2048) {
    /* reorder rows such that the tree-like ordering is preserved */
        M_save = M;
        M = sm_dup (M_save);
        A = sm_alloc ();

        unate = set_clear (set_new (M->last_col->col_num + 1), 
            M->last_col->col_num + 1);
        do {
            added = 0;
            temp = sm_alloc ();
            /* find unate columns */
            sm_foreach_col (M, pcol) {
                if (pcol->col_num % 2) {
                    if (! pcol->prev_col ||
                        pcol->prev_col->col_num != pcol->col_num - 1) {
                        set_insert (unate, pcol->col_num);
                        set_insert (unate, (pcol->col_num - 1));
                    }
                }
                else {
                    if (! pcol->next_col ||
                    pcol->next_col->col_num != pcol->col_num + 1) {
                        set_insert (unate, pcol->col_num);
                        set_insert (unate, (pcol->col_num + 1));
                    }
                }
            }

            /* check if all elements are unate */
            for (i = 0; M->nrows && i <= M->last_row->row_num; i++) {
                if (! (prow = sm_get_row (M, i))) {
                    continue;
                }

                toadd = 1;
                sm_foreach_row_element (prow, elem) {
                    if (! is_in_set (unate, elem->col_num)) {
                        toadd = 0;
                        break;
                    }
                }
                if (toadd) {
                    added = 1;
                    row = temp->nrows;
                    sm_foreach_row_element (prow, elem) {
                        (void) sm_insert (temp, row, elem->col_num);
                    }
                    sm_delrow (M, prow->row_num);
                    i--;
                }
            }

            /* check if all positive elements are unate */
            for (i = 0; M->nrows && i <= M->last_row->row_num; i++) {
                if (! (prow = sm_get_row (M, i))) {
                    continue;
                }

                toadd = 1;
                sm_foreach_row_element (prow, elem) {
                    if (! (elem->col_num % 2) &&
                        ! is_in_set (unate, elem->col_num)) {
                        toadd = 0;
                        break;
                    }
                }
                if (toadd) {
                    added = 1;
                    row = temp->nrows;
                    sm_foreach_row_element (prow, elem) {
                        (void) sm_insert (temp, row, elem->col_num);
                    }
                    sm_delrow (M, prow->row_num);
                    i--;
                }
            }

            temp1 = reorder_rows (temp);
            sm_foreach_row (temp1, prow) {
                row = A->nrows;
                sm_foreach_row_element (prow, elem) {
                    (void) sm_insert (A, row, elem->col_num);
                }
            }
            sm_free (temp);
            sm_free (temp1);
        } while (added && M->nrows);

        if (M->nrows) {
            (void) fprintf (miserr, 
                "warning: unate heuristics left %d rows out of %d\n",
                M->nrows, A->nrows + M->nrows);
            if (g_debug > 2) {
                (void) fprintf (misout, "Left-over ratrix:\n");
                sm_print(misout, M);
                (void) fprintf (misout, "\n");
            }
            temp = sm_alloc ();
            sm_foreach_row (M, prow) {
                row = temp->nrows;
                sm_foreach_row_element (prow, elem) {
                    (void) sm_insert (temp, row, elem->col_num);
                }
            }
            temp1 = reorder_rows (temp);
            sm_foreach_row (temp1, prow) {
                row = A->nrows;
                sm_foreach_row_element (prow, elem) {
                    (void) sm_insert (A, row, elem->col_num);
                }
            }
            sm_free (temp);
            sm_free (temp1);
        }
        sm_free (M);

        M = M_save;
        set_free (unate);
    }
    else {
        A = reorder_rows (M);
    }

    /* reorder cols; at every level the column pair with most elements BELOW
     * it is put first; weights might be used also... 
     */
    col_value = ALLOC (value_t, A->last_col->col_num + 1);
    col_value_save = ALLOC (double, A->last_col->col_num + 1);
    order = ALLOC (sm_element **, A->nrows);

    for (col = 0; col <= A->last_col->col_num; col++) {
        col_value_save[col] = 0.0;
    }

    /* run through the rows in reverse order */
    for (row = A->nrows - 1; row >= 0; row--) {
        prow = sm_get_row (A, row);

        col = 0;
        sm_foreach_row_element (prow, elem) {
            if (is_unate) {
                col_value_save[elem->col_num]++;
            }
            else {
                if (g_option & 4) {
                    /* skip odd columns */
                    if (! (elem->col_num % 2)) {
                        col_value_save[elem->col_num / 2]++;
                    }
                }
                else {
                    col_value_save[elem->col_num / 2]++;
                }
            }

            col_value[col].elem = elem;

            if (is_unate) {
                col_value[col].value = col_value_save[elem->col_num];
            }
            else {
                col_value[col].value = col_value_save[elem->col_num / 2];
                if (g_option & 64) {
                    if (WEIGHT(weights, elem->col_num) > 0) {
                        col_value[col].value /= WEIGHT(weights, elem->col_num);
                    }
                    else {
                        col_value[col].value *= 2;
                    }
                }
                if (g_option & 32) {
                    /* leave odd columns first */
                    if (elem->col_num % 2) {
                        col_value[col].value = 1000000.0;
                    }
                }
                else if (g_option & 128) {
                    /* leave odd columns last */
                    if (elem->col_num % 2) {
                        col_value[col].value = 0.0;
                    }
                }
            }

            col++;
        }

        if (g_option & 8) {
            /* do not sort columns */
        }
        else {
            if (g_option & 16) {
                qsort ((char*) col_value, col, sizeof(value_t), compare_rev);
            }
            else {
                qsort ((char*) col_value, col, sizeof(value_t), compare);
            }
        }

        order[row] = ALLOC (sm_element *, prow->length);

        for (col = 0; col < prow->length; col++) {
            order[row][col] = col_value[col].elem;
        }
    }

    /* statically allocate the stacks */
    expanded = ALLOC (sm_element *, A->nrows);

    if (g_debug > 2) {
        (void) fprintf (misout, "Col ordering:\n");
        for (row = 0; row < A->nrows; row++) {
            (void) fprintf (misout, "%d: ", row);
            prow = sm_get_row (A, row);
            for (col = 0; col < prow->length; col++) {
                (void) fprintf (misout, "%d ", order[row][col]->col_num);
            }
            (void) fprintf (misout, "\n");
        }
    }

    if (g_debug > 3) {
        (void) fprintf (misout, "Reordered matrix:\n");
        sm_print (misout, A);
        (void) fprintf (misout, "\n");
    }

    if (g_debug > 1) {
        (void) fprintf(misout, "reordering done (time is %s)\n", 
            util_print_time(util_cpu_time() - start_time));
    }

    /* give an upper bound (for rule 5) if available */
    got_best = 0;
    sol = bin_solution_alloc (A->last_col->col_num + 1);
    best = bin_solution_alloc (A->last_col->col_num + 1);
    if (ubound > 0) {
        /* hope we'll succeed... */
        best->cost = ubound;
    }
    else {
        /* not a very good bound... */
        sm_foreach_col (A, pcol) {
            best->cost += WEIGHT(weights, pcol->col_num);
        }
    }
    best->cost++;

    /* do the actual work */
    sm_bin_mincov (0);

    if (! g_record_fun) {
        /* check out various things */
        if (! got_best) {
            (void) fprintf(miserr,"internal error; couldn't improve on bound\n");
	    (void) fprintf(miserr,"unsatisfiable binate covering matrix ?\n");
            exit(-1);
        }

        /* put back the solution in sparse matrix (reordered) form */
        result = sm_row_alloc();
        for (i = 0; i < A->last_col->col_num + 1; i++) {
            if (is_in_set (best->set, i)) {
                sm_row_insert (result, i);
            }
        }

        if (g_debug > 0) {
            (void) fprintf (misout, "calls %d leaves %d r1 %d r2 %d r3 %d r4 %d r5 %d\n", 
                call_count, leaves_count, r1, r2, r3, r4, r5);

            if (g_debug > 1) {
                (void) fprintf (misout, "Solution is ");
                sm_row_print (misout, result);
                (void) fprintf (misout, "\n");
            }

            (void) fprintf(misout, "best solution %d; time %s\n", best->cost,
                util_print_time(util_cpu_time() - start_time));
        }

        /* check the cost and the result itself ... */
        cost = 0;
        sm_foreach_row_element (result, elem) {
            cost += WEIGHT (w, elem->col_num);
        }
        if (cost != best->cost) {
            (void) fprintf (miserr, "Solution cost is corrupted\n");
            exit (-1);
        }
        if (! verify_cover(M, result)) {
            (void) fprintf (misout, "Illegal solution ");
            sm_row_print (misout, result);
            (void) fprintf (misout, "\nwith cost %d\n", best->cost);

            (void) fprintf (miserr, "internal error -- cover verification failed\n");
            exit (-1);
        }
    }

    FREE (expanded);
    FREE (col_value);
    FREE (col_value_save);
    bin_solution_free(best);
    bin_solution_free(sol);
    for (row = A->nrows - 1; row >= 0; row--) {
        FREE (order[row]);
    }
    FREE (order);
    sm_free (A);

    return result;
}

/* reorder the rows of M according to g_option */
static sm_matrix *
reorder_rows (M)

sm_matrix *M;