- Generated on Wed Oct 12 2011 00:34:49 for VIS by
1.7.3
|
VIS
|
00001 00057 #include "imgInt.h" 00058 00059 static char rcsid[] UNUSED = "$Id: imgUtil.c,v 1.74 2005/05/14 21:08:32 jinh Exp $"; 00060 00061 /*---------------------------------------------------------------------------*/ 00062 /* Variable declarations */ 00063 /*---------------------------------------------------------------------------*/ 00064 00065 static int nImgComps = 0; /* number of image computations */ 00066 static int nPreComps = 0; /* number of pre-image computations */ 00067 00070 /*---------------------------------------------------------------------------*/ 00071 /* Static function prototypes */ 00072 /*---------------------------------------------------------------------------*/ 00073 00074 static int CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t *domainVarMddIdArray, array_t *quantifyVarMddIdArray); 00075 00079 /*---------------------------------------------------------------------------*/ 00080 /* Definition of exported functions */ 00081 /*---------------------------------------------------------------------------*/ 00082 Img_OptimizeType Img_ImageInfoObtainOptimizeType(Img_ImageInfo_t * imageInfo); 00083 void Img_ImageInfoSetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo); 00084 void Img_ImageInfoResetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo); 00085 void Img_ImageInfoResetLinearComputeRange(Img_ImageInfo_t * imageInfo); 00086 void Img_ImageInfoSetLinearComputeRange(Img_ImageInfo_t * imageInfo); 00087 00088 00098 void 00099 Img_Init(void) 00100 { 00101 /* Set the default settings. */ 00102 00103 } 00104 00114 void 00115 Img_End(void) 00116 { 00117 /* Do Nothing. */ 00118 } 00119 00120 00134 Img_MethodType 00135 Img_UserSpecifiedMethod(void) 00136 { 00137 char *userSpecifiedMethod; 00138 00139 userSpecifiedMethod = Cmd_FlagReadByName("image_method"); 00140 00141 if (userSpecifiedMethod == NIL(char)) 00142 return IMGDEFAULT_METHOD; 00143 if (strcmp(userSpecifiedMethod, "monolithic") == 0) 00144 return Img_Monolithic_c; 00145 if (strcmp(userSpecifiedMethod, "tfm") == 0) 00146 return Img_Tfm_c; 00147 if (strcmp(userSpecifiedMethod, "hybrid") == 0) 00148 return Img_Hybrid_c; 00149 if (strcmp(userSpecifiedMethod, "iwls95") == 0) 00150 return Img_Iwls95_c; 00151 if (strcmp(userSpecifiedMethod, "mlp") == 0) 00152 return Img_Mlp_c; 00153 00154 fprintf(vis_stderr, "** img error: Unrecognized image_method %s", 00155 userSpecifiedMethod); 00156 fprintf(vis_stderr, "using default method.\n"); 00157 00158 return IMGDEFAULT_METHOD; 00159 } 00160 00200 Img_ImageInfo_t * 00201 Img_ImageInfoInitialize( 00202 Img_ImageInfo_t *imageInfo, 00203 graph_t * mddNetwork, 00204 array_t * roots, 00205 array_t * domainVars, 00206 array_t * rangeVars, 00207 array_t * quantifyVars, 00208 mdd_t * domainCube, 00209 mdd_t * rangeCube, 00210 mdd_t * quantifyCube, 00211 Ntk_Network_t * network, 00212 Img_MethodType methodType, 00213 Img_DirectionType directionType, 00214 int FAFWFlag, 00215 mdd_t *Winning) 00216 { 00217 char *flagValue; 00218 int verbosity; 00219 mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork); 00220 int updateFlag = 0; 00221 00222 assert(array_n(roots) != 0); 00223 00224 /* If it does not exist, create a new one and initialize fields appropriately 00225 */ 00226 if (imageInfo == NIL(Img_ImageInfo_t)) { 00227 imageInfo = ALLOC(Img_ImageInfo_t, 1); 00228 memset(imageInfo, 0, sizeof(Img_ImageInfo_t)); 00229 imageInfo->directionType = directionType; 00230 if (Cmd_FlagReadByName("linear_optimize")) 00231 imageInfo->linearOptimize = Opt_NS; 00232 00233 /* 00234 * Initialization of the function structure inside ImageInfo . 00235 * Since no duplication is needed, this process is not encapsulated 00236 * inside a static procedure. 00237 */ 00238 imageInfo->functionData.FAFWFlag = FAFWFlag; 00239 imageInfo->functionData.Winning = Winning; 00240 imageInfo->functionData.mddNetwork = mddNetwork; 00241 imageInfo->functionData.roots = roots; 00242 imageInfo->functionData.domainVars = domainVars; 00243 imageInfo->functionData.rangeVars = rangeVars; 00244 imageInfo->functionData.quantifyVars = quantifyVars; 00245 imageInfo->functionData.domainCube = domainCube; 00246 imageInfo->functionData.rangeCube = rangeCube; 00247 imageInfo->functionData.quantifyCube = quantifyCube; 00248 imageInfo->functionData.domainBddVars = mdd_id_array_to_bdd_array( 00249 mddManager, domainVars); 00250 imageInfo->functionData.rangeBddVars = mdd_id_array_to_bdd_array( 00251 mddManager, rangeVars); 00252 imageInfo->functionData.quantifyBddVars = mdd_id_array_to_bdd_array( 00253 mddManager, quantifyVars); 00254 if (bdd_get_package_name() == CUDD) { 00255 int i, nVars, idD, idR; 00256 mdd_t *varD, *varR; 00257 00258 nVars = bdd_num_vars(mddManager); 00259 imageInfo->functionData.permutD2R = ALLOC(int, sizeof(int) * nVars); 00260 imageInfo->functionData.permutR2D = ALLOC(int, sizeof(int) * nVars); 00261 for (i = 0; i < nVars; i++) { 00262 imageInfo->functionData.permutD2R[i] = i; 00263 imageInfo->functionData.permutR2D[i] = i; 00264 } 00265 nVars = array_n(imageInfo->functionData.rangeBddVars); 00266 for (i = 0; i < nVars; i++) { 00267 varD = array_fetch(bdd_t *, imageInfo->functionData.domainBddVars, i); 00268 varR = array_fetch(bdd_t *, imageInfo->functionData.rangeBddVars, i); 00269 idD = (int)bdd_top_var_id(varD); 00270 idR = (int)bdd_top_var_id(varR); 00271 imageInfo->functionData.permutD2R[idD] = idR; 00272 imageInfo->functionData.permutR2D[idR] = idD; 00273 } 00274 } else { 00275 imageInfo->functionData.permutD2R = NIL(int); 00276 imageInfo->functionData.permutR2D = NIL(int); 00277 } 00278 if (domainCube) 00279 imageInfo->functionData.createVarCubesFlag = 1; 00280 imageInfo->functionData.network = network; 00281 imageInfo->methodData = NIL(void); 00282 updateFlag = 1; 00283 } 00284 00285 /* 00286 * If methodType is default, use user-specified method if set. 00287 */ 00288 if (methodType == Img_Default_c) 00289 methodType = Img_UserSpecifiedMethod(); 00290 00291 /* If image_method changes, we need to free existing method data and 00292 * to update proper function calls. 00293 */ 00294 if (imageInfo->methodData) { 00295 if (imageInfo->methodType != methodType) { 00296 (*imageInfo->imageFreeProc)(imageInfo->methodData); 00297 imageInfo->methodData = NIL(void); 00298 updateFlag = 1; 00299 } 00300 } 00301 00302 if (updateFlag) { 00303 imageInfo->methodType = methodType; 00304 switch (methodType) { 00305 case Img_Monolithic_c: 00306 imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdMono; 00307 imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdMono; 00308 imageInfo->imageComputeFwdWithDomainVarsProc = 00309 ImgImageInfoComputeFwdWithDomainVarsMono; 00310 imageInfo->imageComputeBwdWithDomainVarsProc = 00311 ImgImageInfoComputeBwdWithDomainVarsMono; 00312 imageInfo->imageFreeProc = ImgImageInfoFreeMono; 00313 imageInfo->imagePrintMethodParamsProc = 00314 ImgImageInfoPrintMethodParamsMono; 00315 break; 00316 00317 case Img_Tfm_c: 00318 case Img_Hybrid_c: 00319 imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdTfm; 00320 imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdTfm; 00321 imageInfo->imageComputeFwdWithDomainVarsProc = 00322 ImgImageInfoComputeFwdWithDomainVarsTfm; 00323 imageInfo->imageComputeBwdWithDomainVarsProc = 00324 ImgImageInfoComputeBwdWithDomainVarsTfm; 00325 imageInfo->imageFreeProc = ImgImageInfoFreeTfm; 00326 imageInfo->imagePrintMethodParamsProc = 00327 ImgImageInfoPrintMethodParamsTfm; 00328 break; 00329 00330 case Img_Linear_Range_c: 00331 case Img_Iwls95_c: 00332 case Img_Mlp_c: 00333 case Img_Linear_c: 00334 imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdIwls95; 00335 imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdIwls95; 00336 imageInfo->imageComputeFwdWithDomainVarsProc = 00337 ImgImageInfoComputeFwdWithDomainVarsIwls95; 00338 imageInfo->imageComputeBwdWithDomainVarsProc = 00339 ImgImageInfoComputeBwdWithDomainVarsIwls95; 00340 imageInfo->imageFreeProc = ImgImageInfoFreeIwls95; 00341 imageInfo->imagePrintMethodParamsProc = 00342 ImgImageInfoPrintMethodParamsIwls95; 00343 break; 00344 00345 default: 00346 fail("** img error: Unexpected type when updating image method"); 00347 } 00348 imageInfo->fwdTrMinimizedFlag = FALSE; 00349 imageInfo->bwdTrMinimizedFlag = FALSE; 00350 imageInfo->printMinimizeStatus = 0; 00351 imageInfo->savedRelation = NIL(void); 00352 00353 flagValue = Cmd_FlagReadByName("image_verbosity"); 00354 if (flagValue != NIL(char)) { 00355 verbosity = atoi(flagValue); 00356 imageInfo->verbosity = verbosity; 00357 if (verbosity == 1) 00358 imageInfo->printMinimizeStatus = 1; 00359 else if (verbosity > 1) 00360 imageInfo->printMinimizeStatus = 2; 00361 } 00362 } 00363 00364 /* 00365 * Perform method-specific initialization of methodData. 00366 */ 00367 switch (imageInfo->methodType) { 00368 case Img_Monolithic_c: 00369 imageInfo->methodData = 00370 ImgImageInfoInitializeMono(imageInfo->methodData, 00371 &(imageInfo->functionData), 00372 directionType); 00373 break; 00374 case Img_Tfm_c: 00375 case Img_Hybrid_c: 00376 imageInfo->methodData = 00377 ImgImageInfoInitializeTfm(imageInfo->methodData, 00378 &(imageInfo->functionData), 00379 directionType, 00380 imageInfo->methodType); 00381 break; 00382 case Img_Iwls95_c: 00383 case Img_Mlp_c: 00384 case Img_Linear_c: 00385 case Img_Linear_Range_c: 00386 imageInfo->methodData = 00387 ImgImageInfoInitializeIwls95(imageInfo->methodData, 00388 &(imageInfo->functionData), 00389 directionType, 00390 imageInfo->methodType); 00391 break; 00392 00393 default: 00394 fail("IMG Error : Unexpected type when initalizing image method"); 00395 } 00396 return imageInfo; 00397 } 00398 00411 int Img_IsQuantifyCubeSame( 00412 Img_ImageInfo_t *imageInfo, 00413 mdd_t *quantifyCube) 00414 { 00415 if(imageInfo->functionData.quantifyCube == quantifyCube) 00416 return (1); 00417 else 00418 return(0); 00419 } 00420 00433 int Img_IsQuantifyArraySame( 00434 Img_ImageInfo_t *imageInfo, 00435 array_t *quantifyArray) 00436 { 00437 if(imageInfo->functionData.quantifyVars == quantifyArray) 00438 return (1); 00439 else 00440 return(0); 00441 } 00442 00456 void 00457 Img_ImageInfoUpdateVariables( 00458 Img_ImageInfo_t *imageInfo, 00459 graph_t * mddNetwork, 00460 array_t * domainVars, 00461 array_t * quantifyVars, 00462 mdd_t * domainCube, 00463 mdd_t * quantifyCube) 00464 { 00465 mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork); 00466 00467 imageInfo->functionData.domainVars = domainVars; 00468 imageInfo->functionData.quantifyVars = quantifyVars; 00469 imageInfo->functionData.domainCube = domainCube; 00470 imageInfo->functionData.quantifyCube = quantifyCube; 00471 mdd_array_free(imageInfo->functionData.domainBddVars); 00472 imageInfo->functionData.domainBddVars = mdd_id_array_to_bdd_array( 00473 mddManager, domainVars); 00474 mdd_array_free(imageInfo->functionData.quantifyBddVars); 00475 imageInfo->functionData.quantifyBddVars = mdd_id_array_to_bdd_array( 00476 mddManager, quantifyVars); 00477 } 00478 00479 00497 void 00498 Img_ImageAllowPartialImage(Img_ImageInfo_t *info, 00499 boolean value) 00500 { 00501 if (info->methodType == Img_Iwls95_c || info->methodType == Img_Mlp_c) { 00502 ImgImageAllowPartialImageIwls95(info->methodData, value); 00503 } 00504 return; 00505 } 00506 00516 void 00517 Img_ImagePrintPartialImageOptions(void) 00518 { 00519 ImgPrintPartialImageOptions(); 00520 return; 00521 } 00522 00523 00538 boolean 00539 Img_ImageWasPartial(Img_ImageInfo_t *info) 00540 { 00541 if (info->methodType == Img_Iwls95_c || info->methodType == Img_Mlp_c) 00542 return (ImgImageWasPartialIwls95(info->methodData)); 00543 else 00544 return FALSE; 00545 } 00546 00562 mdd_t * 00563 Img_ImageInfoComputeImageWithDomainVars( 00564 Img_ImageInfo_t * imageInfo, 00565 mdd_t * fromLowerBound, 00566 mdd_t * fromUpperBound, 00567 array_t * toCareSetArray) 00568 { 00569 mdd_t *image; 00570 mdd_manager *mddManager; 00571 long peakMem; 00572 int peakLiveNode; 00573 00574 if (mdd_is_tautology(fromLowerBound, 0)){ 00575 mddManager = Part_PartitionReadMddManager( 00576 imageInfo->functionData.mddNetwork); 00577 return (mdd_zero(mddManager)); 00578 } 00579 image = ((*imageInfo->imageComputeFwdWithDomainVarsProc) 00580 (&(imageInfo->functionData), imageInfo, 00581 fromLowerBound, fromUpperBound, toCareSetArray)); 00582 nImgComps++; 00583 00584 if (imageInfo->verbosity >= 2 && bdd_get_package_name() == CUDD) { 00585 mddManager = Part_PartitionReadMddManager( 00586 imageInfo->functionData.mddNetwork); 00587 peakMem = bdd_read_peak_memory(mddManager); 00588 peakLiveNode = bdd_read_peak_live_node(mddManager); 00589 fprintf(vis_stdout, "** img info: current peak memory = %ld\n", peakMem); 00590 fprintf(vis_stdout, "** img info: current peak live nodes = %d\n", 00591 peakLiveNode); 00592 } 00593 #ifndef NDEBUG 00594 assert(CheckImageValidity( 00595 Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork), 00596 image, 00597 imageInfo->functionData.rangeVars, 00598 imageInfo->functionData.quantifyVars)); 00599 #endif 00600 return(image); 00601 } 00602 00618 mdd_t * 00619 Img_ImageInfoComputeFwdWithDomainVars( 00620 Img_ImageInfo_t * imageInfo, 00621 mdd_t * fromLowerBound, 00622 mdd_t * fromUpperBound, 00623 mdd_t * toCareSet) 00624 { 00625 array_t *toCareSetArray; 00626 mdd_t *image; 00627 00628 toCareSetArray = array_alloc(mdd_t *, 0); 00629 array_insert(mdd_t *, toCareSetArray, 0, toCareSet); 00630 image = Img_ImageInfoComputeImageWithDomainVars(imageInfo, fromLowerBound, 00631 fromUpperBound, toCareSetArray); 00632 array_free(toCareSetArray); 00633 return(image); 00634 } 00635 00636 00658 mdd_t * 00659 Img_ImageInfoComputeFwd(Img_ImageInfo_t * imageInfo, 00660 mdd_t * fromLowerBound, 00661 mdd_t * fromUpperBound, 00662 array_t * toCareSetArray) 00663 { 00664 mdd_t *image; 00665 if (mdd_is_tautology(fromLowerBound, 0)){ 00666 mdd_manager *mddManager = Part_PartitionReadMddManager( 00667 imageInfo->functionData.mddNetwork); 00668 return (mdd_zero(mddManager)); 00669 } 00670 image = ((*imageInfo->imageComputeFwdProc) (&(imageInfo->functionData), 00671 imageInfo, 00672 fromLowerBound, 00673 fromUpperBound, 00674 toCareSetArray)); 00675 nImgComps++; 00676 #ifndef NDEBUG 00677 assert(CheckImageValidity( 00678 Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork), 00679 image, 00680 imageInfo->functionData.domainVars, 00681 imageInfo->functionData.quantifyVars)); 00682 #endif 00683 return image; 00684 } 00685 00686 00704 mdd_t * 00705 Img_ImageInfoComputePreImageWithDomainVars( 00706 Img_ImageInfo_t * imageInfo, 00707 mdd_t * fromLowerBound, 00708 mdd_t * fromUpperBound, 00709 array_t * toCareSetArray) 00710 { 00711 mdd_t *image; 00712 if (mdd_is_tautology(fromLowerBound, 0)){ 00713 mdd_manager *mddManager = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork); 00714 return (mdd_zero(mddManager)); 00715 } 00716 image = ((*imageInfo->imageComputeBwdWithDomainVarsProc) 00717 (&(imageInfo->functionData), imageInfo, 00718 fromLowerBound, fromUpperBound, toCareSetArray)); 00719 nPreComps++; 00720 #ifndef NDEBUG 00721 assert(CheckImageValidity( 00722 Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork), 00723 image, 00724 imageInfo->functionData.rangeVars, 00725 imageInfo->functionData.quantifyVars)); 00726 #endif 00727 return image; 00728 } 00746 mdd_t * 00747 Img_ImageInfoComputeEXWithDomainVars( 00748 Img_ImageInfo_t * imageInfo, 00749 mdd_t * fromLowerBound, 00750 mdd_t * fromUpperBound, 00751 array_t * toCareSetArray) 00752 { 00753 mdd_t *image; 00754 if (mdd_is_tautology(fromLowerBound, 0)){ 00755 mdd_manager *mddManager = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork); 00756 return (mdd_zero(mddManager)); 00757 } 00758 image = ((*imageInfo->imageComputeBwdWithDomainVarsProc) 00759 (&(imageInfo->functionData), imageInfo, 00760 fromLowerBound, fromUpperBound, toCareSetArray)); 00761 nPreComps++; 00762 00763 return image; 00764 } 00765 00766 00783 mdd_t * 00784 Img_ImageInfoComputeBwdWithDomainVars( 00785 Img_ImageInfo_t * imageInfo, 00786 mdd_t * fromLowerBound, 00787 mdd_t * fromUpperBound, 00788 mdd_t * toCareSet) 00789 { 00790 array_t *toCareSetArray; 00791 mdd_t *preImage; 00792 00793 toCareSetArray = array_alloc(mdd_t *, 0); 00794 array_insert(mdd_t *, toCareSetArray, 0, toCareSet); 00795 preImage = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, 00796 fromLowerBound, fromUpperBound, toCareSetArray); 00797 array_free(toCareSetArray); 00798 return(preImage); 00799 } 00800 00801 00822 mdd_t * 00823 Img_ImageInfoComputeBwd(Img_ImageInfo_t * imageInfo, 00824 mdd_t * fromLowerBound, 00825 mdd_t * fromUpperBound, 00826 array_t * toCareSetArray) 00827 { 00828 mdd_t *image; 00829 if (mdd_is_tautology(fromLowerBound, 0)){ 00830 mdd_manager *mddManager = 00831 Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork); 00832 return (mdd_zero(mddManager)); 00833 } 00834 image = ((*imageInfo->imageComputeBwdProc) (&(imageInfo->functionData), 00835 imageInfo, 00836 fromLowerBound, 00837 fromUpperBound, 00838 toCareSetArray)); 00839 nPreComps++; 00840 #ifndef NDEBUG 00841 assert(CheckImageValidity( 00842 Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork), 00843 image, 00844 imageInfo->functionData.rangeVars, 00845 imageInfo->functionData.quantifyVars)); 00846 #endif 00847 return image; 00848 } 00849 00850 00861 void 00862 Img_ImageInfoFree(Img_ImageInfo_t * imageInfo) 00863 { 00864 (*imageInfo->imageFreeProc) (imageInfo->methodData); 00865 if (imageInfo->functionData.domainBddVars) 00866 mdd_array_free(imageInfo->functionData.domainBddVars); 00867 if (imageInfo->functionData.rangeBddVars) 00868 mdd_array_free(imageInfo->functionData.rangeBddVars); 00869 if (imageInfo->functionData.quantifyBddVars) 00870 mdd_array_free(imageInfo->functionData.quantifyBddVars); 00871 if (imageInfo->functionData.permutD2R) 00872 FREE(imageInfo->functionData.permutD2R); 00873 if (imageInfo->functionData.permutR2D) 00874 FREE(imageInfo->functionData.permutR2D); 00875 if (imageInfo->savedRelation) 00876 mdd_array_free((array_t *) imageInfo->savedRelation); 00877 FREE(imageInfo); 00878 } 00879 00890 void 00891 Img_ImageInfoFreeFAFW(Img_ImageInfo_t * imageInfo) 00892 { 00893 if (imageInfo->functionData.quantifyVars) 00894 mdd_array_free(imageInfo->functionData.quantifyVars); 00895 if (imageInfo->functionData.quantifyCube) 00896 mdd_free(imageInfo->functionData.quantifyCube); 00897 } 00898 00911 char * 00912 Img_ImageInfoObtainMethodTypeAsString(Img_ImageInfo_t * imageInfo) 00913 { 00914 char *methodString; 00915 Img_MethodType methodType = imageInfo->methodType; 00916 00917 switch (methodType) { 00918 case Img_Monolithic_c: 00919 methodString = util_strsav("monolithic"); 00920 break; 00921 case Img_Tfm_c: 00922 methodString = util_strsav("tfm"); 00923 break; 00924 case Img_Hybrid_c: 00925 methodString = util_strsav("hybrid"); 00926 break; 00927 case Img_Iwls95_c: 00928 methodString = util_strsav("iwls95"); 00929 break; 00930 case Img_Mlp_c: 00931 methodString = util_strsav("mlp"); 00932 break; 00933 case Img_Linear_c: 00934 methodString = util_strsav("linear"); 00935 break; 00936 case Img_Default_c: 00937 methodString = util_strsav("default"); 00938 break; 00939 default: 00940 fail("IMG Error : Unexpected type when initalizing image method"); 00941 } 00942 return methodString; 00943 } 00944 00945 00957 Img_MethodType 00958 Img_ImageInfoObtainMethodType(Img_ImageInfo_t * imageInfo) 00959 { 00960 return(imageInfo->methodType); 00961 } 00962 00974 Img_OptimizeType 00975 Img_ImageInfoObtainOptimizeType(Img_ImageInfo_t * imageInfo) 00976 { 00977 return(imageInfo->linearOptimize); 00978 } 00979 00991 void 00992 Img_ImageInfoSetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo) 00993 { 00994 imageInfo->useOptimizedRelationFlag = 1; 00995 } 00996 01008 void 01009 Img_ImageInfoResetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo) 01010 { 01011 imageInfo->useOptimizedRelationFlag = 0; 01012 } 01013 01025 void 01026 Img_ImageInfoResetLinearComputeRange(Img_ImageInfo_t * imageInfo) 01027 { 01028 imageInfo->linearComputeRange = 0; 01029 } 01030 01042 void 01043 Img_ImageInfoSetLinearComputeRange(Img_ImageInfo_t * imageInfo) 01044 { 01045 imageInfo->linearComputeRange = 1; 01046 } 01047 01057 void 01058 Img_ImageInfoPrintMethodParams(Img_ImageInfo_t *imageInfo, FILE *fp) 01059 { 01060 (*imageInfo->imagePrintMethodParamsProc)(imageInfo->methodData, fp); 01061 } 01062 01072 void 01073 Img_ResetTrMinimizedFlag(Img_ImageInfo_t *imageInfo, 01074 Img_DirectionType directionType) 01075 { 01076 if (directionType == Img_Forward_c || directionType == Img_Both_c) 01077 imageInfo->fwdTrMinimizedFlag = FALSE; 01078 if (directionType == Img_Backward_c || directionType == Img_Both_c) 01079 imageInfo->bwdTrMinimizedFlag = FALSE; 01080 } 01081 01082 01092 Img_MinimizeType 01093 Img_ReadMinimizeMethod(void) 01094 { 01095 01096 int value; 01097 char *flagValue; 01098 Img_MinimizeType minimizeMethod = Img_Restrict_c; 01099 01100 flagValue = Cmd_FlagReadByName("image_minimize_method"); 01101 if (flagValue != NIL(char)) { 01102 sscanf(flagValue, "%d", &value); 01103 switch (value) { 01104 case 0 : 01105 minimizeMethod = Img_Restrict_c; 01106 break; 01107 case 1 : 01108 minimizeMethod = Img_Constrain_c; 01109 break; 01110 case 2 : 01111 if (bdd_get_package_name() != CUDD) { 01112 fprintf(vis_stderr, "** img error : Compact in image_minimize_method "); 01113 fprintf(vis_stderr, "is currently supported only by CUDD. ***\n"); 01114 fprintf(vis_stderr, 01115 "** img error : Reverting to default minimize method : restrict\n"); 01116 break; 01117 } 01118 minimizeMethod = Img_Compact_c; 01119 break; 01120 case 3 : 01121 if (bdd_get_package_name() != CUDD) { 01122 fprintf(vis_stderr, "** img error : Squeeze in image_minimize_method "); 01123 fprintf(vis_stderr, "is currently supported only by CUDD. ***\n"); 01124 fprintf(vis_stderr, 01125 "** img error : Reverting to default minimize method : restrict\n"); 01126 break; 01127 } 01128 minimizeMethod = Img_Squeeze_c; 01129 break; 01130 case 4 : 01131 minimizeMethod = Img_And_c; 01132 break; 01133 default : 01134 fprintf(vis_stderr, 01135 "** img error : invalid value %s for image_minimize_method[0-4]. ***\n", 01136 flagValue); 01137 fprintf(vis_stderr, 01138 "** img error : Reverting to default minimize method : restrict\n"); 01139 break; 01140 } 01141 } 01142 return(minimizeMethod); 01143 } 01144 01145 01174 void 01175 Img_MinimizeTransitionRelation( 01176 Img_ImageInfo_t *imageInfo, 01177 array_t *constrainArray, 01178 Img_MinimizeType minimizeMethod, 01179 Img_DirectionType directionType, 01180 boolean reorderIwls95Clusters) 01181 { 01182 if (minimizeMethod == Img_DefaultMinimizeMethod_c) 01183 minimizeMethod = Img_ReadMinimizeMethod(); 01184 01185 switch (imageInfo->methodType) { 01186 case Img_Monolithic_c: 01187 if (imageInfo->fwdTrMinimizedFlag) 01188 break; 01189 ImgMinimizeTransitionRelationMono(imageInfo, constrainArray, 01190 minimizeMethod, imageInfo->printMinimizeStatus); 01191 imageInfo->fwdTrMinimizedFlag = TRUE; 01192 break; 01193 case Img_Tfm_c: 01194 case Img_Hybrid_c: 01195 if (imageInfo->fwdTrMinimizedFlag) 01196 break; 01197 ImgMinimizeTransitionFunction(imageInfo->methodData, constrainArray, 01198 minimizeMethod, directionType, 01199 imageInfo->printMinimizeStatus); 01200 if (directionType == Img_Forward_c || directionType == Img_Both_c) 01201 imageInfo->fwdTrMinimizedFlag = TRUE; 01202 if (directionType == Img_Backward_c || directionType == Img_Both_c) 01203 imageInfo->bwdTrMinimizedFlag = TRUE; 01204 break; 01205 case Img_Iwls95_c: 01206 case Img_Mlp_c: 01207 case Img_Linear_c: 01208 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 01209 if (imageInfo->fwdTrMinimizedFlag == FALSE) { 01210 ImgMinimizeTransitionRelationIwls95(imageInfo->methodData, 01211 &(imageInfo->functionData), 01212 constrainArray, minimizeMethod, 01213 Img_Forward_c, 01214 reorderIwls95Clusters, 01215 imageInfo->printMinimizeStatus); 01216 imageInfo->fwdTrMinimizedFlag = TRUE; 01217 } 01218 } 01219 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 01220 if (imageInfo->bwdTrMinimizedFlag == FALSE) { 01221 ImgMinimizeTransitionRelationIwls95(imageInfo->methodData, 01222 &(imageInfo->functionData), 01223 constrainArray, minimizeMethod, 01224 Img_Backward_c, 01225 reorderIwls95Clusters, 01226 imageInfo->printMinimizeStatus); 01227 imageInfo->bwdTrMinimizedFlag = TRUE; 01228 } 01229 } 01230 break; 01231 default: 01232 fail("** img error: Unexpected type when minimizing transition relation"); 01233 } 01234 } 01235 01236 01237 01253 mdd_t * 01254 Img_MinimizeImage( 01255 mdd_t *image, 01256 mdd_t *constraint, 01257 Img_MinimizeType method, 01258 boolean underapprox) 01259 { 01260 mdd_t *newImage; 01261 mdd_t *l, *u; 01262 01263 if (method == Img_DefaultMinimizeMethod_c) 01264 method = Img_ReadMinimizeMethod(); 01265 01266 if(underapprox){ 01267 switch (method) { 01268 case Img_Restrict_c : 01269 newImage = bdd_minimize(image, constraint); 01270 break; 01271 case Img_Constrain_c : 01272 newImage = bdd_cofactor(image, constraint); 01273 break; 01274 case Img_Compact_c : 01275 newImage = bdd_compact(image, constraint); 01276 break; 01277 case Img_Squeeze_c : 01278 l = bdd_and(image, constraint, 1, 1); 01279 u = bdd_or(image, constraint, 1, 0); 01280 newImage = bdd_squeeze(l, u); 01281 if (bdd_size(newImage) >= bdd_size(image)) { 01282 bdd_free(newImage); 01283 newImage = bdd_dup(image); 01284 } 01285 mdd_free(l); 01286 mdd_free(u); 01287 break; 01288 case Img_And_c : 01289 newImage = bdd_and(image, constraint, 1, 1); 01290 break; 01291 default : 01292 fail("** img error : Unexpected type when minimizing an image"); 01293 } 01294 }else{ /* if underapprox */ 01295 switch (method) { 01296 case Img_Squeeze_c : 01297 l = image; 01298 u = bdd_or(image, constraint, 1, 0); 01299 newImage = bdd_squeeze(l, u); 01300 if (bdd_size(newImage) >= bdd_size(image)) { 01301 bdd_free(newImage); 01302 newImage = bdd_dup(image); 01303 } 01304 mdd_free(u); 01305 break; 01306 case Img_OrNot_c : 01307 newImage = bdd_or(image, constraint, 1, 0); 01308 break; 01309 default : 01310 fail("** img error: Unexpected type when adding dont-cares to an image"); 01311 } 01312 }/* if underapprox */ 01313 01314 return(newImage); 01315 } 01316 01326 mdd_t * 01327 Img_AddDontCareToImage( 01328 mdd_t *image, 01329 mdd_t *constraint, 01330 Img_MinimizeType method) 01331 { 01332 return(Img_MinimizeImage(image, constraint, Img_Restrict_c, method)); 01333 } 01334 01335 01336 01348 mdd_t * 01349 Img_MinimizeImageArray( 01350 mdd_t *image, 01351 array_t *constraintArray, 01352 Img_MinimizeType method, 01353 boolean underapprox) 01354 { 01355 int i; 01356 mdd_t *newImage, *tmpImage; 01357 mdd_t *constraint; 01358 01359 if (method == Img_DefaultMinimizeMethod_c) 01360 method = Img_ReadMinimizeMethod(); 01361 01362 newImage = mdd_dup(image); 01363 arrayForEachItem(mdd_t *, constraintArray, i, constraint) { 01364 tmpImage = newImage; 01365 newImage = Img_MinimizeImage(tmpImage, constraint, method, underapprox); 01366 mdd_free(tmpImage); 01367 } 01368 return(newImage); 01369 } 01370 01382 void 01383 Img_SetPrintMinimizeStatus(Img_ImageInfo_t *imageInfo, int status) 01384 { 01385 if (status < 0 || status > 2) 01386 (void)fprintf(vis_stderr, 01387 "** img error: invalid value[%d] for status.\n", status); 01388 else 01389 imageInfo->printMinimizeStatus = status; 01390 } 01391 01403 int 01404 Img_ReadPrintMinimizeStatus(Img_ImageInfo_t *imageInfo) 01405 { 01406 return(imageInfo->printMinimizeStatus); 01407 } 01408 01419 void 01420 Img_AbstractTransitionRelation(Img_ImageInfo_t *imageInfo, 01421 array_t *abstractVars, mdd_t *abstractCube, 01422 Img_DirectionType directionType) 01423 { 01424 switch (imageInfo->methodType) { 01425 case Img_Monolithic_c: 01426 ImgAbstractTransitionRelationMono(imageInfo, abstractVars, 01427 abstractCube, imageInfo->printMinimizeStatus); 01428 break; 01429 case Img_Tfm_c: 01430 case Img_Hybrid_c: 01431 ImgAbstractTransitionFunction(imageInfo, abstractVars, 01432 abstractCube, directionType, 01433 imageInfo->printMinimizeStatus); 01434 break; 01435 case Img_Iwls95_c: 01436 case Img_Mlp_c: 01437 case Img_Linear_c: 01438 ImgAbstractTransitionRelationIwls95(imageInfo, abstractVars, 01439 abstractCube, directionType, 01440 imageInfo->printMinimizeStatus); 01441 break; 01442 default: 01443 fail("** img error : Unexpected type when abstracting transition relation"); 01444 } 01445 } 01446 01457 void 01458 Img_DupTransitionRelation(Img_ImageInfo_t *imageInfo, 01459 Img_DirectionType directionType) 01460 { 01461 switch (imageInfo->methodType) { 01462 case Img_Monolithic_c: 01463 ImgDuplicateTransitionRelationMono(imageInfo); 01464 break; 01465 case Img_Tfm_c: 01466 case Img_Hybrid_c: 01467 ImgDuplicateTransitionFunction(imageInfo, directionType); 01468 break; 01469 case Img_Iwls95_c: 01470 case Img_Mlp_c: 01471 case Img_Linear_c: 01472 ImgDuplicateTransitionRelationIwls95(imageInfo, directionType); 01473 break; 01474 default: 01475 fail("** img error: Unexpected type when duplicating transition relation"); 01476 } 01477 } 01478 01488 void 01489 Img_RestoreTransitionRelation(Img_ImageInfo_t *imageInfo, 01490 Img_DirectionType directionType) 01491 { 01492 01493 switch (imageInfo->methodType) { 01494 case Img_Monolithic_c: 01495 ImgRestoreTransitionRelationMono(imageInfo, directionType); 01496 break; 01497 case Img_Tfm_c: 01498 case Img_Hybrid_c: 01499 ImgRestoreTransitionFunction(imageInfo, directionType); 01500 break; 01501 case Img_Iwls95_c: 01502 case Img_Mlp_c: 01503 case Img_Linear_c: 01504 ImgRestoreTransitionRelationIwls95(imageInfo, directionType); 01505 break; 01506 default: 01507 fail("** img error : Unexpected type when backup transition relation"); 01508 } 01509 } 01510 01511 01521 int 01522 Img_ApproximateTransitionRelation(Img_ImageInfo_t *imageInfo, 01523 bdd_approx_dir_t approxDir, 01524 bdd_approx_type_t approxMethod, 01525 int approxThreshold, 01526 double approxQuality, 01527 double approxQualityBias, 01528 Img_DirectionType directionType, 01529 mdd_t *bias) 01530 { 01531 int unchanged = 0; 01532 mdd_manager *mgr = 01533 Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork); 01534 01535 switch (imageInfo->methodType) { 01536 case Img_Monolithic_c: 01537 unchanged = ImgApproximateTransitionRelationMono(mgr, imageInfo, 01538 approxDir, approxMethod, 01539 approxThreshold, 01540 approxQuality, 01541 approxQualityBias, bias); 01542 break; 01543 case Img_Tfm_c: 01544 case Img_Hybrid_c: 01545 unchanged = ImgApproximateTransitionFunction(mgr, 01546 imageInfo->methodData, 01547 approxDir, approxMethod, 01548 approxThreshold, 01549 approxQuality, 01550 approxQualityBias, 01551 directionType, bias); 01552 break; 01553 case Img_Iwls95_c: 01554 case Img_Mlp_c: 01555 case Img_Linear_c: 01556 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 01557 unchanged = ImgApproximateTransitionRelationIwls95(mgr, 01558 imageInfo->methodData, 01559 approxDir, approxMethod, 01560 approxThreshold, 01561 approxQuality, 01562 approxQualityBias, 01563 Img_Forward_c, bias); 01564 } 01565 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 01566 unchanged += ImgApproximateTransitionRelationIwls95(mgr, 01567 imageInfo->methodData, 01568 approxDir, approxMethod, 01569 approxThreshold, 01570 approxQuality, 01571 approxQualityBias, 01572 Img_Backward_c, bias); 01573 } 01574 break; 01575 default: 01576 fail( 01577 "** img error : Unexpected type when approximating transition relation"); 01578 } 01579 return(unchanged); 01580 } 01581 01582 01592 mdd_t * 01593 Img_ApproximateImage(mdd_manager *mgr, 01594 mdd_t *image, 01595 bdd_approx_dir_t approxDir, 01596 bdd_approx_type_t approxMethod, 01597 int approxThreshold, 01598 double approxQuality, 01599 double approxQualityBias, 01600 mdd_t *bias) 01601 { 01602 double quality; 01603 double qualityBias; 01604 int nvars = mdd_get_number_of_bdd_support(mgr, image); 01605 mdd_t *approxImage; 01606 01607 if (approxQuality != 0.0) 01608 quality = approxQuality; 01609 else 01610 quality = 1.0; /* default */ 01611 01612 /* based on approximation method specified, compute subset or superset */ 01613 switch (approxMethod) { 01614 case BDD_APPROX_HB: 01615 approxImage = bdd_approx_hb(image, approxDir, nvars, approxThreshold); 01616 break; 01617 case BDD_APPROX_SP: 01618 approxImage = bdd_approx_sp(image, approxDir, nvars, approxThreshold, 0); 01619 break; 01620 case BDD_APPROX_UA: 01621 approxImage = bdd_approx_ua(image, approxDir, nvars, approxThreshold, 0, 01622 quality); 01623 break; 01624 case BDD_APPROX_RUA: 01625 approxImage = bdd_approx_remap_ua(image, approxDir, nvars, approxThreshold, 01626 quality); 01627 break; 01628 case BDD_APPROX_BIASED_RUA: 01629 if (approxQualityBias != 0.0) 01630 qualityBias = approxQualityBias; 01631 else 01632 qualityBias = 0.5; /* default */ 01633 approxImage = bdd_approx_biased_rua(image, approxDir, bias, nvars, 01634 approxThreshold, quality, qualityBias); 01635 break; 01636 case BDD_APPROX_COMP: 01637 approxImage = bdd_approx_compress(image, approxDir, nvars, approxThreshold); 01638 break; 01639 default: 01640 assert(0); 01641 approxImage = NIL(mdd_t); 01642 break; 01643 } 01644 01645 return(approxImage); 01646 } 01647 01648 01658 int 01659 Img_IsPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo) 01660 { 01661 if (imageInfo->methodType == Img_Iwls95_c || 01662 imageInfo->methodType == Img_Mlp_c || 01663 imageInfo->methodType == Img_Linear_c) 01664 return(1); 01665 else if (imageInfo->methodType == Img_Hybrid_c) 01666 return(ImgIsPartitionedTransitionRelationTfm(imageInfo)); 01667 else 01668 return(0); 01669 } 01670 01671 01681 void 01682 Img_ResetNumberOfImageComputation(Img_DirectionType imgDir) 01683 { 01684 if (imgDir == Img_Forward_c || imgDir == Img_Both_c) 01685 nImgComps = 0; 01686 if (imgDir == Img_Backward_c || imgDir == Img_Both_c) 01687 nPreComps = 0; 01688 } 01689 01690 01700 int 01701 Img_GetNumberOfImageComputation(Img_DirectionType imgDir) 01702 { 01703 if (imgDir == Img_Forward_c) 01704 return(nImgComps); 01705 else if (imgDir == Img_Backward_c) 01706 return(nPreComps); 01707 else 01708 return(nImgComps + nPreComps); 01709 } 01710 01711 01721 array_t * 01722 Img_GetPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, 01723 Img_DirectionType directionType) 01724 { 01725 array_t *relationArray; 01726 01727 switch (imageInfo->methodType) { 01728 case Img_Monolithic_c: 01729 relationArray = (array_t *)imageInfo->methodData; 01730 break; 01731 case Img_Tfm_c: 01732 case Img_Hybrid_c: 01733 relationArray = ImgGetTransitionFunction(imageInfo->methodData, 01734 directionType); 01735 break; 01736 case Img_Iwls95_c: 01737 case Img_Mlp_c: 01738 case Img_Linear_c: 01739 relationArray = ImgGetTransitionRelationIwls95(imageInfo->methodData, 01740 directionType); 01741 break; 01742 default: 01743 fail("** img error: Unexpected image method type.\n"); 01744 } 01745 01746 return(relationArray); 01747 } 01748 01749 01759 void 01760 Img_ReplaceIthPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, 01761 int i, mdd_t *relation, Img_DirectionType directionType) 01762 { 01763 switch (imageInfo->methodType) { 01764 case Img_Monolithic_c: 01765 break; 01766 case Img_Tfm_c: 01767 case Img_Hybrid_c: 01768 ImgReplaceIthTransitionFunction(imageInfo->methodData, i, relation, 01769 directionType); 01770 break; 01771 case Img_Iwls95_c: 01772 case Img_Mlp_c: 01773 case Img_Linear_c: 01774 ImgReplaceIthPartitionedTransitionRelationIwls95(imageInfo->methodData, 01775 i, relation, directionType); 01776 break; 01777 default: 01778 fail("** img error: Unexpected image method type.\n"); 01779 } 01780 } 01781 01782 01792 void 01793 Img_ReplacePartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, 01794 array_t *relationArray, Img_DirectionType directionType) 01795 { 01796 switch (imageInfo->methodType) { 01797 case Img_Monolithic_c: 01798 break; 01799 case Img_Tfm_c: 01800 case Img_Hybrid_c: 01801 ImgUpdateTransitionFunction(imageInfo->methodData, relationArray, 01802 directionType); 01803 break; 01804 case Img_Iwls95_c: 01805 case Img_Mlp_c: 01806 case Img_Linear_c: 01807 ImgUpdateTransitionRelationIwls95(imageInfo->methodData, 01808 relationArray, directionType); 01809 break; 01810 default: 01811 fail("** img error: Unexpected image method type.\n"); 01812 } 01813 } 01814 01815 01825 mdd_t * 01826 Img_ComposeIntermediateNodes(graph_t *partition, mdd_t *node, 01827 array_t *psVars, array_t *nsVars, array_t *inputVars) 01828 { 01829 mdd_manager *mgr = Part_PartitionReadMddManager(partition); 01830 array_t *supportList; 01831 st_table *supportTable = st_init_table(st_numcmp, st_numhash); 01832 int i, j; 01833 int existIntermediateVars; 01834 int mddId; 01835 vertex_t *vertex; 01836 array_t *varBddFunctionArray, *varArray; 01837 mdd_t *var, *func, *tmpMdd; 01838 mdd_t *composedNode; 01839 Mvf_Function_t *mvf; 01840 01841 if (psVars) { 01842 for (i = 0; i < array_n(psVars); i++) { 01843 mddId = array_fetch(int, psVars, i); 01844 st_insert(supportTable, (char *)(long)mddId, NULL); 01845 } 01846 } 01847 if (nsVars) { 01848 for (i = 0; i < array_n(nsVars); i++) { 01849 mddId = array_fetch(int, nsVars, i); 01850 st_insert(supportTable, (char *)(long)mddId, NULL); 01851 } 01852 } 01853 if (inputVars) { 01854 for (i = 0; i < array_n(inputVars); i++) { 01855 mddId = array_fetch(int, inputVars, i); 01856 st_insert(supportTable, (char *)(long)mddId, NULL); 01857 } 01858 } 01859 01860 composedNode = mdd_dup(node); 01861 01862 existIntermediateVars = 1; 01863 while (existIntermediateVars) { 01864 existIntermediateVars = 0; 01865 supportList = mdd_get_support(mgr, composedNode); 01866 for (i = 0; i < array_n(supportList); i++) { 01867 mddId = array_fetch(int, supportList, i); 01868 if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) { 01869 vertex = Part_PartitionFindVertexByMddId(partition, mddId); 01870 mvf = Part_VertexReadFunction(vertex); 01871 varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mgr, mddId, mvf); 01872 varArray = mdd_id_to_bdd_array(mgr, mddId); 01873 assert(array_n(varBddFunctionArray) == array_n(varArray)); 01874 for (j = 0; j < array_n(varBddFunctionArray); j++) { 01875 var = array_fetch(mdd_t *, varArray, j); 01876 func = array_fetch(mdd_t *, varBddFunctionArray, j); 01877 tmpMdd = composedNode; 01878 composedNode = bdd_compose(composedNode, var, func); 01879 mdd_free(tmpMdd); 01880 mdd_free(var); 01881 mdd_free(func); 01882 } 01883 array_free(varBddFunctionArray); 01884 array_free(varArray); 01885 existIntermediateVars = 1; 01886 } 01887 } 01888 array_free(supportList); 01889 } 01890 st_free_table(supportTable); 01891 return(composedNode); 01892 } 01893 01894 01922 void 01923 Img_ImageConstrainAndClusterTransitionRelation(Img_ImageInfo_t *imageInfo, 01924 Img_DirectionType direction, 01925 mdd_t *constrain, 01926 Img_MinimizeType minimizeMethod, 01927 boolean underApprox, 01928 boolean cleanUp, 01929 boolean forceReorder, 01930 int printStatus) 01931 { 01932 switch (imageInfo->methodType) { 01933 case Img_Monolithic_c: 01934 ImgImageConstrainAndClusterTransitionRelationMono(imageInfo, 01935 constrain, 01936 minimizeMethod, 01937 underApprox, 01938 cleanUp, 01939 forceReorder, 01940 printStatus); 01941 break; 01942 case Img_Tfm_c: 01943 case Img_Hybrid_c: 01944 ImgImageConstrainAndClusterTransitionRelationTfm(imageInfo, 01945 direction, 01946 constrain, 01947 minimizeMethod, 01948 underApprox, 01949 cleanUp, 01950 forceReorder, 01951 printStatus); 01952 break; 01953 case Img_Iwls95_c: 01954 case Img_Mlp_c: 01955 case Img_Linear_c: 01956 ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp(imageInfo, 01957 direction, 01958 constrain, 01959 minimizeMethod, 01960 underApprox, 01961 cleanUp, 01962 forceReorder, 01963 printStatus); 01964 break; 01965 default: 01966 fail("** img error: Unexpected image method type.\n"); 01967 } 01968 } 01969 01981 Img_MinimizeType 01982 Img_GuidedSearchReadUnderApproxMinimizeMethod(void) 01983 { 01984 char *flagValue; 01985 Img_MinimizeType minimizeMethod = Img_And_c; 01986 01987 flagValue = Cmd_FlagReadByName("guided_search_underapprox_minimize_method"); 01988 if (flagValue != NIL(char)) { 01989 if (strcmp(flagValue, "constrain") == 0) { 01990 minimizeMethod = Img_Constrain_c; 01991 } else if (strcmp(flagValue, "and") == 0) { 01992 minimizeMethod = Img_And_c; 01993 } else { 01994 fprintf(vis_stderr, 01995 "** img error : invalid value %s for guided_search_underapprox_minimize_method. ***\n", 01996 flagValue); 01997 fprintf(vis_stderr, 01998 "** img error : Reverting to default minimize method : And\n"); 01999 } 02000 } 02001 return(minimizeMethod); 02002 } 02003 02015 Img_MinimizeType 02016 Img_GuidedSearchReadOverApproxMinimizeMethod(void) 02017 { 02018 char *flagValue; 02019 Img_MinimizeType minimizeMethod = Img_OrNot_c; 02020 02021 flagValue = Cmd_FlagReadByName("guided_search_overapprox_minimize_method"); 02022 if (flagValue != NIL(char)) { 02023 if (strcmp(flagValue, "ornot") == 0) { 02024 minimizeMethod = Img_OrNot_c; 02025 } else if (strcmp(flagValue, "squeeze") == 0) { 02026 minimizeMethod = Img_Squeeze_c; 02027 } else { 02028 fprintf(vis_stderr, 02029 "** img error : invalid value %s for guided_search_overapprox_minimize_method. ***\n", 02030 flagValue); 02031 fprintf(vis_stderr, 02032 "** img error : Reverting to default method : OrNot\n"); 02033 } 02034 } 02035 return(minimizeMethod); 02036 } 02037 02038 02048 mdd_t * 02049 Img_Substitute(Img_ImageInfo_t *imageInfo, mdd_t *f, Img_SubstituteDir dir) 02050 { 02051 mdd_t *new_; 02052 02053 new_ = ImgSubstitute(f, &(imageInfo->functionData), dir); 02054 return(new_); 02055 } 02056 02057 02058 /*---------------------------------------------------------------------------*/ 02059 /* Definition of internal functions */ 02060 /*---------------------------------------------------------------------------*/ 02061 02080 array_t * 02081 ImgMinimizeImageArrayWithCareSetArray( 02082 array_t *imageArray, 02083 array_t *careSetArray, 02084 Img_MinimizeType minimizeMethod, 02085 boolean underapprox, 02086 boolean printInfo, 02087 Img_DirectionType dir 02088 ) 02089 { 02090 array_t *result; /* of mdd_t * */ 02091 02092 result = mdd_array_duplicate(imageArray); 02093 ImgMinimizeImageArrayWithCareSetArrayInSitu(result, careSetArray, 02094 minimizeMethod, underapprox, 02095 printInfo, dir); 02096 return result; 02097 } 02098 02120 void 02121 ImgMinimizeImageArrayWithCareSetArrayInSitu( 02122 array_t *imageArray, 02123 array_t *careSetArray, 02124 Img_MinimizeType minimizeMethod, 02125 boolean underapprox, 02126 boolean printInfo, 02127 Img_DirectionType dir) 02128 { 02129 int i; 02130 mdd_t *cluster = NIL(mdd_t); 02131 long constrainSize, initialTotalSize; 02132 char *dirname = NIL(char); 02133 02134 if (minimizeMethod == Img_DefaultMinimizeMethod_c) 02135 minimizeMethod = Img_ReadMinimizeMethod(); 02136 02137 if(printInfo){ 02138 constrainSize = mdd_size_multiple(careSetArray); 02139 initialTotalSize = mdd_size_multiple(imageArray); 02140 assert(dir != Img_Both_c); 02141 if(dir == Img_Forward_c) 02142 dirname = "fwd"; 02143 else 02144 dirname = "bwd"; 02145 } else { /* to remove uninitialized variable warnings */ 02146 constrainSize = 0; 02147 initialTotalSize = 0; 02148 } 02149 02150 arrayForEachItem(mdd_t *, imageArray, i, cluster){ 02151 mdd_t *minimized; 02152 02153 minimized = Img_MinimizeImageArray(cluster, careSetArray, 02154 minimizeMethod, underapprox); 02155 array_insert(mdd_t *, imageArray, i, minimized); 02156 02157 if(printInfo) 02158 (void) fprintf(vis_stdout, 02159 "IMG Info: minimized %s relation %d | %ld => %d in component %d.\n", 02160 dirname, mdd_size(cluster), constrainSize, 02161 mdd_size(minimized), i); 02162 mdd_free(cluster); 02163 } 02164 02165 if(printInfo) 02166 (void) fprintf(vis_stdout, 02167 "IMG Info: minimized %s relation %ld | %ld => %ld with %d components.\n", 02168 dirname, initialTotalSize, constrainSize, 02169 mdd_size_multiple(imageArray), array_n(imageArray)); 02170 02171 return; 02172 } 02173 02183 mdd_t * 02184 ImgSubstitute(mdd_t *f, ImgFunctionData_t *functionData, Img_SubstituteDir dir) 02185 { 02186 mdd_t *new_; 02187 02188 if (bdd_get_package_name() == CUDD) { 02189 if (dir == Img_D2R_c) 02190 new_ = bdd_substitute_with_permut(f, functionData->permutD2R); 02191 else 02192 new_ = bdd_substitute_with_permut(f, functionData->permutR2D); 02193 } else { 02194 if (dir == Img_D2R_c) { 02195 new_ = bdd_substitute(f, functionData->domainBddVars, 02196 functionData->rangeBddVars); 02197 } else { 02198 new_ = bdd_substitute(f, functionData->rangeBddVars, 02199 functionData->domainBddVars); 02200 } 02201 } 02202 return(new_); 02203 } 02204 02214 array_t * 02215 ImgSubstituteArray(array_t *f_array, ImgFunctionData_t *functionData, 02216 Img_SubstituteDir dir) 02217 { 02218 array_t *new_array; 02219 02220 if (bdd_get_package_name() == CUDD) { 02221 if (dir == Img_D2R_c) { 02222 new_array = bdd_substitute_array_with_permut(f_array, 02223 functionData->permutD2R); 02224 } else { 02225 new_array = bdd_substitute_array_with_permut(f_array, 02226 functionData->permutR2D); 02227 } 02228 } else { 02229 if (dir == Img_D2R_c) { 02230 new_array = bdd_substitute_array(f_array, functionData->domainBddVars, 02231 functionData->rangeBddVars); 02232 } else { 02233 new_array = bdd_substitute_array(f_array, functionData->rangeBddVars, 02234 functionData->domainBddVars); 02235 } 02236 } 02237 return(new_array); 02238 } 02239 02249 void 02250 ImgPrintPartialImageOptions(void) 02251 { 02252 ImgPartialImageOption_t *PIoption; 02253 char *dummy; 02254 PIoption = ImgGetPartialImageOptions(); 02255 02256 dummy = ALLOC(char, 25); 02257 switch (PIoption->partialImageMethod) { 02258 case Img_PIApprox_c: sprintf(dummy, "%s", "approx");break; 02259 case Img_PIClipping_c: sprintf(dummy, "%s", "clipping");break; 02260 default: sprintf(dummy, "%s", "approx");break; 02261 } 02262 fprintf(vis_stdout, "HD: Partial Image number of variables = %d\n", PIoption->nvars); 02263 fprintf(vis_stdout, "HD: Partial Image Method = %s\n", dummy); 02264 fprintf(vis_stdout, "HD: Partial Image Threshold = %d\n", PIoption->partialImageThreshold); 02265 fprintf(vis_stdout, "HD: Partial Image Size = %d\n", PIoption->partialImageSize); 02266 switch (PIoption->partialImageApproxMethod) { 02267 case BDD_APPROX_HB: sprintf(dummy, "%s", "heavy_branch"); break; 02268 case BDD_APPROX_SP: sprintf(dummy, "%s", "short_paths"); break; 02269 02270 case BDD_APPROX_UA: sprintf(dummy, "%s", "under_approx"); break; 02271 case BDD_APPROX_RUA: sprintf(dummy, "%s", "remap_ua"); break; 02272 02273 case BDD_APPROX_COMP: sprintf(dummy, "%s", "compress"); break; 02274 default: sprintf(dummy, "%s", "remap_ua"); break; 02275 } 02276 fprintf(vis_stdout, "HD: Partial Image Approximation Method = %s\n", dummy); 02277 02278 fprintf(vis_stdout, "HD: Partial Image Approximation quality factor = %g\n", PIoption->quality); 02279 fprintf(vis_stdout, "HD: Partial Image Approximation Bias quality factor = %g\n", PIoption->qualityBias); 02280 fprintf(vis_stdout, "HD: Partial Image Clipping factor = %g\n", PIoption->clippingDepthFrac); 02281 02282 FREE(dummy); 02283 FREE(PIoption); 02284 return; 02285 02286 } /* end of ImgPrintPartialImageOptions */ 02287 02297 ImgPartialImageOption_t * 02298 ImgGetPartialImageOptions(void) 02299 { 02300 ImgPartialImageOption_t *options; 02301 char *qualityString; 02302 char *partialImageThresholdString, *partialImageApproxString, *partialImageSizeString; 02303 char *partialImageMethodString, *clippingDepthString; 02304 02305 options = ALLOC(ImgPartialImageOption_t , 1); 02306 if (options == NIL(ImgPartialImageOption_t)) return NIL(ImgPartialImageOption_t); 02307 02308 /* initialize to default values; */ 02309 options->nvars = 0; 02310 options->partialImageMethod = Img_PIApprox_c; 02311 options->partialImageThreshold = 200000; 02312 options->partialImageSize = 100000; 02313 options->partialImageApproxMethod = BDD_APPROX_RUA; 02314 options->quality = 1.0; 02315 options->qualityBias = 0.5; 02316 options->clippingDepthFrac = IMG_PI_CLIP_DEPTH; 02317 02318 /* what kind of approximation to apply to the image */ 02319 partialImageMethodString = Cmd_FlagReadByName("hd_partial_image_method"); 02320 if (partialImageMethodString != NIL(char)) { 02321 if (strcmp(partialImageMethodString, "approx") == 0) { 02322 options->partialImageMethod = Img_PIApprox_c; 02323 } else if (strcmp(partialImageMethodString, "clipping") == 0) { 02324 options->partialImageMethod = Img_PIClipping_c; 02325 } 02326 } 02327 02328 /* threshold to trigger partial image computation */ 02329 partialImageThresholdString = Cmd_FlagReadByName("hd_partial_image_threshold"); 02330 if (partialImageThresholdString != NIL(char)) { 02331 options->partialImageThreshold = strtol(partialImageThresholdString, NULL, 10); 02332 if (options->partialImageThreshold < 0) { 02333 options->partialImageThreshold = 200000; 02334 } 02335 } 02336 02337 /* intended size of partial image */ 02338 partialImageSizeString = Cmd_FlagReadByName("hd_partial_image_size"); 02339 if (partialImageSizeString != NIL(char)) { 02340 options->partialImageSize = strtol(partialImageSizeString, NULL, 10); 02341 if (options->partialImageSize < 0) { 02342 options->partialImageSize = 100000; 02343 } 02344 } 02345 02346 /* which approximation method to apply */ 02347 partialImageApproxString = Cmd_FlagReadByName("hd_partial_image_approx"); 02348 if (partialImageApproxString != NIL(char)) { 02349 if (strcmp(partialImageApproxString, "heavy_branch") == 0) { 02350 options->partialImageApproxMethod = BDD_APPROX_HB; 02351 } else if (strcmp(partialImageApproxString, "short_paths") == 0) { 02352 options->partialImageApproxMethod = BDD_APPROX_SP; 02353 } else if (strcmp(partialImageApproxString, "under_approx") == 0) { 02354 options->partialImageApproxMethod = BDD_APPROX_UA; 02355 } else if (strcmp(partialImageApproxString, "remap_ua") == 0) { 02356 options->partialImageApproxMethod = BDD_APPROX_RUA; 02357 } else if (strcmp(partialImageApproxString, "compress") == 0) { 02358 options->partialImageApproxMethod = BDD_APPROX_COMP; 02359 } else if (strcmp(partialImageApproxString, "biased_rua") == 0) { 02360 options->partialImageApproxMethod = BDD_APPROX_BIASED_RUA; 02361 } 02362 } 02363 /* quality factor for remap_ua and under_approx methods */ 02364 qualityString = Cmd_FlagReadByName("hd_partial_image_approx_quality"); 02365 if (qualityString != NIL(char)) { 02366 options->quality = strtod(qualityString, NULL); 02367 if (options->quality < 0.0) { 02368 options->quality = 1.0; 02369 } 02370 } 02371 02372 /* quality factor for remap_ua and under_approx methods */ 02373 qualityString = Cmd_FlagReadByName("hd_partial_image_approx_bias_quality"); 02374 if (qualityString != NIL(char)) { 02375 options->qualityBias = strtod(qualityString, NULL); 02376 if (options->qualityBias < 0.0) { 02377 options->qualityBias = 0.5; 02378 } 02379 } 02380 02381 /* fraction of depth of Bdd to clip at. */ 02382 clippingDepthString = Cmd_FlagReadByName("hd_partial_image_clipping_depth"); 02383 if (clippingDepthString != NIL(char)) { 02384 options->clippingDepthFrac = strtod(clippingDepthString, NULL); 02385 if ((options->clippingDepthFrac > 1.0) || 02386 (options->clippingDepthFrac < 0.0)) { 02387 options->clippingDepthFrac = IMG_PI_CLIP_DEPTH; 02388 } 02389 } 02390 02391 return (options); 02392 } /* end of ImgGetPartialImageOptions */ 02393 02404 int 02405 ImgArrayBddArrayCheckValidity(array_t *arrayBddArray) 02406 { 02407 int i; 02408 for(i=0; i<array_n(arrayBddArray); i++) { 02409 ImgBddArrayCheckValidity(array_fetch(array_t*, arrayBddArray, i)); 02410 } 02411 return 1; 02412 } 02413 02414 02424 int 02425 ImgBddArrayCheckValidity(array_t *bddArray) 02426 { 02427 int i; 02428 for(i=0; i<array_n(bddArray); i++) { 02429 ImgBddCheckValidity(array_fetch(bdd_t*, bddArray, i)); 02430 } 02431 return 1; 02432 } 02433 02434 02449 int 02450 ImgBddCheckValidity(bdd_t *bdd) 02451 { 02452 #ifndef NDEBUG 02453 int i; 02454 #endif 02455 assert(bdd_get_free(bdd) == 0); /* Bdd should not have been freed */ 02456 assert(((unsigned long)bdd_get_node(bdd, &i)) & ~0xf); /* Valid node pointer */ 02457 assert(((unsigned long)bdd_get_manager(bdd)) & ~0xf); /* Valid manager pointer */ 02458 return 1; 02459 } 02460 02461 02471 void 02472 ImgPrintVarIdTable(st_table *table) 02473 { 02474 st_generator *stgen; 02475 long varId; 02476 st_foreach_item(table, stgen, &varId, NULL){ 02477 (void) fprintf(vis_stdout, "%d ", (int) varId); 02478 } 02479 (void) fprintf(vis_stdout, "\n"); 02480 } 02481 02482 02492 int 02493 ImgCheckToCareSetArrayChanged(array_t *toCareSetArray1, 02494 array_t *toCareSetArray2) 02495 { 02496 int i, size1, size2; 02497 mdd_t *careSet1, *careSet2; 02498 02499 size1 = array_n(toCareSetArray1); 02500 size2 = array_n(toCareSetArray2); 02501 02502 if (size1 != size2) 02503 return(1); 02504 02505 for (i = 0; i < size1; i++) { 02506 careSet1 = array_fetch(mdd_t *, toCareSetArray1, i); 02507 careSet2 = array_fetch(mdd_t *, toCareSetArray2, i); 02508 if (bdd_equal(careSet1, careSet2) == 0) 02509 return(1); 02510 } 02511 02512 return(0); 02513 } 02514 02515 02516 /*---------------------------------------------------------------------------*/ 02517 02518 /* Definition of static functions */ 02519 /*---------------------------------------------------------------------------*/ 02520 02532 static int 02533 CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t 02534 *domainVarMddIdArray, array_t *quantifyVarMddIdArray) 02535 { 02536 int i; 02537 array_t *imageSupportArray = mdd_get_support(mddManager, image); 02538 st_table *imageSupportTable = st_init_table(st_numcmp, st_numhash); 02539 for (i=0; i<array_n(imageSupportArray); i++){ 02540 long mddId = (long) array_fetch(int, imageSupportArray, i); 02541 (void) st_insert(imageSupportTable, (char *) mddId, NIL(char)); 02542 } 02543 for (i=0; i<array_n(domainVarMddIdArray); i++){ 02544 int domainVarId; 02545 domainVarId = array_fetch(int, domainVarMddIdArray, i); 02546 assert(st_is_member(imageSupportTable, (char *)(long)domainVarId) == 0); 02547 } 02548 for (i=0; i<array_n(quantifyVarMddIdArray); i++){ 02549 int quantifyVarId; 02550 quantifyVarId = array_fetch(int, quantifyVarMddIdArray, i); 02551 assert(st_is_member(imageSupportTable, (char *)(long)quantifyVarId) == 0); 02552 } 02553 st_free_table(imageSupportTable); 02554 array_free(imageSupportArray); 02555 return 1; 02556 } 02557 02558
1.7.3