abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cofactor.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 /*
16  The cofactor of a cover against a cube "c" is a cover formed by the
17  cofactor of each cube in the cover against c. The cofactor of two
18  cubes is null if they are distance 1 or more apart. If they are
19  distance zero apart, the cofactor is the restriction of the cube
20  to the minterms of c.
21 
22  The cube list contains the following information:
23 
24  T[0] = pointer to a cube identifying the variables that have
25  been cofactored against
26  T[1] = pointer to just beyond the sentinel (i.e., T[n] in this case)
27  T[2]
28  .
29  . = pointers to cubes
30  .
31  T[n-2]
32  T[n-1] = NULL pointer (sentinel)
33 
34 
35  Cofactoring involves repeated application of "cdist0" to check if a
36  cube of the cover intersects the cofactored cube. This can be
37  slow, especially for the recursive descent of the espresso
38  routines. Therefore, a special cofactor routine "scofactor" is
39  provided which assumes the cofactor is only in a single variable.
40 */
41 
42 
43 /* cofactor -- compute the cofactor of a cover with respect to a cube */
45 IN pcube *T;
46 IN register pcube c;
47 {
48  pcube temp = cube.temp[0], *Tc_save, *Tc, *T1;
49  register pcube p;
50  int listlen;
51 
52  listlen = CUBELISTSIZE(T) + 5;
53 
54  /* Allocate a new list of cube pointers (max size is previous size) */
55  Tc_save = Tc = ALLOC(pcube, listlen);
56 
57  /* pass on which variables have been cofactored against */
58  *Tc++ = set_or(new_cube(), T[0], set_diff(temp, cube.fullset, c));
59  Tc++;
60 
61  /* Loop for each cube in the list, determine suitability, and save */
62  for(T1 = T+2; (p = *T1++) != NULL; ) {
63  if (p != c) {
64 
65 #ifdef NO_INLINE
66  if (! cdist0(p, c)) goto false;
67 #else
68  {register int w,last;register unsigned int x;if((last=cube.inword)!=-1)
69  {x=p[last]&c[last];if(~(x|x>>1)&cube.inmask)goto false;for(w=1;w<last;w++)
70  {x=p[w]&c[w];if(~(x|x>>1)&DISJOINT)goto false;}}}{register int w,var,last;
71  register pcube mask;for(var=cube.num_binary_vars;var<cube.num_vars;var++){
72  mask=cube.var_mask[var];last=cube.last_word[var];for(w=cube.first_word[var
73  ];w<=last;w++)if(p[w]&c[w]&mask[w])goto nextvar;goto false;nextvar:;}}
74 #endif
75 
76  *Tc++ = p;
77  false: ;
78  }
79  }
80 
81  *Tc++ = (pcube) NULL; /* sentinel */
82  Tc_save[1] = (pcube) Tc; /* save pointer to last */
83  return Tc_save;
84 }
85 
86 /*
87  scofactor -- compute the cofactor of a cover with respect to a cube,
88  where the cube is "active" in only a single variable.
89 
90  This routine has been optimized for speed.
91 */
92 
94 IN pcube *T, c;
95 IN int var;
96 {
97  pcube *Tc, *Tc_save;
98  register pcube p, mask = cube.temp[1], *T1;
99  register int first = cube.first_word[var], last = cube.last_word[var];
100  int listlen;
101 
102  listlen = CUBELISTSIZE(T) + 5;
103 
104  /* Allocate a new list of cube pointers (max size is previous size) */
105  Tc_save = Tc = ALLOC(pcube, listlen);
106 
107  /* pass on which variables have been cofactored against */
108  *Tc++ = set_or(new_cube(), T[0], set_diff(mask, cube.fullset, c));
109  Tc++;
110 
111  /* Setup for the quick distance check */
112  (void) set_and(mask, cube.var_mask[var], c);
113 
114  /* Loop for each cube in the list, determine suitability, and save */
115  for(T1 = T+2; (p = *T1++) != NULL; )
116  if (p != c) {
117  register int i = first;
118  do
119  if (p[i] & mask[i]) {
120  *Tc++ = p;
121  break;
122  }
123  while (++i <= last);
124  }
125 
126  *Tc++ = (pcube) NULL; /* sentinel */
127  Tc_save[1] = (pcube) Tc; /* save pointer to last */
128  return Tc_save;
129 }
130 
132 IN pcube *T;
133 {
134  int *count = cdata.part_zeros;
135  pcube *T1;
136 
137  /* Clear the column counts (count of # zeros in each column) */
138  { register int i;
139  for(i = cube.size - 1; i >= 0; i--)
140  count[i] = 0;
141  }
142 
143  /* Count the number of zeros in each column */
144  { register int i, *cnt;
145  register unsigned int val;
146  register pcube p, cof = T[0], full = cube.fullset;
147  for(T1 = T+2; (p = *T1++) != NULL; )
148  for(i = LOOP(p); i > 0; i--)
149  if ((val = full[i] & ~ (p[i] | cof[i]))) {
150  cnt = count + ((i-1) << LOGBPI);
151 #if BPI == 32
152  if (val & 0xFF000000) {
153  if (val & 0x80000000) cnt[31]++;
154  if (val & 0x40000000) cnt[30]++;
155  if (val & 0x20000000) cnt[29]++;
156  if (val & 0x10000000) cnt[28]++;
157  if (val & 0x08000000) cnt[27]++;
158  if (val & 0x04000000) cnt[26]++;
159  if (val & 0x02000000) cnt[25]++;
160  if (val & 0x01000000) cnt[24]++;
161  }
162  if (val & 0x00FF0000) {
163  if (val & 0x00800000) cnt[23]++;
164  if (val & 0x00400000) cnt[22]++;
165  if (val & 0x00200000) cnt[21]++;
166  if (val & 0x00100000) cnt[20]++;
167  if (val & 0x00080000) cnt[19]++;
168  if (val & 0x00040000) cnt[18]++;
169  if (val & 0x00020000) cnt[17]++;
170  if (val & 0x00010000) cnt[16]++;
171  }
172 #endif
173  if (val & 0xFF00) {
174  if (val & 0x8000) cnt[15]++;
175  if (val & 0x4000) cnt[14]++;
176  if (val & 0x2000) cnt[13]++;
177  if (val & 0x1000) cnt[12]++;
178  if (val & 0x0800) cnt[11]++;
179  if (val & 0x0400) cnt[10]++;
180  if (val & 0x0200) cnt[ 9]++;
181  if (val & 0x0100) cnt[ 8]++;
182  }
183  if (val & 0x00FF) {
184  if (val & 0x0080) cnt[ 7]++;
185  if (val & 0x0040) cnt[ 6]++;
186  if (val & 0x0020) cnt[ 5]++;
187  if (val & 0x0010) cnt[ 4]++;
188  if (val & 0x0008) cnt[ 3]++;
189  if (val & 0x0004) cnt[ 2]++;
190  if (val & 0x0002) cnt[ 1]++;
191  if (val & 0x0001) cnt[ 0]++;
192  }
193  }
194  }
195 
196  /*
197  * Perform counts for each variable:
198  * cdata.var_zeros[var] = number of zeros in the variable
199  * cdata.parts_active[var] = number of active parts for each variable
200  * cdata.vars_active = number of variables which are active
201  * cdata.vars_unate = number of variables which are active and unate
202  *
203  * best -- the variable which is best for splitting based on:
204  * mostactive -- most # active parts in any variable
205  * mostzero -- most # zeros in any variable
206  * mostbalanced -- minimum over the maximum # zeros / part / variable
207  */
208 
209  { register int var, i, lastbit, active, maxactive;
210  int best = -1, mostactive = 0, mostzero = 0, mostbalanced = 32000;
211  cdata.vars_unate = cdata.vars_active = 0;
212 
213  for(var = 0; var < cube.num_vars; var++) {
214  if (var < cube.num_binary_vars) { /* special hack for binary vars */
215  i = count[var*2];
216  lastbit = count[var*2 + 1];
217  active = (i > 0) + (lastbit > 0);
218  cdata.var_zeros[var] = i + lastbit;
219  maxactive = MAX(i, lastbit);
220  } else {
221  maxactive = active = cdata.var_zeros[var] = 0;
222  lastbit = cube.last_part[var];
223  for(i = cube.first_part[var]; i <= lastbit; i++) {
224  cdata.var_zeros[var] += count[i];
225  active += (count[i] > 0);
226  if (active > maxactive) maxactive = active;
227  }
228  }
229 
230  /* first priority is to maximize the number of active parts */
231  /* for binary case, this will usually select the output first */
232  if (active > mostactive)
233  best = var, mostactive = active, mostzero = cdata.var_zeros[best],
234  mostbalanced = maxactive;
235  else if (active == mostactive)
236  {
237  /* secondary condition is to maximize the number zeros */
238  /* for binary variables, this is the same as minimum # of 2's */
239  if (cdata.var_zeros[var] > mostzero)
240  best = var, mostzero = cdata.var_zeros[best],
241  mostbalanced = maxactive;
242  else if (cdata.var_zeros[var] == mostzero)
243  /* third condition is to pick a balanced variable */
244  /* for binary vars, this means roughly equal # 0's and 1's */
245  if (maxactive < mostbalanced)
246  best = var, mostbalanced = maxactive;
247  }
248 
249  cdata.parts_active[var] = active;
250  cdata.is_unate[var] = (active == 1);
251  cdata.vars_active += (active > 0);
252  cdata.vars_unate += (active == 1);
253  }
254  cdata.best = best;
255  }
256 }
257 
258 int binate_split_select(T, cleft, cright, debug_flag)
259 IN pcube *T;
260 IN register pcube cleft, cright;
261 IN int debug_flag;
262 {
263  int best = cdata.best;
264  register int i, lastbit = cube.last_part[best], halfbit = 0;
265  register pcube cof=T[0];
266 
267  /* Create the cubes to cofactor against */
268  (void) set_diff(cleft, cube.fullset, cube.var_mask[best]);
269  (void) set_diff(cright, cube.fullset, cube.var_mask[best]);
270  for(i = cube.first_part[best]; i <= lastbit; i++)
271  if (! is_in_set(cof,i))
272  halfbit++;
273  for(i = cube.first_part[best], halfbit = halfbit/2; halfbit > 0; i++)
274  if (! is_in_set(cof,i))
275  halfbit--, set_insert(cleft, i);
276  for(; i <= lastbit; i++)
277  if (! is_in_set(cof,i))
278  set_insert(cright, i);
279 
280  if (debug & debug_flag) {
281  (void) printf("BINATE_SPLIT_SELECT: split against %d\n", best);
282  if (verbose_debug)
283  (void) printf("cl=%s\ncr=%s\n", pc1(cleft), pc2(cright));
284  }
285  return best;
286 }
287 
288 
290 pcover A;
291 {
292  register pcube last, p, *plist, *list;
293 
294  list = plist = ALLOC(pcube, A->count + 3);
295  *plist++ = new_cube();
296  plist++;
297  foreach_set(A, last, p) {
298  *plist++ = p;
299  }
300  *plist++ = NULL; /* sentinel */
301  list[1] = (pcube) plist;
302  return list;
303 }
304 
305 
307 pcover A, B;
308 {
309  register pcube last, p, *plist, *list;
310 
311  list = plist = ALLOC(pcube, A->count + B->count + 3);
312  *plist++ = new_cube();
313  plist++;
314  foreach_set(A, last, p) {
315  *plist++ = p;
316  }
317  foreach_set(B, last, p) {
318  *plist++ = p;
319  }
320  *plist++ = NULL;
321  list[1] = (pcube) plist;
322  return list;
323 }
324 
325 
326 pcube *cube3list(A, B, C)
327 pcover A, B, C;
328 {
329  register pcube last, p, *plist, *list;
330 
331  plist = ALLOC(pcube, A->count + B->count + C->count + 3);
332  list = plist;
333  *plist++ = new_cube();
334  plist++;
335  foreach_set(A, last, p) {
336  *plist++ = p;
337  }
338  foreach_set(B, last, p) {
339  *plist++ = p;
340  }
341  foreach_set(C, last, p) {
342  *plist++ = p;
343  }
344  *plist++ = NULL;
345  list[1] = (pcube) plist;
346  return list;
347 }
348 
349 
351 pcube *A1;
352 {
353  register int i;
354  register pcube p, pdest, cof = A1[0];
355  register pcover A;
356 
357  A = new_cover(CUBELISTSIZE(A1));
358  for(i = 2; (p = A1[i]) != NULL; i++) {
359  pdest = GETSET(A, i-2);
360  INLINEset_or(pdest, p, cof);
361  }
362  A->count = CUBELISTSIZE(A1);
363  return A;
364 }
365 
367 pcube *T;
368 {
369  register pcube *Tdest;
370  register int i, ncubes;
371 
372  (void) set_copy(cube.temp[0], T[0]); /* retrieve cofactor */
373 
374  ncubes = CUBELISTSIZE(T);
375  qsort((char *) (T+2), ncubes, sizeof(pset), (int (*)()) d1_order);
376 
377  Tdest = T+2;
378  /* *Tdest++ = T[2]; */
379  for(i = 3; i < ncubes; i++) {
380  if (d1_order(&T[i-1], &T[i]) != 0) {
381  *Tdest++ = T[i];
382  }
383  }
384 
385  *Tdest++ = NULL; /* sentinel */
386  Tdest[1] = (pcube) Tdest; /* save pointer to last */
387 }
389 
pcover cubeunlist(pcube *A1)
Definition: cofactor.c:350
pset set_or()
#define new_cube()
Definition: espresso.h:262
char * pc1(pcube c)
Definition: cvrout.c:379
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#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
pset set_and()
char * pc2(pcube c)
Definition: cvrout.c:381
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define IN
Definition: espresso.h:332
#define INLINEset_or(r, a, b)
Definition: espresso.h:205
void simplify_cubelist(pcube *T)
Definition: cofactor.c:366
ABC_NAMESPACE_IMPL_START pcube * cofactor(IN pcube *T, IN register pcube c)
Definition: cofactor.c:44
#define CUBELISTSIZE(T)
Definition: espresso.h:329
pset set_diff()
#define ALLOC(type, num)
Definition: avl.h:27
#define LOGBPI
Definition: espresso.h:69
unsigned int debug
Definition: globals.c:19
#define DISJOINT
Definition: espresso.h:514
pcube * cube2list(pcover A, pcover B)
Definition: cofactor.c:306
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define is_in_set(set, e)
Definition: espresso.h:170
#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
#define MAX(a, b)
Definition: avl.h:23
int d1_order()
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
pcube * scofactor(IN pcube *T, IN pcube c, IN int var)
Definition: cofactor.c:93
bool verbose_debug
Definition: globals.c:20
#define set_insert(set, e)
Definition: espresso.h:172
#define GETSET(family, index)
Definition: espresso.h:161
#define LOOP(set)
Definition: espresso.h:104
bool cdist0()
#define pcube
Definition: espresso.h:261
void massive_count(IN pcube *T)
Definition: cofactor.c:131
pcube * cube1list(pcover A)
Definition: cofactor.c:289