00001
00055 #include "util.h"
00056 #include "cuddInt.h"
00057
00058
00059
00060
00061
00062
00063
00064
00065
00066
00067
00068
00069
00070
00071
00072
00073
00074
00075
00076
00077
00078 #ifndef lint
00079 static char rcsid[] DD_UNUSED = "$Id: cuddSign.c,v 1.22 2009/02/20 02:14:58 fabio Exp $";
00080 #endif
00081
00082 static int size;
00083
00084 #ifdef DD_STATS
00085 static int num_calls;
00086 static int table_mem;
00087 #endif
00088
00089
00090
00091
00092
00093
00094
00097
00098
00099
00100
00101 static double * ddCofMintermAux (DdManager *dd, DdNode *node, st_table *table);
00102
00106
00107
00108
00109
00126 double *
00127 Cudd_CofMinterm(
00128 DdManager * dd,
00129 DdNode * node)
00130 {
00131 st_table *table;
00132 double *values;
00133 double *result = NULL;
00134 int i, firstLevel;
00135
00136 #ifdef DD_STATS
00137 long startTime;
00138 startTime = util_cpu_time();
00139 num_calls = 0;
00140 table_mem = sizeof(st_table);
00141 #endif
00142
00143 table = st_init_table(st_ptrcmp, st_ptrhash);
00144 if (table == NULL) {
00145 (void) fprintf(dd->err,
00146 "out-of-memory, couldn't measure DD cofactors.\n");
00147 dd->errorCode = CUDD_MEMORY_OUT;
00148 return(NULL);
00149 }
00150 size = dd->size;
00151 values = ddCofMintermAux(dd, node, table);
00152 if (values != NULL) {
00153 result = ALLOC(double,size + 1);
00154 if (result != NULL) {
00155 #ifdef DD_STATS
00156 table_mem += (size + 1) * sizeof(double);
00157 #endif
00158 if (Cudd_IsConstant(node))
00159 firstLevel = 1;
00160 else
00161 firstLevel = cuddI(dd,Cudd_Regular(node)->index);
00162 for (i = 0; i < size; i++) {
00163 if (i >= cuddI(dd,Cudd_Regular(node)->index)) {
00164 result[dd->invperm[i]] = values[i - firstLevel];
00165 } else {
00166 result[dd->invperm[i]] = values[size - firstLevel];
00167 }
00168 }
00169 result[size] = values[size - firstLevel];
00170 } else {
00171 dd->errorCode = CUDD_MEMORY_OUT;
00172 }
00173 }
00174
00175 #ifdef DD_STATS
00176 table_mem += table->num_bins * sizeof(st_table_entry *);
00177 #endif
00178 if (Cudd_Regular(node)->ref == 1) FREE(values);
00179 st_foreach(table, cuddStCountfree, NULL);
00180 st_free_table(table);
00181 #ifdef DD_STATS
00182 (void) fprintf(dd->out,"Number of calls: %d\tTable memory: %d bytes\n",
00183 num_calls, table_mem);
00184 (void) fprintf(dd->out,"Time to compute measures: %s\n",
00185 util_print_time(util_cpu_time() - startTime));
00186 #endif
00187 if (result == NULL) {
00188 (void) fprintf(dd->out,
00189 "out-of-memory, couldn't measure DD cofactors.\n");
00190 dd->errorCode = CUDD_MEMORY_OUT;
00191 }
00192 return(result);
00193
00194 }
00195
00196
00197
00198
00199
00200
00201
00202
00203
00204
00205
00206
00227 static double *
00228 ddCofMintermAux(
00229 DdManager * dd,
00230 DdNode * node,
00231 st_table * table)
00232 {
00233 DdNode *N;
00234 DdNode *Nv, *Nnv;
00235 double *values;
00236 double *valuesT, *valuesE;
00237 int i;
00238 int localSize, localSizeT, localSizeE;
00239 double vT, vE;
00240
00241 statLine(dd);
00242 #ifdef DD_STATS
00243 num_calls++;
00244 #endif
00245
00246 if (st_lookup(table, node, &values)) {
00247 return(values);
00248 }
00249
00250 N = Cudd_Regular(node);
00251 if (cuddIsConstant(N)) {
00252 localSize = 1;
00253 } else {
00254 localSize = size - cuddI(dd,N->index) + 1;
00255 }
00256 values = ALLOC(double, localSize);
00257 if (values == NULL) {
00258 dd->errorCode = CUDD_MEMORY_OUT;
00259 return(NULL);
00260 }
00261
00262 if (cuddIsConstant(N)) {
00263 if (node == DD_ZERO(dd) || node == Cudd_Not(DD_ONE(dd))) {
00264 values[0] = 0.0;
00265 } else {
00266 values[0] = 1.0;
00267 }
00268 } else {
00269 Nv = Cudd_NotCond(cuddT(N),N!=node);
00270 Nnv = Cudd_NotCond(cuddE(N),N!=node);
00271
00272 valuesT = ddCofMintermAux(dd, Nv, table);
00273 if (valuesT == NULL) return(NULL);
00274 valuesE = ddCofMintermAux(dd, Nnv, table);
00275 if (valuesE == NULL) return(NULL);
00276
00277 if (Cudd_IsConstant(Nv)) {
00278 localSizeT = 1;
00279 } else {
00280 localSizeT = size - cuddI(dd,Cudd_Regular(Nv)->index) + 1;
00281 }
00282 if (Cudd_IsConstant(Nnv)) {
00283 localSizeE = 1;
00284 } else {
00285 localSizeE = size - cuddI(dd,Cudd_Regular(Nnv)->index) + 1;
00286 }
00287 values[0] = valuesT[localSizeT - 1];
00288 for (i = 1; i < localSize; i++) {
00289 if (i >= cuddI(dd,Cudd_Regular(Nv)->index) - cuddI(dd,N->index)) {
00290 vT = valuesT[i - cuddI(dd,Cudd_Regular(Nv)->index) +
00291 cuddI(dd,N->index)];
00292 } else {
00293 vT = valuesT[localSizeT - 1];
00294 }
00295 if (i >= cuddI(dd,Cudd_Regular(Nnv)->index) - cuddI(dd,N->index)) {
00296 vE = valuesE[i - cuddI(dd,Cudd_Regular(Nnv)->index) +
00297 cuddI(dd,N->index)];
00298 } else {
00299 vE = valuesE[localSizeE - 1];
00300 }
00301 values[i] = (vT + vE) / 2.0;
00302 }
00303 if (Cudd_Regular(Nv)->ref == 1) FREE(valuesT);
00304 if (Cudd_Regular(Nnv)->ref == 1) FREE(valuesE);
00305 }
00306
00307 if (N->ref > 1) {
00308 if (st_add_direct(table, (char *) node, (char *) values) == ST_OUT_OF_MEM) {
00309 FREE(values);
00310 return(NULL);
00311 }
00312 #ifdef DD_STATS
00313 table_mem += localSize * sizeof(double) + sizeof(st_table_entry);
00314 #endif
00315 }
00316 return(values);
00317
00318 }
