ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
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) */
56bool full_row(p, cof)
57IN 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
68bool cdist0(a, b)
69register 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
109int cdist01(a, b)
110register 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
154int cdist(a, b)
155register 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
195pset force_lower(xlower, a, b)
196INOUT pset xlower;
197IN 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
246void consensus(r, a, b)
247INOUT pcube r;
248IN 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
294register 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
346bool ccommon(a, b, cof)
347register 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 */
407int descend(a, b)
408pset *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 */
423int ascend(a, b)
424pset *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 */
440int lex_order(a, b)
441pset *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 */
453int d1_order(a, b)
454pset *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
469order */
470int desc1(a, b)
471register 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
#define TRUE
Definition abcBm.c:38
#define FALSE
Definition abcBm.c:37
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define b1
Definition bbrImage.c:97
int lex_order()
bool full_row()
int bit_index()
int ascend()
#define DISJOINT
Definition espresso.h:514
int d1_order()
#define INLINEset_clear(r, size)
Definition espresso.h:197
pset force_lower()
void consensus()
#define INOUT
Definition espresso.h:334
#define pcube
Definition espresso.h:261
#define LOOP(set)
Definition espresso.h:104
int desc1()
int descend()
#define SIZE(set)
Definition espresso.h:112
int cdist()
#define IN
Definition espresso.h:332
unsigned int * pset
Definition espresso.h:73
int cdist01()
#define count_ones(v)
Definition espresso.h:245
bool cdist0()
int cactive()
bool ccommon()
Cube * p
Definition exorList.c:222
@ BPI
Definition exor.h:59
#define a1
Definition extraBdd.h:80
Definition exor.h:123