abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
unate.c File Reference
#include "espresso.h"

Go to the source code of this file.

Macros

#define MAGIC   500 /* save 500 cubes before containment */
 

Functions

static
ABC_NAMESPACE_IMPL_START
pset_family 
abs_covered ()
 
static pset_family abs_covered_many ()
 
static int abs_select_restricted ()
 
pcover map_cover_to_unate (pcube *T)
 
pcover map_unate_to_cover (pset_family A)
 
pset_family unate_compl (pset_family A)
 
pset_family unate_complement (pset_family A)
 
pset_family exact_minimum_cover (IN pset_family T)
 
pset_family unate_intersect (pset_family A, pset_family B, bool largest_only)
 
static pset_family abs_covered (pset_family A, int pick)
 
static pset_family abs_covered_many (pset_family A, pset pick_set)
 
static int abs_select_restricted (pset_family A, pset restrict)
 

Macro Definition Documentation

#define MAGIC   500 /* save 500 cubes before containment */

Definition at line 303 of file unate.c.

Function Documentation

static ABC_NAMESPACE_IMPL_START pset_family abs_covered ( )
static
static pset_family abs_covered ( pset_family  A,
int  pick 
)
static

Definition at line 371 of file unate.c.

374 {
375  register pset last, p, pdest;
376  register pset_family Aprime;
377 
378  Aprime = sf_new(A->count, A->sf_size);
379  pdest = Aprime->data;
380  foreach_set(A, last, p)
381  if (! is_in_set(p, pick)) {
382  INLINEset_copy(pdest, p);
383  Aprime->count++;
384  pdest += Aprime->wsize;
385  }
386  return Aprime;
387 }
pset_family sf_new()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int count
Definition: espresso.h:80
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define INLINEset_copy(r, a)
Definition: espresso.h:195
int sf_size
Definition: espresso.h:78
if(last==0)
Definition: sparse_int.h:34
#define is_in_set(set, e)
Definition: espresso.h:170
unsigned int * pset
Definition: espresso.h:73
pset data
Definition: espresso.h:82
int wsize
Definition: espresso.h:77
static pset_family abs_covered_many ( )
static
static pset_family abs_covered_many ( pset_family  A,
pset  pick_set 
)
static

Definition at line 395 of file unate.c.

398 {
399  register pset last, p, pdest;
400  register pset_family Aprime;
401 
402  Aprime = sf_new(A->count, A->sf_size);
403  pdest = Aprime->data;
404  foreach_set(A, last, p)
405  if (setp_disjoint(p, pick_set)) {
406  INLINEset_copy(pdest, p);
407  Aprime->count++;
408  pdest += Aprime->wsize;
409  }
410  return Aprime;
411 }
pset_family sf_new()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int count
Definition: espresso.h:80
bool setp_disjoint()
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define INLINEset_copy(r, a)
Definition: espresso.h:195
int sf_size
Definition: espresso.h:78
if(last==0)
Definition: sparse_int.h:34
unsigned int * pset
Definition: espresso.h:73
pset data
Definition: espresso.h:82
int wsize
Definition: espresso.h:77
static int abs_select_restricted ( )
static
static int abs_select_restricted ( pset_family  A,
pset  restrict 
)
static

Definition at line 420 of file unate.c.

423 {
424  register int i, best_var, best_count, *count;
425 
426  /* Sum the elements in these columns */
427  count = sf_count_restricted(A, restrict);
428 
429  /* Find which variable has maximum weight */
430  best_var = -1;
431  best_count = 0;
432  for(i = 0; i < A->sf_size; i++) {
433  if (count[i] > best_count) {
434  best_var = i;
435  best_count = count[i];
436  }
437  }
438  FREE(count);
439 
440  if (best_var == -1)
441  fatal("abs_select_restricted: should not have best_var == -1");
442 
443  return best_var;
444 }
void fatal(char *s)
Definition: cvrmisc.c:140
int sf_size
Definition: espresso.h:78
#define FREE(obj)
Definition: avl.h:31
int * sf_count_restricted()
pset_family exact_minimum_cover ( IN pset_family  T)

Definition at line 226 of file unate.c.

228 {
229  register pset p, last, p1;
230  register int i, n;
231  int lev, lvl;
232  pset nlast;
233  pset_family temp;
234  long start = ptime();
235  struct {
236  pset_family sf;
237  int level;
238  } stack[32]; /* 32 suffices for 2 ** 32 cubes ! */
239 
240  if (T->count <= 0)
241  return sf_new(1, T->sf_size);
242  for(n = T->count, lev = 0; n != 0; n >>= 1, lev++) ;
243 
244  /* A simple heuristic ordering */
245  T = lex_sort(sf_save(T));
246 
247  /* Push a full set on the stack to get things started */
248  n = 1;
249  stack[0].sf = sf_new(1, T->sf_size);
250  stack[0].level = lev;
251  set_fill(GETSET(stack[0].sf, stack[0].sf->count++), T->sf_size);
252 
253  nlast = GETSET(T, T->count - 1);
254  foreach_set(T, last, p) {
255 
256  /* "unstack" the set into a family */
257  temp = sf_new(set_ord(p), T->sf_size);
258  for(i = 0; i < T->sf_size; i++)
259  if (is_in_set(p, i)) {
260  p1 = set_fill(GETSET(temp, temp->count++), T->sf_size);
261  set_remove(p1, i);
262  }
263  stack[n].sf = temp;
264  stack[n++].level = lev;
265 
266  /* Pop the stack and perform (leveled) intersections */
267  while (n > 1 && (stack[n-1].level==stack[n-2].level || p == nlast)) {
268  temp = unate_intersect(stack[n-1].sf, stack[n-2].sf, FALSE);
269  lvl = MIN(stack[n-1].level, stack[n-2].level) - 1;
270  if (debug & MINCOV && lvl < 10) {
271  printf("# EXACT_MINCOV[%d]: %4d = %4d x %4d, time = %s\n",
272  lvl, temp->count, stack[n-1].sf->count,
273  stack[n-2].sf->count, print_time(ptime() - start));
274  (void) fflush(stdout);
275  }
276  sf_free(stack[n-2].sf);
277  sf_free(stack[n-1].sf);
278  stack[n-2].sf = temp;
279  stack[n-2].level = lvl;
280  n--;
281  }
282  }
283 
284  temp = stack[0].sf;
285  p1 = set_fill(set_new(T->sf_size), T->sf_size);
286  foreach_set(temp, last, p)
287  INLINEset_diff(p, p1, p);
288  set_free(p1);
289  if (debug & MINCOV1) {
290  printf("MINCOV: family of all minimal coverings is\n");
291  sf_print(temp);
292  }
293  sf_free(T); /* this is the copy of T we made ... */
294  return temp;
295 }
#define INLINEset_diff(r, a, b)
Definition: espresso.h:208
pset_family sf_new()
#define set_free(r)
Definition: espresso.h:167
#define FALSE
Definition: cudd.h:91
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define MIN(a, b)
Definition: util_old.h:256
int count
Definition: espresso.h:80
void sf_free()
#define foreach_set(R, last, p)
Definition: espresso.h:135
pcover lex_sort(pcover T)
Definition: cvrm.c:121
#define print_time(t)
Definition: espresso.h:22
unsigned int debug
Definition: globals.c:19
if(last==0)
Definition: sparse_int.h:34
#define is_in_set(set, e)
Definition: espresso.h:170
unsigned int * pset
Definition: espresso.h:73
void sf_print()
#define MINCOV1
Definition: espresso.h:363
#define ptime()
Definition: util_old.h:283
#define set_new(size)
Definition: espresso.h:164
pset set_fill()
pset_family unate_intersect(pset_family A, pset_family B, bool largest_only)
Definition: unate.c:305
#define set_remove(set, e)
Definition: espresso.h:171
#define MINCOV
Definition: espresso.h:362
#define GETSET(family, index)
Definition: espresso.h:161
pset_family sf_save()
int set_ord()
pcover map_cover_to_unate ( pcube T)

Definition at line 23 of file unate.c.

25 {
26  register unsigned int word_test, word_set, bit_test, bit_set;
27  register pcube p, pA;
28  pset_family A;
29  pcube *T1;
30  int ncol, i;
31 
32  A = sf_new(CUBELISTSIZE(T), cdata.vars_unate);
33  A->count = CUBELISTSIZE(T);
34  foreachi_set(A, i, p) {
35  (void) set_clear(p, A->sf_size);
36  }
37  ncol = 0;
38 
39  for(i = 0; i < cube.size; i++) {
40  if (cdata.part_zeros[i] > 0) {
41  assert(ncol <= cdata.vars_unate);
42 
43  /* Copy a column from T to A */
44  word_test = WHICH_WORD(i);
45  bit_test = 1 << WHICH_BIT(i);
46  word_set = WHICH_WORD(ncol);
47  bit_set = 1 << WHICH_BIT(ncol);
48 
49  pA = A->data;
50  for(T1 = T+2; (p = *T1++) != 0; ) {
51  if ((p[word_test] & bit_test) == 0) {
52  pA[word_set] |= bit_set;
53  }
54  pA += A->wsize;
55  }
56 
57  ncol++;
58  }
59  }
60 
61  return A;
62 }
pset_family sf_new()
pset set_clear()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int count
Definition: espresso.h:80
#define CUBELISTSIZE(T)
Definition: espresso.h:329
int sf_size
Definition: espresso.h:78
#define WHICH_BIT(element)
Definition: espresso.h:88
#define WHICH_WORD(element)
Definition: espresso.h:87
#define assert(ex)
Definition: util_old.h:213
pset data
Definition: espresso.h:82
int wsize
Definition: espresso.h:77
#define pcube
Definition: espresso.h:261
#define foreachi_set(R, i, p)
Definition: espresso.h:143
pcover map_unate_to_cover ( pset_family  A)

Definition at line 64 of file unate.c.

66 {
67  register int i, ncol, lp;
68  register pcube p, pB;
69  int var, nunate, *unate;
70  pcube last;
71  pset_family B;
72 
73  B = sf_new(A->count, cube.size);
74  B->count = A->count;
75 
76  /* Find the unate variables */
77  unate = ALLOC(int, cube.num_vars);
78  nunate = 0;
79  for(var = 0; var < cube.num_vars; var++) {
80  if (cdata.is_unate[var]) {
81  unate[nunate++] = var;
82  }
83  }
84 
85  /* Loop for each set of A */
86  pB = B->data;
87  foreach_set(A, last, p) {
88 
89  /* Initialize this set of B */
90  INLINEset_fill(pB, cube.size);
91 
92  /* Now loop for the unate variables; if the part is in A,
93  * then this variable of B should be a single 1 in the unate
94  * part.
95  */
96  for(ncol = 0; ncol < nunate; ncol++) {
97  if (is_in_set(p, ncol)) {
98  lp = cube.last_part[unate[ncol]];
99  for(i = cube.first_part[unate[ncol]]; i <= lp; i++) {
100  if (cdata.part_zeros[i] == 0) {
101  set_remove(pB, i);
102  }
103  }
104  }
105  }
106  pB += B->wsize;
107  }
108 
109  FREE(unate);
110  return B;
111 }
pset_family sf_new()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int var(Lit p)
Definition: SolverTypes.h:62
int count
Definition: espresso.h:80
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define ALLOC(type, num)
Definition: avl.h:27
#define FREE(obj)
Definition: avl.h:31
#define is_in_set(set, e)
Definition: espresso.h:170
#define set_remove(set, e)
Definition: espresso.h:171
pset data
Definition: espresso.h:82
int wsize
Definition: espresso.h:77
#define pcube
Definition: espresso.h:261
#define INLINEset_fill(r, size)
Definition: espresso.h:199
pset_family unate_compl ( pset_family  A)

Definition at line 117 of file unate.c.

119 {
120  register pset p, last;
121 
122  /* Make sure A is single-cube containment minimal */
123 /* A = sf_rev_contain(A);*/
124 
125  foreach_set(A, last, p) {
126  PUTSIZE(p, set_ord(p));
127  }
128 
129  /* Recursively find the complement */
130  A = unate_complement(A);
131 
132  /* Now, we can guarantee a minimal result by containing the result */
133  A = sf_rev_contain(A);
134  return A;
135 }
pset_family sf_rev_contain(INOUT pset_family A)
Definition: contain.c:58
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define PUTSIZE(set, size)
Definition: espresso.h:113
pset_family unate_complement(pset_family A)
Definition: unate.c:141
#define foreach_set(R, last, p)
Definition: espresso.h:135
unsigned int * pset
Definition: espresso.h:73
int set_ord()
pset_family unate_complement ( pset_family  A)

Definition at line 141 of file unate.c.

143 {
144  pset_family Abar;
145  register pset p, p1, restrict;
146  register int i;
147  int max_i, min_set_ord, j;
148 
149  /* Check for no sets in the matrix -- complement is the universe */
150  if (A->count == 0) {
151  sf_free(A);
152  Abar = sf_new(1, A->sf_size);
153  (void) set_clear(GETSET(Abar, Abar->count++), A->sf_size);
154 
155  /* Check for a single set in the maxtrix -- compute de Morgan complement */
156  } else if (A->count == 1) {
157  p = A->data;
158  Abar = sf_new(A->sf_size, A->sf_size);
159  for(i = 0; i < A->sf_size; i++) {
160  if (is_in_set(p, i)) {
161  p1 = set_clear(GETSET(Abar, Abar->count++), A->sf_size);
162  set_insert(p1, i);
163  }
164  }
165  sf_free(A);
166 
167  } else {
168 
169  /* Select splitting variable as the variable which belongs to a set
170  * of the smallest size, and which has greatest column count
171  */
172  restrict = set_new(A->sf_size);
173  min_set_ord = A->sf_size + 1;
174  foreachi_set(A, i, p) {
175  if (SIZE(p) < min_set_ord) {
176  set_copy(restrict, p);
177  min_set_ord = SIZE(p);
178  } else if (SIZE(p) == min_set_ord) {
179  set_or(restrict, restrict, p);
180  }
181  }
182 
183  /* Check for no data (shouldn't happen ?) */
184  if (min_set_ord == 0) {
185  A->count = 0;
186  Abar = A;
187 
188  /* Check for "essential" columns */
189  } else if (min_set_ord == 1) {
190  Abar = unate_complement(abs_covered_many(A, restrict));
191  sf_free(A);
192  foreachi_set(Abar, i, p) {
193  set_or(p, p, restrict);
194  }
195 
196  /* else, recur as usual */
197  } else {
198  max_i = abs_select_restricted(A, restrict);
199 
200  /* Select those rows of A which are not covered by max_i,
201  * recursively find all minimal covers of these rows, and
202  * then add back in max_i
203  */
204  Abar = unate_complement(abs_covered(A, max_i));
205  foreachi_set(Abar, i, p) {
206  set_insert(p, max_i);
207  }
208 
209  /* Now recur on A with all zero's on column max_i */
210  foreachi_set(A, i, p) {
211  if (is_in_set(p, max_i)) {
212  set_remove(p, max_i);
213  j = SIZE(p) - 1;
214  PUTSIZE(p, j);
215  }
216  }
217 
218  Abar = sf_append(Abar, unate_complement(A));
219  }
220  set_free(restrict);
221  }
222 
223  return Abar;
224 }
pset set_or()
pset_family sf_new()
#define set_free(r)
Definition: espresso.h:167
pset set_clear()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
pset set_copy()
#define PUTSIZE(set, size)
Definition: espresso.h:113
int count
Definition: espresso.h:80
void sf_free()
static pset_family abs_covered_many()
pset_family unate_complement(pset_family A)
Definition: unate.c:141
static int abs_select_restricted()
int sf_size
Definition: espresso.h:78
#define is_in_set(set, e)
Definition: espresso.h:170
unsigned int * pset
Definition: espresso.h:73
#define set_new(size)
Definition: espresso.h:164
#define set_remove(set, e)
Definition: espresso.h:171
static ABC_NAMESPACE_IMPL_START pset_family abs_covered()
#define set_insert(set, e)
Definition: espresso.h:172
#define GETSET(family, index)
Definition: espresso.h:161
pset_family sf_append()
pset data
Definition: espresso.h:82
#define SIZE(set)
Definition: espresso.h:112
#define foreachi_set(R, i, p)
Definition: espresso.h:143
pset_family unate_intersect ( pset_family  A,
pset_family  B,
bool  largest_only 
)

Definition at line 305 of file unate.c.

308 {
309  register pset pi, pj, lasti, lastj, pt;
310  pset_family T, Tsave;
311  bool save;
312  int maxord, ord;
313 
314  /* How large should each temporary result cover be ? */
315  T = sf_new(MAGIC, A->sf_size);
316  Tsave = NULL;
317  maxord = 0;
318  pt = T->data;
319 
320  /* Form pairwise intersection of each set of A with each cube of B */
321  foreach_set(A, lasti, pi) {
322 
323  foreach_set(B, lastj, pj) {
324 
325  save = set_andp(pt, pi, pj);
326 
327  /* Check if we want the largest only */
328  if (save && largest_only) {
329  if ((ord = set_ord(pt)) > maxord) {
330  /* discard Tsave and T */
331  if (Tsave != NULL) {
332  sf_free(Tsave);
333  Tsave = NULL;
334  }
335  pt = T->data;
336  T->count = 0;
337  /* Re-create pt (which was just thrown away) */
338  (void) set_and(pt, pi, pj);
339  maxord = ord;
340  } else if (ord < maxord) {
341  save = FALSE;
342  }
343  }
344 
345  if (save) {
346  if (++T->count >= T->capacity) {
347  T = sf_contain(T);
348  Tsave = (Tsave == NULL) ? T : sf_union(Tsave, T);
349  T = sf_new(MAGIC, A->sf_size);
350  pt = T->data;
351  } else {
352  pt += T->wsize;
353  }
354  }
355  }
356  }
357 
358 
359  /* Contain the final result and merge it into Tsave */
360  T = sf_contain(T);
361  Tsave = (Tsave == NULL) ? T : sf_union(Tsave, T);
362 
363  return Tsave;
364 }
pset_family sf_new()
#define FALSE
Definition: cudd.h:91
pset set_and()
int count
Definition: espresso.h:80
void sf_free()
#define foreach_set(R, last, p)
Definition: espresso.h:135
ABC_NAMESPACE_IMPL_START pset_family sf_contain(INOUT pset_family A)
Definition: contain.c:37
bool set_andp()
int sf_size
Definition: espresso.h:78
unsigned int * pset
Definition: espresso.h:73
pset_family sf_union(INOUT pset_family A, INOUT pset_family B)
Definition: contain.c:121
pset data
Definition: espresso.h:82
#define MAGIC
Definition: unate.c:303
int capacity
Definition: espresso.h:79
int wsize
Definition: espresso.h:77
int set_ord()