- Generated on Wed Oct 12 2011 00:34:49 for VIS by
1.7.3
|
VIS
|
00001 00075 #include "imgInt.h" 00076 00077 static char rcsid[] UNUSED = "$Id: imgTfm.c,v 1.93 2005/04/23 14:30:54 jinh Exp $"; 00078 00079 /*---------------------------------------------------------------------------*/ 00080 /* Constant declarations */ 00081 /*---------------------------------------------------------------------------*/ 00082 00083 /*---------------------------------------------------------------------------*/ 00084 /* Type declarations */ 00085 /*---------------------------------------------------------------------------*/ 00086 00087 /*---------------------------------------------------------------------------*/ 00088 /* Structure declarations */ 00089 /*---------------------------------------------------------------------------*/ 00090 00091 /*---------------------------------------------------------------------------*/ 00092 /* Variable declarations */ 00093 /*---------------------------------------------------------------------------*/ 00094 00095 static st_table *HookInfoList; /* adds a hook function to flush image 00096 cache before veriable reordering */ 00097 static int nHookInfoList; /* the number of hook functions */ 00098 00099 /*---------------------------------------------------------------------------*/ 00100 /* Macro declarations */ 00101 /*---------------------------------------------------------------------------*/ 00102 00103 00106 /*---------------------------------------------------------------------------*/ 00107 /* Static function prototypes */ 00108 /*---------------------------------------------------------------------------*/ 00109 00110 static ImgTfmInfo_t * TfmInfoStructAlloc(Img_MethodType method); 00111 static int CompareIndex(const void *e1, const void *e2); 00112 static int HookInfoFunction(bdd_manager *mgr, char *str, void *method); 00113 static array_t * ChoosePartialVars(ImgTfmInfo_t *info, array_t *vector, int nPartialVars, int partialMethod); 00114 static void PrintRecursionStatistics(ImgTfmInfo_t *info, int preFlag); 00115 static void PrintFoundVariableStatistics(ImgTfmInfo_t *info, int preFlag); 00116 static void GetRecursionStatistics(ImgTfmInfo_t *info, int preFlag, int *nRecurs, int *nLeaves, int *nTurns, float *averageDepth, int *maxDepth, int *nDecomps, int *topDecomp, int *maxDecomp, float *averageDecomp); 00117 static int ReadSetIntValue(char *string, int l, int u, int defaultValue); 00118 static boolean ReadSetBooleanValue(char *string, boolean defaultValue); 00119 static void FindIntermediateVarsRecursively(ImgTfmInfo_t *info, mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *vector, st_table *domainQuantifyVarMddIdTable, array_t *intermediateVarMddIdArray); 00120 static void GetIntermediateRelationsRecursively(mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *relationArray, st_table *domainQuantifyVarMddIdTable, array_t *intermediateVarMddIdArray); 00121 static int CheckNondeterminism(Ntk_Network_t *network); 00122 static array_t * TfmCreateBitVector(ImgTfmInfo_t *info, int composeIntermediateVars, int findIntermediateVars); 00123 static array_t * TfmCreateBitRelationArray(ImgTfmInfo_t *info, int composeIntermediateVars, int findIntermediateVars); 00124 static void TfmSetupPartialTransitionRelation(ImgTfmInfo_t *info, array_t **partialRelationArray); 00125 static void TfmBuildRelationArray(ImgTfmInfo_t *info, ImgFunctionData_t *functionData, array_t *bitRelationArray, Img_DirectionType directionType, int writeMatrix); 00126 static void RebuildTransitionRelation(ImgTfmInfo_t *info, Img_DirectionType directionType); 00127 static void MinimizeTransitionFunction(array_t *vector, array_t *relationArray, mdd_t *constrain, Img_MinimizeType minimizeMethod, int printStatus); 00128 static void AddDontCareToTransitionFunction(array_t *vector, array_t *relationArray, mdd_t *constrain, Img_MinimizeType minimizeMethod, int printStatus); 00129 00133 /*---------------------------------------------------------------------------*/ 00134 /* Definition of exported functions */ 00135 /*---------------------------------------------------------------------------*/ 00136 00137 00151 int 00152 Img_TfmGetRecursionStatistics(Img_ImageInfo_t *imageInfo, int preFlag, 00153 int *nRecurs, int *nLeaves, int *nTurns, 00154 float *averageDepth, int *maxDepth, int *nDecomps, 00155 int *topDecomp, int *maxDecomp, 00156 float *averageDecomp) 00157 { 00158 ImgTfmInfo_t *info; 00159 00160 if (imageInfo->methodType != Img_Tfm_c && 00161 imageInfo->methodType != Img_Hybrid_c) { 00162 return(0); 00163 } 00164 00165 info = (ImgTfmInfo_t *)imageInfo->methodData; 00166 if (preFlag) { 00167 *nRecurs = info->nRecursionB; 00168 *nLeaves = info->nLeavesB; 00169 *nTurns = info->nTurnsB; 00170 *averageDepth = info->averageDepthB; 00171 *maxDepth = info->maxDepthB; 00172 *nDecomps = 0; 00173 *topDecomp = 0; 00174 *maxDecomp = 0; 00175 *averageDecomp = 0.0; 00176 } else { 00177 *nRecurs = info->nRecursion; 00178 *nLeaves = info->nLeaves; 00179 *nTurns = info->nTurns; 00180 *averageDepth = info->averageDepth; 00181 *maxDepth = info->maxDepth; 00182 *nDecomps = info->nDecomps; 00183 *topDecomp = info->topDecomp; 00184 *maxDecomp = info->maxDecomp; 00185 *averageDecomp = info->averageDecomp; 00186 } 00187 return(1); 00188 } 00189 00190 00204 void 00205 Img_TfmPrintStatistics(Img_ImageInfo_t *imageInfo, Img_DirectionType dir) 00206 { 00207 if (dir == Img_Forward_c || dir == Img_Both_c) { 00208 Img_TfmPrintCacheStatistics(imageInfo, 0); 00209 Img_TfmPrintRecursionStatistics(imageInfo, 0); 00210 } 00211 if (dir == Img_Backward_c || dir == Img_Both_c) { 00212 Img_TfmPrintCacheStatistics(imageInfo, 1); 00213 Img_TfmPrintRecursionStatistics(imageInfo, 1); 00214 } 00215 } 00216 00217 00231 void 00232 Img_TfmPrintRecursionStatistics(Img_ImageInfo_t *imageInfo, int preFlag) 00233 { 00234 float avgDepth, avgDecomp; 00235 int nRecurs, nLeaves, nTurns, nDecomps, topDecomp, maxDecomp; 00236 int maxDepth; 00237 00238 (void) Img_TfmGetRecursionStatistics(imageInfo, preFlag, &nRecurs, &nLeaves, 00239 &nTurns, &avgDepth, &maxDepth, &nDecomps, 00240 &topDecomp, &maxDecomp, &avgDecomp); 00241 if (preFlag) 00242 fprintf(vis_stdout, "** recursion statistics of splitting (preImg) **\n"); 00243 else 00244 fprintf(vis_stdout, "** recursion statistics of splitting (img) **\n"); 00245 fprintf(vis_stdout, "# recursions = %d\n", nRecurs); 00246 fprintf(vis_stdout, "# leaves = %d\n", nLeaves); 00247 fprintf(vis_stdout, "# turns = %d\n", nTurns); 00248 fprintf(vis_stdout, "# average recursion depth = %g (max = %d)\n", 00249 avgDepth, maxDepth); 00250 if (!preFlag) { 00251 fprintf(vis_stdout, 00252 "# decompositions = %d (top = %d, max = %d, average = %g)\n", 00253 nDecomps, topDecomp, maxDecomp, avgDecomp); 00254 } 00255 } 00256 00257 00271 void 00272 Img_PrintTfmOptions(void) 00273 { 00274 ImgTfmOption_t *options; 00275 Img_MethodType method; 00276 char *flagValue, dummy[40]; 00277 00278 flagValue = Cmd_FlagReadByName("image_method"); 00279 if (flagValue) { 00280 if (strcmp(flagValue, "hybrid") == 0) 00281 method = Img_Hybrid_c; 00282 else 00283 method = Img_Tfm_c; 00284 } else 00285 method = Img_Tfm_c; 00286 00287 options = ImgTfmGetOptions(method); 00288 00289 switch (options->splitMethod) { 00290 case 0 : 00291 sprintf(dummy, "input split"); 00292 break; 00293 case 1 : 00294 sprintf(dummy, "output split"); 00295 break; 00296 case 2 : 00297 sprintf(dummy, "mixed"); 00298 break; 00299 case 3 : 00300 sprintf(dummy, "hybrid"); 00301 break; 00302 default : 00303 sprintf(dummy, "invalid"); 00304 break; 00305 } 00306 fprintf(vis_stdout, "TFM: tfm_split_method = %d (%s)\n", 00307 options->splitMethod, dummy); 00308 00309 switch (options->inputSplit) { 00310 case 0 : 00311 sprintf(dummy, "support before splitting"); 00312 break; 00313 case 1 : 00314 sprintf(dummy, "support after splitting"); 00315 break; 00316 case 2 : 00317 sprintf(dummy, "estimate BDD size after splitting"); 00318 break; 00319 case 3 : 00320 sprintf(dummy, "top variable"); 00321 break; 00322 default : 00323 sprintf(dummy, "invalid"); 00324 break; 00325 } 00326 fprintf(vis_stdout, "TFM: tfm_input_split = %d (%s)\n", 00327 options->inputSplit, dummy); 00328 00329 if (options->piSplitFlag) 00330 sprintf(dummy, "yes"); 00331 else 00332 sprintf(dummy, "no"); 00333 fprintf(vis_stdout, "TFM: tfm_pi_split_flag = %s\n", dummy); 00334 00335 /* whether to convert image computation to range computation */ 00336 switch (options->rangeComp) { 00337 case 0 : 00338 sprintf(dummy, "do not convert"); 00339 break; 00340 case 1 : 00341 sprintf(dummy, "convert to range computation"); 00342 break; 00343 case 2 : 00344 sprintf(dummy, "convert with threshold"); 00345 break; 00346 default : 00347 sprintf(dummy, "invalid"); 00348 break; 00349 } 00350 fprintf(vis_stdout, "TFM: tfm_range_comp = %d (%s)\n", 00351 options->rangeComp, dummy); 00352 00353 fprintf(vis_stdout, "TFM: tfm_range_threshold = %d\n", 00354 options->rangeThreshold); 00355 00356 fprintf(vis_stdout, "TFM: tfm_range_try_threshold = %d\n", 00357 options->rangeTryThreshold); 00358 00359 if (options->rangeCheckReorder) 00360 sprintf(dummy, "yes"); 00361 else 00362 sprintf(dummy, "no"); 00363 fprintf(vis_stdout, "TFM: tfm_range_check_reorder = %s\n", dummy); 00364 00365 switch (options->tieBreakMode) { 00366 case 0 : 00367 sprintf(dummy, "closest variable to top"); 00368 break; 00369 case 1 : 00370 sprintf(dummy, "smallest BDD size after splitting"); 00371 break; 00372 default : 00373 sprintf(dummy, "invalid"); 00374 break; 00375 } 00376 fprintf(vis_stdout, "TFM: tfm_tie_break_mode = %d (%s)\n", 00377 options->tieBreakMode, dummy); 00378 00379 switch (options->outputSplit) { 00380 case 0 : 00381 sprintf(dummy, "smallest BDD size"); 00382 break; 00383 case 1 : 00384 sprintf(dummy, "largest BDD size"); 00385 break; 00386 case 2 : 00387 sprintf(dummy, "top variable"); 00388 break; 00389 default : 00390 sprintf(dummy, "invalid"); 00391 break; 00392 } 00393 fprintf(vis_stdout, "TFM: tfm_output_split = %d (%s)\n", 00394 options->outputSplit, dummy); 00395 00396 fprintf(vis_stdout, "TFM: tfm_turn_depth = %d\n", 00397 options->turnDepth); 00398 00399 if (options->findDecompVar) 00400 sprintf(dummy, "yes"); 00401 else 00402 sprintf(dummy, "no"); 00403 fprintf(vis_stdout, "TFM: tfm_find_decomp_var = %s\n", dummy); 00404 00405 if (options->sortVectorFlag) 00406 sprintf(dummy, "yes"); 00407 else 00408 sprintf(dummy, "no"); 00409 fprintf(vis_stdout, "TFM: tfm_sort_vector_flag = %s\n", dummy); 00410 00411 if (options->printStatistics) 00412 sprintf(dummy, "yes"); 00413 else 00414 sprintf(dummy, "no"); 00415 fprintf(vis_stdout, "TFM: tfm_print_stats = %s\n", dummy); 00416 00417 if (options->printBddSize) 00418 sprintf(dummy, "yes"); 00419 else 00420 sprintf(dummy, "no"); 00421 fprintf(vis_stdout, "TFM: tfm_print_bdd_size = %s\n", dummy); 00422 00423 if (options->splitCubeFunc) 00424 sprintf(dummy, "yes"); 00425 else 00426 sprintf(dummy, "no"); 00427 fprintf(vis_stdout, "TFM: tfm_split_cube_func = %s\n", dummy); 00428 00429 switch (options->findEssential) { 00430 case 0 : 00431 sprintf(dummy, "off"); 00432 break; 00433 case 1 : 00434 sprintf(dummy, "on"); 00435 break; 00436 case 2 : 00437 sprintf(dummy, "dynamic"); 00438 break; 00439 default : 00440 sprintf(dummy, "invalid"); 00441 break; 00442 } 00443 fprintf(vis_stdout, "TFM: tfm_find_essential = %d (%s)\n", 00444 options->findEssential, dummy); 00445 00446 switch (options->printEssential) { 00447 case 0 : 00448 sprintf(dummy, "off"); 00449 break; 00450 case 1 : 00451 sprintf(dummy, "at the end"); 00452 break; 00453 case 2 : 00454 sprintf(dummy, "at every image computation"); 00455 break; 00456 default : 00457 sprintf(dummy, "invalid"); 00458 break; 00459 } 00460 fprintf(vis_stdout, "TFM: tfm_print_essential = %d (%s)\n", 00461 options->printEssential, dummy); 00462 00463 switch (options->useCache) { 00464 case 0 : 00465 sprintf(dummy, "off"); 00466 break; 00467 case 1 : 00468 sprintf(dummy, "on"); 00469 break; 00470 case 2 : 00471 sprintf(dummy, "store all intermediate"); 00472 break; 00473 default : 00474 sprintf(dummy, "invalid"); 00475 break; 00476 } 00477 fprintf(vis_stdout, "TFM: tfm_use_cache = %d (%s)\n", 00478 options->useCache, dummy); 00479 00480 if (options->globalCache) 00481 sprintf(dummy, "yes"); 00482 else 00483 sprintf(dummy, "no"); 00484 fprintf(vis_stdout, "TFM: tfm_global_cache = %s\n", dummy); 00485 00486 fprintf(vis_stdout, "TFM: tfm_max_chain_length = %d\n", 00487 options->maxChainLength); 00488 00489 fprintf(vis_stdout, "TFM: tfm_init_cache_size = %d\n", 00490 options->initCacheSize); 00491 00492 switch (options->autoFlushCache) { 00493 case 0 : 00494 sprintf(dummy, "when requested"); 00495 break; 00496 case 1 : 00497 sprintf(dummy, "at the end of image computation"); 00498 break; 00499 case 2 : 00500 sprintf(dummy, "before reordering"); 00501 break; 00502 default : 00503 sprintf(dummy, "invalid"); 00504 break; 00505 } 00506 fprintf(vis_stdout, "TFM: tfm_auto_flush_cache = %d (%s)\n", 00507 options->autoFlushCache, dummy); 00508 00509 if (options->composeIntermediateVars) 00510 sprintf(dummy, "yes"); 00511 else 00512 sprintf(dummy, "no"); 00513 fprintf(vis_stdout, "TFM: tfm_compose_intermediate_vars = %s\n", dummy); 00514 00515 switch (options->preSplitMethod) { 00516 case 0 : 00517 sprintf(dummy, "input split"); 00518 break; 00519 case 1 : 00520 sprintf(dummy, "output split"); 00521 break; 00522 case 2 : 00523 sprintf(dummy, "mixed"); 00524 break; 00525 case 3 : 00526 sprintf(dummy, "substitution"); 00527 break; 00528 case 4 : 00529 sprintf(dummy, "hybrid"); 00530 break; 00531 default : 00532 sprintf(dummy, "invalid"); 00533 break; 00534 } 00535 fprintf(vis_stdout, "TFM: tfm_pre_split_method = %d (%s)\n", 00536 options->preSplitMethod, dummy); 00537 00538 switch (options->preInputSplit) { 00539 case 0 : 00540 sprintf(dummy, "support before splitting"); 00541 break; 00542 case 1 : 00543 sprintf(dummy, "support after splitting"); 00544 break; 00545 case 2 : 00546 sprintf(dummy, "estimate BDD size after splitting"); 00547 break; 00548 case 3 : 00549 sprintf(dummy, "top variable"); 00550 break; 00551 default : 00552 sprintf(dummy, "invalid"); 00553 break; 00554 } 00555 fprintf(vis_stdout, "TFM: tfm_pre_input_split = %d (%s)\n", 00556 options->preInputSplit, dummy); 00557 00558 switch (options->preOutputSplit) { 00559 case 0 : 00560 sprintf(dummy, "smallest BDD size"); 00561 break; 00562 case 1 : 00563 sprintf(dummy, "largest BDD size"); 00564 break; 00565 case 2 : 00566 sprintf(dummy, "top variable"); 00567 break; 00568 default : 00569 sprintf(dummy, "invalid"); 00570 break; 00571 } 00572 fprintf(vis_stdout, "TFM: tfm_pre_output_split = %d (%s)\n", 00573 options->preOutputSplit, dummy); 00574 00575 switch (options->preDcLeafMethod) { 00576 case 0 : 00577 sprintf(dummy, "substitution"); 00578 break; 00579 case 1 : 00580 sprintf(dummy, "constraint cofactoring"); 00581 break; 00582 case 2 : 00583 sprintf(dummy, "hybrid"); 00584 break; 00585 default : 00586 sprintf(dummy, "invalid"); 00587 break; 00588 } 00589 fprintf(vis_stdout, "TFM: tfm_pre_dc_leaf_method = %d (%s)\n", 00590 options->preDcLeafMethod, dummy); 00591 00592 if (options->preMinimize) 00593 sprintf(dummy, "yes"); 00594 else 00595 sprintf(dummy, "no"); 00596 fprintf(vis_stdout, "TFM: tfm_pre_minimize = %s\n", dummy); 00597 00598 fprintf(vis_stdout, "TFM: tfm_verbosity = %d\n", 00599 options->verbosity); 00600 00601 FREE(options); 00602 } 00603 00604 00605 /*---------------------------------------------------------------------------*/ 00606 /* Definition of internal functions */ 00607 /*---------------------------------------------------------------------------*/ 00608 00609 00621 void * 00622 ImgImageInfoInitializeTfm(void *methodData, ImgFunctionData_t * functionData, 00623 Img_DirectionType directionType, 00624 Img_MethodType method) 00625 { 00626 int i; 00627 int latches; 00628 int variables, nVars; 00629 array_t *vector; 00630 graph_t *mddNetwork; 00631 mdd_manager *mddManager; 00632 array_t *rangeVarMddIdArray; 00633 ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; 00634 int index; 00635 mdd_t *var; 00636 char *flagValue; 00637 char filename[20]; 00638 int composeIntermediateVars, findIntermediateVars; 00639 int nonDeterministic; 00640 00641 if (info) { 00642 if (info->option->useCache) { 00643 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 00644 if (!info->imgCache) 00645 ImgCacheInitTable(info, info->option->initCacheSize, 00646 info->option->globalCache, FALSE); 00647 } 00648 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 00649 if (!info->preCache) 00650 ImgCacheInitTable(info, info->option->initCacheSize, 00651 info->option->globalCache, TRUE); 00652 } 00653 } 00654 if (info->buildTR && 00655 (((directionType == Img_Forward_c || directionType == Img_Both_c) && 00656 !info->fwdClusteredRelationArray) || 00657 ((directionType == Img_Backward_c || directionType == Img_Both_c) && 00658 !info->bwdClusteredRelationArray))) { 00659 TfmBuildRelationArray(info, functionData, NIL(array_t), directionType, 0); 00660 } 00661 return((void *)info); 00662 } 00663 00664 mddNetwork = functionData->mddNetwork; 00665 mddManager = Part_PartitionReadMddManager(mddNetwork); 00666 rangeVarMddIdArray = functionData->rangeVars; 00667 00668 nonDeterministic = CheckNondeterminism(functionData->network); 00669 if (nonDeterministic) 00670 info = TfmInfoStructAlloc(Img_Hybrid_c); 00671 else 00672 info = TfmInfoStructAlloc(method); 00673 info->nonDeterministic = nonDeterministic; 00674 info->functionData = functionData; 00675 info->quantifyVarsTable = st_init_table(st_numcmp, st_numhash); 00676 for (i = 0; i < array_n(functionData->quantifyBddVars); i++) { 00677 var = array_fetch(mdd_t *, functionData->quantifyBddVars, i); 00678 index = (int)bdd_top_var_id(var); 00679 st_insert(info->quantifyVarsTable, (char *)(long)index, NIL(char)); 00680 } 00681 info->rangeVarsTable = st_init_table(st_numcmp, st_numhash); 00682 for (i = 0; i < array_n(functionData->rangeBddVars); i++) { 00683 var = array_fetch(mdd_t *, functionData->rangeBddVars, i); 00684 index = (int)bdd_top_var_id(var); 00685 st_insert(info->rangeVarsTable, (char *)(long)index, NIL(char)); 00686 } 00687 00688 latches = 2 * mdd_get_number_of_bdd_vars(mddManager, rangeVarMddIdArray); 00689 nVars = latches + mdd_get_number_of_bdd_vars(mddManager, 00690 functionData->quantifyVars); 00691 variables = bdd_num_vars(mddManager); /* real number of variables */ 00692 info->nRealVars = nVars; 00693 info->nVars = variables; 00694 00695 if (info->nonDeterministic) { 00696 if (method == Img_Tfm_c) { 00697 fprintf(vis_stdout, 00698 "** tfm warning: The circuit may have nondeterminism.\n"); 00699 fprintf(vis_stdout, "\tautomatically switched to hybrid mode = 2.\n"); 00700 info->method = Img_Hybrid_c; 00701 } else { 00702 if (info->option->hybridMode == 2) { 00703 if (info->option->buildPartialTR) { 00704 fprintf(vis_stdout, 00705 "** hyb warning: The circuit may have nondeterminism.\n"); 00706 fprintf(vis_stdout, 00707 "\tdid not use partial transition relation.\n"); 00708 } else { 00709 fprintf(vis_stdout, 00710 "** hyb info: The circuit may have nondeterminism.\n"); 00711 } 00712 } else { 00713 fprintf(vis_stdout, 00714 "** hyb warning: The circuit may have nondeterminism.\n"); 00715 fprintf(vis_stdout, "\tautomatically switched to hybrid mode = 2.\n"); 00716 } 00717 } 00718 } 00719 if (info->nonDeterministic || 00720 (info->option->hybridMode > 0 && 00721 (info->option->splitMethod == 3 || info->option->preSplitMethod == 4))) { 00722 if (info->option->hybridMode == 2 || info->nonDeterministic) 00723 info->buildTR = 2; 00724 else 00725 info->buildTR = 1; 00726 } 00727 if (info->buildTR == 2 && 00728 info->option->buildPartialTR && 00729 info->nonDeterministic == 0 && 00730 info->option->useCache == 0) { 00731 info->buildPartialTR = TRUE; 00732 } 00733 00734 info->imgKeepPiInTr = info->option->imgKeepPiInTr; 00735 if (info->option->useCache) 00736 info->preKeepPiInTr = TRUE; 00737 else 00738 info->preKeepPiInTr = info->option->preKeepPiInTr; 00739 00740 if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c && 00741 nVars != variables) { 00742 if (info->option->composeIntermediateVars) { 00743 composeIntermediateVars = 1; 00744 findIntermediateVars = 0; 00745 } else { 00746 composeIntermediateVars = 0; 00747 findIntermediateVars = 1; 00748 } 00749 } else { 00750 composeIntermediateVars = 0; 00751 findIntermediateVars = 0; 00752 } 00753 00754 if (info->buildTR != 2 || info->buildPartialTR) { /* deterministic */ 00755 vector = TfmCreateBitVector(info, composeIntermediateVars, 00756 findIntermediateVars); 00757 } else 00758 vector = NIL(array_t); 00759 00760 info->manager = mddManager; 00761 if (info->buildPartialTR) 00762 info->fullVector = vector; 00763 else 00764 info->vector = vector; 00765 if (info->buildTR == 2) 00766 info->useConstraint = 1; 00767 else if (info->option->splitMethod == 1) 00768 info->useConstraint = 0; 00769 else { 00770 if (info->option->rangeComp == 2) 00771 info->useConstraint = 2; 00772 else if (info->option->rangeComp == 0) 00773 info->useConstraint = 1; 00774 else 00775 info->useConstraint = 0; 00776 } 00777 if (info->option->useCache) { 00778 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 00779 ImgCacheInitTable(info, info->option->initCacheSize, 00780 info->option->globalCache, FALSE); 00781 } 00782 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 00783 ImgCacheInitTable(info, info->option->initCacheSize, 00784 info->option->globalCache, TRUE); 00785 } 00786 if (info->option->autoFlushCache == 2) { 00787 if (nHookInfoList == 0) { 00788 HookInfoList = st_init_table(st_ptrcmp, st_ptrhash); 00789 bdd_add_hook(info->manager, HookInfoFunction, BDD_PRE_REORDERING_HOOK); 00790 st_insert(HookInfoList, (char *)info, NIL(char)); 00791 } else { 00792 if (info->option->globalCache == 0) 00793 st_insert(HookInfoList, (char *)info, NIL(char)); 00794 } 00795 nHookInfoList++; 00796 } 00797 } 00798 00799 info->trmOption = ImgGetTrmOptions(); 00800 info->domainVarBddArray = functionData->domainBddVars; 00801 info->quantifyVarBddArray = functionData->quantifyBddVars; 00802 info->rangeVarBddArray = functionData->rangeBddVars; 00803 00804 if (info->vector && info->option->sortVectorFlag && info->option->useCache) 00805 array_sort(info->vector, CompareIndex); 00806 if (info->buildPartialTR) 00807 TfmSetupPartialTransitionRelation(info, NIL(array_t *)); 00808 if (info->buildTR) 00809 TfmBuildRelationArray(info, functionData, NIL(array_t), directionType, 1); 00810 if (info->buildTR == 1) { 00811 ImgPrintVectorDependency(info, info->vector, info->option->verbosity); 00812 if (info->option->writeSupportMatrix == 1) { 00813 sprintf(filename, "support%d.mat", info->option->supportFileCount++); 00814 ImgWriteSupportMatrix(info, info->vector, NIL(array_t), filename); 00815 } 00816 } 00817 if (info->option->writeSupportMatrixAndStop) 00818 exit(0); 00819 00820 flagValue = Cmd_FlagReadByName("image_eliminate_depend_vars"); 00821 if (flagValue == NIL(char)) 00822 info->eliminateDepend = 0; /* the default value */ 00823 else 00824 info->eliminateDepend = atoi(flagValue); 00825 if (info->eliminateDepend && bdd_get_package_name() != CUDD) { 00826 fprintf(vis_stderr, 00827 "** tfm error : image_eliminate_depend_vars is available for only CUDD.\n"); 00828 info->eliminateDepend = 0; 00829 } 00830 info->nPrevEliminatedFwd = -1; 00831 00832 flagValue = Cmd_FlagReadByName("image_verbosity"); 00833 if (flagValue) 00834 info->imageVerbosity = atoi(flagValue); 00835 00836 if (info->option->printEssential) { 00837 info->foundEssentials = ALLOC(int, IMG_TF_MAX_PRINT_DEPTH); 00838 memset(info->foundEssentials, 0, sizeof(int) * IMG_TF_MAX_PRINT_DEPTH); 00839 } 00840 if (info->option->debug) 00841 info->debugCareSet = bdd_one(mddManager); 00842 else 00843 info->debugCareSet = NIL(mdd_t); 00844 return((void *)info); 00845 } 00846 00847 00859 mdd_t * 00860 ImgImageInfoComputeFwdTfm(ImgFunctionData_t *functionData, 00861 Img_ImageInfo_t *imageInfo, 00862 mdd_t *fromLowerBound, 00863 mdd_t *fromUpperBound, 00864 array_t *toCareSetArray) 00865 { 00866 ImgTfmInfo_t *info = (ImgTfmInfo_t *)imageInfo->methodData; 00867 mdd_t *image, *domainSubset; 00868 00869 if (info->vector == NIL(array_t) && 00870 !(info->buildTR == 2 && info->fwdClusteredRelationArray)) { 00871 fprintf(vis_stderr, "** img error: The data structure has not been "); 00872 fprintf(vis_stderr, "initialized for image computation\n"); 00873 return(NIL(mdd_t)); 00874 } 00875 00876 info->updatedFlag = FALSE; 00877 domainSubset = bdd_between(fromLowerBound, fromUpperBound); 00878 00879 image = ImgTfmImage(info, domainSubset); 00880 00881 mdd_free(domainSubset); 00882 return(image); 00883 } 00884 00885 00898 mdd_t * 00899 ImgImageInfoComputeFwdWithDomainVarsTfm(ImgFunctionData_t *functionData, 00900 Img_ImageInfo_t *imageInfo, 00901 mdd_t *fromLowerBound, 00902 mdd_t *fromUpperBound, 00903 array_t *toCareSetArray) 00904 { 00905 mdd_t *image; 00906 00907 image = ImgImageInfoComputeFwdTfm(functionData, 00908 imageInfo , fromLowerBound, fromUpperBound, toCareSetArray); 00909 return(image); 00910 } 00911 00912 00924 mdd_t * 00925 ImgImageInfoComputeBwdTfm(ImgFunctionData_t *functionData, 00926 Img_ImageInfo_t *imageInfo, 00927 mdd_t *fromLowerBound, 00928 mdd_t *fromUpperBound, 00929 array_t *toCareSetArray) 00930 { 00931 ImgTfmInfo_t *info = (ImgTfmInfo_t *)imageInfo->methodData; 00932 mdd_t *image, *domainSubset, *simplifiedImage; 00933 array_t *replace; 00934 00935 if (info->vector == NIL(array_t) && 00936 !(info->buildTR == 2 && info->bwdClusteredRelationArray)) { 00937 fprintf(vis_stderr, "** img error: The data structure has not been "); 00938 fprintf(vis_stderr, "initialized for backward image computation\n"); 00939 return(NIL(mdd_t)); 00940 } 00941 00942 info->updatedFlag = FALSE; 00943 domainSubset = bdd_between(fromLowerBound, fromUpperBound); 00944 00945 if (info->toCareSetArray) 00946 replace = info->toCareSetArray; 00947 else { 00948 replace = NIL(array_t); 00949 info->toCareSetArray = toCareSetArray; 00950 } 00951 image = ImgTfmPreImage(info, domainSubset); 00952 info->toCareSetArray = replace; 00953 00954 mdd_free(domainSubset); 00955 simplifiedImage = bdd_minimize_array(image, toCareSetArray); 00956 bdd_free(image); 00957 return(simplifiedImage); 00958 } 00959 00960 00972 mdd_t * 00973 ImgImageInfoComputeBwdWithDomainVarsTfm(ImgFunctionData_t *functionData, 00974 Img_ImageInfo_t *imageInfo, 00975 mdd_t *fromLowerBound, 00976 mdd_t *fromUpperBound, 00977 array_t *toCareSetArray) 00978 { 00979 mdd_t *image; 00980 00981 image = ImgImageInfoComputeBwdTfm(functionData, 00982 imageInfo, fromLowerBound, fromUpperBound, toCareSetArray); 00983 return(image); 00984 } 00985 00986 00996 void 00997 ImgImageInfoFreeTfm(void *methodData) 00998 { 00999 ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; 01000 01001 if (info == NIL(ImgTfmInfo_t)) { 01002 fprintf(vis_stderr, "** img error: Trying to free the NULL image info\n"); 01003 return; 01004 } 01005 if (info->option->printStatistics) { 01006 if (info->nRecursion) { 01007 if (info->imgCache) 01008 ImgPrintCacheStatistics(info->imgCache); 01009 PrintRecursionStatistics(info, 0); 01010 PrintFoundVariableStatistics(info, 0); 01011 } 01012 if (info->nRecursionB) { 01013 if (info->preCache) 01014 ImgPrintCacheStatistics(info->preCache); 01015 PrintRecursionStatistics(info, 1); 01016 PrintFoundVariableStatistics(info, 1); 01017 } 01018 } 01019 if (info->vector != NIL(array_t)) 01020 ImgVectorFree(info->vector); 01021 if (info->toCareSetArray != NIL(array_t)) 01022 mdd_array_free(info->toCareSetArray); 01023 if (info->imgCache) 01024 ImgCacheDestroyTable(info->imgCache, info->option->globalCache); 01025 if (info->preCache) 01026 ImgCacheDestroyTable(info->preCache, info->option->globalCache); 01027 st_free_table(info->quantifyVarsTable); 01028 st_free_table(info->rangeVarsTable); 01029 if (info->intermediateVarsTable) { 01030 st_free_table(info->intermediateVarsTable); 01031 info->intermediateVarsTable = NIL(st_table); 01032 } 01033 if (info->intermediateBddVars) { 01034 mdd_array_free(info->intermediateBddVars); 01035 info->intermediateBddVars= NIL(array_t); 01036 } 01037 if (info->newQuantifyBddVars) { 01038 mdd_array_free(info->newQuantifyBddVars); 01039 info->newQuantifyBddVars = NIL(array_t); 01040 } 01041 01042 if (info->option->useCache) { 01043 if (info->option->autoFlushCache == 2) { 01044 nHookInfoList--; 01045 st_delete(HookInfoList, &info, NULL); 01046 if (nHookInfoList == 0) { 01047 st_free_table(HookInfoList); 01048 bdd_remove_hook(info->manager, HookInfoFunction, 01049 BDD_PRE_REORDERING_HOOK); 01050 } 01051 } 01052 } 01053 if (info->option != NULL) 01054 FREE(info->option); 01055 01056 if (info->fwdClusteredRelationArray) 01057 mdd_array_free(info->fwdClusteredRelationArray); 01058 if (info->bwdClusteredRelationArray) 01059 mdd_array_free(info->bwdClusteredRelationArray); 01060 if (info->fwdArraySmoothVarBddArray) 01061 mdd_array_array_free(info->fwdArraySmoothVarBddArray); 01062 if (info->bwdArraySmoothVarBddArray) 01063 mdd_array_array_free(info->bwdArraySmoothVarBddArray); 01064 if (info->fwdSmoothVarCubeArray) 01065 mdd_array_free(info->fwdSmoothVarCubeArray); 01066 if (info->bwdSmoothVarCubeArray) 01067 mdd_array_free(info->bwdSmoothVarCubeArray); 01068 if (info->trmOption) 01069 ImgFreeTrmOptions(info->trmOption); 01070 if (info->partialBddVars) 01071 mdd_array_free(info->partialBddVars); 01072 if (info->partialVarFlag) 01073 FREE(info->partialVarFlag); 01074 if (info->fullVector != NIL(array_t)) 01075 ImgVectorFree(info->fullVector); 01076 01077 if (info->foundEssentials) 01078 FREE(info->foundEssentials); 01079 if (info->debugCareSet) 01080 mdd_free(info->debugCareSet); 01081 01082 if (info->savedArraySmoothVarBddArray != NIL(array_t)) 01083 mdd_array_array_free(info->savedArraySmoothVarBddArray); 01084 if (info->savedSmoothVarCubeArray != NIL(array_t)) 01085 mdd_array_free(info->savedSmoothVarCubeArray); 01086 FREE(info); 01087 } 01088 01089 01100 void 01101 ImgImageInfoPrintMethodParamsTfm(void *methodData, FILE *fp) 01102 { 01103 ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; 01104 01105 if (fp == NULL) 01106 return; 01107 if (info->vector) 01108 ImgPrintVectorDependency(info, info->vector, 1); 01109 if (info->method == Img_Tfm_c) { 01110 fprintf(vis_stdout, 01111 "For the options in tfm method, try print_tfm_options.\n"); 01112 return; 01113 } 01114 if (info->fwdClusteredRelationArray != NIL(array_t)) { 01115 fprintf(fp, "Shared size of transition relation for forward image"); 01116 fprintf(fp, " computation is %10ld BDD nodes (%-4d components)\n", 01117 bdd_size_multiple(info->fwdClusteredRelationArray), 01118 array_n(info->fwdClusteredRelationArray)); 01119 } 01120 if (info->bwdClusteredRelationArray != NIL(array_t)) { 01121 fprintf(fp, "Shared size of transition relation for backward image"); 01122 fprintf(fp, " computation is %10ld BDD nodes (%-4d components)\n", 01123 bdd_size_multiple(info->bwdClusteredRelationArray), 01124 array_n(info->bwdClusteredRelationArray)); 01125 } 01126 fprintf(vis_stdout, "For the options in hybrid method,"); 01127 fprintf(vis_stdout, " try print_hybrid_options and print_tfm_options.\n"); 01128 } 01129 01130 01140 void 01141 ImgRestoreTransitionFunction(Img_ImageInfo_t *imageInfo, 01142 Img_DirectionType directionType) 01143 { 01144 ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)imageInfo->methodData; 01145 01146 if (tfmInfo->vector) { 01147 ImgVectorFree(tfmInfo->vector); 01148 tfmInfo->vector = (array_t *)imageInfo->savedRelation; 01149 imageInfo->savedRelation = NIL(void); 01150 } 01151 if (tfmInfo->fwdClusteredRelationArray) { 01152 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 01153 mdd_array_free(tfmInfo->fwdClusteredRelationArray); 01154 tfmInfo->fwdClusteredRelationArray = tfmInfo->fwdSavedRelation; 01155 tfmInfo->fwdSavedRelation = NIL(array_t); 01156 } 01157 } 01158 if (tfmInfo->bwdClusteredRelationArray) { 01159 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 01160 mdd_array_free(tfmInfo->bwdClusteredRelationArray); 01161 tfmInfo->bwdClusteredRelationArray = tfmInfo->bwdSavedRelation; 01162 tfmInfo->bwdSavedRelation = NIL(array_t); 01163 } 01164 } 01165 } 01166 01167 01177 void 01178 ImgDuplicateTransitionFunction(Img_ImageInfo_t *imageInfo, 01179 Img_DirectionType directionType) 01180 { 01181 array_t *copiedVector; 01182 array_t *copiedRelation; 01183 ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)imageInfo->methodData; 01184 01185 if (tfmInfo->vector) { 01186 copiedVector = ImgVectorCopy(tfmInfo, tfmInfo->vector); 01187 assert(!imageInfo->savedRelation); 01188 imageInfo->savedRelation = (void *)tfmInfo->vector; 01189 tfmInfo->vector = copiedVector; 01190 } 01191 if (tfmInfo->fwdClusteredRelationArray) { 01192 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 01193 copiedRelation = mdd_array_duplicate(tfmInfo->fwdClusteredRelationArray); 01194 tfmInfo->fwdSavedRelation = tfmInfo->fwdClusteredRelationArray; 01195 tfmInfo->fwdClusteredRelationArray = copiedRelation; 01196 } 01197 } 01198 if (tfmInfo->bwdClusteredRelationArray) { 01199 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 01200 copiedRelation = mdd_array_duplicate(tfmInfo->bwdClusteredRelationArray); 01201 tfmInfo->bwdSavedRelation = tfmInfo->bwdClusteredRelationArray; 01202 tfmInfo->bwdClusteredRelationArray = copiedRelation; 01203 } 01204 } 01205 } 01206 01207 01217 void 01218 ImgMinimizeTransitionFunction(void *methodData, 01219 array_t *constrainArray, Img_MinimizeType minimizeMethod, 01220 Img_DirectionType directionType, int printStatus) 01221 { 01222 ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; 01223 int i, j; 01224 bdd_t *function, *simplifiedFunction; 01225 bdd_t *constrain; 01226 bdd_t *relation, *simplifiedRelation; 01227 int size = 0; 01228 long sizeConstrain; 01229 ImgComponent_t *comp; 01230 01231 if (printStatus) 01232 sizeConstrain = bdd_size_multiple(constrainArray); 01233 else 01234 sizeConstrain = 0; 01235 01236 if (info->vector) { 01237 if (printStatus) 01238 size = ImgVectorBddSize(info->vector); 01239 01240 arrayForEachItem(ImgComponent_t *, info->vector, i, comp) { 01241 function = mdd_dup(comp->func); 01242 arrayForEachItem(bdd_t *, constrainArray, j, constrain) { 01243 if (bdd_is_tautology(constrain, 1)) 01244 continue; 01245 simplifiedFunction = Img_MinimizeImage(function, constrain, 01246 minimizeMethod, TRUE); 01247 if (printStatus == 2) { 01248 (void) fprintf(vis_stdout, 01249 "IMG Info: minimized function %d | %d => %d in component %d\n", 01250 bdd_size(function), bdd_size(constrain), 01251 bdd_size(simplifiedFunction), i); 01252 } 01253 mdd_free(function); 01254 function = simplifiedFunction; 01255 } 01256 if (mdd_equal(function, comp->func)) 01257 mdd_free(function); 01258 else { 01259 mdd_free(comp->func); 01260 comp->func = function; 01261 ImgSupportClear(info, comp->support); 01262 ImgComponentGetSupport(comp); 01263 } 01264 } 01265 01266 if (printStatus) { 01267 (void) fprintf(vis_stdout, 01268 "IMG Info: minimized function [%d | %ld => %ld] with %d components\n", 01269 size, sizeConstrain, 01270 ImgVectorBddSize(info->vector), array_n(info->vector)); 01271 } 01272 } 01273 01274 if (info->buildTR == 0) 01275 return; 01276 else if (info->buildTR == 1 && info->option->synchronizeTr) { 01277 if (info->fwdClusteredRelationArray && 01278 (directionType == Img_Forward_c || directionType == Img_Both_c)) { 01279 RebuildTransitionRelation(info, Img_Forward_c); 01280 } 01281 if (info->bwdClusteredRelationArray && 01282 (directionType == Img_Backward_c || directionType == Img_Both_c)) { 01283 RebuildTransitionRelation(info, Img_Backward_c); 01284 } 01285 return; 01286 } 01287 01288 if (info->fwdClusteredRelationArray && 01289 (directionType == Img_Forward_c || directionType == Img_Both_c)) { 01290 if (printStatus) 01291 size = bdd_size_multiple(info->fwdClusteredRelationArray); 01292 arrayForEachItem(bdd_t *, constrainArray, i, constrain) { 01293 if (bdd_is_tautology(constrain, 1)) 01294 continue; 01295 01296 arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, j, relation) { 01297 simplifiedRelation = Img_MinimizeImage(relation, constrain, 01298 minimizeMethod, TRUE); 01299 if (printStatus == 2) { 01300 (void) fprintf(vis_stdout, 01301 "IMG Info: minimized fwd relation %d | %d => %d in component %d\n", 01302 bdd_size(relation), bdd_size(constrain), 01303 bdd_size(simplifiedRelation), j); 01304 } 01305 mdd_free(relation); 01306 array_insert(bdd_t*, info->fwdClusteredRelationArray, j, 01307 simplifiedRelation); 01308 } 01309 } 01310 if (printStatus) { 01311 (void) fprintf(vis_stdout, 01312 "IMG Info: minimized fwd relation [%d | %ld => %ld] with %d components\n", 01313 size, sizeConstrain, 01314 bdd_size_multiple(info->fwdClusteredRelationArray), 01315 array_n(info->fwdClusteredRelationArray)); 01316 } 01317 } 01318 if (info->bwdClusteredRelationArray && 01319 (directionType == Img_Backward_c || directionType == Img_Both_c)) { 01320 if (printStatus) 01321 size = bdd_size_multiple(info->bwdClusteredRelationArray); 01322 arrayForEachItem(bdd_t *, constrainArray, i, constrain) { 01323 if (bdd_is_tautology(constrain, 1)) 01324 continue; 01325 01326 arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, j, relation) { 01327 simplifiedRelation = Img_MinimizeImage(relation, constrain, 01328 minimizeMethod, TRUE); 01329 if (printStatus == 2) { 01330 (void) fprintf(vis_stdout, 01331 "IMG Info: minimized bwd relation %d | %d => %d in component %d\n", 01332 bdd_size(relation), bdd_size(constrain), 01333 bdd_size(simplifiedRelation), j); 01334 } 01335 mdd_free(relation); 01336 array_insert(bdd_t*, info->bwdClusteredRelationArray, j, 01337 simplifiedRelation); 01338 } 01339 } 01340 if (printStatus) { 01341 (void) fprintf(vis_stdout, 01342 "IMG Info: minimized bwd relation [%d | %ld => %ld] with %d components\n", 01343 size, sizeConstrain, 01344 bdd_size_multiple(info->bwdClusteredRelationArray), 01345 array_n(info->bwdClusteredRelationArray)); 01346 } 01347 } 01348 } 01349 01350 01361 void 01362 ImgAddDontCareToTransitionFunction(void *methodData, 01363 array_t *constrainArray, 01364 Img_MinimizeType minimizeMethod, 01365 Img_DirectionType directionType, 01366 int printStatus) 01367 { 01368 ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; 01369 int i, j; 01370 bdd_t *function, *simplifiedFunction; 01371 bdd_t *constrain; 01372 bdd_t *relation, *simplifiedRelation; 01373 int size = 0; 01374 long sizeConstrain; 01375 ImgComponent_t *comp; 01376 01377 if (printStatus) 01378 sizeConstrain = bdd_size_multiple(constrainArray); 01379 else 01380 sizeConstrain = 0; 01381 01382 if (info->vector) { 01383 if (printStatus) 01384 size = ImgVectorBddSize(info->vector); 01385 01386 arrayForEachItem(ImgComponent_t *, info->vector, i, comp) { 01387 function = mdd_dup(comp->func); 01388 arrayForEachItem(bdd_t *, constrainArray, j, constrain) { 01389 if (bdd_is_tautology(constrain, 1)) 01390 continue; 01391 simplifiedFunction = Img_AddDontCareToImage(function, constrain, 01392 minimizeMethod); 01393 if (printStatus == 2) { 01394 (void) fprintf(vis_stdout, 01395 "IMG Info: minimized function %d | %d => %d in component %d\n", 01396 bdd_size(function), bdd_size(constrain), 01397 bdd_size(simplifiedFunction), i); 01398 } 01399 mdd_free(function); 01400 function = simplifiedFunction; 01401 } 01402 if (mdd_equal(function, comp->func)) 01403 mdd_free(function); 01404 else { 01405 mdd_free(comp->func); 01406 comp->func = function; 01407 ImgSupportClear(info, comp->support); 01408 ImgComponentGetSupport(comp); 01409 } 01410 } 01411 01412 if (printStatus) { 01413 (void) fprintf(vis_stdout, 01414 "IMG Info: minimized function [%d | %ld => %ld] with %d components\n", 01415 size, sizeConstrain, 01416 ImgVectorBddSize(info->vector), array_n(info->vector)); 01417 } 01418 } 01419 01420 if (info->buildTR == 0) 01421 return; 01422 else if (info->buildTR == 1 && info->option->synchronizeTr) { 01423 if (info->fwdClusteredRelationArray && 01424 (directionType == Img_Forward_c || directionType == Img_Both_c)) { 01425 RebuildTransitionRelation(info, Img_Forward_c); 01426 } 01427 if (info->bwdClusteredRelationArray && 01428 (directionType == Img_Backward_c || directionType == Img_Both_c)) { 01429 RebuildTransitionRelation(info, Img_Backward_c); 01430 } 01431 return; 01432 } 01433 01434 if (info->fwdClusteredRelationArray && 01435 (directionType == Img_Forward_c || directionType == Img_Both_c)) { 01436 if (printStatus) 01437 size = bdd_size_multiple(info->fwdClusteredRelationArray); 01438 arrayForEachItem(bdd_t *, constrainArray, i, constrain) { 01439 if (bdd_is_tautology(constrain, 1)) 01440 continue; 01441 01442 arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, j, relation) { 01443 simplifiedRelation = Img_AddDontCareToImage(relation, constrain, 01444 minimizeMethod); 01445 if (printStatus == 2) { 01446 (void) fprintf(vis_stdout, 01447 "IMG Info: minimized fwd relation %d | %d => %d in component %d\n", 01448 bdd_size(relation), bdd_size(constrain), 01449 bdd_size(simplifiedRelation), j); 01450 } 01451 mdd_free(relation); 01452 array_insert(bdd_t*, info->fwdClusteredRelationArray, j, 01453 simplifiedRelation); 01454 } 01455 } 01456 if (printStatus) { 01457 (void) fprintf(vis_stdout, 01458 "IMG Info: minimized fwd relation [%d | %ld => %ld] with %d components\n", 01459 size, sizeConstrain, 01460 bdd_size_multiple(info->fwdClusteredRelationArray), 01461 array_n(info->fwdClusteredRelationArray)); 01462 } 01463 } 01464 if (info->bwdClusteredRelationArray && 01465 (directionType == Img_Backward_c || directionType == Img_Both_c)) { 01466 if (printStatus) 01467 size = bdd_size_multiple(info->bwdClusteredRelationArray); 01468 arrayForEachItem(bdd_t *, constrainArray, i, constrain) { 01469 if (bdd_is_tautology(constrain, 1)) 01470 continue; 01471 01472 arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, j, relation) { 01473 simplifiedRelation = Img_AddDontCareToImage(relation, constrain, 01474 minimizeMethod); 01475 if (printStatus == 2) { 01476 (void) fprintf(vis_stdout, 01477 "IMG Info: minimized bwd relation %d | %d => %d in component %d\n", 01478 bdd_size(relation), bdd_size(constrain), 01479 bdd_size(simplifiedRelation), j); 01480 } 01481 mdd_free(relation); 01482 array_insert(bdd_t*, info->bwdClusteredRelationArray, j, 01483 simplifiedRelation); 01484 } 01485 } 01486 if (printStatus) { 01487 (void) fprintf(vis_stdout, 01488 "IMG Info: minimized bwd relation [%d | %ld => %ld] with %d components\n", 01489 size, sizeConstrain, 01490 bdd_size_multiple(info->bwdClusteredRelationArray), 01491 array_n(info->bwdClusteredRelationArray)); 01492 } 01493 } 01494 } 01495 01496 01507 void 01508 ImgAbstractTransitionFunction(Img_ImageInfo_t *imageInfo, 01509 array_t *abstractVars, mdd_t *abstractCube, 01510 Img_DirectionType directionType, int printStatus) 01511 { 01512 ImgTfmInfo_t *info = (ImgTfmInfo_t *)imageInfo->methodData; 01513 int i, size = 0; 01514 bdd_t *abstractedFunction; 01515 ImgComponent_t *comp; 01516 array_t *vector; 01517 int flag = 0; 01518 int fwd_size = 0, bwd_size = 0; 01519 bdd_t *relation, *abstractedRelation; 01520 01521 if (!abstractVars || array_n(abstractVars) == 0) 01522 return; 01523 01524 if (info->vector) { 01525 if (printStatus) 01526 size = ImgVectorBddSize(info->vector); 01527 01528 arrayForEachItem(ImgComponent_t *, info->vector, i, comp) { 01529 if (bdd_is_tautology(comp->func, 1)) 01530 continue; 01531 if (abstractCube) 01532 abstractedFunction = bdd_smooth_with_cube(comp->func, abstractCube); 01533 else 01534 abstractedFunction = bdd_smooth(comp->func, abstractVars); 01535 if (bdd_is_tautology(abstractedFunction, 1)) { 01536 comp->flag = 1; 01537 flag = 1; 01538 continue; 01539 } 01540 if (mdd_equal(abstractedFunction, comp->func)) 01541 mdd_free(abstractedFunction); 01542 else { 01543 if (printStatus == 2) { 01544 (void) fprintf(vis_stdout, 01545 "IMG Info: abstracted function %d => %d in component %d\n", 01546 bdd_size(comp->func), bdd_size(abstractedFunction), i); 01547 } 01548 mdd_free(comp->func); 01549 comp->func = abstractedFunction; 01550 ImgSupportClear(info, comp->support); 01551 ImgComponentGetSupport(comp); 01552 } 01553 } 01554 01555 if (flag) { 01556 vector = info->vector; 01557 info->vector = array_alloc(ImgComponent_t *, 0); 01558 arrayForEachItem(ImgComponent_t *, vector, i, comp) { 01559 if (comp->flag) { 01560 ImgComponentFree(comp); 01561 continue; 01562 } 01563 array_insert_last(ImgComponent_t *, info->vector, comp); 01564 } 01565 array_free(vector); 01566 } 01567 01568 if (printStatus) { 01569 (void) fprintf(vis_stdout, 01570 "IMG Info: abstracted function [%d => %ld] with %d components\n", 01571 size, ImgVectorBddSize(info->vector), 01572 array_n(info->vector)); 01573 } 01574 } 01575 01576 if (info->buildTR == 0) 01577 return; 01578 else if (info->buildTR == 1 && info->option->synchronizeTr) { 01579 if (info->fwdClusteredRelationArray && 01580 (directionType == Img_Forward_c || directionType == Img_Both_c)) { 01581 RebuildTransitionRelation(info, Img_Forward_c); 01582 } 01583 if (info->bwdClusteredRelationArray && 01584 (directionType == Img_Backward_c || directionType == Img_Both_c)) { 01585 RebuildTransitionRelation(info, Img_Backward_c); 01586 } 01587 return; 01588 } 01589 01590 if (printStatus) { 01591 if (directionType == Img_Forward_c || directionType == Img_Both_c) 01592 fwd_size = bdd_size_multiple(info->fwdClusteredRelationArray); 01593 if (directionType == Img_Backward_c || directionType == Img_Both_c) 01594 bwd_size = bdd_size_multiple(info->bwdClusteredRelationArray); 01595 } 01596 if (info->fwdClusteredRelationArray && 01597 (directionType == Img_Forward_c || directionType == Img_Both_c)) { 01598 arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) { 01599 if (abstractCube) 01600 abstractedRelation = bdd_smooth_with_cube(relation, abstractCube); 01601 else 01602 abstractedRelation = bdd_smooth(relation, abstractVars); 01603 if (printStatus == 2) { 01604 (void) fprintf(vis_stdout, 01605 "IMG Info: abstracted fwd relation %d => %d in component %d\n", 01606 bdd_size(relation), bdd_size(abstractedRelation), i); 01607 } 01608 mdd_free(relation); 01609 array_insert(bdd_t*, info->fwdClusteredRelationArray, i, 01610 abstractedRelation); 01611 } 01612 } 01613 if (info->bwdClusteredRelationArray && 01614 (directionType == Img_Backward_c || directionType == Img_Both_c)) { 01615 arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) { 01616 if (abstractCube) 01617 abstractedRelation = bdd_smooth_with_cube(relation, abstractCube); 01618 else 01619 abstractedRelation = bdd_smooth(relation, abstractVars); 01620 if (printStatus == 2) { 01621 (void) fprintf(vis_stdout, 01622 "IMG Info: abstracted bwd relation %d => %d in component %d\n", 01623 bdd_size(relation), bdd_size(abstractedRelation), i); 01624 } 01625 mdd_free(relation); 01626 array_insert(bdd_t*, info->bwdClusteredRelationArray, i, 01627 abstractedRelation); 01628 } 01629 } 01630 if (printStatus) { 01631 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 01632 (void) fprintf(vis_stdout, 01633 "IMG Info: abstracted fwd relation [%d => %ld] with %d components\n", 01634 fwd_size, 01635 bdd_size_multiple(info->fwdClusteredRelationArray), 01636 array_n(info->fwdClusteredRelationArray)); 01637 } 01638 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 01639 (void) fprintf(vis_stdout, 01640 "IMG Info: abstracted bwd relation [%d => %ld] with %d components\n", 01641 bwd_size, 01642 bdd_size_multiple(info->bwdClusteredRelationArray), 01643 array_n(info->bwdClusteredRelationArray)); 01644 } 01645 } 01646 } 01647 01648 01658 int 01659 ImgApproximateTransitionFunction(mdd_manager *mgr, 01660 void *methodData, bdd_approx_dir_t approxDir, 01661 bdd_approx_type_t approxMethod, int approxThreshold, 01662 double approxQuality, double approxQualityBias, 01663 Img_DirectionType directionType, mdd_t *bias) 01664 { 01665 ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; 01666 int i; 01667 bdd_t *approxFunction; 01668 int unchanged = 0; 01669 ImgComponent_t *comp; 01670 bdd_t *relation, *approxRelation; 01671 01672 if (info->vector) { 01673 arrayForEachItem(ImgComponent_t *, info->vector, i, comp) { 01674 approxFunction = Img_ApproximateImage(mgr, comp->func, 01675 approxDir, approxMethod, 01676 approxThreshold, approxQuality, 01677 approxQualityBias, bias); 01678 if (bdd_is_tautology(approxFunction, 1)) { 01679 fprintf(vis_stdout, 01680 "** img warning : bdd_one from subsetting in [%d].\n", i); 01681 mdd_free(approxFunction); 01682 unchanged++; 01683 } else if (bdd_is_tautology(approxFunction, 0)) { 01684 fprintf(vis_stdout, 01685 "** img warning : bdd_zero from subsetting in [%d].\n", i); 01686 mdd_free(approxFunction); 01687 unchanged++; 01688 } else if (mdd_equal(approxFunction, comp->func)) { 01689 mdd_free(approxFunction); 01690 unchanged++; 01691 } else { 01692 mdd_free(comp->func); 01693 comp->func = approxFunction; 01694 ImgSupportClear(info, comp->support); 01695 ImgComponentGetSupport(comp); 01696 } 01697 } 01698 } 01699 01700 if (info->buildTR == 0) 01701 return(unchanged); 01702 else if (info->buildTR == 1 && info->option->synchronizeTr) { 01703 if (info->fwdClusteredRelationArray && 01704 (directionType == Img_Forward_c || directionType == Img_Both_c)) { 01705 RebuildTransitionRelation(info, Img_Forward_c); 01706 } 01707 if (info->bwdClusteredRelationArray && 01708 (directionType == Img_Backward_c || directionType == Img_Both_c)) { 01709 RebuildTransitionRelation(info, Img_Backward_c); 01710 } 01711 return(unchanged); 01712 } 01713 01714 if (info->fwdClusteredRelationArray && 01715 (directionType == Img_Forward_c || directionType == Img_Both_c)) { 01716 arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) { 01717 approxRelation = Img_ApproximateImage(mgr, relation, 01718 approxDir, approxMethod, 01719 approxThreshold, approxQuality, 01720 approxQualityBias, bias); 01721 if (bdd_is_tautology(approxRelation, 1)) { 01722 fprintf(vis_stdout, 01723 "** img warning : bdd_one from subsetting in fwd[%d].\n", i); 01724 mdd_free(approxRelation); 01725 unchanged++; 01726 } else if (bdd_is_tautology(approxRelation, 0)) { 01727 fprintf(vis_stdout, 01728 "** img warning : bdd_zero from subsetting in fwd[%d].\n", i); 01729 mdd_free(approxRelation); 01730 unchanged++; 01731 } else if (mdd_equal(approxRelation, relation)) { 01732 mdd_free(approxRelation); 01733 unchanged++; 01734 } else { 01735 mdd_free(relation); 01736 array_insert(bdd_t*, info->fwdClusteredRelationArray, i, 01737 approxRelation); 01738 } 01739 } 01740 } 01741 if (info->bwdClusteredRelationArray && 01742 (directionType == Img_Backward_c || directionType == Img_Both_c)) { 01743 arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) { 01744 approxRelation = Img_ApproximateImage(mgr, relation, 01745 approxDir, approxMethod, 01746 approxThreshold, approxQuality, 01747 approxQualityBias, bias); 01748 if (bdd_is_tautology(approxRelation, 1)) { 01749 fprintf(vis_stdout, 01750 "** img warning : bdd_one from subsetting in bwd[%d].\n", i); 01751 mdd_free(approxRelation); 01752 unchanged++; 01753 } else if (bdd_is_tautology(approxRelation, 0)) { 01754 fprintf(vis_stdout, 01755 "** img warning : bdd_zero from subsetting in bwd[%d].\n", i); 01756 mdd_free(approxRelation); 01757 unchanged++; 01758 } else if (mdd_equal(approxRelation, relation)) { 01759 mdd_free(approxRelation); 01760 unchanged++; 01761 } else { 01762 mdd_free(relation); 01763 array_insert(bdd_t*, info->bwdClusteredRelationArray, i, 01764 approxRelation); 01765 } 01766 } 01767 } 01768 return(unchanged); 01769 } 01770 01771 01781 array_t * 01782 ImgGetTransitionFunction(void *methodData, Img_DirectionType directionType) 01783 { 01784 ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)methodData; 01785 if (tfmInfo->vector) 01786 return(tfmInfo->vector); 01787 if (directionType == Img_Forward_c) 01788 return(tfmInfo->fwdClusteredRelationArray); 01789 return(tfmInfo->bwdClusteredRelationArray); 01790 } 01791 01792 01802 void 01803 ImgUpdateTransitionFunction(void *methodData, array_t *vector, 01804 Img_DirectionType directionType) 01805 { 01806 ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)methodData; 01807 if (tfmInfo->vector) 01808 tfmInfo->vector = vector; 01809 else if (directionType == Img_Forward_c) 01810 tfmInfo->fwdClusteredRelationArray = vector; 01811 else 01812 tfmInfo->bwdClusteredRelationArray = vector; 01813 } 01814 01815 01825 void 01826 ImgReplaceIthTransitionFunction(void *methodData, int i, mdd_t *function, 01827 Img_DirectionType directionType) 01828 { 01829 ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; 01830 array_t *relationArray; 01831 ImgComponent_t *comp; 01832 mdd_t *old; 01833 01834 if (info->vector) { 01835 comp = array_fetch(ImgComponent_t *, info->vector, i); 01836 mdd_free(comp->func); 01837 comp->func = function; 01838 ImgSupportClear(info, comp->support); 01839 ImgComponentGetSupport(comp); 01840 return; 01841 } 01842 01843 if (directionType == Img_Forward_c) 01844 relationArray = info->fwdClusteredRelationArray; 01845 else 01846 relationArray = info->bwdClusteredRelationArray; 01847 01848 old = array_fetch(mdd_t *, relationArray, i); 01849 mdd_free(old); 01850 array_insert(mdd_t *, relationArray, i, function); 01851 } 01852 01853 01865 ImgTfmOption_t * 01866 ImgTfmGetOptions(Img_MethodType method) 01867 { 01868 char *flagValue; 01869 ImgTfmOption_t *option; 01870 01871 option = ALLOC(ImgTfmOption_t, 1); 01872 memset(option, 0, sizeof(ImgTfmOption_t)); 01873 01874 option->debug = ReadSetBooleanValue("tfm_debug", FALSE); 01875 option->checkEquivalence = ReadSetBooleanValue("tfm_check_equivalence", 01876 FALSE); 01877 option->writeSupportMatrix = ReadSetIntValue("tfm_write_support_matrix", 01878 0, 2, 0); 01879 option->writeSupportMatrixWithYvars = 01880 ReadSetBooleanValue("tfm_write_support_matrix_with_y", FALSE); 01881 option->writeSupportMatrixAndStop = 01882 ReadSetBooleanValue("tfm_write_support_matrix_and_stop", FALSE); 01883 option->writeSupportMatrixReverseRow = 01884 ReadSetBooleanValue("tfm_write_support_matrix_reverse_row", TRUE); 01885 option->writeSupportMatrixReverseCol = 01886 ReadSetBooleanValue("tfm_write_support_matrix_reverse_col", TRUE); 01887 01888 option->verbosity = ReadSetIntValue("tfm_verbosity", 0, 2, 0); 01889 if (method == Img_Tfm_c) 01890 option->splitMethod = ReadSetIntValue("tfm_split_method", 0, 3, 0); 01891 else 01892 option->splitMethod = 3; /* the default value */ 01893 option->inputSplit = ReadSetIntValue("tfm_input_split", 0, 3, 0); 01894 option->piSplitFlag = ReadSetBooleanValue("tfm_pi_split_flag", TRUE); 01895 if (method == Img_Tfm_c) 01896 option->rangeComp = ReadSetIntValue("tfm_range_comp", 0, 2, 1); 01897 else 01898 option->rangeComp = ReadSetIntValue("tfm_range_comp", 0, 2, 2); 01899 01900 flagValue = Cmd_FlagReadByName("tfm_range_threshold"); 01901 if (flagValue == NIL(char)) 01902 option->rangeThreshold = 10; /* the default value */ 01903 else 01904 option->rangeThreshold = atoi(flagValue); 01905 01906 flagValue = Cmd_FlagReadByName("tfm_range_try_threshold"); 01907 if (flagValue == NIL(char)) 01908 option->rangeTryThreshold = 2; /* the default value */ 01909 else 01910 option->rangeTryThreshold = atoi(flagValue); 01911 01912 option->rangeCheckReorder = 01913 ReadSetBooleanValue("tfm_range_check_reorder", FALSE); 01914 option->tieBreakMode = ReadSetIntValue("tfm_tie_break", 0, 1, 0); 01915 01916 option->outputSplit = ReadSetIntValue("tfm_output_split", 0, 2, 0); 01917 01918 flagValue = Cmd_FlagReadByName("tfm_turn_depth"); 01919 if (flagValue == NIL(char)) { 01920 if (method == Img_Tfm_c) 01921 option->turnDepth = 5; /* the default for tfm */ 01922 else 01923 option->turnDepth = -1; /* the default for hybrid */ 01924 } else 01925 option->turnDepth = atoi(flagValue); 01926 01927 option->findDecompVar = ReadSetBooleanValue("tfm_find_decomp_var", FALSE); 01928 option->globalCache = ReadSetBooleanValue("tfm_global_cache", TRUE); 01929 01930 flagValue = Cmd_FlagReadByName("tfm_use_cache"); 01931 if (flagValue == NIL(char)) { 01932 if (method == Img_Tfm_c) 01933 option->useCache = 1; 01934 else 01935 option->useCache = 0; 01936 } else 01937 option->useCache = atoi(flagValue); 01938 01939 flagValue = Cmd_FlagReadByName("tfm_max_chain_length"); 01940 if (flagValue == NIL(char)) 01941 option->maxChainLength = 2; /* the default value */ 01942 else 01943 option->maxChainLength = atoi(flagValue); 01944 01945 flagValue = Cmd_FlagReadByName("tfm_init_cache_size"); 01946 if (flagValue == NIL(char)) 01947 option->initCacheSize = 1001; /* the default value */ 01948 else 01949 option->initCacheSize = atoi(flagValue); 01950 01951 option->autoFlushCache = ReadSetIntValue("tfm_auto_flush_cache", 0, 2, 1); 01952 if (method == Img_Tfm_c) 01953 option->sortVectorFlag = ReadSetBooleanValue("tfm_sort_vector", TRUE); 01954 else 01955 option->sortVectorFlag = ReadSetBooleanValue("tfm_sort_vector", FALSE); 01956 option->printStatistics = ReadSetBooleanValue("tfm_print_stats", FALSE); 01957 option->printBddSize = ReadSetBooleanValue("tfm_print_bdd_size", FALSE); 01958 01959 flagValue = Cmd_FlagReadByName("tfm_max_essential_depth"); 01960 if (flagValue == NIL(char)) 01961 option->maxEssentialDepth = 5; /* the default value */ 01962 else 01963 option->maxEssentialDepth = atoi(flagValue); 01964 01965 option->findEssential = ReadSetIntValue("tfm_find_essential", 0, 2, 0); 01966 if (option->findEssential && bdd_get_package_name() != CUDD) { 01967 fprintf(vis_stderr, 01968 "** tfm error: tfm_find_essential is available for only CUDD.\n"); 01969 option->findEssential = 0; 01970 } 01971 option->printEssential = ReadSetIntValue("tfm_print_essential", 0, 2, 0); 01972 option->splitCubeFunc = ReadSetBooleanValue("tfm_split_cube_func", FALSE); 01973 option->composeIntermediateVars = 01974 ReadSetBooleanValue("tfm_compose_intermediate_vars", FALSE); 01975 01976 if (method == Img_Tfm_c) 01977 option->preSplitMethod = ReadSetIntValue("tfm_pre_split_method", 0, 4, 0); 01978 else 01979 option->preSplitMethod = 4; 01980 option->preInputSplit = ReadSetIntValue("tfm_pre_input_split", 0, 3, 0); 01981 option->preOutputSplit = ReadSetIntValue("tfm_pre_output_split", 0, 2, 0); 01982 option->preDcLeafMethod = ReadSetIntValue("tfm_pre_dc_leaf_method", 0, 2, 0); 01983 option->preMinimize = ReadSetBooleanValue("tfm_pre_minimize", FALSE); 01984 01985 option->trSplitMethod = ReadSetIntValue("hybrid_tr_split_method", 0, 1, 0); 01986 01987 option->hybridMode = ReadSetIntValue("hybrid_mode", 0, 2, 1); 01988 option->buildPartialTR = 01989 ReadSetBooleanValue("hybrid_build_partial_tr", FALSE); 01990 01991 flagValue = Cmd_FlagReadByName("hybrid_partial_num_vars"); 01992 if (flagValue == NIL(char)) 01993 option->nPartialVars = 8; /* the default value */ 01994 else 01995 option->nPartialVars = atoi(flagValue); 01996 01997 option->partialMethod = ReadSetIntValue("hybrid_partial_method", 0, 1, 0); 01998 01999 option->delayedSplit = ReadSetBooleanValue("hybrid_delayed_split", FALSE); 02000 02001 flagValue = Cmd_FlagReadByName("hybrid_split_min_depth"); 02002 if (flagValue == NIL(char)) 02003 option->splitMinDepth = 1; /* the default value */ 02004 else 02005 option->splitMinDepth = atoi(flagValue); 02006 02007 flagValue = Cmd_FlagReadByName("hybrid_split_max_depth"); 02008 if (flagValue == NIL(char)) 02009 option->splitMaxDepth = 5; /* the default value */ 02010 else 02011 option->splitMaxDepth = atoi(flagValue); 02012 02013 flagValue = Cmd_FlagReadByName("hybrid_pre_split_min_depth"); 02014 if (flagValue == NIL(char)) 02015 option->preSplitMinDepth = 0; /* the default value */ 02016 else 02017 option->preSplitMinDepth = atoi(flagValue); 02018 02019 flagValue = Cmd_FlagReadByName("hybrid_pre_split_max_depth"); 02020 if (flagValue == NIL(char)) 02021 option->preSplitMaxDepth = 4; /* the default value */ 02022 else 02023 option->preSplitMaxDepth = atoi(flagValue); 02024 02025 flagValue = Cmd_FlagReadByName("hybrid_lambda_threshold"); 02026 if (flagValue == NIL(char)) 02027 option->lambdaThreshold = 0.6; /* the default value */ 02028 else 02029 sscanf(flagValue, "%f", &option->lambdaThreshold); 02030 02031 flagValue = Cmd_FlagReadByName("hybrid_pre_lambda_threshold"); 02032 if (flagValue == NIL(char)) 02033 option->preLambdaThreshold = 0.65; /* the default value */ 02034 else 02035 sscanf(flagValue, "%f", &option->preLambdaThreshold); 02036 02037 flagValue = Cmd_FlagReadByName("hybrid_conjoin_vector_size"); 02038 if (flagValue == NIL(char)) 02039 option->conjoinVectorSize = 10; /* the default value */ 02040 else 02041 option->conjoinVectorSize = atoi(flagValue); 02042 02043 flagValue = Cmd_FlagReadByName("hybrid_conjoin_relation_size"); 02044 if (flagValue == NIL(char)) 02045 option->conjoinRelationSize = 1; /* the default value */ 02046 else 02047 option->conjoinRelationSize = atoi(flagValue); 02048 02049 flagValue = Cmd_FlagReadByName("hybrid_conjoin_relation_bdd_size"); 02050 if (flagValue == NIL(char)) 02051 option->conjoinRelationBddSize = 200; /* the default value */ 02052 else 02053 option->conjoinRelationBddSize = atoi(flagValue); 02054 02055 flagValue = Cmd_FlagReadByName("hybrid_improve_lambda"); 02056 if (flagValue == NIL(char)) 02057 option->improveLambda = 0.1; /* the default value */ 02058 else 02059 sscanf(flagValue, "%f", &option->improveLambda); 02060 02061 flagValue = Cmd_FlagReadByName("hybrid_improve_vector_size"); 02062 if (flagValue == NIL(char)) 02063 option->improveVectorSize = 3; /* the default value */ 02064 else 02065 option->improveVectorSize = atoi(flagValue); 02066 02067 flagValue = Cmd_FlagReadByName("hybrid_improve_vector_bdd_size"); 02068 if (flagValue == NIL(char)) 02069 option->improveVectorBddSize = 30.0; /* the default value */ 02070 else 02071 sscanf(flagValue, "%f", &option->improveVectorBddSize); 02072 02073 option->decideMode = ReadSetIntValue("hybrid_decide_mode", 0, 3, 3); 02074 02075 option->reorderWithFrom = 02076 ReadSetBooleanValue("hybrid_reorder_with_from", TRUE); 02077 option->preReorderWithFrom = 02078 ReadSetBooleanValue("hybrid_pre_reorder_with_from", FALSE); 02079 02080 option->lambdaMode = ReadSetIntValue("hybrid_lambda_mode", 0, 2, 0); 02081 option->preLambdaMode = ReadSetIntValue("hybrid_pre_lambda_mode", 0, 3, 2); 02082 option->lambdaWithFrom = ReadSetBooleanValue("hybrid_lambda_with_from", TRUE); 02083 option->lambdaWithTr = ReadSetBooleanValue("hybrid_lambda_with_tr", TRUE); 02084 option->lambdaWithClustering = 02085 ReadSetBooleanValue("hybrid_lambda_with_clustering", FALSE); 02086 02087 option->synchronizeTr = ReadSetBooleanValue("hybrid_synchronize_tr", FALSE); 02088 option->imgKeepPiInTr = ReadSetBooleanValue("hybrid_img_keep_pi", FALSE); 02089 option->preKeepPiInTr = ReadSetBooleanValue("hybrid_pre_keep_pi", FALSE); 02090 02091 flagValue = Cmd_FlagReadByName("hybrid_tr_method"); 02092 if (flagValue == NIL(char)) 02093 option->trMethod = Img_Iwls95_c; /* the default value */ 02094 else { 02095 if (strcmp(flagValue, "iwls95") == 0) 02096 option->trMethod = Img_Iwls95_c; 02097 else if (strcmp(flagValue, "mlp") == 0) 02098 option->trMethod = Img_Mlp_c; 02099 else { 02100 fprintf(vis_stderr, 02101 "** tfm error : invalid value %s for hybrid_tr_method\n", 02102 flagValue); 02103 option->trMethod = Img_Iwls95_c; 02104 } 02105 } 02106 option->preCanonical = ReadSetBooleanValue("hybrid_pre_canonical", FALSE); 02107 02108 option->printLambda = ReadSetBooleanValue("hybrid_print_lambda", FALSE); 02109 02110 return(option); 02111 } 02112 02113 02125 void 02126 ImgImageFreeClusteredTransitionRelationTfm(void *methodData, 02127 Img_DirectionType directionType) 02128 { 02129 ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; 02130 02131 if (info->vector) { 02132 ImgVectorFree(info->vector); 02133 info->vector = NIL(array_t); 02134 } 02135 if (info->fullVector) { 02136 ImgVectorFree(info->fullVector); 02137 info->fullVector = NIL(array_t); 02138 } 02139 if (info->partialBddVars) 02140 mdd_array_free(info->partialBddVars); 02141 if (info->partialVarFlag) 02142 FREE(info->partialVarFlag); 02143 if (info->fwdClusteredRelationArray != NIL(array_t)) { 02144 mdd_array_free(info->fwdClusteredRelationArray); 02145 info->fwdClusteredRelationArray = NIL(array_t); 02146 } 02147 if (info->bwdClusteredRelationArray != NIL(array_t)) { 02148 mdd_array_free(info->bwdClusteredRelationArray); 02149 info->bwdClusteredRelationArray = NIL(array_t); 02150 } 02151 } 02152 02153 02171 void 02172 ImgImageConstrainAndClusterTransitionRelationTfm(Img_ImageInfo_t *imageInfo, 02173 Img_DirectionType direction, 02174 mdd_t *constrain, 02175 Img_MinimizeType minimizeMethod, 02176 boolean underApprox, 02177 boolean cleanUp, 02178 boolean forceReorder, 02179 int printStatus) 02180 { 02181 ImgFunctionData_t *functionData = &(imageInfo->functionData); 02182 ImgTfmInfo_t *info = (ImgTfmInfo_t *)imageInfo->methodData; 02183 graph_t *mddNetwork; 02184 mdd_manager *mddManager = Part_PartitionReadMddManager( 02185 functionData->mddNetwork); 02186 int composeIntermediateVars, findIntermediateVars; 02187 array_t *relationArray; 02188 02189 /* free existing function vector and/or relation */ 02190 ImgImageFreeClusteredTransitionRelationTfm(imageInfo->methodData, direction); 02191 if (forceReorder) 02192 bdd_reorder(mddManager); 02193 02194 mddNetwork = functionData->mddNetwork; 02195 02196 /* create function vector or bit relation */ 02197 if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c && 02198 info->nVars != info->nRealVars) { 02199 if (info->option->composeIntermediateVars) { 02200 composeIntermediateVars = 1; 02201 findIntermediateVars = 0; 02202 } else { 02203 composeIntermediateVars = 0; 02204 findIntermediateVars = 1; 02205 } 02206 } else { 02207 composeIntermediateVars = 0; 02208 findIntermediateVars = 0; 02209 } 02210 02211 if (info->buildTR == 2) { /* non-deterministic */ 02212 if (info->buildPartialTR) { 02213 info->fullVector = TfmCreateBitVector(info, composeIntermediateVars, 02214 findIntermediateVars); 02215 TfmSetupPartialTransitionRelation(info, &relationArray); 02216 } else { 02217 info->vector = NIL(array_t); 02218 relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars, 02219 findIntermediateVars); 02220 } 02221 } else { 02222 info->vector = TfmCreateBitVector(info, composeIntermediateVars, 02223 findIntermediateVars); 02224 if (info->buildTR == 0 || info->option->synchronizeTr) 02225 relationArray = NIL(array_t); 02226 else { 02227 relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars, 02228 findIntermediateVars); 02229 } 02230 } 02231 02232 /* apply the constrain to the bit relation */ 02233 if (constrain) { 02234 if (underApprox) { 02235 MinimizeTransitionFunction(info->vector, relationArray, 02236 constrain, minimizeMethod, printStatus); 02237 } else { 02238 AddDontCareToTransitionFunction(info->vector, relationArray, 02239 constrain, minimizeMethod, printStatus); 02240 } 02241 } 02242 02243 if (info->vector && info->option->sortVectorFlag && info->option->useCache) 02244 array_sort(info->vector, CompareIndex); 02245 if (info->buildTR) { 02246 TfmBuildRelationArray(info, functionData, relationArray, direction, 0); 02247 if (relationArray) 02248 mdd_array_free(relationArray); 02249 } 02250 02251 /* Print information */ 02252 if (info->option->verbosity > 0){ 02253 if (info->method == Img_Tfm_c) 02254 fprintf(vis_stdout,"Computing Image Using tfm technique.\n"); 02255 else 02256 fprintf(vis_stdout,"Computing Image Using hybrid technique.\n"); 02257 fprintf(vis_stdout,"Total # of domain binary variables = %3d\n", 02258 array_n(functionData->domainBddVars)); 02259 fprintf(vis_stdout,"Total # of range binary variables = %3d\n", 02260 array_n(functionData->rangeBddVars)); 02261 fprintf(vis_stdout,"Total # of quantify binary variables = %3d\n", 02262 array_n(functionData->quantifyBddVars)); 02263 if (info->vector) { 02264 (void) fprintf(vis_stdout, 02265 "Shared size of transition function vector for image "); 02266 (void) fprintf(vis_stdout, 02267 "computation is %10ld BDD nodes (%-4d components)\n", 02268 ImgVectorBddSize(info->vector), array_n(info->vector)); 02269 } 02270 if (((direction == Img_Forward_c) || (direction == Img_Both_c)) && 02271 (info->fwdClusteredRelationArray != NIL(array_t))) { 02272 (void) fprintf(vis_stdout, 02273 "Shared size of transition relation for forward image "); 02274 (void) fprintf(vis_stdout, 02275 "computation is %10ld BDD nodes (%-4d components)\n", 02276 bdd_size_multiple(info->fwdClusteredRelationArray), 02277 array_n(info->fwdClusteredRelationArray)); 02278 } 02279 if (((direction == Img_Backward_c) || (direction == Img_Both_c)) && 02280 (info->bwdClusteredRelationArray != NIL(array_t))) { 02281 (void) fprintf(vis_stdout, 02282 "Shared size of transition relation for backward image "); 02283 (void) fprintf(vis_stdout, 02284 "computation is %10ld BDD nodes (%-4d components)\n", 02285 bdd_size_multiple(info->bwdClusteredRelationArray), 02286 array_n(info->bwdClusteredRelationArray)); 02287 } 02288 } 02289 } 02290 02291 02301 int 02302 ImgIsPartitionedTransitionRelationTfm(Img_ImageInfo_t *imageInfo) 02303 { 02304 ImgTfmInfo_t *info = (ImgTfmInfo_t *)imageInfo->methodData; 02305 02306 if (info->buildTR) 02307 return(1); 02308 else 02309 return(0); 02310 } 02311 02312 02313 /*---------------------------------------------------------------------------*/ 02314 /* Definition of static functions */ 02315 /*---------------------------------------------------------------------------*/ 02316 02317 02329 static ImgTfmInfo_t * 02330 TfmInfoStructAlloc(Img_MethodType method) 02331 { 02332 ImgTfmInfo_t *info; 02333 02334 info = ALLOC(ImgTfmInfo_t, 1); 02335 memset(info, 0, sizeof(ImgTfmInfo_t)); 02336 info->method = method; 02337 info->option = ImgTfmGetOptions(method); 02338 return(info); 02339 } 02340 02341 02351 static int 02352 CompareIndex(const void *e1, const void *e2) 02353 { 02354 ImgComponent_t *c1, *c2; 02355 int id1, id2; 02356 02357 c1 = *((ImgComponent_t **)e1); 02358 c2 = *((ImgComponent_t **)e2); 02359 02360 id1 = (int)bdd_top_var_id(c1->var); 02361 id2 = (int)bdd_top_var_id(c2->var); 02362 02363 if (id1 > id2) 02364 return(1); 02365 else if (id1 < id2) 02366 return(-1); 02367 else 02368 return(0); 02369 } 02370 02371 02381 static int 02382 HookInfoFunction(bdd_manager *mgr, char *str, void *method) 02383 { 02384 ImgTfmInfo_t *info; 02385 st_generator *stGen; 02386 02387 if (HookInfoList) { 02388 st_foreach_item(HookInfoList, stGen, &info, NULL) { 02389 if (info->imgCache) 02390 ImgFlushCache(info->imgCache); 02391 if (info->preCache) 02392 ImgFlushCache(info->preCache); 02393 } 02394 } 02395 return(0); 02396 } 02397 02398 02409 static array_t * 02410 ChoosePartialVars(ImgTfmInfo_t *info, array_t *vector, int nPartialVars, 02411 int partialMethod) 02412 { 02413 int i, j, nVars; 02414 ImgComponent_t *comp; 02415 char *support; 02416 int *varCost; 02417 int big, small, nChosen, insert, id; 02418 mdd_t *var; 02419 int *partialVars = ALLOC(int, nPartialVars); 02420 array_t *partialBddVars = array_alloc(mdd_t *, 0); 02421 02422 nVars = info->nVars; 02423 varCost = ALLOC(int, nVars); 02424 memset(varCost, 0, sizeof(int) * nVars); 02425 02426 if (partialMethod == 0) { 02427 /* chooses the variable whose function has the largest bdd size */ 02428 for (i = 0; i < array_n(vector); i++) { 02429 comp = array_fetch(ImgComponent_t *, vector, i); 02430 id = (int)bdd_top_var_id(comp->var); 02431 varCost[id] = bdd_size(comp->func); 02432 } 02433 } else { 02434 /* chooses the variable that appears the most frequently */ 02435 for (i = 0; i < array_n(vector); i++) { 02436 comp = array_fetch(ImgComponent_t *, vector, i); 02437 support = comp->support; 02438 for (j = 0; j < nVars; j++) { 02439 if (support[j]) 02440 varCost[j]++; 02441 } 02442 } 02443 } 02444 02445 nChosen = 0; 02446 big = small = -1; 02447 for (i = 0; i < nVars; i++) { 02448 if (varCost[i] == 0) 02449 continue; 02450 if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) 02451 continue; 02452 if (info->intermediateVarsTable && 02453 st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) { 02454 continue; 02455 } 02456 if (nChosen == 0) { 02457 partialVars[0] = i; 02458 nChosen = 1; 02459 big = small = varCost[i]; 02460 } else if (varCost[i] < small) { 02461 if (nChosen < nPartialVars) { 02462 partialVars[nChosen] = i; 02463 nChosen++; 02464 small = varCost[i]; 02465 } else 02466 continue; 02467 } else if (varCost[i] > big) { 02468 if (nChosen < nPartialVars) { 02469 for (j = nChosen; j > 0; j--) 02470 partialVars[j] = partialVars[j - 1]; 02471 partialVars[0] = i; 02472 nChosen++; 02473 big = varCost[i]; 02474 } else { 02475 for (j = nPartialVars - 1; j > 0; j--) 02476 partialVars[j] = partialVars[j - 1]; 02477 partialVars[0] = i; 02478 big = varCost[i]; 02479 small = varCost[partialVars[nPartialVars - 1]]; 02480 } 02481 } else { 02482 insert = nChosen; 02483 for (j = 0; j < nChosen; j++) { 02484 if (varCost[i] > varCost[partialVars[j]]) { 02485 insert = j; 02486 break; 02487 } 02488 } 02489 if (nChosen < nPartialVars) { 02490 for (j = nChosen; j > insert; j--) 02491 partialVars[j] = partialVars[j - 1]; 02492 partialVars[insert] = i; 02493 nChosen++; 02494 } else if (insert < nChosen) { 02495 for (j = nPartialVars - 1; j > insert; j--) 02496 partialVars[j] = partialVars[j - 1]; 02497 partialVars[insert] = i; 02498 small = varCost[partialVars[nPartialVars - 1]]; 02499 } 02500 } 02501 } 02502 FREE(varCost); 02503 02504 for (i = 0; i < nChosen; i++) { 02505 var = bdd_var_with_index(info->manager, partialVars[i]); 02506 array_insert_last(mdd_t *, partialBddVars, var); 02507 } 02508 02509 FREE(partialVars); 02510 return(partialBddVars); 02511 } 02512 02513 02525 static void 02526 PrintRecursionStatistics(ImgTfmInfo_t *info, int preFlag) 02527 { 02528 float avgDepth, avgDecomp; 02529 int nRecurs, nLeaves, nTurns, nDecomps, topDecomp, maxDecomp, maxDepth; 02530 02531 GetRecursionStatistics(info, preFlag, &nRecurs, &nLeaves, &nTurns, &avgDepth, 02532 &maxDepth, &nDecomps, &topDecomp, &maxDecomp, &avgDecomp); 02533 if (preFlag) 02534 fprintf(vis_stdout, "** recursion statistics of splitting (preImg) **\n"); 02535 else 02536 fprintf(vis_stdout, "** recursion statistics of splitting (img) **\n"); 02537 fprintf(vis_stdout, "# recursions = %d\n", nRecurs); 02538 fprintf(vis_stdout, "# leaves = %d\n", nLeaves); 02539 fprintf(vis_stdout, "# turns = %d\n", nTurns); 02540 fprintf(vis_stdout, "# average recursion depth = %g (max = %d)\n", 02541 avgDepth, maxDepth); 02542 if (!preFlag) { 02543 fprintf(vis_stdout, 02544 "# decompositions = %d (top = %d, max = %d, average = %g)\n", 02545 nDecomps, topDecomp, maxDecomp, avgDecomp); 02546 } 02547 } 02548 02549 02561 static void 02562 PrintFoundVariableStatistics(ImgTfmInfo_t *info, int preFlag) 02563 { 02564 int i, maxDepth; 02565 02566 if (preFlag) { 02567 fprintf(vis_stdout, "# split = %d, conjoin = %d\n", 02568 info->nSplitsB, info->nConjoinsB); 02569 return; 02570 } 02571 02572 fprintf(vis_stdout, 02573 "# found essential vars = %d (top = %d, average = %g, averageDepth = %g)\n", 02574 info->nFoundEssentials, info->topFoundEssentialDepth, 02575 info->averageFoundEssential, info->averageFoundEssentialDepth); 02576 if (info->option->printEssential == 1) { 02577 maxDepth = info->maxDepth < IMG_TF_MAX_PRINT_DEPTH ? 02578 info->maxDepth : IMG_TF_MAX_PRINT_DEPTH; 02579 fprintf(vis_stdout, "foundEssential:"); 02580 for (i = 0; i < maxDepth; i++) 02581 fprintf(vis_stdout, " [%d]%d", i, info->foundEssentials[i]); 02582 fprintf(vis_stdout, "\n"); 02583 } 02584 if (info->useConstraint == 2) 02585 fprintf(vis_stdout, "# range computations = %d\n", info->nRangeComps); 02586 fprintf(vis_stdout, 02587 "# found dependent vars = %d (average = %g)\n", 02588 info->nFoundDependVars, info->averageFoundDependVars); 02589 fprintf(vis_stdout, "# tautologous subimage = %d\n", info->nEmptySubImage); 02590 fprintf(vis_stdout, "# split = %d, conjoin = %d, cubeSplit = %d\n", 02591 info->nSplits, info->nConjoins, info->nCubeSplits); 02592 } 02593 02594 02608 static void 02609 GetRecursionStatistics(ImgTfmInfo_t *info, int preFlag, int *nRecurs, 02610 int *nLeaves, int *nTurns, float *averageDepth, 02611 int *maxDepth, int *nDecomps, int *topDecomp, 02612 int *maxDecomp, float *averageDecomp) 02613 { 02614 if (preFlag) { 02615 *nRecurs = info->nRecursionB; 02616 *nLeaves = info->nLeavesB; 02617 *nTurns = info->nTurnsB; 02618 *averageDepth = info->averageDepthB; 02619 *maxDepth = info->maxDepthB; 02620 *nDecomps = 0; 02621 *topDecomp = 0; 02622 *maxDecomp = 0; 02623 *averageDecomp = 0.0; 02624 } else { 02625 *nRecurs = info->nRecursion; 02626 *nLeaves = info->nLeaves; 02627 *nTurns = info->nTurns; 02628 *averageDepth = info->averageDepth; 02629 *maxDepth = info->maxDepth; 02630 *nDecomps = info->nDecomps; 02631 *topDecomp = info->topDecomp; 02632 *maxDecomp = info->maxDecomp; 02633 *averageDecomp = info->averageDecomp; 02634 } 02635 } 02636 02637 02649 static int 02650 ReadSetIntValue(char *string, int l, int u, int defaultValue) 02651 { 02652 char *flagValue; 02653 int tmp; 02654 int value = defaultValue; 02655 02656 flagValue = Cmd_FlagReadByName(string); 02657 if (flagValue != NIL(char)) { 02658 sscanf(flagValue, "%d", &tmp); 02659 if (tmp >= l && (tmp <= u || u == 0)) 02660 value = tmp; 02661 else { 02662 fprintf(vis_stderr, 02663 "** tfm error: invalid value %d for %s[%d-%d]. **\n", tmp, string, 02664 l, u); 02665 } 02666 } 02667 02668 return(value); 02669 } 02670 02671 02683 static boolean 02684 ReadSetBooleanValue(char *string, boolean defaultValue) 02685 { 02686 char *flagValue; 02687 boolean value = defaultValue; 02688 02689 flagValue = Cmd_FlagReadByName(string); 02690 if (flagValue != NIL(char)) { 02691 if (strcmp(flagValue, "yes") == 0) 02692 value = TRUE; 02693 else if (strcmp(flagValue, "no") == 0) 02694 value = FALSE; 02695 else { 02696 fprintf(vis_stderr, 02697 "** tfm error: invalid value %s for %s[yes/no]. **\n", 02698 flagValue, string); 02699 } 02700 } 02701 02702 return(value); 02703 } 02704 02705 02718 static void 02719 FindIntermediateVarsRecursively(ImgTfmInfo_t *info, mdd_manager *mddManager, 02720 vertex_t *vertex, int mddId, 02721 st_table *vertexTable, array_t *vector, 02722 st_table *domainQuantifyVarMddIdTable, 02723 array_t *intermediateVarMddIdArray) 02724 { 02725 Mvf_Function_t *mvf; 02726 lsList faninEdges; 02727 lsGen gen; 02728 vertex_t *faninVertex; 02729 edge_t *faninEdge; 02730 array_t *varBddFunctionArray, *bddArray; 02731 int i; 02732 mdd_t *var, *func; 02733 ImgComponent_t *comp; 02734 02735 if (st_is_member(vertexTable, (char *)vertex)) 02736 return; 02737 st_insert(vertexTable, (char *)vertex, NIL(char)); 02738 if (mddId != -1) { /* This is not the next state function node */ 02739 /* There is an mdd variable associated with this vertex */ 02740 array_insert_last(int, intermediateVarMddIdArray, mddId); 02741 mvf = Part_VertexReadFunction(vertex); 02742 varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mddManager, mddId, mvf); 02743 bddArray = mdd_id_to_bdd_array(mddManager, mddId); 02744 assert(array_n(varBddFunctionArray) == array_n(bddArray)); 02745 for (i = 0; i < array_n(bddArray); i++) { 02746 var = array_fetch(mdd_t *, bddArray, i); 02747 func = array_fetch(mdd_t *, varBddFunctionArray, i); 02748 comp = ImgComponentAlloc(info); 02749 comp->var = var; 02750 comp->func = func; 02751 comp->intermediate = 1; 02752 ImgComponentGetSupport(comp); 02753 array_insert_last(ImgComponent_t *, vector, comp); 02754 } 02755 array_free(varBddFunctionArray); 02756 array_free(bddArray); 02757 } 02758 faninEdges = g_get_in_edges(vertex); 02759 if (lsLength(faninEdges) == 0) 02760 return; 02761 lsForEachItem(faninEdges, gen, faninEdge) { 02762 faninVertex = g_e_source(faninEdge); 02763 mddId = Part_VertexReadMddId(faninVertex); 02764 if (st_is_member(domainQuantifyVarMddIdTable, (char *)(long)mddId)) { 02765 /* This is either domain var or quantify var */ 02766 continue; 02767 } 02768 FindIntermediateVarsRecursively(info, mddManager, faninVertex, mddId, 02769 vertexTable, vector, 02770 domainQuantifyVarMddIdTable, 02771 intermediateVarMddIdArray); 02772 } 02773 } 02774 02775 02788 static void 02789 GetIntermediateRelationsRecursively(mdd_manager *mddManager, vertex_t *vertex, 02790 int mddId, st_table *vertexTable, 02791 array_t *relationArray, 02792 st_table *domainQuantifyVarMddIdTable, 02793 array_t *intermediateVarMddIdArray) 02794 { 02795 Mvf_Function_t *mvf; 02796 lsList faninEdges; 02797 lsGen gen; 02798 vertex_t *faninVertex; 02799 edge_t *faninEdge; 02800 array_t *varBddRelationArray; 02801 02802 if (st_is_member(vertexTable, (char *)vertex)) 02803 return; 02804 st_insert(vertexTable, (char *)vertex, NIL(char)); 02805 if (mddId != -1) { /* This is not the next state function node */ 02806 /* There is an mdd variable associated with this vertex */ 02807 array_insert_last(int, intermediateVarMddIdArray, mddId); 02808 mvf = Part_VertexReadFunction(vertex); 02809 varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, mddId, mvf); 02810 array_append(relationArray, varBddRelationArray); 02811 array_free(varBddRelationArray); 02812 } 02813 faninEdges = g_get_in_edges(vertex); 02814 if (lsLength(faninEdges) == 0) 02815 return; 02816 lsForEachItem(faninEdges, gen, faninEdge) { 02817 faninVertex = g_e_source(faninEdge); 02818 mddId = Part_VertexReadMddId(faninVertex); 02819 if (st_is_member(domainQuantifyVarMddIdTable, (char *)(long)mddId)) { 02820 /* This is either domain var or quantify var */ 02821 continue; 02822 } 02823 GetIntermediateRelationsRecursively(mddManager, faninVertex, mddId, 02824 vertexTable, relationArray, 02825 domainQuantifyVarMddIdTable, 02826 intermediateVarMddIdArray); 02827 } 02828 } 02829 02830 02844 static int 02845 CheckNondeterminism(Ntk_Network_t *network) 02846 { 02847 Ntk_Node_t *node; 02848 lsGen gen; 02849 Var_Variable_t *var; 02850 int numValues; 02851 02852 Ntk_NetworkForEachNode(network, gen, node) { 02853 var = Ntk_NodeReadVariable(node); 02854 numValues = Var_VariableReadNumValues(var); 02855 if (numValues > 2) { 02856 lsFinish(gen); 02857 return 1; 02858 } 02859 } 02860 return 0; 02861 } 02862 02863 02875 static array_t * 02876 TfmCreateBitVector(ImgTfmInfo_t *info, 02877 int composeIntermediateVars, int findIntermediateVars) 02878 { 02879 int i, j; 02880 array_t *vector; 02881 graph_t *mddNetwork; 02882 mdd_manager *mddManager; 02883 array_t *roots; 02884 array_t *rangeVarMddIdArray; 02885 int index; 02886 mdd_t *var; 02887 ImgComponent_t *comp; 02888 st_table *vertexTable; 02889 st_table *domainQuantifyVarMddIdTable; 02890 array_t *intermediateVarMddIdArray, *intermediateBddVars; 02891 int mddId; 02892 ImgFunctionData_t *functionData = info->functionData; 02893 02894 mddNetwork = functionData->mddNetwork; 02895 mddManager = Part_PartitionReadMddManager(mddNetwork); 02896 roots = functionData->roots; 02897 rangeVarMddIdArray = functionData->rangeVars; 02898 02899 if (findIntermediateVars) { 02900 vertexTable = st_init_table(st_ptrcmp, st_ptrhash); 02901 domainQuantifyVarMddIdTable = st_init_table(st_numcmp, st_numhash); 02902 intermediateVarMddIdArray = array_alloc(int, 0); 02903 arrayForEachItem(int, functionData->domainVars, i, mddId) { 02904 st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char)); 02905 } 02906 arrayForEachItem(int, functionData->quantifyVars, i, mddId) { 02907 st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char)); 02908 } 02909 } else { 02910 vertexTable = NIL(st_table); 02911 domainQuantifyVarMddIdTable = NIL(st_table); 02912 intermediateVarMddIdArray = NIL(array_t); 02913 } 02914 02915 vector = array_alloc(ImgComponent_t *, 0); 02916 /* 02917 * Iterate over the function of all the root nodes. 02918 */ 02919 for (i = 0; i < array_n(roots); i++) { 02920 mdd_t *func; 02921 char *nodeName = array_fetch(char*, roots, i); 02922 vertex_t *vertex = Part_PartitionFindVertexByName(mddNetwork, nodeName); 02923 Mvf_Function_t *mvf = Part_VertexReadFunction(vertex); 02924 int mddId = array_fetch(int, rangeVarMddIdArray, i); 02925 array_t *varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mddManager, 02926 mddId, mvf); 02927 array_t *bddArray = mdd_id_to_bdd_array(mddManager, mddId); 02928 02929 assert(array_n(varBddFunctionArray) == array_n(bddArray)); 02930 if (info->option->debug) { 02931 mdd_t *rel1, *rel2; 02932 array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, 02933 mddId, 02934 mvf); 02935 for (j = 0; j < array_n(bddArray); j++) { 02936 var = array_fetch(mdd_t *, bddArray, j); 02937 func = array_fetch(mdd_t *, varBddFunctionArray, j); 02938 rel1 = array_fetch(mdd_t *, varBddRelationArray, j); 02939 rel2 = mdd_xnor(var, func); 02940 if (!mdd_equal(rel1, rel2)) { 02941 if (mdd_lequal(rel1, rel2, 1, 1)) 02942 fprintf(vis_stdout, "** %d(%d): rel < funcRel\n", i, j); 02943 else if (mdd_lequal(rel2, rel1, 1, 1)) 02944 fprintf(vis_stdout, "** %d(%d): rel > funcRel\n", i, j); 02945 else 02946 fprintf(vis_stdout, "** %d(%d): rel != funcRel\n", i, j); 02947 } 02948 mdd_free(rel1); 02949 mdd_free(rel2); 02950 } 02951 02952 array_free(varBddRelationArray); 02953 } 02954 for (j = 0; j < array_n(bddArray); j++) { 02955 var = array_fetch(mdd_t *, bddArray, j); 02956 func = array_fetch(mdd_t *, varBddFunctionArray, j); 02957 if (array_n(bddArray) == 1 && bdd_is_tautology(func, 1)) { 02958 array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, 02959 mddId, mvf); 02960 mdd_t *relation = array_fetch(mdd_t *, varBddRelationArray, 0); 02961 /* non-deterministic constant */ 02962 if (bdd_is_tautology(relation, 1)) { 02963 mdd_array_free(varBddRelationArray); 02964 mdd_free(func); 02965 break; 02966 } 02967 mdd_array_free(varBddRelationArray); 02968 } 02969 comp = ImgComponentAlloc(info); 02970 comp->var = ImgSubstitute(var, functionData, Img_R2D_c); 02971 if (composeIntermediateVars) { 02972 comp->func = Img_ComposeIntermediateNodes(functionData->mddNetwork, 02973 func, functionData->domainVars, functionData->rangeVars, 02974 functionData->quantifyVars); 02975 mdd_free(func); 02976 } else 02977 comp->func = func; 02978 ImgComponentGetSupport(comp); 02979 array_insert_last(ImgComponent_t *, vector, comp); 02980 } 02981 if (findIntermediateVars) { 02982 int n1, n2; 02983 02984 n1 = array_n(vector); 02985 FindIntermediateVarsRecursively(info, mddManager, vertex, -1, 02986 vertexTable, vector, 02987 domainQuantifyVarMddIdTable, 02988 intermediateVarMddIdArray); 02989 n2 = array_n(vector); 02990 info->nIntermediateVars += n2 - n1; 02991 } 02992 array_free(varBddFunctionArray); 02993 mdd_array_free(bddArray); 02994 } 02995 if (findIntermediateVars) { 02996 int nonExistFlag; 02997 02998 /* checks whether intermediate variables are already found */ 02999 if (info->intermediateVarsTable && info->intermediateBddVars && 03000 info->newQuantifyBddVars) { 03001 nonExistFlag = 0; 03002 } else { 03003 assert(!info->intermediateVarsTable); 03004 assert(!info->intermediateBddVars); 03005 assert(!info->newQuantifyBddVars); 03006 nonExistFlag = 1; 03007 } 03008 03009 if (info->option->verbosity) { 03010 (void)fprintf(vis_stdout, "** img info: %d intermediate variables\n", 03011 info->nIntermediateVars); 03012 } 03013 st_free_table(vertexTable); 03014 st_free_table(domainQuantifyVarMddIdTable); 03015 if (nonExistFlag) { 03016 intermediateBddVars = mdd_id_array_to_bdd_array(mddManager, 03017 intermediateVarMddIdArray); 03018 } else 03019 intermediateBddVars = NIL(array_t); 03020 array_free(intermediateVarMddIdArray); 03021 if (nonExistFlag) { 03022 info->intermediateVarsTable = st_init_table(st_numcmp, st_numhash); 03023 for (i = 0; i < array_n(intermediateBddVars); i++) { 03024 var = array_fetch(mdd_t *, intermediateBddVars, i); 03025 index = (int)bdd_top_var_id(var); 03026 st_insert(info->intermediateVarsTable, (char *)(long)index, NIL(char)); 03027 } 03028 info->newQuantifyBddVars = mdd_array_duplicate( 03029 functionData->quantifyBddVars); 03030 for (i = 0; i < array_n(intermediateBddVars); i++) { 03031 var = array_fetch(mdd_t *, intermediateBddVars, i); 03032 array_insert_last(mdd_t *, info->newQuantifyBddVars, mdd_dup(var)); 03033 } 03034 info->intermediateBddVars = intermediateBddVars; 03035 } 03036 } 03037 03038 return(vector); 03039 } 03040 03041 03053 static array_t * 03054 TfmCreateBitRelationArray(ImgTfmInfo_t *info, 03055 int composeIntermediateVars, int findIntermediateVars) 03056 { 03057 array_t *bddRelationArray = array_alloc(mdd_t*, 0); 03058 ImgFunctionData_t *functionData = info->functionData; 03059 array_t *domainVarMddIdArray = functionData->domainVars; 03060 array_t *rangeVarMddIdArray = functionData->rangeVars; 03061 array_t *quantifyVarMddIdArray = functionData->quantifyVars; 03062 graph_t *mddNetwork = functionData->mddNetwork; 03063 array_t *roots = functionData->roots; 03064 int i, j, n1, n2, mddId, nIntermediateVars = 0; 03065 mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork); 03066 st_table *vertexTable = st_init_table(st_ptrcmp, st_ptrhash); 03067 st_table *domainQuantifyVarMddIdTable = 03068 st_init_table(st_numcmp, st_numhash); 03069 char *nodeName; 03070 mdd_t *relation, *composedRelation; 03071 array_t *intermediateVarMddIdArray, *intermediateBddVars; 03072 int index; 03073 mdd_t *var; 03074 03075 if (findIntermediateVars) 03076 intermediateVarMddIdArray = array_alloc(int, 0); 03077 else 03078 intermediateVarMddIdArray = NIL(array_t); 03079 03080 arrayForEachItem(int, domainVarMddIdArray, i, mddId) { 03081 st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char)); 03082 } 03083 arrayForEachItem(int, quantifyVarMddIdArray, i, mddId) { 03084 st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char)); 03085 } 03086 03087 arrayForEachItem(char *, roots, i, nodeName) { 03088 vertex_t *vertex = Part_PartitionFindVertexByName(mddNetwork, nodeName); 03089 Mvf_Function_t *mvf = Part_VertexReadFunction(vertex); 03090 int mddId = array_fetch(int, rangeVarMddIdArray, i); 03091 03092 array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, 03093 mddId, mvf); 03094 if (composeIntermediateVars) { 03095 for (j = 0; j < array_n(varBddRelationArray); j++) { 03096 relation = array_fetch(mdd_t *, varBddRelationArray, j); 03097 composedRelation = Img_ComposeIntermediateNodes( 03098 functionData->mddNetwork, relation, functionData->domainVars, 03099 functionData->rangeVars, functionData->quantifyVars); 03100 mdd_free(relation); 03101 array_insert(mdd_t *, varBddRelationArray, j, composedRelation); 03102 } 03103 03104 array_append(bddRelationArray, varBddRelationArray); 03105 array_free(varBddRelationArray); 03106 } else { 03107 array_append(bddRelationArray, varBddRelationArray); 03108 array_free(varBddRelationArray); 03109 03110 if (findIntermediateVars) { 03111 if (info->option->verbosity) 03112 n1 = array_n(bddRelationArray); 03113 GetIntermediateRelationsRecursively(mddManager, vertex, -1, vertexTable, 03114 bddRelationArray, 03115 domainQuantifyVarMddIdTable, 03116 intermediateVarMddIdArray); 03117 if (info->option->verbosity) { 03118 n2 = array_n(bddRelationArray); 03119 nIntermediateVars += n2 - n1; 03120 } 03121 } 03122 } 03123 } 03124 03125 st_free_table(vertexTable); 03126 st_free_table(domainQuantifyVarMddIdTable); 03127 if (findIntermediateVars) { 03128 int nonExistFlag; 03129 03130 /* checks whether intermediate variables are already found */ 03131 if (info->intermediateVarsTable && info->intermediateBddVars && 03132 info->newQuantifyBddVars) { 03133 nonExistFlag = 0; 03134 } else { 03135 assert(!info->intermediateVarsTable); 03136 assert(!info->intermediateBddVars); 03137 assert(!info->newQuantifyBddVars); 03138 nonExistFlag = 1; 03139 } 03140 03141 if (info->option->verbosity) { 03142 (void)fprintf(vis_stdout, "** img info: %d intermediate variables\n", 03143 info->nIntermediateVars); 03144 } 03145 if (nonExistFlag) { 03146 intermediateBddVars = mdd_id_array_to_bdd_array(mddManager, 03147 intermediateVarMddIdArray); 03148 } else 03149 intermediateBddVars = NIL(array_t); 03150 array_free(intermediateVarMddIdArray); 03151 if (nonExistFlag) { 03152 info->intermediateVarsTable = st_init_table(st_numcmp, st_numhash); 03153 for (i = 0; i < array_n(intermediateBddVars); i++) { 03154 var = array_fetch(mdd_t *, intermediateBddVars, i); 03155 index = (int)bdd_top_var_id(var); 03156 st_insert(info->intermediateVarsTable, (char *)(long)index, NIL(char)); 03157 } 03158 info->newQuantifyBddVars = mdd_array_duplicate( 03159 functionData->quantifyBddVars); 03160 for (i = 0; i < array_n(intermediateBddVars); i++) { 03161 var = array_fetch(mdd_t *, intermediateBddVars, i); 03162 array_insert_last(mdd_t *, info->newQuantifyBddVars, mdd_dup(var)); 03163 } 03164 info->intermediateBddVars = intermediateBddVars; 03165 } 03166 } 03167 return(bddRelationArray); 03168 } 03169 03170 03182 static void 03183 TfmSetupPartialTransitionRelation(ImgTfmInfo_t *info, 03184 array_t **partialRelationArray) 03185 { 03186 int i, id; 03187 mdd_t *var, *relation; 03188 ImgComponent_t *comp, *newComp; 03189 array_t *partialVector; 03190 ImgFunctionData_t *functionData = info->functionData; 03191 03192 if (!info->buildPartialTR) 03193 return; 03194 03195 info->partialBddVars = ChoosePartialVars(info, info->fullVector, 03196 info->option->nPartialVars, 03197 info->option->partialMethod); 03198 info->partialVarFlag = ALLOC(char, info->nVars); 03199 memset(info->partialVarFlag, 0, sizeof(char) * info->nVars); 03200 for (i = 0; i < array_n(info->partialBddVars); i++) { 03201 var = array_fetch(mdd_t *, info->partialBddVars, i); 03202 id = (int)bdd_top_var_id(var); 03203 info->partialVarFlag[id] = 1; 03204 } 03205 03206 partialVector = array_alloc(ImgComponent_t *, 0); 03207 if (partialRelationArray) 03208 *partialRelationArray = array_alloc(mdd_t *, 0); 03209 03210 for (i = 0; i < array_n(info->fullVector); i++) { 03211 comp = array_fetch(ImgComponent_t *, info->fullVector, i); 03212 id = (int)bdd_top_var_id(comp->var); 03213 if (info->partialVarFlag[id]) { 03214 newComp = ImgComponentCopy(info, comp); 03215 array_insert_last(ImgComponent_t *, partialVector, newComp); 03216 03217 if (newComp->intermediate) 03218 relation = mdd_xnor(newComp->var, newComp->func); 03219 else { 03220 var = ImgSubstitute(newComp->var, functionData, Img_D2R_c); 03221 relation = mdd_xnor(var, newComp->func); 03222 mdd_free(var); 03223 } 03224 array_insert_last(mdd_t *, *partialRelationArray, relation); 03225 } 03226 } 03227 03228 info->vector = partialVector; 03229 } 03230 03231 03243 static void 03244 TfmBuildRelationArray(ImgTfmInfo_t *info, ImgFunctionData_t *functionData, 03245 array_t *bitRelationArray, 03246 Img_DirectionType directionType, int writeMatrix) 03247 { 03248 int i; 03249 mdd_t *var, *relation; 03250 array_t *relationArray; 03251 ImgComponent_t *comp; 03252 int id; 03253 array_t *domainVarBddArray, *quantifyVarBddArray; 03254 mdd_t *one, *res1, *res2; 03255 char filename[20]; 03256 int composeIntermediateVars, findIntermediateVars; 03257 03258 if ((info->buildTR == 1 && info->option->synchronizeTr) || 03259 info->buildPartialTR) { 03260 relationArray = array_alloc(mdd_t *, 0); 03261 if (info->fullVector) { 03262 for (i = 0; i < array_n(info->fullVector); i++) { 03263 comp = array_fetch(ImgComponent_t *, info->fullVector, i); 03264 id = (int)bdd_top_var_id(comp->var); 03265 if (!info->partialVarFlag[id]) { 03266 if (comp->intermediate) 03267 relation = mdd_xnor(comp->var, comp->func); 03268 else { 03269 var = ImgSubstitute(comp->var, functionData, Img_D2R_c); 03270 relation = mdd_xnor(var, comp->func); 03271 mdd_free(var); 03272 } 03273 array_insert_last(mdd_t *, relationArray, relation); 03274 } 03275 } 03276 } else { 03277 for (i = 0; i < array_n(info->vector); i++) { 03278 comp = array_fetch(ImgComponent_t *, info->vector, i); 03279 if (comp->intermediate) 03280 relation = mdd_xnor(comp->var, comp->func); 03281 else { 03282 var = ImgSubstitute(comp->var, functionData, Img_D2R_c); 03283 relation = mdd_xnor(var, comp->func); 03284 mdd_free(var); 03285 } 03286 array_insert_last(mdd_t *, relationArray, relation); 03287 } 03288 } 03289 03290 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 03291 if (info->imgKeepPiInTr) { 03292 if (info->intermediateBddVars) 03293 quantifyVarBddArray = info->intermediateBddVars; 03294 else 03295 quantifyVarBddArray = array_alloc(mdd_t *, 0); 03296 domainVarBddArray = array_join(info->domainVarBddArray, 03297 info->quantifyVarBddArray); 03298 } else { 03299 if (info->newQuantifyBddVars) 03300 quantifyVarBddArray = info->newQuantifyBddVars; 03301 else 03302 quantifyVarBddArray = info->quantifyVarBddArray; 03303 domainVarBddArray = info->domainVarBddArray; 03304 } 03305 info->fwdClusteredRelationArray = ImgClusterRelationArray( 03306 info->manager, info->functionData, 03307 info->option->trMethod, Img_Forward_c, info->trmOption, 03308 relationArray, domainVarBddArray, quantifyVarBddArray, 03309 info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray, 03310 &info->fwdSmoothVarCubeArray, 0); 03311 if (writeMatrix && info->option->writeSupportMatrix == 3) { 03312 sprintf(filename, "support%d.mat", info->option->supportFileCount++); 03313 ImgWriteSupportMatrix(info, info->vector, 03314 info->fwdClusteredRelationArray, filename); 03315 } else if (writeMatrix && info->option->writeSupportMatrix == 2) { 03316 sprintf(filename, "support%d.mat", info->option->supportFileCount++); 03317 ImgWriteSupportMatrix(info, NIL(array_t), 03318 info->fwdClusteredRelationArray, filename); 03319 } 03320 if (info->imgKeepPiInTr) { 03321 if (!info->intermediateBddVars) 03322 array_free(quantifyVarBddArray); 03323 array_free(domainVarBddArray); 03324 } 03325 if (info->option->checkEquivalence && (!info->fullVector)) { 03326 assert(ImgCheckEquivalence(info, info->vector, 03327 info->fwdClusteredRelationArray, 03328 NIL(mdd_t), NIL(mdd_t), 0)); 03329 } 03330 if (info->option->debug) { 03331 one = mdd_one(info->manager); 03332 if (info->fullVector) { 03333 res1 = ImgImageByHybrid(info, info->fullVector, one); 03334 res2 = ImgImageByHybridWithStaticSplit(info, info->vector, one, 03335 info->fwdClusteredRelationArray, 03336 NIL(mdd_t), NIL(mdd_t)); 03337 } else { 03338 res1 = ImgImageByHybrid(info, info->vector, one); 03339 res2 = ImgImageByHybridWithStaticSplit(info, NIL(array_t), one, 03340 info->fwdClusteredRelationArray, 03341 NIL(mdd_t), NIL(mdd_t)); 03342 } 03343 assert(mdd_equal(res1, res2)); 03344 mdd_free(one); 03345 mdd_free(res1); 03346 mdd_free(res2); 03347 } 03348 } 03349 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 03350 if (info->preKeepPiInTr) { 03351 if (info->intermediateBddVars) 03352 quantifyVarBddArray = info->intermediateBddVars; 03353 else 03354 quantifyVarBddArray = array_alloc(mdd_t *, 0); 03355 domainVarBddArray = array_join(info->domainVarBddArray, 03356 info->quantifyVarBddArray); 03357 } else { 03358 if (info->newQuantifyBddVars) 03359 quantifyVarBddArray = info->newQuantifyBddVars; 03360 else 03361 quantifyVarBddArray = info->quantifyVarBddArray; 03362 domainVarBddArray = info->domainVarBddArray; 03363 } 03364 info->bwdClusteredRelationArray = ImgClusterRelationArray( 03365 info->manager, info->functionData, 03366 info->option->trMethod, Img_Backward_c, info->trmOption, 03367 relationArray, domainVarBddArray, quantifyVarBddArray, 03368 info->rangeVarBddArray, &info->bwdArraySmoothVarBddArray, 03369 &info->bwdSmoothVarCubeArray, 0); 03370 if (writeMatrix && info->option->writeSupportMatrix == 3) { 03371 sprintf(filename, "support%d.mat", info->option->supportFileCount++); 03372 ImgWriteSupportMatrix(info, info->vector, 03373 info->bwdClusteredRelationArray, filename); 03374 } else if (writeMatrix && info->option->writeSupportMatrix == 2) { 03375 sprintf(filename, "support%d.mat", info->option->supportFileCount++); 03376 ImgWriteSupportMatrix(info, NIL(array_t), 03377 info->bwdClusteredRelationArray, filename); 03378 } 03379 if (info->preKeepPiInTr) { 03380 if (!info->intermediateBddVars) 03381 array_free(quantifyVarBddArray); 03382 array_free(domainVarBddArray); 03383 } 03384 if (info->option->checkEquivalence && (!info->fullVector)) { 03385 assert(ImgCheckEquivalence(info, info->vector, 03386 info->bwdClusteredRelationArray, 03387 NIL(mdd_t), NIL(mdd_t), 1)); 03388 } 03389 if (info->option->debug) { 03390 one = mdd_one(info->manager); 03391 if (info->fullVector) { 03392 res1 = ImgImageByHybrid(info, info->fullVector, one); 03393 res2 = ImgImageByHybridWithStaticSplit(info, info->vector, one, 03394 info->bwdClusteredRelationArray, 03395 NIL(mdd_t), NIL(mdd_t)); 03396 } else { 03397 res1 = ImgImageByHybrid(info, info->vector, one); 03398 res2 = ImgImageByHybridWithStaticSplit(info, NIL(array_t), one, 03399 info->bwdClusteredRelationArray, 03400 NIL(mdd_t), NIL(mdd_t)); 03401 } 03402 assert(mdd_equal(res1, res2)); 03403 mdd_free(one); 03404 mdd_free(res1); 03405 mdd_free(res2); 03406 } 03407 } 03408 03409 mdd_array_free(relationArray); 03410 } else { 03411 graph_t *mddNetwork = functionData->mddNetwork; 03412 03413 if (bitRelationArray) 03414 relationArray = bitRelationArray; 03415 else { 03416 if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c && 03417 info->nVars != info->nRealVars) { 03418 if (info->option->composeIntermediateVars) { 03419 composeIntermediateVars = 1; 03420 findIntermediateVars = 0; 03421 } else { 03422 composeIntermediateVars = 0; 03423 findIntermediateVars = 1; 03424 } 03425 } else { 03426 composeIntermediateVars = 0; 03427 findIntermediateVars = 0; 03428 } 03429 03430 relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars, 03431 findIntermediateVars); 03432 } 03433 03434 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 03435 if (info->imgKeepPiInTr) { 03436 if (info->intermediateBddVars) 03437 quantifyVarBddArray = info->intermediateBddVars; 03438 else 03439 quantifyVarBddArray = array_alloc(mdd_t *, 0); 03440 domainVarBddArray = array_join(info->domainVarBddArray, 03441 info->quantifyVarBddArray); 03442 } else { 03443 if (info->newQuantifyBddVars) 03444 quantifyVarBddArray = info->newQuantifyBddVars; 03445 else 03446 quantifyVarBddArray = info->quantifyVarBddArray; 03447 domainVarBddArray = info->domainVarBddArray; 03448 } 03449 info->fwdClusteredRelationArray = ImgClusterRelationArray( 03450 info->manager, info->functionData, info->option->trMethod, 03451 Img_Forward_c, info->trmOption, relationArray, 03452 domainVarBddArray, quantifyVarBddArray, 03453 info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray, 03454 &info->fwdSmoothVarCubeArray, 0); 03455 if (writeMatrix && info->option->writeSupportMatrix >= 2) { 03456 sprintf(filename, "support%d.mat", info->option->supportFileCount++); 03457 ImgWriteSupportMatrix(info, NIL(array_t), 03458 info->fwdClusteredRelationArray, filename); 03459 } 03460 if (info->imgKeepPiInTr) { 03461 if (!info->intermediateBddVars) 03462 array_free(quantifyVarBddArray); 03463 array_free(domainVarBddArray); 03464 } 03465 } 03466 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 03467 if (info->preKeepPiInTr) { 03468 if (info->intermediateBddVars) 03469 quantifyVarBddArray = info->intermediateBddVars; 03470 else 03471 quantifyVarBddArray = array_alloc(mdd_t *, 0); 03472 domainVarBddArray = array_join(info->domainVarBddArray, 03473 info->quantifyVarBddArray); 03474 } else { 03475 if (info->newQuantifyBddVars) 03476 quantifyVarBddArray = info->newQuantifyBddVars; 03477 else 03478 quantifyVarBddArray = info->quantifyVarBddArray; 03479 domainVarBddArray = info->domainVarBddArray; 03480 } 03481 info->bwdClusteredRelationArray = ImgClusterRelationArray( 03482 info->manager, info->functionData, 03483 info->option->trMethod, Img_Backward_c, info->trmOption, 03484 relationArray, domainVarBddArray, quantifyVarBddArray, 03485 info->rangeVarBddArray, &info->bwdArraySmoothVarBddArray, 03486 &info->bwdSmoothVarCubeArray, 0); 03487 if (writeMatrix && info->option->writeSupportMatrix >= 2) { 03488 sprintf(filename, "support%d.mat", info->option->supportFileCount++); 03489 ImgWriteSupportMatrix(info, NIL(array_t), 03490 info->bwdClusteredRelationArray, filename); 03491 } 03492 if (info->preKeepPiInTr) { 03493 if (!info->intermediateBddVars) 03494 array_free(quantifyVarBddArray); 03495 array_free(domainVarBddArray); 03496 } 03497 } 03498 03499 if (!bitRelationArray) 03500 mdd_array_free(relationArray); 03501 } 03502 } 03503 03504 03516 static void 03517 RebuildTransitionRelation(ImgTfmInfo_t *info, Img_DirectionType directionType) 03518 { 03519 int i; 03520 mdd_t *var, *relation; 03521 ImgComponent_t *comp; 03522 array_t *relationArray; 03523 array_t *quantifyVarBddArray, *domainVarBddArray; 03524 03525 relationArray = array_alloc(mdd_t *, 0); 03526 03527 for (i = 0; i < array_n(info->vector); i++) { 03528 comp = array_fetch(ImgComponent_t *, info->vector, i); 03529 var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); 03530 relation = mdd_xnor(var, comp->func); 03531 array_insert_last(mdd_t *, relationArray, relation); 03532 mdd_free(var); 03533 } 03534 03535 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 03536 mdd_array_free(info->fwdClusteredRelationArray); 03537 if (info->imgKeepPiInTr) { 03538 if (info->intermediateBddVars) 03539 quantifyVarBddArray = info->intermediateBddVars; 03540 else 03541 quantifyVarBddArray = array_alloc(mdd_t *, 0); 03542 domainVarBddArray = array_join(info->domainVarBddArray, 03543 info->quantifyVarBddArray); 03544 } else { 03545 if (info->newQuantifyBddVars) 03546 quantifyVarBddArray = info->newQuantifyBddVars; 03547 else 03548 quantifyVarBddArray = info->quantifyVarBddArray; 03549 domainVarBddArray = info->domainVarBddArray; 03550 } 03551 info->fwdClusteredRelationArray = ImgClusterRelationArray( 03552 info->manager, info->functionData, info->option->trMethod, 03553 Img_Forward_c, info->trmOption, relationArray, 03554 domainVarBddArray, quantifyVarBddArray, 03555 info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray, 03556 &info->fwdSmoothVarCubeArray, 0); 03557 if (info->imgKeepPiInTr) { 03558 if (!info->intermediateBddVars) 03559 array_free(quantifyVarBddArray); 03560 array_free(domainVarBddArray); 03561 } 03562 } 03563 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 03564 mdd_array_free(info->bwdClusteredRelationArray); 03565 if (info->preKeepPiInTr) { 03566 if (info->intermediateBddVars) 03567 quantifyVarBddArray = info->intermediateBddVars; 03568 else 03569 quantifyVarBddArray = array_alloc(mdd_t *, 0); 03570 domainVarBddArray = array_join(info->domainVarBddArray, 03571 info->quantifyVarBddArray); 03572 } else { 03573 if (info->newQuantifyBddVars) 03574 quantifyVarBddArray = info->newQuantifyBddVars; 03575 else 03576 quantifyVarBddArray = info->quantifyVarBddArray; 03577 domainVarBddArray = info->domainVarBddArray; 03578 } 03579 info->bwdClusteredRelationArray = ImgClusterRelationArray( 03580 info->manager, info->functionData, 03581 info->option->trMethod, Img_Backward_c, info->trmOption, 03582 relationArray, domainVarBddArray, quantifyVarBddArray, 03583 info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray, 03584 &info->fwdSmoothVarCubeArray, 0); 03585 if (info->preKeepPiInTr) { 03586 if (!info->intermediateBddVars) 03587 array_free(quantifyVarBddArray); 03588 array_free(domainVarBddArray); 03589 } 03590 } 03591 03592 mdd_array_free(relationArray); 03593 } 03594 03595 03605 static void 03606 MinimizeTransitionFunction(array_t *vector, array_t *relationArray, 03607 mdd_t *constrain, Img_MinimizeType minimizeMethod, 03608 int printStatus) 03609 { 03610 int i; 03611 bdd_t *relation, *simplifiedRelation, *simplifiedFunc; 03612 long sizeConstrain = 0, size = 0; 03613 ImgComponent_t *comp; 03614 03615 if (bdd_is_tautology(constrain, 1)) 03616 return; 03617 03618 if (vector) { 03619 if (printStatus) { 03620 size = ImgVectorBddSize(vector); 03621 sizeConstrain = bdd_size(constrain); 03622 } 03623 03624 arrayForEachItem(ImgComponent_t *, vector, i, comp) { 03625 simplifiedFunc = Img_MinimizeImage(comp->func, constrain, minimizeMethod, 03626 TRUE); 03627 if (printStatus == 2) { 03628 (void)fprintf(vis_stdout, 03629 "IMG Info: minimized function %d | %ld => %d in component %d\n", 03630 bdd_size(comp->func), sizeConstrain, 03631 bdd_size(simplifiedFunc), i); 03632 } 03633 mdd_free(comp->func); 03634 comp->func = simplifiedFunc; 03635 } 03636 03637 if (printStatus) { 03638 (void) fprintf(vis_stdout, 03639 "IMG Info: minimized function [%ld | %ld => %ld] with %d components\n", 03640 size, sizeConstrain, 03641 ImgVectorBddSize(vector), array_n(vector)); 03642 } 03643 } 03644 03645 if (relationArray) { 03646 if (printStatus) { 03647 size = bdd_size_multiple(relationArray); 03648 sizeConstrain = bdd_size(constrain); 03649 } 03650 03651 arrayForEachItem(bdd_t*, relationArray, i, relation) { 03652 simplifiedRelation = Img_MinimizeImage(relation, constrain, 03653 minimizeMethod, TRUE); 03654 if (printStatus == 2) { 03655 (void)fprintf(vis_stdout, 03656 "IMG Info: minimized relation %d | %ld => %d in component %d\n", 03657 bdd_size(relation), sizeConstrain, 03658 bdd_size(simplifiedRelation), i); 03659 } 03660 mdd_free(relation); 03661 array_insert(bdd_t *, relationArray, i, simplifiedRelation); 03662 } 03663 03664 if (printStatus) { 03665 (void) fprintf(vis_stdout, 03666 "IMG Info: minimized relation [%ld | %ld => %ld] with %d components\n", 03667 size, sizeConstrain, 03668 bdd_size_multiple(relationArray), array_n(relationArray)); 03669 } 03670 } 03671 } 03672 03673 03683 static void 03684 AddDontCareToTransitionFunction(array_t *vector, array_t *relationArray, 03685 mdd_t *constrain, 03686 Img_MinimizeType minimizeMethod, 03687 int printStatus) 03688 { 03689 int i; 03690 bdd_t *relation, *simplifiedRelation, *simplifiedFunc; 03691 long sizeConstrain = 0, size = 0; 03692 ImgComponent_t *comp; 03693 03694 if (bdd_is_tautology(constrain, 1)) 03695 return; 03696 03697 if (vector) { 03698 if (printStatus) { 03699 size = ImgVectorBddSize(vector); 03700 sizeConstrain = bdd_size(constrain); 03701 } 03702 03703 arrayForEachItem(ImgComponent_t *, vector, i, comp) { 03704 simplifiedFunc = Img_AddDontCareToImage(comp->func, constrain, 03705 minimizeMethod); 03706 if (printStatus == 2) { 03707 (void)fprintf(vis_stdout, 03708 "IMG Info: minimized function %d | %ld => %d in component %d\n", 03709 bdd_size(comp->func), sizeConstrain, 03710 bdd_size(simplifiedFunc), i); 03711 } 03712 mdd_free(comp->func); 03713 comp->func = simplifiedFunc; 03714 } 03715 03716 if (printStatus) { 03717 (void) fprintf(vis_stdout, 03718 "IMG Info: minimized function [%ld | %ld => %ld] with %d components\n", 03719 size, sizeConstrain, 03720 ImgVectorBddSize(vector), array_n(vector)); 03721 } 03722 } 03723 03724 if (relationArray) { 03725 if (printStatus) { 03726 size = bdd_size_multiple(relationArray); 03727 sizeConstrain = bdd_size(constrain); 03728 } 03729 03730 arrayForEachItem(bdd_t*, relationArray, i, relation) { 03731 simplifiedRelation = Img_AddDontCareToImage(relation, constrain, 03732 minimizeMethod); 03733 if (printStatus == 2) { 03734 (void)fprintf(vis_stdout, 03735 "IMG Info: minimized relation %d | %ld => %d in component %d\n", 03736 bdd_size(relation), sizeConstrain, 03737 bdd_size(simplifiedRelation), i); 03738 } 03739 mdd_free(relation); 03740 array_insert(bdd_t *, relationArray, i, simplifiedRelation); 03741 } 03742 03743 if (printStatus) { 03744 (void) fprintf(vis_stdout, 03745 "IMG Info: minimized relation [%ld | %ld => %ld] with %d components\n", 03746 size, sizeConstrain, 03747 bdd_size_multiple(relationArray), array_n(relationArray)); 03748 } 03749 } 03750 }
1.7.3