00001
00028 #include "util_hack.h"
00029 #include "cuddInt.h"
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051 #ifndef lint
00052 static char rcsid[] DD_UNUSED = "$Id: cuddSign.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
00053 #endif
00054
00055 static int size;
00056
00057 #ifdef DD_STATS
00058 static int num_calls;
00059 static int table_mem;
00060 #endif
00061
00062
00063
00064
00065
00066
00067
00070
00071
00072
00073
00074 static double * ddCofMintermAux ARGS((DdManager *dd, DdNode *node, st_table *table));
00075
00079
00080
00081
00082
00099 double *
00100 Cudd_CofMinterm(
00101 DdManager * dd,
00102 DdNode * node)
00103 {
00104 st_table *table;
00105 double *values;
00106 double *result = NULL;
00107 int i, firstLevel;
00108
00109 #ifdef DD_STATS
00110 long startTime;
00111 startTime = util_cpu_time();
00112 num_calls = 0;
00113 table_mem = sizeof(st_table);
00114 #endif
00115
00116 table = st_init_table(st_ptrcmp, st_ptrhash);
00117 if (table == NULL) {
00118 (void) fprintf(dd->err,
00119 "out-of-memory, couldn't measure DD cofactors.\n");
00120 dd->errorCode = CUDD_MEMORY_OUT;
00121 return(NULL);
00122 }
00123 size = dd->size;
00124 values = ddCofMintermAux(dd, node, table);
00125 if (values != NULL) {
00126 result = ALLOC(double,size + 1);
00127 if (result != NULL) {
00128 #ifdef DD_STATS
00129 table_mem += (size + 1) * sizeof(double);
00130 #endif
00131 if (Cudd_IsConstant(node))
00132 firstLevel = 1;
00133 else
00134 firstLevel = cuddI(dd,Cudd_Regular(node)->index);
00135 for (i = 0; i < size; i++) {
00136 if (i >= cuddI(dd,Cudd_Regular(node)->index)) {
00137 result[dd->invperm[i]] = values[i - firstLevel];
00138 } else {
00139 result[dd->invperm[i]] = values[size - firstLevel];
00140 }
00141 }
00142 result[size] = values[size - firstLevel];
00143 } else {
00144 dd->errorCode = CUDD_MEMORY_OUT;
00145 }
00146 }
00147
00148 #ifdef DD_STATS
00149 table_mem += table->num_bins * sizeof(st_table_entry *);
00150 #endif
00151 if (Cudd_Regular(node)->ref == 1) FREE(values);
00152 st_foreach(table, cuddStCountfree, NULL);
00153 st_free_table(table);
00154 #ifdef DD_STATS
00155 (void) fprintf(dd->out,"Number of calls: %d\tTable memory: %d bytes\n",
00156 num_calls, table_mem);
00157 (void) fprintf(dd->out,"Time to compute measures: %s\n",
00158 util_print_time(util_cpu_time() - startTime));
00159 #endif
00160 if (result == NULL) {
00161 (void) fprintf(dd->out,
00162 "out-of-memory, couldn't measure DD cofactors.\n");
00163 dd->errorCode = CUDD_MEMORY_OUT;
00164 }
00165 return(result);
00166
00167 }
00168
00169
00170
00171
00172
00173
00174
00175
00176
00177
00178
00179
00200 static double *
00201 ddCofMintermAux(
00202 DdManager * dd,
00203 DdNode * node,
00204 st_table * table)
00205 {
00206 DdNode *N;
00207 DdNode *Nv, *Nnv;
00208 double *values;
00209 double *valuesT, *valuesE;
00210 int i;
00211 int localSize, localSizeT, localSizeE;
00212 double vT, vE;
00213
00214 statLine(dd);
00215 #ifdef DD_STATS
00216 num_calls++;
00217 #endif
00218
00219 if (st_lookup(table, (char *) node, (char **) &values)) {
00220 return(values);
00221 }
00222
00223 N = Cudd_Regular(node);
00224 if (cuddIsConstant(N)) {
00225 localSize = 1;
00226 } else {
00227 localSize = size - cuddI(dd,N->index) + 1;
00228 }
00229 values = ALLOC(double, localSize);
00230 if (values == NULL) {
00231 dd->errorCode = CUDD_MEMORY_OUT;
00232 return(NULL);
00233 }
00234
00235 if (cuddIsConstant(N)) {
00236 if (node == DD_ZERO(dd) || node == Cudd_Not(DD_ONE(dd))) {
00237 values[0] = 0.0;
00238 } else {
00239 values[0] = 1.0;
00240 }
00241 } else {
00242 Nv = Cudd_NotCond(cuddT(N),N!=node);
00243 Nnv = Cudd_NotCond(cuddE(N),N!=node);
00244
00245 valuesT = ddCofMintermAux(dd, Nv, table);
00246 if (valuesT == NULL) return(NULL);
00247 valuesE = ddCofMintermAux(dd, Nnv, table);
00248 if (valuesE == NULL) return(NULL);
00249
00250 if (Cudd_IsConstant(Nv)) {
00251 localSizeT = 1;
00252 } else {
00253 localSizeT = size - cuddI(dd,Cudd_Regular(Nv)->index) + 1;
00254 }
00255 if (Cudd_IsConstant(Nnv)) {
00256 localSizeE = 1;
00257 } else {
00258 localSizeE = size - cuddI(dd,Cudd_Regular(Nnv)->index) + 1;
00259 }
00260 values[0] = valuesT[localSizeT - 1];
00261 for (i = 1; i < localSize; i++) {
00262 if (i >= cuddI(dd,Cudd_Regular(Nv)->index) - cuddI(dd,N->index)) {
00263 vT = valuesT[i - cuddI(dd,Cudd_Regular(Nv)->index) +
00264 cuddI(dd,N->index)];
00265 } else {
00266 vT = valuesT[localSizeT - 1];
00267 }
00268 if (i >= cuddI(dd,Cudd_Regular(Nnv)->index) - cuddI(dd,N->index)) {
00269 vE = valuesE[i - cuddI(dd,Cudd_Regular(Nnv)->index) +
00270 cuddI(dd,N->index)];
00271 } else {
00272 vE = valuesE[localSizeE - 1];
00273 }
00274 values[i] = (vT + vE) / 2.0;
00275 }
00276 if (Cudd_Regular(Nv)->ref == 1) FREE(valuesT);
00277 if (Cudd_Regular(Nnv)->ref == 1) FREE(valuesE);
00278 }
00279
00280 if (N->ref > 1) {
00281 if (st_add_direct(table, (char *) node, (char *) values) == ST_OUT_OF_MEM) {
00282 FREE(values);
00283 return(NULL);
00284 }
00285 #ifdef DD_STATS
00286 table_mem += localSize * sizeof(double) + sizeof(st_table_entry);
00287 #endif
00288 }
00289 return(values);
00290
00291 }
00292
