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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START pcubecofactor (IN pcube *T, IN register pcube c)
 
pcubescofactor (IN pcube *T, IN pcube c, IN int var)
 
void massive_count (IN pcube *T)
 
int binate_split_select (IN pcube *T, IN register pcube cleft, IN register pcube cright, IN int debug_flag)
 
pcubecube1list (pcover A)
 
pcubecube2list (pcover A, pcover B)
 
pcubecube3list (pcover A, pcover B, pcover C)
 
pcover cubeunlist (pcube *A1)
 
void simplify_cubelist (pcube *T)
 

Function Documentation

int binate_split_select ( IN pcube T,
IN register pcube  cleft,
IN register pcube  cright,
IN int  debug_flag 
)

Definition at line 258 of file cofactor.c.

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 }
char * pc1(pcube c)
Definition: cvrout.c:379
char * pc2(pcube c)
Definition: cvrout.c:381
pset set_diff()
unsigned int debug
Definition: globals.c:19
#define is_in_set(set, e)
Definition: espresso.h:170
bool verbose_debug
Definition: globals.c:20
#define set_insert(set, e)
Definition: espresso.h:172
#define pcube
Definition: espresso.h:261
ABC_NAMESPACE_IMPL_START pcube* cofactor ( IN pcube T,
IN register pcube  c 
)

Definition at line 44 of file cofactor.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 }
pset set_or()
#define new_cube()
Definition: espresso.h:262
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int var(Lit p)
Definition: SolverTypes.h:62
#define CUBELISTSIZE(T)
Definition: espresso.h:329
pset set_diff()
#define ALLOC(type, num)
Definition: avl.h:27
#define DISJOINT
Definition: espresso.h:514
bool cdist0()
#define pcube
Definition: espresso.h:261
pcube* cube1list ( pcover  A)

Definition at line 289 of file cofactor.c.

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 }
#define new_cube()
Definition: espresso.h:262
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define ALLOC(type, num)
Definition: avl.h:27
#define pcube
Definition: espresso.h:261
pcube* cube2list ( pcover  A,
pcover  B 
)

Definition at line 306 of file cofactor.c.

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 }
#define new_cube()
Definition: espresso.h:262
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define ALLOC(type, num)
Definition: avl.h:27
#define pcube
Definition: espresso.h:261
pcube* cube3list ( pcover  A,
pcover  B,
pcover  C 
)

Definition at line 326 of file cofactor.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 }
#define new_cube()
Definition: espresso.h:262
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define ALLOC(type, num)
Definition: avl.h:27
#define pcube
Definition: espresso.h:261
pcover cubeunlist ( pcube A1)

Definition at line 350 of file cofactor.c.

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 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define pcover
Definition: espresso.h:264
#define INLINEset_or(r, a, b)
Definition: espresso.h:205
#define CUBELISTSIZE(T)
Definition: espresso.h:329
#define new_cover(i)
Definition: espresso.h:265
#define GETSET(family, index)
Definition: espresso.h:161
#define pcube
Definition: espresso.h:261
void massive_count ( IN pcube T)

Definition at line 131 of file cofactor.c.

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 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int var(Lit p)
Definition: SolverTypes.h:62
#define LOGBPI
Definition: espresso.h:69
#define MAX(a, b)
Definition: avl.h:23
#define LOOP(set)
Definition: espresso.h:104
#define pcube
Definition: espresso.h:261
pcube* scofactor ( IN pcube T,
IN pcube  c,
IN int  var 
)

Definition at line 93 of file cofactor.c.

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 }
pset set_or()
#define new_cube()
Definition: espresso.h:262
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int var(Lit p)
Definition: SolverTypes.h:62
pset set_and()
#define CUBELISTSIZE(T)
Definition: espresso.h:329
pset set_diff()
#define ALLOC(type, num)
Definition: avl.h:27
#define pcube
Definition: espresso.h:261
void simplify_cubelist ( pcube T)

Definition at line 366 of file cofactor.c.

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 }
pset set_copy()
#define CUBELISTSIZE(T)
Definition: espresso.h:329
unsigned int * pset
Definition: espresso.h:73
int d1_order()
#define pcube
Definition: espresso.h:261