ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
indep.c
Go to the documentation of this file.
1/*
2 * Revision Control Information
3 *
4 * $Source$
5 * $Author$
6 * $Revision$
7 * $Date$
8 *
9 */
10#include "mincov_int.h"
11
13
14
15static sm_matrix *build_intersection_matrix();
16
17
18#if 0
19/*
20 * verify that all rows in 'indep' are actually independent !
21 */
22static int
23verify_indep_set(A, indep)
24sm_matrix *A;
25sm_row *indep;
26{
27 register sm_row *prow, *prow1;
28 register sm_element *p, *p1;
29
30 for(p = indep->first_col; p != 0; p = p->next_col) {
31 prow = sm_get_row(A, p->col_num);
32 for(p1 = p->next_col; p1 != 0; p1 = p1->next_col) {
33 prow1 = sm_get_row(A, p1->col_num);
34 if (sm_row_intersects(prow, prow1)) {
35 return 0;
36 }
37 }
38 }
39 return 1;
40}
41#endif
42
45sm_matrix *A;
46int *weight;
47{
48 register sm_row *best_row, *prow;
49 register sm_element *p;
50 int least_weight;
51 sm_row *save;
52 sm_matrix *B;
53 solution_t *indep;
54
55 indep = solution_alloc();
56 B = build_intersection_matrix(A);
57
58 while (B->nrows > 0) {
59 /* Find the row which is disjoint from a maximum number of rows */
60 best_row = B->first_row;
61 for(prow = B->first_row->next_row; prow != 0; prow = prow->next_row) {
62 if (prow->length < best_row->length) {
63 best_row = prow;
64 }
65 }
66
67 /* Find which element in this row has least weight */
68 if (weight == NIL(int)) {
69 least_weight = 1;
70 } else {
71 prow = sm_get_row(A, best_row->row_num);
72 least_weight = weight[prow->first_col->col_num];
73 for(p = prow->first_col->next_col; p != 0; p = p->next_col) {
74 if (weight[p->col_num] < least_weight) {
75 least_weight = weight[p->col_num];
76 }
77 }
78 }
79 indep->cost += least_weight;
80 (void) sm_row_insert(indep->row, best_row->row_num);
81
82 /* Discard the rows which intersect this row */
83 save = sm_row_dup(best_row);
84 for(p = save->first_col; p != 0; p = p->next_col) {
85 sm_delrow(B, p->col_num);
86 sm_delcol(B, p->col_num);
87 }
88 sm_row_free(save);
89 }
90
91 sm_free(B);
92
93/*
94 if (! verify_indep_set(A, indep->row)) {
95 fail("sm_maximal_independent_set: row set is not independent");
96 }
97*/
98 return indep;
99}
100
101static sm_matrix *
102build_intersection_matrix(A)
103sm_matrix *A;
104{
105 register sm_row *prow, *prow1;
106 register sm_element *p, *p1;
107 register sm_col *pcol;
108 sm_matrix *B;
109
110 /* Build row-intersection matrix */
111 B = sm_alloc();
112 for(prow = A->first_row; prow != 0; prow = prow->next_row) {
113
114 /* Clear flags on all rows we can reach from row 'prow' */
115 for(p = prow->first_col; p != 0; p = p->next_col) {
116 pcol = sm_get_col(A, p->col_num);
117 for(p1 = pcol->first_row; p1 != 0; p1 = p1->next_row) {
118 prow1 = sm_get_row(A, p1->row_num);
119 prow1->flag = 0;
120 }
121 }
122
123 /* Now record which rows can be reached */
124 for(p = prow->first_col; p != 0; p = p->next_col) {
125 pcol = sm_get_col(A, p->col_num);
126 for(p1 = pcol->first_row; p1 != 0; p1 = p1->next_row) {
127 prow1 = sm_get_row(A, p1->row_num);
128 if (! prow1->flag) {
129 prow1->flag = 1;
130 (void) sm_insert(B, prow->row_num, prow1->row_num);
131 }
132 }
133 }
134 }
135
136 return B;
137}
139
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define NIL(type)
Definition avl.h:25
Cube * p
Definition exorList.c:222
ABC_NAMESPACE_IMPL_START sm_matrix * sm_alloc()
Definition matrix.c:31
solution_t * solution_alloc()
Definition solution.c:17
solution_t * sm_maximal_independent_set()
struct solution_struct solution_t
Definition mincov_int.h:35
typedefABC_NAMESPACE_HEADER_START struct sm_element_struct sm_element
Definition sparse.h:21
struct sm_col_struct sm_col
Definition sparse.h:23
void sm_delcol()
int sm_row_intersects()
#define sm_get_row(A, rownum)
Definition sparse.h:93
void sm_row_free()
sm_element * sm_row_insert()
void sm_free()
void sm_delrow()
struct sm_matrix_struct sm_matrix
Definition sparse.h:24
sm_element * sm_insert()
struct sm_row_struct sm_row
Definition sparse.h:22
sm_row * sm_row_dup()
#define sm_get_col(A, colnum)
Definition sparse.h:89
sm_element * first_row
Definition sparse.h:63
sm_row * first_row
Definition sparse.h:79
sm_element * first_col
Definition sparse.h:48
int row_num
Definition sparse.h:45
sm_row * next_row
Definition sparse.h:50