- Generated on Wed Oct 12 2011 00:34:49 for VIS by
1.7.3
|
VIS
|
00001 00037 #include "imgInt.h" 00038 00039 static char rcsid[] UNUSED = "$Id: imgHybrid.c,v 1.27 2008/11/27 02:19:53 fabio Exp $"; 00040 00041 /*---------------------------------------------------------------------------*/ 00042 /* Constant declarations */ 00043 /*---------------------------------------------------------------------------*/ 00044 00045 /*---------------------------------------------------------------------------*/ 00046 /* Type declarations */ 00047 /*---------------------------------------------------------------------------*/ 00048 00049 /*---------------------------------------------------------------------------*/ 00050 /* Structure declarations */ 00051 /*---------------------------------------------------------------------------*/ 00052 00053 /*---------------------------------------------------------------------------*/ 00054 /* Variable declarations */ 00055 /*---------------------------------------------------------------------------*/ 00056 00057 /*---------------------------------------------------------------------------*/ 00058 /* Macro declarations */ 00059 /*---------------------------------------------------------------------------*/ 00060 00063 /*---------------------------------------------------------------------------*/ 00064 /* Static function prototypes */ 00065 /*---------------------------------------------------------------------------*/ 00066 00067 static float ComputeSupportLambda(ImgTfmInfo_t *info, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, mdd_t *from, array_t *vector, int newRelationFlag, int preFlag, float *improvedLambda); 00068 00072 /*---------------------------------------------------------------------------*/ 00073 /* Definition of exported functions */ 00074 /*---------------------------------------------------------------------------*/ 00075 00076 00088 void 00089 Img_PrintHybridOptions(void) 00090 { 00091 ImgTfmOption_t *options; 00092 char dummy[80]; 00093 00094 options = ImgTfmGetOptions(Img_Hybrid_c); 00095 00096 switch (options->hybridMode) { 00097 case 0 : 00098 sprintf(dummy, "with only transition function"); 00099 break; 00100 case 1 : 00101 sprintf(dummy, "with both transition function and relation"); 00102 break; 00103 case 2 : 00104 sprintf(dummy, "with only transition relation"); 00105 break; 00106 default : 00107 sprintf(dummy, "invalid"); 00108 break; 00109 } 00110 fprintf(vis_stdout, "HYB: hybrid_mode = %d (%s)\n", 00111 options->hybridMode, dummy); 00112 00113 switch (options->trSplitMethod) { 00114 case 0 : 00115 sprintf(dummy, "support"); 00116 break; 00117 case 1 : 00118 sprintf(dummy, "estimate BDD size"); 00119 break; 00120 default : 00121 sprintf(dummy, "invalid"); 00122 break; 00123 } 00124 fprintf(vis_stdout, "HYB: hybrid_tr_split_method = %d (%s)\n", 00125 options->trSplitMethod, dummy); 00126 00127 if (options->buildPartialTR) 00128 sprintf(dummy, "yes"); 00129 else 00130 sprintf(dummy, "no"); 00131 fprintf(vis_stdout, "HYB: hybrid_build_partial_tr = %s\n", dummy); 00132 00133 fprintf(vis_stdout, "HYB: hybrid_partial_num_vars = %d\n", 00134 options->nPartialVars); 00135 00136 switch (options->partialMethod) { 00137 case 0 : 00138 sprintf(dummy, "BDD size"); 00139 break; 00140 case 1 : 00141 sprintf(dummy, "support"); 00142 break; 00143 default : 00144 sprintf(dummy, "invalid"); 00145 break; 00146 } 00147 fprintf(vis_stdout, "HYB: hybrid_partial_method = %d (%s)\n", 00148 options->partialMethod, dummy); 00149 00150 if (options->delayedSplit) 00151 sprintf(dummy, "yes"); 00152 else 00153 sprintf(dummy, "no"); 00154 fprintf(vis_stdout, "HYB: hybrid_delayed_split = %s\n", dummy); 00155 00156 fprintf(vis_stdout, "HYB: hybrid_split_min_depth = %d\n", 00157 options->splitMinDepth); 00158 fprintf(vis_stdout, "HYB: hybrid_split_max_depth = %d\n", 00159 options->splitMaxDepth); 00160 fprintf(vis_stdout, "HYB: hybrid_pre_split_min_depth = %d\n", 00161 options->preSplitMinDepth); 00162 fprintf(vis_stdout, "HYB: hybrid_pre_split_max_depth = %d\n", 00163 options->preSplitMaxDepth); 00164 00165 fprintf(vis_stdout, "HYB: hybrid_lambda_threshold = %.2f\n", 00166 options->lambdaThreshold); 00167 fprintf(vis_stdout, "HYB: hybrid_pre_lambda_threshold = %.2f\n", 00168 options->preLambdaThreshold); 00169 fprintf(vis_stdout, "HYB: hybrid_conjoin_vector_size = %d\n", 00170 options->conjoinVectorSize); 00171 fprintf(vis_stdout, "HYB: hybrid_conjoin_relation_size = %d\n", 00172 options->conjoinRelationSize); 00173 fprintf(vis_stdout, "HYB: hybrid_conjoin_relation_bdd_size = %d\n", 00174 options->conjoinRelationBddSize); 00175 fprintf(vis_stdout, "HYB: hybrid_improve_lambda = %.2f\n", 00176 options->improveLambda); 00177 fprintf(vis_stdout, "HYB: hybrid_improve_vector_size = %d\n", 00178 options->improveVectorSize); 00179 fprintf(vis_stdout, "HYB: hybrid_improve_vector_bdd_size = %.2f\n", 00180 options->improveVectorBddSize); 00181 00182 switch (options->decideMode) { 00183 case 0 : 00184 sprintf(dummy, "use only lambda"); 00185 break; 00186 case 1 : 00187 sprintf(dummy, "lambda + special check"); 00188 break; 00189 case 2 : 00190 sprintf(dummy, "lambda + improvement"); 00191 break; 00192 case 3 : 00193 sprintf(dummy, "use all"); 00194 break; 00195 default : 00196 sprintf(dummy, "invalid"); 00197 break; 00198 } 00199 fprintf(vis_stdout, "HYB: hybrid_decide_mode = %d (%s)\n", 00200 options->decideMode, dummy); 00201 00202 if (options->reorderWithFrom) 00203 sprintf(dummy, "yes"); 00204 else 00205 sprintf(dummy, "no"); 00206 fprintf(vis_stdout, "HYB: hybrid_reorder_with_from = %s\n", dummy); 00207 00208 if (options->preReorderWithFrom) 00209 sprintf(dummy, "yes"); 00210 else 00211 sprintf(dummy, "no"); 00212 fprintf(vis_stdout, "HYB: hybrid_pre_reorder_with_from = %s\n", dummy); 00213 00214 switch (options->lambdaMode) { 00215 case 0 : 00216 sprintf(dummy, "total lifetime with ps/pi variables"); 00217 break; 00218 case 1 : 00219 sprintf(dummy, "active lifetime with ps/pi variables"); 00220 break; 00221 case 2 : 00222 sprintf(dummy, "total lifetime with ps/ns/pi variables"); 00223 break; 00224 default : 00225 sprintf(dummy, "invalid"); 00226 break; 00227 } 00228 fprintf(vis_stdout, "HYB: hybrid_lambda_mode = %d (%s)\n", 00229 options->lambdaMode, dummy); 00230 00231 switch (options->preLambdaMode) { 00232 case 0 : 00233 sprintf(dummy, "total lifetime with ns/pi variables"); 00234 break; 00235 case 1 : 00236 sprintf(dummy, "active lifetime with ps/pi variables"); 00237 break; 00238 case 2 : 00239 sprintf(dummy, "total lifetime with ps/ns/pi variables"); 00240 break; 00241 case 3 : 00242 sprintf(dummy, "total lifetime with ps/pi variables"); 00243 break; 00244 default : 00245 sprintf(dummy, "invalid"); 00246 break; 00247 } 00248 fprintf(vis_stdout, "HYB: hybrid_pre_lambda_mode = %d (%s)\n", 00249 options->preLambdaMode, dummy); 00250 00251 if (options->lambdaWithFrom) 00252 sprintf(dummy, "yes"); 00253 else 00254 sprintf(dummy, "no"); 00255 fprintf(vis_stdout, "HYB: hybrid_lambda_with_from = %s\n", dummy); 00256 00257 if (options->lambdaWithTr) 00258 sprintf(dummy, "yes"); 00259 else 00260 sprintf(dummy, "no"); 00261 fprintf(vis_stdout, "HYB: hybrid_lambda_with_tr = %s\n", dummy); 00262 00263 if (options->lambdaWithClustering) 00264 sprintf(dummy, "yes"); 00265 else 00266 sprintf(dummy, "no"); 00267 fprintf(vis_stdout, "HYB: hybrid_lambda_with_clustering = %s\n", dummy); 00268 00269 if (options->synchronizeTr) 00270 sprintf(dummy, "yes"); 00271 else 00272 sprintf(dummy, "no"); 00273 fprintf(vis_stdout, "HYB: hybrid_synchronize_tr = %s\n", dummy); 00274 00275 if (options->imgKeepPiInTr) 00276 sprintf(dummy, "yes"); 00277 else 00278 sprintf(dummy, "no"); 00279 fprintf(vis_stdout, "HYB: hybrid_img_keep_pi = %s\n", dummy); 00280 00281 if (options->preKeepPiInTr) 00282 sprintf(dummy, "yes"); 00283 else 00284 sprintf(dummy, "no"); 00285 fprintf(vis_stdout, "HYB: hybrid_pre_keep_pi = %s\n", dummy); 00286 00287 if (options->preCanonical) 00288 sprintf(dummy, "yes"); 00289 else 00290 sprintf(dummy, "no"); 00291 fprintf(vis_stdout, "HYB: hybrid_pre_canonical = %s\n", dummy); 00292 00293 switch (options->trMethod) { 00294 case Img_Iwls95_c : 00295 sprintf(dummy, "IWLS95"); 00296 break; 00297 case Img_Mlp_c : 00298 sprintf(dummy, "MLP"); 00299 break; 00300 default : 00301 sprintf(dummy, "invalid"); 00302 break; 00303 } 00304 fprintf(vis_stdout, "HYB: hybrid_tr_method = %s\n", dummy); 00305 00306 FREE(options); 00307 } 00308 00309 00310 /*---------------------------------------------------------------------------*/ 00311 /* Definition of internal functions */ 00312 /*---------------------------------------------------------------------------*/ 00313 00314 00324 int 00325 ImgDecideSplitOrConjoin(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, 00326 int preFlag, array_t *relationArray, 00327 mdd_t *cofactorCube, mdd_t *abstractCube, 00328 int useBothFlag, int depth) 00329 { 00330 int conjoin = 0; 00331 float lambda, improvedLambda; 00332 int vectorBddSize, vectorSize; 00333 int improved; 00334 int minDepth; 00335 int checkSpecialCases; 00336 int checkImprovement; 00337 int relationSize = 0; 00338 00339 if (!preFlag) { 00340 if (vector && array_n(vector) <= 2) 00341 return(0); /* terminal case */ 00342 } 00343 00344 if (info->option->decideMode == 1 || info->option->decideMode == 3) 00345 checkSpecialCases = 1; 00346 else 00347 checkSpecialCases = 0; 00348 if (info->option->decideMode == 2 || info->option->decideMode == 3) 00349 checkImprovement = 1; 00350 else 00351 checkImprovement = 0; 00352 00353 if (checkSpecialCases) { 00354 if (vector && array_n(vector) <= info->option->conjoinVectorSize) { 00355 if (preFlag) 00356 info->nConjoinsB++; 00357 else 00358 info->nConjoins++; 00359 if (info->option->printLambda) { 00360 fprintf(vis_stdout, "%d: conjoin - small vector size (%d)\n", 00361 depth, array_n(vector)); 00362 } 00363 return(1); 00364 } 00365 } 00366 00367 if (preFlag) 00368 minDepth = info->option->preSplitMinDepth; 00369 else 00370 minDepth = info->option->splitMinDepth; 00371 00372 if (useBothFlag && relationArray && vector) { 00373 lambda = ComputeSupportLambda(info, relationArray, cofactorCube, 00374 abstractCube, from, vector, 00375 0, preFlag, &improvedLambda); 00376 } else if (relationArray) { 00377 if (checkSpecialCases) { 00378 if (array_n(relationArray) <= info->option->conjoinRelationSize || 00379 (relationSize = (int)bdd_size_multiple(relationArray)) <= 00380 info->option->conjoinRelationBddSize) { 00381 if (preFlag) 00382 info->nConjoinsB++; 00383 else 00384 info->nConjoins++; 00385 if (info->option->printLambda) { 00386 fprintf(vis_stdout, "%d: conjoin - small relation array (%d, %ld)\n", 00387 depth, array_n(relationArray), 00388 bdd_size_multiple(relationArray)); 00389 } 00390 return(1); 00391 } 00392 } 00393 00394 lambda = ComputeSupportLambda(info, relationArray, cofactorCube, 00395 abstractCube, from, NIL(array_t), 00396 0, preFlag, &improvedLambda); 00397 } else { 00398 int i; 00399 ImgComponent_t *comp; 00400 00401 relationArray = array_alloc(mdd_t *, 0); 00402 for (i = 0; i < array_n(vector); i++) { 00403 comp = array_fetch(ImgComponent_t *, vector, i); 00404 array_insert_last(mdd_t *, relationArray, comp->func); 00405 } 00406 00407 lambda = ComputeSupportLambda(info, relationArray, NIL(mdd_t), 00408 NIL(mdd_t), from, NIL(array_t), 00409 1, preFlag, &improvedLambda); 00410 00411 array_free(relationArray); 00412 } 00413 00414 if ((preFlag == 0 && lambda <= info->option->lambdaThreshold) || 00415 (preFlag == 1 && lambda <= info->option->preLambdaThreshold)) { 00416 if (preFlag) 00417 info->nConjoinsB++; 00418 else 00419 info->nConjoins++; 00420 if (info->option->printLambda) { 00421 fprintf(vis_stdout, "%d: conjoin - small lambda (%.2f)\n", 00422 depth, lambda); 00423 } 00424 conjoin = 1; 00425 } else { 00426 if (checkImprovement) { 00427 if (vector) { 00428 vectorBddSize = ImgVectorBddSize(vector); 00429 vectorSize = array_n(vector); 00430 if (depth == minDepth || 00431 improvedLambda >= info->option->improveLambda || 00432 ((float)vectorBddSize * 100.0 / (float)info->prevVectorBddSize) <= 00433 info->option->improveVectorBddSize || 00434 (info->prevVectorSize - vectorSize) >= 00435 info->option->improveVectorSize) { 00436 improved = 1; 00437 } else 00438 improved = 0; 00439 info->prevVectorBddSize = vectorBddSize; 00440 info->prevVectorSize = vectorSize; 00441 } else { 00442 if (relationSize) 00443 vectorBddSize = relationSize; 00444 else 00445 vectorBddSize = (int)bdd_size_multiple(relationArray); 00446 if (depth == minDepth || 00447 improvedLambda >= info->option->improveLambda || 00448 ((float)vectorBddSize * 100.0 / (float)info->prevVectorBddSize) <= 00449 info->option->improveVectorBddSize) { 00450 improved = 1; 00451 } else 00452 improved = 0; 00453 info->prevVectorBddSize = vectorBddSize; 00454 } 00455 if (improved) { 00456 if (preFlag) 00457 info->nSplitsB++; 00458 else 00459 info->nSplits++; 00460 if (info->option->printLambda) { 00461 fprintf(vis_stdout, "%d: split - big lambda (%.2f) - improved\n", 00462 depth, lambda); 00463 } 00464 conjoin = 0; 00465 } else { 00466 if (preFlag) 00467 info->nConjoinsB++; 00468 else 00469 info->nConjoins++; 00470 if (info->option->printLambda) { 00471 fprintf(vis_stdout, "%d: conjon - big lambda (%.2f) - not improved\n", 00472 depth, lambda); 00473 } 00474 conjoin = 1; 00475 } 00476 } else { 00477 if (preFlag) 00478 info->nSplitsB++; 00479 else 00480 info->nSplits++; 00481 if (info->option->printLambda) { 00482 fprintf(vis_stdout, "%d: split - big lambda (%.2f)\n", 00483 depth, lambda); 00484 } 00485 conjoin = 0; 00486 } 00487 } 00488 00489 return(conjoin); /* 0 : split, 1 : conjoin */ 00490 } 00491 00492 00502 mdd_t * 00503 ImgImageByHybrid(ImgTfmInfo_t *info, array_t *vector, mdd_t *from) 00504 { 00505 int i, j, nVars; 00506 array_t *relationArray; 00507 mdd_t *result, *domain, *relation, *var, *nextVar; 00508 ImgComponent_t *comp; 00509 char *support; 00510 array_t *smoothVarsBddArray, *introducedVarsBddArray; 00511 array_t *domainVarsBddArray; 00512 int bddId; 00513 00514 if (from && bdd_is_tautology(from, 0)) 00515 return(mdd_zero(info->manager)); 00516 00517 nVars = info->nVars; 00518 support = ALLOC(char, sizeof(char) * nVars); 00519 memset(support, 0, sizeof(char) * nVars); 00520 00521 relationArray = array_alloc(mdd_t *, 0); 00522 introducedVarsBddArray = array_alloc(mdd_t *, 0); 00523 00524 for (i = 0; i < array_n(vector); i++) { 00525 comp = array_fetch(ImgComponent_t *, vector, i); 00526 if (comp->intermediate) { 00527 relation = mdd_xnor(comp->var, comp->func); 00528 bddId = (int)bdd_top_var_id(comp->var); 00529 support[bddId] = 1; 00530 } else { 00531 nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 00532 relation = mdd_xnor(nextVar, comp->func); 00533 array_insert_last(mdd_t *, introducedVarsBddArray, nextVar); 00534 } 00535 array_insert_last(mdd_t *, relationArray, relation); 00536 00537 for (j = 0; j < nVars; j++) 00538 support[j] = support[j] | comp->support[j]; 00539 } 00540 00541 if (from && (!bdd_is_tautology(from, 1))) { 00542 if (info->option->reorderWithFrom) 00543 array_insert_last(mdd_t *, relationArray, mdd_dup(from)); 00544 00545 comp = ImgComponentAlloc(info); 00546 comp->func = from; 00547 ImgComponentGetSupport(comp); 00548 for (i = 0; i < nVars; i++) 00549 support[i] = support[i] | comp->support[i]; 00550 comp->func = NIL(mdd_t); 00551 ImgComponentFree(comp); 00552 } 00553 00554 smoothVarsBddArray = array_alloc(mdd_t *, 0); 00555 if (!info->option->reorderWithFrom) 00556 domainVarsBddArray = array_alloc(mdd_t *, 0); 00557 else 00558 domainVarsBddArray = NIL(array_t); 00559 for (i = 0; i < nVars; i++) { 00560 if (support[i]) { 00561 var = bdd_var_with_index(info->manager, i); 00562 if ((!from) || info->option->reorderWithFrom) 00563 array_insert_last(mdd_t *, smoothVarsBddArray, var); 00564 else { 00565 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)) || 00566 (info->intermediateVarsTable && 00567 st_lookup(info->intermediateVarsTable, (char *)(long)i, 00568 NIL(char *)))) { 00569 array_insert_last(mdd_t *, smoothVarsBddArray, var); 00570 } else { 00571 array_insert_last(mdd_t *, domainVarsBddArray, var); 00572 } 00573 } 00574 } 00575 } 00576 FREE(support); 00577 00578 if ((!from) || info->option->reorderWithFrom) { 00579 result = ImgMultiwayLinearAndSmooth(info->manager, 00580 relationArray, 00581 smoothVarsBddArray, 00582 introducedVarsBddArray, 00583 info->option->trMethod, 00584 Img_Forward_c, 00585 info->trmOption); 00586 } else { 00587 result = ImgMultiwayLinearAndSmoothWithFrom(info->manager, 00588 relationArray, from, 00589 smoothVarsBddArray, 00590 domainVarsBddArray, 00591 introducedVarsBddArray, 00592 info->option->trMethod, 00593 Img_Forward_c, 00594 info->trmOption); 00595 mdd_array_free(domainVarsBddArray); 00596 } 00597 mdd_array_free(relationArray); 00598 mdd_array_free(smoothVarsBddArray); 00599 mdd_array_free(introducedVarsBddArray); 00600 domain = ImgSubstitute(result, info->functionData, Img_R2D_c); 00601 mdd_free(result); 00602 return(domain); 00603 } 00604 00605 00615 mdd_t * 00616 ImgImageByHybridWithStaticSplit(ImgTfmInfo_t *info, array_t *vector, 00617 mdd_t *from, array_t *relationArray, 00618 mdd_t *cofactorCube, mdd_t *abstractCube) 00619 { 00620 int i, j; 00621 array_t *mergedRelationArray; 00622 mdd_t *result, *domain, *relation, *var, *nextVar; 00623 ImgComponent_t *comp, *supportComp; 00624 int nVars; 00625 char *support; 00626 array_t *smoothVarsBddArray, *introducedVarsBddArray; 00627 array_t *domainVarsBddArray; 00628 00629 if (from && bdd_is_tautology(from, 0)) 00630 return(mdd_zero(info->manager)); 00631 00632 if (cofactorCube && abstractCube) { 00633 if (!bdd_is_tautology(cofactorCube, 1) && 00634 !bdd_is_tautology(abstractCube, 1)) { 00635 mergedRelationArray = ImgGetCofactoredAbstractedRelationArray( 00636 info->manager, relationArray, 00637 cofactorCube, abstractCube); 00638 } else if (!bdd_is_tautology(cofactorCube, 1)) { 00639 mergedRelationArray = ImgGetCofactoredRelationArray(relationArray, 00640 cofactorCube); 00641 } else if (!bdd_is_tautology(abstractCube, 1)) { 00642 mergedRelationArray = ImgGetAbstractedRelationArray(info->manager, 00643 relationArray, 00644 abstractCube); 00645 } else 00646 mergedRelationArray = mdd_array_duplicate(relationArray); 00647 } else 00648 mergedRelationArray = mdd_array_duplicate(relationArray); 00649 00650 nVars = info->nVars; 00651 support = ALLOC(char, sizeof(char) * nVars); 00652 memset(support, 0, sizeof(char) * nVars); 00653 00654 supportComp = ImgComponentAlloc(info); 00655 for (i = 0; i < array_n(mergedRelationArray); i++) { 00656 supportComp->func = array_fetch(mdd_t *, mergedRelationArray, i);; 00657 ImgSupportClear(info, supportComp->support); 00658 ImgComponentGetSupport(supportComp); 00659 for (j = 0; j < nVars; j++) 00660 support[j] = support[j] | supportComp->support[j]; 00661 } 00662 00663 if (vector && array_n(vector) > 0) { 00664 for (i = 0; i < array_n(vector); i++) { 00665 comp = array_fetch(ImgComponent_t *, vector, i); 00666 if (comp->intermediate) { 00667 relation = mdd_xnor(comp->var, comp->func); 00668 support[(int)bdd_top_var_id(comp->var)] = 1; 00669 } else { 00670 nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 00671 relation = mdd_xnor(nextVar, comp->func); 00672 support[(int)bdd_top_var_id(nextVar)] = 1; 00673 mdd_free(nextVar); 00674 } 00675 array_insert_last(mdd_t *, mergedRelationArray, relation); 00676 00677 for (j = 0; j < nVars; j++) 00678 support[j] = support[j] | comp->support[j]; 00679 } 00680 } 00681 00682 if (from) { 00683 if ((!bdd_is_tautology(from, 1)) && info->option->reorderWithFrom) 00684 array_insert_last(mdd_t *, mergedRelationArray, mdd_dup(from)); 00685 00686 supportComp->func = from; 00687 ImgSupportClear(info, supportComp->support); 00688 ImgComponentGetSupport(supportComp); 00689 for (i = 0; i < nVars; i++) 00690 support[i] = support[i] | supportComp->support[i]; 00691 } 00692 supportComp->func = NIL(mdd_t); 00693 ImgComponentFree(supportComp); 00694 00695 smoothVarsBddArray = array_alloc(mdd_t *, 0); 00696 introducedVarsBddArray = array_alloc(mdd_t *, 0); 00697 if (!info->option->reorderWithFrom) 00698 domainVarsBddArray = array_alloc(mdd_t *, 0); 00699 else 00700 domainVarsBddArray = NIL(array_t); 00701 for (i = 0; i < nVars; i++) { 00702 if (support[i]) { 00703 var = bdd_var_with_index(info->manager, i); 00704 if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) 00705 array_insert_last(mdd_t *, introducedVarsBddArray, var); 00706 else if ((!from) || info->option->reorderWithFrom) 00707 array_insert_last(mdd_t *, smoothVarsBddArray, var); 00708 else { 00709 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)) || 00710 (info->intermediateVarsTable && 00711 st_lookup(info->intermediateVarsTable, (char *)(long)i, 00712 NIL(char *)))) { 00713 array_insert_last(mdd_t *, smoothVarsBddArray, var); 00714 } else { 00715 array_insert_last(mdd_t *, domainVarsBddArray, var); 00716 } 00717 } 00718 } 00719 } 00720 FREE(support); 00721 00722 if ((!from) || info->option->reorderWithFrom) { 00723 result = ImgMultiwayLinearAndSmooth(info->manager, 00724 mergedRelationArray, 00725 smoothVarsBddArray, 00726 introducedVarsBddArray, 00727 info->option->trMethod, 00728 Img_Forward_c, 00729 info->trmOption); 00730 } else { 00731 result = ImgMultiwayLinearAndSmoothWithFrom(info->manager, 00732 mergedRelationArray, from, 00733 smoothVarsBddArray, 00734 domainVarsBddArray, 00735 introducedVarsBddArray, 00736 info->option->trMethod, 00737 Img_Forward_c, 00738 info->trmOption); 00739 mdd_array_free(domainVarsBddArray); 00740 } 00741 mdd_array_free(mergedRelationArray); 00742 mdd_array_free(smoothVarsBddArray); 00743 mdd_array_free(introducedVarsBddArray); 00744 00745 domain = ImgSubstitute(result, info->functionData, Img_R2D_c); 00746 mdd_free(result); 00747 return(domain); 00748 } 00749 00750 00760 mdd_t * 00761 ImgPreImageByHybrid(ImgTfmInfo_t *info, array_t *vector, mdd_t *from) 00762 { 00763 int i, j, nVars; 00764 array_t *relationArray; 00765 mdd_t *result, *relation, *var, *nextVar; 00766 ImgComponent_t *comp; 00767 char *support; 00768 array_t *smoothVarsBddArray, *introducedVarsBddArray; 00769 array_t *rangeVarsBddArray; 00770 mdd_t *fromRange; 00771 00772 if (bdd_is_tautology(from, 1)) 00773 return(mdd_one(info->manager)); 00774 else if (bdd_is_tautology(from, 0)) 00775 return(mdd_zero(info->manager)); 00776 00777 nVars = info->nVars; 00778 support = ALLOC(char, sizeof(char) * nVars); 00779 memset(support, 0, sizeof(char) * nVars); 00780 00781 relationArray = array_alloc(mdd_t *, 0); 00782 00783 for (i = 0; i < array_n(vector); i++) { 00784 comp = array_fetch(ImgComponent_t *, vector, i); 00785 if (comp->intermediate) { 00786 relation = mdd_xnor(comp->var, comp->func); 00787 support[(int)bdd_top_var_id(comp->var)] = 1; 00788 } else { 00789 nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 00790 relation = mdd_xnor(nextVar, comp->func); 00791 support[(int)bdd_top_var_id(nextVar)] = 1; 00792 mdd_free(nextVar); 00793 } 00794 array_insert_last(mdd_t *, relationArray, relation); 00795 00796 for (j = 0; j < nVars; j++) 00797 support[j] = support[j] | comp->support[j]; 00798 } 00799 00800 fromRange = ImgSubstitute(from, info->functionData, Img_D2R_c); 00801 comp = ImgComponentAlloc(info); 00802 comp->func = fromRange; 00803 ImgComponentGetSupport(comp); 00804 for (i = 0; i < nVars; i++) 00805 support[i] = support[i] | comp->support[i]; 00806 comp->func = NIL(mdd_t); 00807 ImgComponentFree(comp); 00808 00809 smoothVarsBddArray = array_alloc(mdd_t *, 0); 00810 introducedVarsBddArray = array_alloc(mdd_t *, 0); 00811 if (!info->option->preReorderWithFrom) 00812 rangeVarsBddArray = array_alloc(mdd_t *, 0); 00813 else 00814 rangeVarsBddArray = NIL(array_t); 00815 for (i = 0; i < nVars; i++) { 00816 if (support[i]) { 00817 var = bdd_var_with_index(info->manager, i); 00818 if (info->intermediateVarsTable && 00819 st_lookup(info->intermediateVarsTable, (char *)(long)i, 00820 NIL(char *))) { 00821 array_insert_last(mdd_t *, smoothVarsBddArray, var); 00822 } else if (st_lookup(info->rangeVarsTable, (char *)(long)i, 00823 NIL(char *))) { 00824 if (info->option->preReorderWithFrom) 00825 array_insert_last(mdd_t *, smoothVarsBddArray, var); 00826 else 00827 array_insert_last(mdd_t *, rangeVarsBddArray, var); 00828 } else { 00829 if (info->preKeepPiInTr) 00830 array_insert_last(mdd_t *, introducedVarsBddArray, var); 00831 else { 00832 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, 00833 NIL(char *))) { 00834 array_insert_last(mdd_t *, smoothVarsBddArray, var); 00835 } else 00836 array_insert_last(mdd_t *, introducedVarsBddArray, var); 00837 } 00838 } 00839 } 00840 } 00841 FREE(support); 00842 00843 if (info->option->preReorderWithFrom) { 00844 array_insert_last(mdd_t *, relationArray, fromRange); 00845 result = ImgMultiwayLinearAndSmooth(info->manager, 00846 relationArray, 00847 smoothVarsBddArray, 00848 introducedVarsBddArray, 00849 info->option->trMethod, 00850 Img_Backward_c, 00851 info->trmOption); 00852 } else { 00853 result = ImgMultiwayLinearAndSmoothWithFrom(info->manager, 00854 relationArray, fromRange, 00855 smoothVarsBddArray, 00856 rangeVarsBddArray, 00857 introducedVarsBddArray, 00858 info->option->trMethod, 00859 Img_Backward_c, 00860 info->trmOption); 00861 mdd_free(fromRange); 00862 mdd_array_free(rangeVarsBddArray); 00863 } 00864 mdd_array_free(relationArray); 00865 mdd_array_free(smoothVarsBddArray); 00866 mdd_array_free(introducedVarsBddArray); 00867 return(result); 00868 } 00869 00870 00880 mdd_t * 00881 ImgPreImageByHybridWithStaticSplit(ImgTfmInfo_t *info, array_t *vector, 00882 mdd_t *from, array_t *relationArray, 00883 mdd_t *cofactorCube, mdd_t *abstractCube) 00884 { 00885 int i, j; 00886 array_t *mergedRelationArray; 00887 mdd_t *result, *relation, *var, *nextVar, *fromRange; 00888 ImgComponent_t *comp, *supportComp; 00889 int nVars; 00890 char *support; 00891 array_t *smoothVarsBddArray, *introducedVarsBddArray; 00892 array_t *rangeVarsBddArray; 00893 00894 if (bdd_is_tautology(from, 1)) 00895 return(mdd_one(info->manager)); 00896 if (bdd_is_tautology(from, 0)) 00897 return(mdd_zero(info->manager)); 00898 00899 if (cofactorCube && abstractCube) { 00900 if (!bdd_is_tautology(cofactorCube, 1) && 00901 !bdd_is_tautology(abstractCube, 1)) { 00902 mergedRelationArray = ImgGetCofactoredAbstractedRelationArray( 00903 info->manager, relationArray, 00904 cofactorCube, abstractCube); 00905 } else if (!bdd_is_tautology(cofactorCube, 1)) { 00906 mergedRelationArray = ImgGetCofactoredRelationArray(relationArray, 00907 cofactorCube); 00908 } else if (!bdd_is_tautology(abstractCube, 1)) { 00909 mergedRelationArray = ImgGetAbstractedRelationArray(info->manager, 00910 relationArray, 00911 abstractCube); 00912 } else 00913 mergedRelationArray = mdd_array_duplicate(relationArray); 00914 } else 00915 mergedRelationArray = mdd_array_duplicate(relationArray); 00916 00917 nVars = info->nVars; 00918 support = ALLOC(char, sizeof(char) * nVars); 00919 memset(support, 0, sizeof(char) * nVars); 00920 00921 supportComp = ImgComponentAlloc(info); 00922 for (i = 0; i < array_n(mergedRelationArray); i++) { 00923 supportComp->func = array_fetch(mdd_t *, mergedRelationArray, i);; 00924 ImgSupportClear(info, supportComp->support); 00925 ImgComponentGetSupport(supportComp); 00926 for (j = 0; j < nVars; j++) 00927 support[j] = support[j] | supportComp->support[j]; 00928 } 00929 00930 if (vector && array_n(vector) > 0) { 00931 for (i = 0; i < array_n(vector); i++) { 00932 comp = array_fetch(ImgComponent_t *, vector, i); 00933 if (comp->intermediate) { 00934 relation = mdd_xnor(comp->var, comp->func); 00935 support[(int)bdd_top_var_id(comp->var)] = 1; 00936 } else { 00937 nextVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 00938 relation = mdd_xnor(nextVar, comp->func); 00939 support[(int)bdd_top_var_id(nextVar)] = 1; 00940 mdd_free(nextVar); 00941 } 00942 array_insert_last(mdd_t *, mergedRelationArray, relation); 00943 00944 for (j = 0; j < nVars; j++) 00945 support[j] = support[j] | comp->support[j]; 00946 } 00947 } 00948 00949 fromRange = ImgSubstitute(from, info->functionData, Img_D2R_c); 00950 supportComp->func = fromRange; 00951 ImgSupportClear(info, supportComp->support); 00952 ImgComponentGetSupport(supportComp); 00953 for (i = 0; i < nVars; i++) 00954 support[i] = support[i] | supportComp->support[i]; 00955 supportComp->func = NIL(mdd_t); 00956 ImgComponentFree(supportComp); 00957 00958 smoothVarsBddArray = array_alloc(mdd_t *, 0); 00959 introducedVarsBddArray = array_alloc(mdd_t *, 0); 00960 if (!info->option->preReorderWithFrom) 00961 rangeVarsBddArray = array_alloc(mdd_t *, 0); 00962 else 00963 rangeVarsBddArray = NIL(array_t); 00964 for (i = 0; i < nVars; i++) { 00965 if (support[i]) { 00966 var = bdd_var_with_index(info->manager, i); 00967 if (info->intermediateVarsTable && 00968 st_lookup(info->intermediateVarsTable, (char *)(long)i, 00969 NIL(char *))) { 00970 array_insert_last(mdd_t *, smoothVarsBddArray, var); 00971 } else if (st_lookup(info->rangeVarsTable, (char *)(long)i, 00972 NIL(char *))) { 00973 if (info->option->preReorderWithFrom) 00974 array_insert_last(mdd_t *, smoothVarsBddArray, var); 00975 else 00976 array_insert_last(mdd_t *, rangeVarsBddArray, var); 00977 } else { 00978 if (info->preKeepPiInTr) 00979 array_insert_last(mdd_t *, introducedVarsBddArray, var); 00980 else { 00981 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, 00982 NIL(char *))) { 00983 array_insert_last(mdd_t *, smoothVarsBddArray, var); 00984 } else 00985 array_insert_last(mdd_t *, introducedVarsBddArray, var); 00986 } 00987 } 00988 } 00989 } 00990 FREE(support); 00991 00992 if (info->option->preReorderWithFrom) { 00993 array_insert_last(mdd_t *, mergedRelationArray, fromRange); 00994 result = ImgMultiwayLinearAndSmooth(info->manager, 00995 mergedRelationArray, 00996 smoothVarsBddArray, 00997 introducedVarsBddArray, 00998 info->option->trMethod, 00999 Img_Backward_c, 01000 info->trmOption); 01001 } else { 01002 result = ImgMultiwayLinearAndSmoothWithFrom(info->manager, 01003 mergedRelationArray, fromRange, 01004 smoothVarsBddArray, 01005 rangeVarsBddArray, 01006 introducedVarsBddArray, 01007 info->option->trMethod, 01008 Img_Backward_c, 01009 info->trmOption); 01010 mdd_free(fromRange); 01011 mdd_array_free(rangeVarsBddArray); 01012 } 01013 mdd_array_free(mergedRelationArray); 01014 mdd_array_free(smoothVarsBddArray); 01015 mdd_array_free(introducedVarsBddArray); 01016 01017 return(result); 01018 } 01019 01020 01030 int 01031 ImgCheckEquivalence(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, 01032 mdd_t *cofactorCube, mdd_t *abstractCube, int preFlag) 01033 { 01034 int i, equal; 01035 mdd_t *product1, *product2; 01036 mdd_t *var, *tmp, *relation; 01037 ImgComponent_t *comp; 01038 array_t *newRelationArray, *tmpRelationArray; 01039 array_t *domainVarBddArray, *quantifyVarBddArray; 01040 01041 tmpRelationArray = array_alloc(mdd_t *, 0); 01042 for (i = 0; i < array_n(vector); i++) { 01043 comp = array_fetch(ImgComponent_t *, vector, i); 01044 if (comp->intermediate) 01045 relation = mdd_xnor(comp->var, comp->func); 01046 else { 01047 var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 01048 relation = mdd_xnor(var, comp->func); 01049 mdd_free(var); 01050 } 01051 array_insert_last(mdd_t *, tmpRelationArray, relation); 01052 } 01053 01054 if (preFlag) { 01055 if (info->preKeepPiInTr) { 01056 quantifyVarBddArray = array_alloc(mdd_t *, 0); 01057 domainVarBddArray = array_join(info->domainVarBddArray, 01058 info->quantifyVarBddArray); 01059 } else { 01060 quantifyVarBddArray = info->quantifyVarBddArray; 01061 domainVarBddArray = info->domainVarBddArray; 01062 } 01063 newRelationArray = ImgClusterRelationArray(info->manager, 01064 info->functionData, info->option->trMethod, Img_Backward_c, 01065 info->trmOption, tmpRelationArray, domainVarBddArray, 01066 quantifyVarBddArray, info->rangeVarBddArray, 01067 NIL(array_t *), NIL(array_t *), 0); 01068 if (info->preKeepPiInTr) { 01069 array_free(quantifyVarBddArray); 01070 array_free(domainVarBddArray); 01071 } 01072 } else { 01073 newRelationArray = ImgClusterRelationArray(info->manager, 01074 info->functionData, info->option->trMethod, Img_Forward_c, 01075 info->trmOption, tmpRelationArray, info->domainVarBddArray, 01076 info->quantifyVarBddArray, info->rangeVarBddArray, 01077 NIL(array_t *), NIL(array_t *), 0); 01078 } 01079 mdd_array_free(tmpRelationArray); 01080 01081 product1 = mdd_one(info->manager); 01082 for (i = 0; i < array_n(newRelationArray); i++) { 01083 relation = array_fetch(mdd_t *, newRelationArray, i); 01084 tmp = product1; 01085 product1 = mdd_and(tmp, relation, 1, 1); 01086 mdd_free(tmp); 01087 } 01088 mdd_array_free(newRelationArray); 01089 01090 if (cofactorCube && abstractCube) { 01091 newRelationArray = ImgGetCofactoredAbstractedRelationArray(info->manager, 01092 relationArray, cofactorCube, abstractCube); 01093 } else 01094 newRelationArray = relationArray; 01095 01096 product2 = mdd_one(info->manager); 01097 for (i = 0; i < array_n(newRelationArray); i++) { 01098 relation = array_fetch(mdd_t *, newRelationArray, i); 01099 tmp = product2; 01100 product2 = mdd_and(tmp, relation, 1, 1); 01101 mdd_free(tmp); 01102 } 01103 01104 if (newRelationArray != relationArray) 01105 mdd_array_free(newRelationArray); 01106 01107 if (mdd_equal(product1, product2)) 01108 equal = 1; 01109 else 01110 equal = 0; 01111 01112 mdd_free(product1); 01113 mdd_free(product2); 01114 01115 return(equal); 01116 } 01117 01118 01131 int 01132 ImgCheckMatching(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray) 01133 { 01134 int i, equal = 1; 01135 mdd_t *var, *relation; 01136 ImgComponent_t *comp; 01137 st_table *relationTable; 01138 int *ptr; 01139 01140 relationTable = st_init_table(st_ptrcmp, st_ptrhash); 01141 01142 for (i = 0; i < array_n(relationArray); i++) { 01143 relation = array_fetch(mdd_t *, relationArray, i); 01144 ptr = (int *)bdd_pointer(relation); 01145 st_insert(relationTable, (char *)ptr, NULL); 01146 } 01147 01148 for (i = 0; i < array_n(vector); i++) { 01149 comp = array_fetch(ImgComponent_t *, vector, i); 01150 if (comp->intermediate) 01151 relation = mdd_xnor(comp->var, comp->func); 01152 else { 01153 var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 01154 relation = mdd_xnor(var, comp->func); 01155 mdd_free(var); 01156 } 01157 ptr = (int *)bdd_pointer(relation); 01158 if (!st_lookup(relationTable, (char *)ptr, NULL)) { 01159 if (comp->intermediate) { 01160 fprintf(vis_stderr, 01161 "Error : relation of varId[%d - intermediate] not found\n", 01162 (int)bdd_top_var_id(comp->var)); 01163 } else { 01164 fprintf(vis_stderr, "Error : relation of varId[%d] not found\n", 01165 (int)bdd_top_var_id(comp->var)); 01166 } 01167 equal = 0; 01168 } 01169 mdd_free(relation); 01170 } 01171 01172 st_free_table(relationTable); 01173 return(equal); 01174 } 01175 01176 01177 /*---------------------------------------------------------------------------*/ 01178 /* Definition of static functions */ 01179 /*---------------------------------------------------------------------------*/ 01180 01181 01193 static float 01194 ComputeSupportLambda(ImgTfmInfo_t *info, array_t *relationArray, 01195 mdd_t *cofactorCube, mdd_t *abstractCube, 01196 mdd_t *from, array_t *vector, int newRelationFlag, 01197 int preFlag, float *improvedLambda) 01198 { 01199 array_t *newRelationArray, *clusteredRelationArray; 01200 ImgComponent_t *comp; 01201 int i, j, nVars, nSupports; 01202 mdd_t *newFrom, *var; 01203 char *support; 01204 array_t *smoothVarsBddArray, *introducedVarsBddArray; 01205 array_t *domainVarsBddArray; 01206 array_t *smoothSchedule, *smoothVars; 01207 float lambda; 01208 int size, total, lifetime; 01209 Img_DirectionType direction; 01210 int lambdaWithFrom, prevArea; 01211 array_t *orderedRelationArray; 01212 int nIntroducedVars; 01213 int *highest, *lowest; 01214 mdd_t *relation; 01215 int asIs; 01216 01217 if (cofactorCube && abstractCube) { 01218 newRelationArray = ImgGetCofactoredAbstractedRelationArray(info->manager, 01219 relationArray, cofactorCube, abstractCube); 01220 if (from && info->option->lambdaWithFrom) { 01221 if (preFlag) 01222 newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c); 01223 else 01224 newFrom = mdd_dup(from); 01225 array_insert_last(mdd_t *, newRelationArray, newFrom); 01226 lambdaWithFrom = 1; 01227 } else { 01228 lambdaWithFrom = 0; 01229 newFrom = NIL(mdd_t); 01230 } 01231 } else { 01232 if (from && info->option->lambdaWithFrom) { 01233 if (newRelationFlag) { 01234 newRelationArray = relationArray; 01235 if (preFlag) 01236 newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c); 01237 else 01238 newFrom = from; 01239 } else { 01240 /* We don't want to modify the original relation array */ 01241 newRelationArray = mdd_array_duplicate(relationArray); 01242 if (preFlag) 01243 newFrom = ImgSubstitute(from, info->functionData, Img_D2R_c); 01244 else 01245 newFrom = mdd_dup(from); 01246 } 01247 array_insert_last(mdd_t *, newRelationArray, newFrom); 01248 lambdaWithFrom = 1; 01249 } else { 01250 newRelationArray = relationArray; 01251 newFrom = NIL(mdd_t); 01252 lambdaWithFrom = 0; 01253 } 01254 } 01255 01256 if (vector) { 01257 for (i = 0; i < array_n(vector); i++) { 01258 comp = array_fetch(ImgComponent_t *, vector, i); 01259 array_insert_last(mdd_t *, newRelationArray, mdd_dup(comp->func)); 01260 } 01261 } 01262 01263 nVars = info->nVars; 01264 support = ALLOC(char, sizeof(char) * nVars); 01265 memset(support, 0, sizeof(char) * nVars); 01266 01267 comp = ImgComponentAlloc(info); 01268 for (i = 0; i < array_n(newRelationArray); i++) { 01269 comp->func = array_fetch(mdd_t *, newRelationArray, i);; 01270 ImgSupportClear(info, comp->support); 01271 ImgComponentGetSupport(comp); 01272 for (j = 0; j < nVars; j++) 01273 support[j] = support[j] | comp->support[j]; 01274 } 01275 comp->func = NIL(mdd_t); 01276 ImgComponentFree(comp); 01277 01278 nSupports = 0; 01279 smoothVarsBddArray = array_alloc(mdd_t *, 0); 01280 domainVarsBddArray = array_alloc(mdd_t *, 0); 01281 introducedVarsBddArray = array_alloc(mdd_t *, 0); 01282 for (i = 0; i < nVars; i++) { 01283 if (support[i]) { 01284 var = bdd_var_with_index(info->manager, i); 01285 if (preFlag) { 01286 if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) { 01287 if (lambdaWithFrom) 01288 array_insert_last(mdd_t *, smoothVarsBddArray, var); 01289 else 01290 array_insert_last(mdd_t *, domainVarsBddArray, var); 01291 if (info->option->preLambdaMode == 0 || 01292 info->option->preLambdaMode == 2) 01293 nSupports++; 01294 } else { 01295 if (info->preKeepPiInTr) { 01296 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, 01297 NIL(char *))) { 01298 array_insert_last(mdd_t *, introducedVarsBddArray, var); 01299 nSupports++; 01300 } else if (info->intermediateVarsTable && 01301 st_lookup(info->intermediateVarsTable, (char *)(long)i, 01302 NIL(char *))) { 01303 array_insert_last(mdd_t *, smoothVarsBddArray, var); 01304 nSupports++; 01305 } else { /* ps variables */ 01306 array_insert_last(mdd_t *, introducedVarsBddArray, var); 01307 if (info->option->preLambdaMode != 0) 01308 nSupports++; 01309 } 01310 } else { 01311 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, 01312 NIL(char *)) || 01313 (info->intermediateVarsTable && 01314 st_lookup(info->intermediateVarsTable, (char *)(long)i, 01315 NIL(char *)))) { 01316 array_insert_last(mdd_t *, smoothVarsBddArray, var); 01317 nSupports++; 01318 } else { /* ps variables */ 01319 array_insert_last(mdd_t *, introducedVarsBddArray, var); 01320 if (info->option->preLambdaMode != 0) 01321 nSupports++; 01322 } 01323 } 01324 } 01325 } else { /* image computation */ 01326 if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) { 01327 array_insert_last(mdd_t *, introducedVarsBddArray, var); 01328 if (info->option->lambdaMode == 2) 01329 nSupports++; 01330 } else { 01331 if (lambdaWithFrom) 01332 array_insert_last(mdd_t *, smoothVarsBddArray, var); 01333 else { 01334 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, 01335 NIL(char *)) || 01336 (info->intermediateVarsTable && 01337 st_lookup(info->intermediateVarsTable, (char *)(long)i, 01338 NIL(char *)))) { 01339 array_insert_last(mdd_t *, smoothVarsBddArray, var); 01340 } else 01341 array_insert_last(mdd_t *, domainVarsBddArray, var); 01342 } 01343 nSupports++; 01344 } 01345 } 01346 } 01347 } 01348 01349 if (preFlag) 01350 direction = Img_Backward_c; 01351 else 01352 direction = Img_Forward_c; 01353 01354 if (info->option->lambdaFromMlp) { 01355 FREE(support); 01356 if (info->option->lambdaWithClustering) { 01357 ImgMlpClusterRelationArray(info->manager, info->functionData, 01358 newRelationArray, domainVarsBddArray, 01359 smoothVarsBddArray, introducedVarsBddArray, 01360 direction, &clusteredRelationArray, NIL(array_t *), 01361 info->trmOption); 01362 if (newRelationArray != relationArray) 01363 mdd_array_free(newRelationArray); 01364 newRelationArray = clusteredRelationArray; 01365 } 01366 prevArea = info->prevTotal; 01367 asIs = newRelationFlag ? 0 : 1; /* 0 when relationArray is an array of 01368 functions, i.e. without next state 01369 variables */ 01370 lambda = ImgMlpComputeLambda(info->manager, newRelationArray, 01371 domainVarsBddArray, smoothVarsBddArray, 01372 introducedVarsBddArray, direction, 01373 info->option->lambdaMode, asIs, &prevArea, 01374 improvedLambda, info->trmOption); 01375 info->prevTotal = prevArea; 01376 } else { 01377 smoothSchedule = ImgGetQuantificationSchedule(info->manager, 01378 info->functionData, info->option->trMethod, 01379 direction, info->trmOption, newRelationArray, 01380 smoothVarsBddArray, domainVarsBddArray, 01381 introducedVarsBddArray, 01382 info->option->lambdaWithClustering, 01383 &orderedRelationArray); 01384 01385 if (direction == Img_Forward_c) { 01386 size = array_n(smoothSchedule); 01387 lifetime = 0; 01388 if (info->option->lambdaMode == 0) { /* total lifetime (lambda) */ 01389 for (i = 1; i < size; i++) { 01390 smoothVars = array_fetch(array_t *, smoothSchedule, i); 01391 lifetime += array_n(smoothVars) * i; 01392 } 01393 total = nSupports * (size - 1); 01394 } else if (info->option->lambdaMode == 1) { /* active lifetime (lambda) */ 01395 lowest = ALLOC(int, sizeof(int) * nVars); 01396 for (i = 0; i < nVars; i++) 01397 lowest[i] = nVars; 01398 highest = ALLOC(int, sizeof(int) * nVars); 01399 memset(highest, 0, sizeof(int) * nVars); 01400 01401 comp = ImgComponentAlloc(info); 01402 for (i = 0; i < size - 1; i++) { 01403 relation = array_fetch(mdd_t *, orderedRelationArray, i); 01404 comp->func = relation; 01405 ImgSupportClear(info, comp->support); 01406 ImgComponentGetSupport(comp); 01407 for (j = 0; j < nVars; j++) { 01408 if (!comp->support[j]) 01409 continue; 01410 if (st_lookup(info->rangeVarsTable, (char *)(long)j, NIL(char *))) 01411 continue; 01412 if (i < lowest[j]) 01413 lowest[j] = i; 01414 if (i > highest[j]) 01415 highest[j] = i; 01416 } 01417 } 01418 comp->func = NIL(mdd_t); 01419 ImgComponentFree(comp); 01420 01421 for (i = 0; i < nVars; i++) { 01422 if (lowest[i] == nVars) 01423 continue; 01424 if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) 01425 continue; 01426 lifetime += highest[i] - lowest[i] + 1; 01427 } 01428 01429 if (newRelationFlag) 01430 lifetime += array_n(newRelationArray); 01431 total = nSupports * (size - 1); 01432 01433 FREE(lowest); 01434 FREE(highest); 01435 } else { /* total lifetime (lambda) with introduced variables */ 01436 for (i = 1; i < size; i++) { 01437 smoothVars = array_fetch(array_t *, smoothSchedule, i); 01438 lifetime += array_n(smoothVars) * i; 01439 } 01440 01441 if (newRelationFlag) { 01442 nIntroducedVars = array_n(newRelationArray); 01443 lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2; 01444 } else { 01445 comp = ImgComponentAlloc(info); 01446 for (i = 0; i < size - 1; i++) { 01447 relation = array_fetch(mdd_t *, orderedRelationArray, i); 01448 comp->func = relation; 01449 ImgSupportClear(info, comp->support); 01450 ImgComponentGetSupport(comp); 01451 nIntroducedVars = 0; 01452 for (j = 0; j < nVars; j++) { 01453 if (!comp->support[j]) 01454 continue; 01455 if (st_lookup(info->rangeVarsTable, (char *)(long)j, NIL(char *))) 01456 nIntroducedVars++; 01457 } 01458 lifetime += (size - i - 1) * nIntroducedVars; 01459 } 01460 comp->func = NIL(mdd_t); 01461 ImgComponentFree(comp); 01462 } 01463 total = nSupports * (size - 1); 01464 } 01465 mdd_array_array_free(smoothSchedule); 01466 } else if (info->option->preLambdaMode == 0) { /* total lifetime (lambda) */ 01467 /* direction == Img_Backward_c */ 01468 size = array_n(smoothSchedule); 01469 lifetime = 0; 01470 for (i = 1; i < size; i++) { 01471 smoothVars = array_fetch(array_t *, smoothSchedule, i); 01472 lifetime += array_n(smoothVars) * i; 01473 } 01474 total = nSupports * (size - 1); 01475 mdd_array_array_free(smoothSchedule); 01476 } else { /* direction == Img_Backward_c */ 01477 size = array_n(smoothSchedule); 01478 mdd_array_array_free(smoothSchedule); 01479 lifetime = 0; 01480 01481 lowest = ALLOC(int, sizeof(int) * nVars); 01482 for (i = 0; i < nVars; i++) 01483 lowest[i] = nVars; 01484 highest = ALLOC(int, sizeof(int) * nVars); 01485 memset(highest, 0, sizeof(int) * nVars); 01486 01487 comp = ImgComponentAlloc(info); 01488 for (i = 0; i < size - 1; i++) { 01489 relation = array_fetch(mdd_t *, orderedRelationArray, i); 01490 comp->func = relation; 01491 ImgSupportClear(info, comp->support); 01492 ImgComponentGetSupport(comp); 01493 for (j = 0; j < nVars; j++) { 01494 if (!comp->support[j]) 01495 continue; 01496 if (i < lowest[j]) 01497 lowest[j] = i; 01498 if (i > highest[j]) 01499 highest[j] = i; 01500 } 01501 } 01502 comp->func = NIL(mdd_t); 01503 ImgComponentFree(comp); 01504 01505 if (info->option->preLambdaMode == 1) { /* active lifetime (lambda) */ 01506 for (i = 0; i < nVars; i++) { 01507 if (lowest[i] == nVars) 01508 continue; 01509 if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)) || 01510 st_lookup(info->quantifyVarsTable, (char *)(long)i, 01511 NIL(char *)) || 01512 (info->intermediateVarsTable && 01513 st_lookup(info->intermediateVarsTable, (char *)(long)i, 01514 NIL(char *)))) { 01515 lifetime += highest[i] - lowest[i] + 1; 01516 } 01517 } 01518 if (newRelationFlag) 01519 lifetime += array_n(newRelationArray); 01520 total = nSupports * (size - 1); 01521 } else if (info->option->preLambdaMode == 2) { 01522 /* total lifetime (lambda) with introduced variables */ 01523 for (i = 0; i < nVars; i++) { 01524 if (lowest[i] == nVars) 01525 continue; 01526 if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)) || 01527 st_lookup(info->quantifyVarsTable, (char *)(long)i, 01528 NIL(char *)) || 01529 (info->intermediateVarsTable && 01530 st_lookup(info->intermediateVarsTable, (char *)(long)i, 01531 NIL(char *)))) { 01532 lifetime += highest[i] + 1; 01533 } else { 01534 lifetime += size - lowest[i] - 1; 01535 } 01536 } 01537 if (newRelationFlag) { 01538 nIntroducedVars = array_n(newRelationArray); 01539 lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2; 01540 } 01541 total = nSupports * (size - 1); 01542 } else { /* total lifetime (lambda) with ps/pi variables */ 01543 for (i = 0; i < nVars; i++) { 01544 if (lowest[i] == nVars) 01545 continue; 01546 if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) 01547 continue; 01548 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, 01549 NIL(char *)) || 01550 (info->intermediateVarsTable && 01551 st_lookup(info->intermediateVarsTable, (char *)(long)i, 01552 NIL(char *)))) { 01553 lifetime += highest[i] + 1; 01554 } else { 01555 lifetime += size - lowest[i] - 1; 01556 } 01557 } 01558 if (newRelationFlag) { 01559 nIntroducedVars = array_n(newRelationArray); 01560 lifetime += nIntroducedVars * (nIntroducedVars + 1) / 2; 01561 } 01562 total = nSupports * (size - 1); 01563 } 01564 01565 FREE(lowest); 01566 FREE(highest); 01567 } 01568 01569 FREE(support); 01570 mdd_array_free(orderedRelationArray); 01571 01572 if (total == 0.0) { 01573 lambda = 0.0; 01574 *improvedLambda = 0.0; 01575 } else { 01576 lambda = (float)lifetime / (float)total; 01577 if (info->prevTotal) { 01578 *improvedLambda = info->prevLambda - 01579 (float)lifetime / (float)info->prevTotal; 01580 } else 01581 *improvedLambda = 0.0; 01582 } 01583 info->prevTotal = total; 01584 } 01585 01586 mdd_array_free(smoothVarsBddArray); 01587 mdd_array_free(domainVarsBddArray); 01588 mdd_array_free(introducedVarsBddArray); 01589 if (newRelationArray != relationArray) 01590 mdd_array_free(newRelationArray); 01591 if (newRelationFlag && from && info->option->lambdaWithFrom && 01592 newFrom != from) { 01593 mdd_free(newFrom); 01594 } 01595 01596 if (info->option->verbosity >= 2) { 01597 if (preFlag) 01598 fprintf(vis_stdout, "** tfm info: lambda for preimage = %.2f\n", lambda); 01599 else 01600 fprintf(vis_stdout, "** tfm info: lambda for image = %.2f\n", lambda); 01601 } 01602 01603 info->prevLambda = lambda; 01604 return(lambda); 01605 }
1.7.3