00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015 #include "espresso.h"
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036 pcover essential(Fp, Dp)
00037 IN pcover *Fp, *Dp;
00038 {
00039 register pcube last, p;
00040 pcover E, F = *Fp, D = *Dp;
00041
00042
00043 (void) sf_active(F);
00044
00045
00046 E = new_cover(10);
00047
00048 foreach_set(F, last, p) {
00049
00050 if (! TESTP(p, NONESSEN)) {
00051
00052 if (TESTP(p, RELESSEN)) {
00053
00054 if (essen_cube(F, D, p)) {
00055 if (debug & ESSEN)
00056 printf("ESSENTIAL: %s\n", pc1(p));
00057 E = sf_addset(E, p);
00058 RESET(p, ACTIVE);
00059 F->active_count--;
00060 }
00061 }
00062 }
00063 }
00064
00065 *Fp = sf_inactive(F);
00066 *Dp = sf_join(D, E);
00067 sf_free(D);
00068 return E;
00069 }
00070
00071
00072
00073
00074
00075
00076
00077
00078
00079
00080 bool essen_cube(F, D, c)
00081 IN pcover F, D;
00082 IN pcube c;
00083 {
00084 pcover H, FD;
00085 pcube *H1;
00086 bool essen;
00087
00088
00089 FD = sf_join(F, D);
00090 H = cb_consensus(FD, c);
00091 free_cover(FD);
00092
00093
00094 H1 = cube2list(H, D);
00095 essen = ! cube_is_covered(H1, c);
00096 free_cubelist(H1);
00097
00098 free_cover(H);
00099 return essen;
00100 }
00101
00102
00103
00104
00105
00106 pcover cb_consensus(T, c)
00107 register pcover T;
00108 register pcube c;
00109 {
00110 register pcube temp, last, p;
00111 register pcover R;
00112
00113 R = new_cover(T->count*2);
00114 temp = new_cube();
00115 foreach_set(T, last, p) {
00116 if (p != c) {
00117 switch (cdist01(p, c)) {
00118 case 0:
00119
00120 R = cb_consensus_dist0(R, p, c);
00121 break;
00122
00123 case 1:
00124
00125 consensus(temp, p, c);
00126 R = sf_addset(R, temp);
00127 break;
00128 }
00129 }
00130 }
00131 set_free(temp);
00132 return R;
00133 }
00134
00135
00136
00137
00138
00139
00140 pcover cb_consensus_dist0(R, p, c)
00141 pcover R;
00142 register pcube p, c;
00143 {
00144 int var;
00145 bool got_one;
00146 register pcube temp, mask;
00147 register pcube p_diff_c=cube.temp[0], p_and_c=cube.temp[1];
00148
00149
00150 if (setp_implies(p, c)) {
00151 return R;
00152 }
00153
00154
00155 temp = new_cube();
00156 got_one = FALSE;
00157 INLINEset_diff(p_diff_c, p, c);
00158 INLINEset_and(p_and_c, p, c);
00159
00160 for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
00161
00162 mask = cube.var_mask[var];
00163 if (! setp_disjoint(p_diff_c, mask)) {
00164 INLINEset_merge(temp, c, p_and_c, mask);
00165 R = sf_addset(R, temp);
00166 got_one = TRUE;
00167 }
00168 }
00169
00170
00171 if (! got_one && cube.num_binary_vars > 0) {
00172
00173 INLINEset_and(temp, p, c);
00174 R = sf_addset(R, temp);
00175 }
00176
00177 set_free(temp);
00178 return R;
00179 }