abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cvrm.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 /*
11  module: cvrm.c
12  Purpose: miscellaneous cover manipulation
13  a) verify two covers are equal, check consistency of a cover
14  b) unravel a multiple-valued cover into minterms
15  c) sort covers
16 */
17 
18 #include "espresso.h"
19 
21 
22 
23 
24 static void cb_unravel(c, start, end, startbase, B1)
25 IN register pcube c;
26 IN int start, end;
27 IN pcube startbase;
28 INOUT pcover B1;
29 {
30  pcube base = cube.temp[0], p, last;
31  int expansion, place, skip, var, size, offset;
32  register int i, j, k, n;
33 
34  /* Determine how many cubes it will blow up into, and create a mask
35  for those parts that have only a single coordinate
36  */
37  expansion = 1;
38  (void) set_copy(base, startbase);
39  for(var = start; var <= end; var++) {
40  if ((size = set_dist(c, cube.var_mask[var])) < 2) {
41  (void) set_or(base, base, cube.var_mask[var]);
42  } else {
43  expansion *= size;
44  }
45  }
46  (void) set_and(base, c, base);
47 
48  /* Add the unravelled sets starting at the last element of B1 */
49  offset = B1->count;
50  B1->count += expansion;
51  foreach_remaining_set(B1, last, GETSET(B1, offset-1), p) {
52  INLINEset_copy(p, base);
53  }
54 
55  place = expansion;
56  for(var = start; var <= end; var++) {
57  if ((size = set_dist(c, cube.var_mask[var])) > 1) {
58  skip = place;
59  place = place / size;
60  n = 0;
61  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
62  if (is_in_set(c, i)) {
63  for(j = n; j < expansion; j += skip) {
64  for(k = 0; k < place; k++) {
65  p = GETSET(B1, j+k+offset);
66  (void) set_insert(p, i);
67  }
68  }
69  n += place;
70  }
71  }
72  }
73  }
74 }
75 
76 
77 pcover unravel_range(B, start, end)
78 IN pcover B;
79 IN int start, end;
80 {
81  pcover B1;
82  int var, total_size, expansion, size;
83  register pcube p, last, startbase = cube.temp[1];
84 
85  /* Create the starting base for those variables not being unravelled */
86  (void) set_copy(startbase, cube.emptyset);
87  for(var = 0; var < start; var++)
88  (void) set_or(startbase, startbase, cube.var_mask[var]);
89  for(var = end+1; var < cube.num_vars; var++)
90  (void) set_or(startbase, startbase, cube.var_mask[var]);
91 
92  /* Determine how many cubes it will blow up into */
93  total_size = 0;
94  foreach_set(B, last, p) {
95  expansion = 1;
96  for(var = start; var <= end; var++)
97  if ((size = set_dist(p, cube.var_mask[var])) >= 2)
98  if ((expansion *= size) > 1000000)
99  fatal("unreasonable expansion in unravel");
100  total_size += expansion;
101  }
102 
103  /* We can now allocate a cover of exactly the correct size */
104  B1 = new_cover(total_size);
105  foreach_set(B, last, p) {
106  cb_unravel(p, start, end, startbase, B1);
107  }
108  free_cover(B);
109  return B1;
110 }
111 
112 
113 pcover unravel(B, start)
114 IN pcover B;
115 IN int start;
116 {
117  return unravel_range(B, start, cube.num_vars-1);
118 }
119 
120 /* lex_sort -- sort cubes in a standard lexical fashion */
122 pcover T;
123 {
124  pcover T1 = sf_unlist(sf_sort(T, lex_order), T->count, T->sf_size);
125  free_cover(T);
126  return T1;
127 }
128 
129 
130 /* size_sort -- sort cubes by their size */
132 pcover T;
133 {
134  pcover T1 = sf_unlist(sf_sort(T, descend), T->count, T->sf_size);
135  free_cover(T);
136  return T1;
137 }
138 
139 
140 /* mini_sort -- sort cubes according to the heuristics of mini */
141 pcover mini_sort(F, compare)
142 pcover F;
143 int (*compare)();
144 {
145  register int *count, cnt, n = cube.size, i;
146  register pcube p, last;
147  pcover F_sorted;
148  pcube *F1;
149 
150  /* Perform a column sum over the set family */
151  count = sf_count(F);
152 
153  /* weight is "inner product of the cube and the column sums" */
154  foreach_set(F, last, p) {
155  cnt = 0;
156  for(i = 0; i < n; i++)
157  if (is_in_set(p, i))
158  cnt += count[i];
159  PUTSIZE(p, cnt);
160  }
161  FREE(count);
162 
163  /* use qsort to sort the array */
164  qsort((char *) (F1 = sf_list(F)), F->count, sizeof(pcube), compare);
165  F_sorted = sf_unlist(F1, F->count, F->sf_size);
166  free_cover(F);
167 
168  return F_sorted;
169 }
170 
171 
172 /* sort_reduce -- Espresso strategy for ordering the cubes before reduction */
174 IN pcover T;
175 {
176  register pcube p, last, largest = NULL;
177  register int bestsize = -1, size, n = cube.num_vars;
178  pcover T_sorted;
179  pcube *T1;
180 
181  if (T->count == 0)
182  return T;
183 
184  /* find largest cube */
185  foreach_set(T, last, p)
186  if ((size = set_ord(p)) > bestsize)
187  largest = p, bestsize = size;
188 
189  foreach_set(T, last, p)
190  PUTSIZE(p, ((n - cdist(largest,p)) << 7) + MIN(set_ord(p),127));
191 
192  qsort((char *) (T1 = sf_list(T)), T->count, sizeof(pcube), (int (*)()) descend);
193  T_sorted = sf_unlist(T1, T->count, T->sf_size);
194  free_cover(T);
195 
196  return T_sorted;
197 }
198 
200 register pcover F;
201 {
202  pset temp;
203  register int i, k;
204 #ifdef RANDOM
205  long random();
206 #endif
207 
208  temp = set_new(F->sf_size);
209  for(i = F->count - 1; i > 0; i--) {
210  /* Choose a random number between 0 and i */
211 #ifdef RANDOM
212  k = random() % i;
213 #else
214  /* this is not meant to be really used; just provides an easy
215  "out" if random() and srandom() aren't around
216  */
217  k = (i*23 + 997) % i;
218 #endif
219  /* swap sets i and k */
220  (void) set_copy(temp, GETSET(F, k));
221  (void) set_copy(GETSET(F, k), GETSET(F, i));
222  (void) set_copy(GETSET(F, i), temp);
223  }
224  set_free(temp);
225  return F;
226 }
227 
228 /*
229  * cubelist_partition -- take a cubelist T and see if it has any components;
230  * if so, return cubelist's of the two partitions A and B; the return value
231  * is the size of the partition; if not, A and B
232  * are undefined and the return value is 0
233  */
234 int cubelist_partition(T, A, B, comp_debug)
235 pcube *T; /* a list of cubes */
236 pcube **A, **B; /* cubelist of partition and remainder */
237 unsigned int comp_debug;
238 {
239  register pcube *T1, p, seed, cof;
240  pcube *A1, *B1;
241  bool change;
242  int count, numcube;
243 
244  numcube = CUBELISTSIZE(T);
245 
246  /* Mark all cubes -- covered cubes belong to the partition */
247  for(T1 = T+2; (p = *T1++) != NULL; ) {
248  RESET(p, COVERED);
249  }
250 
251  /*
252  * Extract a partition from the cubelist T; start with the first cube as a
253  * seed, and then pull in all cubes which share a variable with the seed;
254  * iterate until no new cubes are brought into the partition.
255  */
256  seed = set_save(T[2]);
257  cof = T[0];
258  SET(T[2], COVERED);
259  count = 1;
260 
261  do {
262  change = FALSE;
263  for(T1 = T+2; (p = *T1++) != NULL; ) {
264  if (! TESTP(p, COVERED) && ccommon(p, seed, cof)) {
265  INLINEset_and(seed, seed, p);
266  SET(p, COVERED);
267  change = TRUE;
268  count++;
269  }
270 
271  }
272  } while (change);
273 
274  set_free(seed);
275 
276  if (comp_debug) {
277  (void) printf("COMPONENT_REDUCTION: split into %d %d\n",
278  count, numcube - count);
279  }
280 
281  if (count != numcube) {
282  /* Allocate and setup the cubelist's for the two partitions */
283  *A = A1 = ALLOC(pcube, numcube+3);
284  *B = B1 = ALLOC(pcube, numcube+3);
285  (*A)[0] = set_save(T[0]);
286  (*B)[0] = set_save(T[0]);
287  A1 = *A + 2;
288  B1 = *B + 2;
289 
290  /* Loop over the cubes in T and distribute to A and B */
291  for(T1 = T+2; (p = *T1++) != NULL; ) {
292  if (TESTP(p, COVERED)) {
293  *A1++ = p;
294  } else {
295  *B1++ = p;
296  }
297  }
298 
299  /* Stuff needed at the end of the cubelist's */
300  *A1++ = NULL;
301  (*A)[1] = (pcube) A1;
302  *B1++ = NULL;
303  (*B)[1] = (pcube) B1;
304  }
305 
306  return numcube - count;
307 }
308 
309 /*
310  * quick cofactor against a single output function
311  */
313 pcover T;
314 register int i;
315 {
316  pcover T1;
317  register pcube p, last, pdest, mask;
318 
319  mask = cube.var_mask[cube.output];
320  T1 = new_cover(T->count);
321  foreach_set(T, last, p) {
322  if (is_in_set(p, i)) {
323  pdest = GETSET(T1, T1->count++);
324  INLINEset_or(pdest, p, mask);
325  RESET(pdest, PRIME);
326  }
327  }
328  return T1;
329 }
330 
331 
332 /*
333  * quick intersection against a single output function
334  */
336 pcover T;
337 int i;
338 {
339  register pcube p, last, mask;
340 
341  if (T == NULL) {
342  return T;
343  }
344 
345  mask = cube.var_mask[cube.output];
346  foreach_set(T, last, p) {
347  INLINEset_diff(p, p, mask);
348  set_insert(p, i);
349  }
350  return T;
351 }
352 
353 
354 /*
355  * A generic routine to perform an operation for each output function
356  *
357  * func() is called with a PLA for each output function (with the output
358  * part effectively removed).
359  * func1() is called after reforming the equivalent output function
360  *
361  * Each function returns TRUE if process is to continue
362  */
363 void foreach_output_function(PLA, func, func1)
364 pPLA PLA;
365 int (*func)();
366 int (*func1)();
367 {
368  pPLA PLA1;
369  int i;
370 
371  /* Loop for each output function */
372  for(i = 0; i < cube.part_size[cube.output]; i++) {
373 
374  /* cofactor on the output part */
375  PLA1 = new_PLA();
376  PLA1->F = cof_output(PLA->F, i + cube.first_part[cube.output]);
377  PLA1->R = cof_output(PLA->R, i + cube.first_part[cube.output]);
378  PLA1->D = cof_output(PLA->D, i + cube.first_part[cube.output]);
379 
380  /* Call a routine to do something with the cover */
381  if ((*func)(PLA1, i) == 0) {
382  free_PLA(PLA1);
383  return;
384  }
385 
386  /* intersect with the particular output part again */
387  PLA1->F = uncof_output(PLA1->F, i + cube.first_part[cube.output]);
388  PLA1->R = uncof_output(PLA1->R, i + cube.first_part[cube.output]);
389  PLA1->D = uncof_output(PLA1->D, i + cube.first_part[cube.output]);
390 
391  /* Call a routine to do something with the final result */
392  if ((*func1)(PLA1, i) == 0) {
393  free_PLA(PLA1);
394  return;
395  }
396 
397  /* Cleanup for next go-around */
398  free_PLA(PLA1);
399 
400 
401  }
402 }
403 
404 static pcover Fmin;
405 static pcube phase;
406 
407 /*
408  * minimize each output function individually
409  */
410 void so_espresso(PLA, strategy)
411 pPLA PLA;
412 int strategy;
413 {
414  Fmin = new_cover(PLA->F->count);
415  if (strategy == 0) {
417  } else {
419  }
420  sf_free(PLA->F);
421  PLA->F = Fmin;
422 }
423 
424 
425 /*
426  * minimize each output function, choose function or complement based on the
427  * one with the fewer number of terms
428  */
429 void so_both_espresso(PLA, strategy)
430 pPLA PLA;
431 int strategy;
432 {
433  phase = set_save(cube.fullset);
434  Fmin = new_cover(PLA->F->count);
435  if (strategy == 0) {
437  } else {
439  }
440  sf_free(PLA->F);
441  PLA->F = Fmin;
442  PLA->phase = phase;
443 }
444 
445 
446 int so_do_espresso(PLA, i)
447 pPLA PLA;
448 int i;
449 {
450  char word[32];
451 
452  /* minimize the single-output function (on-set) */
453  skip_make_sparse = 1;
454  (void) sprintf(word, "ESPRESSO-POS(%d)", i);
455  EXEC_S(PLA->F = espresso(PLA->F, PLA->D, PLA->R), word, PLA->F);
456  return 1;
457 }
458 
459 
460 int so_do_exact(PLA, i)
461 pPLA PLA;
462 int i;
463 {
464  char word[32];
465 
466  /* minimize the single-output function (on-set) */
467  skip_make_sparse = 1;
468  (void) sprintf(word, "EXACT-POS(%d)", i);
469  EXEC_S(PLA->F = minimize_exact(PLA->F, PLA->D, PLA->R, 1), word, PLA->F);
470  return 1;
471 }
472 
473 
474 /*ARGSUSED*/
475 int so_save(PLA, i)
476 pPLA PLA;
477 int i;
478 {
479  Fmin = sf_append(Fmin, PLA->F); /* disposes of PLA->F */
480  PLA->F = NULL;
481  return 1;
482 }
483 
484 
486 pPLA PLA;
487 int i;
488 {
489  char word[32];
490 
491  /* minimize the single-output function (on-set) */
492  (void) sprintf(word, "ESPRESSO-POS(%d)", i);
493  skip_make_sparse = 1;
494  EXEC_S(PLA->F = espresso(PLA->F, PLA->D, PLA->R), word, PLA->F);
495 
496  /* minimize the single-output function (off-set) */
497  (void) sprintf(word, "ESPRESSO-NEG(%d)", i);
498  skip_make_sparse = 1;
499  EXEC_S(PLA->R = espresso(PLA->R, PLA->D, PLA->F), word, PLA->R);
500 
501  return 1;
502 }
503 
504 
505 int so_both_do_exact(PLA, i)
506 pPLA PLA;
507 int i;
508 {
509  char word[32];
510 
511  /* minimize the single-output function (on-set) */
512  (void) sprintf(word, "EXACT-POS(%d)", i);
513  skip_make_sparse = 1;
514  EXEC_S(PLA->F = minimize_exact(PLA->F, PLA->D, PLA->R, 1), word, PLA->F);
515 
516  /* minimize the single-output function (off-set) */
517  (void) sprintf(word, "EXACT-NEG(%d)", i);
518  skip_make_sparse = 1;
519  EXEC_S(PLA->R = minimize_exact(PLA->R, PLA->D, PLA->F, 1), word, PLA->R);
520 
521  return 1;
522 }
523 
524 
525 int so_both_save(PLA, i)
526 pPLA PLA;
527 int i;
528 {
529  if (PLA->F->count > PLA->R->count) {
530  sf_free(PLA->F);
531  PLA->F = PLA->R;
532  PLA->R = NULL;
533  i += cube.first_part[cube.output];
534  set_remove(phase, i);
535  } else {
536  sf_free(PLA->R);
537  PLA->R = NULL;
538  }
539  Fmin = sf_append(Fmin, PLA->F);
540  PLA->F = NULL;
541  return 1;
542 }
544 
pset set_or()
#define INLINEset_diff(r, a, b)
Definition: espresso.h:208
void fatal(char *s)
Definition: cvrmisc.c:140
#define set_free(r)
Definition: espresso.h:167
#define FALSE
Definition: cudd.h:91
ABC_NAMESPACE_IMPL_START pcover espresso(pcover F, pcover D1, pcover R)
Definition: espresso.c:53
int * sf_count()
void so_espresso(pPLA PLA, int strategy)
Definition: cvrm.c:410
int set_dist()
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()
pcover unravel(IN pcover B, IN int start)
Definition: cvrm.c:113
#define MIN(a, b)
Definition: util_old.h:256
#define set_save(r)
Definition: espresso.h:166
void so_both_espresso(pPLA PLA, int strategy)
Definition: cvrm.c:429
int var(Lit p)
Definition: SolverTypes.h:62
pcover size_sort(pcover T)
Definition: cvrm.c:131
#define INLINEset_and(r, a, b)
Definition: espresso.h:202
pcover sort_reduce(IN pcover T)
Definition: cvrm.c:173
#define PUTSIZE(set, size)
Definition: espresso.h:113
int so_do_espresso(pPLA PLA, int i)
Definition: cvrm.c:446
pset set_and()
int lex_order()
#define foreach_remaining_set(R, last, pfirst, p)
Definition: espresso.h:137
void sf_free()
#define PRIME
Definition: espresso.h:127
pcover mini_sort(pcover F, int(*compare)())
Definition: cvrm.c:141
int so_both_do_exact(pPLA PLA, int i)
Definition: cvrm.c:505
#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 INOUT
Definition: espresso.h:334
#define IN
Definition: espresso.h:332
int so_save(pPLA PLA, int i)
Definition: cvrm.c:475
pcover random_order(pcover F)
Definition: cvrm.c:199
#define INLINEset_or(r, a, b)
Definition: espresso.h:205
pcover unravel_range(IN pcover B, IN int start, IN int end)
Definition: cvrm.c:77
pcover lex_sort(pcover T)
Definition: cvrm.c:121
pcover uncof_output(pcover T, int i)
Definition: cvrm.c:335
int cdist()
void foreach_output_function(pPLA PLA, int(*func)(), int(*func1)())
Definition: cvrm.c:363
#define CUBELISTSIZE(T)
Definition: espresso.h:329
#define ALLOC(type, num)
Definition: avl.h:27
#define COVERED
Definition: espresso.h:131
static ABC_NAMESPACE_IMPL_START void cb_unravel(IN register pcube c, IN int start, IN int end, IN pcube startbase, INOUT pcover B1)
Definition: cvrm.c:24
#define INLINEset_copy(r, a)
Definition: espresso.h:195
int so_both_save(pPLA PLA, int i)
Definition: cvrm.c:525
pcover cof_output(pcover T, int i)
Definition: cvrm.c:312
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
#define EXEC_S(fct, name, S)
Definition: espresso.h:420
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define FREE(obj)
Definition: avl.h:31
#define is_in_set(set, e)
Definition: espresso.h:170
long random()
int cubelist_partition(pcube *T, pcube **A, pcube **B, unsigned int comp_debug)
Definition: cvrm.c:234
static int size
Definition: cuddSign.c:86
#define new_cover(i)
Definition: espresso.h:265
unsigned int * pset
Definition: espresso.h:73
int so_do_exact(pPLA PLA, int i)
Definition: cvrm.c:460
char * sprintf()
pcover F
Definition: espresso.h:316
static int descend(struct saucy *s, struct coloring *c, int target, int min)
Definition: abcSaucy.c:1625
bool skip_make_sparse
Definition: globals.c:28
static int largest(void)
Definition: cuddGenetic.c:624
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
#define set_new(size)
Definition: espresso.h:164
#define set_remove(set, e)
Definition: espresso.h:171
#define TRUE
Definition: cudd.h:88
pset * sf_list(IN register pset_family A)
Definition: contain.c:351
pset_family sf_unlist(IN pset *A1, IN int totcnt, IN int size)
Definition: contain.c:366
static pcube phase
Definition: cvrm.c:405
#define set_insert(set, e)
Definition: espresso.h:172
#define GETSET(family, index)
Definition: espresso.h:161
pcover D
Definition: espresso.h:316
pcover R
Definition: espresso.h:316
void free_PLA(pPLA PLA)
Definition: cvrin.c:676
pPLA new_PLA()
Definition: cvrin.c:648
#define TESTP(set, flag)
Definition: espresso.h:124
pset_family sf_append()
pcover minimize_exact()
bool ccommon()
int so_both_do_espresso(pPLA PLA, int i)
Definition: cvrm.c:485
static pcover Fmin
Definition: cvrm.c:404
#define pcube
Definition: espresso.h:261
pset * sf_sort(IN pset_family A, IN int(*compare)())
Definition: contain.c:330
int set_ord()