ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
setc.c File Reference
#include "espresso.h"
Include dependency graph for setc.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START bool full_row (IN register pcube p, IN register pcube cof)
 
bool cdist0 (pcube a, pcube b)
 
int cdist01 (pset a, pset b)
 
int cdist (pset a, pset b)
 
pset force_lower (INOUT pset xlower, IN register pset a, IN register pset b)
 
void consensus (INOUT pcube r, IN register pcube a, IN register pcube b)
 
int cactive (pcube a)
 
bool ccommon (pcube a, pcube b, pcube cof)
 
int descend (pset *a, pset *b)
 
int ascend (pset *a, pset *b)
 
int lex_order (pset *a, pset *b)
 
int d1_order (pset *a, pset *b)
 
int desc1 (pset a, pset b)
 

Function Documentation

◆ ascend()

int ascend ( pset * a,
pset * b )

Definition at line 423 of file setc.c.

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}
#define b1
Definition bbrImage.c:97
#define LOOP(set)
Definition espresso.h:104
#define SIZE(set)
Definition espresso.h:112
unsigned int * pset
Definition espresso.h:73
#define a1
Definition extraBdd.h:80

◆ cactive()

int cactive ( pcube a)

Definition at line 293 of file setc.c.

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}
int bit_index()
#define DISJOINT
Definition espresso.h:514
#define pcube
Definition espresso.h:261
#define count_ones(v)
Definition espresso.h:245
@ BPI
Definition exor.h:59
unsigned short var
Definition giaNewBdd.h:35
Definition exor.h:123
Here is the call graph for this function:

◆ ccommon()

bool ccommon ( pcube a,
pcube b,
pcube cof )

Definition at line 346 of file setc.c.

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}
#define TRUE
Definition abcBm.c:38
#define FALSE
Definition abcBm.c:37

◆ cdist()

int cdist ( pset a,
pset b )

Definition at line 154 of file setc.c.

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}

◆ cdist0()

bool cdist0 ( pcube a,
pcube b )

Definition at line 68 of file setc.c.

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}

◆ cdist01()

int cdist01 ( pset a,
pset b )

Definition at line 109 of file setc.c.

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}

◆ consensus()

void consensus ( INOUT pcube r,
IN register pcube a,
IN register pcube b )

Definition at line 246 of file setc.c.

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}
#define INLINEset_clear(r, size)
Definition espresso.h:197

◆ d1_order()

int d1_order ( pset * a,
pset * b )

Definition at line 453 of file setc.c.

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}

◆ desc1()

int desc1 ( pset a,
pset b )

Definition at line 470 of file setc.c.

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}

◆ descend()

int descend ( pset * a,
pset * b )

Definition at line 407 of file setc.c.

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}

◆ force_lower()

pset force_lower ( INOUT pset xlower,
IN register pset a,
IN register pset b )

Definition at line 195 of file setc.c.

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}

◆ full_row()

ABC_NAMESPACE_IMPL_START bool full_row ( IN register pcube p,
IN register pcube cof )

Definition at line 56 of file setc.c.

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}
Cube * p
Definition exorList.c:222

◆ lex_order()

int lex_order ( pset * a,
pset * b )

Definition at line 440 of file setc.c.

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}