- Generated on Wed Oct 12 2011 00:34:49 for VIS by
1.7.3
|
VIS
|
00001 00035 #include "imgInt.h" 00036 00037 static char rcsid[] UNUSED = "$Id: imgTfmFwd.c,v 1.37 2005/04/22 19:45:46 jinh Exp $"; 00038 00039 /*---------------------------------------------------------------------------*/ 00040 /* Constant declarations */ 00041 /*---------------------------------------------------------------------------*/ 00042 00043 /*---------------------------------------------------------------------------*/ 00044 /* Type declarations */ 00045 /*---------------------------------------------------------------------------*/ 00046 00047 /*---------------------------------------------------------------------------*/ 00048 /* Structure declarations */ 00049 /*---------------------------------------------------------------------------*/ 00050 00051 /*---------------------------------------------------------------------------*/ 00052 /* Variable declarations */ 00053 /*---------------------------------------------------------------------------*/ 00054 00055 /*---------------------------------------------------------------------------*/ 00056 /* Macro declarations */ 00057 /*---------------------------------------------------------------------------*/ 00058 00061 /*---------------------------------------------------------------------------*/ 00062 /* Static function prototypes */ 00063 /*---------------------------------------------------------------------------*/ 00064 00065 static mdd_t * ImageByInputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint, mdd_t *from, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int splitMethod, int turnDepth, int depth); 00066 static mdd_t * ImageByStaticInputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, int turnDepth, int depth); 00067 static mdd_t * ImageByOutputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint, int depth); 00068 static int ImageDecomposeAndChooseSplitVar(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, int splitMethod, int split, int piSplitFlag, array_t *vectorArray, array_t *varArray, mdd_t **singles, array_t *relationArray, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube); 00069 static mdd_t * ImageFast2(ImgTfmInfo_t *info, array_t *vector); 00070 static int FindDecomposableVariable(ImgTfmInfo_t *info, array_t *vector); 00071 static int TfmCheckImageValidity(ImgTfmInfo_t *info, mdd_t *image); 00072 static void FindIntermediateSupport(array_t *vector, ImgComponent_t *comp, int nVars, int nGroups, int *stack, char *stackFlag, int *funcGroup, int *size, char *intermediateVarFlag, int *intermediateVarFuncMap); 00073 static void PrintVectorDecomposition(ImgTfmInfo_t *info, array_t *vectorArray, array_t *varArray); 00074 static int CheckIfValidSplitOrGetNew(ImgTfmInfo_t *info, int split, array_t *vector, array_t *relationArray, mdd_t *from); 00075 static int ChooseInputSplittingVariable(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, int splitMethod, int decompose, int piSplitFlag, int *varOccur); 00076 static int ChooseOutputSplittingVariable(ImgTfmInfo_t *info, array_t *vector, int splitMethod); 00077 00081 /*---------------------------------------------------------------------------*/ 00082 /* Definition of exported functions */ 00083 /*---------------------------------------------------------------------------*/ 00084 00085 00086 /*---------------------------------------------------------------------------*/ 00087 /* Definition of internal functions */ 00088 /*---------------------------------------------------------------------------*/ 00089 00090 00100 mdd_t * 00101 ImgTfmImage(ImgTfmInfo_t *info, mdd_t *from) 00102 { 00103 mdd_t *res, *r, *cube, *newFrom, *one; 00104 array_t *newVector, *depVector; 00105 int splitMethod, turnDepth; 00106 mdd_t *refResult; 00107 array_t *relationArray, *newRelationArray, *tmpRelationArray; 00108 int eliminateDepend; 00109 int partial, saveUseConstraint; 00110 long size1, size2; 00111 mdd_t *cofactorCube, *abstractCube; 00112 int i, maxDepth, size, nDependVars; 00113 00114 info->maxIntermediateSize = 0; 00115 if (info->eliminateDepend == 1 || 00116 (info->eliminateDepend == 2 && info->nPrevEliminatedFwd > 0)) { 00117 eliminateDepend = 1; 00118 } else 00119 eliminateDepend = 0; 00120 00121 saveUseConstraint = info->useConstraint; 00122 if (info->buildTR) { 00123 if (eliminateDepend == 0 && 00124 info->option->splitMethod == 3 && 00125 info->option->splitMaxDepth < 0 && 00126 info->option->buildPartialTR == FALSE && 00127 info->option->rangeComp == 0 && 00128 info->option->findEssential == FALSE) { 00129 r = ImgBddLinearAndSmooth(info->manager, from, 00130 info->fwdClusteredRelationArray, 00131 info->fwdArraySmoothVarBddArray, 00132 info->fwdSmoothVarCubeArray, 00133 info->option->verbosity); 00134 res = ImgSubstitute(r, info->functionData, Img_R2D_c); 00135 mdd_free(r); 00136 return(res); 00137 } 00138 relationArray = mdd_array_duplicate(info->fwdClusteredRelationArray); 00139 } else 00140 relationArray = NIL(array_t); 00141 if (info->useConstraint == 1 || 00142 (info->useConstraint == 2 && 00143 info->nImageComps == info->option->rangeTryThreshold)) { 00144 if (info->buildTR == 2) { 00145 newVector = NIL(array_t); 00146 cube = mdd_one(info->manager); 00147 if (eliminateDepend) { 00148 newFrom = ImgTrmEliminateDependVars(info->functionData, relationArray, 00149 from, NIL(mdd_t *), &nDependVars); 00150 if (nDependVars) { 00151 if (info->option->verbosity > 0) 00152 (void)fprintf(vis_stdout, "Eliminated %d vars.\n", nDependVars); 00153 info->averageFoundDependVars = (info->averageFoundDependVars * 00154 (float)info->nFoundDependVars + (float)nDependVars) / 00155 (float)(info->nFoundDependVars + 1); 00156 info->nFoundDependVars++; 00157 } 00158 00159 info->nPrevEliminatedFwd = nDependVars; 00160 } else 00161 newFrom = from; 00162 cofactorCube = NIL(mdd_t); 00163 abstractCube = NIL(mdd_t); 00164 } else { 00165 newVector = ImgVectorCopy(info, info->vector); 00166 cube = mdd_one(info->manager); 00167 if (eliminateDepend) { 00168 newFrom = ImgTfmEliminateDependVars(info, newVector, relationArray, 00169 from, NIL(array_t *), NIL(mdd_t *)); 00170 } else 00171 newFrom = from; 00172 if (info->option->delayedSplit && relationArray && info->buildTR != 2) { 00173 cofactorCube = mdd_one(info->manager); 00174 abstractCube = mdd_one(info->manager); 00175 } else { 00176 cofactorCube = NIL(mdd_t); 00177 abstractCube = NIL(mdd_t); 00178 } 00179 } 00180 } else { 00181 if (eliminateDepend) { 00182 depVector = ImgVectorCopy(info, info->vector); 00183 newFrom = ImgTfmEliminateDependVars(info, depVector, relationArray, from, 00184 NIL(array_t *), NIL(mdd_t *)); 00185 /* constrain delta w.r.t. from here */ 00186 if (info->option->delayedSplit && relationArray && info->buildTR != 2) { 00187 ImgVectorConstrain(info, depVector, newFrom, relationArray, 00188 &newVector, &cube, &newRelationArray, &cofactorCube, 00189 &abstractCube, FALSE); 00190 } else if (relationArray) { 00191 ImgVectorConstrain(info, depVector, newFrom, relationArray, 00192 &newVector, &cube, NIL(array_t *), &cofactorCube, 00193 &abstractCube, FALSE); 00194 newRelationArray = NIL(array_t); 00195 } else { 00196 ImgVectorConstrain(info, depVector, newFrom, NIL(array_t), 00197 &newVector, &cube, NIL(array_t *), NIL(mdd_t *), 00198 NIL(mdd_t *), FALSE); 00199 newRelationArray = NIL(array_t); 00200 cofactorCube = NIL(mdd_t); 00201 abstractCube = NIL(mdd_t); 00202 } 00203 00204 if (info->useConstraint == 2) { 00205 size1 = ImgVectorBddSize(depVector); 00206 size2 = ImgVectorBddSize(newVector); 00207 if (info->option->rangeCheckReorder) { 00208 bdd_reorder(info->manager); 00209 size1 = ImgVectorBddSize(depVector); 00210 size2 = ImgVectorBddSize(newVector); 00211 } 00212 if (size2 > size1 * info->option->rangeThreshold) { /* cancel */ 00213 if (info->option->verbosity) 00214 fprintf(vis_stdout, "** tfm info: canceled range computation.\n"); 00215 info->useConstraint = 1; 00216 ImgVectorFree(newVector); 00217 newVector = depVector; 00218 mdd_free(cube); 00219 cube = mdd_one(info->manager); 00220 if (newRelationArray && newRelationArray != relationArray) 00221 mdd_array_free(newRelationArray); 00222 if (cofactorCube) { 00223 mdd_free(cofactorCube); 00224 cofactorCube = mdd_one(info->manager); 00225 } 00226 if (abstractCube) { 00227 mdd_free(abstractCube); 00228 abstractCube = mdd_one(info->manager); 00229 } 00230 info->nImageComps++; 00231 } else { 00232 info->useConstraint = 0; 00233 info->nImageComps = 0; 00234 info->nRangeComps++; 00235 } 00236 } 00237 if (info->useConstraint == 0) 00238 ImgVectorFree(depVector); 00239 } else { 00240 newFrom = from; 00241 /* constrain delta w.r.t. from here */ 00242 if (info->option->delayedSplit && relationArray && info->buildTR != 2) { 00243 ImgVectorConstrain(info, info->vector, newFrom, relationArray, 00244 &newVector, &cube, &newRelationArray, &cofactorCube, 00245 &abstractCube, FALSE); 00246 if (info->option->debug) { 00247 refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t)); 00248 res = ImgImageByHybridWithStaticSplit(info, NIL(array_t), NIL(mdd_t), 00249 newRelationArray, 00250 cofactorCube, abstractCube); 00251 assert(mdd_equal(refResult, res)); 00252 mdd_free(refResult); 00253 mdd_free(res); 00254 } 00255 } else if (relationArray) { 00256 ImgVectorConstrain(info, info->vector, newFrom, relationArray, 00257 &newVector, &cube, NIL(array_t *), &cofactorCube, 00258 &abstractCube, FALSE); 00259 newRelationArray = NIL(array_t); 00260 } else { 00261 ImgVectorConstrain(info, info->vector, newFrom, NIL(array_t), 00262 &newVector, &cube, NIL(array_t *), NIL(mdd_t *), 00263 NIL(mdd_t *), FALSE); 00264 newRelationArray = NIL(array_t); 00265 cofactorCube = NIL(mdd_t); 00266 abstractCube = NIL(mdd_t); 00267 } 00268 00269 if (info->useConstraint == 2) { 00270 size1 = ImgVectorBddSize(info->vector); 00271 size2 = ImgVectorBddSize(newVector); 00272 if (info->option->rangeCheckReorder) { 00273 bdd_reorder(info->manager); 00274 size1 = ImgVectorBddSize(info->vector); 00275 size2 = ImgVectorBddSize(newVector); 00276 } 00277 if (size2 > size1 * info->option->rangeThreshold) { /* cancel */ 00278 if (info->option->verbosity) 00279 fprintf(vis_stdout, "** tfm info: canceled range computation.\n"); 00280 info->useConstraint = 1; 00281 ImgVectorFree(newVector); 00282 newVector = info->vector; 00283 mdd_free(cube); 00284 cube = mdd_one(info->manager); 00285 if (newRelationArray && newRelationArray != relationArray) 00286 mdd_array_free(newRelationArray); 00287 if (cofactorCube) { 00288 mdd_free(cofactorCube); 00289 cofactorCube = mdd_one(info->manager); 00290 } 00291 if (abstractCube) { 00292 mdd_free(abstractCube); 00293 abstractCube = mdd_one(info->manager); 00294 } 00295 info->nImageComps++; 00296 } else { 00297 info->useConstraint = 0; 00298 info->nImageComps = 0; 00299 info->nRangeComps++; 00300 } 00301 } 00302 } 00303 if (info->useConstraint == 0 && relationArray) { 00304 if (!newRelationArray) { 00305 if (bdd_is_tautology(cofactorCube, 1) && 00306 bdd_is_tautology(abstractCube, 1)) { 00307 newRelationArray = ImgGetConstrainedRelationArray(info, relationArray, 00308 newFrom); 00309 } else { 00310 tmpRelationArray = ImgGetConstrainedRelationArray(info, relationArray, 00311 newFrom); 00312 newRelationArray = ImgGetCofactoredAbstractedRelationArray( 00313 info->manager, tmpRelationArray, 00314 cofactorCube, abstractCube); 00315 if (info->option->debug) { 00316 array_t *tmpVector; 00317 00318 tmpVector = ImgGetConstrainedVector(info, info->vector, newFrom); 00319 if (info->option->checkEquivalence) { 00320 assert(ImgCheckEquivalence(info, tmpVector, tmpRelationArray, 00321 NIL(mdd_t), NIL(mdd_t), 0)); 00322 } 00323 refResult = ImgImageByHybrid(info, tmpVector, NIL(mdd_t)); 00324 ImgVectorFree(tmpVector); 00325 res = ImgImageByHybridWithStaticSplit(info, NIL(array_t), 00326 NIL(mdd_t), 00327 tmpRelationArray, 00328 NIL(mdd_t), NIL(mdd_t)); 00329 assert(mdd_equal(refResult, res)); 00330 mdd_free(refResult); 00331 mdd_free(res); 00332 } 00333 mdd_array_free(tmpRelationArray); 00334 } 00335 mdd_free(cofactorCube); 00336 cofactorCube = NIL(mdd_t); 00337 mdd_free(abstractCube); 00338 abstractCube = NIL(mdd_t); 00339 if (info->option->debug) { 00340 refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t)); 00341 res = ImgImageByHybridWithStaticSplit(info, NIL(array_t), NIL(mdd_t), 00342 newRelationArray, 00343 NIL(mdd_t), NIL(mdd_t)); 00344 assert(mdd_equal(refResult, res)); 00345 mdd_free(refResult); 00346 mdd_free(res); 00347 00348 if (info->nIntermediateVars) { 00349 mdd_t *tmp; 00350 00351 refResult = ImgImageByHybrid(info, info->vector, newFrom); 00352 res = ImgImageByHybridWithStaticSplit(info, NIL(array_t), newFrom, 00353 relationArray, 00354 NIL(mdd_t), NIL(mdd_t)); 00355 assert(mdd_equal(refResult, res)); 00356 mdd_free(res); 00357 tmp = ImgImageByHybrid(info, newVector, NIL(mdd_t)); 00358 res = mdd_and(tmp, cube, 1, 1); 00359 if (info->option->verbosity) { 00360 size = bdd_size(res); 00361 if (size > info->maxIntermediateSize) 00362 info->maxIntermediateSize = size; 00363 if (info->option->printBddSize) { 00364 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 00365 bdd_size(tmp), bdd_size(cube), size); 00366 } 00367 } 00368 mdd_free(tmp); 00369 assert(mdd_equal(refResult, res)); 00370 mdd_free(refResult); 00371 mdd_free(res); 00372 } 00373 } 00374 } 00375 if (relationArray != newRelationArray) { 00376 mdd_array_free(relationArray); 00377 relationArray = newRelationArray; 00378 } 00379 } 00380 if (info->option->checkEquivalence) { 00381 assert(ImgCheckEquivalence(info, newVector, newRelationArray, 00382 NIL(mdd_t), NIL(mdd_t), 0)); 00383 } 00384 } 00385 partial = 0; 00386 one = mdd_one(info->manager); 00387 splitMethod = info->option->splitMethod; 00388 if (splitMethod == 0) { 00389 r = ImageByInputSplit(info, newVector, one, newFrom, NIL(array_t), 00390 NIL(mdd_t), NIL(mdd_t), 0, 0, 0); 00391 } else if (splitMethod == 1) 00392 r = ImageByOutputSplit(info, newVector, one, 0); 00393 else { 00394 if (info->option->splitMethod == 0) 00395 turnDepth = info->nVars + 1; 00396 else 00397 turnDepth = info->option->turnDepth; 00398 if (turnDepth == 0) { 00399 if (splitMethod == 2) 00400 r = ImageByOutputSplit(info, newVector, one, 0); 00401 else { 00402 if (info->useConstraint && info->buildTR == 2) { 00403 if (info->buildPartialTR) { 00404 r = ImgImageByHybridWithStaticSplit(info, newVector, newFrom, 00405 relationArray, 00406 NIL(mdd_t), NIL(mdd_t)); 00407 } else { 00408 r = ImgImageByHybridWithStaticSplit(info, NIL(array_t), newFrom, 00409 relationArray, 00410 NIL(mdd_t), NIL(mdd_t)); 00411 } 00412 } else 00413 r = ImgImageByHybrid(info, newVector, newFrom); 00414 } 00415 } else if (splitMethod == 2) { 00416 r = ImageByInputSplit(info, newVector, one, newFrom, NIL(array_t), 00417 NIL(mdd_t), NIL(mdd_t), 00418 splitMethod, turnDepth, 0); 00419 } else { 00420 if (info->useConstraint) { 00421 if (info->buildTR) { 00422 if (info->buildTR == 2) { 00423 if (info->buildPartialTR) { 00424 r = ImageByStaticInputSplit(info, newVector, newFrom, 00425 relationArray, turnDepth, 0); 00426 partial = 1; 00427 } else { 00428 r = ImageByStaticInputSplit(info, NIL(array_t), newFrom, 00429 relationArray, turnDepth, 0); 00430 } 00431 } else if (info->option->delayedSplit) { 00432 r = ImageByInputSplit(info, newVector, one, newFrom, relationArray, 00433 cofactorCube, abstractCube, 00434 splitMethod, turnDepth, 0); 00435 } else { 00436 r = ImageByInputSplit(info, newVector, one, newFrom, relationArray, 00437 NIL(mdd_t), NIL(mdd_t), 00438 splitMethod, turnDepth, 0); 00439 } 00440 } else { 00441 r = ImageByInputSplit(info, newVector, one, newFrom, NIL(array_t), 00442 NIL(mdd_t), NIL(mdd_t), 00443 splitMethod, turnDepth, 0); 00444 } 00445 } else if (info->buildTR == 1 && info->option->delayedSplit) { 00446 r = ImageByInputSplit(info, newVector, one, NIL(mdd_t), relationArray, 00447 cofactorCube, abstractCube, 00448 splitMethod, turnDepth, 0); 00449 } else { 00450 r = ImageByInputSplit(info, newVector, one, NIL(mdd_t), relationArray, 00451 NIL(mdd_t), NIL(mdd_t), 00452 splitMethod, turnDepth, 0); 00453 } 00454 } 00455 } 00456 info->useConstraint = saveUseConstraint; 00457 if (relationArray && 00458 !(info->option->debug && (partial || info->buildTR == 2))) { 00459 mdd_array_free(relationArray); 00460 } 00461 if (info->imgCache && info->option->autoFlushCache == 1) 00462 ImgFlushCache(info->imgCache); 00463 mdd_free(one); 00464 if (cofactorCube) 00465 mdd_free(cofactorCube); 00466 if (abstractCube) 00467 mdd_free(abstractCube); 00468 if (newFrom && newFrom != from) 00469 mdd_free(newFrom); 00470 res = bdd_and(r, cube, 1, 1); 00471 if (info->option->verbosity) { 00472 size = bdd_size(res); 00473 if (size > info->maxIntermediateSize) 00474 info->maxIntermediateSize = size; 00475 if (info->option->printBddSize) { 00476 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 00477 bdd_size(r), bdd_size(cube), size); 00478 } 00479 } 00480 mdd_free(r); 00481 mdd_free(cube); 00482 if (newVector != info->vector) 00483 ImgVectorFree(newVector); 00484 00485 if (info->option->debug) { 00486 if (info->buildTR == 2) { 00487 refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from, 00488 relationArray, 00489 NIL(mdd_t), NIL(mdd_t)); 00490 mdd_array_free(relationArray); 00491 } else { 00492 if (partial) { 00493 refResult = ImgImageByHybrid(info, info->fullVector, from); 00494 assert(mdd_equal(refResult, res)); 00495 mdd_free(refResult); 00496 refResult = ImgImageByHybridWithStaticSplit(info, info->vector, from, 00497 relationArray, 00498 NIL(mdd_t), NIL(mdd_t)); 00499 mdd_array_free(relationArray); 00500 } else 00501 refResult = ImgImageByHybrid(info, info->vector, from); 00502 } 00503 assert(mdd_equal(refResult, res)); 00504 mdd_free(refResult); 00505 } 00506 if (info->option->findEssential) 00507 info->lastFoundEssentialDepth = info->foundEssentialDepth; 00508 if (info->option->printEssential == 2) { 00509 maxDepth = info->maxDepth < IMG_TF_MAX_PRINT_DEPTH ? 00510 info->maxDepth : IMG_TF_MAX_PRINT_DEPTH; 00511 fprintf(vis_stdout, "foundEssential:"); 00512 for (i = 0; i < maxDepth; i++) 00513 fprintf(vis_stdout, " [%d]%d", i, info->foundEssentials[i]); 00514 fprintf(vis_stdout, "\n"); 00515 } 00516 if (info->option->verbosity) { 00517 fprintf(vis_stdout, "** tfm info: max intermediate BDD size = %d\n", 00518 info->maxIntermediateSize); 00519 } 00520 if (info->option->debug) 00521 assert(TfmCheckImageValidity(info, res)); 00522 return(res); 00523 } 00524 00525 00535 mdd_t * 00536 ImgChooseTrSplitVar(ImgTfmInfo_t *info, array_t *vector, 00537 array_t *relationArray, int trSplitMethod, int piSplitFlag) 00538 { 00539 int i, j, nVars; 00540 ImgComponent_t *comp; 00541 char *support; 00542 int *varCost, bestCost = 0; 00543 int id, split; 00544 mdd_t *var, *relation; 00545 00546 nVars = info->nVars; 00547 varCost = ALLOC(int, nVars); 00548 memset(varCost, 0, sizeof(int) * nVars); 00549 00550 if (trSplitMethod == 0) { 00551 if (vector) { 00552 for (i = 0; i < array_n(vector); i++) { 00553 comp = array_fetch(ImgComponent_t *, vector, i); 00554 support = comp->support; 00555 for (j = 0; j < nVars; j++) { 00556 if (support[j]) 00557 varCost[j]++; 00558 } 00559 } 00560 } 00561 comp = ImgComponentAlloc(info); 00562 support = comp->support; 00563 for (i = 0; i < array_n(relationArray); i++) { 00564 relation = array_fetch(mdd_t *, relationArray, i); 00565 comp->func = relation; 00566 ImgSupportClear(info, comp->support); 00567 ImgComponentGetSupport(comp); 00568 for (j = 0; j < nVars; j++) { 00569 if (support[j]) 00570 varCost[j]++; 00571 } 00572 } 00573 comp->func = NIL(mdd_t); 00574 ImgComponentFree(comp); 00575 } else { 00576 for (i = 0; i < array_n(info->domainVarBddArray); i++) { 00577 var = array_fetch(mdd_t *, info->domainVarBddArray, i); 00578 id = (int)bdd_top_var_id(var); 00579 if (vector) { 00580 for (j = 0; j < array_n(vector); j++) { 00581 comp = array_fetch(ImgComponent_t *, vector, j); 00582 varCost[id] += bdd_estimate_cofactor(comp->func, var, 1); 00583 varCost[id] += bdd_estimate_cofactor(comp->func, var, 0); 00584 } 00585 } 00586 for (j = 0; j < array_n(relationArray); j++) { 00587 relation = array_fetch(mdd_t *, relationArray, j); 00588 varCost[id] += bdd_estimate_cofactor(relation, var, 1); 00589 varCost[id] += bdd_estimate_cofactor(relation, var, 0); 00590 } 00591 varCost[id] = IMG_TF_MAX_INT - varCost[id]; 00592 } 00593 } 00594 00595 split = -1; 00596 for (i = 0; i < nVars; i++) { 00597 if (varCost[i] == 0) 00598 continue; 00599 if (!piSplitFlag) { 00600 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) 00601 continue; 00602 } 00603 if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) 00604 continue; 00605 if (info->intermediateVarsTable && 00606 st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) { 00607 continue; 00608 } 00609 00610 if (split == -1 || varCost[i] > bestCost) { 00611 bestCost = varCost[i]; 00612 split = i; 00613 } 00614 } 00615 FREE(varCost); 00616 if (split == -1) 00617 return(NIL(mdd_t)); 00618 var = bdd_var_with_index(info->manager, split); 00619 return(var); 00620 } 00621 00622 00623 /*---------------------------------------------------------------------------*/ 00624 /* Definition of static functions */ 00625 /*---------------------------------------------------------------------------*/ 00626 00627 00637 static mdd_t * 00638 ImageByInputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint, 00639 mdd_t *from, array_t *relationArray, mdd_t *cofactorCube, 00640 mdd_t *abstractCube, int splitMethod, int turnDepth, 00641 int depth) 00642 { 00643 array_t *newVector, *tmpVector; 00644 mdd_t *new_, *resT, *resE, *res, *resPart, *resTmp; 00645 mdd_t *var, *varNot, *cube, *tmp, *func; 00646 int size, i, j, k, vectorSize; 00647 array_t *vectorArray, *varArray; 00648 int hit, turnFlag; 00649 int split, nGroups, cubeSize; 00650 mdd_t *refResult, *product; 00651 mdd_t *newFrom, *fromT, *fromE; 00652 ImgComponent_t *comp; 00653 array_t *relationArrayT, *relationArrayE, *partRelationArray; 00654 int constConstrain; 00655 int nRecur; 00656 array_t *newRelationArray, *tmpRelationArray, *abstractVars; 00657 mdd_t *cofactor, *abstract; 00658 mdd_t *newCofactorCube, *newAbstractCube; 00659 mdd_t *partCofactorCube, *partAbstractCube; 00660 mdd_t *cofactorCubeT, *cofactorCubeE; 00661 mdd_t *abstractCubeT, *abstractCubeE; 00662 mdd_t *essentialCube, *tmpRes; 00663 int findEssential; 00664 int foundEssentialDepth; 00665 int foundEssentialDepthT, foundEssentialDepthE; 00666 array_t *vectorT, *vectorE; 00667 mdd_t *andT, *andE, *one; 00668 float prevLambda; 00669 int prevTotal, prevVectorBddSize, prevVectorSize; 00670 int arraySize, nFuncs; 00671 00672 newRelationArray = NIL(array_t); 00673 00674 if (info->option->delayedSplit && relationArray) { 00675 ImgVectorConstrain(info, vector, constraint, relationArray, 00676 &newVector, &res, &newRelationArray, 00677 &cofactor, &abstract, TRUE); 00678 newCofactorCube = mdd_and(cofactorCube, cofactor, 1, 1); 00679 mdd_free(cofactor); 00680 newAbstractCube = mdd_and(abstractCube, abstract, 1, 1); 00681 mdd_free(abstract); 00682 if (info->option->debug) { 00683 refResult = ImgImageByHybrid(info, newVector, from); 00684 resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from, 00685 newRelationArray, 00686 newCofactorCube, 00687 newAbstractCube); 00688 assert(mdd_equal(refResult, resPart)); 00689 mdd_free(refResult); 00690 mdd_free(resPart); 00691 } 00692 } else { 00693 ImgVectorConstrain(info, vector, constraint, relationArray, 00694 &newVector, &res, &newRelationArray, 00695 NIL(mdd_t *), NIL(mdd_t *), TRUE); 00696 newCofactorCube = NIL(mdd_t); 00697 newAbstractCube = NIL(mdd_t); 00698 if (info->option->debug) { 00699 refResult = ImgImageByHybrid(info, newVector, from); 00700 resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from, 00701 newRelationArray, 00702 NIL(mdd_t), NIL(mdd_t)); 00703 assert(mdd_equal(refResult, resPart)); 00704 mdd_free(refResult); 00705 00706 refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from, 00707 relationArray, 00708 NIL(mdd_t), NIL(mdd_t)); 00709 resTmp = mdd_and(resPart, res, 1, 1); 00710 mdd_free(resPart); 00711 assert(mdd_equal(refResult, resTmp)); 00712 mdd_free(refResult); 00713 mdd_free(resTmp); 00714 } 00715 } 00716 00717 if (info->option->checkEquivalence && 00718 relationArray && !info->option->buildPartialTR) { 00719 assert(ImgCheckEquivalence(info, newVector, newRelationArray, 00720 newCofactorCube, newAbstractCube, 0)); 00721 } 00722 00723 if (from && info->option->findEssential) { 00724 if (info->option->findEssential == 1) 00725 findEssential = 1; 00726 else { 00727 if (depth >= info->lastFoundEssentialDepth) 00728 findEssential = 1; 00729 else 00730 findEssential = 0; 00731 } 00732 } else 00733 findEssential = 0; 00734 if (findEssential) { 00735 essentialCube = bdd_find_essential_cube(from); 00736 00737 if (!bdd_is_tautology(essentialCube, 1)) { 00738 info->averageFoundEssential = (info->averageFoundEssential * 00739 (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) / 00740 (float)(info->nFoundEssentials + 1); 00741 info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth * 00742 (float)info->nFoundEssentials + (float)depth) / 00743 (float)(info->nFoundEssentials + 1); 00744 if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth) 00745 info->topFoundEssentialDepth = depth; 00746 info->nFoundEssentials++; 00747 if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH) 00748 info->foundEssentials[depth]++; 00749 tmpVector = newVector; 00750 tmpRelationArray = newRelationArray; 00751 if (info->option->delayedSplit && relationArray) { 00752 ImgVectorMinimize(info, tmpVector, essentialCube, NIL(mdd_t), 00753 tmpRelationArray, &newVector, &tmpRes, 00754 &newRelationArray, &cofactor, &abstract); 00755 tmp = newCofactorCube; 00756 newCofactorCube = mdd_and(tmp, cofactor, 1, 1); 00757 mdd_free(tmp); 00758 mdd_free(cofactor); 00759 tmp = newAbstractCube; 00760 newAbstractCube = mdd_and(tmp, abstract, 1, 1); 00761 mdd_free(tmp); 00762 mdd_free(abstract); 00763 } else { 00764 ImgVectorMinimize(info, tmpVector, essentialCube, NIL(mdd_t), 00765 tmpRelationArray, &newVector, &tmpRes, 00766 &newRelationArray, NIL(mdd_t *), NIL(mdd_t *)); 00767 } 00768 tmp = res; 00769 res = mdd_and(tmp, tmpRes, 1, 1); 00770 mdd_free(tmp); 00771 ImgVectorFree(tmpVector); 00772 if (tmpRelationArray && tmpRelationArray != relationArray && 00773 tmpRelationArray != newRelationArray) 00774 mdd_array_free(tmpRelationArray); 00775 foundEssentialDepth = depth; 00776 } else 00777 foundEssentialDepth = info->option->maxEssentialDepth; 00778 mdd_free(essentialCube); 00779 foundEssentialDepthT = info->option->maxEssentialDepth; 00780 foundEssentialDepthE = info->option->maxEssentialDepth; 00781 } else { 00782 /* To remove compiler warnings */ 00783 foundEssentialDepth = -1; 00784 foundEssentialDepthT = -1; 00785 foundEssentialDepthE = -1; 00786 } 00787 00788 if (info->option->debug) { 00789 if (relationArray && from) { 00790 refResult = ImgImageByHybrid(info, newVector, from); 00791 resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from, 00792 newRelationArray, 00793 newCofactorCube, 00794 newAbstractCube); 00795 assert(mdd_equal(refResult, resPart)); 00796 mdd_free(refResult); 00797 mdd_free(resPart); 00798 } 00799 } 00800 00801 info->nRecursion++; 00802 arraySize = array_n(newVector); 00803 if (info->nIntermediateVars) 00804 nFuncs = ImgVectorFunctionSize(newVector); 00805 else 00806 nFuncs = arraySize; 00807 if (nFuncs <= 1) { 00808 if (info->useConstraint) { 00809 if (nFuncs == 1) { 00810 comp = array_fetch(ImgComponent_t *, newVector, 0); 00811 if (arraySize > 1) 00812 func = ImgGetComposedFunction(newVector); 00813 else 00814 func = comp->func; 00815 if (mdd_lequal(from, func, 1, 1)) { /* func | from = 1 */ 00816 tmp = res; 00817 res = mdd_and(tmp, comp->var, 1, 1); 00818 mdd_free(tmp); 00819 } else if (mdd_lequal(func, from, 1, 0)) { /* func | from = 0 */ 00820 tmp = res; 00821 res = mdd_and(tmp, comp->var, 1, 0); 00822 mdd_free(tmp); 00823 } 00824 if (arraySize > 1) 00825 mdd_free(func); 00826 } 00827 } 00828 if (relationArray && newRelationArray != relationArray) 00829 mdd_array_free(newRelationArray); 00830 if (newCofactorCube) 00831 mdd_free(newCofactorCube); 00832 if (newAbstractCube) 00833 mdd_free(newAbstractCube); 00834 ImgVectorFree(newVector); 00835 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 00836 (float)depth) / (float)(info->nLeaves + 1); 00837 if (depth > info->maxDepth) 00838 info->maxDepth = depth; 00839 info->nLeaves++; 00840 if (findEssential) 00841 info->foundEssentialDepth = foundEssentialDepth; 00842 if (info->option->debug) 00843 assert(TfmCheckImageValidity(info, res)); 00844 return(res); 00845 } 00846 00847 turnFlag = 0; 00848 if (splitMethod == 3 && turnDepth == -1) { 00849 if (depth < info->option->splitMinDepth) { 00850 info->nSplits++; 00851 turnFlag = 0; 00852 } else if (depth > info->option->splitMaxDepth) { 00853 info->nConjoins++; 00854 turnFlag = 1; 00855 } else { 00856 turnFlag = ImgDecideSplitOrConjoin(info, newVector, from, 0, 00857 newRelationArray, newCofactorCube, 00858 newAbstractCube, 0, depth); 00859 } 00860 } else { 00861 if (splitMethod != 0) { 00862 if (depth == turnDepth) 00863 turnFlag = 1; 00864 } 00865 } 00866 if (turnFlag || nFuncs == 2) { 00867 hit = 1; 00868 if (!info->imgCache || 00869 !(resPart = ImgCacheLookupTable(info, info->imgCache, newVector, 00870 from))) { 00871 hit = 0; 00872 if (nFuncs == 2) { 00873 if (info->useConstraint) { 00874 ImgVectorConstrain(info, newVector, from, NIL(array_t), 00875 &tmpVector, &resTmp, NIL(array_t *), 00876 NIL(mdd_t *), NIL(mdd_t *), FALSE); 00877 if (array_n(tmpVector) <= 1) 00878 resPart = resTmp; 00879 else { 00880 mdd_free(resTmp); 00881 resPart = ImageFast2(info, tmpVector); 00882 } 00883 ImgVectorFree(tmpVector); 00884 } else 00885 resPart = ImageFast2(info, newVector); 00886 } else if (splitMethod == 2) { 00887 if (info->useConstraint) { 00888 ImgVectorConstrain(info, newVector, from, NIL(array_t), 00889 &tmpVector, &resTmp, NIL(array_t *), 00890 NIL(mdd_t *), NIL(mdd_t *), FALSE); 00891 if (array_n(tmpVector) <= 1) 00892 resPart = resTmp; 00893 else if (array_n(tmpVector) == 2) { 00894 mdd_free(resTmp); 00895 resPart = ImageFast2(info, tmpVector); 00896 } else { 00897 tmp = mdd_one(info->manager); 00898 resPart = ImageByOutputSplit(info, tmpVector, tmp, depth + 1); 00899 mdd_free(tmp); 00900 tmp = resPart; 00901 resPart = mdd_and(tmp, resTmp, 1, 1); 00902 mdd_free(tmp); 00903 mdd_free(resTmp); 00904 } 00905 ImgVectorFree(tmpVector); 00906 } else { 00907 tmp = mdd_one(info->manager); 00908 resPart = ImageByOutputSplit(info, newVector, tmp, depth + 1); 00909 mdd_free(tmp); 00910 } 00911 } else { 00912 if (relationArray) { 00913 resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from, 00914 newRelationArray, 00915 newCofactorCube, 00916 newAbstractCube); 00917 } else 00918 resPart = ImgImageByHybrid(info, newVector, from); 00919 } 00920 if (info->imgCache) { 00921 if (from) { 00922 ImgCacheInsertTable(info->imgCache, newVector, mdd_dup(from), 00923 resPart); 00924 } else 00925 ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t), resPart); 00926 } 00927 } 00928 00929 if (relationArray && newRelationArray != relationArray) 00930 mdd_array_free(newRelationArray); 00931 if (newCofactorCube) 00932 mdd_free(newCofactorCube); 00933 if (newAbstractCube) 00934 mdd_free(newAbstractCube); 00935 00936 if (info->option->debug) { 00937 refResult = ImgImageByHybrid(info, newVector, from); 00938 assert(mdd_equal(refResult, resPart)); 00939 mdd_free(refResult); 00940 } 00941 00942 new_ = mdd_and(res, resPart, 1, 1); 00943 if (info->option->verbosity) { 00944 size = bdd_size(new_); 00945 if (size > info->maxIntermediateSize) 00946 info->maxIntermediateSize = size; 00947 if (info->option->printBddSize) { 00948 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 00949 bdd_size(res), bdd_size(resPart), size); 00950 } 00951 } 00952 mdd_free(res); 00953 res = new_; 00954 if (!info->imgCache || hit) { 00955 mdd_free(resPart); 00956 ImgVectorFree(newVector); 00957 } 00958 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 00959 (float)depth) / (float)(info->nLeaves + 1); 00960 if (depth > info->maxDepth) 00961 info->maxDepth = depth; 00962 info->nLeaves++; 00963 if (turnFlag) 00964 info->nTurns++; 00965 if (findEssential) 00966 info->foundEssentialDepth = foundEssentialDepth; 00967 if (info->option->debug) 00968 assert(TfmCheckImageValidity(info, res)); 00969 return(res); 00970 } 00971 00972 if (info->imgCache) { 00973 resPart = ImgCacheLookupTable(info, info->imgCache, newVector, from); 00974 if (resPart) { 00975 if (info->option->debug) { 00976 refResult = ImgImageByHybrid(info, newVector, from); 00977 assert(mdd_equal(refResult, resPart)); 00978 mdd_free(refResult); 00979 } 00980 new_ = mdd_and(res, resPart, 1, 1); 00981 if (info->option->verbosity) { 00982 size = bdd_size(new_); 00983 if (size > info->maxIntermediateSize) 00984 info->maxIntermediateSize = size; 00985 if (info->option->printBddSize) { 00986 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 00987 bdd_size(res), bdd_size(resPart), size); 00988 } 00989 } 00990 mdd_free(res); 00991 mdd_free(resPart); 00992 res = new_; 00993 ImgVectorFree(newVector); 00994 if (relationArray && newRelationArray != relationArray) 00995 mdd_array_free(newRelationArray); 00996 if (newCofactorCube) 00997 mdd_free(newCofactorCube); 00998 if (newAbstractCube) 00999 mdd_free(newAbstractCube); 01000 if (findEssential) 01001 info->foundEssentialDepth = foundEssentialDepth; 01002 if (info->option->debug) 01003 assert(TfmCheckImageValidity(info, res)); 01004 return(res); 01005 } 01006 } 01007 01008 if (info->option->splitCubeFunc) { 01009 split = -1; 01010 cubeSize = 0; 01011 for (i = 0; i < array_n(newVector); i++) { 01012 comp = array_fetch(ImgComponent_t *, newVector, i); 01013 if (bdd_is_cube(comp->func)) { 01014 if (split == -1 || info->option->splitCubeFunc == 1 || 01015 bdd_size(comp->func) > cubeSize) { 01016 split = i; 01017 cubeSize = bdd_size(comp->func); 01018 break; 01019 } 01020 } 01021 } 01022 if (split != -1) { 01023 comp = array_fetch(ImgComponent_t *, newVector, split); 01024 info->nCubeSplits++; 01025 if (info->option->delayedSplit && relationArray) { 01026 ImgVectorConstrain(info, newVector, comp->func, newRelationArray, 01027 &vectorT, &andT, &relationArrayT, 01028 &cofactor, &abstract, FALSE); 01029 cofactorCubeT = mdd_and(newCofactorCube, cofactor, 1, 1); 01030 mdd_free(cofactor); 01031 abstractCubeT = mdd_and(newAbstractCube, abstract, 1, 1); 01032 mdd_free(abstract); 01033 } else { 01034 ImgVectorConstrain(info, newVector, comp->func, newRelationArray, 01035 &vectorT, &andT, &relationArrayT, 01036 NIL(mdd_t *), NIL(mdd_t *), FALSE); 01037 cofactorCubeT = NIL(mdd_t); 01038 abstractCubeT = NIL(mdd_t); 01039 } 01040 if (from) 01041 newFrom = bdd_cofactor(from, comp->func); 01042 else 01043 newFrom = from; 01044 if (info->option->checkEquivalence && 01045 relationArray && !info->option->buildPartialTR) { 01046 assert(ImgCheckEquivalence(info, vectorT, relationArrayT, 01047 cofactorCubeT, abstractCubeT, 0)); 01048 } 01049 01050 one = mdd_one(info->manager); 01051 if (newFrom && bdd_is_tautology(newFrom, 0)) 01052 resT = mdd_zero(info->manager); 01053 else { 01054 prevLambda = info->prevLambda; 01055 prevTotal = info->prevTotal; 01056 prevVectorBddSize = info->prevVectorBddSize; 01057 prevVectorSize = info->prevVectorSize; 01058 resT = ImageByInputSplit(info, vectorT, one, newFrom, 01059 relationArrayT, cofactorCubeT, abstractCubeT, 01060 splitMethod, turnDepth, depth + 1); 01061 info->prevLambda = prevLambda; 01062 info->prevTotal = prevTotal; 01063 info->prevVectorBddSize = prevVectorBddSize; 01064 info->prevVectorSize = prevVectorSize; 01065 } 01066 ImgVectorFree(vectorT); 01067 if (newFrom) 01068 mdd_free(newFrom); 01069 if (!bdd_is_tautology(andT, 1)) { 01070 tmp = resT; 01071 resT = mdd_and(tmp, andT, 1, 1); 01072 mdd_free(tmp); 01073 } 01074 if (findEssential) 01075 foundEssentialDepthT = info->foundEssentialDepth; 01076 if (relationArrayT && relationArrayT != newRelationArray) 01077 mdd_array_free(relationArrayT); 01078 if (cofactorCubeT && cofactorCubeT != newCofactorCube) 01079 mdd_free(cofactorCubeT); 01080 if (abstractCubeT && abstractCubeT != newAbstractCube) 01081 mdd_free(abstractCubeT); 01082 01083 tmp = mdd_not(comp->func); 01084 if (info->option->delayedSplit && relationArray) { 01085 ImgVectorConstrain(info, newVector, tmp, newRelationArray, 01086 &vectorE, &andE, &relationArrayE, 01087 &cofactor, &abstract, FALSE); 01088 cofactorCubeE = mdd_and(newCofactorCube, cofactor, 1, 1); 01089 mdd_free(cofactor); 01090 abstractCubeE = mdd_and(newAbstractCube, abstract, 1, 1); 01091 mdd_free(abstract); 01092 } else { 01093 ImgVectorConstrain(info, newVector, tmp, newRelationArray, 01094 &vectorE, &andE, &relationArrayE, 01095 NIL(mdd_t *), NIL(mdd_t *), FALSE); 01096 cofactorCubeE = NIL(mdd_t); 01097 abstractCubeE = NIL(mdd_t); 01098 } 01099 if (from) 01100 newFrom = bdd_cofactor(from, tmp); 01101 else 01102 newFrom = from; 01103 mdd_free(tmp); 01104 if (relationArray && newRelationArray != relationArray) 01105 mdd_array_free(newRelationArray); 01106 if (newCofactorCube) 01107 mdd_free(newCofactorCube); 01108 if (newAbstractCube) 01109 mdd_free(newAbstractCube); 01110 if (info->option->checkEquivalence && 01111 relationArray && !info->option->buildPartialTR) { 01112 assert(ImgCheckEquivalence(info, vectorE, relationArrayE, 01113 cofactorCubeE, abstractCubeE, 0)); 01114 } 01115 01116 if (newFrom && bdd_is_tautology(newFrom, 0)) 01117 resE = mdd_zero(info->manager); 01118 else { 01119 resE = ImageByInputSplit(info, vectorE, one, newFrom, 01120 relationArrayE, cofactorCubeE, abstractCubeE, 01121 splitMethod, turnDepth, depth + 1); 01122 } 01123 ImgVectorFree(vectorE); 01124 if (newFrom) 01125 mdd_free(newFrom); 01126 if (!bdd_is_tautology(andE, 1)) { 01127 tmp = resE; 01128 resE = mdd_and(tmp, andE, 1, 1); 01129 mdd_free(tmp); 01130 } 01131 if (findEssential) 01132 foundEssentialDepthE = info->foundEssentialDepth; 01133 if (relationArrayE && relationArrayE != newRelationArray) 01134 mdd_array_free(relationArrayE); 01135 if (cofactorCubeE && cofactorCubeE != newCofactorCube) 01136 mdd_free(cofactorCubeE); 01137 if (abstractCubeE && abstractCubeE != newAbstractCube) 01138 mdd_free(abstractCubeE); 01139 01140 resPart = bdd_ite(comp->var, resT, resE, 1, 1, 1); 01141 if (info->option->verbosity) { 01142 size = bdd_size(resPart); 01143 if (size > info->maxIntermediateSize) 01144 info->maxIntermediateSize = size; 01145 if (info->option->printBddSize) { 01146 fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n", 01147 bdd_size(resT), bdd_size(resE), size); 01148 } 01149 } 01150 mdd_free(one); 01151 01152 if (info->imgCache) 01153 ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t), resPart); 01154 01155 if (info->option->debug) { 01156 refResult = ImgImageByHybrid(info, newVector, from); 01157 assert(mdd_equal(refResult, resPart)); 01158 mdd_free(refResult); 01159 } 01160 01161 new_ = mdd_and(res, resPart, 1, 1); 01162 if (info->option->verbosity) { 01163 size = bdd_size(new_); 01164 if (size > info->maxIntermediateSize) 01165 info->maxIntermediateSize = size; 01166 if (info->option->printBddSize) { 01167 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 01168 bdd_size(res), bdd_size(resPart), size); 01169 } 01170 } 01171 mdd_free(res); 01172 res = new_; 01173 01174 if (info->option->debug) { 01175 refResult = ImgImageByHybrid(info, newVector, from); 01176 assert(mdd_equal(refResult, resPart)); 01177 mdd_free(refResult); 01178 } 01179 01180 if (!info->imgCache) { 01181 mdd_free(resPart); 01182 ImgVectorFree(newVector); 01183 } 01184 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 01185 (float)depth) / (float)(info->nLeaves + 1); 01186 if (depth > info->maxDepth) 01187 info->maxDepth = depth; 01188 info->nLeaves++; 01189 if (turnFlag) 01190 info->nTurns++; 01191 if (findEssential) { 01192 if (foundEssentialDepth == info->option->maxEssentialDepth) { 01193 if (foundEssentialDepthT < foundEssentialDepthE) 01194 foundEssentialDepth = foundEssentialDepthT; 01195 else 01196 foundEssentialDepth = foundEssentialDepthE; 01197 } 01198 info->foundEssentialDepth = foundEssentialDepth; 01199 } 01200 if (info->option->debug) 01201 assert(TfmCheckImageValidity(info, res)); 01202 return(res); 01203 } 01204 } 01205 01206 /* compute disconnected component and best variable selection */ 01207 vectorArray = array_alloc(array_t *, 0); 01208 varArray = array_alloc(int, 0); 01209 if (info->option->delayedSplit && relationArray) { 01210 nGroups = ImageDecomposeAndChooseSplitVar(info, newVector, from, 0, 01211 info->option->inputSplit, 01212 info->option->piSplitFlag, 01213 vectorArray, varArray, &product, 01214 newRelationArray, &tmpRelationArray, 01215 &cofactor, &abstract); 01216 } else { 01217 nGroups = ImageDecomposeAndChooseSplitVar(info, newVector, from, 0, 01218 info->option->inputSplit, 01219 info->option->piSplitFlag, 01220 vectorArray, varArray, &product, 01221 newRelationArray, &tmpRelationArray, 01222 NIL(mdd_t *), NIL(mdd_t *)); 01223 cofactor = NIL(mdd_t); 01224 abstract = NIL(mdd_t); 01225 01226 if (info->option->debug && nGroups >= 1) { 01227 if (info->option->verbosity > 1) { 01228 ImgPrintVectorDependency(info, newVector, info->option->verbosity); 01229 PrintVectorDecomposition(info, vectorArray, varArray); 01230 } 01231 01232 refResult = ImgImageByHybrid(info, newVector, from); 01233 resPart = mdd_dup(product); 01234 for (i = 0; i < array_n(vectorArray); i++) { 01235 vector = array_fetch(array_t *, vectorArray, i); 01236 resTmp = ImgImageByHybrid(info, vector, from); 01237 tmp = resPart; 01238 resPart = mdd_and(tmp, resTmp, 1, 1); 01239 mdd_free(tmp); 01240 mdd_free(resTmp); 01241 01242 if (arraySize > nFuncs) { 01243 split = array_fetch(int, varArray, i); 01244 assert(!st_is_member(info->intermediateVarsTable, 01245 (char *)(long)split)); 01246 } 01247 } 01248 assert(mdd_equal(refResult, resPart)); 01249 mdd_free(refResult); 01250 mdd_free(resPart); 01251 } 01252 } 01253 vectorSize = array_n(newVector); 01254 if ((!info->imgCache || nGroups <= 1) && !info->option->debug) 01255 ImgVectorFree(newVector); 01256 if (newRelationArray) { 01257 if (newRelationArray != relationArray && 01258 tmpRelationArray != newRelationArray) { 01259 mdd_array_free(newRelationArray); 01260 } 01261 newRelationArray = tmpRelationArray; 01262 } 01263 if (nGroups == 0) { 01264 if (relationArray && newRelationArray != relationArray) 01265 mdd_array_free(newRelationArray); 01266 if (newCofactorCube) 01267 mdd_free(newCofactorCube); 01268 if (newAbstractCube) 01269 mdd_free(newAbstractCube); 01270 if (cofactor) 01271 mdd_free(cofactor); 01272 if (abstract) 01273 mdd_free(abstract); 01274 01275 array_free(vectorArray); 01276 array_free(varArray); 01277 01278 if (info->option->debug) { 01279 refResult = ImgImageByHybrid(info, newVector, from); 01280 assert(mdd_equal(refResult, product)); 01281 mdd_free(refResult); 01282 ImgVectorFree(newVector); 01283 } 01284 01285 new_ = mdd_and(res, product, 1, 1); 01286 if (info->option->verbosity) { 01287 size = bdd_size(new_); 01288 if (size > info->maxIntermediateSize) 01289 info->maxIntermediateSize = size; 01290 if (info->option->printBddSize) { 01291 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 01292 bdd_size(res), bdd_size(product), size); 01293 } 01294 } 01295 mdd_free(res); 01296 mdd_free(product); 01297 res = new_; 01298 01299 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 01300 (float)depth) / (float)(info->nLeaves + 1); 01301 if (depth > info->maxDepth) 01302 info->maxDepth = depth; 01303 info->nLeaves++; 01304 if (findEssential) 01305 info->foundEssentialDepth = foundEssentialDepth; 01306 if (info->option->debug) 01307 assert(TfmCheckImageValidity(info, res)); 01308 return(res); 01309 } 01310 01311 if (info->option->delayedSplit && relationArray) { 01312 tmp = newCofactorCube; 01313 newCofactorCube = mdd_and(tmp, cofactor, 1, 1); 01314 mdd_free(tmp); 01315 mdd_free(cofactor); 01316 tmp = newAbstractCube; 01317 newAbstractCube = mdd_and(tmp, abstract, 1, 1); 01318 mdd_free(tmp); 01319 mdd_free(abstract); 01320 } 01321 01322 if (nGroups > 1) { 01323 if (info->nDecomps == 0 || depth < info->topDecomp) 01324 info->topDecomp = depth; 01325 if (info->nDecomps == 0 || vectorSize > info->maxDecomp) 01326 info->maxDecomp = vectorSize; 01327 info->averageDecomp = (info->averageDecomp * (float)info->nDecomps + 01328 (float)nGroups) / (float)(info->nDecomps + 1); 01329 info->nDecomps++; 01330 } 01331 01332 if (relationArray && nGroups > 1) { 01333 abstractVars = array_alloc(mdd_t *, 0); 01334 for (i = 0; i < array_n(vectorArray); i++) { 01335 vector = array_fetch(array_t *, vectorArray, i); 01336 cube = mdd_one(info->manager); 01337 for (j = 0; j < nGroups; j++) { 01338 if (j == i) 01339 continue; 01340 tmpVector = array_fetch(array_t *, vectorArray, j); 01341 for (k = 0; k < array_n(tmpVector); k++) { 01342 comp = array_fetch(ImgComponent_t *, tmpVector, k); 01343 tmp = cube; 01344 cube = mdd_and(cube, comp->var, 1, 1); 01345 mdd_free(tmp); 01346 } 01347 } 01348 tmp = ImgSubstitute(cube, info->functionData, Img_D2R_c); 01349 mdd_free(cube); 01350 array_insert_last(mdd_t *, abstractVars, tmp); 01351 } 01352 } else 01353 abstractVars = NIL(array_t); 01354 for (i = 0; i < array_n(vectorArray); i++) { 01355 vector = array_fetch(array_t *, vectorArray, i); 01356 if (from) 01357 newFrom = mdd_dup(from); 01358 else 01359 newFrom = from; 01360 01361 if (relationArray) { 01362 if (nGroups == 1) { 01363 partRelationArray = newRelationArray; 01364 if (info->option->delayedSplit) { 01365 partCofactorCube = newCofactorCube; 01366 partAbstractCube = newAbstractCube; 01367 } else { 01368 partCofactorCube = NIL(mdd_t); 01369 partAbstractCube = NIL(mdd_t); 01370 } 01371 } else { 01372 cube = array_fetch(mdd_t *, abstractVars, i); 01373 if (info->option->delayedSplit) { 01374 partRelationArray = newRelationArray; 01375 partCofactorCube = mdd_dup(newCofactorCube); 01376 partAbstractCube = mdd_and(newAbstractCube, cube, 1, 1); 01377 } else { 01378 partRelationArray = ImgGetAbstractedRelationArray(info->manager, 01379 newRelationArray, 01380 cube); 01381 mdd_free(cube); 01382 partCofactorCube = NIL(mdd_t); 01383 partAbstractCube = NIL(mdd_t); 01384 } 01385 } 01386 if (info->option->debug) { 01387 refResult = ImgImageByHybrid(info, vector, from); 01388 resPart = ImgImageByHybridWithStaticSplit(info, NIL(array_t), from, 01389 partRelationArray, 01390 partCofactorCube, 01391 partAbstractCube); 01392 assert(mdd_equal(refResult, resPart)); 01393 mdd_free(refResult); 01394 mdd_free(resPart); 01395 } 01396 } else { 01397 partRelationArray = newRelationArray; 01398 partCofactorCube = NIL(mdd_t); 01399 partAbstractCube = NIL(mdd_t); 01400 } 01401 hit = 1; 01402 if (!info->imgCache || nGroups == 1 || 01403 !(resPart = ImgCacheLookupTable(info, info->imgCache, vector, 01404 newFrom))) { 01405 hit = 0; 01406 if (arraySize > nFuncs) 01407 size = ImgVectorFunctionSize(vector); 01408 else 01409 size = array_n(vector); 01410 if (size == 1) { 01411 comp = array_fetch(ImgComponent_t *, vector, 0); 01412 if (array_n(vector) > 1) 01413 func = ImgGetComposedFunction(vector); 01414 else 01415 func = comp->func; 01416 if (info->useConstraint) { 01417 constConstrain = ImgConstConstrain(func, newFrom); 01418 if (constConstrain == 1) 01419 resPart = mdd_dup(comp->var); 01420 else if (constConstrain == 0) 01421 resPart = mdd_not(comp->var); 01422 else 01423 resPart = mdd_one(info->manager); 01424 } else { 01425 if (bdd_is_tautology(func, 1)) 01426 resPart = mdd_dup(comp->var); 01427 else if (bdd_is_tautology(func, 0)) 01428 resPart = mdd_not(comp->var); 01429 else 01430 resPart = mdd_one(info->manager); 01431 } 01432 if (array_n(vector) > 1) 01433 mdd_free(func); 01434 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 01435 (float)depth) / (float)(info->nLeaves + 1); 01436 if (depth > info->maxDepth) 01437 info->maxDepth = depth; 01438 info->nLeaves++; 01439 } else if (size == 2) { 01440 if (info->useConstraint) { 01441 ImgVectorConstrain(info, vector, newFrom, NIL(array_t), 01442 &newVector, &resTmp, NIL(array_t *), 01443 NIL(mdd_t *), NIL(mdd_t *), FALSE); 01444 if (array_n(newVector) <= 1) 01445 resPart = resTmp; 01446 else { 01447 mdd_free(resTmp); 01448 resPart = ImageFast2(info, newVector); 01449 } 01450 ImgVectorFree(newVector); 01451 } else 01452 resPart = ImageFast2(info, vector); 01453 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 01454 (float)depth) / (float)(info->nLeaves + 1); 01455 if (depth > info->maxDepth) 01456 info->maxDepth = depth; 01457 info->nLeaves++; 01458 } else { 01459 nRecur = 0; 01460 split = array_fetch(int, varArray, i); 01461 if (partRelationArray && info->imgKeepPiInTr == FALSE) { 01462 if (st_lookup(info->quantifyVarsTable, (char *)(long)split, 01463 NIL(char *))) { 01464 int newSplit; 01465 01466 /* checks the splitting is valid */ 01467 newSplit = CheckIfValidSplitOrGetNew(info, split, vector, 01468 partRelationArray, from); 01469 if (newSplit == -1) { 01470 resPart = ImgImageByHybrid(info, vector, from); 01471 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 01472 (float)depth) / (float)(info->nLeaves + 1); 01473 if (depth > info->maxDepth) 01474 info->maxDepth = depth; 01475 info->nLeaves++; 01476 info->nTurns++; 01477 goto cache; 01478 } 01479 split = newSplit; 01480 } 01481 } 01482 var = bdd_var_with_index(info->manager, split); 01483 if (newFrom) 01484 fromT = bdd_cofactor(newFrom, var); 01485 else 01486 fromT = NIL(mdd_t); 01487 if (partRelationArray) { 01488 if (info->option->delayedSplit) { 01489 relationArrayT = partRelationArray; 01490 cofactorCubeT = mdd_and(partCofactorCube, var, 1, 1); 01491 } else { 01492 relationArrayT = ImgGetCofactoredRelationArray(partRelationArray, 01493 var); 01494 cofactorCubeT = partCofactorCube; 01495 } 01496 } else { 01497 relationArrayT = NIL(array_t); 01498 cofactorCubeT = NIL(mdd_t); 01499 } 01500 if (!fromT || !bdd_is_tautology(fromT, 0)) { 01501 prevLambda = info->prevLambda; 01502 prevTotal = info->prevTotal; 01503 prevVectorBddSize = info->prevVectorBddSize; 01504 prevVectorSize = info->prevVectorSize; 01505 resT = ImageByInputSplit(info, vector, var, fromT, 01506 relationArrayT, cofactorCubeT, partAbstractCube, 01507 splitMethod, turnDepth, depth + 1); 01508 if (info->option->debug) { 01509 refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t), 01510 fromT, relationArrayT, 01511 cofactorCubeT, 01512 partAbstractCube); 01513 assert(mdd_equal(refResult, resT)); 01514 mdd_free(refResult); 01515 } 01516 info->prevLambda = prevLambda; 01517 info->prevTotal = prevTotal; 01518 info->prevVectorBddSize = prevVectorBddSize; 01519 info->prevVectorSize = prevVectorSize; 01520 if (findEssential) 01521 foundEssentialDepthT = info->foundEssentialDepth; 01522 nRecur++; 01523 } else 01524 resT = mdd_zero(info->manager); 01525 if (fromT) 01526 mdd_free(fromT); 01527 if (relationArrayT && relationArrayT != partRelationArray) 01528 mdd_array_free(relationArrayT); 01529 if (cofactorCubeT && cofactorCubeT != partCofactorCube) 01530 mdd_free(cofactorCubeT); 01531 01532 if (bdd_is_tautology(resT, 1)) { 01533 mdd_free(var); 01534 resPart = resT; 01535 info->nEmptySubImage++; 01536 } else { 01537 varNot = mdd_not(var); 01538 mdd_free(var); 01539 if (newFrom) 01540 fromE = bdd_cofactor(newFrom, varNot); 01541 else 01542 fromE = NIL(mdd_t); 01543 if (partRelationArray) { 01544 if (info->option->delayedSplit) { 01545 relationArrayE = partRelationArray; 01546 cofactorCubeE = mdd_and(partCofactorCube, varNot, 1, 1); 01547 } else { 01548 relationArrayE = ImgGetCofactoredRelationArray(partRelationArray, 01549 varNot); 01550 cofactorCubeE = partCofactorCube; 01551 } 01552 } else { 01553 relationArrayE = NIL(array_t); 01554 cofactorCubeE = NIL(mdd_t); 01555 } 01556 if (!fromE || !bdd_is_tautology(fromE, 0)) { 01557 resE = ImageByInputSplit(info, vector, varNot, fromE, 01558 relationArrayE, cofactorCubeE, partAbstractCube, 01559 splitMethod, turnDepth, depth + 1); 01560 if (info->option->debug) { 01561 refResult = ImgImageByHybridWithStaticSplit(info, NIL(array_t), 01562 fromE, relationArrayE, 01563 cofactorCubeE, 01564 partAbstractCube); 01565 assert(mdd_equal(refResult, resE)); 01566 mdd_free(refResult); 01567 } 01568 if (findEssential) 01569 foundEssentialDepthE = info->foundEssentialDepth; 01570 nRecur++; 01571 } else 01572 resE = mdd_zero(info->manager); 01573 mdd_free(varNot); 01574 if (fromE) 01575 mdd_free(fromE); 01576 if (relationArrayE && relationArrayE != partRelationArray) 01577 mdd_array_free(relationArrayE); 01578 if (cofactorCubeE && cofactorCubeE != partCofactorCube) 01579 mdd_free(cofactorCubeE); 01580 01581 resPart = mdd_or(resT, resE, 1, 1); 01582 if (info->option->debug) { 01583 refResult = ImgImageByHybrid(info, vector, from); 01584 assert(mdd_equal(refResult, resPart)); 01585 mdd_free(refResult); 01586 } 01587 if (info->option->verbosity) { 01588 size = bdd_size(resPart); 01589 if (size > info->maxIntermediateSize) 01590 info->maxIntermediateSize = size; 01591 if (info->option->printBddSize) { 01592 fprintf(vis_stdout, "** tfm info: bdd_or(%d,%d) = %d\n", 01593 bdd_size(resT), bdd_size(resE), size); 01594 } 01595 } 01596 01597 mdd_free(resT); 01598 mdd_free(resE); 01599 } 01600 if (nRecur == 0) { 01601 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 01602 (float)depth) / (float)(info->nLeaves + 1); 01603 if (depth > info->maxDepth) 01604 info->maxDepth = depth; 01605 info->nLeaves++; 01606 } 01607 } 01608 cache: 01609 if (info->imgCache) { 01610 ImgCacheInsertTable(info->imgCache, vector, newFrom, resPart); 01611 if (info->option->debug) { 01612 refResult = ImgImageByHybrid(info, vector, newFrom); 01613 assert(mdd_equal(refResult, resPart)); 01614 mdd_free(refResult); 01615 } 01616 } 01617 } 01618 if (!info->imgCache || hit) { 01619 ImgVectorFree(vector); 01620 if (newFrom) 01621 mdd_free(newFrom); 01622 } 01623 new_ = mdd_and(product, resPart, 1, 1); 01624 if (info->option->verbosity) { 01625 size = bdd_size(new_); 01626 if (size > info->maxIntermediateSize) 01627 info->maxIntermediateSize = size; 01628 if (info->option->printBddSize) { 01629 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 01630 bdd_size(product), bdd_size(resPart), size); 01631 } 01632 } 01633 mdd_free(product); 01634 if (!info->imgCache || hit) 01635 mdd_free(resPart); 01636 product = new_; 01637 if (nGroups > 1 && partRelationArray != newRelationArray) 01638 mdd_array_free(partRelationArray); 01639 if (partCofactorCube && partCofactorCube != newCofactorCube) 01640 mdd_free(partCofactorCube); 01641 if (partAbstractCube && partAbstractCube != newAbstractCube) 01642 mdd_free(partAbstractCube); 01643 } 01644 if (abstractVars) 01645 array_free(abstractVars); 01646 01647 if (relationArray && newRelationArray != relationArray) 01648 mdd_array_free(newRelationArray); 01649 if (newCofactorCube) 01650 mdd_free(newCofactorCube); 01651 if (newAbstractCube) 01652 mdd_free(newAbstractCube); 01653 01654 array_free(vectorArray); 01655 array_free(varArray); 01656 01657 if (info->imgCache && nGroups > 1) { 01658 if (from) { 01659 ImgCacheInsertTable(info->imgCache, newVector, mdd_dup(from), 01660 mdd_dup(product)); 01661 } else { 01662 ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t), 01663 mdd_dup(product)); 01664 } 01665 } 01666 01667 if (info->option->debug) { 01668 refResult = ImgImageByHybrid(info, newVector, from); 01669 assert(mdd_equal(refResult, product)); 01670 mdd_free(refResult); 01671 if (!info->imgCache || nGroups == 1) 01672 ImgVectorFree(newVector); 01673 } 01674 01675 new_ = mdd_and(res, product, 1, 1); 01676 if (info->option->verbosity) { 01677 size = bdd_size(new_); 01678 if (size > info->maxIntermediateSize) 01679 info->maxIntermediateSize = size; 01680 if (info->option->printBddSize) { 01681 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 01682 bdd_size(res), bdd_size(product), size); 01683 } 01684 } 01685 mdd_free(res); 01686 mdd_free(product); 01687 res = new_; 01688 01689 if (findEssential) { 01690 if (foundEssentialDepth == info->option->maxEssentialDepth) { 01691 if (foundEssentialDepthT < foundEssentialDepthE) 01692 foundEssentialDepth = foundEssentialDepthT; 01693 else 01694 foundEssentialDepth = foundEssentialDepthE; 01695 } 01696 info->foundEssentialDepth = foundEssentialDepth; 01697 } 01698 if (info->option->debug) 01699 assert(TfmCheckImageValidity(info, res)); 01700 return(res); 01701 } 01702 01703 01713 static mdd_t * 01714 ImageByStaticInputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, 01715 array_t *relationArray, int turnDepth, int depth) 01716 { 01717 array_t *vectorT, *vectorE, *tmpVector; 01718 mdd_t *resT, *resE, *res, *tmp, *cubeT, *cubeE; 01719 mdd_t *fromT, *fromE; 01720 mdd_t *var, *varNot; 01721 array_t *relationArrayT, *relationArrayE; 01722 array_t *newRelationArray, *tmpRelationArray; 01723 int nRecur; 01724 mdd_t *refResult, *and_; 01725 mdd_t *essentialCube; 01726 int findEssential; 01727 int foundEssentialDepth, foundEssentialDepthT, foundEssentialDepthE; 01728 int turnFlag, size; 01729 01730 info->nRecursion++; 01731 01732 turnFlag = 0; 01733 if (turnDepth == -1) { 01734 if (depth < info->option->splitMinDepth) { 01735 info->nSplits++; 01736 turnFlag = 0; 01737 } else if (depth > info->option->splitMaxDepth) { 01738 info->nConjoins++; 01739 turnFlag = 1; 01740 } else { 01741 turnFlag = ImgDecideSplitOrConjoin(info, vector, from, 0, 01742 relationArray, NIL(mdd_t), 01743 NIL(mdd_t), 1, depth); 01744 } 01745 } else { 01746 if (depth == turnDepth) 01747 turnFlag = 1; 01748 else 01749 turnFlag = 0; 01750 } 01751 if (turnFlag) { 01752 res = ImgImageByHybridWithStaticSplit(info, vector, from, relationArray, 01753 NIL(mdd_t), NIL(mdd_t)); 01754 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 01755 (float)depth) / (float)(info->nLeaves + 1); 01756 if (depth > info->maxDepth) 01757 info->maxDepth = depth; 01758 info->nLeaves++; 01759 info->foundEssentialDepth = info->option->maxEssentialDepth; 01760 return(res); 01761 } 01762 01763 if (info->option->findEssential) { 01764 if (info->option->findEssential == 1) 01765 findEssential = 1; 01766 else { 01767 if (depth >= info->lastFoundEssentialDepth) 01768 findEssential = 1; 01769 else 01770 findEssential = 0; 01771 } 01772 } else 01773 findEssential = 0; 01774 if (findEssential) { 01775 essentialCube = bdd_find_essential_cube(from); 01776 01777 if (!bdd_is_tautology(essentialCube, 1)) { 01778 info->averageFoundEssential = (info->averageFoundEssential * 01779 (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) / 01780 (float)(info->nFoundEssentials + 1); 01781 info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth * 01782 (float)info->nFoundEssentials + (float)depth) / 01783 (float)(info->nFoundEssentials + 1); 01784 if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth) 01785 info->topFoundEssentialDepth = depth; 01786 if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH) 01787 info->foundEssentials[depth]++; 01788 info->nFoundEssentials++; 01789 ImgVectorMinimize(info, vector, essentialCube, NIL(mdd_t), relationArray, 01790 &tmpVector, &and_, 01791 &tmpRelationArray, NIL(mdd_t *), NIL(mdd_t *)); 01792 foundEssentialDepth = depth; 01793 } else { 01794 tmpVector = vector; 01795 tmpRelationArray = relationArray; 01796 and_ = NIL(mdd_t); 01797 foundEssentialDepth = info->option->maxEssentialDepth; 01798 } 01799 mdd_free(essentialCube); 01800 foundEssentialDepthT = info->option->maxEssentialDepth; 01801 foundEssentialDepthE = info->option->maxEssentialDepth; 01802 } else { 01803 tmpVector = vector; 01804 tmpRelationArray = relationArray; 01805 and_ = NIL(mdd_t); 01806 /* To remove compiler warnings */ 01807 foundEssentialDepth = -1; 01808 foundEssentialDepthT = -1; 01809 foundEssentialDepthE = -1; 01810 } 01811 01812 var = ImgChooseTrSplitVar(info, tmpVector, tmpRelationArray, 01813 info->option->trSplitMethod, 01814 info->option->piSplitFlag); 01815 if (!var) { 01816 res = ImgImageByHybridWithStaticSplit(info, vector, from, relationArray, 01817 NIL(mdd_t), NIL(mdd_t)); 01818 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 01819 (float)depth) / (float)(info->nLeaves + 1); 01820 if (depth > info->maxDepth) 01821 info->maxDepth = depth; 01822 info->nLeaves++; 01823 info->foundEssentialDepth = info->option->maxEssentialDepth; 01824 return(res); 01825 } 01826 01827 nRecur = 0; 01828 if (tmpVector) { 01829 ImgVectorConstrain(info, tmpVector, var, tmpRelationArray, 01830 &vectorT, &cubeT, &newRelationArray, 01831 NIL(mdd_t *), NIL(mdd_t *), TRUE); 01832 } else { 01833 vectorT = NIL(array_t); 01834 cubeT = NIL(mdd_t); 01835 newRelationArray = tmpRelationArray; 01836 } 01837 fromT = bdd_cofactor(from, var); 01838 relationArrayT = ImgGetCofactoredRelationArray(newRelationArray, var); 01839 if (relationArray && newRelationArray != tmpRelationArray) 01840 mdd_array_free(newRelationArray); 01841 if (!bdd_is_tautology(fromT, 0)) { 01842 resT = ImageByStaticInputSplit(info, vectorT, fromT, 01843 relationArrayT, turnDepth, depth + 1); 01844 if (findEssential) 01845 foundEssentialDepthT = info->foundEssentialDepth; 01846 if (vectorT) { 01847 ImgVectorFree(vectorT); 01848 if (!bdd_is_tautology(cubeT, 1)) { 01849 tmp = resT; 01850 resT = mdd_and(tmp, cubeT, 1, 1); 01851 mdd_free(tmp); 01852 } 01853 mdd_free(cubeT); 01854 } 01855 nRecur++; 01856 } else { 01857 resT = mdd_zero(info->manager); 01858 if (vectorT) { 01859 ImgVectorFree(vectorT); 01860 mdd_free(cubeT); 01861 } 01862 } 01863 mdd_free(fromT); 01864 mdd_array_free(relationArrayT); 01865 01866 if (bdd_is_tautology(resT, 1)) { 01867 mdd_free(var); 01868 if (vector && newRelationArray != relationArray) 01869 mdd_array_free(newRelationArray); 01870 res = resT; 01871 info->nEmptySubImage++; 01872 } else { 01873 varNot = mdd_not(var); 01874 mdd_free(var); 01875 if (tmpVector) { 01876 ImgVectorConstrain(info, tmpVector, varNot, tmpRelationArray, 01877 &vectorE, &cubeE, &newRelationArray, 01878 NIL(mdd_t *), NIL(mdd_t *), TRUE); 01879 } else { 01880 vectorE = NIL(array_t); 01881 cubeE = NIL(mdd_t); 01882 newRelationArray = tmpRelationArray; 01883 } 01884 fromE = bdd_cofactor(from, varNot); 01885 relationArrayE = ImgGetCofactoredRelationArray(newRelationArray, varNot); 01886 if (vector && newRelationArray != tmpRelationArray) 01887 mdd_array_free(newRelationArray); 01888 if (!bdd_is_tautology(fromE, 0)) { 01889 resE = ImageByStaticInputSplit(info, vectorE, fromE, 01890 relationArrayE, turnDepth, depth + 1); 01891 if (findEssential) 01892 foundEssentialDepthE = info->foundEssentialDepth; 01893 if (vectorE) { 01894 ImgVectorFree(vectorE); 01895 if (!bdd_is_tautology(cubeE, 1)) { 01896 tmp = resE; 01897 resE = mdd_and(tmp, cubeE, 1, 1); 01898 mdd_free(tmp); 01899 } 01900 mdd_free(cubeE); 01901 } 01902 nRecur++; 01903 } else { 01904 resE = mdd_zero(info->manager); 01905 if (vectorE) { 01906 ImgVectorFree(vectorE); 01907 mdd_free(cubeE); 01908 } 01909 } 01910 mdd_free(fromE); 01911 mdd_array_free(relationArrayE); 01912 01913 res = mdd_or(resT, resE, 1, 1); 01914 if (info->option->verbosity) { 01915 size = bdd_size(res); 01916 if (size > info->maxIntermediateSize) 01917 info->maxIntermediateSize = size; 01918 if (info->option->printBddSize) { 01919 fprintf(vis_stdout, "** tfm info: bdd_or(%d,%d) = %d\n", 01920 bdd_size(resT), bdd_size(resE), size); 01921 } 01922 } 01923 mdd_free(resT); 01924 mdd_free(resE); 01925 mdd_free(varNot); 01926 } 01927 01928 if (tmpVector && tmpVector != vector) 01929 ImgVectorFree(tmpVector); 01930 if (tmpRelationArray && tmpRelationArray != relationArray) 01931 mdd_array_free(tmpRelationArray); 01932 01933 if (and_) { 01934 tmp = res; 01935 res = mdd_and(tmp, and_, 1, 1); 01936 if (info->option->verbosity) { 01937 size = bdd_size(res); 01938 if (size > info->maxIntermediateSize) 01939 info->maxIntermediateSize = size; 01940 if (info->option->printBddSize) { 01941 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 01942 bdd_size(tmp), bdd_size(and_), size); 01943 } 01944 } 01945 mdd_free(tmp); 01946 } 01947 01948 if (info->option->debug) { 01949 refResult = ImgImageByHybridWithStaticSplit(info, vector, from, 01950 relationArray, 01951 NIL(mdd_t), NIL(mdd_t)); 01952 assert(mdd_equal(refResult, res)); 01953 mdd_free(refResult); 01954 } 01955 01956 if (nRecur == 0) { 01957 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 01958 (float)depth) / (float)(info->nLeaves + 1); 01959 if (depth > info->maxDepth) 01960 info->maxDepth = depth; 01961 info->nLeaves++; 01962 } 01963 01964 if (findEssential) { 01965 if (foundEssentialDepth == info->option->maxEssentialDepth) { 01966 if (foundEssentialDepthT < foundEssentialDepthE) 01967 foundEssentialDepth = foundEssentialDepthT; 01968 else 01969 foundEssentialDepth = foundEssentialDepthE; 01970 } 01971 info->foundEssentialDepth = foundEssentialDepth; 01972 } 01973 return(res); 01974 } 01975 01976 01986 static mdd_t * 01987 ImageByOutputSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint, 01988 int depth) 01989 { 01990 array_t *newVector; 01991 mdd_t *new_, *resT, *resE, *res, *resPart; 01992 mdd_t *constrain, *tmp, *func; 01993 int size, i, vectorSize; 01994 array_t *vectorArray, *varArray; 01995 ImgComponent_t *comp; 01996 int hit; 01997 int split, nGroups; 01998 mdd_t *product, *refResult; 01999 02000 ImgVectorConstrain(info, vector, constraint, NIL(array_t), 02001 &newVector, &res, NIL(array_t *), 02002 NIL(mdd_t *), NIL(mdd_t *), FALSE); 02003 02004 info->nRecursion++; 02005 if (info->nIntermediateVars) 02006 size = ImgVectorFunctionSize(newVector); 02007 else 02008 size = array_n(newVector); 02009 if (size <= 1) { 02010 ImgVectorFree(newVector); 02011 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 02012 (float)depth) / (float)(info->nLeaves + 1); 02013 if (depth > info->maxDepth) 02014 info->maxDepth = depth; 02015 info->nLeaves++; 02016 return(res); 02017 } 02018 02019 if (size == 2) { 02020 hit = 1; 02021 if (!info->imgCache || 02022 !(resPart = ImgCacheLookupTable(info, info->imgCache, newVector, 02023 NIL(bdd_t)))) { 02024 hit = 0; 02025 resPart = ImageFast2(info, newVector); 02026 if (info->imgCache) 02027 ImgCacheInsertTable(info->imgCache, newVector, NIL(bdd_t), resPart); 02028 } 02029 02030 if (info->option->debug) { 02031 refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t)); 02032 assert(mdd_equal(refResult, resPart)); 02033 mdd_free(refResult); 02034 } 02035 new_ = mdd_and(res, resPart, 1, 1); 02036 if (info->option->verbosity) { 02037 size = bdd_size(new_); 02038 if (size > info->maxIntermediateSize) 02039 info->maxIntermediateSize = size; 02040 if (info->option->printBddSize) { 02041 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 02042 bdd_size(res), bdd_size(resPart), size); 02043 } 02044 } 02045 mdd_free(res); 02046 if (!info->imgCache || hit) { 02047 mdd_free(resPart); 02048 ImgVectorFree(newVector); 02049 } 02050 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 02051 (float)depth) / (float)(info->nLeaves + 1); 02052 if (depth > info->maxDepth) 02053 info->maxDepth = depth; 02054 info->nLeaves++; 02055 return(new_); 02056 } 02057 02058 if (info->imgCache) { 02059 resPart = ImgCacheLookupTable(info, info->imgCache, newVector, NIL(mdd_t)); 02060 if (resPart) { 02061 if (info->option->debug) { 02062 refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t)); 02063 assert(mdd_equal(refResult, resPart)); 02064 mdd_free(refResult); 02065 } 02066 new_ = mdd_and(res, resPart, 1, 1); 02067 if (info->option->verbosity) { 02068 size = bdd_size(new_); 02069 if (size > info->maxIntermediateSize) 02070 info->maxIntermediateSize = size; 02071 if (info->option->printBddSize) { 02072 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 02073 bdd_size(res), bdd_size(resPart), size); 02074 } 02075 } 02076 mdd_free(res); 02077 mdd_free(resPart); 02078 res = new_; 02079 ImgVectorFree(newVector); 02080 return(res); 02081 } 02082 } 02083 02084 /* compute disconnected component and best variable selection */ 02085 vectorArray = array_alloc(array_t *, 0); 02086 varArray = array_alloc(array_t *, 0); 02087 nGroups = ImageDecomposeAndChooseSplitVar(info, newVector, NIL(mdd_t), 1, 02088 info->option->outputSplit, 0, 02089 vectorArray, varArray, &product, 02090 NIL(array_t), NIL(array_t *), 02091 NIL(mdd_t *), NIL(mdd_t *)); 02092 vectorSize = array_n(newVector); 02093 if ((!info->imgCache || nGroups <= 1) && !info->option->debug) 02094 ImgVectorFree(newVector); 02095 if (nGroups == 0) { 02096 array_free(vectorArray); 02097 array_free(varArray); 02098 02099 if (info->option->debug) { 02100 refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t)); 02101 assert(mdd_equal(refResult, product)); 02102 mdd_free(refResult); 02103 ImgVectorFree(newVector); 02104 } 02105 02106 new_ = mdd_and(res, product, 1, 1); 02107 if (info->option->verbosity) { 02108 size = bdd_size(new_); 02109 if (size > info->maxIntermediateSize) 02110 info->maxIntermediateSize = size; 02111 if (info->option->printBddSize) { 02112 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 02113 bdd_size(res), bdd_size(product), size); 02114 } 02115 } 02116 mdd_free(res); 02117 mdd_free(product); 02118 res = new_; 02119 02120 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 02121 (float)depth) / (float)(info->nLeaves + 1); 02122 if (depth > info->maxDepth) 02123 info->maxDepth = depth; 02124 info->nLeaves++; 02125 return(res); 02126 } else if (nGroups > 1) { 02127 if (info->nDecomps == 0 || depth < info->topDecomp) 02128 info->topDecomp = depth; 02129 if (info->nDecomps == 0 || vectorSize > info->maxDecomp) 02130 info->maxDecomp = vectorSize; 02131 info->averageDecomp = (info->averageDecomp * (float)info->nDecomps + 02132 (float)nGroups) / (float)(info->nDecomps + 1); 02133 info->nDecomps++; 02134 } 02135 02136 product = mdd_one(info->manager); 02137 for (i = 0; i < array_n(vectorArray); i++) { 02138 vector = array_fetch(array_t *, vectorArray, i); 02139 02140 hit = 1; 02141 if (!info->imgCache || nGroups == 1 || 02142 !(resPart = ImgCacheLookupTable(info, info->imgCache, vector, 02143 NIL(bdd_t)))) { 02144 hit = 0; 02145 if (info->nIntermediateVars) 02146 size = ImgVectorFunctionSize(vector); 02147 else 02148 size = array_n(vector); 02149 if (size == 1) { 02150 comp = array_fetch(ImgComponent_t *, vector, 0); 02151 if (array_n(vector) > 1) 02152 func = ImgGetComposedFunction(vector); 02153 else 02154 func = comp->func; 02155 if (bdd_is_tautology(func, 1)) 02156 resPart = mdd_dup(comp->var); 02157 else if (bdd_is_tautology(func, 0)) 02158 resPart = mdd_not(comp->var); 02159 else 02160 resPart = mdd_one(info->manager); 02161 if (array_n(vector) > 1) 02162 mdd_free(func); 02163 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 02164 (float)depth) / (float)(info->nLeaves + 1); 02165 if (depth > info->maxDepth) 02166 info->maxDepth = depth; 02167 info->nLeaves++; 02168 } else if (size == 2) { 02169 resPart = ImageFast2(info, vector); 02170 info->averageDepth = (info->averageDepth * (float)info->nLeaves + 02171 (float)depth) / (float)(info->nLeaves + 1); 02172 if (depth > info->maxDepth) 02173 info->maxDepth = depth; 02174 info->nLeaves++; 02175 } else { 02176 split = array_fetch(int, varArray, i); 02177 comp = array_fetch(ImgComponent_t *, vector, split); 02178 constrain = comp->func; 02179 resT = ImageByOutputSplit(info, vector, constrain, depth + 1); 02180 tmp = mdd_not(constrain); 02181 resE = ImageByOutputSplit(info, vector, tmp, depth + 1); 02182 mdd_free(tmp); 02183 02184 resPart = bdd_ite(comp->var, resT, resE, 1, 1, 1); 02185 if (info->option->verbosity) { 02186 size = bdd_size(resPart); 02187 if (size > info->maxIntermediateSize) 02188 info->maxIntermediateSize = size; 02189 if (info->option->printBddSize) { 02190 fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n", 02191 bdd_size(resT), bdd_size(resE), size); 02192 } 02193 } 02194 mdd_free(resT); 02195 mdd_free(resE); 02196 } 02197 if (info->imgCache) 02198 ImgCacheInsertTable(info->imgCache, vector, NIL(bdd_t), resPart); 02199 } 02200 if (!info->imgCache || hit) 02201 ImgVectorFree(vector); 02202 new_ = mdd_and(product, resPart, 1, 1); 02203 if (info->option->verbosity) { 02204 size = bdd_size(new_); 02205 if (size > info->maxIntermediateSize) 02206 info->maxIntermediateSize = size; 02207 if (info->option->printBddSize) { 02208 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 02209 bdd_size(product), bdd_size(resPart), size); 02210 } 02211 } 02212 mdd_free(product); 02213 if (!info->imgCache || hit) 02214 mdd_free(resPart); 02215 product = new_; 02216 } 02217 02218 array_free(vectorArray); 02219 array_free(varArray); 02220 02221 if (info->imgCache && nGroups > 1) { 02222 ImgCacheInsertTable(info->imgCache, newVector, NIL(mdd_t), 02223 mdd_dup(product)); 02224 } 02225 02226 if (info->option->debug) { 02227 refResult = ImgImageByHybrid(info, newVector, NIL(mdd_t)); 02228 assert(mdd_equal(refResult, product)); 02229 mdd_free(refResult); 02230 if (!info->imgCache || nGroups == 1) 02231 ImgVectorFree(newVector); 02232 } 02233 02234 new_ = mdd_and(res, product, 1, 1); 02235 if (info->option->verbosity) { 02236 size = bdd_size(new_); 02237 if (size > info->maxIntermediateSize) 02238 info->maxIntermediateSize = size; 02239 if (info->option->printBddSize) { 02240 fprintf(vis_stdout, "** tfm info: bdd_and(%d,%d) = %d\n", 02241 bdd_size(res), bdd_size(product), size); 02242 } 02243 } 02244 mdd_free(res); 02245 mdd_free(product); 02246 res = new_; 02247 02248 return(res); 02249 } 02250 02251 02263 static int 02264 ImageDecomposeAndChooseSplitVar(ImgTfmInfo_t *info, array_t *vector, 02265 mdd_t *from, int splitMethod, int split, 02266 int piSplitFlag, 02267 array_t *vectorArray, array_t *varArray, 02268 mdd_t **singles, array_t *relationArray, 02269 array_t **newRelationArray, 02270 mdd_t **cofactorCube, mdd_t **abstractCube) 02271 { 02272 int i, j, f, index; 02273 int nGroups, nSingles, nChosen; 02274 int nVars, nFuncs, arraySize; 02275 char *varFlag; 02276 int *funcGroup; 02277 int *varOccur; 02278 int bestVar; 02279 int *stack, size; 02280 ImgComponent_t *comp, *newComp; 02281 array_t *partVector; 02282 char *stackFlag; 02283 char *support; 02284 mdd_t *func; 02285 int *varCost; 02286 int decompose; 02287 int res, constConstrain; 02288 mdd_t *tmp, *cofactor, *abstract, *nsVar; 02289 array_t *tmpRelationArray; 02290 char *intermediateVarFlag; 02291 int *intermediateVarFuncMap; 02292 02293 if (info->useConstraint && from && splitMethod == 0) 02294 decompose = 0; 02295 else 02296 decompose = 1; 02297 02298 arraySize = array_n(vector); 02299 if (info->nIntermediateVars) 02300 nFuncs = ImgVectorFunctionSize(vector); 02301 else 02302 nFuncs = arraySize; 02303 nVars = info->nVars; 02304 02305 *singles = mdd_one(info->manager); 02306 if (relationArray) { 02307 cofactor = mdd_one(info->manager); 02308 abstract = mdd_one(info->manager); 02309 } else { 02310 cofactor = NIL(mdd_t); 02311 abstract = NIL(mdd_t); 02312 } 02313 02314 if (decompose) { 02315 funcGroup = ALLOC(int, arraySize); 02316 memset(funcGroup, 0, sizeof(int) * arraySize); 02317 varFlag = ALLOC(char, nVars); 02318 memset(varFlag, 0, sizeof(char) * nVars); 02319 stack = ALLOC(int, arraySize); 02320 stackFlag = ALLOC(char, arraySize); 02321 memset(stackFlag, 0, sizeof(char) * arraySize); 02322 if (arraySize > nFuncs) { 02323 intermediateVarFlag = ALLOC(char, nVars); 02324 memset(intermediateVarFlag, 0, sizeof(char) * nVars); 02325 intermediateVarFuncMap = ALLOC(int, nVars); 02326 memset(intermediateVarFuncMap, 0, sizeof(int) * nVars); 02327 for (i = 0; i < arraySize; i++) { 02328 comp = array_fetch(ImgComponent_t *, vector, i); 02329 if (comp->intermediate) { 02330 index = (int)bdd_top_var_id(comp->var); 02331 intermediateVarFlag[index] = 1; 02332 intermediateVarFuncMap[index] = i; 02333 } 02334 } 02335 } else { 02336 /* To remove compiler warnings */ 02337 intermediateVarFlag = NIL(char); 02338 intermediateVarFuncMap = NIL(int); 02339 } 02340 } else { 02341 /* To remove compiler warnings */ 02342 funcGroup = NIL(int); 02343 varFlag = NIL(char); 02344 stack = NIL(int); 02345 stackFlag = NIL(char); 02346 intermediateVarFlag = NIL(char); 02347 intermediateVarFuncMap = NIL(int); 02348 } 02349 varOccur = ALLOC(int, nVars); 02350 if (splitMethod == 0 && split > 0) 02351 varCost = ALLOC(int, nVars); 02352 else 02353 varCost = NIL(int); 02354 02355 nGroups = 0; 02356 nSingles = 0; 02357 nChosen = 0; 02358 while (nChosen < nFuncs) { 02359 bestVar = -1; 02360 memset(varOccur, 0, sizeof(int) * nVars); 02361 if (varCost) 02362 memset(varCost, 0, sizeof(int) * nVars); 02363 02364 if (decompose) { 02365 size = 0; 02366 for (i = 0; i < arraySize; i++) { 02367 if (funcGroup[i] == 0) { 02368 stack[0] = i; 02369 size = 1; 02370 stackFlag[i] = 1; 02371 break; 02372 } 02373 } 02374 assert(size == 1); 02375 02376 while (size) { 02377 size--; 02378 f = stack[size]; 02379 funcGroup[f] = nGroups + 1; 02380 comp = array_fetch(ImgComponent_t *, vector, f); 02381 nChosen++; 02382 if (nChosen == arraySize) 02383 break; 02384 support = comp->support; 02385 if (comp->intermediate) { 02386 index = (int)bdd_top_var_id(comp->var); 02387 support[index] = 1; 02388 } 02389 for (i = 0; i < nVars; i++) { 02390 if (!support[i]) 02391 continue; 02392 varOccur[i]++; 02393 if (varFlag[i]) 02394 continue; 02395 varFlag[i] = 1; 02396 for (j = 0; j < arraySize; j++) { 02397 if (j == f || stackFlag[j]) 02398 continue; 02399 comp = array_fetch(ImgComponent_t *, vector, j); 02400 if (arraySize != nFuncs) { 02401 if (intermediateVarFlag[i] && comp->intermediate) { 02402 index = (int)bdd_top_var_id(comp->var); 02403 if (index == i) { 02404 if (funcGroup[j] == 0) { 02405 stack[size] = j; 02406 size++; 02407 stackFlag[j] = 1; 02408 } 02409 FindIntermediateSupport(vector, comp, nVars, nGroups, 02410 stack, stackFlag, funcGroup, &size, 02411 intermediateVarFlag, 02412 intermediateVarFuncMap); 02413 continue; 02414 } 02415 } 02416 } 02417 if (funcGroup[j]) 02418 continue; 02419 if (comp->support[i]) { 02420 stack[size] = j; 02421 size++; 02422 stackFlag[j] = 1; 02423 } 02424 } 02425 } 02426 if (comp->intermediate) { 02427 index = (int)bdd_top_var_id(comp->var); 02428 support[index] = 0; 02429 } 02430 } 02431 } else { 02432 for (i = 0; i < arraySize; i++) { 02433 comp = array_fetch(ImgComponent_t *, vector, i); 02434 support = comp->support; 02435 for (j = 0; j < nVars; j++) { 02436 if (support[j]) 02437 varOccur[j]++; 02438 } 02439 } 02440 nChosen = nFuncs; 02441 } 02442 02443 nGroups++; 02444 02445 /* Collect the functions which belong to the current group */ 02446 partVector = array_alloc(ImgComponent_t *, 0); 02447 for (i = 0; i < arraySize; i++) { 02448 if (decompose == 0 || funcGroup[i] == nGroups) { 02449 comp = array_fetch(ImgComponent_t *, vector, i); 02450 newComp = ImgComponentCopy(info, comp); 02451 array_insert_last(ImgComponent_t *, partVector, newComp); 02452 } 02453 } 02454 if (arraySize == nFuncs) 02455 size = array_n(partVector); 02456 else 02457 size = ImgVectorFunctionSize(partVector); 02458 if (size == 1) { 02459 nSingles++; 02460 if (size == array_n(partVector)) { 02461 comp = array_fetch(ImgComponent_t *, partVector, 0); 02462 func = comp->func; 02463 } else { 02464 comp = ImgGetLatchComponent(partVector); 02465 func = ImgGetComposedFunction(partVector); 02466 } 02467 if (from) { 02468 constConstrain = ImgConstConstrain(func, from); 02469 if (constConstrain == 1) 02470 res = 1; 02471 else if (constConstrain == 0) 02472 res = 0; 02473 else 02474 res = 2; 02475 } else { 02476 if (bdd_is_tautology(func, 1)) 02477 res = 1; 02478 else if (bdd_is_tautology(func, 0)) 02479 res = 0; 02480 else 02481 res = 2; 02482 } 02483 if (size != array_n(partVector)) 02484 mdd_free(func); 02485 if (res == 1) { 02486 tmp = *singles; 02487 *singles = mdd_and(tmp, comp->var, 1, 1); 02488 mdd_free(tmp); 02489 } else if (res == 0) { 02490 tmp = *singles; 02491 *singles = mdd_and(tmp, comp->var, 1, 0); 02492 mdd_free(tmp); 02493 } 02494 if (abstract) { 02495 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 02496 tmp = abstract; 02497 abstract = mdd_and(tmp, nsVar, 1, 1); 02498 mdd_free(tmp); 02499 mdd_free(nsVar); 02500 } 02501 02502 ImgVectorFree(partVector); 02503 continue; 02504 } 02505 02506 array_insert_last(array_t *, vectorArray, partVector); 02507 02508 if (splitMethod == 0) { /* input splitting */ 02509 if (decompose) { 02510 if (info->option->findDecompVar) { 02511 bestVar = FindDecomposableVariable(info, partVector); 02512 if (bestVar != -1) 02513 split = -1; 02514 } 02515 } else if (from) { 02516 comp = ImgComponentAlloc(info); 02517 comp->func = from; 02518 ImgComponentGetSupport(comp); 02519 for (i = 0; i < nVars; i++) { 02520 if (comp->support[i]) 02521 varOccur[i]++; 02522 } 02523 comp->func = NIL(mdd_t); 02524 ImgComponentFree(comp); 02525 } 02526 02527 if (split != -1) { 02528 bestVar = ChooseInputSplittingVariable(info, partVector, from, 02529 info->option->inputSplit, decompose, 02530 info->option->piSplitFlag, varOccur); 02531 02532 } 02533 } else { /* output splitting */ 02534 bestVar = ChooseOutputSplittingVariable(info, partVector, 02535 info->option->outputSplit); 02536 } 02537 assert(bestVar != -1); 02538 array_insert_last(int, varArray, bestVar); 02539 } 02540 02541 if (newRelationArray) 02542 *newRelationArray = relationArray; 02543 if (cofactorCube && abstractCube) { 02544 if (cofactor) 02545 *cofactorCube = cofactor; 02546 if (abstract) 02547 *abstractCube = abstract; 02548 } else { 02549 if (cofactor) { 02550 if (bdd_is_tautology(cofactor, 1)) 02551 mdd_free(cofactor); 02552 else { 02553 *newRelationArray = ImgGetCofactoredRelationArray(relationArray, 02554 cofactor); 02555 mdd_free(cofactor); 02556 } 02557 } 02558 if (abstract) { 02559 if (bdd_is_tautology(abstract, 1)) 02560 mdd_free(abstract); 02561 else { 02562 tmpRelationArray = *newRelationArray; 02563 *newRelationArray = ImgGetAbstractedRelationArray(info->manager, 02564 tmpRelationArray, 02565 abstract); 02566 mdd_free(abstract); 02567 if (tmpRelationArray != relationArray) 02568 mdd_array_free(tmpRelationArray); 02569 } 02570 } 02571 } 02572 02573 if (decompose) { 02574 FREE(stackFlag); 02575 FREE(stack); 02576 FREE(funcGroup); 02577 FREE(varFlag); 02578 if (arraySize > nFuncs) { 02579 FREE(intermediateVarFlag); 02580 FREE(intermediateVarFuncMap); 02581 } 02582 } 02583 FREE(varOccur); 02584 if (varCost) 02585 FREE(varCost); 02586 nGroups -= nSingles; 02587 return(nGroups); 02588 } 02589 02590 02602 static mdd_t * 02603 ImageFast2(ImgTfmInfo_t *info, array_t *vector) 02604 { 02605 mdd_t *f1, *f2; 02606 int f21n, f21p; 02607 mdd_t *res, *resp, *resn; 02608 mdd_t *i1, *i2; 02609 ImgComponent_t *comp; 02610 mdd_t *refResult; 02611 int i, freeFlag, size; 02612 array_t *varArray, *funcArray; 02613 02614 assert(ImgVectorFunctionSize(vector) == 2); 02615 02616 if (info->option->debug) 02617 refResult = ImgImageByHybrid(info, vector, NIL(mdd_t)); 02618 else 02619 refResult = NIL(mdd_t); 02620 02621 if (array_n(vector) == 2) { 02622 comp = array_fetch(ImgComponent_t *, vector, 0); 02623 f1 = comp->func; 02624 i1 = comp->var; 02625 02626 comp = array_fetch(ImgComponent_t *, vector, 1); 02627 f2 = comp->func; 02628 i2 = comp->var; 02629 02630 freeFlag = 0; 02631 } else { 02632 varArray = array_alloc(mdd_t *, 0); 02633 funcArray = array_alloc(mdd_t *, 0); 02634 02635 i1 = NIL(mdd_t); 02636 i2 = NIL(mdd_t); 02637 f1 = NIL(mdd_t); 02638 f2 = NIL(mdd_t); 02639 02640 for (i = 0; i < array_n(vector); i++) { 02641 comp = array_fetch(ImgComponent_t *, vector, i); 02642 if (comp->intermediate) { 02643 array_insert_last(mdd_t *, varArray, comp->var); 02644 array_insert_last(mdd_t *, funcArray, comp->func); 02645 continue; 02646 } 02647 if (f1) { 02648 f2 = comp->func; 02649 i2 = comp->var; 02650 } else { 02651 f1 = comp->func; 02652 i1 = comp->var; 02653 } 02654 } 02655 02656 f1 = bdd_vector_compose(f1, varArray, funcArray); 02657 f2 = bdd_vector_compose(f2, varArray, funcArray); 02658 array_free(varArray); 02659 array_free(funcArray); 02660 freeFlag = 1; 02661 } 02662 02663 ImgCheckConstConstrain(f1, f2, &f21p, &f21n); 02664 02665 if (f21p == 1) 02666 resp = mdd_dup(i2); 02667 else if (f21p == 0) 02668 resp = mdd_not(i2); 02669 else 02670 resp = mdd_one(info->manager); 02671 02672 if (f21n == 1) 02673 resn = mdd_dup(i2); 02674 else if (f21n == 0) 02675 resn = mdd_not(i2); 02676 else 02677 resn = mdd_one(info->manager); 02678 02679 /* merge final result */ 02680 res = bdd_ite(i1, resp, resn, 1, 1, 1); 02681 if (info->option->verbosity) { 02682 size = bdd_size(res); 02683 if (size > info->maxIntermediateSize) 02684 info->maxIntermediateSize = size; 02685 if (info->option->printBddSize) { 02686 fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n", 02687 bdd_size(resp), bdd_size(resn), size); 02688 } 02689 } 02690 mdd_free(resp); 02691 mdd_free(resn); 02692 if (freeFlag) { 02693 mdd_free(f1); 02694 mdd_free(f2); 02695 } 02696 02697 if (info->option->debug) { 02698 assert(mdd_equal(refResult, res)); 02699 mdd_free(refResult); 02700 } 02701 02702 return(res); 02703 } 02704 02705 02715 static int 02716 FindDecomposableVariable(ImgTfmInfo_t *info, array_t *vector) 02717 { 02718 int i, j, f, split; 02719 int nChosen, index, varId; 02720 int nVars, nFuncs; 02721 char *varFlag; 02722 int *funcGroup; 02723 int *stack, size; 02724 ImgComponent_t *comp; 02725 char *stackFlag; 02726 char *support; 02727 int arraySize; 02728 char *intermediateVarFlag; 02729 int *intermediateVarFuncMap; 02730 02731 arraySize = array_n(vector); 02732 if (info->nIntermediateVars) 02733 nFuncs = ImgVectorFunctionSize(vector); 02734 else 02735 nFuncs = arraySize; 02736 nVars = info->nVars; 02737 02738 funcGroup = ALLOC(int, arraySize); 02739 varFlag = ALLOC(char, nVars); 02740 stack = ALLOC(int, arraySize); 02741 stackFlag = ALLOC(char, arraySize); 02742 02743 if (arraySize > nFuncs) { 02744 intermediateVarFlag = ALLOC(char, nVars); 02745 memset(intermediateVarFlag, 0, sizeof(char) * nVars); 02746 intermediateVarFuncMap = ALLOC(int, nVars); 02747 memset(intermediateVarFuncMap, 0, sizeof(int) * nVars); 02748 for (i = 0; i < arraySize; i++) { 02749 comp = array_fetch(ImgComponent_t *, vector, i); 02750 if (comp->intermediate) { 02751 index = (int)bdd_top_var_id(comp->var); 02752 intermediateVarFlag[index] = 1; 02753 intermediateVarFuncMap[index] = i; 02754 } 02755 } 02756 } else { 02757 intermediateVarFlag = NIL(char); 02758 intermediateVarFuncMap = NIL(int); 02759 } 02760 02761 varId = -1; 02762 for (split = 0; split < nVars; split++) { 02763 if (intermediateVarFlag[split]) 02764 continue; 02765 02766 memset(funcGroup, 0, sizeof(int) * arraySize); 02767 memset(varFlag, 0, sizeof(char) * nVars); 02768 memset(stackFlag, 0, sizeof(char) * arraySize); 02769 02770 varFlag[split] = 1; 02771 nChosen = 0; 02772 02773 stack[0] = 0; 02774 size = 1; 02775 stackFlag[0] = 1; 02776 02777 while (size) { 02778 size--; 02779 f = stack[size]; 02780 funcGroup[f] = 1; 02781 comp = array_fetch(ImgComponent_t *, vector, f); 02782 nChosen++; 02783 if (nChosen == arraySize) 02784 break; 02785 support = comp->support; 02786 if (comp->intermediate) { 02787 index = (int)bdd_top_var_id(comp->var); 02788 support[index] = 1; 02789 } 02790 for (i = 0; i < nVars; i++) { 02791 if (!support[i]) 02792 continue; 02793 if (varFlag[i]) 02794 continue; 02795 varFlag[i] = 1; 02796 for (j = 0; j < nFuncs; j++) { 02797 if (j == f || stackFlag[j]) 02798 continue; 02799 comp = array_fetch(ImgComponent_t *, vector, j); 02800 if (arraySize != nFuncs) { 02801 if (intermediateVarFlag[i] && comp->intermediate) { 02802 index = (int)bdd_top_var_id(comp->var); 02803 if (index == i) { 02804 if (funcGroup[j] == 0) { 02805 stack[size] = j; 02806 size++; 02807 stackFlag[j] = 1; 02808 } 02809 FindIntermediateSupport(vector, comp, nVars, 0, 02810 stack, stackFlag, funcGroup, &size, 02811 intermediateVarFlag, 02812 intermediateVarFuncMap); 02813 continue; 02814 } 02815 } 02816 } 02817 if (funcGroup[j]) 02818 continue; 02819 if (comp->support[i]) { 02820 stack[size] = j; 02821 size++; 02822 stackFlag[j] = 1; 02823 } 02824 } 02825 } 02826 if (comp->intermediate) { 02827 index = (int)bdd_top_var_id(comp->var); 02828 support[index] = 0; 02829 } 02830 } 02831 02832 if (nChosen < nFuncs) { 02833 varId = split; 02834 break; 02835 } 02836 } 02837 02838 FREE(stackFlag); 02839 FREE(stack); 02840 FREE(funcGroup); 02841 FREE(varFlag); 02842 if (arraySize > nFuncs) { 02843 FREE(intermediateVarFlag); 02844 FREE(intermediateVarFuncMap); 02845 } 02846 02847 return(varId); 02848 } 02849 02850 02860 static int 02861 TfmCheckImageValidity(ImgTfmInfo_t *info, mdd_t *image) 02862 { 02863 int i, id; 02864 array_t *supportIds; 02865 int status = 1; 02866 02867 supportIds = mdd_get_bdd_support_ids(info->manager, image); 02868 for (i = 0; i < array_n(supportIds); i++) { 02869 id = array_fetch(int, supportIds, i); 02870 if (st_lookup(info->quantifyVarsTable, (char *)(long)id, NIL(char *))) { 02871 fprintf(vis_stderr, 02872 "** tfm error: image contains a primary input variable (%d)\n", 02873 id); 02874 status = 0; 02875 } 02876 if (st_lookup(info->rangeVarsTable, (char *)(long)id, NIL(char *))) { 02877 fprintf(vis_stderr, 02878 "** tfm error: image contains a range variable (%d)\n", id); 02879 status = 0; 02880 } 02881 if (info->intermediateVarsTable && 02882 st_lookup(info->intermediateVarsTable, (char *)(long)id, NIL(char *))) { 02883 fprintf(vis_stderr, 02884 "** tfm error: image contains an intermediate variable (%d)\n", 02885 id); 02886 status = 0; 02887 } 02888 } 02889 array_free(supportIds); 02890 return(status); 02891 } 02892 02893 02906 static void 02907 FindIntermediateSupport(array_t *vector, ImgComponent_t *comp, 02908 int nVars, int nGroups, 02909 int *stack, char *stackFlag, int *funcGroup, int *size, 02910 char *intermediateVarFlag, int *intermediateVarFuncMap) 02911 { 02912 int i, f; 02913 ImgComponent_t *intermediateComp; 02914 02915 for (i = 0; i < nVars; i++) { 02916 if (comp->support[i]) { 02917 if (intermediateVarFlag[i]) { 02918 f = intermediateVarFuncMap[i]; 02919 if (stackFlag[f] || funcGroup[f] == nGroups + 1) 02920 continue; 02921 stack[*size] = f; 02922 (*size)++; 02923 stackFlag[f] = 1; 02924 02925 intermediateComp = array_fetch(ImgComponent_t *, vector, f); 02926 FindIntermediateSupport(vector, intermediateComp, nVars, nGroups, 02927 stack, stackFlag, funcGroup, size, 02928 intermediateVarFlag, intermediateVarFuncMap); 02929 } 02930 } 02931 } 02932 } 02933 02934 02944 static void 02945 PrintVectorDecomposition(ImgTfmInfo_t *info, array_t *vectorArray, 02946 array_t *varArray) 02947 { 02948 int i, j, n; 02949 int var, index; 02950 ImgComponent_t *comp; 02951 array_t *vector; 02952 02953 fprintf(vis_stdout, "** tfm info: vector decomposition\n"); 02954 n = array_n(vectorArray); 02955 for (i = 0; i < n; i++) { 02956 vector = array_fetch(array_t *, vectorArray, i); 02957 var = array_fetch(int, varArray, i); 02958 fprintf(vis_stdout, "Group[%d] : num = %d, split = %d\n", 02959 i, array_n(vector), var); 02960 for (j = 0; j < array_n(vector); j++) { 02961 comp = array_fetch(ImgComponent_t *, vector, j); 02962 index = (int)bdd_top_var_id(comp->var); 02963 fprintf(vis_stdout, " %d", index); 02964 } 02965 fprintf(vis_stdout, "\n"); 02966 } 02967 } 02968 02969 02982 static int 02983 CheckIfValidSplitOrGetNew(ImgTfmInfo_t *info, int split, array_t *vector, 02984 array_t *relationArray, mdd_t *from) 02985 { 02986 int newSplit = split; 02987 int i, j, nVars; 02988 ImgComponent_t *comp; 02989 char *support; 02990 int *varOccur; 02991 int decompose; 02992 02993 nVars = info->nVars; 02994 support = ALLOC(char, sizeof(char) * nVars); 02995 memset(support, 0, sizeof(char) * nVars); 02996 02997 comp = ImgComponentAlloc(info); 02998 for (i = 0; i < array_n(relationArray); i++) { 02999 comp->func = array_fetch(mdd_t *, relationArray, i);; 03000 ImgSupportClear(info, comp->support); 03001 ImgComponentGetSupport(comp); 03002 for (j = 0; j < nVars; j++) { 03003 if (comp->support[j]) { 03004 if (j == split) { 03005 comp->func = NIL(mdd_t); 03006 ImgComponentFree(comp); 03007 FREE(support); 03008 return(split); 03009 } 03010 support[j] = 1; 03011 } 03012 } 03013 } 03014 03015 comp->func = NIL(mdd_t); 03016 ImgComponentFree(comp); 03017 03018 if (info->useConstraint && from) 03019 decompose = 0; 03020 else 03021 decompose = 1; 03022 03023 varOccur = ALLOC(int, nVars); 03024 memset(varOccur, 0, sizeof(int) * nVars); 03025 03026 if (from) { 03027 comp = ImgComponentAlloc(info); 03028 comp->func = from; 03029 ImgComponentGetSupport(comp); 03030 for (i = 0; i < nVars; i++) { 03031 if (comp->support[i]) 03032 varOccur[i]++; 03033 } 03034 comp->func = NIL(mdd_t); 03035 ImgComponentFree(comp); 03036 } 03037 03038 FREE(support); 03039 03040 newSplit = ChooseInputSplittingVariable(info, vector, from, 03041 info->option->inputSplit, decompose, 03042 info->option->piSplitFlag, varOccur); 03043 03044 FREE(varOccur); 03045 03046 return(newSplit); 03047 } 03048 03049 03059 static int 03060 ChooseInputSplittingVariable(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, 03061 int splitMethod, int decompose, int piSplitFlag, int *varOccur) 03062 { 03063 int nVars = info->nVars; 03064 int bestVar = -1; 03065 int secondBestVar = -1; 03066 int bestCost, newCost; 03067 int bestOccur, tieCount; 03068 int secondBestOccur, secondTieCount; 03069 int i, j; 03070 ImgComponent_t *comp; 03071 mdd_t *var, *varNot, *pcFunc, *ncFunc; 03072 int *varCost; 03073 int size = ImgVectorFunctionSize(vector); 03074 03075 if (info->option->inputSplit > 0) { 03076 varCost = ALLOC(int, nVars); 03077 memset(varCost, 0, sizeof(int) * nVars); 03078 } else 03079 varCost = NIL(int); 03080 03081 switch (splitMethod) { 03082 case 0: 03083 /* Find the most frequently occurred variable */ 03084 bestOccur = 0; 03085 tieCount = 0; 03086 secondBestOccur = 0; 03087 secondTieCount = 0; 03088 03089 for (i = 0; i < nVars; i++) { 03090 if (varOccur[i] == 0) 03091 continue; 03092 if (piSplitFlag == 0) { 03093 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, 03094 NIL(char *))) { 03095 if ((bestOccur == 0 && secondBestOccur == 0) || 03096 (varOccur[i] > bestOccur && varOccur[i] > secondBestOccur)) { 03097 secondBestOccur = varOccur[i]; 03098 secondBestVar = i; 03099 secondTieCount = 1; 03100 } else if (secondBestOccur > bestOccur && 03101 varOccur[i] == secondBestOccur) { 03102 secondTieCount++; 03103 if (info->option->tieBreakMode == 0 && 03104 bdd_get_level_from_id(info->manager, i) < 03105 bdd_get_level_from_id(info->manager, secondBestVar)) { 03106 secondBestVar = i; 03107 } 03108 } 03109 continue; 03110 } 03111 } 03112 if (size < array_n(vector) && 03113 st_lookup(info->intermediateVarsTable, (char *)(long)i, 03114 NIL(char *))) { 03115 continue; 03116 } 03117 if (bestOccur == 0 || varOccur[i] > bestOccur) { 03118 bestOccur = varOccur[i]; 03119 bestVar = i; 03120 tieCount = 1; 03121 } else if (varOccur[i] == bestOccur) { 03122 tieCount++; 03123 if (info->option->tieBreakMode == 0 && 03124 bdd_get_level_from_id(info->manager, i) < 03125 bdd_get_level_from_id(info->manager, bestVar)) { 03126 bestVar = i; 03127 } 03128 } 03129 } 03130 03131 if (piSplitFlag == 0 && bestVar == -1) { 03132 bestVar = secondBestVar; 03133 bestOccur = secondBestOccur; 03134 tieCount = secondTieCount; 03135 } 03136 03137 if (info->option->tieBreakMode == 1 && tieCount > 1) { 03138 bestCost = IMG_TF_MAX_INT; 03139 for (i = bestVar; i < nVars; i++) { 03140 if (varOccur[i] != bestOccur) 03141 continue; 03142 if (size < array_n(vector) && 03143 st_lookup(info->intermediateVarsTable, (char *)(long)i, 03144 NIL(char *))) { 03145 continue; 03146 } 03147 var = bdd_var_with_index(info->manager, i); 03148 newCost = 0; 03149 for (j = 0; j < array_n(vector); j++) { 03150 comp = array_fetch(ImgComponent_t *, vector, j); 03151 newCost += bdd_estimate_cofactor(comp->func, var, 1); 03152 newCost += bdd_estimate_cofactor(comp->func, var, 0); 03153 } 03154 if (decompose == 0) { 03155 newCost += bdd_estimate_cofactor(from, var, 1); 03156 newCost += bdd_estimate_cofactor(from, var, 0); 03157 } 03158 mdd_free(var); 03159 03160 if (newCost < bestCost) { 03161 bestVar = i; 03162 bestCost = newCost; 03163 } else if (newCost == bestCost) { 03164 if (bdd_get_level_from_id(info->manager, i) < 03165 bdd_get_level_from_id(info->manager, bestVar)) { 03166 bestVar = i; 03167 } 03168 } 03169 } 03170 } 03171 break; 03172 case 1: 03173 /* Find the variable which makes the smallest support after splitting */ 03174 bestCost = IMG_TF_MAX_INT; 03175 for (i = 0; i < nVars; i++) { 03176 if (varOccur[i] == 0) 03177 continue; 03178 if (size < array_n(vector) && 03179 st_lookup(info->intermediateVarsTable, (char *)(long)i, 03180 NIL(char *))) { 03181 continue; 03182 } 03183 var = bdd_var_with_index(info->manager, i); 03184 varNot = mdd_not(var); 03185 for (j = 0; j < array_n(vector); j++) { 03186 comp = array_fetch(ImgComponent_t *, vector, j); 03187 pcFunc = bdd_cofactor(comp->func, var); 03188 varCost[i] += ImgCountBddSupports(pcFunc); 03189 mdd_free(pcFunc); 03190 ncFunc = bdd_cofactor(comp->func, varNot); 03191 varCost[i] += ImgCountBddSupports(ncFunc); 03192 mdd_free(ncFunc); 03193 } 03194 if (decompose == 0) { 03195 pcFunc = bdd_cofactor(from, var); 03196 varCost[i] += ImgCountBddSupports(pcFunc); 03197 mdd_free(pcFunc); 03198 ncFunc = bdd_cofactor(from, varNot); 03199 varCost[i] += ImgCountBddSupports(ncFunc); 03200 mdd_free(ncFunc); 03201 } 03202 mdd_free(var); 03203 mdd_free(varNot); 03204 03205 if (varCost[i] < bestCost) { 03206 bestCost = varCost[i]; 03207 bestVar = i; 03208 } else if (varCost[i] == bestCost) { 03209 if (varOccur[i] < varOccur[bestVar]) { 03210 bestVar = i; 03211 } else if (varOccur[i] == varOccur[bestVar]) { 03212 if (bdd_get_level_from_id(info->manager, i) < 03213 bdd_get_level_from_id(info->manager, bestVar)) { 03214 bestVar = i; 03215 } 03216 } 03217 } 03218 } 03219 break; 03220 case 2: 03221 /* Find the variable which makes the smallest BDDs of all functions 03222 after splitting */ 03223 bestCost = IMG_TF_MAX_INT; 03224 for (i = 0; i < nVars; i++) { 03225 if (varOccur[i] == 0) 03226 continue; 03227 if (size < array_n(vector) && 03228 st_lookup(info->intermediateVarsTable, (char *)(long)i, 03229 NIL(char *))) { 03230 continue; 03231 } 03232 var = bdd_var_with_index(info->manager, i); 03233 for (j = 0; j < array_n(vector); j++) { 03234 comp = array_fetch(ImgComponent_t *, vector, j); 03235 varCost[i] += bdd_estimate_cofactor(comp->func, var, 1); 03236 varCost[i] += bdd_estimate_cofactor(comp->func, var, 0); 03237 } 03238 if (decompose == 0) { 03239 varCost[i] += bdd_estimate_cofactor(from, var, 1); 03240 varCost[i] += bdd_estimate_cofactor(from, var, 0); 03241 } 03242 mdd_free(var); 03243 03244 if (varCost[i] < bestCost) { 03245 bestCost = varCost[i]; 03246 bestVar = i; 03247 } else if (varCost[i] == bestCost) { 03248 if (varOccur[i] < varOccur[bestVar]) { 03249 bestVar = i; 03250 } else if (varOccur[i] == varOccur[bestVar]) { 03251 if (bdd_get_level_from_id(info->manager, i) < 03252 bdd_get_level_from_id(info->manager, bestVar)) { 03253 bestVar = i; 03254 } 03255 } 03256 } 03257 } 03258 break; 03259 case 3: /* top variable */ 03260 for (i = 0; i < nVars; i++) { 03261 if (varOccur[i] == 0) 03262 continue; 03263 if (size < array_n(vector) && 03264 st_lookup(info->intermediateVarsTable, (char *)(long)i, 03265 NIL(char *))) { 03266 continue; 03267 } 03268 if (piSplitFlag == 0) { 03269 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, 03270 NIL(char *))) { 03271 if (bestVar == -1 && secondBestVar == -1) 03272 secondBestVar = i; 03273 else if (bdd_get_level_from_id(info->manager, i) < 03274 bdd_get_level_from_id(info->manager, secondBestVar)) { 03275 secondBestVar = i; 03276 } 03277 continue; 03278 } 03279 } 03280 if (bestVar == -1 || 03281 bdd_get_level_from_id(info->manager, i) < 03282 bdd_get_level_from_id(info->manager, bestVar)) { 03283 bestVar = i; 03284 } 03285 } 03286 03287 if (piSplitFlag == 0 && bestVar == -1) 03288 bestVar = secondBestVar; 03289 break; 03290 default: 03291 break; 03292 } 03293 03294 if (varCost) 03295 FREE(varCost); 03296 03297 return(bestVar); 03298 } 03299 03300 03310 static int 03311 ChooseOutputSplittingVariable(ImgTfmInfo_t *info, array_t *vector, 03312 int splitMethod) 03313 { 03314 int bestVar = -1; 03315 int bestCost, newCost; 03316 int i; 03317 ImgComponent_t *comp; 03318 int size = ImgVectorFunctionSize(vector); 03319 int index; 03320 03321 switch (splitMethod) { 03322 case 0: /* smallest */ 03323 bestCost = IMG_TF_MAX_INT; 03324 for (i = 0; i < array_n(vector); i++) { 03325 comp = array_fetch(ImgComponent_t *, vector, i); 03326 if (size < array_n(vector) && 03327 st_lookup(info->intermediateVarsTable, 03328 (char *)(long)bdd_top_var_id(comp->var), NIL(char *))) { 03329 continue; 03330 } 03331 newCost = bdd_size(comp->func); 03332 if (newCost < bestCost) { 03333 bestVar = i; 03334 bestCost = newCost; 03335 } 03336 } 03337 break; 03338 case 1: /* largest */ 03339 bestCost = 0; 03340 for (i = 0; i < array_n(vector); i++) { 03341 comp = array_fetch(ImgComponent_t *, vector, i); 03342 if (size < array_n(vector) && 03343 st_lookup(info->intermediateVarsTable, 03344 (char *)(long)bdd_top_var_id(comp->var), NIL(char *))) { 03345 continue; 03346 } 03347 newCost = bdd_size(comp->func); 03348 if (newCost > bestCost) { 03349 bestVar = i; 03350 bestCost = newCost; 03351 } 03352 } 03353 break; 03354 case 2: /* top variable */ 03355 default: 03356 comp = array_fetch(ImgComponent_t *, vector, 0); 03357 bestVar = (int)bdd_top_var_id(comp->var); 03358 for (i = 0; i < array_n(vector); i++) { 03359 comp = array_fetch(ImgComponent_t *, vector, i); 03360 index = (int)bdd_top_var_id(comp->var); 03361 if (size < array_n(vector) && 03362 st_lookup(info->intermediateVarsTable, (char *)(long)index, 03363 NIL(char *))) { 03364 continue; 03365 } 03366 if (bestVar == -1 || 03367 bdd_get_level_from_id(info->manager, index) < 03368 bdd_get_level_from_id(info->manager, bestVar)) { 03369 bestVar = i; 03370 } 03371 } 03372 break; 03373 } 03374 03375 return(bestVar); 03376 }
1.7.3