- Generated on Wed Oct 12 2011 00:34:49 for VIS by
1.7.3
|
VIS
|
00001 00036 #include "imgInt.h" 00037 00038 static char rcsid[] UNUSED = "$Id: imgTfmBwd.c,v 1.29 2002/08/18 04:47:07 fabio Exp $"; 00039 00040 /*---------------------------------------------------------------------------*/ 00041 /* Constant declarations */ 00042 /*---------------------------------------------------------------------------*/ 00043 00044 /*---------------------------------------------------------------------------*/ 00045 /* Type declarations */ 00046 /*---------------------------------------------------------------------------*/ 00047 00048 /*---------------------------------------------------------------------------*/ 00049 /* Structure declarations */ 00050 /*---------------------------------------------------------------------------*/ 00051 00052 /*---------------------------------------------------------------------------*/ 00053 /* Variable declarations */ 00054 /*---------------------------------------------------------------------------*/ 00055 00056 /*---------------------------------------------------------------------------*/ 00057 /* Macro declarations */ 00058 /*---------------------------------------------------------------------------*/ 00059 00062 /*---------------------------------------------------------------------------*/ 00063 /* Static function prototypes */ 00064 /*---------------------------------------------------------------------------*/ 00065 00066 static bdd_t * PreImageByDomainCofactoring(ImgTfmInfo_t *info, array_t *delta, bdd_t *image, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int splitMethod, int turnDepth, int depth); 00067 static mdd_t * PreImageByStaticDomainCofactoring(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, int turnDepth, int depth); 00068 static bdd_t * PreImageByConstraintCofactoring(ImgTfmInfo_t *info, array_t *delta, bdd_t *image, int splitMethod, int turnDepth, int depth); 00069 static mdd_t * PreImageBySubstitution(ImgTfmInfo_t *info, array_t *vector, mdd_t *from); 00070 static bdd_t * PreImageMakeVectorCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image, array_t *relationArray, array_t **newVector, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube); 00071 static bdd_t * PreImageMakeRelationCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image, array_t *relationArray, array_t **newVector, array_t **newRelationArray); 00072 static bdd_t * PreImageDeleteOneComponent(ImgTfmInfo_t *info, array_t *delta, int index, array_t **newDelta); 00073 static int PreImageChooseSplitVar(ImgTfmInfo_t *info, array_t *delta, bdd_t *img, int splitMethod, int split); 00074 static mdd_t * DomainCofactoring(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, mdd_t *c, array_t **newVector, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube); 00075 static int CheckPreImageVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *image); 00076 00080 /*---------------------------------------------------------------------------*/ 00081 /* Definition of exported functions */ 00082 /*---------------------------------------------------------------------------*/ 00083 00084 00085 /*---------------------------------------------------------------------------*/ 00086 /* Definition of internal functions */ 00087 /*---------------------------------------------------------------------------*/ 00088 00089 00099 bdd_t * 00100 ImgTfmPreImage(ImgTfmInfo_t *info, bdd_t *image) 00101 { 00102 bdd_t *preImg, *pre; 00103 int turnDepth; 00104 bdd_t *refResult, *one; 00105 array_t *relationArray; 00106 int partial; 00107 bdd_t *from; 00108 array_t *vector; 00109 00110 if (bdd_is_tautology(image, 1)) { 00111 preImg = mdd_one(info->manager); 00112 return(preImg); 00113 } else if (bdd_is_tautology(image, 0)) { 00114 preImg = mdd_zero(info->manager); 00115 return(preImg); 00116 } 00117 00118 info->maxIntermediateSize = 0; 00119 if (info->buildTR) { 00120 if (info->option->preSplitMethod == 4 && 00121 info->option->preSplitMaxDepth < 0 && 00122 info->option->buildPartialTR == FALSE && 00123 info->preKeepPiInTr == FALSE && 00124 info->option->preCanonical == FALSE) { 00125 mdd_t *range; 00126 range = ImgSubstitute(image, info->functionData, Img_D2R_c); 00127 preImg = ImgBddLinearAndSmooth(info->manager, range, 00128 info->bwdClusteredRelationArray, 00129 info->bwdArraySmoothVarBddArray, 00130 info->bwdSmoothVarCubeArray, 00131 info->option->verbosity); 00132 mdd_free(range); 00133 return(preImg); 00134 } 00135 relationArray = mdd_array_duplicate(info->bwdClusteredRelationArray); 00136 } else 00137 relationArray = NIL(array_t); 00138 00139 one = mdd_one(info->manager); 00140 00141 vector = info->vector; 00142 from = image; 00143 00144 partial = 0; 00145 if (info->option->preSplitMethod == 0) { 00146 preImg = PreImageByDomainCofactoring(info, vector, from, 00147 NIL(array_t), NIL(mdd_t), NIL(mdd_t), 00148 info->option->preSplitMethod, 0, 0); 00149 } else if (info->option->preSplitMethod == 1) { 00150 preImg = PreImageByConstraintCofactoring(info, vector, from, 00151 info->option->preSplitMethod, 00152 0, 0); 00153 } else if (info->option->preSplitMethod == 3) { 00154 preImg = PreImageBySubstitution(info, vector, from); 00155 } else { 00156 turnDepth = info->option->turnDepth; 00157 if (turnDepth == 0) { 00158 if (info->option->preSplitMethod == 2) { 00159 preImg = PreImageByConstraintCofactoring(info, vector, from, 00160 info->option->preSplitMethod, 00161 turnDepth, 0); 00162 } else 00163 preImg = ImgPreImageByHybrid(info, vector, from); 00164 } else if (info->option->preSplitMethod == 2) { 00165 preImg = PreImageByDomainCofactoring(info, vector, from, 00166 relationArray, 00167 NIL(mdd_t), NIL(mdd_t), 00168 info->option->preSplitMethod, 00169 turnDepth, 0); 00170 } else { 00171 if (info->buildTR) { 00172 if (info->buildTR == 2) { 00173 if (info->buildPartialTR) { 00174 preImg = PreImageByStaticDomainCofactoring(info, vector, 00175 from, relationArray, 00176 turnDepth, 0); 00177 partial = 1; 00178 } else { 00179 preImg = PreImageByStaticDomainCofactoring(info, NIL(array_t), 00180 from, relationArray, 00181 turnDepth, 0); 00182 } 00183 } else if (info->option->delayedSplit) { 00184 preImg = PreImageByDomainCofactoring(info, vector, from, 00185 relationArray, one, one, 00186 info->option->preSplitMethod, 00187 turnDepth, 0); 00188 } else { 00189 preImg = PreImageByDomainCofactoring(info, vector, from, 00190 relationArray, 00191 NIL(mdd_t), NIL(mdd_t), 00192 info->option->preSplitMethod, 00193 turnDepth, 0); 00194 } 00195 } else { 00196 preImg = PreImageByDomainCofactoring(info, vector, from, 00197 relationArray, 00198 NIL(mdd_t), NIL(mdd_t), 00199 info->option->preSplitMethod, 00200 turnDepth, 0); 00201 } 00202 } 00203 } 00204 mdd_free(one); 00205 00206 if (info->option->debug) { 00207 if (info->buildTR == 2) { 00208 refResult = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), 00209 image, relationArray, 00210 NIL(mdd_t), NIL(mdd_t)); 00211 } else { 00212 if (partial) { 00213 refResult = ImgPreImageByHybridWithStaticSplit(info, info->vector, 00214 image, relationArray, 00215 NIL(mdd_t), NIL(mdd_t)); 00216 } else 00217 refResult = ImgPreImageByHybrid(info, info->vector, image); 00218 } 00219 assert(mdd_equal_mod_care_set_array(refResult, preImg, 00220 info->toCareSetArray)); 00221 mdd_free(refResult); 00222 } 00223 00224 if (relationArray) 00225 mdd_array_free(relationArray); 00226 00227 if (info->preCache && info->option->autoFlushCache == 1) 00228 ImgFlushCache(info->preCache); 00229 if (info->preKeepPiInTr == TRUE) { 00230 if (info->functionData->quantifyCube) 00231 pre = bdd_smooth_with_cube(preImg, info->functionData->quantifyCube); 00232 else 00233 pre = bdd_smooth(preImg, info->functionData->quantifyBddVars); 00234 mdd_free(preImg); 00235 } else 00236 pre = preImg; 00237 if (info->option->verbosity) { 00238 fprintf(vis_stdout, 00239 "** tfm info: max BDD size for intermediate product = %d\n", 00240 info->maxIntermediateSize); 00241 } 00242 return(pre); 00243 } 00244 00245 00246 /*---------------------------------------------------------------------------*/ 00247 /* Definition of static functions */ 00248 /*---------------------------------------------------------------------------*/ 00249 00250 00260 static bdd_t * 00261 PreImageByDomainCofactoring(ImgTfmInfo_t *info, array_t *delta, bdd_t *image, 00262 array_t *relationArray, 00263 mdd_t *cofactorCube, mdd_t *abstractCube, 00264 int splitMethod, int turnDepth, int depth) 00265 { 00266 array_t *newDelta, *tmpDelta, *vectorT, *vectorE; 00267 bdd_t *preImg, *preImgT, *preImgE, *imgT, *imgE, *newImg, *tmpImg; 00268 int split; 00269 bdd_t *var, *varNot, *refResult; 00270 int nRecur; 00271 array_t *relationArrayT, *relationArrayE; 00272 array_t *newRelationArray, *tmpRelationArray; 00273 mdd_t *cofactorCubeT, *cofactorCubeE; 00274 mdd_t *abstractCubeT, *abstractCubeE; 00275 mdd_t *newCofactorCube, *newAbstractCube; 00276 mdd_t *cofactor, *abstract; 00277 mdd_t *essentialCube, *tmp; 00278 int findEssential; 00279 int foundEssentialDepth, foundEssentialDepthT, foundEssentialDepthE; 00280 int turnFlag, size; 00281 mdd_t *saveCareSet = NIL(mdd_t); 00282 00283 newRelationArray = NIL(array_t); 00284 00285 if (info->option->checkEquivalence && relationArray) { 00286 assert(ImgCheckEquivalence(info, delta, relationArray, 00287 cofactorCube, abstractCube, 1)); 00288 } 00289 00290 info->nRecursionB++; 00291 if (info->option->debug) { 00292 if (relationArray) { 00293 refResult = ImgPreImageByHybrid(info, delta, image); 00294 preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), image, 00295 relationArray, 00296 cofactorCube, abstractCube); 00297 tmp = refResult; 00298 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 00299 mdd_free(tmp); 00300 tmp = preImg; 00301 preImg = mdd_and(tmp, info->debugCareSet, 1, 1); 00302 mdd_free(tmp); 00303 assert(mdd_equal_mod_care_set_array(refResult, preImg, 00304 info->toCareSetArray)); 00305 mdd_free(refResult); 00306 mdd_free(preImg); 00307 } 00308 } 00309 00310 if (info->nIntermediateVars) 00311 size = ImgVectorFunctionSize(delta); 00312 else 00313 size = array_n(delta); 00314 if (size == 1) { 00315 preImg = PreImageBySubstitution(info, delta, image); 00316 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 00317 (float)depth) / (float)(info->nLeavesB + 1); 00318 if (depth > info->maxDepthB) 00319 info->maxDepthB = depth; 00320 info->nLeavesB++; 00321 info->foundEssentialDepth = info->option->maxEssentialDepth; 00322 return(preImg); 00323 } 00324 00325 if (info->option->findEssential) { 00326 if (info->option->findEssential == 1) 00327 findEssential = 1; 00328 else { 00329 if (depth >= info->lastFoundEssentialDepth) 00330 findEssential = 1; 00331 else 00332 findEssential = 0; 00333 } 00334 } else 00335 findEssential = 0; 00336 if (findEssential) { 00337 essentialCube = bdd_find_essential_cube(image); 00338 00339 if (!bdd_is_tautology(essentialCube, 1)) { 00340 info->averageFoundEssential = (info->averageFoundEssential * 00341 (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) / 00342 (float)(info->nFoundEssentials + 1); 00343 info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth * 00344 (float)info->nFoundEssentials + (float)depth) / 00345 (float)(info->nFoundEssentials + 1); 00346 if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth) 00347 info->topFoundEssentialDepth = depth; 00348 if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH) 00349 info->foundEssentials[depth]++; 00350 info->nFoundEssentials++; 00351 if (info->option->delayedSplit && relationArray) { 00352 tmpRelationArray = relationArray; 00353 tmpImg = ImgVectorMinimize(info, delta, essentialCube, image, 00354 tmpRelationArray, &tmpDelta, NIL(mdd_t *), 00355 NIL(array_t *), &cofactor, &abstract); 00356 if (bdd_is_tautology(cofactor, 1)) 00357 newCofactorCube = cofactorCube; 00358 else 00359 newCofactorCube = mdd_and(cofactorCube, cofactor, 1, 1); 00360 mdd_free(cofactor); 00361 if (bdd_is_tautology(abstract, 1)) 00362 newAbstractCube = abstractCube; 00363 else 00364 newAbstractCube = mdd_and(abstractCube, abstract, 1, 1); 00365 mdd_free(abstract); 00366 } else { 00367 if (relationArray) 00368 tmpRelationArray = mdd_array_duplicate(relationArray); 00369 else 00370 tmpRelationArray = relationArray; 00371 tmpImg = ImgVectorMinimize(info, delta, essentialCube, image, 00372 tmpRelationArray, &tmpDelta, NIL(mdd_t *), 00373 NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *)); 00374 newCofactorCube = cofactorCube; 00375 newAbstractCube = abstractCube; 00376 } 00377 foundEssentialDepth = depth; 00378 } else { 00379 tmpDelta = delta; 00380 tmpRelationArray = relationArray; 00381 tmpImg = image; 00382 newCofactorCube = cofactorCube; 00383 newAbstractCube = abstractCube; 00384 foundEssentialDepth = info->option->maxEssentialDepth; 00385 } 00386 mdd_free(essentialCube); 00387 foundEssentialDepthT = info->option->maxEssentialDepth; 00388 foundEssentialDepthE = info->option->maxEssentialDepth; 00389 } else { 00390 tmpDelta = delta; 00391 tmpRelationArray = relationArray; 00392 tmpImg = image; 00393 newCofactorCube = cofactorCube; 00394 newAbstractCube = abstractCube; 00395 /* To remove compiler warnings */ 00396 foundEssentialDepth = -1; 00397 foundEssentialDepthT = -1; 00398 foundEssentialDepthE = -1; 00399 } 00400 00401 if (!info->option->preCanonical) { 00402 newImg = tmpImg; 00403 newDelta = tmpDelta; 00404 newRelationArray = tmpRelationArray; 00405 } else if (info->option->delayedSplit && relationArray) { 00406 newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg, 00407 tmpRelationArray, &newDelta, 00408 &newRelationArray, 00409 &cofactor, &abstract); 00410 if (!bdd_is_tautology(cofactor, 1)) { 00411 if (newCofactorCube == cofactorCube) 00412 newCofactorCube = mdd_and(cofactorCube, cofactor, 1, 1); 00413 else { 00414 tmp = newCofactorCube; 00415 newCofactorCube = mdd_and(tmp, cofactor, 1, 1); 00416 mdd_free(tmp); 00417 } 00418 } 00419 mdd_free(cofactor); 00420 if (!bdd_is_tautology(abstract, 1)) { 00421 if (newAbstractCube == abstractCube) 00422 newAbstractCube = mdd_and(abstractCube, abstract, 1, 1); 00423 else { 00424 tmp = newAbstractCube; 00425 newAbstractCube = mdd_and(tmp, abstract, 1, 1); 00426 mdd_free(tmp); 00427 } 00428 } 00429 mdd_free(abstract); 00430 } else { 00431 newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg, 00432 tmpRelationArray, &newDelta, 00433 &newRelationArray, 00434 NIL(mdd_t *), NIL(mdd_t *)); 00435 } 00436 if (tmpDelta != delta) 00437 ImgVectorFree(tmpDelta); 00438 if (tmpImg != image) 00439 mdd_free(tmpImg); 00440 if (tmpRelationArray && tmpRelationArray != relationArray && 00441 tmpRelationArray != newRelationArray) { 00442 mdd_array_free(tmpRelationArray); 00443 } 00444 00445 if (info->option->debug) { 00446 if (relationArray) { 00447 refResult = ImgPreImageByHybrid(info, newDelta, newImg); 00448 preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg, 00449 newRelationArray, 00450 newCofactorCube, 00451 newAbstractCube); 00452 tmp = refResult; 00453 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 00454 mdd_free(tmp); 00455 tmp = preImg; 00456 preImg = mdd_and(tmp, info->debugCareSet, 1, 1); 00457 mdd_free(tmp); 00458 assert(mdd_equal_mod_care_set_array(refResult, preImg, 00459 info->toCareSetArray)); 00460 mdd_free(refResult); 00461 mdd_free(preImg); 00462 } 00463 } 00464 00465 if (bdd_is_tautology(newImg, 1) || bdd_is_tautology(newImg, 0)) { 00466 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 00467 (float)depth) / (float)(info->nLeavesB + 1); 00468 if (depth > info->maxDepthB) 00469 info->maxDepthB = depth; 00470 info->nLeavesB++; 00471 if (info->option->debug) { 00472 refResult = ImgPreImageByHybrid(info, newDelta, newImg); 00473 tmp = refResult; 00474 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 00475 mdd_free(tmp); 00476 tmp = mdd_and(newImg, info->debugCareSet, 1, 1); 00477 assert(mdd_equal_mod_care_set_array(refResult, tmp, 00478 info->toCareSetArray)); 00479 mdd_free(refResult); 00480 mdd_free(tmp); 00481 } 00482 if (newDelta != delta) 00483 ImgVectorFree(newDelta); 00484 if (relationArray && newRelationArray != relationArray) 00485 mdd_array_free(newRelationArray); 00486 if (newCofactorCube && newCofactorCube != cofactorCube) 00487 mdd_free(newCofactorCube); 00488 if (newAbstractCube && newAbstractCube != abstractCube) 00489 mdd_free(newAbstractCube); 00490 if (findEssential) 00491 info->foundEssentialDepth = foundEssentialDepth; 00492 return(newImg); 00493 } 00494 if (array_n(newDelta) <= 1) { 00495 if (array_n(newDelta) == 0) 00496 preImg = newImg; 00497 else { 00498 assert(array_n(newDelta) == 1); 00499 preImg = PreImageBySubstitution(info, newDelta, newImg); 00500 mdd_free(newImg); 00501 } 00502 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 00503 (float)depth) / (float)(info->nLeavesB + 1); 00504 if (depth > info->maxDepthB) 00505 info->maxDepthB = depth; 00506 info->nLeavesB++; 00507 if (info->option->debug) { 00508 refResult = ImgPreImageByHybrid(info, delta, image); 00509 tmp = refResult; 00510 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 00511 mdd_free(tmp); 00512 tmp = mdd_and(preImg, info->debugCareSet, 1, 1); 00513 assert(mdd_equal_mod_care_set_array(refResult, tmp, 00514 info->toCareSetArray)); 00515 mdd_free(refResult); 00516 mdd_free(tmp); 00517 } 00518 if (newDelta != delta) 00519 ImgVectorFree(newDelta); 00520 if (relationArray && newRelationArray != relationArray) 00521 mdd_array_free(newRelationArray); 00522 if (newCofactorCube && newCofactorCube != cofactorCube) 00523 mdd_free(newCofactorCube); 00524 if (newAbstractCube && newAbstractCube != abstractCube) 00525 mdd_free(newAbstractCube); 00526 if (findEssential) 00527 info->foundEssentialDepth = foundEssentialDepth; 00528 return(preImg); 00529 } 00530 00531 if (info->preCache) { 00532 preImg = ImgCacheLookupTable(info, info->preCache, newDelta, newImg); 00533 if (preImg) { 00534 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 00535 (float)depth) / (float)(info->nLeavesB + 1); 00536 if (depth > info->maxDepthB) 00537 info->maxDepthB = depth; 00538 info->nLeavesB++; 00539 if (info->option->debug) { 00540 refResult = ImgPreImageByHybrid(info, newDelta, newImg); 00541 tmp = refResult; 00542 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 00543 mdd_free(tmp); 00544 tmp = mdd_and(preImg, info->debugCareSet, 1, 1); 00545 assert(mdd_equal_mod_care_set_array(refResult, tmp, 00546 info->toCareSetArray)); 00547 mdd_free(refResult); 00548 mdd_free(tmp); 00549 } 00550 if (newDelta != delta) 00551 ImgVectorFree(newDelta); 00552 if (newImg != image) 00553 mdd_free(newImg); 00554 if (relationArray && newRelationArray != relationArray) 00555 mdd_array_free(newRelationArray); 00556 if (newCofactorCube && newCofactorCube != cofactorCube) 00557 mdd_free(newCofactorCube); 00558 if (newAbstractCube && newAbstractCube != abstractCube) 00559 mdd_free(newAbstractCube); 00560 if (findEssential) 00561 info->foundEssentialDepth = foundEssentialDepth; 00562 return(preImg); 00563 } 00564 } 00565 00566 turnFlag = 0; 00567 if (splitMethod == 4 && turnDepth == -1) { 00568 if (depth < info->option->preSplitMinDepth) { 00569 info->nSplitsB++; 00570 turnFlag = 0; 00571 } else if (depth > info->option->preSplitMaxDepth) { 00572 info->nConjoinsB++; 00573 turnFlag = 1; 00574 } else { 00575 turnFlag = ImgDecideSplitOrConjoin(info, newDelta, newImg, 1, 00576 newRelationArray, newCofactorCube, 00577 newAbstractCube, 0, depth); 00578 } 00579 } else { 00580 if (depth == turnDepth) 00581 turnFlag = 1; 00582 else 00583 turnFlag = 0; 00584 } 00585 if (turnFlag) { 00586 if (splitMethod == 2) { 00587 preImg = PreImageByConstraintCofactoring(info, newDelta, newImg, 00588 info->option->preSplitMethod, 00589 0, depth + 1); 00590 } else { 00591 if (relationArray) { 00592 preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg, 00593 newRelationArray, 00594 newCofactorCube, 00595 newAbstractCube); 00596 } else 00597 preImg = ImgPreImageByHybrid(info, newDelta, newImg); 00598 } 00599 if (info->option->debug) { 00600 refResult = ImgPreImageByHybrid(info, newDelta, newImg); 00601 tmp = refResult; 00602 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 00603 mdd_free(tmp); 00604 tmp = mdd_and(preImg, info->debugCareSet, 1, 1); 00605 assert(mdd_equal_mod_care_set_array(refResult, tmp, 00606 info->toCareSetArray)); 00607 mdd_free(refResult); 00608 mdd_free(tmp); 00609 } 00610 if (splitMethod == 4) { 00611 if (info->preCache) 00612 ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg)); 00613 else { 00614 if (newDelta != delta) 00615 ImgVectorFree(newDelta); 00616 if (newImg != image) 00617 mdd_free(newImg); 00618 } 00619 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 00620 (float)depth) / (float)(info->nLeavesB + 1); 00621 if (depth > info->maxDepthB) 00622 info->maxDepthB = depth; 00623 info->nLeavesB++; 00624 } else { 00625 if (newDelta != delta) 00626 ImgVectorFree(newDelta); 00627 if (newImg != image) 00628 mdd_free(newImg); 00629 } 00630 if (relationArray && newRelationArray != relationArray) 00631 mdd_array_free(newRelationArray); 00632 if (newCofactorCube && newCofactorCube != cofactorCube) 00633 mdd_free(newCofactorCube); 00634 if (newAbstractCube && newAbstractCube != abstractCube) 00635 mdd_free(newAbstractCube); 00636 info->nTurnsB++; 00637 if (findEssential) 00638 info->foundEssentialDepth = foundEssentialDepth; 00639 return(preImg); 00640 } 00641 00642 split = PreImageChooseSplitVar(info, newDelta, newImg, 00643 0, info->option->preInputSplit); 00644 00645 /* No more present state variable to split */ 00646 if (split == -1) { 00647 if (info->option->preDcLeafMethod == 0 || 00648 info->option->preDcLeafMethod == 2) { 00649 if (info->option->preDcLeafMethod == 0) 00650 preImg = PreImageBySubstitution(info, newDelta, newImg); 00651 else if (relationArray) { 00652 preImg = ImgPreImageByHybridWithStaticSplit(info, NIL(array_t), newImg, 00653 newRelationArray, 00654 newCofactorCube, 00655 newAbstractCube); 00656 } else 00657 preImg = ImgPreImageByHybrid(info, newDelta, newImg); 00658 if (info->preCache) 00659 ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg)); 00660 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 00661 (float)depth) / (float)(info->nLeavesB + 1); 00662 if (depth > info->maxDepthB) 00663 info->maxDepthB = depth; 00664 info->nLeavesB++; 00665 } else { 00666 preImg = PreImageByConstraintCofactoring(info, newDelta, newImg, 00667 splitMethod, turnDepth, 00668 depth + 1); 00669 info->nRecursionB--; 00670 } 00671 if (splitMethod == 0) 00672 info->nTurnsB++; 00673 if (info->option->debug) { 00674 refResult = ImgPreImageByHybrid(info, newDelta, newImg); 00675 tmp = refResult; 00676 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 00677 mdd_free(tmp); 00678 tmp = mdd_and(preImg, info->debugCareSet, 1, 1); 00679 assert(mdd_equal_mod_care_set_array(refResult, tmp, 00680 info->toCareSetArray)); 00681 mdd_free(refResult); 00682 mdd_free(tmp); 00683 } 00684 if (info->option->preDcLeafMethod != 0 || !info->preCache) { 00685 if (newDelta != delta) 00686 ImgVectorFree(newDelta); 00687 if (newImg != image) 00688 mdd_free(newImg); 00689 } 00690 if (relationArray && newRelationArray != relationArray) 00691 mdd_array_free(newRelationArray); 00692 if (newCofactorCube && newCofactorCube != cofactorCube) 00693 mdd_free(newCofactorCube); 00694 if (newAbstractCube && newAbstractCube != abstractCube) 00695 mdd_free(newAbstractCube); 00696 if (findEssential) 00697 info->foundEssentialDepth = foundEssentialDepth; 00698 return(preImg); 00699 } 00700 00701 var = bdd_var_with_index(info->manager, split); 00702 varNot = mdd_not(var); 00703 if (info->option->delayedSplit && relationArray) { 00704 imgT = DomainCofactoring(info, newDelta, newImg, newRelationArray, var, 00705 &vectorT, &relationArrayT, &cofactor, &abstract); 00706 if (bdd_is_tautology(cofactor, 1)) 00707 cofactorCubeT = newCofactorCube; 00708 else 00709 cofactorCubeT = mdd_and(newCofactorCube, cofactor, 1, 1); 00710 mdd_free(cofactor); 00711 if (bdd_is_tautology(abstract, 1)) 00712 abstractCubeT = newAbstractCube; 00713 else 00714 abstractCubeT = mdd_and(newAbstractCube, abstract, 1, 1); 00715 mdd_free(abstract); 00716 00717 imgE = DomainCofactoring(info, newDelta, newImg, newRelationArray, varNot, 00718 &vectorE, &relationArrayE, &cofactor, &abstract); 00719 if (bdd_is_tautology(cofactor, 1)) 00720 cofactorCubeE = newCofactorCube; 00721 else 00722 cofactorCubeE = mdd_and(newCofactorCube, cofactor, 1, 1); 00723 mdd_free(cofactor); 00724 if (bdd_is_tautology(abstract, 1)) 00725 abstractCubeE = newAbstractCube; 00726 else 00727 abstractCubeE = mdd_and(newAbstractCube, abstract, 1, 1); 00728 mdd_free(abstract); 00729 } else { 00730 imgT = DomainCofactoring(info, newDelta, newImg, newRelationArray, var, 00731 &vectorT, &relationArrayT, 00732 NIL(mdd_t *), NIL(mdd_t *)); 00733 cofactorCubeT = NIL(mdd_t); 00734 abstractCubeT = NIL(mdd_t); 00735 00736 imgE = DomainCofactoring(info, newDelta, newImg, newRelationArray, varNot, 00737 &vectorE, &relationArrayE, 00738 NIL(mdd_t *), NIL(mdd_t *)); 00739 cofactorCubeE = NIL(mdd_t); 00740 abstractCubeE = NIL(mdd_t); 00741 } 00742 if (relationArray && newRelationArray != relationArray) 00743 mdd_array_free(newRelationArray); 00744 mdd_free(varNot); 00745 00746 if (!info->preCache && !info->option->debug) { 00747 if (newDelta != delta) 00748 ImgVectorFree(newDelta); 00749 if (newImg != image) 00750 mdd_free(newImg); 00751 } 00752 00753 nRecur = 0; 00754 if (bdd_is_tautology(imgT, 1)) 00755 preImgT = mdd_one(info->manager); 00756 else if (bdd_is_tautology(imgT, 0)) 00757 preImgT = mdd_zero(info->manager); 00758 else { 00759 if (info->option->debug) { 00760 saveCareSet = info->debugCareSet; 00761 info->debugCareSet = mdd_and(saveCareSet, var, 1, 1); 00762 } 00763 preImgT = PreImageByDomainCofactoring(info, vectorT, imgT, relationArrayT, 00764 cofactorCubeT, abstractCubeT, 00765 splitMethod, turnDepth, 00766 depth + 1); 00767 if (info->option->debug) { 00768 mdd_free(info->debugCareSet); 00769 info->debugCareSet = saveCareSet; 00770 } 00771 if (findEssential) 00772 foundEssentialDepthT = info->foundEssentialDepth; 00773 nRecur++; 00774 } 00775 ImgVectorFree(vectorT); 00776 mdd_free(imgT); 00777 if (relationArrayT && relationArrayT != newRelationArray) 00778 mdd_array_free(relationArrayT); 00779 if (cofactorCubeT && cofactorCubeT != newCofactorCube) 00780 mdd_free(cofactorCubeT); 00781 if (abstractCubeT && abstractCubeT != newAbstractCube) 00782 mdd_free(abstractCubeT); 00783 00784 if (bdd_is_tautology(imgE, 1)) 00785 preImgE = mdd_one(info->manager); 00786 else if (bdd_is_tautology(imgE, 0)) 00787 preImgE = mdd_zero(info->manager); 00788 else { 00789 if (info->option->debug) { 00790 saveCareSet = info->debugCareSet; 00791 info->debugCareSet = mdd_and(saveCareSet, var, 1, 0); 00792 } 00793 preImgE = PreImageByDomainCofactoring(info, vectorE, imgE, relationArrayE, 00794 cofactorCubeE, abstractCubeE, 00795 splitMethod, turnDepth, 00796 depth + 1); 00797 if (info->option->debug) { 00798 mdd_free(info->debugCareSet); 00799 info->debugCareSet = saveCareSet; 00800 } 00801 if (findEssential) 00802 foundEssentialDepthE = info->foundEssentialDepth; 00803 nRecur++; 00804 } 00805 ImgVectorFree(vectorE); 00806 mdd_free(imgE); 00807 if (relationArrayE && relationArrayT != newRelationArray) 00808 mdd_array_free(relationArrayE); 00809 if (cofactorCubeE && cofactorCubeE != newCofactorCube) 00810 mdd_free(cofactorCubeE); 00811 if (abstractCubeE && abstractCubeE != newAbstractCube) 00812 mdd_free(abstractCubeE); 00813 if (newCofactorCube && newCofactorCube != cofactorCube) 00814 mdd_free(newCofactorCube); 00815 if (newAbstractCube && newAbstractCube != abstractCube) 00816 mdd_free(newAbstractCube); 00817 00818 preImg = bdd_ite(var, preImgT, preImgE, 1, 1, 1); 00819 if (info->option->verbosity) { 00820 size = bdd_size(preImg); 00821 if (size > info->maxIntermediateSize) 00822 info->maxIntermediateSize = size; 00823 if (info->option->printBddSize) { 00824 fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n", 00825 bdd_size(preImgT), bdd_size(preImgE), bdd_size(preImg)); 00826 } 00827 } 00828 mdd_free(var); 00829 mdd_free(preImgE); 00830 mdd_free(preImgT); 00831 00832 if (info->preCache) 00833 ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg)); 00834 00835 if (info->option->debug) { 00836 refResult = ImgPreImageByHybrid(info, newDelta, newImg); 00837 tmp = refResult; 00838 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 00839 mdd_free(tmp); 00840 tmp = mdd_and(preImg, info->debugCareSet, 1, 1); 00841 assert(mdd_equal_mod_care_set_array(refResult, tmp, 00842 info->toCareSetArray)); 00843 mdd_free(refResult); 00844 mdd_free(tmp); 00845 if (!info->preCache) { 00846 if (newDelta != delta) 00847 ImgVectorFree(newDelta); 00848 if (newImg != image) 00849 mdd_free(newImg); 00850 } 00851 } 00852 00853 if (nRecur == 0) { 00854 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 00855 (float)depth) / (float)(info->nLeavesB + 1); 00856 if (depth > info->maxDepthB) 00857 info->maxDepthB = depth; 00858 info->nLeavesB++; 00859 } 00860 00861 if (findEssential) { 00862 if (foundEssentialDepth == info->option->maxEssentialDepth) { 00863 if (foundEssentialDepthT < foundEssentialDepthE) 00864 foundEssentialDepth = foundEssentialDepthT; 00865 else 00866 foundEssentialDepth = foundEssentialDepthE; 00867 } 00868 info->foundEssentialDepth = foundEssentialDepth; 00869 } 00870 return(preImg); 00871 } 00872 00873 00883 static mdd_t * 00884 PreImageByStaticDomainCofactoring(ImgTfmInfo_t *info, array_t *vector, 00885 mdd_t *from, array_t *relationArray, 00886 int turnDepth, int depth) 00887 { 00888 array_t *vectorT, *vectorE, *newVector; 00889 mdd_t *resT, *resE, *res, *cubeT, *cubeE; 00890 mdd_t *fromT, *fromE, *newFrom, *tmpFrom; 00891 mdd_t *var, *varNot; 00892 array_t *relationArrayT, *relationArrayE; 00893 array_t *newRelationArray, *tmpRelationArray; 00894 int nRecur; 00895 mdd_t *essentialCube, *refResult; 00896 int findEssential; 00897 int foundEssentialDepth, foundEssentialDepthT, foundEssentialDepthE; 00898 int turnFlag, size; 00899 mdd_t *saveCareSet = NIL(mdd_t), *tmp; 00900 00901 info->nRecursionB++; 00902 00903 turnFlag = 0; 00904 if (turnDepth == -1) { 00905 if (depth < info->option->preSplitMinDepth) { 00906 info->nSplitsB++; 00907 turnFlag = 0; 00908 } else if (depth > info->option->preSplitMaxDepth) { 00909 info->nConjoinsB++; 00910 turnFlag = 1; 00911 } else { 00912 turnFlag = ImgDecideSplitOrConjoin(info, vector, from, 1, 00913 relationArray, NIL(mdd_t), 00914 NIL(mdd_t), 1, depth); 00915 } 00916 } else { 00917 if (depth == turnDepth) 00918 turnFlag = 1; 00919 else 00920 turnFlag = 0; 00921 } 00922 if (turnFlag) { 00923 res = ImgPreImageByHybridWithStaticSplit(info, vector, from, relationArray, 00924 NIL(mdd_t), NIL(mdd_t)); 00925 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 00926 (float)depth) / (float)(info->nLeavesB + 1); 00927 if (depth > info->maxDepthB) 00928 info->maxDepthB = depth; 00929 info->nLeavesB++; 00930 info->foundEssentialDepth = info->option->maxEssentialDepth; 00931 return(res); 00932 } 00933 00934 if (info->option->findEssential) { 00935 if (info->option->findEssential == 1) 00936 findEssential = 1; 00937 else { 00938 if (depth >= info->lastFoundEssentialDepth) 00939 findEssential = 1; 00940 else 00941 findEssential = 0; 00942 } 00943 } else 00944 findEssential = 0; 00945 if (findEssential) { 00946 essentialCube = bdd_find_essential_cube(from); 00947 00948 if (!bdd_is_tautology(essentialCube, 1)) { 00949 info->averageFoundEssential = (info->averageFoundEssential * 00950 (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) / 00951 (float)(info->nFoundEssentials + 1); 00952 info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth * 00953 (float)info->nFoundEssentials + (float)depth) / 00954 (float)(info->nFoundEssentials + 1); 00955 if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth) 00956 info->topFoundEssentialDepth = depth; 00957 if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH) 00958 info->foundEssentials[depth]++; 00959 info->nFoundEssentials++; 00960 if (vector) { 00961 array_t *tmpVector; 00962 if (info->option->preCanonical) { 00963 tmpFrom = PreImageMakeRelationCanonical(info, vector, from, 00964 relationArray, &newVector, 00965 &newRelationArray); 00966 } else { 00967 tmpFrom = from; 00968 newVector = vector; 00969 newRelationArray = relationArray; 00970 } 00971 tmpVector = newVector; 00972 newFrom = ImgVectorMinimize(info, tmpVector, essentialCube, tmpFrom, 00973 newRelationArray, &newVector, NIL(mdd_t *), 00974 NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *)); 00975 if (tmpVector != vector) 00976 ImgVectorFree(tmpVector); 00977 if (tmpFrom != from) 00978 mdd_free(tmpFrom); 00979 } else { 00980 tmpRelationArray = ImgGetCofactoredRelationArray(relationArray, 00981 essentialCube); 00982 if (info->option->preCanonical) { 00983 newFrom = PreImageMakeRelationCanonical(info, vector, from, 00984 tmpRelationArray, &newVector, 00985 &newRelationArray); 00986 mdd_array_free(tmpRelationArray); 00987 } else { 00988 newFrom = from; 00989 newVector = vector; 00990 newRelationArray = tmpRelationArray; 00991 } 00992 } 00993 foundEssentialDepth = depth; 00994 } else { 00995 if (info->option->preCanonical) { 00996 newFrom = PreImageMakeRelationCanonical(info, vector, from, 00997 relationArray, 00998 &newVector, &newRelationArray); 00999 } else { 01000 newFrom = from; 01001 newVector = vector; 01002 newRelationArray = relationArray; 01003 } 01004 foundEssentialDepth = info->option->maxEssentialDepth; 01005 } 01006 mdd_free(essentialCube); 01007 foundEssentialDepthT = info->option->maxEssentialDepth; 01008 foundEssentialDepthE = info->option->maxEssentialDepth; 01009 } else { 01010 if (info->option->preCanonical) { 01011 newFrom = PreImageMakeRelationCanonical(info, vector, from, relationArray, 01012 &newVector, &newRelationArray); 01013 } else { 01014 newFrom = from; 01015 newVector = vector; 01016 newRelationArray = relationArray; 01017 } 01018 /* To remove compiler warnings */ 01019 foundEssentialDepth = -1; 01020 foundEssentialDepthT = -1; 01021 foundEssentialDepthE = -1; 01022 } 01023 01024 if (info->option->debug) { 01025 refResult = ImgPreImageByHybridWithStaticSplit(info, vector, from, 01026 relationArray, 01027 NIL(mdd_t), NIL(mdd_t)); 01028 res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom, 01029 newRelationArray, 01030 NIL(mdd_t), NIL(mdd_t)); 01031 tmp = refResult; 01032 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 01033 mdd_free(tmp); 01034 tmp = res; 01035 res = mdd_and(tmp, info->debugCareSet, 1, 1); 01036 mdd_free(tmp); 01037 assert(mdd_equal_mod_care_set_array(refResult, res, info->toCareSetArray)); 01038 mdd_free(refResult); 01039 mdd_free(res); 01040 } 01041 01042 if (bdd_is_tautology(newFrom, 1)) { 01043 if (newVector && newVector != vector) 01044 ImgVectorFree(newVector); 01045 if (newRelationArray != relationArray) 01046 mdd_array_free(newRelationArray); 01047 if (newFrom != from) 01048 mdd_free(newFrom); 01049 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 01050 (float)depth) / (float)(info->nLeavesB + 1); 01051 if (depth > info->maxDepthB) 01052 info->maxDepthB = depth; 01053 info->nLeavesB++; 01054 if (findEssential) 01055 info->foundEssentialDepth = foundEssentialDepth; 01056 return(mdd_one(info->manager)); 01057 } 01058 01059 if (depth == turnDepth || 01060 (info->option->splitCubeFunc && bdd_is_cube(newFrom))) { 01061 res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom, 01062 newRelationArray, 01063 NIL(mdd_t), NIL(mdd_t)); 01064 if (newVector && newVector != vector) 01065 ImgVectorFree(newVector); 01066 if (newRelationArray != relationArray) 01067 mdd_array_free(newRelationArray); 01068 if (newFrom != from) 01069 mdd_free(newFrom); 01070 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 01071 (float)depth) / (float)(info->nLeavesB + 1); 01072 if (depth > info->maxDepthB) 01073 info->maxDepthB = depth; 01074 info->nLeavesB++; 01075 if (findEssential) 01076 info->foundEssentialDepth = foundEssentialDepth; 01077 return(res); 01078 } 01079 01080 var = ImgChooseTrSplitVar(info, newVector, newRelationArray, 01081 info->option->trSplitMethod, 0); 01082 if (!var) { 01083 res = ImgPreImageByHybridWithStaticSplit(info, newVector, newFrom, 01084 newRelationArray, 01085 NIL(mdd_t), NIL(mdd_t)); 01086 if (newVector && newVector != vector) 01087 ImgVectorFree(newVector); 01088 if (newRelationArray != relationArray) 01089 mdd_array_free(newRelationArray); 01090 if (newFrom != from) 01091 mdd_free(newFrom); 01092 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 01093 (float)depth) / (float)(info->nLeavesB + 1); 01094 if (depth > info->maxDepthB) 01095 info->maxDepthB = depth; 01096 info->nLeavesB++; 01097 if (findEssential) 01098 info->foundEssentialDepth = foundEssentialDepth; 01099 return(res); 01100 } 01101 01102 varNot = mdd_not(var); 01103 01104 nRecur = 0; 01105 if (newVector) { 01106 ImgVectorConstrain(info, newVector, var, NIL(array_t), 01107 &vectorT, &cubeT, NIL(array_t *), 01108 NIL(mdd_t *), NIL(mdd_t *), TRUE); 01109 fromT = bdd_cofactor(newFrom, cubeT); 01110 mdd_free(cubeT); 01111 } else { 01112 vectorT = NIL(array_t); 01113 fromT = mdd_dup(newFrom); 01114 } 01115 relationArrayT = ImgGetCofactoredRelationArray(newRelationArray, var); 01116 if (bdd_is_tautology(fromT, 1)) { 01117 resT = mdd_one(info->manager); 01118 if (vectorT) 01119 ImgVectorFree(vectorT); 01120 } else if (bdd_is_tautology(fromT, 0)) { 01121 resT = mdd_zero(info->manager); 01122 if (vectorT) 01123 ImgVectorFree(vectorT); 01124 } else { 01125 if (info->option->debug) { 01126 saveCareSet = info->debugCareSet; 01127 info->debugCareSet = mdd_and(saveCareSet, var, 1, 1); 01128 } 01129 resT = PreImageByStaticDomainCofactoring(info, vectorT, fromT, 01130 relationArrayT, turnDepth, depth + 1); 01131 if (info->option->debug) { 01132 mdd_free(info->debugCareSet); 01133 info->debugCareSet = saveCareSet; 01134 } 01135 if (findEssential) 01136 foundEssentialDepthE = info->foundEssentialDepth; 01137 if (vectorT) 01138 ImgVectorFree(vectorT); 01139 nRecur++; 01140 } 01141 mdd_free(fromT); 01142 mdd_array_free(relationArrayT); 01143 01144 if (newVector) { 01145 ImgVectorConstrain(info, newVector, varNot, NIL(array_t), 01146 &vectorE, &cubeE, NIL(array_t *), 01147 NIL(mdd_t *), NIL(mdd_t *), TRUE); 01148 if (newVector != vector) 01149 ImgVectorFree(newVector); 01150 fromE = bdd_cofactor(newFrom, cubeE); 01151 mdd_free(cubeE); 01152 } else { 01153 vectorE = NIL(array_t); 01154 fromE = mdd_dup(newFrom); 01155 } 01156 if (newFrom != from) 01157 mdd_free(newFrom); 01158 relationArrayE = ImgGetCofactoredRelationArray(newRelationArray, varNot); 01159 if (newRelationArray != relationArray) 01160 mdd_array_free(newRelationArray); 01161 if (bdd_is_tautology(fromE, 1)) { 01162 resE = mdd_one(info->manager); 01163 if (vectorE) 01164 ImgVectorFree(vectorE); 01165 } else if (bdd_is_tautology(fromE, 0)) { 01166 resE = mdd_zero(info->manager); 01167 if (vectorE) 01168 ImgVectorFree(vectorE); 01169 } else { 01170 if (info->option->debug) { 01171 saveCareSet = info->debugCareSet; 01172 info->debugCareSet = mdd_and(saveCareSet, var, 1, 0); 01173 } 01174 resE = PreImageByStaticDomainCofactoring(info, vectorE, fromE, 01175 relationArrayE, turnDepth, depth + 1); 01176 if (info->option->debug) { 01177 mdd_free(info->debugCareSet); 01178 info->debugCareSet = saveCareSet; 01179 } 01180 if (findEssential) 01181 foundEssentialDepthE = info->foundEssentialDepth; 01182 if (vectorE) 01183 ImgVectorFree(vectorE); 01184 nRecur++; 01185 } 01186 mdd_free(fromE); 01187 mdd_array_free(relationArrayE); 01188 01189 res = bdd_ite(var, resT, resE, 1, 1, 1); 01190 if (info->option->verbosity) { 01191 size = bdd_size(res); 01192 if (size > info->maxIntermediateSize) 01193 info->maxIntermediateSize = size; 01194 if (info->option->printBddSize) { 01195 fprintf(vis_stdout, "** tfm info: bdd_ite(2,%d,%d) = %d\n", 01196 bdd_size(resT), bdd_size(resE), bdd_size(res)); 01197 } 01198 } 01199 mdd_free(resT); 01200 mdd_free(resE); 01201 mdd_free(var); 01202 mdd_free(varNot); 01203 01204 if (info->option->debug) { 01205 refResult = ImgPreImageByHybridWithStaticSplit(info, vector, from, 01206 relationArray, 01207 NIL(mdd_t), NIL(mdd_t)); 01208 tmp = refResult; 01209 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 01210 mdd_free(tmp); 01211 tmp = mdd_and(res, info->debugCareSet, 1, 1); 01212 assert(mdd_equal_mod_care_set_array(refResult, tmp, info->toCareSetArray)); 01213 mdd_free(refResult); 01214 mdd_free(tmp); 01215 } 01216 01217 if (nRecur == 0) { 01218 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 01219 (float)depth) / (float)(info->nLeavesB + 1); 01220 if (depth > info->maxDepthB) 01221 info->maxDepthB = depth; 01222 info->nLeavesB++; 01223 } 01224 01225 if (findEssential) { 01226 if (foundEssentialDepth == info->option->maxEssentialDepth) { 01227 if (foundEssentialDepthT < foundEssentialDepthE) 01228 foundEssentialDepth = foundEssentialDepthT; 01229 else 01230 foundEssentialDepth = foundEssentialDepthE; 01231 } 01232 info->foundEssentialDepth = foundEssentialDepth; 01233 } 01234 return(res); 01235 } 01236 01237 01247 static bdd_t * 01248 PreImageByConstraintCofactoring(ImgTfmInfo_t *info, array_t *delta, 01249 bdd_t *image, int splitMethod, 01250 int turnDepth, int depth) 01251 { 01252 array_t *newDelta, *tmpDelta, *vector; 01253 bdd_t *preImg, *preImgT, *preImgE, *imgT, *imgE; 01254 bdd_t *c, *newImg, *tmpImg; 01255 int split; 01256 bdd_t *var, *varNot, *refResult; 01257 ImgComponent_t *comp; 01258 int nRecur, size; 01259 mdd_t *essentialCube; 01260 int findEssential; 01261 int foundEssentialDepth; 01262 int foundEssentialDepthT, foundEssentialDepthE; 01263 mdd_t *saveCareSet = NIL(mdd_t), *tmp; 01264 01265 info->nRecursionB++; 01266 01267 if (info->nIntermediateVars) 01268 size = ImgVectorFunctionSize(delta); 01269 else 01270 size = array_n(delta); 01271 if (size == 1) { 01272 preImg = PreImageBySubstitution(info, delta, image); 01273 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 01274 (float)depth) / (float)(info->nLeavesB + 1); 01275 if (depth > info->maxDepthB) 01276 info->maxDepthB = depth; 01277 info->nLeavesB++; 01278 info->foundEssentialDepth = info->option->maxEssentialDepth; 01279 return(preImg); 01280 } 01281 01282 if (info->option->findEssential) { 01283 if (info->option->findEssential == 1) 01284 findEssential = 1; 01285 else { 01286 if (depth >= info->lastFoundEssentialDepth) 01287 findEssential = 1; 01288 else 01289 findEssential = 0; 01290 } 01291 } else 01292 findEssential = 0; 01293 if (findEssential) { 01294 essentialCube = bdd_find_essential_cube(image); 01295 01296 if (!bdd_is_tautology(essentialCube, 1)) { 01297 info->averageFoundEssential = (info->averageFoundEssential * 01298 (float)info->nFoundEssentials + (float)(bdd_size(essentialCube) - 1)) / 01299 (float)(info->nFoundEssentials + 1); 01300 info->averageFoundEssentialDepth = (info->averageFoundEssentialDepth * 01301 (float)info->nFoundEssentials + (float)depth) / 01302 (float)(info->nFoundEssentials + 1); 01303 if (info->nFoundEssentials == 0 || depth < info->topFoundEssentialDepth) 01304 info->topFoundEssentialDepth = depth; 01305 if (info->option->printEssential && depth < IMG_TF_MAX_PRINT_DEPTH) 01306 info->foundEssentials[depth]++; 01307 info->nFoundEssentials++; 01308 tmpImg = ImgVectorMinimize(info, delta, essentialCube, image, 01309 NIL(array_t), &tmpDelta, NIL(mdd_t *), 01310 NIL(array_t *), NIL(mdd_t *), NIL(mdd_t *)); 01311 foundEssentialDepth = depth; 01312 } else { 01313 tmpDelta = delta; 01314 tmpImg = image; 01315 foundEssentialDepth = info->option->maxEssentialDepth; 01316 } 01317 mdd_free(essentialCube); 01318 foundEssentialDepthT = info->option->maxEssentialDepth; 01319 foundEssentialDepthE = info->option->maxEssentialDepth; 01320 } else { 01321 tmpDelta = delta; 01322 tmpImg = image; 01323 /* To remove compiler warnings */ 01324 foundEssentialDepth = -1; 01325 foundEssentialDepthT = -1; 01326 foundEssentialDepthE = -1; 01327 } 01328 01329 if (info->option->preCanonical) { 01330 newImg = PreImageMakeVectorCanonical(info, tmpDelta, tmpImg, NIL(array_t), 01331 &newDelta, NIL(array_t *), NIL(mdd_t *), 01332 NIL(mdd_t *)); 01333 } else { 01334 newImg = tmpImg; 01335 newDelta = tmpDelta; 01336 } 01337 if (tmpDelta != delta) 01338 ImgVectorFree(tmpDelta); 01339 if (tmpImg != image) 01340 mdd_free(tmpImg); 01341 01342 if (bdd_is_tautology(newImg, 1) || bdd_is_tautology(newImg, 0)) { 01343 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 01344 (float)depth) / (float)(info->nLeavesB + 1); 01345 if (depth > info->maxDepthB) 01346 info->maxDepthB = depth; 01347 info->nLeavesB++; 01348 if (info->option->debug) { 01349 refResult = ImgPreImageByHybrid(info, newDelta, newImg); 01350 tmp = refResult; 01351 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 01352 mdd_free(tmp); 01353 tmp = mdd_and(newImg, info->debugCareSet, 1, 1); 01354 assert(mdd_equal_mod_care_set_array(refResult, tmp, 01355 info->toCareSetArray)); 01356 mdd_free(refResult); 01357 mdd_free(tmp); 01358 } 01359 ImgVectorFree(newDelta); 01360 if (findEssential) 01361 info->foundEssentialDepth = foundEssentialDepth; 01362 return(newImg); 01363 } 01364 01365 if (info->preCache) { 01366 preImg = ImgCacheLookupTable(info, info->preCache, newDelta, newImg); 01367 if (preImg) { 01368 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 01369 (float)depth) / (float)(info->nLeavesB + 1); 01370 if (depth > info->maxDepthB) 01371 info->maxDepthB = depth; 01372 info->nLeavesB++; 01373 if (info->option->debug) { 01374 refResult = ImgPreImageByHybrid(info, newDelta, newImg); 01375 tmp = refResult; 01376 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 01377 mdd_free(tmp); 01378 tmp = mdd_and(preImg, info->debugCareSet, 1, 1); 01379 assert(mdd_equal_mod_care_set_array(refResult, tmp, 01380 info->toCareSetArray)); 01381 mdd_free(refResult); 01382 mdd_free(tmp); 01383 } 01384 ImgVectorFree(newDelta); 01385 mdd_free(newImg); 01386 if (findEssential) 01387 info->foundEssentialDepth = foundEssentialDepth; 01388 return(preImg); 01389 } 01390 } 01391 01392 if (depth == turnDepth) { 01393 preImg = ImgPreImageByHybrid(info, newDelta, newImg); 01394 if (info->option->debug) { 01395 refResult = ImgPreImageByHybrid(info, newDelta, newImg); 01396 tmp = refResult; 01397 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 01398 mdd_free(tmp); 01399 tmp = mdd_and(preImg, info->debugCareSet, 1, 1); 01400 assert(mdd_equal_mod_care_set_array(refResult, tmp, 01401 info->toCareSetArray)); 01402 mdd_free(refResult); 01403 mdd_free(tmp); 01404 } 01405 if (info->preCache) 01406 ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg)); 01407 else { 01408 ImgVectorFree(newDelta); 01409 mdd_free(newImg); 01410 } 01411 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 01412 (float)depth) / (float)(info->nLeavesB + 1); 01413 if (depth > info->maxDepthB) 01414 info->maxDepthB = depth; 01415 info->nLeavesB++; 01416 info->nTurnsB++; 01417 if (findEssential) 01418 info->foundEssentialDepth = foundEssentialDepth; 01419 return(preImg); 01420 } 01421 01422 split = PreImageChooseSplitVar(info, newDelta, newImg, 01423 1, info->option->preOutputSplit); 01424 comp = array_fetch(ImgComponent_t *, newDelta, split); 01425 var = mdd_dup(comp->var); 01426 varNot = mdd_not(var); 01427 imgE = bdd_cofactor(newImg, varNot); 01428 mdd_free(varNot); 01429 imgT = bdd_cofactor(newImg, var); 01430 mdd_free(var); 01431 if (!info->preCache && !info->option->debug) 01432 mdd_free(newImg); 01433 c = PreImageDeleteOneComponent(info, newDelta, split, &vector); 01434 if (!info->preCache && !info->option->debug) 01435 ImgVectorFree(newDelta); 01436 01437 nRecur = 0; 01438 if (bdd_is_tautology(imgT, 1)) 01439 preImgT = mdd_one(info->manager); 01440 else if (bdd_is_tautology(imgT, 0)) 01441 preImgT = mdd_zero(info->manager); 01442 else { 01443 if (info->option->debug) { 01444 saveCareSet = info->debugCareSet; 01445 info->debugCareSet = mdd_and(saveCareSet, c, 1, 1); 01446 } 01447 preImgT = PreImageByConstraintCofactoring(info, vector, imgT, splitMethod, 01448 turnDepth, depth + 1); 01449 if (info->option->debug) { 01450 mdd_free(info->debugCareSet); 01451 info->debugCareSet = saveCareSet; 01452 } 01453 if (findEssential) 01454 foundEssentialDepthT = info->foundEssentialDepth; 01455 nRecur++; 01456 } 01457 mdd_free(imgT); 01458 if (bdd_is_tautology(imgE, 1)) 01459 preImgE = mdd_one(info->manager); 01460 else if (bdd_is_tautology(imgE, 0)) 01461 preImgE = mdd_zero(info->manager); 01462 else { 01463 if (info->option->debug) { 01464 saveCareSet = info->debugCareSet; 01465 info->debugCareSet = mdd_and(saveCareSet, c, 1, 0); 01466 } 01467 preImgE = PreImageByConstraintCofactoring(info, vector, imgE, splitMethod, 01468 turnDepth, depth + 1); 01469 if (info->option->debug) { 01470 mdd_free(info->debugCareSet); 01471 info->debugCareSet = saveCareSet; 01472 } 01473 if (findEssential) 01474 foundEssentialDepthE = info->foundEssentialDepth; 01475 nRecur++; 01476 } 01477 mdd_free(imgE); 01478 ImgVectorFree(vector); 01479 preImg = bdd_ite(c, preImgT, preImgE, 1, 1, 1); 01480 if (info->option->verbosity) { 01481 size = bdd_size(preImg); 01482 if (size > info->maxIntermediateSize) 01483 info->maxIntermediateSize = size; 01484 if (info->option->printBddSize) { 01485 fprintf(vis_stdout, "** tfm info: bdd_ite(%d,%d,%d) = %d\n", 01486 bdd_size(c), bdd_size(preImgT), bdd_size(preImgE), 01487 bdd_size(preImg)); 01488 } 01489 } 01490 mdd_free(c); 01491 mdd_free(preImgT); 01492 mdd_free(preImgE); 01493 01494 if (info->preCache) 01495 ImgCacheInsertTable(info->preCache, newDelta, newImg, mdd_dup(preImg)); 01496 01497 if (info->option->debug) { 01498 refResult = ImgPreImageByHybrid(info, newDelta, newImg); 01499 tmp = refResult; 01500 refResult = mdd_and(tmp, info->debugCareSet, 1, 1); 01501 mdd_free(tmp); 01502 tmp = mdd_and(preImg, info->debugCareSet, 1, 1); 01503 assert(mdd_equal_mod_care_set_array(refResult, tmp, 01504 info->toCareSetArray)); 01505 mdd_free(refResult); 01506 mdd_free(tmp); 01507 if (!info->preCache) { 01508 ImgVectorFree(newDelta); 01509 mdd_free(newImg); 01510 } 01511 } 01512 01513 if (nRecur == 0) { 01514 info->averageDepthB = (info->averageDepthB * (float)info->nLeavesB + 01515 (float)depth) / (float)(info->nLeavesB + 1); 01516 if (depth > info->maxDepthB) 01517 info->maxDepthB = depth; 01518 info->nLeavesB++; 01519 } 01520 01521 if (findEssential) { 01522 if (foundEssentialDepth == info->option->maxEssentialDepth) { 01523 if (foundEssentialDepthT < foundEssentialDepthE) 01524 foundEssentialDepth = foundEssentialDepthT; 01525 else 01526 foundEssentialDepth = foundEssentialDepthE; 01527 } 01528 info->foundEssentialDepth = foundEssentialDepth; 01529 } 01530 return(preImg); 01531 } 01532 01533 01543 static mdd_t * 01544 PreImageBySubstitution(ImgTfmInfo_t *info, array_t *vector, mdd_t *from) 01545 { 01546 int i, index; 01547 ImgComponent_t *comp, *fromComp; 01548 array_t *varArray, *funcArray; 01549 mdd_t *result; 01550 01551 if (bdd_is_tautology(from, 1)) 01552 return(mdd_one(info->manager)); 01553 else if (bdd_is_tautology(from, 0)) 01554 return(mdd_zero(info->manager)); 01555 01556 fromComp = ImgComponentAlloc(info); 01557 fromComp->func = from; 01558 ImgComponentGetSupport(fromComp); 01559 01560 varArray = array_alloc(mdd_t *, 0); 01561 funcArray = array_alloc(mdd_t *, 0); 01562 01563 for (i = 0; i < array_n(vector); i++) { 01564 comp = array_fetch(ImgComponent_t *, vector, i); 01565 index = bdd_top_var_id(comp->var); 01566 if (fromComp->support[index] || comp->intermediate) { 01567 array_insert_last(mdd_t *, varArray, comp->var); 01568 array_insert_last(mdd_t *, funcArray, comp->func); 01569 } 01570 } 01571 01572 fromComp->func = NIL(mdd_t); 01573 ImgComponentFree(fromComp); 01574 01575 result = bdd_vector_compose(from, varArray, funcArray); 01576 array_free(varArray); 01577 array_free(funcArray); 01578 01579 /* quantify all primary inputs */ 01580 if (info->preKeepPiInTr == FALSE) { 01581 array_t *quantifyVarBddArray; 01582 mdd_t *tmp; 01583 01584 if (info->newQuantifyBddVars) 01585 quantifyVarBddArray = info->newQuantifyBddVars; 01586 else 01587 quantifyVarBddArray = info->quantifyVarBddArray; 01588 01589 tmp = result; 01590 result = bdd_smooth(tmp, quantifyVarBddArray); 01591 mdd_free(tmp); 01592 } 01593 01594 return(result); 01595 } 01596 01597 01611 static bdd_t * 01612 PreImageMakeVectorCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image, 01613 array_t *relationArray, array_t **newVector, 01614 array_t **newRelationArray, 01615 mdd_t **cofactorCube, mdd_t **abstractCube) 01616 { 01617 array_t *tmpVector, *cofactoredVector; 01618 bdd_t *simple, *tmp, *newImage; 01619 ImgComponent_t *comp, *comp1, *imgComp; 01620 int i, id, n, pos; 01621 st_table *equivTable; 01622 int *ptr, *regularPtr; 01623 mdd_t *var, *cofactor, *abstract, *nsVar; 01624 array_t *tmpRelationArray; 01625 int changed = 0; 01626 01627 newImage = mdd_dup(image); 01628 01629 imgComp = ImgComponentAlloc(info); 01630 imgComp->func = image; 01631 ImgComponentGetSupport(imgComp); 01632 01633 if (relationArray) { 01634 cofactor = mdd_one(info->manager); 01635 abstract = mdd_one(info->manager); 01636 } else { 01637 cofactor = NIL(mdd_t); 01638 abstract = NIL(mdd_t); 01639 } 01640 01641 if (info->nIntermediateVars) { 01642 mdd_t *tmpCofactor, *tmpAbstract; 01643 mdd_t *constIntermediate; 01644 01645 if (ImgExistConstIntermediateVar(vector)) { 01646 constIntermediate = mdd_one(info->manager); 01647 for (i = 0; i < array_n(vector); i++) { 01648 comp = array_fetch(ImgComponent_t *, vector, i); 01649 if (comp->intermediate) { 01650 if (mdd_is_tautology(comp->func, 1)) { 01651 tmp = constIntermediate; 01652 constIntermediate = mdd_and(tmp, comp->var, 1, 1); 01653 mdd_free(tmp); 01654 } else if (mdd_is_tautology(comp->func, 0)) { 01655 tmp = constIntermediate; 01656 constIntermediate = mdd_and(tmp, comp->var, 1, 0); 01657 mdd_free(tmp); 01658 } 01659 } 01660 } 01661 if (relationArray) { 01662 cofactoredVector = ImgComposeConstIntermediateVars(info, vector, 01663 constIntermediate, 01664 &tmpCofactor, &tmpAbstract, 01665 NIL(mdd_t *), &newImage); 01666 01667 if (!bdd_is_tautology(tmpCofactor, 1)) { 01668 tmp = cofactor; 01669 cofactor = mdd_and(tmp, tmpCofactor, 1, 1); 01670 mdd_free(tmp); 01671 } 01672 mdd_free(tmpCofactor); 01673 if (!bdd_is_tautology(tmpAbstract, 1)) { 01674 tmp = abstract; 01675 abstract = mdd_and(tmp, tmpAbstract, 1, 1); 01676 mdd_free(tmp); 01677 } 01678 mdd_free(tmpAbstract); 01679 } else { 01680 cofactoredVector = ImgComposeConstIntermediateVars(info, vector, 01681 constIntermediate, 01682 NIL(mdd_t *), NIL(mdd_t *), 01683 NIL(mdd_t *), &newImage); 01684 } 01685 mdd_free(constIntermediate); 01686 } else 01687 cofactoredVector = vector; 01688 } else 01689 cofactoredVector = vector; 01690 01691 /* Simplify image -- canonicalize the image first */ 01692 n = 0; 01693 equivTable = st_init_table(st_ptrcmp, st_ptrhash); 01694 tmpVector = array_alloc(ImgComponent_t *, 0); 01695 for (i = 0; i < array_n(cofactoredVector); i++) { 01696 comp = array_fetch(ImgComponent_t *, cofactoredVector, i); 01697 if (comp->intermediate) { 01698 comp1 = ImgComponentCopy(info, comp); 01699 array_insert_last(ImgComponent_t *, tmpVector, comp1); 01700 n++; 01701 continue; 01702 } 01703 id = (int)bdd_top_var_id(comp->var); 01704 if (!imgComp->support[id]) { 01705 if (abstract) { 01706 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 01707 tmp = abstract; 01708 abstract = mdd_and(tmp, nsVar, 1, 1); 01709 mdd_free(tmp); 01710 mdd_free(nsVar); 01711 } 01712 continue; 01713 } 01714 if (mdd_is_tautology(comp->func, 1)) { 01715 changed = 1; 01716 simple = bdd_cofactor(newImage, comp->var); 01717 mdd_free(newImage); 01718 newImage = simple; 01719 if (abstract) { 01720 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 01721 tmp = abstract; 01722 abstract = mdd_and(tmp, nsVar, 1, 1); 01723 mdd_free(tmp); 01724 mdd_free(nsVar); 01725 } 01726 } else if (mdd_is_tautology(comp->func, 0)) { 01727 changed = 1; 01728 tmp = mdd_not(comp->var); 01729 simple = bdd_cofactor(newImage, tmp); 01730 mdd_free(tmp); 01731 mdd_free(newImage); 01732 newImage = simple; 01733 if (abstract) { 01734 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 01735 tmp = abstract; 01736 abstract = mdd_and(tmp, nsVar, 1, 1); 01737 mdd_free(tmp); 01738 mdd_free(nsVar); 01739 } 01740 } else { 01741 ptr = (int *)bdd_pointer(comp->func); 01742 regularPtr = (int *)((unsigned long)ptr & ~01); 01743 if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) { 01744 changed = 1; 01745 comp1 = array_fetch(ImgComponent_t *, tmpVector, pos); 01746 if (mdd_equal(comp->func, comp1->func)) { 01747 tmp = newImage; 01748 newImage = bdd_compose(tmp, comp->var, comp1->var); 01749 mdd_free(tmp); 01750 } else { 01751 tmp = newImage; 01752 var = mdd_not(comp1->var); 01753 newImage = bdd_compose(tmp, comp->var, var); 01754 mdd_free(tmp); 01755 mdd_free(var); 01756 } 01757 if (abstract) { 01758 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 01759 tmp = abstract; 01760 abstract = mdd_and(tmp, nsVar, 1, 1); 01761 mdd_free(tmp); 01762 mdd_free(nsVar); 01763 } 01764 } else { 01765 comp1 = ImgComponentCopy(info, comp); 01766 array_insert_last(ImgComponent_t *, tmpVector, comp1); 01767 st_insert(equivTable, (char *)regularPtr, (char *)(long)n); 01768 n++; 01769 } 01770 } 01771 } 01772 st_free_table(equivTable); 01773 if (cofactoredVector && cofactoredVector != vector) 01774 ImgVectorFree(cofactoredVector); 01775 01776 if (changed) { 01777 /* Now Simplify delta by deleting the non-affecting components */ 01778 *newVector = array_alloc(ImgComponent_t *, 0); 01779 01780 imgComp->func = NIL(mdd_t); 01781 ImgComponentFree(imgComp); 01782 01783 imgComp = ImgComponentAlloc(info); 01784 imgComp->func = newImage; 01785 ImgSupportClear(info, imgComp->support); 01786 ImgComponentGetSupport(imgComp); 01787 for (i = 0; i < array_n(tmpVector); i++) { 01788 comp = array_fetch(ImgComponent_t *, tmpVector, i); 01789 id = (int)bdd_top_var_id(comp->var); 01790 if (imgComp->support[id] || comp->intermediate) 01791 array_insert_last(ImgComponent_t *, *newVector, comp); 01792 else { 01793 if (abstract) { 01794 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 01795 tmp = abstract; 01796 abstract = mdd_and(tmp, nsVar, 1, 1); 01797 mdd_free(tmp); 01798 mdd_free(nsVar); 01799 } 01800 ImgComponentFree(comp); 01801 } 01802 } 01803 array_free(tmpVector); 01804 } else 01805 *newVector = tmpVector; 01806 01807 imgComp->func = NIL(mdd_t); 01808 ImgComponentFree(imgComp); 01809 01810 if (newRelationArray) 01811 *newRelationArray = relationArray; 01812 if (cofactor) { 01813 if (cofactorCube) 01814 *cofactorCube = cofactor; 01815 else { 01816 if (!bdd_is_tautology(cofactor, 1)) { 01817 tmpRelationArray = *newRelationArray; 01818 *newRelationArray = ImgGetCofactoredRelationArray(tmpRelationArray, 01819 cofactor); 01820 if (tmpRelationArray != relationArray) 01821 mdd_array_free(tmpRelationArray); 01822 } 01823 mdd_free(cofactor); 01824 } 01825 } 01826 if (abstract) { 01827 if (abstractCube) 01828 *abstractCube = abstract; 01829 else { 01830 if (bdd_is_tautology(abstract, 1)) 01831 mdd_free(abstract); 01832 else { 01833 tmpRelationArray = *newRelationArray; 01834 *newRelationArray = ImgGetAbstractedRelationArray(info->manager, 01835 tmpRelationArray, 01836 abstract); 01837 mdd_free(abstract); 01838 if (tmpRelationArray != relationArray) 01839 mdd_array_free(tmpRelationArray); 01840 } 01841 } 01842 } 01843 assert(CheckPreImageVector(info, *newVector, newImage)); 01844 return(newImage); 01845 } 01846 01847 01862 static bdd_t * 01863 PreImageMakeRelationCanonical(ImgTfmInfo_t *info, array_t *vector, bdd_t *image, 01864 array_t *relationArray, array_t **newVector, 01865 array_t **newRelationArray) 01866 { 01867 array_t *tmpVector, *cofactoredVector; 01868 bdd_t *simple, *tmp, *newImage; 01869 ImgComponent_t *comp, *comp1, *imgComp; 01870 int i, j, id; 01871 mdd_t *cofactor, *abstract, *var, *nsVar; 01872 array_t *tmpRelationArray; 01873 int changed = 0; 01874 mdd_t *yVarsCube, *rangeCube, *relation, *tmp2; 01875 array_t *supportIds; 01876 01877 imgComp = ImgComponentAlloc(info); 01878 imgComp->func = image; 01879 ImgComponentGetSupport(imgComp); 01880 01881 if (vector) { 01882 newImage = mdd_dup(image); 01883 cofactor = mdd_one(info->manager); 01884 abstract = mdd_one(info->manager); 01885 01886 if (info->nIntermediateVars) { 01887 mdd_t *tmpCofactor, *tmpAbstract; 01888 mdd_t *constIntermediate; 01889 01890 if (ImgExistConstIntermediateVar(vector)) { 01891 constIntermediate = mdd_one(info->manager); 01892 01893 for (i = 0; i < array_n(vector); i++) { 01894 comp = array_fetch(ImgComponent_t *, vector, i); 01895 if (comp->intermediate) { 01896 if (mdd_is_tautology(comp->func, 1)) { 01897 tmp = constIntermediate; 01898 constIntermediate = mdd_and(tmp, comp->var, 1, 1); 01899 mdd_free(tmp); 01900 } else if (mdd_is_tautology(comp->func, 0)) { 01901 tmp = constIntermediate; 01902 constIntermediate = mdd_and(tmp, comp->var, 1, 0); 01903 mdd_free(tmp); 01904 } 01905 } 01906 } 01907 01908 cofactoredVector = ImgComposeConstIntermediateVars(info, vector, 01909 constIntermediate, 01910 &tmpCofactor, 01911 &tmpAbstract, 01912 NIL(mdd_t *), 01913 &newImage); 01914 01915 if (!bdd_is_tautology(tmpCofactor, 1)) { 01916 tmp = cofactor; 01917 cofactor = mdd_and(tmp, tmpCofactor, 1, 1); 01918 mdd_free(tmp); 01919 } 01920 mdd_free(tmpCofactor); 01921 if (!bdd_is_tautology(tmpAbstract, 1)) { 01922 tmp = abstract; 01923 abstract = mdd_and(tmp, tmpAbstract, 1, 1); 01924 mdd_free(tmp); 01925 } 01926 mdd_free(tmpAbstract); 01927 mdd_free(constIntermediate); 01928 } else 01929 cofactoredVector = vector; 01930 } else 01931 cofactoredVector = vector; 01932 01933 /* Simplify image -- canonicalize vector */ 01934 tmpVector = array_alloc(ImgComponent_t *, 0); 01935 for (i = 0; i < array_n(cofactoredVector); i++) { 01936 comp = array_fetch(ImgComponent_t *, cofactoredVector, i); 01937 if (comp->intermediate) { 01938 comp1 = ImgComponentCopy(info, comp); 01939 array_insert_last(ImgComponent_t *, tmpVector, comp1); 01940 continue; 01941 } 01942 id = (int)bdd_top_var_id(comp->var); 01943 if (!imgComp->support[id]) { 01944 if (abstract) { 01945 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 01946 tmp = abstract; 01947 abstract = mdd_and(tmp, nsVar, 1, 1); 01948 mdd_free(tmp); 01949 mdd_free(nsVar); 01950 } 01951 continue; 01952 } 01953 if (mdd_is_tautology(comp->func, 1)) { 01954 changed = 1; 01955 simple = bdd_cofactor(newImage, comp->var); 01956 mdd_free(newImage); 01957 newImage = simple; 01958 if (abstract) { 01959 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 01960 tmp = abstract; 01961 abstract = mdd_and(tmp, nsVar, 1, 1); 01962 mdd_free(tmp); 01963 mdd_free(nsVar); 01964 } 01965 } else if (mdd_is_tautology(comp->func, 0)) { 01966 changed = 1; 01967 tmp = mdd_not(comp->var); 01968 simple = bdd_cofactor(newImage, tmp); 01969 mdd_free(tmp); 01970 mdd_free(newImage); 01971 newImage = simple; 01972 if (abstract) { 01973 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 01974 tmp = abstract; 01975 abstract = mdd_and(tmp, nsVar, 1, 1); 01976 mdd_free(tmp); 01977 mdd_free(nsVar); 01978 } 01979 } else { 01980 comp1 = ImgComponentCopy(info, comp); 01981 array_insert_last(ImgComponent_t *, tmpVector, comp1); 01982 } 01983 } 01984 if (cofactoredVector && cofactoredVector != vector) 01985 ImgVectorFree(cofactoredVector); 01986 01987 if (changed) { 01988 /* Now Simplify delta by deleting the non-affecting components */ 01989 *newVector = array_alloc(ImgComponent_t *, 0); 01990 01991 imgComp->func = NIL(mdd_t); 01992 ImgComponentFree(imgComp); 01993 01994 imgComp = ImgComponentAlloc(info); 01995 imgComp->func = newImage; 01996 ImgSupportClear(info, imgComp->support); 01997 ImgComponentGetSupport(imgComp); 01998 for (i = 0; i < array_n(tmpVector); i++) { 01999 comp = array_fetch(ImgComponent_t *, tmpVector, i); 02000 id = (int)bdd_top_var_id(comp->var); 02001 if (imgComp->support[id] || comp->intermediate) 02002 array_insert_last(ImgComponent_t *, *newVector, comp); 02003 else { 02004 if (abstract) { 02005 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 02006 tmp = abstract; 02007 abstract = mdd_and(tmp, nsVar, 1, 1); 02008 mdd_free(tmp); 02009 mdd_free(nsVar); 02010 } 02011 ImgComponentFree(comp); 02012 } 02013 } 02014 array_free(tmpVector); 02015 } else 02016 *newVector = tmpVector; 02017 } else { 02018 newImage = image; 02019 *newVector = vector; 02020 cofactor = NIL(mdd_t); 02021 abstract = NIL(mdd_t); 02022 } 02023 02024 yVarsCube = mdd_one(info->manager); 02025 for (i = 0; i < info->nVars; i++) { 02026 if (imgComp->support[i]) { 02027 imgComp->support[i] = 0; 02028 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) 02029 continue; 02030 if (info->intermediateVarsTable && 02031 st_lookup(info->intermediateVarsTable, (char *)(long)i, 02032 NIL(char *))) { 02033 continue; 02034 } 02035 var = bdd_var_with_index(info->manager, i); 02036 nsVar = ImgSubstitute(var, info->functionData, Img_D2R_c); 02037 mdd_free(var); 02038 id = (int)bdd_top_var_id(nsVar); 02039 imgComp->support[id] = 1; 02040 tmp = yVarsCube; 02041 yVarsCube = mdd_and(tmp, nsVar, 1, 1); 02042 mdd_free(tmp); 02043 mdd_free(nsVar); 02044 } 02045 } 02046 02047 if (vector) { 02048 for (i = 0; i < array_n(*newVector); i++) { 02049 comp = array_fetch(ImgComponent_t *, *newVector, i); 02050 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 02051 id = (int)bdd_top_var_id(nsVar); 02052 imgComp->support[id] = 2; 02053 mdd_free(nsVar); 02054 } 02055 } 02056 02057 for (i = 0; i < array_n(relationArray); i++) { 02058 relation = array_fetch(mdd_t *, relationArray, i); 02059 supportIds = mdd_get_bdd_support_ids(info->manager, relation); 02060 for (j = 0; j < array_n(supportIds); j++) { 02061 id = array_fetch(int, supportIds, j); 02062 imgComp->support[id] = 2; 02063 } 02064 array_free(supportIds); 02065 } 02066 02067 for (i = 0; i < info->nVars; i++) { 02068 if (imgComp->support[i] == 1) { 02069 nsVar = bdd_var_with_index(info->manager, i); 02070 var = ImgSubstitute(nsVar, info->functionData, Img_R2D_c); 02071 mdd_free(nsVar); 02072 tmp = newImage; 02073 newImage = bdd_smooth_with_cube(tmp, var); 02074 if (tmp != image) 02075 mdd_free(tmp); 02076 mdd_free(var); 02077 } 02078 } 02079 02080 imgComp->func = NIL(mdd_t); 02081 ImgComponentFree(imgComp); 02082 02083 if (bdd_get_package_name() == CUDD) 02084 rangeCube = info->functionData->rangeCube; 02085 else { 02086 rangeCube = mdd_one(info->manager); 02087 for (i = 0; i < array_n(info->functionData->rangeBddVars); i++) { 02088 var = array_fetch(mdd_t *, info->functionData->rangeBddVars, i); 02089 tmp = rangeCube; 02090 rangeCube = mdd_and(tmp, var, 1, 1); 02091 mdd_free(tmp); 02092 } 02093 } 02094 02095 cofactor = NIL(mdd_t); 02096 if (abstract) { 02097 tmp2 = bdd_smooth_with_cube(rangeCube, yVarsCube); 02098 tmp = abstract; 02099 abstract = mdd_and(tmp, tmp2, 1, 1); 02100 mdd_free(tmp); 02101 mdd_free(tmp2); 02102 } else 02103 abstract = bdd_smooth_with_cube(rangeCube, yVarsCube); 02104 mdd_free(yVarsCube); 02105 if (rangeCube != info->functionData->rangeCube) 02106 mdd_free(rangeCube); 02107 02108 *newRelationArray = relationArray; 02109 if (cofactor) { 02110 if (!bdd_is_tautology(cofactor, 1)) { 02111 tmpRelationArray = *newRelationArray; 02112 *newRelationArray = ImgGetCofactoredRelationArray(tmpRelationArray, 02113 cofactor); 02114 if (tmpRelationArray != relationArray) 02115 mdd_array_free(tmpRelationArray); 02116 } 02117 mdd_free(cofactor); 02118 } 02119 if (bdd_is_tautology(abstract, 1)) 02120 mdd_free(abstract); 02121 else { 02122 tmpRelationArray = *newRelationArray; 02123 *newRelationArray = ImgGetAbstractedRelationArray(info->manager, 02124 tmpRelationArray, 02125 abstract); 02126 mdd_free(abstract); 02127 if (tmpRelationArray != relationArray) 02128 mdd_array_free(tmpRelationArray); 02129 } 02130 return(newImage); 02131 } 02132 02133 02144 static bdd_t * 02145 PreImageDeleteOneComponent(ImgTfmInfo_t *info, array_t *delta, int index, 02146 array_t **newDelta) 02147 { 02148 int i; 02149 ImgComponent_t *comp, *tmpComp; 02150 bdd_t *func, *newFunc; 02151 int preMinimize = info->option->preMinimize; 02152 02153 assert(array_n(delta) > 0); 02154 02155 comp = array_fetch(ImgComponent_t *, delta, index); 02156 func = mdd_dup(comp->func); 02157 02158 *newDelta = array_alloc(ImgComponent_t *, 0); 02159 for (i = 0; i < array_n(delta); i++) { 02160 if (i != index) { 02161 comp = array_fetch(ImgComponent_t *, delta, i); 02162 tmpComp = ImgComponentCopy(info, comp); 02163 if (preMinimize) { 02164 newFunc = bdd_minimize(tmpComp->func, func); 02165 if (mdd_equal(newFunc, tmpComp->func)) 02166 mdd_free(newFunc); 02167 else { 02168 mdd_free(tmpComp->func); 02169 tmpComp->func = newFunc; 02170 ImgSupportClear(info, tmpComp->support); 02171 ImgComponentGetSupport(tmpComp); 02172 } 02173 } 02174 array_insert_last(ImgComponent_t *, (*newDelta), tmpComp); 02175 } 02176 } 02177 02178 return(func); 02179 } 02180 02181 02191 static int 02192 PreImageChooseSplitVar(ImgTfmInfo_t *info, array_t *delta, bdd_t *img, 02193 int splitMethod, int split) 02194 { 02195 ImgComponent_t *comp, *imgComp; 02196 int i, j, bestCost, newCost; 02197 int index, bestVar, bestComp; 02198 int nFuncs, nVars, bestOccur = 0; 02199 int *varOccur, *varCost; 02200 mdd_t *var, *varNot, *pcFunc, *ncFunc; 02201 int tieCount = 0; 02202 02203 assert(array_n(delta) > 0); 02204 02205 if (splitMethod == 0) { 02206 bestVar = -1; 02207 bestComp = -1; 02208 nFuncs = array_n(delta); 02209 nVars = info->nVars; 02210 varOccur = ALLOC(int, nVars); 02211 memset(varOccur, 0, sizeof(int) * nVars); 02212 varCost = NIL(int); 02213 for (i = 0; i < nFuncs; i++) { 02214 comp = array_fetch(ImgComponent_t *, delta, i); 02215 for (j = 0; j < nVars; j++) { 02216 if (comp->support[j]) 02217 varOccur[j]++; 02218 } 02219 } 02220 switch (split) { 02221 case 0: /* largest support */ 02222 for (i = 0; i < nVars; i++) { 02223 if (varOccur[i] == 0) 02224 continue; 02225 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) 02226 continue; 02227 if (info->intermediateVarsTable && 02228 st_lookup(info->intermediateVarsTable, (char *)(long)i, 02229 NIL(char *))) { 02230 continue; 02231 } 02232 if (bestVar == -1 || varOccur[i] > bestOccur) { 02233 bestVar = i; 02234 bestOccur = varOccur[i]; 02235 tieCount = 1; 02236 } else if (varOccur[i] == bestOccur) { 02237 tieCount++; 02238 if (info->option->tieBreakMode == 0 && 02239 bdd_get_level_from_id(info->manager, i) < 02240 bdd_get_level_from_id(info->manager, bestVar)) { 02241 bestVar = i; 02242 } 02243 } 02244 } 02245 02246 if (info->option->tieBreakMode == 1 && tieCount > 1) { 02247 bestCost = IMG_TF_MAX_INT; 02248 for (i = bestVar; i < nVars; i++) { 02249 if (varOccur[i] != bestOccur) 02250 continue; 02251 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) 02252 continue; 02253 if (info->intermediateVarsTable && 02254 st_lookup(info->intermediateVarsTable, (char *)(long)i, 02255 NIL(char *))) { 02256 continue; 02257 } 02258 var = bdd_var_with_index(info->manager, i); 02259 newCost = 0; 02260 for (j = 0; j < array_n(delta); j++) { 02261 comp = array_fetch(ImgComponent_t *, delta, j); 02262 newCost += bdd_estimate_cofactor(comp->func, var, 1); 02263 newCost += bdd_estimate_cofactor(comp->func, var, 0); 02264 } 02265 mdd_free(var); 02266 02267 if (newCost < bestCost) { 02268 bestVar = i; 02269 bestCost = newCost; 02270 } else if (newCost == bestCost) { 02271 if (bdd_get_level_from_id(info->manager, i) < 02272 bdd_get_level_from_id(info->manager, bestVar)) { 02273 bestVar = i; 02274 } 02275 } 02276 } 02277 } 02278 break; 02279 case 1: /* smallest support after splitting */ 02280 /* Find the variable which makes the smallest support after splitting */ 02281 bestCost = IMG_TF_MAX_INT; 02282 varCost = ALLOC(int, nVars); 02283 memset(varCost, 0, sizeof(int) * nVars); 02284 for (i = 0; i < nVars; i++) { 02285 if (varOccur[i] == 0) 02286 continue; 02287 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) 02288 continue; 02289 if (info->intermediateVarsTable && 02290 st_lookup(info->intermediateVarsTable, (char *)(long)i, 02291 NIL(char *))) { 02292 continue; 02293 } 02294 var = bdd_var_with_index(info->manager, i); 02295 varNot = mdd_not(var); 02296 for (j = 0; j < array_n(delta); j++) { 02297 comp = array_fetch(ImgComponent_t *, delta, j); 02298 pcFunc = bdd_cofactor(comp->func, var); 02299 varCost[i] += ImgCountBddSupports(pcFunc); 02300 mdd_free(pcFunc); 02301 ncFunc = bdd_cofactor(comp->func, varNot); 02302 varCost[i] += ImgCountBddSupports(ncFunc); 02303 mdd_free(ncFunc); 02304 } 02305 mdd_free(var); 02306 mdd_free(varNot); 02307 02308 if (varCost[i] < bestCost) { 02309 bestCost = varCost[i]; 02310 bestVar = i; 02311 } else if (varCost[i] == bestCost) { 02312 if (varOccur[i] < varOccur[bestVar]) { 02313 bestVar = i; 02314 } else if (varOccur[i] == varOccur[bestVar]) { 02315 if (bdd_get_level_from_id(info->manager, i) < 02316 bdd_get_level_from_id(info->manager, bestVar)) { 02317 bestVar = i; 02318 } 02319 } 02320 } 02321 } 02322 break; 02323 case 2: /* smallest BDD size after splitting */ 02324 /* Find the variable which makes the smallest BDDs of all functions 02325 after splitting */ 02326 bestCost = IMG_TF_MAX_INT; 02327 varCost = ALLOC(int, nVars); 02328 memset(varCost, 0, sizeof(int) * nVars); 02329 for (i = 0; i < nVars; i++) { 02330 if (varOccur[i] == 0) 02331 continue; 02332 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) 02333 continue; 02334 if (info->intermediateVarsTable && 02335 st_lookup(info->intermediateVarsTable, (char *)(long)i, 02336 NIL(char *))) { 02337 continue; 02338 } 02339 var = bdd_var_with_index(info->manager, i); 02340 for (j = 0; j < array_n(delta); j++) { 02341 comp = array_fetch(ImgComponent_t *, delta, j); 02342 varCost[i] += bdd_estimate_cofactor(comp->func, var, 1); 02343 varCost[i] += bdd_estimate_cofactor(comp->func, var, 0); 02344 } 02345 mdd_free(var); 02346 02347 if (varCost[i] < bestCost) { 02348 bestCost = varCost[i]; 02349 bestVar = i; 02350 } else if (varCost[i] == bestCost) { 02351 if (varOccur[i] < varOccur[bestVar]) { 02352 bestVar = i; 02353 } else if (varOccur[i] == varOccur[bestVar]) { 02354 if (bdd_get_level_from_id(info->manager, i) < 02355 bdd_get_level_from_id(info->manager, bestVar)) { 02356 bestVar = i; 02357 } 02358 } 02359 } 02360 } 02361 break; 02362 case 3: /* top variable */ 02363 default: 02364 for (i = 0; i < nVars; i++) { 02365 if (varOccur[i] == 0) 02366 continue; 02367 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) 02368 continue; 02369 if (info->intermediateVarsTable && 02370 st_lookup(info->intermediateVarsTable, (char *)(long)i, 02371 NIL(char *))) { 02372 continue; 02373 } 02374 if (bestVar == -1) 02375 bestVar = i; 02376 else if (bdd_get_level_from_id(info->manager, i) < 02377 bdd_get_level_from_id(info->manager, bestVar)) { 02378 bestVar = i; 02379 } 02380 } 02381 } 02382 FREE(varOccur); 02383 if (varCost) 02384 FREE(varCost); 02385 } else { 02386 bestComp = -1; 02387 bestVar = -1; 02388 switch (split) { 02389 case 0: /* smallest BDD size */ 02390 bestCost = IMG_TF_MAX_INT; 02391 imgComp = ImgComponentAlloc(info); 02392 imgComp->func = img; 02393 ImgComponentGetSupport(imgComp); 02394 for (i = 0; i < array_n(delta); i++) { 02395 comp = array_fetch(ImgComponent_t *, delta, i); 02396 if (comp->intermediate) 02397 continue; 02398 index = (int)bdd_top_var_id(comp->var); 02399 if (imgComp->support[index]) { 02400 newCost = bdd_size(comp->func); 02401 if (newCost < bestCost) { 02402 bestComp = i; 02403 bestCost = newCost; 02404 } 02405 } 02406 } 02407 imgComp->func = NIL(mdd_t); 02408 ImgComponentFree(imgComp); 02409 break; 02410 case 1: /* largest BDD size */ 02411 bestCost = 0; 02412 imgComp = ImgComponentAlloc(info); 02413 imgComp->func = img; 02414 ImgComponentGetSupport(imgComp); 02415 for (i = 0; i < array_n(delta); i++) { 02416 comp = array_fetch(ImgComponent_t *, delta, i); 02417 if (comp->intermediate) 02418 continue; 02419 index = (int)bdd_top_var_id(comp->var); 02420 if (imgComp->support[index]) { 02421 newCost = bdd_size(comp->func); 02422 if (newCost > bestCost) { 02423 bestComp = i; 02424 bestCost = newCost; 02425 } 02426 } 02427 } 02428 imgComp->func = NIL(mdd_t); 02429 ImgComponentFree(imgComp); 02430 break; 02431 case 2: /* top variable */ 02432 default: 02433 for (i = 0; i < array_n(delta); i++) { 02434 comp = array_fetch(ImgComponent_t *, delta, i); 02435 if (comp->intermediate) 02436 continue; 02437 index = (int)bdd_top_var_id(comp->var); 02438 if (bestComp == -1 || 02439 bdd_get_level_from_id(info->manager, index) < 02440 bdd_get_level_from_id(info->manager, bestVar)) { 02441 bestVar = index; 02442 bestComp = i; 02443 } 02444 } 02445 break; 02446 } 02447 assert(bestComp != -1); 02448 } 02449 02450 if (splitMethod == 0) 02451 return(bestVar); 02452 else 02453 return(bestComp); 02454 } 02455 02456 02468 static mdd_t * 02469 DomainCofactoring(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, 02470 array_t *relationArray, mdd_t *c, array_t **newVector, 02471 array_t **newRelationArray, mdd_t **cofactorCube, 02472 mdd_t **abstractCube) 02473 { 02474 mdd_t *res, *tmp; 02475 ImgComponent_t *comp, *comp1; 02476 array_t *vector1; 02477 int i, index, n, pos; 02478 mdd_t *newFrom, *var, *nsVar; 02479 mdd_t *cofactor, *abstract, *constIntermediate; 02480 array_t *tmpRelationArray; 02481 st_table *equivTable; 02482 int *ptr, *regularPtr; 02483 int size; 02484 02485 newFrom = mdd_dup(from); 02486 vector1 = array_alloc(ImgComponent_t *, 0); 02487 02488 if (relationArray) { 02489 cofactor = mdd_one(info->manager); 02490 abstract = mdd_one(info->manager); 02491 } else { 02492 cofactor = NIL(mdd_t); 02493 abstract = NIL(mdd_t); 02494 } 02495 02496 if (info->nIntermediateVars) { 02497 size = ImgVectorFunctionSize(vector); 02498 if (size == array_n(vector)) 02499 constIntermediate = NIL(mdd_t); 02500 else 02501 constIntermediate = mdd_one(info->manager); 02502 } else 02503 constIntermediate = NIL(mdd_t); 02504 02505 n = 0; 02506 equivTable = st_init_table(st_ptrcmp, st_ptrhash); 02507 index = (int)bdd_top_var_id(c); 02508 for (i = 0; i < array_n(vector); i++) { 02509 comp = array_fetch(ImgComponent_t *, vector, i); 02510 if (comp->support[index]) 02511 res = bdd_cofactor(comp->func, c); 02512 else 02513 res = mdd_dup(comp->func); 02514 if (bdd_is_tautology(res, 1)) { 02515 if (comp->intermediate) { 02516 tmp = constIntermediate; 02517 constIntermediate = mdd_and(tmp, comp->var, 1, 1); 02518 mdd_free(tmp); 02519 mdd_free(res); 02520 continue; 02521 } 02522 tmp = newFrom; 02523 newFrom = bdd_cofactor(tmp, comp->var); 02524 mdd_free(tmp); 02525 mdd_free(res); 02526 if (relationArray) { 02527 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 02528 tmp = abstract; 02529 abstract = mdd_and(tmp, nsVar, 1, 1); 02530 mdd_free(tmp); 02531 mdd_free(nsVar); 02532 } 02533 } else if (bdd_is_tautology(res, 0)) { 02534 if (comp->intermediate) { 02535 tmp = constIntermediate; 02536 constIntermediate = mdd_and(tmp, comp->var, 1, 0); 02537 mdd_free(tmp); 02538 mdd_free(res); 02539 continue; 02540 } 02541 tmp = newFrom; 02542 var = mdd_not(comp->var); 02543 newFrom = bdd_cofactor(tmp, var); 02544 mdd_free(tmp); 02545 mdd_free(var); 02546 mdd_free(res); 02547 if (relationArray) { 02548 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 02549 tmp = abstract; 02550 abstract = mdd_and(tmp, nsVar, 1, 1); 02551 mdd_free(tmp); 02552 mdd_free(nsVar); 02553 } 02554 } else { 02555 if (comp->intermediate) { 02556 comp1 = ImgComponentAlloc(info); 02557 comp1->var = mdd_dup(comp->var); 02558 comp1->func = res; 02559 if (mdd_equal(res, comp->func)) 02560 ImgSupportCopy(info, comp1->support, comp->support); 02561 else 02562 ImgComponentGetSupport(comp1); 02563 comp1->intermediate = 1; 02564 array_insert_last(ImgComponent_t *, vector1, comp1); 02565 n++; 02566 continue; 02567 } 02568 ptr = (int *)bdd_pointer(res); 02569 regularPtr = (int *)((unsigned long)ptr & ~01); 02570 if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) { 02571 comp1 = array_fetch(ImgComponent_t *, vector1, pos); 02572 if (mdd_equal(res, comp1->func)) { 02573 tmp = newFrom; 02574 newFrom = bdd_compose(tmp, comp->var, comp1->var); 02575 mdd_free(tmp); 02576 } else { 02577 tmp = newFrom; 02578 var = mdd_not(comp1->var); 02579 newFrom = bdd_compose(tmp, comp->var, var); 02580 mdd_free(tmp); 02581 mdd_free(var); 02582 } 02583 mdd_free(res); 02584 if (abstract) { 02585 nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 02586 tmp = abstract; 02587 abstract = mdd_and(tmp, nsVar, 1, 1); 02588 mdd_free(tmp); 02589 mdd_free(nsVar); 02590 } 02591 } else { 02592 comp1 = ImgComponentAlloc(info); 02593 comp1->var = mdd_dup(comp->var); 02594 comp1->func = res; 02595 if (mdd_equal(res, comp->func)) 02596 ImgSupportCopy(info, comp1->support, comp->support); 02597 else 02598 ImgComponentGetSupport(comp1); 02599 array_insert_last(ImgComponent_t *, vector1, comp1); 02600 st_insert(equivTable, (char *)regularPtr, (char *)(long)n); 02601 n++; 02602 } 02603 } 02604 } 02605 st_free_table(equivTable); 02606 02607 if (constIntermediate) { 02608 if (!bdd_is_tautology(constIntermediate, 1)) { 02609 mdd_t *tmpCofactor, *tmpAbstract; 02610 02611 if (relationArray) { 02612 vector1 = ImgComposeConstIntermediateVars(info, vector1, 02613 constIntermediate, 02614 &tmpCofactor, &tmpAbstract, 02615 NIL(mdd_t *), &newFrom); 02616 if (!bdd_is_tautology(tmpCofactor, 1)) { 02617 tmp = cofactor; 02618 cofactor = mdd_and(tmp, tmpCofactor, 1, 1); 02619 mdd_free(tmp); 02620 } 02621 mdd_free(tmpCofactor); 02622 if (!bdd_is_tautology(tmpAbstract, 1)) { 02623 tmp = abstract; 02624 abstract = mdd_and(tmp, tmpAbstract, 1, 1); 02625 mdd_free(tmp); 02626 } 02627 mdd_free(tmpAbstract); 02628 tmp = cofactor; 02629 cofactor = mdd_and(tmp, constIntermediate, 1, 1); 02630 mdd_free(tmp); 02631 } else { 02632 vector1 = ImgComposeConstIntermediateVars(info, vector1, 02633 constIntermediate, 02634 NIL(mdd_t *), NIL(mdd_t *), 02635 NIL(mdd_t *), &newFrom); 02636 } 02637 } 02638 mdd_free(constIntermediate); 02639 } 02640 02641 *newVector = vector1; 02642 02643 if (relationArray) { 02644 if (newRelationArray) 02645 *newRelationArray = relationArray; 02646 if (cofactorCube && abstractCube) { 02647 if (cofactor) { 02648 if (bdd_is_tautology(cofactor, 1)) { 02649 mdd_free(cofactor); 02650 *cofactorCube = mdd_dup(c); 02651 } else { 02652 *cofactorCube = mdd_and(cofactor, c, 1, 1); 02653 mdd_free(cofactor); 02654 } 02655 } 02656 if (abstract) 02657 *abstractCube = abstract; 02658 } else { 02659 if (bdd_is_tautology(cofactor, 1)) { 02660 *newRelationArray = ImgGetCofactoredRelationArray(relationArray, c); 02661 mdd_free(cofactor); 02662 } else { 02663 tmp = cofactor; 02664 cofactor = mdd_and(tmp, c, 1, 1); 02665 mdd_free(tmp); 02666 *newRelationArray = ImgGetCofactoredRelationArray(relationArray, 02667 cofactor); 02668 mdd_free(cofactor); 02669 } 02670 if (bdd_is_tautology(abstract, 1)) 02671 mdd_free(abstract); 02672 else { 02673 tmpRelationArray = *newRelationArray; 02674 *newRelationArray = ImgGetAbstractedRelationArray(info->manager, 02675 tmpRelationArray, 02676 abstract); 02677 mdd_free(abstract); 02678 if (tmpRelationArray != relationArray) 02679 mdd_array_free(tmpRelationArray); 02680 } 02681 } 02682 } else 02683 *newRelationArray = NIL(array_t); 02684 02685 return(newFrom); 02686 } 02687 02688 02698 static int 02699 CheckPreImageVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *image) 02700 { 02701 ImgComponent_t *comp, *imgComp; 02702 int i, id, size, status; 02703 02704 status = 1; 02705 if (info->nIntermediateVars) 02706 size = ImgVectorFunctionSize(vector); 02707 else 02708 size = array_n(vector); 02709 if (size != mdd_get_number_of_bdd_support(info->manager, image)) { 02710 fprintf(vis_stderr, 02711 "** tfm error: function vector length is different. (%d != %d)\n", 02712 size, mdd_get_number_of_bdd_support(info->manager, image)); 02713 status = 0; 02714 } 02715 02716 imgComp = ImgComponentAlloc(info); 02717 imgComp->func = image; 02718 ImgComponentGetSupport(imgComp); 02719 for (i = 0; i < array_n(vector); i++) { 02720 comp = array_fetch(ImgComponent_t *, vector, i); 02721 id = (int)bdd_top_var_id(comp->var); 02722 if (comp->intermediate) 02723 imgComp->support[id] = 2; 02724 else if (imgComp->support[id] == 0) { 02725 fprintf(vis_stderr, 02726 "** tfm error: variable index[%d] is not in constraint\n", id); 02727 status = 0; 02728 } else 02729 imgComp->support[id] = 2; 02730 } 02731 for (i = 0; i < info->nVars; i++) { 02732 if (imgComp->support[i] == 1) { 02733 fprintf(vis_stderr, 02734 "** tfm error: variable index[%d] is not in function vector\n", i); 02735 status = 0; 02736 } 02737 } 02738 imgComp->func = NIL(mdd_t); 02739 ImgComponentFree(imgComp); 02740 return(status); 02741 }
1.7.3