abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
irred.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 "espresso.h"
11 
13 
14 
15 static void fcube_is_covered();
16 static void ftautology();
17 static bool ftaut_special_cases();
18 
19 
20 static int Rp_current;
21 
22 /*
23  * irredundant -- Return a minimal subset of F
24  */
25 
26 pcover
28 pcover F, D;
29 {
30  mark_irredundant(F, D);
31  return sf_inactive(F);
32 }
33 
34 
35 /*
36  * mark_irredundant -- find redundant cubes, and mark them "INACTIVE"
37  */
38 
39 void
41 pcover F, D;
42 {
43  pcover E, Rt, Rp;
44  pset p, p1, last;
45  sm_matrix *table;
46  sm_row *cover;
47  sm_element *pe;
48 
49  /* extract a minimum cover */
50  irred_split_cover(F, D, &E, &Rt, &Rp);
51  table = irred_derive_table(D, E, Rp);
52  cover = sm_minimum_cover(table, NIL(int), /* heuristic */ 1, /* debug */ 0);
53 
54  /* mark the cubes for the result */
55  foreach_set(F, last, p) {
56  RESET(p, ACTIVE);
57  RESET(p, RELESSEN);
58  }
59  foreach_set(E, last, p) {
60  p1 = GETSET(F, SIZE(p));
61  assert(setp_equal(p1, p));
62  SET(p1, ACTIVE);
63  SET(p1, RELESSEN); /* for essen(), mark as rel. ess. */
64  }
65  sm_foreach_row_element(cover, pe) {
66  p1 = GETSET(F, pe->col_num);
67  SET(p1, ACTIVE);
68  }
69 
70  if (debug & IRRED) {
71  printf("# IRRED: F=%d E=%d R=%d Rt=%d Rp=%d Rc=%d Final=%d Bound=%d\n",
72  F->count, E->count, Rt->count+Rp->count, Rt->count, Rp->count,
73  cover->length, E->count + cover->length, 0);
74  }
75 
76  free_cover(E);
77  free_cover(Rt);
78  free_cover(Rp);
79  sm_free(table);
80  sm_row_free(cover);
81 }
82 
83 /*
84  * irred_split_cover -- find E, Rt, and Rp from the cover F, D
85  *
86  * E -- relatively essential cubes
87  * Rt -- totally redundant cubes
88  * Rp -- partially redundant cubes
89  */
90 
91 void
92 irred_split_cover(F, D, E, Rt, Rp)
93 pcover F, D;
94 pcover *E, *Rt, *Rp;
95 {
96  register pcube p, last;
97  register int index;
98  pcover R;
99  pcube *FD, *ED;
100 
101  /* number the cubes of F -- these numbers track into E, Rp, Rt, etc. */
102  index = 0;
103  foreach_set(F, last, p) {
104  PUTSIZE(p, index);
105  index++;
106  }
107 
108  *E = new_cover(10);
109  *Rt = new_cover(10);
110  *Rp = new_cover(10);
111  R = new_cover(10);
112 
113  /* Split F into E and R */
114  FD = cube2list(F, D);
115  foreach_set(F, last, p) {
116  if (cube_is_covered(FD, p)) {
117  R = sf_addset(R, p);
118  } else {
119  *E = sf_addset(*E, p);
120  }
121  if (debug & IRRED1) {
122  (void) printf("IRRED1: zr=%d ze=%d to-go=%d time=%s\n",
123  R->count, (*E)->count, F->count - (R->count + (*E)->count),
124  print_time(ptime()));
125  }
126  }
127  free_cubelist(FD);
128 
129  /* Split R into Rt and Rp */
130  ED = cube2list(*E, D);
131  foreach_set(R, last, p) {
132  if (cube_is_covered(ED, p)) {
133  *Rt = sf_addset(*Rt, p);
134  } else {
135  *Rp = sf_addset(*Rp, p);
136  }
137  if (debug & IRRED1) {
138  (void) printf("IRRED1: zr=%d zrt=%d to-go=%d time=%s\n",
139  (*Rp)->count, (*Rt)->count,
140  R->count - ((*Rp)->count +(*Rt)->count), print_time(ptime()));
141  }
142  }
143  free_cubelist(ED);
144 
145  free_cover(R);
146 }
147 
148 /*
149  * irred_derive_table -- given the covers D, E and the set of
150  * partially redundant primes Rp, build a covering table showing
151  * possible selections of primes to cover Rp.
152  */
153 
154 sm_matrix *
156 pcover D, E, Rp;
157 {
158  register pcube last, p, *list;
159  sm_matrix *table;
160  int size_last_dominance, i;
161 
162  /* Mark each cube in DE as not part of the redundant set */
163  foreach_set(D, last, p) {
164  RESET(p, REDUND);
165  }
166  foreach_set(E, last, p) {
167  RESET(p, REDUND);
168  }
169 
170  /* Mark each cube in Rp as partially redundant */
171  foreach_set(Rp, last, p) {
172  SET(p, REDUND); /* belongs to redundant set */
173  }
174 
175  /* For each cube in Rp, find ways to cover its minterms */
176  list = cube3list(D, E, Rp);
177  table = sm_alloc();
178  size_last_dominance = 0;
179  i = 0;
180  foreach_set(Rp, last, p) {
181  Rp_current = SIZE(p);
182  fcube_is_covered(list, p, table);
183  RESET(p, REDUND); /* can now consider this cube redundant */
184  if (debug & IRRED1) {
185  (void) printf("IRRED1: %d of %d to-go=%d, table=%dx%d time=%s\n",
186  i, Rp->count, Rp->count - i,
187  table->nrows, table->ncols, print_time(ptime()));
188  }
189  /* try to keep memory limits down by reducing table as we go along */
190  if (table->nrows - size_last_dominance > 1000) {
191  (void) sm_row_dominance(table);
192  size_last_dominance = table->nrows;
193  if (debug & IRRED1) {
194  (void) printf("IRRED1: delete redundant rows, now %dx%d\n",
195  table->nrows, table->ncols);
196  }
197  }
198  i++;
199  }
200  free_cubelist(list);
201 
202  return table;
203 }
204 
205 /* cube_is_covered -- determine if a cubelist "covers" a single cube */
206 bool
208 pcube *T, c;
209 {
210  return tautology(cofactor(T,c));
211 }
212 
213 
214 
215 /* tautology -- answer the tautology question for T */
216 bool
218 pcube *T; /* T will be disposed of */
219 {
220  register pcube cl, cr;
221  register int best, result;
222  static int taut_level = 0;
223 
224  if (debug & TAUT) {
225  debug_print(T, "TAUTOLOGY", taut_level++);
226  }
227 
228  if ((result = taut_special_cases(T)) == MAYBE) {
229  cl = new_cube();
230  cr = new_cube();
231  best = binate_split_select(T, cl, cr, TAUT);
232  result = tautology(scofactor(T, cl, best)) &&
233  tautology(scofactor(T, cr, best));
234  free_cubelist(T);
235  free_cube(cl);
236  free_cube(cr);
237  }
238 
239  if (debug & TAUT) {
240  printf("exit TAUTOLOGY[%d]: %s\n", --taut_level, print_bool(result));
241  }
242  return result;
243 }
244 
245 /*
246  * taut_special_cases -- check special cases for tautology
247  */
248 
249 bool
251 pcube *T; /* will be disposed if answer is determined */
252 {
253  register pcube *T1, *Tsave, p, ceil=cube.temp[0], temp=cube.temp[1];
254  pcube *A, *B;
255  int var;
256 
257  /* Check for a row of all 1's which implies tautology */
258  for(T1 = T+2; (p = *T1++) != NULL; ) {
259  if (full_row(p, T[0])) {
260  free_cubelist(T);
261  return TRUE;
262  }
263  }
264 
265  /* Check for a column of all 0's which implies no tautology */
266 start:
267  INLINEset_copy(ceil, T[0]);
268  for(T1 = T+2; (p = *T1++) != NULL; ) {
269  INLINEset_or(ceil, ceil, p);
270  }
271  if (! setp_equal(ceil, cube.fullset)) {
272  free_cubelist(T);
273  return FALSE;
274  }
275 
276  /* Collect column counts, determine unate variables, etc. */
277  massive_count(T);
278 
279  /* If function is unate (and no row of all 1's), then no tautology */
280  if (cdata.vars_unate == cdata.vars_active) {
281  free_cubelist(T);
282  return FALSE;
283 
284  /* If active in a single variable (and no column of 0's) then tautology */
285  } else if (cdata.vars_active == 1) {
286  free_cubelist(T);
287  return TRUE;
288 
289  /* Check for unate variables, and reduce cover if there are any */
290  } else if (cdata.vars_unate != 0) {
291  /* Form a cube "ceil" with full variables in the unate variables */
292  (void) set_copy(ceil, cube.emptyset);
293  for(var = 0; var < cube.num_vars; var++) {
294  if (cdata.is_unate[var]) {
295  INLINEset_or(ceil, ceil, cube.var_mask[var]);
296  }
297  }
298 
299  /* Save only those cubes that are "full" in all unate variables */
300  for(Tsave = T1 = T+2; (p = *T1++) != 0; ) {
301  if (setp_implies(ceil, set_or(temp, p, T[0]))) {
302  *Tsave++ = p;
303  }
304  }
305  *Tsave++ = NULL;
306  T[1] = (pcube) Tsave;
307 
308  if (debug & TAUT) {
309  printf("UNATE_REDUCTION: %d unate variables, reduced to %d\n",
310  (int)cdata.vars_unate, (int)CUBELISTSIZE(T));
311  }
312  goto start;
313 
314  /* Check for component reduction */
315  } else if (cdata.var_zeros[cdata.best] < CUBELISTSIZE(T) / 2) {
316  if (cubelist_partition(T, &A, &B, debug & TAUT) == 0) {
317  return MAYBE;
318  } else {
319  free_cubelist(T);
320  if (tautology(A)) {
321  free_cubelist(B);
322  return TRUE;
323  } else {
324  return tautology(B);
325  }
326  }
327  }
328 
329  /* We tried as hard as we could, but must recurse from here on */
330  return MAYBE;
331 }
332 
333 /* fcube_is_covered -- determine exactly how a cubelist "covers" a cube */
334 static void
335 fcube_is_covered(T, c, table)
336 pcube *T, c;
337 sm_matrix *table;
338 {
339  ftautology(cofactor(T,c), table);
340 }
341 
342 
343 /* ftautology -- find ways to make a tautology */
344 static void
345 ftautology(T, table)
346 pcube *T; /* T will be disposed of */
347 sm_matrix *table;
348 {
349  register pcube cl, cr;
350  register int best;
351  static int ftaut_level = 0;
352 
353  if (debug & TAUT) {
354  debug_print(T, "FIND_TAUTOLOGY", ftaut_level++);
355  }
356 
357  if (ftaut_special_cases(T, table) == MAYBE) {
358  cl = new_cube();
359  cr = new_cube();
360  best = binate_split_select(T, cl, cr, TAUT);
361 
362  ftautology(scofactor(T, cl, best), table);
363  ftautology(scofactor(T, cr, best), table);
364 
365  free_cubelist(T);
366  free_cube(cl);
367  free_cube(cr);
368  }
369 
370  if (debug & TAUT) {
371  (void) printf("exit FIND_TAUTOLOGY[%d]: table is %d by %d\n",
372  --ftaut_level, table->nrows, table->ncols);
373  }
374 }
375 
376 static bool
378 pcube *T; /* will be disposed if answer is determined */
379 sm_matrix *table;
380 {
381  register pcube *T1, *Tsave, p, temp = cube.temp[0], ceil = cube.temp[1];
382  int var, rownum;
383 
384  /* Check for a row of all 1's in the essential cubes */
385  for(T1 = T+2; (p = *T1++) != 0; ) {
386  if (! TESTP(p, REDUND)) {
387  if (full_row(p, T[0])) {
388  /* subspace is covered by essentials -- no new rows for table */
389  free_cubelist(T);
390  return TRUE;
391  }
392  }
393  }
394 
395  /* Collect column counts, determine unate variables, etc. */
396 start:
397  massive_count(T);
398 
399  /* If function is unate, find the rows of all 1's */
400  if (cdata.vars_unate == cdata.vars_active) {
401  /* find which nonessentials cover this subspace */
402  rownum = table->last_row ? table->last_row->row_num+1 : 0;
403  (void) sm_insert(table, rownum, Rp_current);
404  for(T1 = T+2; (p = *T1++) != 0; ) {
405  if (TESTP(p, REDUND)) {
406  /* See if a redundant cube covers this leaf */
407  if (full_row(p, T[0])) {
408  (void) sm_insert(table, rownum, (int) SIZE(p));
409  }
410  }
411  }
412  free_cubelist(T);
413  return TRUE;
414 
415  /* Perform unate reduction if there are any unate variables */
416  } else if (cdata.vars_unate != 0) {
417  /* Form a cube "ceil" with full variables in the unate variables */
418  (void) set_copy(ceil, cube.emptyset);
419  for(var = 0; var < cube.num_vars; var++) {
420  if (cdata.is_unate[var]) {
421  INLINEset_or(ceil, ceil, cube.var_mask[var]);
422  }
423  }
424 
425  /* Save only those cubes that are "full" in all unate variables */
426  for(Tsave = T1 = T+2; (p = *T1++) != 0; ) {
427  if (setp_implies(ceil, set_or(temp, p, T[0]))) {
428  *Tsave++ = p;
429  }
430  }
431  *Tsave++ = 0;
432  T[1] = (pcube) Tsave;
433 
434  if (debug & TAUT) {
435  printf("UNATE_REDUCTION: %d unate variables, reduced to %d\n",
436  (int)cdata.vars_unate, (int)CUBELISTSIZE(T));
437  }
438  goto start;
439  }
440 
441  /* Not much we can do about it */
442  return MAYBE;
443 }
445 
static ABC_NAMESPACE_IMPL_START void fcube_is_covered()
pset set_or()
int length
Definition: sparse.h:46
static bool ftaut_special_cases()
#define FALSE
Definition: cudd.h:91
#define new_cube()
Definition: espresso.h:262
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define free_cover(r)
Definition: espresso.h:266
#define pcover
Definition: espresso.h:264
pset set_copy()
pcube * cube3list(pcover A, pcover B, pcover C)
Definition: cofactor.c:326
int var(Lit p)
Definition: SolverTypes.h:62
bool taut_special_cases(pcube *T)
Definition: irred.c:250
#define PUTSIZE(set, size)
Definition: espresso.h:113
#define free_cube(r)
Definition: espresso.h:263
#define SET(set, flag)
Definition: espresso.h:122
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define RESET(set, flag)
Definition: espresso.h:123
#define INLINEset_or(r, a, b)
Definition: espresso.h:205
bool setp_equal()
#define NIL(type)
Definition: avl.h:25
bool tautology(pcube *T)
Definition: irred.c:217
#define print_time(t)
Definition: espresso.h:22
pset_family sf_addset()
ABC_NAMESPACE_IMPL_START pcube * cofactor(IN pcube *T, IN register pcube c)
Definition: cofactor.c:44
#define CUBELISTSIZE(T)
Definition: espresso.h:329
bool cube_is_covered(pcube *T, pcube c)
Definition: irred.c:207
int row_num
Definition: sparse.h:45
bool full_row()
unsigned int debug
Definition: globals.c:19
#define print_bool(x)
Definition: espresso.h:258
#define sm_foreach_row_element(prow, p)
Definition: sparse.h:103
#define INLINEset_copy(r, a)
Definition: espresso.h:195
pcube * cube2list(pcover A, pcover B)
Definition: cofactor.c:306
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define IRRED
Definition: espresso.h:356
void sm_free(sm_matrix *A)
Definition: matrix.c:60
ABC_NAMESPACE_IMPL_START int sm_row_dominance(sm_matrix *A)
Definition: dominate.c:17
int cubelist_partition(pcube *T, pcube **A, pcube **B, unsigned int comp_debug)
Definition: cvrm.c:234
sm_matrix * irred_derive_table(pcover D, pcover E, pcover Rp)
Definition: irred.c:155
#define new_cover(i)
Definition: espresso.h:265
int binate_split_select(IN pcube *T, IN register pcube cleft, IN register pcube cright, IN int debug_flag)
Definition: cofactor.c:258
unsigned int * pset
Definition: espresso.h:73
void mark_irredundant(pcover F, pcover D)
Definition: irred.c:40
static int Rp_current
Definition: irred.c:20
#define ptime()
Definition: util_old.h:283
sm_element * sm_insert(sm_matrix *A, int row, int col)
Definition: matrix.c:155
sm_row * sm_minimum_cover(sm_matrix *A, int *weight, int heuristic, int debug_level)
Definition: mincov.c:34
ABC_NAMESPACE_IMPL_START sm_matrix * sm_alloc()
Definition: matrix.c:31
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
#define TAUT
Definition: espresso.h:360
#define TRUE
Definition: cudd.h:88
pcube * scofactor(IN pcube *T, IN pcube c, IN int var)
Definition: cofactor.c:93
#define free_cubelist(T)
Definition: espresso.h:267
void debug_print(pcube *T, char *name, int level)
Definition: cvrout.c:385
#define MAYBE
Definition: espresso.h:257
#define GETSET(family, index)
Definition: espresso.h:161
#define IRRED1
Definition: espresso.h:365
#define REDUND
Definition: espresso.h:130
bool setp_implies()
typedefABC_NAMESPACE_HEADER_START struct sm_element_struct sm_element
Definition: sparse.h:21
#define TESTP(set, flag)
Definition: espresso.h:124
static void ftautology()
#define assert(ex)
Definition: util_old.h:213
static int result
Definition: cuddGenetic.c:125
#define ACTIVE
Definition: espresso.h:129
pcover irredundant(pcover F, pcover D)
Definition: irred.c:27
void sm_row_free(sm_row *prow)
Definition: rows.c:53
void irred_split_cover(pcover F, pcover D, pcover *E, pcover *Rt, pcover *Rp)
Definition: irred.c:92
sm_row * last_row
Definition: sparse.h:80
pset_family sf_inactive()
#define RELESSEN
Definition: espresso.h:132
#define SIZE(set)
Definition: espresso.h:112
#define pcube
Definition: espresso.h:261
void massive_count(IN pcube *T)
Definition: cofactor.c:131