00001
00002
00003
00004
00005
00006
00007
00008
00009
00010 #include "espresso.h"
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 pcube *cofactor(T, c)
00042 IN pcube *T;
00043 IN register pcube c;
00044 {
00045 pcube temp = cube.temp[0], *Tc_save, *Tc, *T1;
00046 register pcube p;
00047 int listlen;
00048
00049 listlen = CUBELISTSIZE(T) + 5;
00050
00051
00052 Tc_save = Tc = ALLOC(pcube, listlen);
00053
00054
00055 *Tc++ = set_or(new_cube(), T[0], set_diff(temp, cube.fullset, c));
00056 Tc++;
00057
00058
00059 for(T1 = T+2; (p = *T1++) != NULL; ) {
00060 if (p != c) {
00061
00062 #ifdef NO_INLINE
00063 if (! cdist0(p, c)) goto false;
00064 #else
00065 {register int w,last;register unsigned int x;if((last=cube.inword)!=-1)
00066 {x=p[last]&c[last];if(~(x|x>>1)&cube.inmask)goto false;for(w=1;w<last;w++)
00067 {x=p[w]&c[w];if(~(x|x>>1)&DISJOINT)goto false;}}}{register int w,var,last;
00068 register pcube mask;for(var=cube.num_binary_vars;var<cube.num_vars;var++){
00069 mask=cube.var_mask[var];last=cube.last_word[var];for(w=cube.first_word[var
00070 ];w<=last;w++)if(p[w]&c[w]&mask[w])goto nextvar;goto false;nextvar:;}}
00071 #endif
00072
00073 *Tc++ = p;
00074 false: ;
00075 }
00076 }
00077
00078 *Tc++ = (pcube) NULL;
00079 Tc_save[1] = (pcube) Tc;
00080 return Tc_save;
00081 }
00082
00083
00084
00085
00086
00087
00088
00089
00090 pcube *scofactor(T, c, var)
00091 IN pcube *T, c;
00092 IN int var;
00093 {
00094 pcube *Tc, *Tc_save;
00095 register pcube p, mask = cube.temp[1], *T1;
00096 register int first = cube.first_word[var], last = cube.last_word[var];
00097 int listlen;
00098
00099 listlen = CUBELISTSIZE(T) + 5;
00100
00101
00102 Tc_save = Tc = ALLOC(pcube, listlen);
00103
00104
00105 *Tc++ = set_or(new_cube(), T[0], set_diff(mask, cube.fullset, c));
00106 Tc++;
00107
00108
00109 (void) set_and(mask, cube.var_mask[var], c);
00110
00111
00112 for(T1 = T+2; (p = *T1++) != NULL; )
00113 if (p != c) {
00114 register int i = first;
00115 do
00116 if (p[i] & mask[i]) {
00117 *Tc++ = p;
00118 break;
00119 }
00120 while (++i <= last);
00121 }
00122
00123 *Tc++ = (pcube) NULL;
00124 Tc_save[1] = (pcube) Tc;
00125 return Tc_save;
00126 }
00127
00128 void massive_count(T)
00129 IN pcube *T;
00130 {
00131 int *count = cdata.part_zeros;
00132 pcube *T1;
00133
00134
00135 { register int i;
00136 for(i = cube.size - 1; i >= 0; i--)
00137 count[i] = 0;
00138 }
00139
00140
00141 { register int i, *cnt;
00142 register unsigned int val;
00143 register pcube p, cof = T[0], full = cube.fullset;
00144 for(T1 = T+2; (p = *T1++) != NULL; )
00145 for(i = LOOP(p); i > 0; i--)
00146 if (val = full[i] & ~ (p[i] | cof[i])) {
00147 cnt = count + ((i-1) << LOGBPI);
00148 #if BPI == 32
00149 if (val & 0xFF000000) {
00150 if (val & 0x80000000) cnt[31]++;
00151 if (val & 0x40000000) cnt[30]++;
00152 if (val & 0x20000000) cnt[29]++;
00153 if (val & 0x10000000) cnt[28]++;
00154 if (val & 0x08000000) cnt[27]++;
00155 if (val & 0x04000000) cnt[26]++;
00156 if (val & 0x02000000) cnt[25]++;
00157 if (val & 0x01000000) cnt[24]++;
00158 }
00159 if (val & 0x00FF0000) {
00160 if (val & 0x00800000) cnt[23]++;
00161 if (val & 0x00400000) cnt[22]++;
00162 if (val & 0x00200000) cnt[21]++;
00163 if (val & 0x00100000) cnt[20]++;
00164 if (val & 0x00080000) cnt[19]++;
00165 if (val & 0x00040000) cnt[18]++;
00166 if (val & 0x00020000) cnt[17]++;
00167 if (val & 0x00010000) cnt[16]++;
00168 }
00169 #endif
00170 if (val & 0xFF00) {
00171 if (val & 0x8000) cnt[15]++;
00172 if (val & 0x4000) cnt[14]++;
00173 if (val & 0x2000) cnt[13]++;
00174 if (val & 0x1000) cnt[12]++;
00175 if (val & 0x0800) cnt[11]++;
00176 if (val & 0x0400) cnt[10]++;
00177 if (val & 0x0200) cnt[ 9]++;
00178 if (val & 0x0100) cnt[ 8]++;
00179 }
00180 if (val & 0x00FF) {
00181 if (val & 0x0080) cnt[ 7]++;
00182 if (val & 0x0040) cnt[ 6]++;
00183 if (val & 0x0020) cnt[ 5]++;
00184 if (val & 0x0010) cnt[ 4]++;
00185 if (val & 0x0008) cnt[ 3]++;
00186 if (val & 0x0004) cnt[ 2]++;
00187 if (val & 0x0002) cnt[ 1]++;
00188 if (val & 0x0001) cnt[ 0]++;
00189 }
00190 }
00191 }
00192
00193
00194
00195
00196
00197
00198
00199
00200
00201
00202
00203
00204
00205
00206 { register int var, i, lastbit, active, maxactive;
00207 int best = -1, mostactive = 0, mostzero = 0, mostbalanced = 32000;
00208 cdata.vars_unate = cdata.vars_active = 0;
00209
00210 for(var = 0; var < cube.num_vars; var++) {
00211 if (var < cube.num_binary_vars) {
00212 i = count[var*2];
00213 lastbit = count[var*2 + 1];
00214 active = (i > 0) + (lastbit > 0);
00215 cdata.var_zeros[var] = i + lastbit;
00216 maxactive = MAX(i, lastbit);
00217 } else {
00218 maxactive = active = cdata.var_zeros[var] = 0;
00219 lastbit = cube.last_part[var];
00220 for(i = cube.first_part[var]; i <= lastbit; i++) {
00221 cdata.var_zeros[var] += count[i];
00222 active += (count[i] > 0);
00223 if (active > maxactive) maxactive = active;
00224 }
00225 }
00226
00227
00228
00229 if (active > mostactive)
00230 best = var, mostactive = active, mostzero = cdata.var_zeros[best],
00231 mostbalanced = maxactive;
00232 else if (active == mostactive)
00233
00234
00235 if (cdata.var_zeros[var] > mostzero)
00236 best = var, mostzero = cdata.var_zeros[best],
00237 mostbalanced = maxactive;
00238 else if (cdata.var_zeros[var] == mostzero)
00239
00240
00241 if (maxactive < mostbalanced)
00242 best = var, mostbalanced = maxactive;
00243
00244 cdata.parts_active[var] = active;
00245 cdata.is_unate[var] = (active == 1);
00246 cdata.vars_active += (active > 0);
00247 cdata.vars_unate += (active == 1);
00248 }
00249 cdata.best = best;
00250 }
00251 }
00252
00253 int binate_split_select(T, cleft, cright, debug_flag)
00254 IN pcube *T;
00255 IN register pcube cleft, cright;
00256 IN int debug_flag;
00257 {
00258 int best = cdata.best;
00259 register int i, lastbit = cube.last_part[best], halfbit = 0;
00260 register pcube cof=T[0];
00261
00262
00263 (void) set_diff(cleft, cube.fullset, cube.var_mask[best]);
00264 (void) set_diff(cright, cube.fullset, cube.var_mask[best]);
00265 for(i = cube.first_part[best]; i <= lastbit; i++)
00266 if (! is_in_set(cof,i))
00267 halfbit++;
00268 for(i = cube.first_part[best], halfbit = halfbit/2; halfbit > 0; i++)
00269 if (! is_in_set(cof,i))
00270 halfbit--, set_insert(cleft, i);
00271 for(; i <= lastbit; i++)
00272 if (! is_in_set(cof,i))
00273 set_insert(cright, i);
00274
00275 if (debug & debug_flag) {
00276 (void) printf("BINATE_SPLIT_SELECT: split against %d\n", best);
00277 if (verbose_debug)
00278 (void) printf("cl=%s\ncr=%s\n", pc1(cleft), pc2(cright));
00279 }
00280 return best;
00281 }
00282
00283
00284 pcube *cube1list(A)
00285 pcover A;
00286 {
00287 register pcube last, p, *plist, *list;
00288
00289 list = plist = ALLOC(pcube, A->count + 3);
00290 *plist++ = new_cube();
00291 plist++;
00292 foreach_set(A, last, p) {
00293 *plist++ = p;
00294 }
00295 *plist++ = NULL;
00296 list[1] = (pcube) plist;
00297 return list;
00298 }
00299
00300
00301 pcube *cube2list(A, B)
00302 pcover A, B;
00303 {
00304 register pcube last, p, *plist, *list;
00305
00306 list = plist = ALLOC(pcube, A->count + B->count + 3);
00307 *plist++ = new_cube();
00308 plist++;
00309 foreach_set(A, last, p) {
00310 *plist++ = p;
00311 }
00312 foreach_set(B, last, p) {
00313 *plist++ = p;
00314 }
00315 *plist++ = NULL;
00316 list[1] = (pcube) plist;
00317 return list;
00318 }
00319
00320
00321 pcube *cube3list(A, B, C)
00322 pcover A, B, C;
00323 {
00324 register pcube last, p, *plist, *list;
00325
00326 plist = ALLOC(pcube, A->count + B->count + C->count + 3);
00327 list = plist;
00328 *plist++ = new_cube();
00329 plist++;
00330 foreach_set(A, last, p) {
00331 *plist++ = p;
00332 }
00333 foreach_set(B, last, p) {
00334 *plist++ = p;
00335 }
00336 foreach_set(C, last, p) {
00337 *plist++ = p;
00338 }
00339 *plist++ = NULL;
00340 list[1] = (pcube) plist;
00341 return list;
00342 }
00343
00344
00345 pcover cubeunlist(A1)
00346 pcube *A1;
00347 {
00348 register int i;
00349 register pcube p, pdest, cof = A1[0];
00350 register pcover A;
00351
00352 A = new_cover(CUBELISTSIZE(A1));
00353 for(i = 2; (p = A1[i]) != NULL; i++) {
00354 pdest = GETSET(A, i-2);
00355 INLINEset_or(pdest, p, cof);
00356 }
00357 A->count = CUBELISTSIZE(A1);
00358 return A;
00359 }
00360
00361 simplify_cubelist(T)
00362 pcube *T;
00363 {
00364 register pcube *Tdest;
00365 register int i, ncubes;
00366
00367 (void) set_copy(cube.temp[0], T[0]);
00368
00369 ncubes = CUBELISTSIZE(T);
00370 qsort((char *) (T+2), ncubes, sizeof(pset), (int (*)()) d1_order);
00371
00372 Tdest = T+2;
00373
00374 for(i = 3; i < ncubes; i++) {
00375 if (d1_order(&T[i-1], &T[i]) != 0) {
00376 *Tdest++ = T[i];
00377 }
00378 }
00379
00380 *Tdest++ = NULL;
00381 Tdest[1] = (pcube) Tdest;
00382 }