00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050 #include "espresso.h"
00051
00052
00053 bool full_row(p, cof)
00054 IN register pcube p, cof;
00055 {
00056 register int i = LOOP(p);
00057 do if ((p[i] | cof[i]) != cube.fullset[i]) return FALSE; while (--i > 0);
00058 return TRUE;
00059 }
00060
00061
00062
00063
00064
00065 bool cdist0(a, b)
00066 register pcube a, b;
00067 {
00068 {
00069 register int w, last; register unsigned int x;
00070 if ((last = cube.inword) != -1) {
00071
00072
00073 x = a[last] & b[last];
00074 if (~(x | x >> 1) & cube.inmask)
00075 return FALSE;
00076
00077
00078 for(w = 1; w < last; w++) {
00079 x = a[w] & b[w];
00080 if (~(x | x >> 1) & DISJOINT)
00081 return FALSE;
00082 }
00083 }
00084 }
00085
00086 {
00087 register int w, var, last; register pcube mask;
00088 for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
00089 mask = cube.var_mask[var]; last = cube.last_word[var];
00090 for(w = cube.first_word[var]; w <= last; w++)
00091 if (a[w] & b[w] & mask[w])
00092 goto nextvar;
00093 return FALSE;
00094 nextvar: ;
00095 }
00096 }
00097 return TRUE;
00098 }
00099
00100
00101
00102
00103
00104
00105
00106 int cdist01(a, b)
00107 register pset a, b;
00108 {
00109 int dist = 0;
00110
00111 {
00112 register int w, last; register unsigned int x;
00113 if ((last = cube.inword) != -1) {
00114
00115
00116 x = a[last] & b[last];
00117 if (x = ~ (x | x >> 1) & cube.inmask)
00118 if ((dist = count_ones(x)) > 1)
00119 return 2;
00120
00121
00122 for(w = 1; w < last; w++) {
00123 x = a[w] & b[w];
00124 if (x = ~ (x | x >> 1) & DISJOINT)
00125 if (dist == 1 || (dist += count_ones(x)) > 1)
00126 return 2;
00127 }
00128 }
00129 }
00130
00131 {
00132 register int w, var, last; register pcube mask;
00133 for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
00134 mask = cube.var_mask[var]; last = cube.last_word[var];
00135 for(w = cube.first_word[var]; w <= last; w++)
00136 if (a[w] & b[w] & mask[w])
00137 goto nextvar;
00138 if (++dist > 1)
00139 return 2;
00140 nextvar: ;
00141 }
00142 }
00143 return dist;
00144 }
00145
00146
00147
00148
00149
00150
00151 int cdist(a, b)
00152 register pset a, b;
00153 {
00154 int dist = 0;
00155
00156 {
00157 register int w, last; register unsigned int x;
00158 if ((last = cube.inword) != -1) {
00159
00160
00161 x = a[last] & b[last];
00162 if (x = ~ (x | x >> 1) & cube.inmask)
00163 dist = count_ones(x);
00164
00165
00166 for(w = 1; w < last; w++) {
00167 x = a[w] & b[w];
00168 if (x = ~ (x | x >> 1) & DISJOINT)
00169 dist += count_ones(x);
00170 }
00171 }
00172 }
00173
00174 {
00175 register int w, var, last; register pcube mask;
00176 for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
00177 mask = cube.var_mask[var]; last = cube.last_word[var];
00178 for(w = cube.first_word[var]; w <= last; w++)
00179 if (a[w] & b[w] & mask[w])
00180 goto nextvar;
00181 dist++;
00182 nextvar: ;
00183 }
00184 }
00185 return dist;
00186 }
00187
00188
00189
00190
00191
00192 pset force_lower(xlower, a, b)
00193 INOUT pset xlower;
00194 IN register pset a, b;
00195 {
00196
00197 {
00198 register int w, last; register unsigned int x;
00199 if ((last = cube.inword) != -1) {
00200
00201
00202 x = a[last] & b[last];
00203 if (x = ~(x | x >> 1) & cube.inmask)
00204 xlower[last] |= (x | (x << 1)) & a[last];
00205
00206
00207 for(w = 1; w < last; w++) {
00208 x = a[w] & b[w];
00209 if (x = ~(x | x >> 1) & DISJOINT)
00210 xlower[w] |= (x | (x << 1)) & a[w];
00211 }
00212 }
00213 }
00214
00215 {
00216 register int w, var, last; register pcube mask;
00217 for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
00218 mask = cube.var_mask[var]; last = cube.last_word[var];
00219 for(w = cube.first_word[var]; w <= last; w++)
00220 if (a[w] & b[w] & mask[w])
00221 goto nextvar;
00222 for(w = cube.first_word[var]; w <= last; w++)
00223 xlower[w] |= a[w] & mask[w];
00224 nextvar: ;
00225 }
00226 }
00227 return xlower;
00228 }
00229
00230
00231
00232
00233
00234
00235
00236
00237
00238
00239
00240
00241
00242
00243 void consensus(r, a, b)
00244 INOUT pcube r;
00245 IN register pcube a, b;
00246 {
00247 INLINEset_clear(r, cube.size);
00248
00249 {
00250 register int w, last; register unsigned int x;
00251 if ((last = cube.inword) != -1) {
00252
00253
00254 r[last] = x = a[last] & b[last];
00255 if (x = ~(x | x >> 1) & cube.inmask)
00256 r[last] |= (x | (x << 1)) & (a[last] | b[last]);
00257
00258
00259 for(w = 1; w < last; w++) {
00260 r[w] = x = a[w] & b[w];
00261 if (x = ~(x | x >> 1) & DISJOINT)
00262 r[w] |= (x | (x << 1)) & (a[w] | b[w]);
00263 }
00264 }
00265 }
00266
00267
00268 {
00269 bool empty; int var; unsigned int x;
00270 register int w, last; register pcube mask;
00271 for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
00272 mask = cube.var_mask[var];
00273 last = cube.last_word[var];
00274 empty = TRUE;
00275 for(w = cube.first_word[var]; w <= last; w++)
00276 if (x = a[w] & b[w] & mask[w])
00277 empty = FALSE, r[w] |= x;
00278 if (empty)
00279 for(w = cube.first_word[var]; w <= last; w++)
00280 r[w] |= mask[w] & (a[w] | b[w]);
00281 }
00282 }
00283 }
00284
00285
00286
00287
00288
00289
00290 int cactive(a)
00291 register pcube a;
00292 {
00293 int active = -1, dist = 0, bit_index();
00294
00295 {
00296 register int w, last;
00297 register unsigned int x;
00298 if ((last = cube.inword) != -1) {
00299
00300
00301 x = a[last];
00302 if (x = ~ (x & x >> 1) & cube.inmask) {
00303 if ((dist = count_ones(x)) > 1)
00304 return -1;
00305 active = (last-1)*(BPI/2) + bit_index(x) / 2;
00306 }
00307
00308
00309 for(w = 1; w < last; w++) {
00310 x = a[w];
00311 if (x = ~ (x & x >> 1) & DISJOINT) {
00312 if ((dist += count_ones(x)) > 1)
00313 return -1;
00314 active = (w-1)*(BPI/2) + bit_index(x) / 2;
00315 }
00316 }
00317 }
00318 }
00319
00320 {
00321 register int w, var, last;
00322 register pcube mask;
00323 for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
00324 mask = cube.var_mask[var];
00325 last = cube.last_word[var];
00326 for(w = cube.first_word[var]; w <= last; w++)
00327 if (mask[w] & ~ a[w]) {
00328 if (++dist > 1)
00329 return -1;
00330 active = var;
00331 break;
00332 }
00333 }
00334 }
00335 return active;
00336 }
00337
00338
00339
00340
00341
00342
00343 bool ccommon(a, b, cof)
00344 register pcube a, b, cof;
00345 {
00346 {
00347 int last;
00348 register int w;
00349 register unsigned int x, y;
00350 if ((last = cube.inword) != -1) {
00351
00352
00353 x = a[last] | cof[last];
00354 y = b[last] | cof[last];
00355 if (~(x & x>>1) & ~(y & y>>1) & cube.inmask)
00356 return TRUE;
00357
00358
00359 for(w = 1; w < last; w++) {
00360 x = a[w] | cof[w];
00361 y = b[w] | cof[w];
00362 if (~(x & x>>1) & ~(y & y>>1) & DISJOINT)
00363 return TRUE;
00364 }
00365 }
00366 }
00367
00368 {
00369 int var;
00370 register int w, last;
00371 register pcube mask;
00372 for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
00373 mask = cube.var_mask[var]; last = cube.last_word[var];
00374
00375 for(w = cube.first_word[var]; w <= last; w++)
00376 if (mask[w] & ~a[w] & ~cof[w]) {
00377
00378
00379 for(w = cube.first_word[var]; w <= last; w++)
00380 if (mask[w] & ~b[w] & ~cof[w])
00381 return TRUE;
00382 break;
00383 }
00384 }
00385 }
00386 return FALSE;
00387 }
00388
00389
00390
00391
00392
00393
00394
00395
00396
00397
00398
00399
00400
00401
00402
00403
00404 int descend(a, b)
00405 pset *a, *b;
00406 {
00407 register pset a1 = *a, b1 = *b;
00408 if (SIZE(a1) > SIZE(b1)) return -1;
00409 else if (SIZE(a1) < SIZE(b1)) return 1;
00410 else {
00411 register int i = LOOP(a1);
00412 do
00413 if (a1[i] > b1[i]) return -1; else if (a1[i] < b1[i]) return 1;
00414 while (--i > 0);
00415 }
00416 return 0;
00417 }
00418
00419
00420 int ascend(a, b)
00421 pset *a, *b;
00422 {
00423 register pset a1 = *a, b1 = *b;
00424 if (SIZE(a1) > SIZE(b1)) return 1;
00425 else if (SIZE(a1) < SIZE(b1)) return -1;
00426 else {
00427 register int i = LOOP(a1);
00428 do
00429 if (a1[i] > b1[i]) return 1; else if (a1[i] < b1[i]) return -1;
00430 while (--i > 0);
00431 }
00432 return 0;
00433 }
00434
00435
00436
00437 int lex_order(a, b)
00438 pset *a, *b;
00439 {
00440 register pset a1 = *a, b1 = *b;
00441 register int i = LOOP(a1);
00442 do
00443 if (a1[i] > b1[i]) return -1; else if (a1[i] < b1[i]) return 1;
00444 while (--i > 0);
00445 return 0;
00446 }
00447
00448
00449
00450 int d1_order(a, b)
00451 pset *a, *b;
00452 {
00453 register pset a1 = *a, b1 = *b, c1 = cube.temp[0];
00454 register int i = LOOP(a1);
00455 register unsigned int x1, x2;
00456 do
00457 if ((x1 = a1[i] | c1[i]) > (x2 = b1[i] | c1[i])) return -1;
00458 else if (x1 < x2) return 1;
00459 while (--i > 0);
00460 return 0;
00461 }
00462
00463
00464
00465
00466
00467 int desc1(a, b)
00468 register pset a, b;
00469 {
00470 if (a == (pset) NULL)
00471 return (b == (pset) NULL) ? 0 : 1;
00472 else if (b == (pset) NULL)
00473 return -1;
00474 if (SIZE(a) > SIZE(b)) return -1;
00475 else if (SIZE(a) < SIZE(b)) return 1;
00476 else {
00477 register int i = LOOP(a);
00478 do
00479 if (a[i] > b[i]) return -1; else if (a[i] < b[i]) return 1;
00480 while (--i > 0);
00481 }
00482 return 0;
00483 }