abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
setc.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  setc.c -- massive bit-hacking for performing special "cube"-type
12  operations on a set
13 
14  The basic trick used for binary valued variables is the following:
15 
16  If a[w] and b[w] contain a full word of binary variables, then:
17 
18  1) to get the full word of their intersection, we use
19 
20  x = a[w] & b[w];
21 
22 
23  2) to see if the intersection is null in any variables, we examine
24 
25  x = ~(x | x >> 1) & DISJOINT;
26 
27  this will have a single 1 in each binary variable for which
28  the intersection is null. In particular, if this is zero,
29  then there are no disjoint variables; or, if this is nonzero,
30  then there is at least one disjoint variable. A "count_ones"
31  over x will tell in how many variables they have an null
32  intersection.
33 
34 
35  3) to get a mask which selects the disjoint variables, we use
36 
37  (x | x << 1)
38 
39  this provides a selector which can be used to see where
40  they have an null intersection
41 
42 
43  cdist return distance between two cubes
44  cdist0 return true if two cubes are distance 0 apart
45  cdist01 return distance, or 2 if distance exceeds 1
46  consensus compute consensus of two cubes distance 1 apart
47  force_lower expand hack (for now), related to consensus
48 */
49 
50 #include "espresso.h"
51 
53 
54 
55 /* see if the cube has a full row of 1's (with respect to cof) */
56 bool full_row(p, cof)
57 IN register pcube p, cof;
58 {
59  register int i = LOOP(p);
60  do if ((p[i] | cof[i]) != cube.fullset[i]) return FALSE; while (--i > 0);
61  return TRUE;
62 }
63 
64 /*
65  cdist0 -- return TRUE if a and b are distance 0 apart
66 */
67 
68 bool cdist0(a, b)
69 register pcube a, b;
70 {
71  { /* Check binary variables */
72  register int w, last; register unsigned int x;
73  if ((last = cube.inword) != -1) {
74 
75  /* Check the partial word of binary variables */
76  x = a[last] & b[last];
77  if (~(x | x >> 1) & cube.inmask)
78  return FALSE; /* disjoint in some variable */
79 
80  /* Check the full words of binary variables */
81  for(w = 1; w < last; w++) {
82  x = a[w] & b[w];
83  if (~(x | x >> 1) & DISJOINT)
84  return FALSE; /* disjoint in some variable */
85  }
86  }
87  }
88 
89  { /* Check the multiple-valued variables */
90  register int w, var, last; register pcube mask;
91  for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
92  mask = cube.var_mask[var]; last = cube.last_word[var];
93  for(w = cube.first_word[var]; w <= last; w++)
94  if (a[w] & b[w] & mask[w])
95  goto nextvar;
96  return FALSE; /* disjoint in this variable */
97  nextvar: ;
98  }
99  }
100  return TRUE;
101 }
102 
103 /*
104  cdist01 -- return the "distance" between two cubes (defined as the
105  number of null variables in their intersection). If the distance
106  exceeds 1, the value 2 is returned.
107 */
108 
109 int cdist01(a, b)
110 register pset a, b;
111 {
112  int dist = 0;
113 
114  { /* Check binary variables */
115  register int w, last; register unsigned int x;
116  if ((last = cube.inword) != -1) {
117 
118  /* Check the partial word of binary variables */
119  x = a[last] & b[last];
120  if ((x = ~ (x | x >> 1) & cube.inmask))
121  if ((dist = count_ones(x)) > 1)
122  return 2;
123 
124  /* Check the full words of binary variables */
125  for(w = 1; w < last; w++) {
126  x = a[w] & b[w];
127  if ((x = ~ (x | x >> 1) & DISJOINT))
128  if (dist == 1 || (dist += count_ones(x)) > 1)
129  return 2;
130  }
131  }
132  }
133 
134  { /* Check the multiple-valued variables */
135  register int w, var, last; register pcube mask;
136  for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
137  mask = cube.var_mask[var]; last = cube.last_word[var];
138  for(w = cube.first_word[var]; w <= last; w++)
139  if (a[w] & b[w] & mask[w])
140  goto nextvar;
141  if (++dist > 1)
142  return 2;
143  nextvar: ;
144  }
145  }
146  return dist;
147 }
148 
149 /*
150  cdist -- return the "distance" between two cubes (defined as the
151  number of null variables in their intersection).
152 */
153 
154 int cdist(a, b)
155 register pset a, b;
156 {
157  int dist = 0;
158 
159  { /* Check binary variables */
160  register int w, last; register unsigned int x;
161  if ((last = cube.inword) != -1) {
162 
163  /* Check the partial word of binary variables */
164  x = a[last] & b[last];
165  if ((x = ~ (x | x >> 1) & cube.inmask))
166  dist = count_ones(x);
167 
168  /* Check the full words of binary variables */
169  for(w = 1; w < last; w++) {
170  x = a[w] & b[w];
171  if ((x = ~ (x | x >> 1) & DISJOINT))
172  dist += count_ones(x);
173  }
174  }
175  }
176 
177  { /* Check the multiple-valued variables */
178  register int w, var, last; register pcube mask;
179  for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
180  mask = cube.var_mask[var]; last = cube.last_word[var];
181  for(w = cube.first_word[var]; w <= last; w++)
182  if (a[w] & b[w] & mask[w])
183  goto nextvar;
184  dist++;
185  nextvar: ;
186  }
187  }
188  return dist;
189 }
190 
191 /*
192  force_lower -- Determine which variables of a do not intersect b.
193 */
194 
195 pset force_lower(xlower, a, b)
196 INOUT pset xlower;
197 IN register pset a, b;
198 {
199 
200  { /* Check binary variables (if any) */
201  register int w, last; register unsigned int x;
202  if ((last = cube.inword) != -1) {
203 
204  /* Check the partial word of binary variables */
205  x = a[last] & b[last];
206  if ((x = ~(x | x >> 1) & cube.inmask))
207  xlower[last] |= (x | (x << 1)) & a[last];
208 
209  /* Check the full words of binary variables */
210  for(w = 1; w < last; w++) {
211  x = a[w] & b[w];
212  if ((x = ~(x | x >> 1) & DISJOINT))
213  xlower[w] |= (x | (x << 1)) & a[w];
214  }
215  }
216  }
217 
218  { /* Check the multiple-valued variables */
219  register int w, var, last; register pcube mask;
220  for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
221  mask = cube.var_mask[var]; last = cube.last_word[var];
222  for(w = cube.first_word[var]; w <= last; w++)
223  if (a[w] & b[w] & mask[w])
224  goto nextvar;
225  for(w = cube.first_word[var]; w <= last; w++)
226  xlower[w] |= a[w] & mask[w];
227  nextvar: ;
228  }
229  }
230  return xlower;
231 }
232 
233 /*
234  consensus -- multiple-valued consensus
235 
236  Although this looks very messy, the idea is to compute for r the
237  "and" of the cubes a and b for each variable, unless the "and" is
238  null in a variable, in which case the "or" of a and b is computed
239  for this variable.
240 
241  Because we don't check how many variables are null in the
242  intersection of a and b, the returned value for r really only
243  represents the consensus when a and b are distance 1 apart.
244 */
245 
246 void consensus(r, a, b)
247 INOUT pcube r;
248 IN register pcube a, b;
249 {
250  INLINEset_clear(r, cube.size);
251 
252  { /* Check binary variables (if any) */
253  register int w, last; register unsigned int x;
254  if ((last = cube.inword) != -1) {
255 
256  /* Check the partial word of binary variables */
257  r[last] = x = a[last] & b[last];
258  if ((x = ~(x | x >> 1) & cube.inmask))
259  r[last] |= (x | (x << 1)) & (a[last] | b[last]);
260 
261  /* Check the full words of binary variables */
262  for(w = 1; w < last; w++) {
263  r[w] = x = a[w] & b[w];
264  if ((x = ~(x | x >> 1) & DISJOINT))
265  r[w] |= (x | (x << 1)) & (a[w] | b[w]);
266  }
267  }
268  }
269 
270 
271  { /* Check the multiple-valued variables */
272  bool empty; int var; unsigned int x;
273  register int w, last; register pcube mask;
274  for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
275  mask = cube.var_mask[var];
276  last = cube.last_word[var];
277  empty = TRUE;
278  for(w = cube.first_word[var]; w <= last; w++)
279  if ((x = a[w] & b[w] & mask[w]))
280  empty = FALSE, r[w] |= x;
281  if (empty)
282  for(w = cube.first_word[var]; w <= last; w++)
283  r[w] |= mask[w] & (a[w] | b[w]);
284  }
285  }
286 }
287 
288 /*
289  cactive -- return the index of the single active variable in
290  the cube, or return -1 if there are none or more than 2.
291 */
292 
293 int cactive(a)
294 register pcube a;
295 {
296  int active = -1, dist = 0, bit_index();
297 
298  { /* Check binary variables */
299  register int w, last;
300  register unsigned int x;
301  if ((last = cube.inword) != -1) {
302 
303  /* Check the partial word of binary variables */
304  x = a[last];
305  if ((x = ~ (x & x >> 1) & cube.inmask)) {
306  if ((dist = count_ones(x)) > 1)
307  return -1; /* more than 2 active variables */
308  active = (last-1)*(BPI/2) + bit_index(x) / 2;
309  }
310 
311  /* Check the full words of binary variables */
312  for(w = 1; w < last; w++) {
313  x = a[w];
314  if ((x = ~ (x & x >> 1) & DISJOINT)) {
315  if ((dist += count_ones(x)) > 1)
316  return -1; /* more than 2 active variables */
317  active = (w-1)*(BPI/2) + bit_index(x) / 2;
318  }
319  }
320  }
321  }
322 
323  { /* Check the multiple-valued variables */
324  register int w, var, last;
325  register pcube mask;
326  for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
327  mask = cube.var_mask[var];
328  last = cube.last_word[var];
329  for(w = cube.first_word[var]; w <= last; w++)
330  if (mask[w] & ~ a[w]) {
331  if (++dist > 1)
332  return -1;
333  active = var;
334  break;
335  }
336  }
337  }
338  return active;
339 }
340 
341 /*
342  ccommon -- return TRUE if a and b are share "active" variables
343  active variables include variables that are empty;
344 */
345 
346 bool ccommon(a, b, cof)
347 register pcube a, b, cof;
348 {
349  { /* Check binary variables */
350  int last;
351  register int w;
352  register unsigned int x, y;
353  if ((last = cube.inword) != -1) {
354 
355  /* Check the partial word of binary variables */
356  x = a[last] | cof[last];
357  y = b[last] | cof[last];
358  if (~(x & x>>1) & ~(y & y>>1) & cube.inmask)
359  return TRUE;
360 
361  /* Check the full words of binary variables */
362  for(w = 1; w < last; w++) {
363  x = a[w] | cof[w];
364  y = b[w] | cof[w];
365  if (~(x & x>>1) & ~(y & y>>1) & DISJOINT)
366  return TRUE;
367  }
368  }
369  }
370 
371  { /* Check the multiple-valued variables */
372  int var;
373  register int w, last;
374  register pcube mask;
375  for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
376  mask = cube.var_mask[var]; last = cube.last_word[var];
377  /* Check for some part missing from a */
378  for(w = cube.first_word[var]; w <= last; w++)
379  if (mask[w] & ~a[w] & ~cof[w]) {
380 
381  /* If so, check for some part missing from b */
382  for(w = cube.first_word[var]; w <= last; w++)
383  if (mask[w] & ~b[w] & ~cof[w])
384  return TRUE; /* both active */
385  break;
386  }
387  }
388  }
389  return FALSE;
390 }
391 
392 /*
393  These routines compare two sets (cubes) for the qsort() routine and
394  return:
395 
396  -1 if set a is to precede set b
397  0 if set a and set b are equal
398  1 if set a is to follow set b
399 
400  Usually the SIZE field of the set is assumed to contain the size
401  of the set (which will save recomputing the set size during the
402  sort). For distance-1 merging, the global variable cube.temp[0] is
403  a mask which mask's-out the merging variable.
404 */
405 
406 /* descend -- comparison for descending sort on set size */
407 int descend(a, b)
408 pset *a, *b;
409 {
410  register pset a1 = *a, b1 = *b;
411  if (SIZE(a1) > SIZE(b1)) return -1;
412  else if (SIZE(a1) < SIZE(b1)) return 1;
413  else {
414  register int i = LOOP(a1);
415  do
416  if (a1[i] > b1[i]) return -1; else if (a1[i] < b1[i]) return 1;
417  while (--i > 0);
418  }
419  return 0;
420 }
421 
422 /* ascend -- comparison for ascending sort on set size */
423 int ascend(a, b)
424 pset *a, *b;
425 {
426  register pset a1 = *a, b1 = *b;
427  if (SIZE(a1) > SIZE(b1)) return 1;
428  else if (SIZE(a1) < SIZE(b1)) return -1;
429  else {
430  register int i = LOOP(a1);
431  do
432  if (a1[i] > b1[i]) return 1; else if (a1[i] < b1[i]) return -1;
433  while (--i > 0);
434  }
435  return 0;
436 }
437 
438 
439 /* lex_order -- comparison for "lexical" ordering of cubes */
440 int lex_order(a, b)
441 pset *a, *b;
442 {
443  register pset a1 = *a, b1 = *b;
444  register int i = LOOP(a1);
445  do
446  if (a1[i] > b1[i]) return -1; else if (a1[i] < b1[i]) return 1;
447  while (--i > 0);
448  return 0;
449 }
450 
451 
452 /* d1_order -- comparison for distance-1 merge routine */
453 int d1_order(a, b)
454 pset *a, *b;
455 {
456  register pset a1 = *a, b1 = *b, c1 = cube.temp[0];
457  register int i = LOOP(a1);
458  register unsigned int x1, x2;
459  do
460  if ((x1 = a1[i] | c1[i]) > (x2 = b1[i] | c1[i])) return -1;
461  else if (x1 < x2) return 1;
462  while (--i > 0);
463  return 0;
464 }
465 
466 
467 /* desc1 -- comparison (without indirection) for descending sort */
468 /* also has effect of handling NULL pointers,and a NULL pointer has smallest
469 order */
470 int desc1(a, b)
471 register pset a, b;
472 {
473  if (a == (pset) NULL)
474  return (b == (pset) NULL) ? 0 : 1;
475  else if (b == (pset) NULL)
476  return -1;
477  if (SIZE(a) > SIZE(b)) return -1;
478  else if (SIZE(a) < SIZE(b)) return 1;
479  else {
480  register int i = LOOP(a);
481  do
482  if (a[i] > b[i]) return -1; else if (a[i] < b[i]) return 1;
483  while (--i > 0);
484  }
485  return 0;
486 }
488 
bool ccommon(pcube a, pcube b, pcube cof)
Definition: setc.c:346
#define FALSE
Definition: cudd.h:91
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int var(Lit p)
Definition: SolverTypes.h:62
#define b1
Definition: extraBdd.h:76
#define a1
Definition: extraBdd.h:80
int cdist(pset a, pset b)
Definition: setc.c:154
bool cdist0(pcube a, pcube b)
Definition: setc.c:68
#define INOUT
Definition: espresso.h:334
#define IN
Definition: espresso.h:332
int lex_order(pset *a, pset *b)
Definition: setc.c:440
int desc1(pset a, pset b)
Definition: setc.c:470
int d1_order(pset *a, pset *b)
Definition: setc.c:453
int ascend(pset *a, pset *b)
Definition: setc.c:423
#define DISJOINT
Definition: espresso.h:514
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
int bit_index()
pset force_lower(INOUT pset xlower, IN register pset a, IN register pset b)
Definition: setc.c:195
unsigned int * pset
Definition: espresso.h:73
void consensus(INOUT pcube r, IN register pcube a, IN register pcube b)
Definition: setc.c:246
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
ABC_NAMESPACE_IMPL_START bool full_row(IN register pcube p, IN register pcube cof)
Definition: setc.c:56
#define TRUE
Definition: cudd.h:88
int descend(pset *a, pset *b)
Definition: setc.c:407
#define LOOP(set)
Definition: espresso.h:104
int cdist01(pset a, pset b)
Definition: setc.c:109
#define count_ones(v)
Definition: espresso.h:245
int cactive(pcube a)
Definition: setc.c:293
static DdNode * empty
Definition: cuddZddLin.c:98
#define SIZE(set)
Definition: espresso.h:112
#define pcube
Definition: espresso.h:261
#define INLINEset_clear(r, size)
Definition: espresso.h:197