00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019 #include "espresso.h"
00020
00021 static bool toggle = TRUE;
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
00051
00052
00053
00054
00055
00056 pcover reduce(F, D)
00057 INOUT pcover F;
00058 IN pcover D;
00059 {
00060 register pcube last, p, cunder, *FD;
00061
00062
00063 if (use_random_order)
00064 F = random_order(F);
00065 else {
00066 F = toggle ? sort_reduce(F) : mini_sort(F, descend);
00067 toggle = ! toggle;
00068 }
00069
00070
00071 FD = cube2list(F, D);
00072 foreach_set(F, last, p) {
00073 cunder = reduce_cube(FD, p);
00074 if (setp_equal(cunder, p)) {
00075 SET(p, ACTIVE);
00076 SET(p, PRIME);
00077 } else {
00078 if (debug & REDUCE) {
00079 printf("REDUCE: %s to %s %s\n",
00080 pc1(p), pc2(cunder), print_time(ptime()));
00081 }
00082 set_copy(p, cunder);
00083 RESET(p, PRIME);
00084 if (setp_empty(cunder))
00085 RESET(p, ACTIVE);
00086 else
00087 SET(p, ACTIVE);
00088 }
00089 free_cube(cunder);
00090 }
00091 free_cubelist(FD);
00092
00093
00094 return sf_inactive(F);
00095 }
00096
00097
00098 pcube reduce_cube(FD, p)
00099 IN pcube *FD, p;
00100 {
00101 pcube cunder;
00102
00103 cunder = sccc(cofactor(FD, p));
00104 return set_and(cunder, cunder, p);
00105 }
00106
00107
00108
00109 pcube sccc(T)
00110 INOUT pcube *T;
00111 {
00112 pcube r;
00113 register pcube cl, cr;
00114 register int best;
00115 static int sccc_level = 0;
00116
00117 if (debug & REDUCE1) {
00118 debug_print(T, "SCCC", sccc_level++);
00119 }
00120
00121 if (sccc_special_cases(T, &r) == MAYBE) {
00122 cl = new_cube();
00123 cr = new_cube();
00124 best = binate_split_select(T, cl, cr, REDUCE1);
00125 r = sccc_merge(sccc(scofactor(T, cl, best)),
00126 sccc(scofactor(T, cr, best)), cl, cr);
00127 free_cubelist(T);
00128 }
00129
00130 if (debug & REDUCE1)
00131 printf("SCCC[%d]: result is %s\n", --sccc_level, pc1(r));
00132 return r;
00133 }
00134
00135
00136 pcube sccc_merge(left, right, cl, cr)
00137 INOUT register pcube left, right;
00138 INOUT register pcube cl, cr;
00139 {
00140 INLINEset_and(left, left, cl);
00141 INLINEset_and(right, right, cr);
00142 INLINEset_or(left, left, right);
00143 free_cube(right);
00144 free_cube(cl);
00145 free_cube(cr);
00146 return left;
00147 }
00148
00149
00150
00151
00152
00153
00154
00155
00156
00157
00158
00159
00160
00161
00162
00163 pcube sccc_cube(result, p)
00164 register pcube result, p;
00165 {
00166 register pcube temp=cube.temp[0], mask;
00167 int var;
00168
00169 if ((var = cactive(p)) >= 0) {
00170 mask = cube.var_mask[var];
00171 INLINEset_xor(temp, p, mask);
00172 INLINEset_and(result, result, temp);
00173 }
00174 return result;
00175 }
00176
00177
00178
00179
00180
00181 bool sccc_special_cases(T, result)
00182 INOUT pcube *T;
00183 OUT pcube *result;
00184 {
00185 register pcube *T1, p, temp = cube.temp[1], ceil, cof = T[0];
00186 pcube *A, *B;
00187
00188
00189 if (T[2] == NULL) {
00190 *result = set_save(cube.fullset);
00191 free_cubelist(T);
00192 return TRUE;
00193 }
00194
00195
00196 for(T1 = T+2; (p = *T1++) != NULL; ) {
00197 if (full_row(p, cof)) {
00198 *result = new_cube();
00199 free_cubelist(T);
00200 return TRUE;
00201 }
00202 }
00203
00204
00205 massive_count(T);
00206
00207
00208 if (cdata.vars_unate == cdata.vars_active || T[3] == NULL) {
00209 *result = set_save(cube.fullset);
00210 for(T1 = T+2; (p = *T1++) != NULL; ) {
00211 (void) sccc_cube(*result, set_or(temp, p, cof));
00212 }
00213 free_cubelist(T);
00214 return TRUE;
00215 }
00216
00217
00218 ceil = set_save(cof);
00219 for(T1 = T+2; (p = *T1++) != NULL; ) {
00220 INLINEset_or(ceil, ceil, p);
00221 }
00222 if (! setp_equal(ceil, cube.fullset)) {
00223 *result = sccc_cube(set_save(cube.fullset), ceil);
00224 if (setp_equal(*result, cube.fullset)) {
00225 free_cube(ceil);
00226 } else {
00227 *result = sccc_merge(sccc(cofactor(T,ceil)),
00228 set_save(cube.fullset), ceil, *result);
00229 }
00230 free_cubelist(T);
00231 return TRUE;
00232 }
00233 free_cube(ceil);
00234
00235
00236 if (cdata.vars_active == 1) {
00237 *result = new_cube();
00238 free_cubelist(T);
00239 return TRUE;
00240 }
00241
00242
00243 if (cdata.var_zeros[cdata.best] < CUBELISTSIZE(T)/2) {
00244 if (cubelist_partition(T, &A, &B, debug & REDUCE1) == 0) {
00245 return MAYBE;
00246 } else {
00247 free_cubelist(T);
00248 *result = sccc(A);
00249 ceil = sccc(B);
00250 (void) set_and(*result, *result, ceil);
00251 set_free(ceil);
00252 return TRUE;
00253 }
00254 }
00255
00256
00257 return MAYBE;
00258 }