134 int *count = cdata.part_zeros;
139 for(i = cube.size - 1; i >= 0; i--)
144 {
register int i, *cnt;
145 register unsigned int val;
146 register pcube p, cof = T[0], full = cube.fullset;
147 for(T1 = T+2; (p = *T1++) != NULL; )
148 for(i =
LOOP(p); i > 0; i--)
149 if ((val = full[i] & ~ (p[i] | cof[i]))) {
150 cnt = count + ((i-1) <<
LOGBPI);
152 if (val & 0xFF000000) {
153 if (val & 0x80000000) cnt[31]++;
154 if (val & 0x40000000) cnt[30]++;
155 if (val & 0x20000000) cnt[29]++;
156 if (val & 0x10000000) cnt[28]++;
157 if (val & 0x08000000) cnt[27]++;
158 if (val & 0x04000000) cnt[26]++;
159 if (val & 0x02000000) cnt[25]++;
160 if (val & 0x01000000) cnt[24]++;
162 if (val & 0x00FF0000) {
163 if (val & 0x00800000) cnt[23]++;
164 if (val & 0x00400000) cnt[22]++;
165 if (val & 0x00200000) cnt[21]++;
166 if (val & 0x00100000) cnt[20]++;
167 if (val & 0x00080000) cnt[19]++;
168 if (val & 0x00040000) cnt[18]++;
169 if (val & 0x00020000) cnt[17]++;
170 if (val & 0x00010000) cnt[16]++;
174 if (val & 0x8000) cnt[15]++;
175 if (val & 0x4000) cnt[14]++;
176 if (val & 0x2000) cnt[13]++;
177 if (val & 0x1000) cnt[12]++;
178 if (val & 0x0800) cnt[11]++;
179 if (val & 0x0400) cnt[10]++;
180 if (val & 0x0200) cnt[ 9]++;
181 if (val & 0x0100) cnt[ 8]++;
184 if (val & 0x0080) cnt[ 7]++;
185 if (val & 0x0040) cnt[ 6]++;
186 if (val & 0x0020) cnt[ 5]++;
187 if (val & 0x0010) cnt[ 4]++;
188 if (val & 0x0008) cnt[ 3]++;
189 if (val & 0x0004) cnt[ 2]++;
190 if (val & 0x0002) cnt[ 1]++;
191 if (val & 0x0001) cnt[ 0]++;
209 {
register int var, i, lastbit, active, maxactive;
210 int best = -1, mostactive = 0, mostzero = 0, mostbalanced = 32000;
211 cdata.vars_unate = cdata.vars_active = 0;
213 for(var = 0; var < cube.num_vars; var++) {
214 if (var < cube.num_binary_vars) {
216 lastbit = count[var*2 + 1];
217 active = (i > 0) + (lastbit > 0);
218 cdata.var_zeros[
var] = i + lastbit;
219 maxactive =
MAX(i, lastbit);
221 maxactive = active = cdata.var_zeros[
var] = 0;
222 lastbit = cube.last_part[
var];
223 for(i = cube.first_part[var]; i <= lastbit; i++) {
224 cdata.var_zeros[
var] += count[i];
225 active += (count[i] > 0);
226 if (active > maxactive) maxactive = active;
232 if (active > mostactive)
233 best =
var, mostactive = active, mostzero = cdata.var_zeros[
best],
234 mostbalanced = maxactive;
235 else if (active == mostactive)
239 if (cdata.var_zeros[var] > mostzero)
240 best =
var, mostzero = cdata.var_zeros[
best],
241 mostbalanced = maxactive;
242 else if (cdata.var_zeros[var] == mostzero)
245 if (maxactive < mostbalanced)
246 best =
var, mostbalanced = maxactive;
249 cdata.parts_active[
var] = active;
250 cdata.is_unate[
var] = (active == 1);
251 cdata.vars_active += (active > 0);
252 cdata.vars_unate += (active == 1);