- Generated on Wed Oct 12 2011 00:34:49 for VIS by
1.7.3
|
VIS
|
00001 00060 #include "imgInt.h" 00061 #include "fsm.h" 00062 00063 static char rcsid[] UNUSED = "$Id: imgIwls95.c,v 1.127 2005/05/18 18:11:57 jinh Exp $"; 00064 00065 /*---------------------------------------------------------------------------*/ 00066 /* Constant declarations */ 00067 /*---------------------------------------------------------------------------*/ 00068 #define domainVar_c 0 00069 #define rangeVar_c 1 00070 #define quantifyVar_c 2 00071 #define IMG_IWLS95_DEBUG 00072 00073 /*---------------------------------------------------------------------------*/ 00074 /* Type declarations */ 00075 /*---------------------------------------------------------------------------*/ 00076 00077 typedef struct Iwls95InfoStruct Iwls95Info_t; 00078 typedef struct CtrInfoStruct CtrInfo_t; 00079 typedef struct VarInfoStruct VarInfo_t; 00080 typedef struct CtrItemStruct CtrItem_t; 00081 typedef struct VarItemStruct VarItem_t; 00082 00083 /*---------------------------------------------------------------------------*/ 00084 /* Structure declarations */ 00085 /*---------------------------------------------------------------------------*/ 00127 struct Iwls95InfoStruct { 00128 array_t *bitRelationArray; 00129 00130 array_t *quantifyVarMddIdArray; 00131 00132 array_t *fwdOptClusteredRelationArray; 00133 array_t *fwdClusteredRelationArray; 00134 array_t *fwdOriClusteredRelationArray; 00135 array_t *bwdClusteredRelationArray; 00136 array_t *bwdOriClusteredRelationArray; 00137 array_t *bwdClusteredCofactoredRelationArray; 00138 array_t *careSetArray; 00139 00140 array_t *fwdOptArraySmoothVarBddArray; 00141 array_t *fwdArraySmoothVarBddArray; 00142 array_t *bwdArraySmoothVarBddArray; 00143 array_t *fwdOptSmoothVarCubeArray; 00144 array_t *fwdSmoothVarCubeArray; 00145 array_t *bwdSmoothVarCubeArray; 00146 00147 boolean allowPartialImage; 00148 boolean wasPartialImage; 00149 ImgPartialImageOption_t *PIoption; 00150 00151 array_t *savedArraySmoothVarBddArray; 00152 array_t *savedSmoothVarCubeArray; 00153 00154 Img_MethodType method; 00155 ImgTrmOption_t *option; 00156 00157 int eliminateDepend; 00158 /* 0 : do not perform this 00159 1 : eliminates dependent variables from 00160 constraint and modifies function vector by 00161 composition at every image computation. 00162 2 : once the number of eliminated variables 00163 becomes zero, do not perform. 00164 */ 00165 int nFoundDependVars; 00166 float averageFoundDependVars; 00167 00168 int nPrevEliminatedFwd; 00169 int linearComputeRange; 00170 00171 boolean lazySiftFlag; 00172 }; 00173 00174 00187 struct CtrInfoStruct { 00188 int ctrId; /* Unique id of the cluster */ 00189 int numLocalSmoothVars; /* 00190 * Number of smooth variables in the support of the 00191 * cluster which can be quantified out if the cluster 00192 * is multiplied in the current product. 00193 */ 00194 int numSmoothVars; /* Number of smooth variables in the support */ 00195 int numIntroducedVars; /* 00196 * Number of range variables introduced if the cluster 00197 * is multiplied in the current product. 00198 */ 00199 int maxSmoothVarIndex; /* Max. index of a smooth variable in the support */ 00200 int rankMaxSmoothVarIndex; /* Rank of maximum index amongst all ctr's */ 00201 lsList varItemList; /* List of varItemStruct of the support variables */ 00202 lsHandle ctrInfoListHandle; /* 00203 * Handle to the list of info struct of ctr's 00204 * which are yet to be ordered. 00205 */ 00206 }; 00207 00208 00209 00222 struct VarInfoStruct { 00223 int bddId; /* BDD id of the variable */ 00224 int numCtr; /* Number of components which depend on this variable. */ 00225 int varType; /* Domain, range or quantify variable ?*/ 00226 lsList ctrItemList; /* List of ctrItemStruct corresponding to the clusters 00227 that depend on it */ 00228 }; 00229 00230 00231 00244 struct VarItemStruct { 00245 VarInfo_t *varInfo; /* The pointer to the corresponding variable info 00246 * structure */ 00247 lsHandle ctrItemHandle; /* 00248 * The list handle to the ctrItemStruct 00249 * corresponding to the ctrInfo (the one which 00250 * contains this varItem in the varItemList) in the 00251 * ctrItemList field of the varInfo. 00252 */ 00253 }; 00254 00255 00268 struct CtrItemStruct { 00269 CtrInfo_t *ctrInfo; /* Pointer to the corresponding cluster 00270 * info structure. */ 00271 lsHandle varItemHandle; /* 00272 * The list handle to the varItemStruct 00273 * corresponding to the varInfo (the one which 00274 * contains this ctrItem in the ctrItemList) in the 00275 * varItemList field of the ctrInfo. 00276 */ 00277 }; 00278 00279 00280 00281 /*---------------------------------------------------------------------------*/ 00282 /* Variable declarations */ 00283 /*---------------------------------------------------------------------------*/ 00284 00285 static double *signatures; 00286 00287 /*---------------------------------------------------------------------------*/ 00288 /* Macro declarations */ 00289 /*---------------------------------------------------------------------------*/ 00290 00291 00294 /*---------------------------------------------------------------------------*/ 00295 /* Static function prototypes */ 00296 /*---------------------------------------------------------------------------*/ 00297 00298 static void ResetClusteredCofactoredRelationArray(mdd_manager *mddManager, Iwls95Info_t *info); 00299 static void FreeClusteredCofactoredRelationArray(Iwls95Info_t *info); 00300 static ImgTrmOption_t * TrmGetOptions(void); 00301 static void CreateBitRelationArray(Iwls95Info_t *info, ImgFunctionData_t *functionData); 00302 static void FreeBitRelationArray(Iwls95Info_t *info); 00303 static void OrderClusterOrder(mdd_manager *mddManager, array_t *relationArray, array_t *fromVarBddArray, array_t *toVarBddArray, array_t *quantifyVarBddArray, array_t **orderedClusteredRelationArrayPtr, array_t **smoothVarBddArrayPtr, ImgTrmOption_t *option, boolean freeRelationArray); 00304 static array_t * CreateClusters(bdd_manager *bddManager, array_t *relationArray, ImgTrmOption_t *option); 00305 static void OrderRelationArray(mdd_manager *mddManager, array_t *relationArray, array_t *domainVarBddArray, array_t *quantifyVarBddArray, array_t *rangeVarBddArray, ImgTrmOption_t *option, array_t **orderedRelationArrayPtr, array_t **arraySmoothVarBddArrayPtr); 00306 static array_t * RelationArraySmoothLocalVars(array_t *relationArray, array_t *ctrInfoArray, array_t *varInfoArray, st_table *bddIdToBddTable); 00307 static void OrderRelationArrayAux(array_t *relationArray, lsList remainingCtrInfoList, array_t *ctrInfoArray, array_t *varInfoArray, int *sortedMaxIndexVector, int numSmoothVarsRemaining, int numIntroducedVarsRemaining, st_table *bddIdToBddTable, ImgTrmOption_t *option, array_t *domainAndQuantifyVarBddArray, array_t **orderedRelationArrayPtr, array_t **arraySmoothVarBddArrayPtr, array_t *arrayDomainQuantifyVarsWithZeroNumCtr); 00308 static array_t * UpdateInfoArrays(CtrInfo_t *ctrInfo, st_table *bddIdToBddTable, int *numSmoothVarsRemainingPtr, int *numIntroducedVarsRemainingPtr); 00309 static float CalculateBenefit(CtrInfo_t *ctrInfo, int maxNumLocalSmoothVars, int maxNumSmoothVars, int maxIndex, int maxNumIntroducedVars, ImgTrmOption_t *option); 00310 static void PrintOption(Img_MethodType method, ImgTrmOption_t *option, FILE *fp); 00311 static Iwls95Info_t * Iwls95InfoStructAlloc(Img_MethodType method); 00312 static CtrInfo_t * CtrInfoStructAlloc(void); 00313 static void CtrInfoStructFree(CtrInfo_t *ctrInfo); 00314 static VarInfo_t * VarInfoStructAlloc(void); 00315 static void VarInfoStructFree(VarInfo_t *varInfo); 00316 static void CtrItemStructFree(CtrItem_t *ctrItem); 00317 static void VarItemStructFree(VarItem_t *varItem); 00318 static int CtrInfoMaxIndexCompare(const void * p1, const void * p2); 00319 static void PrintCtrInfoStruct(CtrInfo_t *ctrInfo); 00320 static void PrintVarInfoStruct(VarInfo_t *varInfo); 00321 static int CheckQuantificationSchedule(array_t *relationArray, array_t *arraySmoothVarBddArray); 00322 static int CheckCtrInfoArray(array_t *ctrInfoArray, int numDomainVars, int numQuantifyVars, int numRangeVars); 00323 static int CheckCtrInfo(CtrInfo_t *ctrInfo, int numDomainVars, int numQuantifyVars, int numRangeVars); 00324 static int CheckVarInfoArray(array_t *varInfoArray, int numRelation); 00325 static array_t * BddArrayDup(array_t *bddArray); 00326 static array_t * BddArrayArrayDup(array_t *bddArray); 00327 static mdd_t * BddLinearAndSmooth(mdd_manager *mddManager, bdd_t *fromSet, array_t *relationArray, array_t *arraySmoothVarBddArray, array_t *smoothVarCubeArray, int verbosity, ImgPartialImageOption_t *PIoption, boolean *partial, boolean lazySiftFlag); 00328 static void HashIdToBddTable(st_table *table, array_t *idArray, array_t *bddArray); 00329 static void PrintSmoothIntroducedCount(array_t *clusterArray, array_t **arraySmoothVarBddArrayPtr, array_t *psBddIdArray, array_t *nsBddIdArray); 00330 static void PrintBddIdFromBddArray(array_t *bddArray); 00331 static void PrintBddIdTable(st_table *idTable); 00332 static void PartitionTraverseRecursively(mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *relationArray, st_table *domainQuantifyVarMddIdTable, array_t *quantifyVarMddIdArray); 00333 static void PrintPartitionRecursively(vertex_t *vertex, st_table *vertexTable, int indent); 00334 static bdd_t * RecomputeImageIfNecessary(ImgFunctionData_t *functionData, mdd_manager *mddManager, bdd_t *domainSubset, array_t *relationArray, array_t *arraySmoothVarBddArray, array_t *smoothVarCubeArray, int verbosity, ImgPartialImageOption_t *PIoption, array_t *toCareSetArray, boolean *partial, boolean lazySiftFlag); 00335 static bdd_t * ComputeSubsetOfIntermediateProduct(bdd_t *product, ImgPartialImageOption_t *PIoption); 00336 static bdd_t * ComputeClippedAndAbstract(bdd_t *product, bdd_t *relation, array_t *smoothVarBddArray, int nvars, int clippingDepth, boolean *partial, int verbosity); 00337 static array_t * CopyArrayBddArray(array_t *arrayBddArray); 00338 static void PrintPartitionedTransitionRelation(mdd_manager *mddManager, Iwls95Info_t *info, Img_DirectionType directionType); 00339 static void ReorderPartitionedTransitionRelation(Iwls95Info_t *info, ImgFunctionData_t *functionData, Img_DirectionType directionType); 00340 static void UpdateQuantificationSchedule(Iwls95Info_t *info, ImgFunctionData_t *functionData, Img_DirectionType directionType); 00341 static array_t * MakeSmoothVarCubeArray(mdd_manager *mddManager, array_t *arraySmoothVarBddArray); 00342 static mdd_t * TrmEliminateDependVars(Img_ImageInfo_t *imageInfo, array_t *relationArray, mdd_t *states, mdd_t **dependRelations); 00343 static int TrmSignatureCompare(int *ptrX, int *ptrY); 00344 static void SetupLazySifting(mdd_manager *mddManager, array_t *bddRelationArray, array_t *domainVarBddArray, array_t *quantifyVarBddArray, array_t *rangeVarBddArray, int verbosity); 00345 static int MddSizeCompare(const void *ptr1, const void *ptr2); 00349 /*---------------------------------------------------------------------------*/ 00350 /* Definition of exported functions */ 00351 /*---------------------------------------------------------------------------*/ 00352 00353 00376 mdd_t* 00377 Img_MultiwayLinearAndSmooth(mdd_manager *mddManager, array_t *relationArray, 00378 array_t *smoothVarMddIdArray, 00379 array_t *introducedVarMddIdArray, 00380 Img_MethodType method, 00381 Img_DirectionType direction) 00382 { 00383 mdd_t *product; 00384 array_t *smoothVarBddArray = mdd_id_array_to_bdd_array(mddManager, 00385 smoothVarMddIdArray); 00386 array_t *introducedVarBddArray = mdd_id_array_to_bdd_array(mddManager, 00387 introducedVarMddIdArray); 00388 00389 product = ImgMultiwayLinearAndSmooth(mddManager, relationArray, 00390 smoothVarBddArray, introducedVarBddArray, 00391 method, direction, NIL(ImgTrmOption_t)); 00392 00393 mdd_array_free(introducedVarBddArray); 00394 mdd_array_free(smoothVarBddArray); 00395 return product; 00396 } 00397 00398 00408 void 00409 Img_PrintPartitionedTransitionRelation(mdd_manager *mddManager, 00410 Img_ImageInfo_t *imageInfo, 00411 Img_DirectionType directionType) 00412 { 00413 Iwls95Info_t *info = (Iwls95Info_t *) imageInfo->methodData; 00414 00415 if (imageInfo->methodType != Img_Iwls95_c && 00416 imageInfo->methodType != Img_Mlp_c && 00417 imageInfo->methodType != Img_Linear_c) 00418 return; 00419 00420 PrintPartitionedTransitionRelation(mddManager, info, directionType); 00421 } 00422 00423 00433 void 00434 Img_ReorderPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, 00435 Img_DirectionType directionType) 00436 { 00437 if (imageInfo->methodType != Img_Iwls95_c && 00438 imageInfo->methodType != Img_Mlp_c && 00439 imageInfo->methodType != Img_Linear_c) 00440 return; 00441 00442 ReorderPartitionedTransitionRelation((Iwls95Info_t *)imageInfo->methodData, 00443 &(imageInfo->functionData), 00444 directionType); 00445 } 00446 00447 00457 void 00458 Img_UpdateQuantificationSchedule(Img_ImageInfo_t *imageInfo, 00459 Img_DirectionType directionType) 00460 { 00461 if (imageInfo->methodType != Img_Iwls95_c) 00462 return; 00463 00464 UpdateQuantificationSchedule((Iwls95Info_t *)imageInfo->methodData, 00465 &(imageInfo->functionData), directionType); 00466 } 00467 00468 00478 void 00479 Img_ClusterRelationArray(mdd_manager *mddManager, 00480 Img_MethodType method, 00481 Img_DirectionType direction, 00482 array_t *relationArray, 00483 array_t *domainVarMddIdArray, 00484 array_t *rangeVarMddIdArray, 00485 array_t *quantifyVarMddIdArray, 00486 array_t **clusteredRelationArray, 00487 array_t **arraySmoothVarBddArray, 00488 array_t **smoothVarCubeArray, 00489 boolean freeRelationArray) 00490 { 00491 array_t *domainVarBddArray; 00492 array_t *quantifyVarBddArray; 00493 array_t *rangeVarBddArray; 00494 ImgTrmOption_t *option; 00495 00496 option = TrmGetOptions(); 00497 domainVarBddArray = mdd_id_array_to_bdd_array(mddManager, 00498 domainVarMddIdArray); 00499 rangeVarBddArray = mdd_id_array_to_bdd_array(mddManager, 00500 rangeVarMddIdArray); 00501 quantifyVarBddArray = mdd_id_array_to_bdd_array(mddManager, 00502 quantifyVarMddIdArray); 00503 00504 *clusteredRelationArray = ImgClusterRelationArray(mddManager, 00505 NIL(ImgFunctionData_t), 00506 method, 00507 direction, 00508 option, 00509 relationArray, 00510 domainVarBddArray, 00511 quantifyVarBddArray, 00512 rangeVarBddArray, 00513 arraySmoothVarBddArray, 00514 smoothVarCubeArray, 00515 freeRelationArray); 00516 00517 ImgFreeTrmOptions(option); 00518 mdd_array_free(domainVarBddArray); 00519 mdd_array_free(rangeVarBddArray); 00520 mdd_array_free(quantifyVarBddArray); 00521 } 00522 00523 00524 /*---------------------------------------------------------------------------*/ 00525 /* Definition of internal functions */ 00526 /*---------------------------------------------------------------------------*/ 00527 00528 00551 mdd_t* 00552 ImgMultiwayLinearAndSmooth(mdd_manager *mddManager, 00553 array_t *relationArray, 00554 array_t *smoothVarBddArray, 00555 array_t *introducedVarBddArray, 00556 Img_MethodType method, 00557 Img_DirectionType direction, 00558 ImgTrmOption_t *option) 00559 { 00560 mdd_t *product; 00561 array_t *domainVarBddArray = array_alloc(bdd_t*, 0); 00562 00563 product = ImgMultiwayLinearAndSmoothWithFrom(mddManager, relationArray, 00564 NIL(mdd_t), 00565 smoothVarBddArray, 00566 domainVarBddArray, 00567 introducedVarBddArray, 00568 method, direction, option); 00569 00570 array_free(domainVarBddArray); 00571 return product; 00572 } 00573 00574 00601 mdd_t* 00602 ImgMultiwayLinearAndSmoothWithFrom(mdd_manager *mddManager, 00603 array_t *relationArray, 00604 mdd_t *from, 00605 array_t *smoothVarBddArray, 00606 array_t *domainVarBddArray, 00607 array_t *introducedVarBddArray, 00608 Img_MethodType method, 00609 Img_DirectionType direction, 00610 ImgTrmOption_t *option) 00611 { 00612 mdd_t *product; 00613 boolean partial = FALSE; 00614 array_t *orderedRelationArray = NIL(array_t); 00615 array_t *arraySmoothVarBddArray = NIL(array_t); 00616 int freeOptionFlag; 00617 int lazySiftFlag = bdd_is_lazy_sift(mddManager); 00618 00619 if (!option) { 00620 option = TrmGetOptions(); 00621 freeOptionFlag = 1; 00622 } else 00623 freeOptionFlag = 0; 00624 00625 if (method == Img_Iwls95_c) { 00626 OrderRelationArray(mddManager, relationArray, domainVarBddArray, 00627 smoothVarBddArray, introducedVarBddArray, option, 00628 &orderedRelationArray, &arraySmoothVarBddArray); 00629 } else if (method == Img_Mlp_c) { 00630 if (direction == Img_Forward_c) { 00631 /* 00632 * domainVarBddArray : PS 00633 * introducedVarBddArray : NS 00634 */ 00635 if (option->mlpMultiway && from == NIL(mdd_t)) { 00636 product = ImgMlpMultiwayAndSmooth(mddManager, NIL(ImgFunctionData_t), 00637 relationArray, domainVarBddArray, 00638 smoothVarBddArray, 00639 introducedVarBddArray, direction, 00640 option); 00641 array_free(domainVarBddArray); 00642 if (freeOptionFlag) 00643 ImgFreeTrmOptions(option); 00644 return product; 00645 } else { 00646 ImgMlpOrderRelationArray(mddManager, relationArray, domainVarBddArray, 00647 smoothVarBddArray, introducedVarBddArray, 00648 direction, &orderedRelationArray, 00649 &arraySmoothVarBddArray, option); 00650 } 00651 } else { /* direction == Img_Backward_c */ 00652 /* 00653 * domainVarBddArray : NS 00654 * introducedVarBddArray : PS 00655 */ 00656 if (option->mlpPreSwapStateVars) { 00657 if (option->mlpMultiway && from == NIL(mdd_t)) { 00658 product = ImgMlpMultiwayAndSmooth(mddManager, NIL(ImgFunctionData_t), 00659 relationArray, 00660 domainVarBddArray, 00661 smoothVarBddArray, 00662 introducedVarBddArray, 00663 Img_Forward_c, option); 00664 array_free(domainVarBddArray); 00665 if (freeOptionFlag) 00666 ImgFreeTrmOptions(option); 00667 return product; 00668 } else { 00669 ImgMlpOrderRelationArray(mddManager, relationArray, 00670 domainVarBddArray, smoothVarBddArray, 00671 introducedVarBddArray, 00672 Img_Forward_c, &orderedRelationArray, 00673 &arraySmoothVarBddArray, option); 00674 } 00675 } else { 00676 if (option->mlpMultiway && from == NIL(mdd_t)) { 00677 product = ImgMlpMultiwayAndSmooth(mddManager, NIL(ImgFunctionData_t), 00678 relationArray, domainVarBddArray, 00679 smoothVarBddArray, 00680 introducedVarBddArray, 00681 Img_Backward_c, option); 00682 array_free(domainVarBddArray); 00683 if (freeOptionFlag) 00684 ImgFreeTrmOptions(option); 00685 return product; 00686 } else { 00687 ImgMlpOrderRelationArray(mddManager, relationArray, 00688 domainVarBddArray, smoothVarBddArray, 00689 introducedVarBddArray, 00690 Img_Backward_c, &orderedRelationArray, 00691 &arraySmoothVarBddArray, option); 00692 } 00693 } 00694 } 00695 } else 00696 assert(0); 00697 00698 product = BddLinearAndSmooth(mddManager, from, 00699 orderedRelationArray, 00700 arraySmoothVarBddArray, 00701 NIL(array_t), 00702 option->verbosity, 00703 NULL, &partial, lazySiftFlag); 00704 00705 if (freeOptionFlag) 00706 ImgFreeTrmOptions(option); 00707 mdd_array_free(orderedRelationArray); 00708 mdd_array_array_free(arraySmoothVarBddArray); 00709 return product; 00710 } 00711 00712 00727 mdd_t* 00728 ImgBddLinearAndSmooth(mdd_manager *mddManager, 00729 mdd_t *from, 00730 array_t *relationArray, 00731 array_t *arraySmoothVarBddArray, 00732 array_t *smoothVarCubeArray, 00733 int verbosity) 00734 { 00735 mdd_t *product; 00736 boolean partial = FALSE; 00737 int lazySiftFlag = bdd_is_lazy_sift(mddManager); 00738 00739 product = BddLinearAndSmooth(mddManager, from, 00740 relationArray, 00741 arraySmoothVarBddArray, 00742 smoothVarCubeArray, 00743 verbosity, 00744 NULL, &partial, lazySiftFlag); 00745 00746 return product; 00747 } 00748 00749 00760 array_t * 00761 ImgClusterRelationArray(mdd_manager *mddManager, 00762 ImgFunctionData_t *functionData, 00763 Img_MethodType method, 00764 Img_DirectionType direction, 00765 ImgTrmOption_t *option, 00766 array_t *relationArray, 00767 array_t *domainVarBddArray, 00768 array_t *quantifyVarBddArray, 00769 array_t *rangeVarBddArray, 00770 array_t **arraySmoothVarBddArray, 00771 array_t **smoothVarCubeArray, 00772 boolean freeRelationArray) 00773 { 00774 array_t *orderedRelationArray; 00775 array_t *clusteredRelationArray; 00776 int freeOptionFlag; 00777 long initialTime, finalTime; 00778 00779 if (!option) { 00780 option = TrmGetOptions(); 00781 freeOptionFlag = 1; 00782 } else 00783 freeOptionFlag = 0; 00784 00785 if (option->verbosity >= 2) 00786 initialTime = util_cpu_time(); 00787 else /* to remove uninitialized variables warning */ 00788 initialTime = 0; 00789 00790 if (method == Img_Iwls95_c) { 00791 assert(direction != Img_Both_c); 00792 if (direction == Img_Forward_c) { 00793 OrderClusterOrder(mddManager, relationArray, domainVarBddArray, 00794 rangeVarBddArray, quantifyVarBddArray, 00795 &orderedRelationArray, arraySmoothVarBddArray, 00796 option, freeRelationArray); 00797 } else { 00798 assert(direction == Img_Backward_c); 00799 OrderClusterOrder(mddManager, relationArray, rangeVarBddArray, 00800 domainVarBddArray, quantifyVarBddArray, 00801 &orderedRelationArray, arraySmoothVarBddArray, 00802 option, freeRelationArray); 00803 00804 } 00805 if (freeOptionFlag) 00806 ImgFreeTrmOptions(option); 00807 00808 if (smoothVarCubeArray) { 00809 if (functionData->createVarCubesFlag) { 00810 *smoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 00811 *arraySmoothVarBddArray); 00812 } else 00813 *smoothVarCubeArray = NIL(array_t); 00814 } 00815 if (option->verbosity >= 2) { 00816 finalTime = util_cpu_time(); 00817 fprintf(vis_stdout, "time for clustering with IWLS95 = %10g\n", 00818 (double)(finalTime - initialTime) / 1000.0); 00819 } 00820 return(orderedRelationArray); 00821 } else if (method == Img_Mlp_c) { 00822 if ((direction == Img_Forward_c && option->mlpReorder == 2) || 00823 (direction == Img_Backward_c && option->mlpPreReorder == 2)) { 00824 if (direction == Img_Forward_c) 00825 option->mlpReorder = 0; 00826 else 00827 option->mlpPreReorder = 0; 00828 ImgMlpClusterRelationArray(mddManager, functionData, relationArray, 00829 domainVarBddArray, quantifyVarBddArray, rangeVarBddArray, 00830 direction, &clusteredRelationArray, NIL(array_t *), option); 00831 if (direction == Img_Forward_c) 00832 option->mlpReorder = 2; 00833 else 00834 option->mlpPreReorder = 2; 00835 ImgMlpOrderRelationArray(mddManager, clusteredRelationArray, 00836 domainVarBddArray, quantifyVarBddArray, rangeVarBddArray, 00837 direction, &orderedRelationArray, arraySmoothVarBddArray, 00838 option); 00839 mdd_array_free(clusteredRelationArray); 00840 } else if ((direction == Img_Forward_c && option->mlpReorder == 3) || 00841 (direction == Img_Backward_c && option->mlpPreReorder == 3)) { 00842 if (direction == Img_Forward_c) 00843 option->mlpReorder = 0; 00844 else 00845 option->mlpPreReorder = 0; 00846 ImgMlpClusterRelationArray(mddManager, functionData, relationArray, 00847 domainVarBddArray, quantifyVarBddArray, rangeVarBddArray, 00848 direction, &clusteredRelationArray, NIL(array_t *), option); 00849 if (direction == Img_Forward_c) 00850 option->mlpReorder = 3; 00851 else 00852 option->mlpPreReorder = 3; 00853 OrderRelationArray(mddManager, clusteredRelationArray, 00854 domainVarBddArray, quantifyVarBddArray, 00855 rangeVarBddArray, option, 00856 &orderedRelationArray, arraySmoothVarBddArray); 00857 mdd_array_free(clusteredRelationArray); 00858 } else { 00859 ImgMlpClusterRelationArray(mddManager, functionData, relationArray, 00860 domainVarBddArray, quantifyVarBddArray, rangeVarBddArray, 00861 direction, &orderedRelationArray, arraySmoothVarBddArray, 00862 option); 00863 } 00864 if (freeOptionFlag) 00865 ImgFreeTrmOptions(option); 00866 if (smoothVarCubeArray) { 00867 if (functionData->createVarCubesFlag) { 00868 *smoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 00869 *arraySmoothVarBddArray); 00870 } else 00871 *smoothVarCubeArray = NIL(array_t); 00872 } 00873 if (option->verbosity >= 2) { 00874 finalTime = util_cpu_time(); 00875 fprintf(vis_stdout, "time for clustering with MLP = %10g\n", 00876 (double)(finalTime - initialTime) / 1000.0); 00877 } 00878 return(orderedRelationArray); 00879 } else 00880 assert(0); 00881 return NIL(array_t); /* we should never get here */ 00882 } 00883 00884 00894 array_t * 00895 ImgGetQuantificationSchedule(mdd_manager *mddManager, 00896 ImgFunctionData_t *functionData, 00897 Img_MethodType method, 00898 Img_DirectionType direction, 00899 ImgTrmOption_t *option, 00900 array_t *relationArray, 00901 array_t *smoothVarBddArray, 00902 array_t *domainVarBddArray, 00903 array_t *introducedVarBddArray, 00904 boolean withClustering, 00905 array_t **orderedRelationArrayPtr) 00906 { 00907 array_t *orderedRelationArray = NIL(array_t); 00908 array_t *clusteredRelationArray; 00909 array_t *arraySmoothVarBddArray = NIL(array_t); 00910 int freeOptionFlag; 00911 00912 if (!option) { 00913 option = TrmGetOptions(); 00914 freeOptionFlag = 1; 00915 } else 00916 freeOptionFlag = 0; 00917 00918 if (method == Img_Iwls95_c) { 00919 if (withClustering) { 00920 OrderRelationArray(mddManager, relationArray, domainVarBddArray, 00921 smoothVarBddArray, introducedVarBddArray, option, 00922 &orderedRelationArray, NIL(array_t *)); 00923 00924 clusteredRelationArray = CreateClusters(mddManager, orderedRelationArray, 00925 option); 00926 mdd_array_free(orderedRelationArray); 00927 00928 OrderRelationArray(mddManager, clusteredRelationArray, domainVarBddArray, 00929 smoothVarBddArray, introducedVarBddArray, option, 00930 &orderedRelationArray, &arraySmoothVarBddArray); 00931 mdd_array_free(clusteredRelationArray); 00932 } else { 00933 OrderRelationArray(mddManager, relationArray, domainVarBddArray, 00934 smoothVarBddArray, introducedVarBddArray, option, 00935 &orderedRelationArray, &arraySmoothVarBddArray); 00936 } 00937 } else if (method == Img_Mlp_c) { 00938 if (withClustering) { 00939 ImgMlpClusterRelationArray(mddManager, functionData, relationArray, 00940 domainVarBddArray, smoothVarBddArray, introducedVarBddArray, 00941 direction, &orderedRelationArray, &arraySmoothVarBddArray, 00942 option); 00943 } else { 00944 ImgMlpOrderRelationArray(mddManager, relationArray, domainVarBddArray, 00945 smoothVarBddArray, introducedVarBddArray, direction, 00946 &orderedRelationArray, &arraySmoothVarBddArray, 00947 option); 00948 } 00949 } else 00950 assert(0); 00951 00952 if (freeOptionFlag) 00953 ImgFreeTrmOptions(option); 00954 if (orderedRelationArrayPtr) 00955 *orderedRelationArrayPtr = orderedRelationArray; 00956 else 00957 mdd_array_free(orderedRelationArray); 00958 return(arraySmoothVarBddArray); 00959 } 00960 00961 00971 ImgTrmOption_t * 00972 ImgGetTrmOptions(void) 00973 { 00974 ImgTrmOption_t *option; 00975 00976 option = TrmGetOptions(); 00977 return(option); 00978 } 00979 00980 00990 void 00991 ImgFreeTrmOptions(ImgTrmOption_t *option) 00992 { 00993 if (option->readCluster) 00994 FREE(option->readCluster); 00995 if (option->writeCluster) 00996 FREE(option->writeCluster); 00997 if (option->writeDepMatrix) 00998 FREE(option->writeDepMatrix); 00999 FREE(option); 01000 } 01001 01002 01014 void 01015 ImgResetMethodDataLinearComputeRange(void *methodData) 01016 { 01017 Iwls95Info_t *info = (Iwls95Info_t *) methodData; 01018 info->linearComputeRange = 0; 01019 } 01020 01031 void 01032 ImgSetMethodDataLinearComputeRange(void *methodData) 01033 { 01034 Iwls95Info_t *info = (Iwls95Info_t *) methodData; 01035 info->linearComputeRange = 1; 01036 } 01037 01048 mdd_t * 01049 Img_ImageGetUnreachableStates(Img_ImageInfo_t * imageInfo) 01050 { 01051 array_t *relationArray; 01052 mdd_t *states; 01053 Iwls95Info_t *info = (Iwls95Info_t *) imageInfo->methodData; 01054 01055 relationArray = info->fwdOptClusteredRelationArray; 01056 states = array_fetch(mdd_t *, relationArray, 0); 01057 states = ImgSubstitute(states, &(imageInfo->functionData), Img_R2D_c); 01058 return(states); 01059 } 01060 01061 01080 void * 01081 ImgImageInfoInitializeIwls95(void *methodData, 01082 ImgFunctionData_t *functionData, 01083 Img_DirectionType directionType, 01084 Img_MethodType method) 01085 { 01086 array_t *fwdClusteredRelationArray; 01087 array_t *bwdClusteredRelationArray; 01088 Iwls95Info_t *info = (Iwls95Info_t *) methodData; 01089 Ntk_Network_t *network; 01090 Ntk_Node_t *node; 01091 char *flagValue; 01092 int i, mddId ; 01093 01094 if (info && 01095 (((info->fwdClusteredRelationArray) && 01096 (info->bwdClusteredRelationArray)) || 01097 ((directionType == Img_Forward_c) && 01098 (info->fwdClusteredRelationArray)) || 01099 ((directionType == Img_Backward_c) && 01100 (info->bwdClusteredRelationArray)))) { 01101 /* Nothing needs to be done. Return */ 01102 return (void *) info; 01103 } 01104 else{ 01105 array_t *rangeVarBddArray, *domainVarBddArray, *quantifyVarBddArray; 01106 array_t *newQuantifyVarMddIdArray; 01107 array_t *clusteredRelationArray; 01108 FILE *fin, *fout; 01109 array_t *bddRelationArray, *quantifyVarMddIdArray; 01110 mdd_manager *mddManager = Part_PartitionReadMddManager(functionData->mddNetwork); 01111 01112 if (info == NIL(Iwls95Info_t)) { 01113 info = Iwls95InfoStructAlloc(method); 01114 } 01115 CreateBitRelationArray(info, functionData); 01116 01118 bddRelationArray = info->bitRelationArray; 01119 quantifyVarMddIdArray = info->quantifyVarMddIdArray; 01120 if(functionData->FAFWFlag) { 01121 network = functionData->network; 01122 newQuantifyVarMddIdArray = array_alloc(int, 0); 01123 for(i=0; i<array_n(quantifyVarMddIdArray); i++) { 01124 mddId = array_fetch(int, quantifyVarMddIdArray, i); 01125 node = Ntk_NetworkFindNodeByMddId(network, mddId); 01126 if(!Ntk_NodeTestIsInput(node)) { 01127 array_insert_last(int, newQuantifyVarMddIdArray, mddId); 01128 } 01129 } 01130 array_free(quantifyVarMddIdArray); 01131 quantifyVarMddIdArray = newQuantifyVarMddIdArray; 01132 info->quantifyVarMddIdArray = newQuantifyVarMddIdArray; 01133 } 01134 01135 info->bitRelationArray = NIL(array_t); 01136 info->quantifyVarMddIdArray = NIL(array_t); 01137 01138 rangeVarBddArray = functionData->rangeBddVars; 01139 domainVarBddArray = functionData->domainBddVars; 01140 quantifyVarBddArray = mdd_id_array_to_bdd_array(mddManager, 01141 quantifyVarMddIdArray); 01142 01143 array_free(quantifyVarMddIdArray); 01144 01145 if (((directionType == Img_Forward_c) || 01146 (directionType == Img_Both_c)) && 01147 (info->fwdClusteredRelationArray == NIL(array_t))) { 01148 if (info->option->readCluster) { 01149 if (info->option->readReorderCluster) { 01150 fin = fopen(info->option->readCluster, "r"); 01151 ImgMlpReadClusterFile(fin, mddManager, 01152 functionData, bddRelationArray, 01153 domainVarBddArray, rangeVarBddArray, 01154 quantifyVarBddArray, Img_Forward_c, 01155 &clusteredRelationArray, NIL(array_t *), 01156 info->option); 01157 fclose(fin); 01158 if (method == Img_Iwls95_c) { 01159 OrderRelationArray(mddManager, clusteredRelationArray, 01160 domainVarBddArray, quantifyVarBddArray, 01161 rangeVarBddArray, info->option, 01162 &info->fwdClusteredRelationArray, 01163 &info->fwdArraySmoothVarBddArray); 01164 } else if (method == Img_Mlp_c) { 01165 ImgMlpOrderRelationArray(mddManager, clusteredRelationArray, 01166 domainVarBddArray, quantifyVarBddArray, 01167 rangeVarBddArray, Img_Forward_c, 01168 &info->fwdClusteredRelationArray, 01169 &info->fwdArraySmoothVarBddArray, 01170 info->option); 01171 } else 01172 assert(0); 01173 mdd_array_free(clusteredRelationArray); 01174 } else { 01175 fin = fopen(info->option->readCluster, "r"); 01176 ImgMlpReadClusterFile(fin, mddManager, 01177 functionData, bddRelationArray, 01178 domainVarBddArray, rangeVarBddArray, 01179 quantifyVarBddArray, Img_Forward_c, 01180 &info->fwdClusteredRelationArray, 01181 &info->fwdArraySmoothVarBddArray, 01182 info->option); 01183 fclose(fin); 01184 } 01185 } else if (method == Img_Iwls95_c) { 01186 /* 01187 * Since clusters are formed by multiplying the latches starting 01188 * from one end we need to order the latches using some heuristics 01189 * first. Right now, we order the latches using the same heuristic 01190 * as the one used for ordering the clusters for early quantifiction. 01191 * However, since we are not interested in the quantification 01192 * schedule at this stage, we will pass a NIL(array_t*) as the last 01193 * argument. 01194 */ 01195 OrderClusterOrder(mddManager, bddRelationArray, domainVarBddArray, 01196 rangeVarBddArray, quantifyVarBddArray, 01197 &info->fwdClusteredRelationArray, 01198 &info->fwdArraySmoothVarBddArray, 01199 info->option, 0); 01200 } else if (method == Img_Mlp_c) { 01201 if (info->option->mlpReorder == 2) { 01202 info->option->mlpReorder = 0; 01203 ImgMlpClusterRelationArray(mddManager, functionData, 01204 bddRelationArray, domainVarBddArray, 01205 quantifyVarBddArray, rangeVarBddArray, 01206 Img_Forward_c, &clusteredRelationArray, 01207 NIL(array_t *), info->option); 01208 info->option->mlpReorder = 2; 01209 ImgMlpOrderRelationArray(mddManager, clusteredRelationArray, 01210 domainVarBddArray, quantifyVarBddArray, 01211 rangeVarBddArray, Img_Forward_c, 01212 &info->fwdClusteredRelationArray, 01213 &info->fwdArraySmoothVarBddArray, info->option); 01214 mdd_array_free(clusteredRelationArray); 01215 } else if (info->option->mlpReorder == 3) { 01216 info->option->mlpReorder = 0; 01217 ImgMlpClusterRelationArray(mddManager, functionData, 01218 bddRelationArray, domainVarBddArray, 01219 quantifyVarBddArray, rangeVarBddArray, 01220 Img_Forward_c, &clusteredRelationArray, 01221 NIL(array_t *), info->option); 01222 info->option->mlpReorder = 3; 01223 OrderRelationArray(mddManager, clusteredRelationArray, 01224 domainVarBddArray, quantifyVarBddArray, 01225 rangeVarBddArray, info->option, 01226 &info->fwdClusteredRelationArray, 01227 &info->fwdArraySmoothVarBddArray); 01228 mdd_array_free(clusteredRelationArray); 01229 } else { 01230 ImgMlpClusterRelationArray(mddManager, functionData, 01231 bddRelationArray, domainVarBddArray, 01232 quantifyVarBddArray, rangeVarBddArray, 01233 Img_Forward_c, &info->fwdClusteredRelationArray, 01234 &info->fwdArraySmoothVarBddArray, info->option); 01235 } 01236 } else if (method == Img_Linear_c || method == Img_Linear_Range_c) { 01237 if(method == Img_Linear_Range_c) { 01238 info->option->linearComputeRange = 1; 01239 method = Img_Linear_c; 01240 } 01241 ImgLinearClusterRelationArray(mddManager, functionData, 01242 bddRelationArray, 01243 Img_Forward_c, 01244 &info->fwdClusteredRelationArray, 01245 &info->fwdArraySmoothVarBddArray, 01246 &info->fwdOptClusteredRelationArray, 01247 &info->fwdOptArraySmoothVarBddArray, 01248 info->option); 01249 } else 01250 assert(0); 01251 01252 if (info->option->verbosity > 2) 01253 PrintPartitionedTransitionRelation(mddManager, info, Img_Forward_c); 01254 if(method == Img_Linear_c) 01255 ImgPrintPartitionedTransitionRelation(mddManager, 01256 info->fwdOptClusteredRelationArray , 01257 info->fwdOptArraySmoothVarBddArray); 01258 01259 if (info->option->printDepMatrix || info->option->writeDepMatrix) { 01260 if (info->option->writeDepMatrix) { 01261 fout = fopen(info->option->writeDepMatrix, "w"); 01262 if (!fout) { 01263 fprintf(vis_stderr, "** img error: can't open file [%s]\n", 01264 info->option->writeDepMatrix); 01265 } 01266 } else 01267 fout = NIL(FILE); 01268 ImgMlpPrintDependenceMatrix(mddManager, 01269 info->fwdClusteredRelationArray, 01270 domainVarBddArray, quantifyVarBddArray, rangeVarBddArray, 01271 Img_Forward_c, info->option->printDepMatrix, fout, 01272 info->option); 01273 if (fout) 01274 fclose(fout); 01275 } 01276 if (info->option->writeCluster) { 01277 fout = fopen(info->option->writeCluster, "w"); 01278 ImgMlpWriteClusterFile(fout, mddManager, 01279 info->fwdClusteredRelationArray, 01280 domainVarBddArray, rangeVarBddArray); 01281 fclose(fout); 01282 } 01283 01284 if (functionData->createVarCubesFlag && info->fwdArraySmoothVarBddArray) 01285 info->fwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 01286 info->fwdArraySmoothVarBddArray); 01287 else 01288 info->fwdSmoothVarCubeArray = NIL(array_t); 01289 01290 if (functionData->createVarCubesFlag && info->fwdOptArraySmoothVarBddArray) 01291 info->fwdOptSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 01292 info->fwdOptArraySmoothVarBddArray); 01293 else 01294 info->fwdOptSmoothVarCubeArray = NIL(array_t); 01295 01296 #ifndef NDEBUG 01297 if(info->fwdClusteredRelationArray) 01298 assert(CheckQuantificationSchedule(info->fwdClusteredRelationArray, 01299 info->fwdArraySmoothVarBddArray)); 01300 if(info->fwdOptClusteredRelationArray) 01301 assert(CheckQuantificationSchedule(info->fwdOptClusteredRelationArray, 01302 info->fwdOptArraySmoothVarBddArray)); 01303 #endif 01304 } 01305 01306 if (((directionType == Img_Backward_c) || 01307 (directionType == Img_Both_c)) && 01308 (info->bwdClusteredRelationArray == NIL(array_t))) { 01309 if (info->option->readCluster) { 01310 if (info->option->readReorderCluster) { 01311 fin = fopen(info->option->readCluster, "r"); 01312 ImgMlpReadClusterFile(fin, mddManager, 01313 functionData, bddRelationArray, 01314 domainVarBddArray, rangeVarBddArray, 01315 quantifyVarBddArray, Img_Backward_c, 01316 &clusteredRelationArray, NIL(array_t *), 01317 info->option); 01318 fclose(fin); 01319 if (method == Img_Iwls95_c) { 01320 OrderRelationArray(mddManager, clusteredRelationArray, 01321 rangeVarBddArray, quantifyVarBddArray, 01322 domainVarBddArray, info->option, 01323 &info->bwdClusteredRelationArray, 01324 &info->bwdArraySmoothVarBddArray); 01325 } else if (method == Img_Mlp_c) { 01326 ImgMlpOrderRelationArray(mddManager, clusteredRelationArray, 01327 domainVarBddArray, quantifyVarBddArray, 01328 rangeVarBddArray, Img_Backward_c, 01329 &info->bwdClusteredRelationArray, 01330 &info->bwdArraySmoothVarBddArray, 01331 info->option); 01332 } else 01333 assert(0); 01334 mdd_array_free(clusteredRelationArray); 01335 } else { 01336 fin = fopen(info->option->readCluster, "r"); 01337 ImgMlpReadClusterFile(fin, mddManager, 01338 functionData, bddRelationArray, 01339 domainVarBddArray, rangeVarBddArray, 01340 quantifyVarBddArray, Img_Backward_c, 01341 &info->bwdClusteredRelationArray, 01342 &info->bwdArraySmoothVarBddArray, 01343 info->option); 01344 fclose(fin); 01345 } 01346 } else if (method == Img_Iwls95_c) { 01347 /* 01348 * Since clusters are formed by multiplying the latches starting 01349 * from one end we need to order the latches using some heuristics 01350 * first. Right now, we order the latches using the same heuristic 01351 * as the one used for ordering the clusters for early quantifiction. 01352 * However, since we are not interested in the quantification 01353 * schedule at this stage, we will pass a NIL(array_t*) as the last 01354 * argument. 01355 */ 01356 OrderClusterOrder(mddManager, bddRelationArray, rangeVarBddArray, 01357 domainVarBddArray, quantifyVarBddArray, 01358 &info->bwdClusteredRelationArray, 01359 &info->bwdArraySmoothVarBddArray, 01360 info->option, 0); 01361 } else if (method == Img_Mlp_c) { 01362 if (info->option->mlpPreReorder == 2) { 01363 info->option->mlpPreReorder = 0; 01364 ImgMlpClusterRelationArray(mddManager, functionData, 01365 bddRelationArray, domainVarBddArray, 01366 quantifyVarBddArray, rangeVarBddArray, 01367 Img_Backward_c, &clusteredRelationArray, 01368 NIL(array_t *), info->option); 01369 info->option->mlpPreReorder = 2; 01370 ImgMlpOrderRelationArray(mddManager, clusteredRelationArray, 01371 domainVarBddArray, quantifyVarBddArray, 01372 rangeVarBddArray, Img_Backward_c, 01373 &info->bwdClusteredRelationArray, 01374 &info->bwdArraySmoothVarBddArray, info->option); 01375 mdd_array_free(clusteredRelationArray); 01376 } else if (info->option->mlpPreReorder == 3) { 01377 info->option->mlpPreReorder = 0; 01378 ImgMlpClusterRelationArray(mddManager, functionData, 01379 bddRelationArray, domainVarBddArray, 01380 quantifyVarBddArray, rangeVarBddArray, 01381 Img_Backward_c, &clusteredRelationArray, 01382 NIL(array_t *), info->option); 01383 info->option->mlpPreReorder = 3; 01384 OrderRelationArray(mddManager, clusteredRelationArray, 01385 domainVarBddArray, quantifyVarBddArray, 01386 rangeVarBddArray, info->option, 01387 &info->bwdClusteredRelationArray, 01388 &info->bwdArraySmoothVarBddArray); 01389 mdd_array_free(clusteredRelationArray); 01390 } else { 01391 ImgMlpClusterRelationArray(mddManager, functionData, 01392 bddRelationArray, domainVarBddArray, 01393 quantifyVarBddArray, rangeVarBddArray, 01394 Img_Backward_c, &info->bwdClusteredRelationArray, 01395 &info->bwdArraySmoothVarBddArray, info->option); 01396 } 01397 } else 01398 assert(0); 01399 01400 info->careSetArray = NIL(array_t); 01401 info->bwdClusteredCofactoredRelationArray = NIL(array_t); 01402 01403 if (info->option->verbosity > 2) 01404 PrintPartitionedTransitionRelation(mddManager, info, Img_Backward_c); 01405 01406 if (info->option->printDepMatrix || info->option->writeDepMatrix) { 01407 if (info->option->writeDepMatrix) { 01408 fout = fopen(info->option->writeDepMatrix, "w"); 01409 if (!fout) { 01410 fprintf(vis_stderr, "** img error: can't open file [%s]\n", 01411 info->option->writeDepMatrix); 01412 } 01413 } else 01414 fout = NIL(FILE); 01415 ImgMlpPrintDependenceMatrix(mddManager, 01416 info->bwdClusteredRelationArray, 01417 domainVarBddArray, quantifyVarBddArray, rangeVarBddArray, 01418 Img_Backward_c, info->option->printDepMatrix, fout, 01419 info->option); 01420 01421 if (fout) 01422 fclose(fout); 01423 } 01424 if (info->option->writeCluster) { 01425 fout = fopen(info->option->writeCluster, "w"); 01426 ImgMlpWriteClusterFile(fout, mddManager, 01427 info->bwdClusteredRelationArray, 01428 domainVarBddArray, rangeVarBddArray); 01429 fclose(fout); 01430 } 01431 01432 if (functionData->createVarCubesFlag) 01433 info->bwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 01434 info->bwdArraySmoothVarBddArray); 01435 else 01436 info->bwdSmoothVarCubeArray = NIL(array_t); 01437 01438 #ifndef NDEBUG 01439 assert(CheckQuantificationSchedule(info->bwdClusteredRelationArray, 01440 info->bwdArraySmoothVarBddArray)); 01441 #endif 01442 } 01443 01444 01445 info->lazySiftFlag = bdd_is_lazy_sift(mddManager); 01446 if (info->lazySiftFlag) { 01447 SetupLazySifting(mddManager, bddRelationArray, domainVarBddArray, 01448 quantifyVarBddArray, rangeVarBddArray, 01449 info->option->verbosity); 01450 } 01451 01452 /* Free the bddRelationArray */ 01453 mdd_array_free(bddRelationArray); 01454 01455 if ((info->option)->verbosity > 0) { 01456 fwdClusteredRelationArray = info->fwdClusteredRelationArray; 01457 bwdClusteredRelationArray = info->bwdClusteredRelationArray; 01458 if (method == Img_Iwls95_c) 01459 fprintf(vis_stdout,"Computing Image Using IWLS95 technique.\n"); 01460 else if (method == Img_Mlp_c) 01461 fprintf(vis_stdout,"Computing Image Using MLP technique.\n"); 01462 else if (method == Img_Linear_c) { 01463 fprintf(vis_stdout,"Computing Image Using LINEAR technique.\n"); 01464 fwdClusteredRelationArray = info->fwdOptClusteredRelationArray; 01465 /*bwdClusteredRelationArray = info->bwdOptClusteredRelationArray;*/ 01466 } 01467 else 01468 assert(0); 01469 fprintf(vis_stdout,"Total # of domain binary variables = %3d\n", 01470 array_n(domainVarBddArray)); 01471 fprintf(vis_stdout,"Total # of range binary variables = %3d\n", 01472 array_n(rangeVarBddArray)); 01473 fprintf(vis_stdout,"Total # of quantify binary variables = %3d\n", 01474 array_n(quantifyVarBddArray)); 01475 if ((directionType == Img_Forward_c) || (directionType == 01476 Img_Both_c)) { 01477 fprintf(vis_stdout, "Shared size of transition relation for forward image computation is %10ld BDD nodes (%-4d components)\n", 01478 bdd_size_multiple(fwdClusteredRelationArray), 01479 array_n(fwdClusteredRelationArray)); 01480 } 01481 if ((directionType == Img_Backward_c) || (directionType == Img_Both_c)) { 01482 fprintf(vis_stdout, "Shared size of transition relation for backward image computation is %10ld BDD nodes (%-4d components)\n", 01483 bdd_size_multiple(bwdClusteredRelationArray), 01484 array_n(bwdClusteredRelationArray)); 01485 } 01486 } 01487 01488 /* Update nvars field in partial image options structure with 01489 total number of variables. */ 01490 if (info->PIoption != NULL) { 01491 (info->PIoption)->nvars = array_n(domainVarBddArray) + 01492 array_n(quantifyVarBddArray) + 01493 array_n(rangeVarBddArray); 01494 } 01495 /* Free the Bdd arrays */ 01496 mdd_array_free(quantifyVarBddArray); 01497 01498 flagValue = Cmd_FlagReadByName("image_eliminate_depend_vars"); 01499 if (flagValue == NIL(char)) 01500 info->eliminateDepend = 0; /* the default value */ 01501 else 01502 info->eliminateDepend = atoi(flagValue); 01503 if (info->eliminateDepend && bdd_get_package_name() != CUDD) { 01504 fprintf(vis_stderr, 01505 "** trm error : image_eliminate_depend_vars is available for only CUDD.\n"); 01506 info->eliminateDepend = 0; 01507 } 01508 info->nPrevEliminatedFwd = -1; 01509 01510 return (void *)info; 01511 } 01512 } 01513 01514 01532 mdd_t * 01533 ImgImageInfoComputeFwdIwls95(ImgFunctionData_t *functionData, 01534 Img_ImageInfo_t *imageInfo, 01535 mdd_t *fromLowerBound, 01536 mdd_t *fromUpperBound, 01537 array_t *toCareSetArray) 01538 { 01539 mdd_t *image, *domainSubset, *newFrom; 01540 mdd_manager *mddManager; 01541 boolean partial; 01542 Iwls95Info_t *info = (Iwls95Info_t *)imageInfo->methodData; 01543 int eliminateDepend; 01544 Img_OptimizeType optDir; 01545 array_t *fwdOriClusteredRelationArray; 01546 array_t *fwdOriArraySmoothVarBddArray; 01547 array_t *fwdOriSmoothVarCubeArray; 01548 array_t *fwdClusteredRelationArray; 01549 Relation_t *head; 01550 int bOptimize; 01551 boolean farSideImageIsEnabled; 01552 char *userSpecifiedMethod; 01553 01554 mddManager = Part_PartitionReadMddManager(functionData->mddNetwork); 01555 01556 if(imageInfo->methodType == Img_Linear_c) { 01557 if(info->fwdClusteredRelationArray == 0 || 01558 imageInfo->useOptimizedRelationFlag) { 01559 fwdOriClusteredRelationArray = info->fwdOptClusteredRelationArray; 01560 fwdOriArraySmoothVarBddArray = info->fwdOptArraySmoothVarBddArray; 01561 fwdOriSmoothVarCubeArray = info->fwdOptSmoothVarCubeArray; 01562 } 01563 else { 01564 fwdOriClusteredRelationArray = info->fwdClusteredRelationArray; 01565 fwdOriArraySmoothVarBddArray = info->fwdArraySmoothVarBddArray; 01566 fwdOriSmoothVarCubeArray = info->fwdSmoothVarCubeArray; 01567 } 01568 } 01569 else { 01570 fwdOriClusteredRelationArray = info->fwdClusteredRelationArray; 01571 fwdOriArraySmoothVarBddArray = info->fwdArraySmoothVarBddArray; 01572 fwdOriSmoothVarCubeArray = info->fwdSmoothVarCubeArray; 01573 } 01574 01575 if (fwdOriClusteredRelationArray == NIL(array_t)) { 01576 fprintf(vis_stderr, "** img error: The data structure has not been "); 01577 fprintf(vis_stderr, "initialized for forward image computation\n"); 01578 return NIL(mdd_t); 01579 } 01580 01581 if (info->eliminateDepend == 1 || 01582 (info->eliminateDepend == 2 && info->nPrevEliminatedFwd > 0)) { 01583 eliminateDepend = 1; 01584 } else 01585 eliminateDepend = 0; 01586 01587 domainSubset = bdd_between(fromLowerBound, fromUpperBound); 01588 01589 if (eliminateDepend) { 01590 fwdClusteredRelationArray = mdd_array_duplicate(fwdOriClusteredRelationArray); 01591 newFrom = TrmEliminateDependVars(imageInfo, fwdClusteredRelationArray, 01592 domainSubset, NIL(mdd_t *)); 01593 mdd_free(domainSubset); 01594 domainSubset = newFrom; 01595 } else 01596 fwdClusteredRelationArray = fwdOriClusteredRelationArray; 01597 01598 /* Record if partial images are allowed. */ 01599 partial = info->allowPartialImage; 01600 info->wasPartialImage = FALSE; 01601 01602 /* bias field is used to bias the intermediate results towards care states */ 01603 if ((info->PIoption)->partialImageApproxMethod == BDD_APPROX_BIASED_RUA) { 01604 /* assume that this array has only one mdd */ 01605 mdd_t *toCareSet = array_fetch(mdd_t *, toCareSetArray, 0); 01606 (info->PIoption)->bias = mdd_dup(toCareSet); 01607 } 01608 01609 /* when the "compositional far side image approach" is selected, and 01610 * there are more than one transition relation clusters, 01611 * over-approximate images (w.r.t individual TR clusters) will be 01612 * used to minimize the transition relation. 01613 */ 01614 farSideImageIsEnabled = FALSE; 01615 userSpecifiedMethod = Cmd_FlagReadByName("image_farside_method"); 01616 if (userSpecifiedMethod != NIL(char)) { 01617 if (!strcmp(userSpecifiedMethod, "1")) 01618 farSideImageIsEnabled = TRUE; 01619 } 01620 01621 if (!farSideImageIsEnabled || array_n(fwdClusteredRelationArray) < 2) { 01622 01623 image = BddLinearAndSmooth(mddManager, domainSubset, 01624 fwdClusteredRelationArray, 01625 fwdOriArraySmoothVarBddArray, 01626 fwdOriSmoothVarCubeArray, 01627 (info->option)->verbosity, 01628 info->PIoption, &partial, info->lazySiftFlag); 01629 01630 }else { 01631 01632 array_t *fwdFarArraySmoothVarBddArray = fwdOriArraySmoothVarBddArray; 01633 array_t *fwdFarSmoothVarCubeArray = fwdOriSmoothVarCubeArray; 01634 array_t *fwdFarClusteredRelationArray = mdd_array_duplicate(fwdClusteredRelationArray); 01635 array_t *upperBoundImages = array_alloc(mdd_t *, 0); 01636 st_table *domainSupportVarTable, *trClusterSupportVarTable; 01637 mdd_t *trCluster, *newDomainset, *newTRcluster, *upperBoundImage; 01638 mdd_t *holdMdd, *tmpMdd; 01639 array_t *tempArray; 01640 int beforeSize, afterSize, middleSize; 01641 int size1, size2, size3; 01642 boolean flag1, flag2; 01643 int i,j, k; 01644 long bddId; 01645 01646 /* compute a series of over-approximate images based on individual 01647 * TR clusters 01648 */ 01649 domainSupportVarTable = st_init_table(st_ptrcmp, st_ptrhash); 01650 tempArray = mdd_get_bdd_support_ids(mddManager, domainSubset); 01651 arrayForEachItem(int, tempArray, j, bddId) { 01652 st_insert(domainSupportVarTable, (char *)bddId, (char *)0); 01653 } 01654 array_free(tempArray); 01655 01656 beforeSize = afterSize = middleSize =0; 01657 arrayForEachItem(mdd_t *, fwdFarClusteredRelationArray, i, trCluster) { 01658 array_t *preQuantifiedVarsInDomainset = array_alloc(mdd_t *, 0); 01659 array_t *preQuantifiedVarsInTRcluster = array_alloc(mdd_t *, 0); 01660 array_t *quantifiedVarsInProduct = array_alloc(mdd_t *, 0); 01661 01662 /* some variables can be quantified before taking the conjunction */ 01663 trClusterSupportVarTable = st_init_table(st_ptrcmp, st_ptrhash); 01664 tempArray = mdd_get_bdd_support_ids(mddManager, trCluster); 01665 arrayForEachItem(int, tempArray, j, bddId) { 01666 st_insert(trClusterSupportVarTable, (char *)bddId, (char *)0); 01667 } 01668 array_free(tempArray); 01669 arrayForEachItem(array_t *, fwdFarArraySmoothVarBddArray, j, tempArray) { 01670 arrayForEachItem(mdd_t *, tempArray, k, holdMdd) { 01671 bddId = (int)bdd_top_var_id(holdMdd); 01672 flag1 = st_is_member(domainSupportVarTable, (char *)bddId); 01673 flag2 = st_is_member(trClusterSupportVarTable, (char *)bddId); 01674 if (flag1 && flag2) 01675 array_insert_last(mdd_t *, quantifiedVarsInProduct, holdMdd); 01676 else if (flag1) 01677 array_insert_last(mdd_t *, preQuantifiedVarsInDomainset, holdMdd); 01678 else if (flag2) 01679 array_insert_last(mdd_t *, preQuantifiedVarsInTRcluster, holdMdd); 01680 else 01681 ; 01682 } 01683 } 01684 st_free_table(trClusterSupportVarTable); 01685 01686 if (array_n(preQuantifiedVarsInDomainset) == 0) 01687 newDomainset = bdd_dup(domainSubset); 01688 else 01689 newDomainset = bdd_smooth(domainSubset, preQuantifiedVarsInDomainset); 01690 array_free(preQuantifiedVarsInDomainset); 01691 01692 if (array_n(preQuantifiedVarsInTRcluster) == 0) 01693 newTRcluster = bdd_dup(trCluster); 01694 else 01695 newTRcluster = bdd_smooth(trCluster, preQuantifiedVarsInTRcluster); 01696 array_free(preQuantifiedVarsInTRcluster); 01697 01698 /* compute the over-approximated image */ 01699 if (array_n(quantifiedVarsInProduct) == 0) 01700 upperBoundImage = bdd_and(newTRcluster, newDomainset, 1, 1); 01701 else 01702 upperBoundImage = bdd_and_smooth(newTRcluster, newDomainset, quantifiedVarsInProduct); 01703 array_free(quantifiedVarsInProduct); 01704 mdd_free(newTRcluster); 01705 mdd_free(newDomainset); 01706 01707 /* minimize the TR cluster with the new upper bound image */ 01708 newTRcluster = Img_MinimizeImage(trCluster, upperBoundImage, 01709 Img_DefaultMinimizeMethod_c, TRUE); 01710 01711 size1 = mdd_size(trCluster); 01712 beforeSize += size1; 01713 size2 = mdd_size(upperBoundImage); 01714 middleSize += size2; 01715 size3 = mdd_size(newTRcluster); 01716 afterSize += size3; 01717 if (info->option->verbosity >= 3) { 01718 fprintf(vis_stdout, "farSideImg: minimize TR cluster[%d] %d |%d => %d\n", i, 01719 size1, size2, size3); 01720 } 01721 01722 if (mdd_equal(newTRcluster, trCluster)) { 01723 mdd_free(newTRcluster); 01724 mdd_free(upperBoundImage); 01725 }else { 01726 mdd_free(trCluster); 01727 array_insert(mdd_t *, fwdFarClusteredRelationArray, i, newTRcluster); 01728 array_insert_last(mdd_t *, upperBoundImages, upperBoundImage); 01729 } 01730 } 01731 st_free_table(domainSupportVarTable); 01732 01733 if (info->option->verbosity >= 2) { 01734 fprintf(vis_stdout, "farSideImg: minimize TR total %d |%d => %d\n", 01735 beforeSize, middleSize, afterSize); 01736 } 01737 01738 /* compute the image with the simplified transition relation */ 01739 image = BddLinearAndSmooth(mddManager, domainSubset, 01740 fwdFarClusteredRelationArray, 01741 fwdFarArraySmoothVarBddArray, 01742 fwdFarSmoothVarCubeArray, 01743 (info->option)->verbosity, 01744 info->PIoption, &partial, info->lazySiftFlag); 01745 mdd_array_free(fwdFarClusteredRelationArray); 01746 01747 /* for performance concerns, the following operations are carried 01748 * out in the domain space 01749 */ 01750 arrayForEachItem(mdd_t *, upperBoundImages, i, holdMdd) { 01751 tmpMdd = ImgSubstitute(holdMdd, functionData, Img_R2D_c); 01752 mdd_free(holdMdd); 01753 array_insert(mdd_t *, upperBoundImages, i, tmpMdd); 01754 } 01755 holdMdd = image; 01756 image = ImgSubstitute(image, functionData,Img_R2D_c); 01757 mdd_free(holdMdd); 01758 01759 /* remove the "bad states" introduced by the TR cluster minimization */ 01760 beforeSize = mdd_size(image); 01761 array_sort(upperBoundImages, MddSizeCompare); 01762 arrayForEachItem(mdd_t *, upperBoundImages, i, tmpMdd) { 01763 size1 = mdd_size(image); 01764 size2 = mdd_size(tmpMdd); 01765 holdMdd = image; 01766 image = mdd_and(image, tmpMdd, 1, 1); 01767 mdd_free(tmpMdd); 01768 mdd_free(holdMdd); 01769 size3 = mdd_size(image); 01770 01771 if (info->option->verbosity >= 3) { 01772 fprintf(vis_stdout, "farSideImg: clip image %d | %d => %d\n", 01773 size1, size2, size3); 01774 } 01775 } 01776 array_free(upperBoundImages); 01777 01778 if (info->option->verbosity >= 2) { 01779 afterSize = mdd_size(image); 01780 fprintf(vis_stdout, "farSideImg: clip image total %d => %d \n", 01781 beforeSize, afterSize); 01782 } 01783 01784 } 01785 01786 01787 /* check that no partial image was computed if not allowed */ 01788 assert(!((!info->allowPartialImage) && partial)); 01789 01790 /* if partial image computed, and if no new states, recompute 01791 * image with relaxed parameters. 01792 */ 01793 if (partial) { 01794 if (bdd_leq_array(image, toCareSetArray, 1, 0)) { 01795 mdd_free(image); 01796 partial = info->allowPartialImage; 01797 image = RecomputeImageIfNecessary(functionData, 01798 mddManager, 01799 domainSubset, 01800 fwdClusteredRelationArray, 01801 fwdOriArraySmoothVarBddArray, 01802 fwdOriSmoothVarCubeArray, 01803 (info->option)->verbosity, 01804 info->PIoption, 01805 toCareSetArray, 01806 &partial, info->lazySiftFlag); 01807 } 01808 } 01809 01810 if(imageInfo->methodType == Img_Linear_c) { 01811 if(imageInfo->useOptimizedRelationFlag) { 01812 if(info->option->linearOptimize == Opt_NS || 01813 info->option->linearOptimize == Opt_Both) 01814 optDir = Opt_Both; 01815 else 01816 optDir = Opt_CS; 01817 01818 head = ImgLinearRelationInit(mddManager, fwdOriClusteredRelationArray, 01819 functionData->domainBddVars, functionData->rangeBddVars, 01820 functionData->quantifyBddVars, info->option); 01821 bOptimize = ImgLinearOptimizeAll(head, optDir, 0); 01822 if(bOptimize) { 01823 ImgLinearRefineRelation(head); 01824 if(info->fwdClusteredRelationArray == 0 && optDir == Opt_Both) { 01825 info->fwdClusteredRelationArray = fwdOriClusteredRelationArray; 01826 info->fwdArraySmoothVarBddArray = 01827 BddArrayArrayDup(fwdOriArraySmoothVarBddArray); 01828 info->fwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 01829 info->fwdArraySmoothVarBddArray); 01830 } 01831 else { 01832 mdd_array_free(fwdOriClusteredRelationArray); 01833 } 01834 fwdOriClusteredRelationArray = ImgLinearExtractRelationArrayT(head); 01835 info->fwdOptClusteredRelationArray = fwdOriClusteredRelationArray; 01836 } 01837 ImgLinearRelationQuit(head); 01838 } 01839 } 01840 01841 /* free the bias function created. */ 01842 if ((info->PIoption)->partialImageApproxMethod == BDD_APPROX_BIASED_RUA) { 01843 mdd_free((info->PIoption)->bias); 01844 (info->PIoption)->bias = NIL(mdd_t); 01845 } 01846 /* indicate whether this image computation was partial or exact. */ 01847 info->wasPartialImage = partial; 01848 info->allowPartialImage = FALSE; 01849 01850 if (eliminateDepend) 01851 mdd_array_free(fwdClusteredRelationArray); 01852 mdd_free(domainSubset); 01853 01854 return image; 01855 } 01856 01871 mdd_t * 01872 ImgImageInfoComputeFwdWithDomainVarsIwls95(ImgFunctionData_t *functionData, 01873 Img_ImageInfo_t *imageInfo, 01874 mdd_t *fromLowerBound, 01875 mdd_t *fromUpperBound, 01876 array_t *toCareSetArray) 01877 { 01878 int i; 01879 array_t *toCareSetArrayRV = NIL(array_t); 01880 mdd_t *toCareSet, *toCareSetRV; 01881 mdd_t *imageRV, *imageDV; 01882 int useToCareSetFlag; 01883 Iwls95Info_t *info = (Iwls95Info_t *)imageInfo->methodData; 01884 01885 if (toCareSetArray && info->allowPartialImage) 01886 useToCareSetFlag = 1; 01887 else 01888 useToCareSetFlag = 0; 01889 01890 if (useToCareSetFlag) { 01891 toCareSetArrayRV = array_alloc(mdd_t *, 0); 01892 arrayForEachItem(bdd_t *, toCareSetArray, i, toCareSet) { 01893 toCareSetRV = ImgSubstitute(toCareSet, functionData, Img_D2R_c); 01894 array_insert(bdd_t *, toCareSetArrayRV, i, toCareSetRV); 01895 } 01896 } 01897 01898 imageRV = ImgImageInfoComputeFwdIwls95(functionData, 01899 imageInfo, 01900 fromLowerBound, 01901 fromUpperBound, 01902 toCareSetArrayRV); 01903 01904 imageDV = ImgSubstitute(imageRV, functionData, Img_R2D_c); 01905 mdd_free(imageRV); 01906 if (useToCareSetFlag) 01907 mdd_array_free(toCareSetArrayRV); 01908 return imageDV; 01909 } 01910 01911 01927 mdd_t * 01928 ImgImageInfoComputeBwdIwls95(ImgFunctionData_t *functionData, 01929 Img_ImageInfo_t *imageInfo, 01930 mdd_t *fromLowerBound, 01931 mdd_t *fromUpperBound, 01932 array_t *toCareSetArray) 01933 { 01934 mdd_t *image, *domainSubset, *simplifiedImage; 01935 mdd_manager *mddManager; 01936 Iwls95Info_t *info = (Iwls95Info_t *)imageInfo->methodData; 01937 boolean partial; 01938 01939 if (info->bwdClusteredRelationArray == NIL(array_t)) { 01940 fprintf(vis_stderr, "** img error: The data structure has not been "); 01941 fprintf(vis_stderr, "initialized for backward image computation\n"); 01942 return NIL(mdd_t); 01943 } 01944 mddManager = Part_PartitionReadMddManager(functionData->mddNetwork); 01945 domainSubset = bdd_between(fromLowerBound, fromUpperBound); 01946 01947 assert(mddManager != NIL(mdd_manager)); 01948 01949 /* Check if we can use the stored simplified relations */ 01950 if (info->careSetArray == NIL(array_t) || 01951 !mdd_array_equal(info->careSetArray, toCareSetArray)){ 01952 FreeClusteredCofactoredRelationArray(info); 01953 info->careSetArray = mdd_array_duplicate(toCareSetArray); 01954 info->bwdClusteredCofactoredRelationArray = 01955 ImgMinimizeImageArrayWithCareSetArray(info->bwdClusteredRelationArray, 01956 toCareSetArray, 01957 Img_DefaultMinimizeMethod_c, TRUE, 01958 (info->option->verbosity > 0), 01959 Img_Backward_c); 01960 } 01961 01962 /* if the partial images are allowed, compute the care set (or its superset) 01963 * so that partial products can be minimized with respect to it. 01964 */ 01965 partial = info->allowPartialImage; 01966 info->wasPartialImage = FALSE; 01967 01968 /* bias is used to bias the intermediate results towards care states */ 01969 if ((info->PIoption)->partialImageApproxMethod == BDD_APPROX_BIASED_RUA) { 01970 /* assume that this array has only one mdd */ 01971 mdd_t *toCareSet = array_fetch(mdd_t *, toCareSetArray, 0); 01972 (info->PIoption)->bias = mdd_dup(toCareSet); 01973 } 01974 01975 01976 image = BddLinearAndSmooth(mddManager, domainSubset, 01977 info->bwdClusteredCofactoredRelationArray, 01978 info->bwdArraySmoothVarBddArray, 01979 info->bwdSmoothVarCubeArray, 01980 (info->option)->verbosity, 01981 info->PIoption, &partial, info->lazySiftFlag); 01982 01983 01984 /* check that no partial image was computed if not allowed */ 01985 assert(!((!info->allowPartialImage) && partial)); 01986 01987 /* if partial image computed, and if no new states, recompute 01988 * image with relaxed parameters. 01989 */ 01990 if (partial && bdd_leq_array(image, toCareSetArray, 1, 0)) { 01991 bdd_free(image); 01992 partial = info->allowPartialImage; 01993 image = RecomputeImageIfNecessary(functionData, 01994 mddManager, 01995 domainSubset, 01996 info->bwdClusteredRelationArray, 01997 info->bwdArraySmoothVarBddArray, 01998 info->bwdSmoothVarCubeArray, 01999 (info->option)->verbosity, 02000 info->PIoption, 02001 toCareSetArray, 02002 &partial, info->lazySiftFlag); 02003 } 02004 02005 /* free the bias function created. */ 02006 if ((info->PIoption)->partialImageApproxMethod == BDD_APPROX_BIASED_RUA) { 02007 mdd_free((info->PIoption)->bias); 02008 (info->PIoption)->bias = NIL(mdd_t); 02009 } 02010 /* indicate whether this image computation was partial or exact. */ 02011 info->wasPartialImage = partial; 02012 info->allowPartialImage = FALSE; 02013 02014 mdd_free(domainSubset); 02015 simplifiedImage = bdd_minimize_array(image, toCareSetArray); 02016 bdd_free(image); 02017 return simplifiedImage; 02018 } 02019 02033 mdd_t * 02034 ImgImageInfoComputeBwdWithDomainVarsIwls95(ImgFunctionData_t *functionData, 02035 Img_ImageInfo_t *imageInfo, 02036 mdd_t *fromLowerBound, 02037 mdd_t *fromUpperBound, 02038 array_t *toCareSetArray) 02039 { 02040 mdd_t *fromLowerBoundRV; 02041 mdd_t *fromUpperBoundRV; 02042 mdd_t *image; 02043 02044 fromLowerBoundRV = ImgSubstitute(fromLowerBound, functionData, Img_D2R_c); 02045 if (mdd_equal(fromLowerBound, fromUpperBound)) 02046 fromUpperBoundRV = fromLowerBoundRV; 02047 else 02048 fromUpperBoundRV = ImgSubstitute(fromUpperBound, functionData, Img_D2R_c); 02049 02050 image = ImgImageInfoComputeBwdIwls95(functionData, 02051 imageInfo, 02052 fromLowerBoundRV, 02053 fromUpperBoundRV, 02054 toCareSetArray); 02055 02056 mdd_free(fromLowerBoundRV); 02057 if (!mdd_equal(fromLowerBound, fromUpperBound)) 02058 mdd_free(fromUpperBoundRV); 02059 return image; 02060 } 02061 02073 void 02074 ImgImageInfoFreeIwls95(void *methodData) 02075 { 02076 Iwls95Info_t *info = (Iwls95Info_t *)methodData; 02077 02078 if (info == NIL(Iwls95Info_t)) { 02079 fprintf(vis_stderr, "** img error: Trying to free the NULL image info\n"); 02080 return; 02081 } 02082 if (info->bitRelationArray != NIL(array_t)) { 02083 mdd_array_free(info->bitRelationArray); 02084 } 02085 if (info->quantifyVarMddIdArray != NIL(array_t)) { 02086 array_free(info->quantifyVarMddIdArray); 02087 } 02088 if (info->fwdOptClusteredRelationArray != NIL(array_t)) { 02089 mdd_array_free(info->fwdOptClusteredRelationArray); 02090 mdd_array_array_free(info->fwdOptArraySmoothVarBddArray); 02091 } 02092 if (info->fwdOptSmoothVarCubeArray) 02093 mdd_array_free(info->fwdOptSmoothVarCubeArray); 02094 if (info->fwdClusteredRelationArray != NIL(array_t)) { 02095 mdd_array_free(info->fwdClusteredRelationArray); 02096 mdd_array_array_free(info->fwdArraySmoothVarBddArray); 02097 } 02098 if (info->fwdSmoothVarCubeArray) 02099 mdd_array_free(info->fwdSmoothVarCubeArray); 02100 if (info->bwdClusteredRelationArray != NIL(array_t)) { 02101 mdd_array_free(info->bwdClusteredRelationArray); 02102 mdd_array_array_free(info->bwdArraySmoothVarBddArray); 02103 } 02104 if (info->bwdSmoothVarCubeArray) 02105 mdd_array_free(info->bwdSmoothVarCubeArray); 02106 FreeClusteredCofactoredRelationArray(info); 02107 02108 if (info->option != NULL) ImgFreeTrmOptions(info->option); 02109 if (info->PIoption != NULL) FREE(info->PIoption); 02110 02111 if (info->savedArraySmoothVarBddArray != NIL(array_t)) 02112 mdd_array_array_free(info->savedArraySmoothVarBddArray); 02113 if (info->savedSmoothVarCubeArray != NIL(array_t)) 02114 mdd_array_free(info->savedSmoothVarCubeArray); 02115 02116 FREE(info); 02117 } 02118 02131 void 02132 ImgImageInfoPrintMethodParamsIwls95(void *methodData, FILE *fp) 02133 { 02134 Iwls95Info_t *info = (Iwls95Info_t *)methodData; 02135 if (fp == NULL) return; 02136 PrintOption(info->method, info->option, fp); 02137 if (info->fwdClusteredRelationArray != NIL(array_t)) { 02138 (void) fprintf(fp, "Shared size of transition relation for forward image computation is %10ld BDD nodes (%-4d components)\n", 02139 bdd_size_multiple(info->fwdClusteredRelationArray), 02140 array_n(info->fwdClusteredRelationArray)); 02141 } 02142 if (info->bwdClusteredRelationArray != NIL(array_t)) { 02143 (void) fprintf(fp, "Shared size of transition relation for backward image computation is %10ld BDD nodes (%-4d components)\n", 02144 bdd_size_multiple(info->bwdClusteredRelationArray), 02145 array_n(info->bwdClusteredRelationArray)); 02146 } 02147 } 02148 02160 st_table * 02161 ImgBddGetSupportIdTable(bdd_t *function) 02162 { 02163 st_table *supportTable; 02164 var_set_t *supportVarSet; 02165 int i; 02166 02167 supportTable = st_init_table(st_numcmp, st_numhash); 02168 supportVarSet = bdd_get_support(function); 02169 for(i=0; i<supportVarSet->n_elts; i++) { 02170 if (var_set_get_elt(supportVarSet, i) == 1) { 02171 st_insert(supportTable, (char *)(long) i, NIL(char)); 02172 } 02173 } 02174 var_set_free(supportVarSet); 02175 return supportTable; 02176 } 02177 02191 boolean 02192 ImgImageWasPartialIwls95(void *methodData) 02193 { 02194 Iwls95Info_t *info = (Iwls95Info_t *) methodData; 02195 return (info->wasPartialImage); 02196 } 02197 02213 void 02214 ImgImageAllowPartialImageIwls95(void *methodData, boolean value) 02215 { 02216 Iwls95Info_t *info = (Iwls95Info_t *) methodData; 02217 info->allowPartialImage = value; 02218 } 02219 02230 void 02231 ImgRestoreTransitionRelationIwls95(Img_ImageInfo_t *imageInfo, 02232 Img_DirectionType directionType) 02233 { 02234 array_t *relationArray; 02235 Iwls95Info_t *iwlsInfo = (Iwls95Info_t *) imageInfo->methodData; 02236 ImgFunctionData_t *functionData = &(imageInfo->functionData); 02237 mdd_manager *mgr = NIL(mdd_manager); 02238 02239 mgr = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork); 02240 02241 if (directionType == Img_Both_c) { 02242 fprintf(vis_stderr, 02243 "** img error : can't restore fwd and bwd at the same time.\n"); 02244 return; 02245 } 02246 02247 relationArray = ImgGetTransitionRelationIwls95(iwlsInfo, directionType); 02248 mdd_array_free(relationArray); 02249 ImgUpdateTransitionRelationIwls95(iwlsInfo, 02250 (array_t *)imageInfo->savedRelation, 02251 directionType); 02252 imageInfo->savedRelation = NIL(void); 02253 02254 assert(iwlsInfo->savedArraySmoothVarBddArray); 02255 if (directionType == Img_Forward_c) { 02256 mdd_array_array_free(iwlsInfo->fwdArraySmoothVarBddArray); 02257 iwlsInfo->fwdArraySmoothVarBddArray = iwlsInfo->savedArraySmoothVarBddArray; 02258 if (functionData->createVarCubesFlag) { 02259 mdd_array_free(iwlsInfo->fwdSmoothVarCubeArray); 02260 iwlsInfo->fwdSmoothVarCubeArray = iwlsInfo->savedSmoothVarCubeArray; 02261 } 02262 } else { 02263 mdd_array_array_free(iwlsInfo->bwdArraySmoothVarBddArray); 02264 iwlsInfo->bwdArraySmoothVarBddArray = iwlsInfo->savedArraySmoothVarBddArray; 02265 if (functionData->createVarCubesFlag) { 02266 mdd_array_free(iwlsInfo->bwdSmoothVarCubeArray); 02267 iwlsInfo->bwdSmoothVarCubeArray = iwlsInfo->savedSmoothVarCubeArray; 02268 } 02269 } 02270 iwlsInfo->savedArraySmoothVarBddArray = NIL(array_t); 02271 iwlsInfo->savedSmoothVarCubeArray = NIL(array_t); 02272 02273 if(directionType == Img_Backward_c || directionType == Img_Both_c) 02274 ResetClusteredCofactoredRelationArray(mgr, iwlsInfo); 02275 } 02276 02288 void 02289 ImgDuplicateTransitionRelationIwls95(Img_ImageInfo_t *imageInfo, 02290 Img_DirectionType directionType) 02291 { 02292 array_t *relationArray, *copiedRelationArray; 02293 Iwls95Info_t *iwlsInfo = (Iwls95Info_t *) imageInfo->methodData; 02294 ImgFunctionData_t *functionData = &(imageInfo->functionData); 02295 02296 if (directionType == Img_Both_c) { 02297 fprintf(vis_stderr, 02298 "** img error : can't duplicate fwd and bwd at the same time.\n"); 02299 return; 02300 } 02301 02302 relationArray = ImgGetTransitionRelationIwls95(iwlsInfo, directionType); 02303 copiedRelationArray = BddArrayDup(relationArray); 02304 assert(!imageInfo->savedRelation); 02305 imageInfo->savedRelation = (void *)relationArray; 02306 ImgUpdateTransitionRelationIwls95(iwlsInfo, 02307 copiedRelationArray, directionType); 02308 02309 assert(!iwlsInfo->savedArraySmoothVarBddArray); 02310 if (directionType == Img_Forward_c) { 02311 iwlsInfo->savedArraySmoothVarBddArray = iwlsInfo->fwdArraySmoothVarBddArray; 02312 iwlsInfo->fwdArraySmoothVarBddArray = 02313 CopyArrayBddArray(iwlsInfo->savedArraySmoothVarBddArray); 02314 if (functionData->createVarCubesFlag) { 02315 iwlsInfo->savedSmoothVarCubeArray = iwlsInfo->fwdSmoothVarCubeArray; 02316 iwlsInfo->fwdSmoothVarCubeArray = 02317 BddArrayDup(iwlsInfo->savedSmoothVarCubeArray); 02318 } 02319 } else { 02320 iwlsInfo->savedArraySmoothVarBddArray = iwlsInfo->bwdArraySmoothVarBddArray; 02321 iwlsInfo->bwdArraySmoothVarBddArray = 02322 CopyArrayBddArray(iwlsInfo->savedArraySmoothVarBddArray); 02323 if (functionData->createVarCubesFlag) { 02324 iwlsInfo->savedSmoothVarCubeArray = iwlsInfo->bwdSmoothVarCubeArray; 02325 iwlsInfo->bwdSmoothVarCubeArray = 02326 BddArrayDup(iwlsInfo->savedSmoothVarCubeArray); 02327 } 02328 } 02329 } 02330 02331 02355 void 02356 ImgMinimizeTransitionRelationIwls95( 02357 void *methodData, 02358 ImgFunctionData_t *functionData, 02359 array_t *constrainArray, 02360 Img_MinimizeType minimizeMethod, 02361 Img_DirectionType directionType, 02362 boolean reorderClusters, 02363 int printStatus) 02364 { 02365 Iwls95Info_t *info = (Iwls95Info_t *)methodData; 02366 02367 if (minimizeMethod == Img_DefaultMinimizeMethod_c) 02368 minimizeMethod = Img_ReadMinimizeMethod(); 02369 02370 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 02371 ImgMinimizeImageArrayWithCareSetArrayInSitu( 02372 info->fwdClusteredRelationArray, constrainArray, minimizeMethod, TRUE, 02373 (printStatus == 2), Img_Forward_c); 02374 02375 if(reorderClusters) 02376 ReorderPartitionedTransitionRelation(info, functionData, 02377 Img_Forward_c); 02378 else{ 02379 /* any minimization method other than restrict may introduce new 02380 variables, which invalidates the quantification schedule */ 02381 assert(minimizeMethod != Img_DefaultMinimizeMethod_c); 02382 if(minimizeMethod != Img_Restrict_c) 02383 UpdateQuantificationSchedule(info, functionData, Img_Forward_c); 02384 } 02385 assert(CheckQuantificationSchedule(info->fwdClusteredRelationArray, 02386 info->fwdArraySmoothVarBddArray)); 02387 } 02388 02389 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 02390 ImgMinimizeImageArrayWithCareSetArrayInSitu( 02391 info->bwdClusteredRelationArray, constrainArray, minimizeMethod, TRUE, 02392 (printStatus == 2), Img_Backward_c); 02393 02394 if(reorderClusters) 02395 ReorderPartitionedTransitionRelation(info, functionData, 02396 Img_Backward_c); 02397 /* Minimization can only introduce PS variables, which need not be 02398 quantified out, hence no need to recompute quantification schedule 02399 in backward case. */ 02400 assert(CheckQuantificationSchedule(info->bwdClusteredRelationArray, 02401 info->bwdArraySmoothVarBddArray)) 02402 } 02403 02404 if(directionType == Img_Backward_c || directionType == Img_Both_c) 02405 FreeClusteredCofactoredRelationArray(info); 02406 02407 return; 02408 } 02409 02410 02425 void 02426 ImgAbstractTransitionRelationIwls95(Img_ImageInfo_t *imageInfo, 02427 array_t *abstractVars, mdd_t *abstractCube, 02428 Img_DirectionType directionType, int printStatus) 02429 { 02430 Iwls95Info_t *info = (Iwls95Info_t *)imageInfo->methodData; 02431 int i, fwd_size, bwd_size; 02432 bdd_t *relation, *abstractedRelation; 02433 02434 if (!abstractVars || array_n(abstractVars) == 0) 02435 return; 02436 02437 fwd_size = bwd_size = 0; 02438 if (printStatus) { 02439 if (directionType == Img_Forward_c || directionType == Img_Both_c) 02440 fwd_size = bdd_size_multiple(info->fwdClusteredRelationArray); 02441 if (directionType == Img_Backward_c || directionType == Img_Both_c) 02442 bwd_size = bdd_size_multiple(info->bwdClusteredRelationArray); 02443 } 02444 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 02445 arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) { 02446 if (abstractCube) 02447 abstractedRelation = bdd_smooth_with_cube(relation, abstractCube); 02448 else 02449 abstractedRelation = bdd_smooth(relation, abstractVars); 02450 if (printStatus == 2) { 02451 (void) fprintf(vis_stdout, 02452 "IMG Info: abstracted fwd relation %d => %d in component %d\n", 02453 bdd_size(relation), bdd_size(abstractedRelation), i); 02454 } 02455 mdd_free(relation); 02456 array_insert(bdd_t*, info->fwdClusteredRelationArray, i, 02457 abstractedRelation); 02458 } 02459 } 02460 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 02461 arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) { 02462 if (abstractCube) 02463 abstractedRelation = bdd_smooth_with_cube(relation, abstractCube); 02464 else 02465 abstractedRelation = bdd_smooth(relation, abstractVars); 02466 if (printStatus == 2) { 02467 (void) fprintf(vis_stdout, 02468 "IMG Info: abstracted bwd relation %d => %d in component %d\n", 02469 bdd_size(relation), bdd_size(abstractedRelation), i); 02470 } 02471 mdd_free(relation); 02472 array_insert(bdd_t*, info->bwdClusteredRelationArray, i, 02473 abstractedRelation); 02474 } 02475 } 02476 if (printStatus) { 02477 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 02478 (void) fprintf(vis_stdout, 02479 "IMG Info: abstracted fwd relation [%d => %ld] with %d components\n", 02480 fwd_size, 02481 bdd_size_multiple(info->fwdClusteredRelationArray), 02482 array_n(info->fwdClusteredRelationArray)); 02483 } 02484 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 02485 (void) fprintf(vis_stdout, 02486 "IMG Info: abstracted bwd relation [%d => %ld] with %d components\n", 02487 bwd_size, 02488 bdd_size_multiple(info->bwdClusteredRelationArray), 02489 array_n(info->bwdClusteredRelationArray)); 02490 } 02491 } 02492 02493 if(directionType == Img_Backward_c || directionType == Img_Both_c) 02494 FreeClusteredCofactoredRelationArray(info); 02495 } 02496 02497 02510 int 02511 ImgApproximateTransitionRelationIwls95(mdd_manager *mgr, void *methodData, 02512 bdd_approx_dir_t approxDir, bdd_approx_type_t approxMethod, 02513 int approxThreshold, double approxQuality, 02514 double approxQualityBias, 02515 Img_DirectionType directionType, mdd_t *bias) 02516 { 02517 Iwls95Info_t *info = (Iwls95Info_t *)methodData; 02518 int i; 02519 bdd_t *relation, *approxRelation; 02520 int unchanged = 0; 02521 02522 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 02523 arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) { 02524 approxRelation = Img_ApproximateImage(mgr, relation, 02525 approxDir, approxMethod, 02526 approxThreshold, approxQuality, 02527 approxQualityBias, bias); 02528 if (bdd_is_tautology(approxRelation, 1)) { 02529 fprintf(vis_stdout, 02530 "** img warning : bdd_one from subsetting in fwd[%d].\n", i); 02531 mdd_free(approxRelation); 02532 unchanged++; 02533 } else if (bdd_is_tautology(approxRelation, 0)) { 02534 fprintf(vis_stdout, 02535 "** img warning : bdd_zero from subsetting in fwd[%d].\n", i); 02536 mdd_free(approxRelation); 02537 unchanged++; 02538 } else if (mdd_equal(approxRelation, relation)) { 02539 mdd_free(approxRelation); 02540 unchanged++; 02541 } else { 02542 mdd_free(relation); 02543 array_insert(bdd_t*, info->fwdClusteredRelationArray, i, 02544 approxRelation); 02545 } 02546 } 02547 } 02548 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 02549 arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) { 02550 approxRelation = Img_ApproximateImage(mgr, relation, 02551 approxDir, approxMethod, 02552 approxThreshold, approxQuality, 02553 approxQualityBias, bias); 02554 if (bdd_is_tautology(approxRelation, 1)) { 02555 fprintf(vis_stdout, 02556 "** img warning : bdd_one from subsetting in bwd[%d].\n", i); 02557 mdd_free(approxRelation); 02558 unchanged++; 02559 } else if (bdd_is_tautology(approxRelation, 0)) { 02560 fprintf(vis_stdout, 02561 "** img warning : bdd_zero from subsetting in bwd[%d].\n", i); 02562 mdd_free(approxRelation); 02563 unchanged++; 02564 } else if (mdd_equal(approxRelation, relation)) { 02565 mdd_free(approxRelation); 02566 unchanged++; 02567 } else { 02568 mdd_free(relation); 02569 array_insert(bdd_t*, info->bwdClusteredRelationArray, i, 02570 approxRelation); 02571 } 02572 } 02573 } 02574 02575 if(directionType == Img_Backward_c || directionType == Img_Both_c) 02576 FreeClusteredCofactoredRelationArray(info); 02577 02578 return(unchanged); 02579 } 02580 02581 02591 array_t * 02592 ImgGetTransitionRelationIwls95(void *methodData, 02593 Img_DirectionType directionType) 02594 { 02595 Iwls95Info_t *info = (Iwls95Info_t *)methodData; 02596 02597 if (directionType == Img_Forward_c) 02598 return(info->fwdClusteredRelationArray); 02599 else if (directionType == Img_Backward_c) 02600 return(info->bwdClusteredRelationArray); 02601 return(NIL(array_t)); 02602 } 02603 02604 02614 void 02615 ImgUpdateTransitionRelationIwls95(void *methodData, array_t *relationArray, 02616 Img_DirectionType directionType) 02617 { 02618 Iwls95Info_t *info = (Iwls95Info_t *)methodData; 02619 02620 if (directionType == Img_Forward_c) 02621 info->fwdClusteredRelationArray = relationArray; 02622 else if (directionType == Img_Backward_c) 02623 info->bwdClusteredRelationArray = relationArray; 02624 } 02625 02626 02636 void 02637 ImgReplaceIthPartitionedTransitionRelationIwls95(void *methodData, 02638 int i, mdd_t *relation, Img_DirectionType directionType) 02639 { 02640 array_t *relationArray; 02641 mdd_t *old; 02642 02643 relationArray = ImgGetTransitionRelationIwls95(methodData, directionType); 02644 if (!relationArray) 02645 return; 02646 old = array_fetch(mdd_t *, relationArray, i); 02647 mdd_free(old); 02648 array_insert(mdd_t *, relationArray, i, relation); 02649 } 02650 02651 02663 void 02664 ImgImageFreeClusteredTransitionRelationIwls95(void *methodData, 02665 Img_DirectionType directionType) 02666 { 02667 Iwls95Info_t *info = (Iwls95Info_t *)methodData; 02668 02669 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 02670 if (info->fwdClusteredRelationArray != NIL(array_t)) { 02671 mdd_array_free(info->fwdClusteredRelationArray); 02672 info->fwdClusteredRelationArray = NIL(array_t); 02673 } 02674 if (info->fwdArraySmoothVarBddArray != NIL(array_t)) { 02675 mdd_array_array_free(info->fwdArraySmoothVarBddArray); 02676 info->fwdArraySmoothVarBddArray = NIL(array_t); 02677 } 02678 if (info->fwdSmoothVarCubeArray != NIL(array_t)) { 02679 mdd_array_free(info->fwdSmoothVarCubeArray); 02680 info->fwdSmoothVarCubeArray = NIL(array_t); 02681 } 02682 } 02683 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 02684 if (info->bwdClusteredRelationArray != NIL(array_t)) { 02685 mdd_array_free(info->bwdClusteredRelationArray); 02686 info->bwdClusteredRelationArray = NIL(array_t); 02687 } 02688 if (info->bwdArraySmoothVarBddArray != NIL(array_t)) { 02689 mdd_array_array_free(info->bwdArraySmoothVarBddArray); 02690 info->bwdArraySmoothVarBddArray = NIL(array_t); 02691 } 02692 if (info->bwdSmoothVarCubeArray != NIL(array_t)) { 02693 mdd_array_free(info->bwdSmoothVarCubeArray); 02694 info->bwdSmoothVarCubeArray = NIL(array_t); 02695 } 02696 } 02697 } 02698 02699 02700 02728 void 02729 ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp( 02730 Img_ImageInfo_t *imageInfo, 02731 Img_DirectionType direction, 02732 mdd_t *constrain, 02733 Img_MinimizeType minimizeMethod, 02734 boolean underApprox, 02735 boolean cleanUp, 02736 boolean forceReorder, 02737 int printStatus) 02738 { 02739 ImgFunctionData_t *functionData = &(imageInfo->functionData); 02740 Iwls95Info_t *info = (Iwls95Info_t *)imageInfo->methodData; 02741 array_t *constrainArray; 02742 mdd_manager *mddManager = Part_PartitionReadMddManager(functionData->mddNetwork); 02743 array_t *relationArray = NIL(array_t); 02744 array_t *relationArrayFwd = NIL(array_t); 02745 array_t *relationArrayBwd = NIL(array_t); 02746 02747 assert(imageInfo->methodType == Img_Iwls95_c || 02748 imageInfo->methodType == Img_Mlp_c); 02749 02750 /* free existing relation */ 02751 ImgImageFreeClusteredTransitionRelationIwls95(imageInfo->methodData, 02752 direction); 02753 if (forceReorder) bdd_reorder(mddManager); 02754 /* create a bit relation and quantifiable variables (PIs and 02755 intermediate variables) if necessary */ 02756 CreateBitRelationArray(info, functionData); 02757 02758 /* make a work copy of the bit array */ 02759 relationArray = BddArrayDup(info->bitRelationArray); 02760 02761 if (cleanUp) FreeBitRelationArray(info); 02762 02763 /* apply the constraint to the bit relation */ 02764 if (constrain) { 02765 constrainArray = array_alloc(mdd_t *, 1); 02766 array_insert(mdd_t *, constrainArray, 0, constrain); 02767 ImgMinimizeImageArrayWithCareSetArrayInSitu(relationArray, 02768 constrainArray, 02769 minimizeMethod, underApprox, 02770 printStatus, direction); 02771 array_free(constrainArray); 02772 } 02773 02774 if (direction == Img_Forward_c) { 02775 relationArrayFwd = relationArray; 02776 } else if (direction == Img_Backward_c) { 02777 relationArrayBwd = relationArray; 02778 } else if (direction == Img_Both_c) { 02779 relationArrayFwd = relationArray; 02780 relationArrayBwd = BddArrayDup(relationArray); 02781 } else { 02782 assert(0); 02783 } 02784 relationArray = NIL(array_t); 02785 02786 /* return order and recluster the relation */ 02787 if (direction == Img_Forward_c || direction == Img_Both_c) { 02788 Img_ClusterRelationArray(mddManager, 02789 imageInfo->methodType, 02790 direction, 02791 relationArrayFwd, 02792 functionData->domainVars, 02793 functionData->rangeVars, 02794 info->quantifyVarMddIdArray, 02795 &info->fwdClusteredRelationArray, 02796 &info->fwdArraySmoothVarBddArray, 02797 NULL, 02798 1); 02799 if (functionData->createVarCubesFlag) { 02800 info->fwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 02801 info->fwdArraySmoothVarBddArray); 02802 } 02803 } 02804 02805 if (direction == Img_Backward_c || direction == Img_Both_c) { 02806 Img_ClusterRelationArray(mddManager, 02807 imageInfo->methodType, 02808 direction, 02809 relationArrayBwd, 02810 functionData->domainVars, 02811 functionData->rangeVars, 02812 info->quantifyVarMddIdArray, 02813 &info->bwdClusteredRelationArray, 02814 &info->bwdArraySmoothVarBddArray, 02815 NULL, 02816 1); 02817 if (functionData->createVarCubesFlag) { 02818 info->bwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 02819 info->bwdArraySmoothVarBddArray); 02820 } 02821 } 02822 02823 if (cleanUp) { 02824 array_free(info->quantifyVarMddIdArray); 02825 info->quantifyVarMddIdArray = NIL(array_t); 02826 } 02827 02828 /* Print information */ 02829 if (info->option->verbosity > 0){ 02830 fprintf(vis_stdout,"Computing Image Using %s technique.\n", 02831 imageInfo->methodType == Img_Mlp_c ? "MLP" : "IWLS95"); 02832 fprintf(vis_stdout,"Total # of domain binary variables = %3d\n", 02833 array_n(functionData->domainBddVars)); 02834 fprintf(vis_stdout,"Total # of range binary variables = %3d\n", 02835 array_n(functionData->rangeBddVars)); 02836 if (info->quantifyVarMddIdArray) { 02837 array_t *bddArray; 02838 02839 bddArray = mdd_id_array_to_bdd_array(mddManager, 02840 info->quantifyVarMddIdArray); 02841 fprintf(vis_stdout,"Total # of quantify binary variables = %3d\n", 02842 array_n(bddArray)); 02843 mdd_array_free(bddArray); 02844 } else { 02845 fprintf(vis_stdout,"Total # of quantify binary variables = %3d\n", 02846 array_n(functionData->quantifyBddVars)); 02847 } 02848 if (((direction == Img_Forward_c) || (direction == Img_Both_c)) && 02849 (info->fwdClusteredRelationArray != NIL(array_t))) { 02850 (void) fprintf(vis_stdout, 02851 "Shared size of transition relation for forward image "); 02852 (void) fprintf(vis_stdout, 02853 "computation is %10ld BDD nodes (%-4d components)\n", 02854 bdd_size_multiple(info->fwdClusteredRelationArray), 02855 array_n(info->fwdClusteredRelationArray)); 02856 } 02857 if (((direction == Img_Backward_c) || (direction == Img_Both_c)) && 02858 (info->bwdClusteredRelationArray != NIL(array_t))) { 02859 (void) fprintf(vis_stdout, 02860 "Shared size of transition relation for backward image "); 02861 (void) fprintf(vis_stdout, 02862 "computation is %10ld BDD nodes (%-4d components)\n", 02863 bdd_size_multiple(info->bwdClusteredRelationArray), 02864 array_n(info->bwdClusteredRelationArray)); 02865 } 02866 }/* if verbosity > 0 */ 02867 02868 if(direction == Img_Backward_c || direction == Img_Both_c) 02869 ResetClusteredCofactoredRelationArray(mddManager, info); 02870 } 02871 02872 02873 02883 void 02884 ImgPrintIntegerArray(array_t *idArray) 02885 { 02886 int i; 02887 fprintf(vis_stdout, 02888 "**************** printing bdd ids from the bdd array ***********\n"); 02889 fprintf(vis_stdout,"%d::\t", array_n(idArray)); 02890 for (i=0;i<array_n(idArray); i++) { 02891 fprintf(vis_stdout," %d ", array_fetch(int, idArray, i)); 02892 } 02893 } 02894 02895 02905 void 02906 ImgPrintPartition(graph_t *partition) 02907 { 02908 vertex_t *vertex; 02909 lsList vertexList = g_get_vertices(partition); 02910 lsGen gen; 02911 st_table *vertexTable = st_init_table(st_ptrcmp, st_ptrhash); 02912 fprintf(vis_stdout,"\n"); 02913 lsForEachItem(vertexList, gen, vertex) { 02914 if (lsLength(g_get_out_edges(vertex)) == 0) 02915 PrintPartitionRecursively(vertex,vertexTable,0); 02916 } 02917 st_free_table(vertexTable); 02918 } 02919 02920 02930 void 02931 ImgPrintPartitionedTransitionRelation(mdd_manager *mddManager, 02932 array_t *relationArray, 02933 array_t *arraySmoothVarBddArray) 02934 { 02935 int i, j, n; 02936 mdd_t *relation; 02937 mdd_t *bdd; 02938 array_t *smoothVarBddArray; 02939 array_t *bvar_list = mdd_ret_bvar_list(mddManager); 02940 var_set_t *vset; 02941 bvar_type bv; 02942 02943 n = array_n(relationArray); 02944 02945 fprintf(vis_stdout, "# of relations = %d\n", n); 02946 if (arraySmoothVarBddArray) { 02947 smoothVarBddArray = array_fetch(array_t *, arraySmoothVarBddArray, 0); 02948 fprintf(vis_stdout, "Early smooth(%d) = ", array_n(smoothVarBddArray)); 02949 for (j = 0; j < array_n(smoothVarBddArray); j++) { 02950 bdd = array_fetch(mdd_t *, smoothVarBddArray, j); 02951 mdd_print_support_to_file(vis_stdout, " %s", bdd); 02952 } 02953 fprintf(vis_stdout, "\n"); 02954 } 02955 for (i = 0; i < n; i++) { 02956 relation = array_fetch(mdd_t *, relationArray, i); 02957 fprintf(vis_stdout, "T[%d] : bdd_size = %d\n", i, bdd_size(relation)); 02958 fprintf(vis_stdout, " support(%d) = ", 02959 mdd_get_number_of_bdd_support(mddManager, relation)); 02960 vset = bdd_get_support(relation); 02961 for (j = 0; j < array_n(bvar_list); j++) { 02962 if (var_set_get_elt(vset, j) == 1) { 02963 bv = array_fetch(bvar_type, bvar_list, j); 02964 mdd_print_support_to_file(vis_stdout, " %s", bv.node); 02965 } 02966 } 02967 var_set_free(vset); 02968 fprintf(vis_stdout, "\n"); 02969 if (arraySmoothVarBddArray) { 02970 smoothVarBddArray = array_fetch(array_t *, arraySmoothVarBddArray, i + 1); 02971 fprintf(vis_stdout, " smooth(%d) = ", array_n(smoothVarBddArray)); 02972 for (j = 0; j < array_n(smoothVarBddArray); j++) { 02973 bdd = array_fetch(mdd_t *, smoothVarBddArray, j); 02974 mdd_print_support_to_file(vis_stdout, " %s", bdd); 02975 } 02976 fprintf(vis_stdout, "\n"); 02977 } 02978 } 02979 } 02980 02981 02995 mdd_t * 02996 ImgTrmEliminateDependVars(ImgFunctionData_t *functionData, 02997 array_t *relationArray, 02998 mdd_t *states, mdd_t **dependRelations, 02999 int *nDependVars) 03000 { 03001 int i, j; 03002 int howMany = 0; /* number of latches that can be eliminated */ 03003 mdd_t *var, *newStates, *abs, *positive, *phi, *tmp, *relation; 03004 int nSupports; /* vars in the support of the state set */ 03005 int *candidates; /* vars to be considered for elimination */ 03006 double minStates; 03007 var_set_t *supportVarSet; 03008 graph_t *mddNetwork; 03009 mdd_manager *mddManager; 03010 03011 mddNetwork = functionData->mddNetwork; 03012 mddManager = Part_PartitionReadMddManager(mddNetwork); 03013 03014 if (dependRelations) 03015 *dependRelations = mdd_one(mddManager); 03016 newStates = mdd_dup(states); 03017 03018 nSupports = 0; 03019 supportVarSet = bdd_get_support(newStates); 03020 for (i = 0; i < supportVarSet->n_elts; i++) { 03021 if (var_set_get_elt(supportVarSet, i) == 1) 03022 nSupports++; 03023 } 03024 candidates = ALLOC(int, nSupports); 03025 if (candidates == NULL) { 03026 var_set_free(supportVarSet); 03027 return(NULL); 03028 } 03029 nSupports = 0; 03030 for (i = 0; i < supportVarSet->n_elts; i++) { 03031 if (var_set_get_elt(supportVarSet, i) == 1) { 03032 candidates[nSupports] = i; 03033 nSupports++; 03034 } 03035 } 03036 var_set_free(supportVarSet); 03037 03038 /* The signatures of the variables in a function are the number 03039 ** of minterms of the positive cofactors with respect to the 03040 ** variables themselves. */ 03041 signatures = bdd_cof_minterm(newStates); 03042 if (signatures == NULL) { 03043 FREE(candidates); 03044 return(NULL); 03045 } 03046 /* We now extract a positive quantity which is higher for those 03047 ** variables that are closer to being essential. */ 03048 minStates = signatures[nSupports]; 03049 for (i = 0; i < nSupports; i++) { 03050 double z = signatures[i] / minStates - 1.0; 03051 signatures[i] = (z < 0.0) ? -z : z; /* make positive */ 03052 } 03053 qsort((void *)candidates, nSupports, sizeof(int), 03054 (int (*)(const void *, const void *))TrmSignatureCompare); 03055 FREE(signatures); 03056 03057 /* Now process the candidates in the given order. */ 03058 for (i = 0; i < nSupports; i++) { 03059 var = bdd_var_with_index(mddManager, candidates[i]); 03060 if (bdd_var_is_dependent(newStates, var)) { 03061 abs = bdd_smooth_with_cube(newStates, var); 03062 if (abs == NULL) 03063 return(NULL); 03064 positive = bdd_cofactor(newStates, var); 03065 if (positive == NULL) 03066 return(NULL); 03067 phi = Img_MinimizeImage(positive, abs, Img_DefaultMinimizeMethod_c, 1); 03068 if (phi == NULL) 03069 return(NULL); 03070 mdd_free(positive); 03071 if (bdd_size(phi) < IMG_MAX_DEP_SIZE) { 03072 howMany++; 03073 for (j = 0; j < array_n(relationArray); j++) { 03074 relation = array_fetch(mdd_t *, relationArray, j); 03075 if (dependRelations) 03076 tmp = bdd_smooth_with_cube(relation, var); 03077 else 03078 tmp = bdd_compose(relation, var, phi); 03079 mdd_free(relation); 03080 array_insert(mdd_t *, relationArray, j, tmp); 03081 } 03082 mdd_free(newStates); 03083 newStates = abs; 03084 if (dependRelations) { 03085 relation = mdd_xnor(var, phi); 03086 tmp = ImgSubstitute(relation, functionData, Img_R2D_c); 03087 mdd_free(relation); 03088 relation = mdd_and(*dependRelations, tmp, 1, 1); 03089 mdd_free(*dependRelations); 03090 *dependRelations = relation; 03091 } 03092 } else { 03093 mdd_free(abs); 03094 } 03095 mdd_free(phi); 03096 } 03097 } 03098 FREE(candidates); 03099 03100 *nDependVars = howMany; 03101 return(newStates); 03102 } /* end of ImgTrmEliminateDependVars */ 03103 03104 03105 /*---------------------------------------------------------------------------*/ 03106 /* Definition of static functions */ 03107 /*---------------------------------------------------------------------------*/ 03108 03121 static void 03122 ResetClusteredCofactoredRelationArray( 03123 mdd_manager *mddManager, 03124 Iwls95Info_t *info) 03125 { 03126 int i; 03127 mdd_t *cluster; 03128 03129 assert(info->bwdClusteredRelationArray != NIL(array_t)); 03130 03131 FreeClusteredCofactoredRelationArray(info); 03132 03133 info->careSetArray = array_alloc(mdd_t *, 1); 03134 array_insert_last(mdd_t *, info->careSetArray, mdd_one(mddManager)); 03135 info->bwdClusteredCofactoredRelationArray = array_alloc(mdd_t *, 0); 03136 03137 arrayForEachItem(mdd_t *, info->bwdClusteredRelationArray, i, cluster){ 03138 array_insert_last(mdd_t *, info->bwdClusteredCofactoredRelationArray, 03139 mdd_dup(cluster)); 03140 } 03141 } 03142 03143 03155 static void 03156 FreeClusteredCofactoredRelationArray( 03157 Iwls95Info_t *info) 03158 { 03159 /* one should only be NIL if the other is, too */ 03160 assert((info->bwdClusteredCofactoredRelationArray != NIL(array_t)) == 03161 (info->careSetArray != NIL(array_t))); 03162 03163 if(info->bwdClusteredCofactoredRelationArray == NIL(array_t)) 03164 return; 03165 03166 mdd_array_free(info->bwdClusteredCofactoredRelationArray); 03167 info->bwdClusteredCofactoredRelationArray = NIL(array_t); 03168 mdd_array_free(info->careSetArray); 03169 info->careSetArray = NIL(array_t); 03170 } 03171 03172 03185 static ImgTrmOption_t * 03186 TrmGetOptions(void) 03187 { 03188 char *flagValue; 03189 ImgTrmOption_t *option; 03190 03191 option = ALLOC(ImgTrmOption_t, 1); 03192 03193 flagValue = Cmd_FlagReadByName("image_cluster_size"); 03194 if (flagValue == NIL(char)) { 03195 option->clusterSize = 5000; /* the default value */ 03196 } 03197 else { 03198 option->clusterSize = atoi(flagValue); 03199 } 03200 03201 flagValue = Cmd_FlagReadByName("image_verbosity"); 03202 if (flagValue == NIL(char)) { 03203 option->verbosity = 0; /* the default value */ 03204 } 03205 else { 03206 option->verbosity = atoi(flagValue); 03207 } 03208 03209 flagValue = Cmd_FlagReadByName("image_W1"); 03210 if (flagValue == NIL(char)) { 03211 option->W1 = 6; /* the default value */ 03212 } 03213 else { 03214 option->W1 = atoi(flagValue); 03215 } 03216 03217 flagValue = Cmd_FlagReadByName("image_W2"); 03218 if (flagValue == NIL(char)) { 03219 option->W2 = 1; /* the default value */ 03220 } 03221 else { 03222 option->W2 = atoi(flagValue); 03223 } 03224 03225 flagValue = Cmd_FlagReadByName("image_W3"); 03226 if (flagValue == NIL(char)) { 03227 option->W3 = 1; /* the default value */ 03228 } 03229 else { 03230 option->W3 = atoi(flagValue); 03231 } 03232 03233 flagValue = Cmd_FlagReadByName("image_W4"); 03234 if (flagValue == NIL(char)) { 03235 option->W4 = 2; /* the default value */ 03236 } 03237 else { 03238 option->W4 = atoi(flagValue); 03239 } 03240 03241 flagValue = Cmd_FlagReadByName("image_print_depend_matrix"); 03242 if (flagValue == NIL(char)) { 03243 option->printDepMatrix = 0; /* the default value */ 03244 } 03245 else { 03246 option->printDepMatrix = atoi(flagValue); 03247 } 03248 03249 03250 flagValue = Cmd_FlagReadByName("mlp_method"); 03251 if (flagValue == NIL(char)) { 03252 option->mlpMethod = 0; /* the default value */ 03253 } 03254 else { 03255 option->mlpMethod = atoi(flagValue); 03256 } 03257 03258 flagValue = Cmd_FlagReadByName("mlp_cluster"); 03259 if (flagValue == NIL(char)) { 03260 option->mlpCluster = 1; /* the default value */ 03261 } 03262 else { 03263 option->mlpCluster = atoi(flagValue); 03264 } 03265 03266 flagValue = Cmd_FlagReadByName("mlp_cluster_dynamic"); 03267 if (flagValue == NIL(char)) { 03268 option->mlpClusterDynamic = 1; /* the default value */ 03269 } 03270 else { 03271 option->mlpClusterDynamic = atoi(flagValue); 03272 } 03273 03274 flagValue = Cmd_FlagReadByName("mlp_affinity_threshold"); 03275 if (flagValue == NIL(char)) { 03276 option->mlpAffinityThreshold = 0.0; /* the default value */ 03277 } 03278 else { 03279 sscanf(flagValue, "%f", &option->mlpAffinityThreshold); 03280 } 03281 03282 flagValue = Cmd_FlagReadByName("mlp_cluster_quantify_vars"); 03283 if (flagValue == NIL(char)) { 03284 option->mlpClusterQuantifyVars = 0; /* the default value */ 03285 } 03286 else { 03287 option->mlpClusterQuantifyVars = atoi(flagValue); 03288 } 03289 03290 flagValue = Cmd_FlagReadByName("mlp_cluster_sorted_list"); 03291 if (flagValue == NIL(char)) { 03292 option->mlpClusterSortedList = 1; /* the default value */ 03293 } 03294 else { 03295 option->mlpClusterSortedList = atoi(flagValue); 03296 } 03297 03298 flagValue = Cmd_FlagReadByName("mlp_initial_cluster"); 03299 if (flagValue == NIL(char)) { 03300 option->mlpInitialCluster = 0; /* the default value */ 03301 } 03302 else { 03303 option->mlpInitialCluster = atoi(flagValue); 03304 } 03305 03306 flagValue = Cmd_FlagReadByName("mlp_cs_first"); 03307 if (flagValue == NIL(char)) { 03308 option->mlpCsFirst = 0; /* the default value */ 03309 } 03310 else { 03311 option->mlpCsFirst = atoi(flagValue); 03312 } 03313 03314 flagValue = Cmd_FlagReadByName("mlp_skip_rs"); 03315 if (flagValue == NIL(char)) { 03316 option->mlpSkipRs = 0; /* the default value */ 03317 } 03318 else { 03319 option->mlpSkipRs = atoi(flagValue); 03320 } 03321 03322 flagValue = Cmd_FlagReadByName("mlp_skip_cs"); 03323 if (flagValue == NIL(char)) { 03324 option->mlpSkipCs = 1; /* the default value */ 03325 } 03326 else { 03327 option->mlpSkipCs = atoi(flagValue); 03328 } 03329 03330 flagValue = Cmd_FlagReadByName("mlp_row_based"); 03331 if (flagValue == NIL(char)) { 03332 option->mlpRowBased = 0; /* the default value */ 03333 } 03334 else { 03335 option->mlpRowBased = atoi(flagValue); 03336 } 03337 03338 flagValue = Cmd_FlagReadByName("mlp_reorder"); 03339 if (flagValue == NIL(char)) { 03340 option->mlpReorder = 0; /* the default value */ 03341 } 03342 else { 03343 option->mlpReorder = atoi(flagValue); 03344 } 03345 03346 flagValue = Cmd_FlagReadByName("mlp_pre_reorder"); 03347 if (flagValue == NIL(char)) { 03348 option->mlpPreReorder = 0; /* the default value */ 03349 } 03350 else { 03351 option->mlpPreReorder = atoi(flagValue); 03352 } 03353 03354 flagValue = Cmd_FlagReadByName("mlp_postprocess"); 03355 if (flagValue == NIL(char)) { 03356 option->mlpPostProcess = 0; /* the default value */ 03357 } 03358 else { 03359 option->mlpPostProcess = atoi(flagValue); 03360 } 03361 03362 flagValue = Cmd_FlagReadByName("mlp_decompose_scc"); 03363 if (flagValue == NIL(char)) { 03364 option->mlpDecomposeScc = 1; /* the default value */ 03365 } 03366 else { 03367 option->mlpDecomposeScc = atoi(flagValue); 03368 } 03369 03370 flagValue = Cmd_FlagReadByName("mlp_cluster_scc"); 03371 if (flagValue == NIL(char)) { 03372 option->mlpClusterScc = 1; /* the default value */ 03373 } 03374 else { 03375 option->mlpClusterScc = atoi(flagValue); 03376 } 03377 03378 flagValue = Cmd_FlagReadByName("mlp_sort_scc"); 03379 if (flagValue == NIL(char)) { 03380 option->mlpSortScc = 1; /* the default value */ 03381 } 03382 else { 03383 option->mlpSortScc = atoi(flagValue); 03384 } 03385 03386 flagValue = Cmd_FlagReadByName("mlp_sort_scc_mode"); 03387 if (flagValue == NIL(char)) { 03388 option->mlpSortSccMode = 2; /* the default value */ 03389 } 03390 else { 03391 option->mlpSortSccMode = atoi(flagValue); 03392 } 03393 03394 flagValue = Cmd_FlagReadByName("mlp_cluster_merge"); 03395 if (flagValue == NIL(char)) { 03396 option->mlpClusterMerge = 0; /* the default value */ 03397 } 03398 else { 03399 option->mlpClusterMerge = atoi(flagValue); 03400 } 03401 03402 flagValue = Cmd_FlagReadByName("mlp_multiway"); 03403 if (flagValue == NIL(char)) { 03404 option->mlpMultiway = 0; /* the default value */ 03405 } 03406 else { 03407 option->mlpMultiway = atoi(flagValue); 03408 } 03409 03410 flagValue = Cmd_FlagReadByName("mlp_lambda_mode"); 03411 if (flagValue == NIL(char)) { 03412 option->mlpLambdaMode = 0; /* the default value */ 03413 } 03414 else { 03415 option->mlpLambdaMode = atoi(flagValue); 03416 } 03417 03418 flagValue = Cmd_FlagReadByName("mlp_sorted_rows"); 03419 if (flagValue == NIL(char)) { 03420 option->mlpSortedRows = 1; /* the default value */ 03421 } 03422 else { 03423 option->mlpSortedRows = atoi(flagValue); 03424 } 03425 03426 flagValue = Cmd_FlagReadByName("mlp_sorted_cols"); 03427 if (flagValue == NIL(char)) { 03428 option->mlpSortedCols = 1; /* the default value */ 03429 } 03430 else { 03431 option->mlpSortedCols = atoi(flagValue); 03432 } 03433 03434 flagValue = Cmd_FlagReadByName("mlp_pre_swap_state_vars"); 03435 if (flagValue == NIL(char)) { 03436 option->mlpPreSwapStateVars = 0; /* the default value */ 03437 } 03438 else { 03439 option->mlpPreSwapStateVars = atoi(flagValue); 03440 } 03441 03442 flagValue = Cmd_FlagReadByName("mlp_print_matrix"); 03443 if (flagValue == NIL(char)) { 03444 option->mlpPrintMatrix = 0; /* the default value */ 03445 } 03446 else { 03447 option->mlpPrintMatrix = atoi(flagValue); 03448 } 03449 03450 flagValue = Cmd_FlagReadByName("mlp_write_order"); 03451 if (flagValue == NIL(char)) { 03452 option->mlpWriteOrder = NIL(char); /* the default value */ 03453 } 03454 else { 03455 option->mlpWriteOrder = util_strsav(flagValue); 03456 } 03457 03458 flagValue = Cmd_FlagReadByName("mlp_verbosity"); 03459 if (flagValue == NIL(char)) { 03460 option->mlpVerbosity = 0; /* the default value */ 03461 } 03462 else { 03463 option->mlpVerbosity = atoi(flagValue); 03464 } 03465 03466 flagValue = Cmd_FlagReadByName("mlp_debug"); 03467 if (flagValue == NIL(char)) { 03468 option->mlpDebug = 0; /* the default value */ 03469 } 03470 else { 03471 option->mlpDebug = atoi(flagValue); 03472 } 03473 03474 flagValue = Cmd_FlagReadByName("image_read_reorder_cluster"); 03475 if (flagValue == NIL(char)) { 03476 option->readReorderCluster = 0; /* the default value */ 03477 } 03478 else { 03479 option->readReorderCluster = atoi(flagValue); 03480 } 03481 03482 flagValue = Cmd_FlagReadByName("image_read_cluster"); 03483 if (flagValue == NIL(char)) { 03484 option->readCluster = NIL(char); /* the default value */ 03485 } 03486 else { 03487 option->readCluster = util_strsav(flagValue); 03488 } 03489 03490 flagValue = Cmd_FlagReadByName("image_write_cluster"); 03491 if (flagValue == NIL(char)) { 03492 option->writeCluster = NIL(char); /* the default value */ 03493 } 03494 else { 03495 option->writeCluster = util_strsav(flagValue); 03496 } 03497 03498 flagValue = Cmd_FlagReadByName("image_write_depend_matrix"); 03499 if (flagValue == NIL(char)) { 03500 option->writeDepMatrix = NIL(char); /* the default value */ 03501 } 03502 else { 03503 option->writeDepMatrix = util_strsav(flagValue); 03504 } 03505 03506 flagValue = Cmd_FlagReadByName("linear_grain_type"); 03507 if (flagValue == NIL(char)) { 03508 option->linearFineGrainFlag = 0; /* the default value */ 03509 } 03510 else { 03511 option->linearFineGrainFlag = 1; 03512 } 03513 03514 flagValue = Cmd_FlagReadByName("linear_optimize"); 03515 if (flagValue == NIL(char)) { 03516 option->linearOptimize = Opt_None; /* the default value */ 03517 } 03518 else { 03519 option->linearOptimize = Opt_NS; 03520 } 03521 03522 option->linearOrderVariable = 0; 03523 flagValue = Cmd_FlagReadByName("linear_order_variable"); 03524 if (flagValue == NIL(char)) { 03525 option->linearOrderVariable = 0; /* the default value */ 03526 } 03527 else { 03528 option->linearOrderVariable = 1; 03529 } 03530 03531 option->linearGroupStateVariable = 0; 03532 flagValue = Cmd_FlagReadByName("linear_group_state_variable"); 03533 if (flagValue == NIL(char)) { 03534 option->linearGroupStateVariable = 0; /* the default value */ 03535 } 03536 else { 03537 option->linearGroupStateVariable = 1; 03538 } 03539 03540 option->linearIncludeCS = 1; 03541 option->linearIncludeNS = 1; 03542 option->linearQuantifyCS = 0; 03543 option->linearComputeRange = 0; 03544 flagValue = Cmd_FlagReadByName("linear_exclude_cs"); 03545 if (flagValue) option->linearIncludeCS = 0; 03546 flagValue = Cmd_FlagReadByName("linear_exclude_ns"); 03547 if (flagValue) option->linearIncludeNS = 0; 03548 03549 return option; 03550 } 03551 03572 static void 03573 CreateBitRelationArray(Iwls95Info_t *info, ImgFunctionData_t *functionData) 03574 { 03575 array_t *bddRelationArray = NIL(array_t); 03576 array_t *domainVarMddIdArray = functionData->domainVars; 03577 array_t *rangeVarMddIdArray = functionData->rangeVars; 03578 array_t *quantifyVarMddIdArray = NIL(array_t); 03579 graph_t *mddNetwork = functionData->mddNetwork; 03580 array_t *roots = functionData->roots; 03581 int i; 03582 int n1, n2, nIntermediateVars = 0; 03583 mdd_manager *mddManager = NIL(mdd_manager); 03584 st_table *vertexTable = NIL(st_table); 03585 st_table *domainQuantifyVarMddIdTable = NIL(st_table); 03586 int mddId; 03587 char *nodeName; 03588 03589 if (info->bitRelationArray != NIL(array_t)) { 03590 assert(info->quantifyVarMddIdArray != NIL(array_t)); 03591 return; 03592 } 03593 03594 bddRelationArray = array_alloc(mdd_t*, 0); 03595 quantifyVarMddIdArray = array_dup(functionData->quantifyVars); 03596 mddManager = Part_PartitionReadMddManager(mddNetwork); 03597 vertexTable = st_init_table(st_ptrcmp, st_ptrhash); 03598 domainQuantifyVarMddIdTable = st_init_table(st_numcmp, st_numhash); 03599 03600 arrayForEachItem(int, domainVarMddIdArray, i, mddId) { 03601 st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char)); 03602 } 03603 arrayForEachItem(int, quantifyVarMddIdArray, i, mddId) { 03604 st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char)); 03605 } 03606 03607 arrayForEachItem(char *, roots, i, nodeName) { 03608 vertex_t *vertex = Part_PartitionFindVertexByName(mddNetwork, nodeName); 03609 Mvf_Function_t *mvf = Part_VertexReadFunction(vertex); 03610 int mddId = array_fetch(int, rangeVarMddIdArray, i); 03611 03612 /*mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);*/ 03613 array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, 03614 mddId, mvf); 03615 array_append(bddRelationArray, varBddRelationArray); 03616 array_free(varBddRelationArray); 03617 /*array_insert_last(mdd_t *, bddRelationArray, relation);*/ 03618 if (info->option->verbosity) 03619 n1 = array_n(bddRelationArray); 03620 else /* to remove uninitialized variable warning */ 03621 n1 = 0; 03622 PartitionTraverseRecursively(mddManager, vertex, -1, vertexTable, 03623 bddRelationArray, 03624 domainQuantifyVarMddIdTable, 03625 quantifyVarMddIdArray); 03626 if (info->option->verbosity) { 03627 n2 = array_n(bddRelationArray); 03628 nIntermediateVars += n2 - n1; 03629 } 03630 } 03631 if (info->option->verbosity) { 03632 (void)fprintf(vis_stdout, "** img info: %d intermediate variables\n", 03633 nIntermediateVars); 03634 } 03635 st_free_table(vertexTable); 03636 st_free_table(domainQuantifyVarMddIdTable); 03637 info->bitRelationArray = bddRelationArray; 03638 info->quantifyVarMddIdArray = quantifyVarMddIdArray; 03639 return; 03640 03641 } 03642 03653 static void 03654 FreeBitRelationArray (Iwls95Info_t *info) 03655 { 03656 mdd_array_free(info->bitRelationArray); 03657 info->bitRelationArray = NIL(array_t); 03658 return; 03659 } 03660 03661 03662 03691 static void 03692 OrderClusterOrder(mdd_manager *mddManager, 03693 array_t *relationArray, 03694 array_t *fromVarBddArray, 03695 array_t *toVarBddArray, 03696 array_t *quantifyVarBddArray, 03697 array_t **orderedClusteredRelationArrayPtr, 03698 array_t **smoothVarBddArrayPtr, 03699 ImgTrmOption_t *option, 03700 boolean freeRelationArray) 03701 { 03702 array_t *clusteredRelationArray; /*clustered version of orderedRelationArray*/ 03703 03704 /* 03705 * Since clusters are formed by multiplying the latches starting 03706 * from one end we need to order the latches using some heuristics 03707 * first. Right now, we order the latches using the same heuristic 03708 * as the one used for ordering the clusters for early quantifiction. 03709 * However, since we are not interested in the quantification 03710 * schedule at this stage, we will pass a NIL(array_t*) as the last 03711 * argument. 03712 */ 03713 *orderedClusteredRelationArrayPtr = NIL(array_t); 03714 OrderRelationArray(mddManager, relationArray, fromVarBddArray, 03715 quantifyVarBddArray, toVarBddArray, option, 03716 orderedClusteredRelationArrayPtr, NIL(array_t *)); 03717 03718 /* free relationArray if told to */ 03719 if (freeRelationArray) mdd_array_free(relationArray); 03720 03721 03722 /* Create the clusters */ 03723 clusteredRelationArray = CreateClusters(mddManager, 03724 *orderedClusteredRelationArrayPtr, 03725 option); 03726 03727 /* Free the orderedRelationArray */ 03728 mdd_array_free(*orderedClusteredRelationArrayPtr); 03729 03730 /* Order the clusters for image and pre-image computation. */ 03731 OrderRelationArray(mddManager, clusteredRelationArray, fromVarBddArray, 03732 quantifyVarBddArray, toVarBddArray, option, 03733 orderedClusteredRelationArrayPtr, smoothVarBddArrayPtr); 03734 /* Free the clusteredRelationArray. */ 03735 mdd_array_free(clusteredRelationArray); 03736 } 03737 03738 03750 static array_t * 03751 CreateClusters(bdd_manager *bddManager, array_t *relationArray, 03752 ImgTrmOption_t *option) 03753 { 03754 array_t *clusterArray; 03755 int i; 03756 bdd_t *cluster, *relation, *tempCluster; 03757 int flag; 03758 int size; 03759 03760 clusterArray = array_alloc(bdd_t *, 0); 03761 03762 for (i=0; i<array_n(relationArray);) { 03763 cluster = bdd_one(bddManager); 03764 flag = 0; 03765 do{ 03766 relation = array_fetch(bdd_t *,relationArray, i); 03767 i++; 03768 tempCluster = bdd_and_with_limit(cluster, relation, 1, 1, 03769 option->clusterSize); 03770 assert(flag || tempCluster != NIL(mdd_t)); 03771 if (tempCluster != NIL(mdd_t)) { 03772 size = bdd_size(tempCluster); 03773 if (size <= option->clusterSize || flag == 0) { 03774 bdd_free(cluster); 03775 cluster = tempCluster; 03776 if (flag == 0 && size >= option->clusterSize) 03777 break; 03778 flag = 1; 03779 } 03780 else{ 03781 bdd_free(tempCluster); 03782 i--; 03783 break; 03784 } 03785 } 03786 else { 03787 i--; 03788 break; 03789 } 03790 } while (i < array_n(relationArray)); 03791 array_insert_last(bdd_t *, clusterArray, cluster); 03792 } 03793 return clusterArray; 03794 } 03795 03814 static void 03815 OrderRelationArray(mdd_manager *mddManager, 03816 array_t *relationArray, 03817 array_t *domainVarBddArray, 03818 array_t *quantifyVarBddArray, 03819 array_t *rangeVarBddArray, 03820 ImgTrmOption_t *option, 03821 array_t **orderedRelationArrayPtr, 03822 array_t **arraySmoothVarBddArrayPtr) 03823 { 03824 array_t *quantifyVarBddIdArray, *domainVarBddIdArray, *rangeVarBddIdArray; 03825 array_t *domainAndQuantifyVarBddArray; 03826 array_t *ctrInfoArray, *varInfoArray, *simplifiedRelationArray; 03827 array_t *sortedMaxIndexArray; 03828 array_t *arrayDomainQuantifyVarsWithZeroNumCtr = NIL(array_t); 03829 int numRelation, numDomainVars, numQuantifyVars, numRangeVars; 03830 int numSmoothVars, numVars; 03831 int bddId; 03832 int i; 03833 int *sortedMaxIndexVector; 03834 int numSmoothVarsRemaining, numIntroducedVarsRemaining; 03835 st_table *bddIdToVarInfoTable, *bddIdToBddTable; 03836 bdd_t *relation, *bdd; 03837 CtrInfo_t *ctrInfo; 03838 VarInfo_t *varInfo; 03839 lsList remainingCtrInfoList; 03840 03841 numRelation = array_n(relationArray); 03842 numDomainVars = array_n(domainVarBddArray); 03843 numRangeVars = array_n(rangeVarBddArray); 03844 numQuantifyVars = array_n(quantifyVarBddArray); 03845 numSmoothVars = numDomainVars + numQuantifyVars; 03846 numVars = numSmoothVars + numRangeVars; 03847 03848 domainVarBddIdArray = bdd_get_varids(domainVarBddArray); 03849 rangeVarBddIdArray = bdd_get_varids(rangeVarBddArray); 03850 quantifyVarBddIdArray = bdd_get_varids(quantifyVarBddArray); 03851 domainAndQuantifyVarBddArray = array_join(domainVarBddArray, 03852 quantifyVarBddArray); 03853 03854 bddIdToBddTable = st_init_table(st_numcmp, st_numhash); 03855 HashIdToBddTable(bddIdToBddTable, domainVarBddIdArray, domainVarBddArray); 03856 HashIdToBddTable(bddIdToBddTable, quantifyVarBddIdArray, quantifyVarBddArray); 03857 HashIdToBddTable(bddIdToBddTable, rangeVarBddIdArray, rangeVarBddArray); 03858 03859 bddIdToVarInfoTable = st_init_table(st_numcmp, st_numhash); 03860 03861 /* 03862 * Create the array of ctrInfo's for each component 03863 */ 03864 ctrInfoArray = array_alloc(CtrInfo_t*, 0); 03865 varInfoArray = array_alloc(VarInfo_t*, 0); 03866 03867 /* 03868 * Create the array of varInfo for each variable 03869 */ 03870 for (i=0; i<numVars; i++) { 03871 varInfo = VarInfoStructAlloc(); 03872 if (i<numDomainVars) { 03873 bddId = array_fetch(int, domainVarBddIdArray, i); 03874 varInfo->varType = domainVar_c; 03875 } 03876 else if (i < (numDomainVars+numQuantifyVars)) { 03877 bddId = array_fetch(int, quantifyVarBddIdArray, i-numDomainVars); 03878 varInfo->varType = quantifyVar_c; 03879 } 03880 else{ 03881 bddId = array_fetch(int, rangeVarBddIdArray, 03882 (i-(numDomainVars+numQuantifyVars))); 03883 varInfo->varType = rangeVar_c; 03884 } 03885 array_insert_last(VarInfo_t*, varInfoArray, varInfo); 03886 varInfo->bddId = bddId; 03887 st_insert(bddIdToVarInfoTable, (char *)(long) bddId, (char *)varInfo); 03888 } 03889 03890 /* 03891 * Fill in the data structure of the ctrInfo and varInfo 03892 */ 03893 for (i=0; i<numRelation; i++) { 03894 st_table *supportTable; 03895 st_generator *stGen; 03896 VarItem_t *varItem; 03897 CtrItem_t *ctrItem; 03898 lsHandle varItemHandle, ctrItemHandle; 03899 long varId; 03900 03901 ctrInfo = CtrInfoStructAlloc(); 03902 array_insert_last(CtrInfo_t*, ctrInfoArray, ctrInfo); 03903 ctrInfo->ctrId = i; 03904 relation = array_fetch(bdd_t*, relationArray, i); 03905 supportTable = ImgBddGetSupportIdTable(relation); 03906 st_foreach_item(supportTable, stGen, &varId, NULL) { 03907 varInfo = NIL(VarInfo_t); 03908 if (st_lookup(bddIdToVarInfoTable, (char *) varId, &varInfo) == 0) { 03909 /* This variable is of no interest, because it is not present 03910 * in the bddIdToVarInfoTable. 03911 */ 03912 continue; 03913 } 03914 varItem = ALLOC(VarItem_t,1); 03915 varItem->varInfo = varInfo; 03916 (void) lsNewBegin(ctrInfo->varItemList, (lsGeneric)varItem, 03917 (lsHandle *)&varItemHandle); 03918 ctrItem = ALLOC(CtrItem_t,1); 03919 ctrItem->ctrInfo = ctrInfo; 03920 (void) lsNewBegin(varInfo->ctrItemList, (lsGeneric)ctrItem, 03921 (lsHandle *)&ctrItemHandle); 03922 varItem->ctrItemHandle = ctrItemHandle; 03923 ctrItem->varItemHandle = varItemHandle; 03924 varInfo->numCtr++; 03925 } 03926 st_free_table(supportTable); 03927 } /* Initialization of ctrInfoArray and varInfoArray complete */ 03928 03929 /* 03930 * Smooth out the quantify variables which are local to a particular cluster. 03931 */ 03932 simplifiedRelationArray = RelationArraySmoothLocalVars(relationArray, 03933 ctrInfoArray, 03934 varInfoArray, 03935 bddIdToBddTable); 03936 03937 assert(CheckCtrInfoArray(ctrInfoArray, numDomainVars, numQuantifyVars, 03938 numRangeVars)); 03939 assert(CheckVarInfoArray(varInfoArray, numRelation)); 03940 03941 /* 03942 * In the ordering scheme of clusters, the number of variables yet to be 03943 * quantified out and number of variables which are yet to be introduced is 03944 * taken into account. The number of smooth variables which are yet to be 03945 * quantified out could have changed. Also some of the range variables may 03946 * not be in the support of any of the clusters. This can happen while doing 03947 * the ordering for clusters for backward image (when a present state 03948 * variable does not appear in the support of any of the next state 03949 * functions. Recalculate these numbers. */ 03950 03951 numSmoothVarsRemaining = numSmoothVars; 03952 numIntroducedVarsRemaining = numRangeVars; 03953 03954 /* 03955 * Find out which variables do not appear in the support of any cluster. 03956 * Update the numSmoothVarsRemaining and numIntroducedVarsRemaining 03957 * accordingly. 03958 * Also, these domainVars and quantifyVars can be quantified out as soon as 03959 * possible. 03960 */ 03961 if (arraySmoothVarBddArrayPtr != NIL(array_t *)) 03962 arrayDomainQuantifyVarsWithZeroNumCtr = array_alloc(bdd_t*, 0); 03963 for (i=0; i<numVars; i++) { 03964 varInfo = array_fetch(VarInfo_t*, varInfoArray, i); 03965 if (varInfo->numCtr == 0) { 03966 if ((varInfo->varType == domainVar_c) || 03967 (varInfo->varType == quantifyVar_c)) { 03968 numSmoothVarsRemaining--; 03969 if (arraySmoothVarBddArrayPtr != NIL(array_t *)) { 03970 st_lookup(bddIdToBddTable, (char *)(long)varInfo->bddId, &bdd); 03971 array_insert_last(bdd_t*, arrayDomainQuantifyVarsWithZeroNumCtr, 03972 bdd_dup(bdd)); 03973 } 03974 } 03975 else numIntroducedVarsRemaining--; 03976 } 03977 } 03978 03979 /* 03980 * The ordering scheme also depends on the value of the maximum index of a 03981 * smooth variable which is yet to be quantified. For efficiency reasons, we 03982 * maintain a vector indicating the maximum index of the clusters. This 03983 * vector is sorted in the decreasing order of index. The rank of a cluster 03984 * is stored in its "rankMaxSmoothVarIndex" field. 03985 */ 03986 sortedMaxIndexArray = array_dup(ctrInfoArray); 03987 array_sort(sortedMaxIndexArray, CtrInfoMaxIndexCompare); 03988 sortedMaxIndexVector = ALLOC(int, numRelation); 03989 for (i=0; i<numRelation; i++) { 03990 ctrInfo = array_fetch(CtrInfo_t*, sortedMaxIndexArray, i); 03991 ctrInfo->rankMaxSmoothVarIndex = i; 03992 sortedMaxIndexVector[i] = ctrInfo->maxSmoothVarIndex; 03993 } 03994 array_free(sortedMaxIndexArray); 03995 03996 /* 03997 * Create a list of clusters which are yet to be ordered. Right now 03998 * put all the clusters. Later on the list will contain only those 03999 * clusters which have not yet been ordered. 04000 */ 04001 remainingCtrInfoList = lsCreate(); 04002 for(i=0; i<numRelation; i++) { 04003 lsHandle ctrHandle; 04004 ctrInfo = array_fetch(CtrInfo_t*, ctrInfoArray, i); 04005 lsNewBegin(remainingCtrInfoList, (lsGeneric)ctrInfo, &ctrHandle); 04006 ctrInfo->ctrInfoListHandle = ctrHandle; 04007 } 04008 04009 /* Call the auxiliary routine to do the ordering. */ 04010 OrderRelationArrayAux(simplifiedRelationArray, remainingCtrInfoList, 04011 ctrInfoArray, varInfoArray, sortedMaxIndexVector, 04012 numSmoothVarsRemaining, numIntroducedVarsRemaining, 04013 bddIdToBddTable, option, domainAndQuantifyVarBddArray, 04014 orderedRelationArrayPtr, arraySmoothVarBddArrayPtr, 04015 arrayDomainQuantifyVarsWithZeroNumCtr); 04016 04017 lsDestroy(remainingCtrInfoList,0); 04018 04019 /* Free the info arrays */ 04020 04021 for (i=0; i<numRelation; i++) { 04022 ctrInfo = array_fetch(CtrInfo_t*, ctrInfoArray, i); 04023 CtrInfoStructFree(ctrInfo); 04024 } 04025 array_free(ctrInfoArray); 04026 04027 for (i=0; i<numVars; i++) { 04028 varInfo = array_fetch(VarInfo_t*, varInfoArray, i); 04029 assert(varInfo->numCtr == 0); 04030 VarInfoStructFree(varInfo); 04031 } 04032 array_free(varInfoArray); 04033 04034 if (option->verbosity >= 3) { 04035 int numRelation = array_n(*orderedRelationArrayPtr); 04036 04037 if (arraySmoothVarBddArrayPtr != NIL(array_t*)) { 04038 PrintSmoothIntroducedCount(*orderedRelationArrayPtr, 04039 arraySmoothVarBddArrayPtr, 04040 domainVarBddIdArray, 04041 rangeVarBddIdArray); 04042 } 04043 if (option->verbosity >= 4) { 04044 for (i= 0; i <numRelation; i++) { 04045 st_table *supportTable; 04046 (void) fprintf(vis_stdout, "Cluster # %d\n",i); 04047 supportTable = ImgBddGetSupportIdTable( 04048 array_fetch(bdd_t*, *orderedRelationArrayPtr, i)); 04049 PrintBddIdTable(supportTable); 04050 if (arraySmoothVarBddArrayPtr != NIL(array_t*)) { 04051 (void) fprintf(vis_stdout, "Exist cube # %d\n",i); 04052 PrintBddIdFromBddArray(array_fetch(array_t*, 04053 *arraySmoothVarBddArrayPtr, i)); 04054 } 04055 } 04056 } 04057 } 04058 FREE(sortedMaxIndexVector); 04059 array_free(simplifiedRelationArray); 04060 04061 /* Free BDD Id arrays */ 04062 array_free(domainVarBddIdArray); 04063 array_free(quantifyVarBddIdArray); 04064 array_free(rangeVarBddIdArray); 04065 array_free(domainAndQuantifyVarBddArray); 04066 /* Free the st_tables */ 04067 st_free_table(bddIdToBddTable); 04068 st_free_table(bddIdToVarInfoTable); 04069 } 04070 04087 static array_t * 04088 RelationArraySmoothLocalVars(array_t *relationArray, array_t *ctrInfoArray, 04089 array_t *varInfoArray, 04090 st_table *bddIdToBddTable) 04091 { 04092 array_t *arraySmoothVarBddArray, *smoothVarBddArray; 04093 array_t *simplifiedRelationArray; 04094 bdd_t *simplifiedRelation, *relation, *varBdd; 04095 int maxSmoothVarIndexForAllCtr, i, numRelation; 04096 04097 numRelation = array_n(relationArray); 04098 04099 /* 04100 * Initialize the array of cubes (of quantified variables which occur in 04101 * only one relation), to be smoothed out. 04102 */ 04103 arraySmoothVarBddArray = array_alloc(array_t*, 0); 04104 for (i=0; i<numRelation; i++) { 04105 smoothVarBddArray = array_alloc(bdd_t*, 0); 04106 array_insert_last(array_t*, arraySmoothVarBddArray, smoothVarBddArray); 04107 } 04108 04109 maxSmoothVarIndexForAllCtr = -1; 04110 for (i=0; i<numRelation; i++) { 04111 VarItem_t *varItem; 04112 lsHandle varItemHandle; 04113 CtrInfo_t *ctrInfo = array_fetch(CtrInfo_t*, ctrInfoArray, i); 04114 int maxSmoothVarIndex = -1; 04115 lsGen varItemListGen = lsStart(ctrInfo->varItemList); 04116 04117 smoothVarBddArray = array_fetch(array_t *, arraySmoothVarBddArray, i); 04118 while (lsNext(varItemListGen, &varItem, &varItemHandle) == 04119 LS_OK) { 04120 int varBddId; 04121 VarInfo_t *varInfo = varItem->varInfo; 04122 if (varInfo->varType == rangeVar_c) { 04123 ctrInfo->numIntroducedVars++; 04124 } 04125 else if (varInfo->numCtr == 1) { 04126 assert(lsLength(varInfo->ctrItemList) == 1); 04127 if (varInfo->varType == quantifyVar_c) { 04128 /* 04129 * The variable can be smoothed out. 04130 * Put it in an array of variables to be 04131 * smoothed out from the relation. 04132 */ 04133 CtrItem_t *ctrItem; 04134 varBddId = varInfo->bddId; 04135 st_lookup(bddIdToBddTable, (char *)(long)varBddId,&varBdd); 04136 array_insert_last(bdd_t*, smoothVarBddArray, bdd_dup(varBdd)); 04137 varInfo->numCtr = 0; 04138 /* Remove the cluster from the ctrItemList of varInfo */ 04139 lsRemoveItem(varItem->ctrItemHandle, &ctrItem); 04140 CtrItemStructFree(ctrItem); 04141 /* Remove the variable from the varItemList of ctrInfo.*/ 04142 lsRemoveItem(varItemHandle, &varItem); 04143 VarItemStructFree(varItem); 04144 continue; 04145 } 04146 else { 04147 /* Increase the numLocalSmoothVars count of the corresponding ctr. */ 04148 ctrInfo->numLocalSmoothVars++; 04149 ctrInfo->numSmoothVars++; 04150 if (maxSmoothVarIndex < varInfo->bddId) { 04151 maxSmoothVarIndex = varInfo->bddId; 04152 } 04153 } 04154 } 04155 else{ /* varInfo->numCtr > 1 */ 04156 assert(varInfo->numCtr > 1); 04157 ctrInfo->numSmoothVars++; 04158 if (maxSmoothVarIndex < varInfo->bddId) { 04159 maxSmoothVarIndex = varInfo->bddId; 04160 } 04161 } 04162 } 04163 lsFinish(varItemListGen); 04164 if (maxSmoothVarIndex >= 0) { 04165 ctrInfo->maxSmoothVarIndex = maxSmoothVarIndex; 04166 } 04167 else{ 04168 ctrInfo->maxSmoothVarIndex = 0; 04169 } 04170 if (maxSmoothVarIndexForAllCtr < maxSmoothVarIndex) { 04171 maxSmoothVarIndexForAllCtr = maxSmoothVarIndex; 04172 } 04173 } 04174 04175 /* 04176 * Initialization Finished. We need to smooth out those quantify 04177 * variables which appear in only one ctr. 04178 */ 04179 simplifiedRelationArray = array_alloc(bdd_t*, 0); 04180 for (i=0; i<numRelation; i++) { 04181 relation = array_fetch(bdd_t*, relationArray, i); 04182 smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i); 04183 if (array_n(smoothVarBddArray) != 0) 04184 simplifiedRelation = bdd_smooth(relation, smoothVarBddArray); 04185 else 04186 simplifiedRelation = bdd_dup(relation); 04187 array_insert_last(bdd_t*, simplifiedRelationArray, simplifiedRelation); 04188 } 04189 mdd_array_array_free(arraySmoothVarBddArray); 04190 return simplifiedRelationArray; 04191 } 04192 04211 static void 04212 OrderRelationArrayAux(array_t *relationArray, 04213 lsList remainingCtrInfoList, 04214 array_t *ctrInfoArray, 04215 array_t *varInfoArray, 04216 int *sortedMaxIndexVector, 04217 int numSmoothVarsRemaining, 04218 int numIntroducedVarsRemaining, 04219 st_table *bddIdToBddTable, 04220 ImgTrmOption_t *option, 04221 array_t *domainAndQuantifyVarBddArray, 04222 array_t **orderedRelationArrayPtr, 04223 array_t **arraySmoothVarBddArrayPtr, 04224 array_t *arrayDomainQuantifyVarsWithZeroNumCtr) 04225 { 04226 int numRelation, ctrCount, currentRankMaxSmoothVarIndex; 04227 int maxIndex = 0; 04228 array_t *orderedRelationArray, *arraySmoothVarBddArray; 04229 array_t *smoothVarBddArray; 04230 int *bestCtrIdVector; 04231 int maxNumLocalSmoothVars, maxNumSmoothVars, maxNumIntroducedVars; 04232 lsGen lsgen; 04233 04234 ctrCount = 0; 04235 currentRankMaxSmoothVarIndex = 0; 04236 04237 numRelation = array_n(relationArray); 04238 04239 arraySmoothVarBddArray = NIL(array_t); 04240 orderedRelationArray = array_alloc(bdd_t*, 0); 04241 *orderedRelationArrayPtr = orderedRelationArray; 04242 if (arraySmoothVarBddArrayPtr != NIL(array_t *)) { 04243 arraySmoothVarBddArray = array_alloc(array_t*, 0); 04244 *arraySmoothVarBddArrayPtr = arraySmoothVarBddArray; 04245 array_insert_last(array_t*, arraySmoothVarBddArray, 04246 arrayDomainQuantifyVarsWithZeroNumCtr); 04247 } 04248 bestCtrIdVector = ALLOC(int, numRelation); 04249 04250 while (ctrCount < numRelation) { 04251 float bestBenefit, benefit; 04252 int bestCtrId; 04253 bdd_t *bestRelation; 04254 lsGen ctrInfoListGen; 04255 CtrInfo_t *ctrInfo, *ctrInfoAux; 04256 04257 bestBenefit = -1.0e20; /* a safely small number */ 04258 bestCtrId = -1; 04259 /* Find the maximum index of the remaining clusters */ 04260 while (currentRankMaxSmoothVarIndex < numRelation && 04261 (maxIndex = sortedMaxIndexVector[currentRankMaxSmoothVarIndex++]) == -1); 04262 04263 /* Calculate the maximum values of local smooth variables etc. */ 04264 maxNumLocalSmoothVars = 0; 04265 maxNumSmoothVars = 0; 04266 maxNumIntroducedVars = 0; 04267 lsForEachItem(remainingCtrInfoList, lsgen, ctrInfo) { 04268 if (ctrInfo->numLocalSmoothVars > maxNumLocalSmoothVars) { 04269 maxNumLocalSmoothVars = ctrInfo->numLocalSmoothVars; 04270 } 04271 if (ctrInfo->numSmoothVars > maxNumSmoothVars) { 04272 maxNumSmoothVars = ctrInfo->numSmoothVars; 04273 } 04274 if (ctrInfo->numIntroducedVars > maxNumIntroducedVars) { 04275 maxNumIntroducedVars = ctrInfo->numIntroducedVars; 04276 } 04277 } 04278 04279 if (option->verbosity >= 4) { 04280 fprintf(vis_stdout, "maxNumLocalSmoothVars = %3d maxNumSmoothVars = %3d ", 04281 maxNumLocalSmoothVars, maxNumSmoothVars); 04282 fprintf(vis_stdout, "maxNumIntroducedVars = %3d\n", maxNumIntroducedVars); 04283 } 04284 /* Calculate the cost function of each of the cluster */ 04285 ctrInfoListGen = lsStart(remainingCtrInfoList); 04286 while (lsNext(ctrInfoListGen, &ctrInfo, NIL(lsHandle)) == 04287 LS_OK) { 04288 benefit = CalculateBenefit(ctrInfo, maxNumLocalSmoothVars, 04289 maxNumSmoothVars, maxIndex, 04290 maxNumIntroducedVars, option); 04291 04292 if (option->verbosity >= 4) { 04293 fprintf(vis_stdout, 04294 "id = %d: numLocalSmoothVars = %d numSmoothVars = %d benefit = %f\n", 04295 ctrInfo->ctrId, ctrInfo->numLocalSmoothVars, 04296 ctrInfo->numSmoothVars, benefit); 04297 } 04298 if (benefit > bestBenefit) { 04299 bestBenefit = benefit; 04300 bestCtrId = ctrInfo->ctrId; 04301 } 04302 } 04303 lsFinish(ctrInfoListGen); 04304 /* 04305 * Insert the relation in the ordered array of relations and put in the 04306 * appropriate cubes. 04307 */ 04308 04309 bestCtrIdVector[ctrCount] = bestCtrId; 04310 ctrInfo = array_fetch(CtrInfo_t*, ctrInfoArray, bestCtrId); 04311 lsRemoveItem(ctrInfo->ctrInfoListHandle, &ctrInfoAux); 04312 assert(ctrInfo == ctrInfoAux); 04313 bestRelation = array_fetch(bdd_t*, relationArray, bestCtrId); 04314 array_insert_last(bdd_t*, orderedRelationArray, bestRelation); 04315 if (option->verbosity >= 4) { 04316 fprintf(vis_stdout, 04317 "Best id = %d benefit = %f numLocalSmoothVars = %d numSmoothVars = %d\n", 04318 bestCtrId, bestBenefit, ctrInfo->numLocalSmoothVars, 04319 ctrInfo->numSmoothVars); 04320 } 04321 /* 04322 * Update the remaining ctrInfo's and the varInfo's affected by choosing 04323 * this cluster. Also get the array of smooth variables which can be 04324 * quantified once this cluster is multiplied in the product. 04325 */ 04326 smoothVarBddArray = UpdateInfoArrays(ctrInfo, bddIdToBddTable, 04327 &numSmoothVarsRemaining, 04328 &numIntroducedVarsRemaining); 04329 assert(CheckCtrInfo(ctrInfo, numSmoothVarsRemaining, 0, 04330 numIntroducedVarsRemaining)); 04331 04332 if (arraySmoothVarBddArrayPtr != NIL(array_t *)) { 04333 if (ctrCount == numRelation-1) { 04334 /* 04335 * In the last element of arraySmoothVarBddArray, put all the domain 04336 * and quantify variables (in case some of them were not in the support 04337 * of any cluster). 04338 */ 04339 int i, j; 04340 st_table *varsTable = st_init_table((ST_PFICPCP)bdd_ptrcmp, 04341 (ST_PFICPI)bdd_ptrhash); 04342 array_t *tmpVarBddArray; 04343 mdd_t *tmpVar; 04344 04345 arrayForEachItem(array_t *, arraySmoothVarBddArray, i, tmpVarBddArray) { 04346 arrayForEachItem(mdd_t *, tmpVarBddArray, j, tmpVar) { 04347 st_insert(varsTable, (char *)tmpVar, NIL(char)); 04348 } 04349 } 04350 arrayForEachItem(mdd_t *, smoothVarBddArray, i, tmpVar) { 04351 st_insert(varsTable, (char *)tmpVar, NIL(char)); 04352 } 04353 arrayForEachItem(mdd_t *, domainAndQuantifyVarBddArray, i, tmpVar) { 04354 if (st_lookup(varsTable, (char *)tmpVar, NIL(char *)) == 0) 04355 array_insert_last(mdd_t *, smoothVarBddArray, mdd_dup(tmpVar)); 04356 } 04357 st_free_table(varsTable); 04358 } 04359 array_insert_last(array_t*, arraySmoothVarBddArray, smoothVarBddArray); 04360 } 04361 else{ 04362 mdd_array_free(smoothVarBddArray); 04363 } 04364 sortedMaxIndexVector[ctrInfo->rankMaxSmoothVarIndex] = -1; 04365 ctrCount++; 04366 } 04367 assert(numIntroducedVarsRemaining == 0); 04368 assert(numSmoothVarsRemaining == 0); 04369 if (option->verbosity >= 3) { 04370 int i; 04371 (void) fprintf(vis_stdout,"Cluster Sequence = "); 04372 for (i=0; i<numRelation; i++) { 04373 (void) fprintf(vis_stdout, "%d ", bestCtrIdVector[i]); 04374 } 04375 (void) fprintf(vis_stdout,"\n"); 04376 } 04377 04378 FREE(bestCtrIdVector); 04379 } 04380 04381 04425 static array_t * 04426 UpdateInfoArrays(CtrInfo_t *ctrInfo, st_table *bddIdToBddTable, 04427 int *numSmoothVarsRemainingPtr, 04428 int *numIntroducedVarsRemainingPtr) 04429 { 04430 array_t *smoothVarBddArray; 04431 lsGen varItemListGen; 04432 int numSmoothVarsRemaining = *numSmoothVarsRemainingPtr; 04433 int numIntroducedVarsRemaining = *numIntroducedVarsRemainingPtr; 04434 VarItem_t *varItem; 04435 lsHandle varItemHandle; 04436 04437 smoothVarBddArray = array_alloc(bdd_t*, 0); 04438 varItemListGen = lsStart(ctrInfo->varItemList); 04439 while (lsNext(varItemListGen, &varItem, &varItemHandle) == 04440 LS_OK) { 04441 VarInfo_t *varInfo = varItem->varInfo; 04442 CtrItem_t *ctrItem; 04443 assert(varInfo->numCtr == lsLength(varInfo->ctrItemList)); 04444 lsRemoveItem(varItem->ctrItemHandle, &ctrItem); 04445 CtrItemStructFree(ctrItem); 04446 varInfo->numCtr--; 04447 lsRemoveItem(varItemHandle, &varItem); 04448 VarItemStructFree(varItem); 04449 04450 /* 04451 * If this variable is to be smoothed (domain or quantify type) and 04452 * the numCtr is 1, then it should be added to the smoothVarBddArray, 04453 * otherwise, the numCtr should be decreased by 1. 04454 * If the variable is of the range type then the number of introduced 04455 * vars remaining and the number of introduced vars should be 04456 * appropriately modified. 04457 */ 04458 if ((varInfo->varType == domainVar_c) || 04459 (varInfo->varType == quantifyVar_c)) { 04460 if (varInfo->numCtr == 0) { 04461 bdd_t *varBdd; 04462 st_lookup(bddIdToBddTable, (char *)(long)(varInfo->bddId), &varBdd); 04463 array_insert_last(bdd_t*, smoothVarBddArray, bdd_dup(varBdd)); 04464 numSmoothVarsRemaining--; 04465 ctrInfo->numLocalSmoothVars--; 04466 ctrInfo->numSmoothVars--; 04467 } 04468 else{ 04469 if (varInfo->numCtr == 1) { 04470 /* 04471 * We need to update the numLocalSmoothVars of the ctr 04472 * which depends on it. 04473 */ 04474 lsFirstItem(varInfo->ctrItemList, &ctrItem, LS_NH); 04475 ctrItem->ctrInfo->numLocalSmoothVars++; 04476 } 04477 /* 04478 * else varInfo->numCtr > 1 : Nothing to be done because neither it 04479 * can be quantified out, nor it is effecting any cost function. 04480 */ 04481 ctrInfo->numSmoothVars--; 04482 } 04483 } 04484 else{/* The variable is of range type, so need to appropriately modify the 04485 * numIntroducedVars of those clusters which contain this range 04486 * variable in their support. 04487 */ 04488 lsHandle ctrItemHandle; 04489 lsGen ctrItemListGen = lsStart(varInfo->ctrItemList); 04490 ctrInfo->numIntroducedVars--; 04491 while (lsNext(ctrItemListGen, &ctrItem, &ctrItemHandle) == LS_OK) { 04492 ctrItem->ctrInfo->numIntroducedVars--; 04493 lsRemoveItem(ctrItem->varItemHandle,&varItem); 04494 lsRemoveItem(ctrItemHandle,&ctrItem); 04495 VarItemStructFree(varItem); 04496 CtrItemStructFree(ctrItem); 04497 } 04498 lsFinish(ctrItemListGen); 04499 numIntroducedVarsRemaining--; 04500 varInfo->numCtr = 0; 04501 } 04502 assert(varInfo->numCtr == lsLength(varInfo->ctrItemList)); 04503 } 04504 lsFinish(varItemListGen); 04505 *numIntroducedVarsRemainingPtr = numIntroducedVarsRemaining; 04506 *numSmoothVarsRemainingPtr = numSmoothVarsRemaining; 04507 return smoothVarBddArray; 04508 } 04509 04510 04544 static float 04545 CalculateBenefit(CtrInfo_t *ctrInfo, int maxNumLocalSmoothVars, int 04546 maxNumSmoothVars, int maxIndex, int 04547 maxNumIntroducedVars, ImgTrmOption_t *option) 04548 { 04549 int W1, W2, W3, W4; 04550 float benefit; 04551 04552 W1 = option->W1; 04553 W2 = option->W2; 04554 W3 = option->W3; 04555 W4 = option->W4; 04556 04557 benefit = 0.0; 04558 benefit += (maxNumLocalSmoothVars ? 04559 ((float)W1 * ((float)ctrInfo->numLocalSmoothVars / 04560 (float)maxNumLocalSmoothVars)) : 0.0); 04561 04562 benefit += (maxNumSmoothVars ? 04563 ((float)W2 * ((float)ctrInfo->numSmoothVars / 04564 (float)maxNumSmoothVars)) : 0.0); 04565 04566 benefit += (maxIndex ? 04567 ((float)W3 * ((float)ctrInfo->maxSmoothVarIndex / 04568 (float)maxIndex)) : 0.0); 04569 04570 benefit -= (maxNumIntroducedVars ? 04571 ((float)W4 * ((float)ctrInfo->numIntroducedVars / 04572 (float)maxNumIntroducedVars)) : 0.0); 04573 04574 return benefit; 04575 } 04576 04588 static void 04589 PrintOption(Img_MethodType method, ImgTrmOption_t *option, FILE *fp) 04590 { 04591 if (method == Img_Iwls95_c) 04592 (void)fprintf(fp, "Printing Information about Image method: IWLS95\n"); 04593 else if (method == Img_Mlp_c) 04594 (void)fprintf(fp, "Printing Information about Image method: MLP\n"); 04595 else if (method == Img_Linear_c) 04596 (void)fprintf(fp, "Printing Information about Image method: LINEAR\n"); 04597 else 04598 assert(0); 04599 (void)fprintf(fp, 04600 "\tThreshold Value of Bdd Size For Creating Clusters = %d\n", 04601 option->clusterSize); 04602 (void)fprintf(fp, 04603 "\t\t(Use \"set image_cluster_size value\" to set this to desired value)\n"); 04604 (void)fprintf(fp, "\tVerbosity = %d\n", option->verbosity); 04605 (void)fprintf(fp, 04606 "\t\t(Use \"set image_verbosity value\" to set this to desired value)\n"); 04607 if (method == Img_Iwls95_c) { 04608 (void)fprintf(fp, "\tW1 =%3d W2 =%2d W3 =%2d W4 =%2d\n", 04609 option->W1, option->W2, option->W3, option->W4); 04610 (void)fprintf(fp, 04611 "\t\t(Use \"set image_W? value\" to set these to desired values)\n"); 04612 } 04613 } 04614 04626 static Iwls95Info_t * 04627 Iwls95InfoStructAlloc(Img_MethodType method) 04628 { 04629 Iwls95Info_t *info; 04630 info = ALLOC(Iwls95Info_t, 1); 04631 memset(info, 0, sizeof(Iwls95Info_t)); 04632 info->method = method; 04633 info->option = TrmGetOptions(); 04634 info->PIoption = ImgGetPartialImageOptions(); 04635 return info; 04636 } 04637 04647 static CtrInfo_t * 04648 CtrInfoStructAlloc(void) 04649 { 04650 CtrInfo_t *ctrInfo; 04651 ctrInfo = ALLOC(CtrInfo_t, 1); 04652 ctrInfo->ctrId = -1; 04653 ctrInfo->numLocalSmoothVars = 0; 04654 ctrInfo->numSmoothVars = 0; 04655 ctrInfo->maxSmoothVarIndex = -1; 04656 ctrInfo->numIntroducedVars = 0; 04657 ctrInfo->varItemList = lsCreate(); 04658 ctrInfo->ctrInfoListHandle = NULL; 04659 return ctrInfo; 04660 } 04661 04662 04672 static void 04673 CtrInfoStructFree(CtrInfo_t *ctrInfo) 04674 { 04675 lsDestroy(ctrInfo->varItemList, 0); 04676 FREE(ctrInfo); 04677 } 04678 04688 static VarInfo_t * 04689 VarInfoStructAlloc(void) 04690 { 04691 VarInfo_t *varInfo; 04692 varInfo = ALLOC(VarInfo_t, 1); 04693 varInfo->bddId = -1; 04694 varInfo->numCtr = 0; 04695 varInfo->varType = -1; 04696 varInfo->ctrItemList = lsCreate(); 04697 return varInfo; 04698 } 04699 04709 static void 04710 VarInfoStructFree(VarInfo_t *varInfo) 04711 { 04712 lsDestroy(varInfo->ctrItemList,0); 04713 FREE(varInfo); 04714 } 04715 04725 static void 04726 CtrItemStructFree(CtrItem_t *ctrItem) 04727 { 04728 FREE(ctrItem); 04729 } 04730 04740 static void 04741 VarItemStructFree(VarItem_t *varItem) 04742 { 04743 FREE(varItem); 04744 } 04745 04757 static int 04758 CtrInfoMaxIndexCompare(const void * p1, const void * p2) 04759 { 04760 CtrInfo_t **infoCtr1 = (CtrInfo_t **) p1; 04761 CtrInfo_t **infoCtr2 = (CtrInfo_t **) p2; 04762 return ((*infoCtr1)->maxSmoothVarIndex > (*infoCtr2)->maxSmoothVarIndex); 04763 } 04764 04765 /* ************************************************************************** 04766 * Debugging Related Routines. 04767 ***************************************************************************/ 04768 04769 04779 static void 04780 PrintCtrInfoStruct(CtrInfo_t *ctrInfo) 04781 { 04782 lsGen lsgen; 04783 VarItem_t *varItem; 04784 04785 (void) fprintf(vis_stdout,"Ctr ID = %d\tNumLocal = %d\tNumSmooth=%d\tNumIntro=%d\tmaxSmooth=%d\trank=%d\n", 04786 ctrInfo->ctrId, ctrInfo->numLocalSmoothVars, 04787 ctrInfo->numSmoothVars, ctrInfo->numIntroducedVars, 04788 ctrInfo->maxSmoothVarIndex, ctrInfo->rankMaxSmoothVarIndex); 04789 lsgen = lsStart(ctrInfo->varItemList); 04790 while (lsNext(lsgen, &varItem, NIL(lsHandle)) == LS_OK) { 04791 (void) fprintf(vis_stdout,"%d\t", varItem->varInfo->bddId); 04792 } 04793 lsFinish(lsgen); 04794 fprintf(vis_stdout,"\n"); 04795 } 04805 static void 04806 PrintVarInfoStruct(VarInfo_t *varInfo) 04807 { 04808 lsGen lsgen; 04809 CtrItem_t *ctrItem; 04810 04811 (void) fprintf(vis_stdout,"Var ID = %d\tNumCtr = %d\tVarType=%d\n", 04812 varInfo->bddId, varInfo->numCtr, varInfo->varType); 04813 lsgen = lsStart(varInfo->ctrItemList); 04814 while (lsNext(lsgen, &ctrItem, NIL(lsHandle)) == LS_OK) { 04815 (void) fprintf(vis_stdout,"%d\t", ctrItem->ctrInfo->ctrId); 04816 } 04817 lsFinish(lsgen); 04818 fprintf(vis_stdout,"\n"); 04819 } 04820 04840 static int 04841 CheckQuantificationSchedule(array_t *relationArray, 04842 array_t *arraySmoothVarBddArray) 04843 { 04844 int i, j; 04845 long varId; 04846 st_table *smoothVarTable, *supportTable; 04847 bdd_t *relation; 04848 array_t *smoothVarBddArray, *smoothVarBddIdArray; 04849 st_generator *stgen; 04850 04851 assert(array_n(relationArray) + 1 == array_n(arraySmoothVarBddArray)); 04852 04853 smoothVarTable = st_init_table(st_numcmp, st_numhash); 04854 04855 smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, 0); 04856 smoothVarBddIdArray = bdd_get_varids(smoothVarBddArray); 04857 for (j=0; j<array_n(smoothVarBddIdArray); j++) { 04858 varId = (long) array_fetch(int, smoothVarBddIdArray, j); 04859 assert(st_insert(smoothVarTable, (char *) varId, NIL(char))==0); 04860 } 04861 array_free(smoothVarBddIdArray); 04862 04863 for (i=0; i<array_n(relationArray); i++) { 04864 relation = array_fetch(bdd_t*, relationArray, i); 04865 supportTable = ImgBddGetSupportIdTable(relation); 04866 /* 04867 * Check that none of the variables in the support have already been 04868 * quantified. 04869 */ 04870 st_foreach_item(supportTable, stgen, &varId, NULL) { 04871 assert(st_is_member(smoothVarTable, (char *) varId) == 0); 04872 04873 } 04874 st_free_table(supportTable); 04875 if (i == (array_n(relationArray)-1)) { 04876 /* Since last element of arraySmoothVarBddArray has all the 04877 * smooth variables, it will not satisfy the condition. 04878 */ 04879 continue; 04880 } 04881 04882 /* 04883 * Put each of the variables quantified at this step in the 04884 * smoothVarTable. And check that none of these smooth variables 04885 * have been introduced before. 04886 */ 04887 smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i + 1); 04888 smoothVarBddIdArray = bdd_get_varids(smoothVarBddArray); 04889 for (j=0; j<array_n(smoothVarBddIdArray); j++) { 04890 varId = (long) array_fetch(int, smoothVarBddIdArray, j); 04891 assert(st_insert(smoothVarTable, (char *) varId, NIL(char))==0); 04892 } 04893 array_free(smoothVarBddIdArray); 04894 } 04895 st_free_table(smoothVarTable); 04896 return 1; 04897 } 04898 04908 static int 04909 CheckCtrInfoArray(array_t *ctrInfoArray, int numDomainVars, int 04910 numQuantifyVars, int numRangeVars) 04911 { 04912 int i; 04913 for (i=0; i<array_n(ctrInfoArray); i++) { 04914 CheckCtrInfo(array_fetch(CtrInfo_t *, ctrInfoArray, i), 04915 numDomainVars, numQuantifyVars, numRangeVars); 04916 } 04917 return 1; 04918 } 04919 04929 static int 04930 CheckCtrInfo(CtrInfo_t *ctrInfo, int numDomainVars, 04931 int numQuantifyVars, int numRangeVars) 04932 { 04933 assert(ctrInfo->numLocalSmoothVars <= (numDomainVars + 04934 numQuantifyVars)); 04935 assert(ctrInfo->numSmoothVars <= (numDomainVars + 04936 numQuantifyVars)); 04937 assert(ctrInfo->numIntroducedVars <= numRangeVars); 04938 assert(lsLength(ctrInfo->varItemList) == 04939 (ctrInfo->numSmoothVars+ctrInfo->numIntroducedVars)); 04940 return 1; 04941 } 04942 04952 static int 04953 CheckVarInfoArray(array_t *varInfoArray, int numRelation) 04954 { 04955 int i; 04956 for (i=0; i<array_n(varInfoArray); i++) { 04957 VarInfo_t *varInfo; 04958 varInfo = array_fetch(VarInfo_t *, varInfoArray, i); 04959 assert(varInfo->numCtr <= numRelation); 04960 assert(varInfo->varType >= 0); 04961 assert(varInfo->varType <= 2); 04962 assert(lsLength(varInfo->ctrItemList) == varInfo->numCtr); 04963 } 04964 return 1; 04965 } 04966 04967 /* **************************************************************** 04968 * Utility Routines. 04969 ****************************************************************/ 04970 04980 static array_t * 04981 BddArrayDup(array_t *bddArray) 04982 { 04983 int i; 04984 array_t *resultArray; 04985 bdd_t *bdd; 04986 resultArray = array_alloc(bdd_t*, 0); 04987 arrayForEachItem(bdd_t *, bddArray, i, bdd) { 04988 array_insert_last(bdd_t*, resultArray, bdd_dup(bdd)); 04989 } 04990 return resultArray; 04991 } 04992 04993 static array_t * 04994 BddArrayArrayDup(array_t *bddArray) 04995 { 04996 int i; 04997 array_t *resultArray; 04998 array_t *arr, *tarr; 04999 05000 resultArray = array_alloc(bdd_t*, 0); 05001 arrayForEachItem(array_t *, bddArray, i, arr) { 05002 tarr = BddArrayDup(arr); 05003 array_insert_last(array_t*, resultArray, tarr); 05004 } 05005 return resultArray; 05006 } 05007 05008 05032 static mdd_t * 05033 BddLinearAndSmooth(mdd_manager *mddManager, 05034 bdd_t *fromSet, 05035 array_t *relationArray, 05036 array_t *arraySmoothVarBddArray, 05037 array_t *smoothVarCubeArray, 05038 int verbosity, 05039 ImgPartialImageOption_t *PIoption, 05040 boolean *partial, boolean lazySiftFlag) 05041 { 05042 int i; 05043 int intermediateSize = 0; 05044 int maxSize = 0; 05045 mdd_t *newProduct; 05046 boolean partialImageAllowed; 05047 bdd_t *product = fromSet; 05048 int clippingDepth = -1; 05049 int partialImageThreshold = 0; 05050 int partialImageMethod = Img_PIApprox_c; 05051 array_t *smoothVarBddArray = NIL(array_t); 05052 mdd_t *smoothVarCube = NIL(mdd_t); 05053 int nvars = -2; 05054 05055 assert(CheckQuantificationSchedule(relationArray, arraySmoothVarBddArray)); 05056 05057 /* Copy (*partial) which indicates whether partial image is allowed. */ 05058 /* (*partial) is set to TRUE later if partial image was performed. */ 05059 partialImageAllowed = *partial; 05060 *partial = FALSE; 05061 05062 /* partial image options */ 05063 if (PIoption != NULL) { 05064 nvars = PIoption->nvars; 05065 clippingDepth = (int) (PIoption->clippingDepthFrac*nvars); 05066 partialImageThreshold = PIoption->partialImageThreshold; 05067 partialImageMethod = PIoption->partialImageMethod; 05068 } 05069 05070 if (fromSet) { 05071 if (smoothVarCubeArray) { 05072 smoothVarCube = array_fetch(mdd_t*, smoothVarCubeArray, 0); 05073 if (bdd_is_tautology(smoothVarCube, 1)) 05074 product = bdd_dup(fromSet); 05075 else 05076 product = bdd_smooth_with_cube(fromSet, smoothVarCube); 05077 } else { 05078 smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, 0); 05079 if (array_n(smoothVarBddArray) == 0) 05080 product = bdd_dup(fromSet); 05081 else 05082 product = bdd_smooth(fromSet, smoothVarBddArray); 05083 } 05084 } else 05085 product = bdd_one(mddManager); 05086 05087 for (i=0; i<array_n(relationArray); i++) { 05088 bdd_t *relation, *tmpProduct; 05089 boolean allowClipping = FALSE; 05090 05091 /* fetch relation to intersect with the next product. */ 05092 relation = array_fetch(bdd_t*, relationArray, i); 05093 if (smoothVarCubeArray) 05094 smoothVarCube = array_fetch(mdd_t*, smoothVarCubeArray, i + 1); 05095 else 05096 smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i + 1); 05097 05098 /* Clipping allowed only if clipping option is specified, partial 05099 * image is allowed, clipping depth is meaningful and sizes are not 05100 * under control. 05101 */ 05102 if ((PIoption != NULL) && 05103 (partialImageAllowed) && 05104 (partialImageMethod == Img_PIClipping_c) && 05105 (nvars >= clippingDepth)) { 05106 /* if conjuncts too small, dont clip. */ 05107 if ((bdd_size(product) > partialImageThreshold) || 05108 (bdd_size(relation) > partialImageThreshold)) { 05109 allowClipping = TRUE; 05110 } 05111 } 05112 05113 if (lazySiftFlag) { 05114 int j; 05115 int nVars = bdd_num_vars(mddManager); 05116 var_set_t *sup_ids = bdd_get_support(relation); 05117 05118 for (j = 0; j < nVars; j++) { 05119 if (var_set_get_elt(sup_ids, j) == 1) { 05120 if (bdd_is_ns_var(mddManager, j)) 05121 bdd_reset_var_to_be_grouped(mddManager, j); 05122 else if (!bdd_is_ps_var(mddManager, j)) 05123 bdd_reset_var_to_be_grouped(mddManager, j); 05124 } 05125 } 05126 var_set_free(sup_ids); 05127 } 05128 05129 /* if clipping not allowed, do regular and-abstract */ 05130 if (!allowClipping) { 05131 if (smoothVarCubeArray) { 05132 if (bdd_is_tautology(smoothVarCube, 1)) 05133 tmpProduct = bdd_and(product, relation, 1, 1); 05134 else { 05135 tmpProduct = bdd_and_smooth_with_cube(product, relation, 05136 smoothVarCube); 05137 } 05138 } else { 05139 if (array_n(smoothVarBddArray) == 0) 05140 tmpProduct = bdd_and(product, relation, 1, 1); 05141 else 05142 tmpProduct = bdd_and_smooth(product, relation, smoothVarBddArray); 05143 } 05144 } else { 05145 /* the conditions to clip are that partial image is allowed, 05146 * partial image method is set to clipping, clipping depth 05147 * is meaningful and either the product or the relation is 05148 * larger than the partial image threshold. 05149 */ 05150 if (smoothVarCubeArray) 05151 smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i+1); 05152 tmpProduct = ComputeClippedAndAbstract(product, relation, 05153 smoothVarBddArray, nvars, 05154 clippingDepth, partial, verbosity); 05155 } 05156 05157 if (lazySiftFlag) { 05158 int k, index; 05159 bdd_t *svar; 05160 05161 if (smoothVarCubeArray) 05162 smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i+1); 05163 for (k = 0; k < array_n(smoothVarBddArray); k++) { 05164 svar = array_fetch(bdd_t *, smoothVarBddArray, k); 05165 index = bdd_top_var_id(svar); 05166 bdd_set_var_to_be_grouped(mddManager, index); 05167 } 05168 } 05169 05170 bdd_free(product); 05171 product = tmpProduct; 05172 05173 /* subset if necessary */ 05174 if ((i != array_n(relationArray)) && 05175 (partialImageAllowed) && 05176 (partialImageMethod == Img_PIApprox_c)) { 05177 intermediateSize = bdd_size(product); 05178 /* approximate if the intermediate product is too large. */ 05179 if (intermediateSize > partialImageThreshold) { 05180 if (verbosity >= 2) { 05181 (void) fprintf(vis_stdout, "Intermediate Block %d Size = %10d\n", i, 05182 intermediateSize); 05183 } 05184 newProduct = ComputeSubsetOfIntermediateProduct(product, PIoption); 05185 if (verbosity >= 2) { 05186 if (!bdd_equal(newProduct, product)) { 05187 (void)fprintf(vis_stdout, 05188 "Intermediate Block Subset Size = %10d\n", 05189 bdd_size(newProduct)); 05190 } else { 05191 (void)fprintf(vis_stdout, "Intermediate Block unchanged\n"); 05192 } 05193 } 05194 /* record if partial image occurred */ 05195 if (!bdd_equal(newProduct, product)) { 05196 *partial = TRUE; 05197 intermediateSize = bdd_size(product); 05198 } 05199 bdd_free(product); 05200 product = newProduct; 05201 } 05202 } 05203 05204 /* keep track of intermediate product size */ 05205 if (verbosity >= 2) { 05206 if ((partialImageMethod != Img_PIApprox_c) || 05207 (!partialImageAllowed) || 05208 ( i == array_n(relationArray))) { 05209 intermediateSize = bdd_size(product); 05210 } 05211 if (maxSize < intermediateSize) { 05212 maxSize = intermediateSize; 05213 } 05214 } 05215 } 05216 if (lazySiftFlag) { 05217 int nVars = bdd_num_vars(mddManager); 05218 for (i = 0; i < nVars; i++) { 05219 if (bdd_is_ps_var(mddManager, i)) 05220 bdd_reset_var_to_be_grouped(mddManager, i); 05221 else 05222 bdd_set_var_to_be_grouped(mddManager, i); 05223 } 05224 } 05225 if (verbosity >= 2) { 05226 (void)fprintf(vis_stdout, 05227 "Max. BDD size for intermediate product = %10d\n", maxSize); 05228 }/* for all clusters */ 05229 05230 return product; 05231 } /* end of BddLinearAndSmooth */ 05232 05246 static void 05247 HashIdToBddTable(st_table *table, array_t *idArray, 05248 array_t *bddArray) 05249 { 05250 int i; 05251 for (i=0; i<array_n(idArray); i++) { 05252 int id; 05253 bdd_t *bdd; 05254 id = array_fetch(int, idArray, i); 05255 bdd = array_fetch(bdd_t*, bddArray, i); 05256 st_insert(table, (char*)(long)id, (char *)bdd); 05257 } 05258 } 05259 05260 05274 static void 05275 PrintSmoothIntroducedCount(array_t *clusterArray, array_t 05276 **arraySmoothVarBddArrayPtr, 05277 array_t *psBddIdArray, array_t 05278 *nsBddIdArray) 05279 { 05280 int i,j; 05281 st_table *nsBddIdTable, *supportTable, *psBddIdTable; 05282 bdd_t *trans; 05283 int introducedCount; 05284 bdd_t *tmp; 05285 st_generator *stgen; 05286 long varId; 05287 array_t *smoothVarBddArray, *arraySmoothVarBddArray; 05288 array_t *smoothVarBddIdArray = NIL(array_t); 05289 int psCount, piNdCount; 05290 05291 if (arraySmoothVarBddArrayPtr == NIL(array_t*)) 05292 arraySmoothVarBddArray = NIL(array_t); 05293 else 05294 arraySmoothVarBddArray = *arraySmoothVarBddArrayPtr; 05295 05296 (void) fprintf(vis_stdout, "**********************************************\n"); 05297 nsBddIdTable = st_init_table(st_numcmp, st_numhash); 05298 for (i=0; i<array_n(nsBddIdArray); i++) 05299 st_insert(nsBddIdTable, (char *)(long) array_fetch(int, nsBddIdArray, i), 05300 (char *) NULL); 05301 psBddIdTable = st_init_table(st_numcmp, st_numhash); 05302 for (i=0; i<array_n(psBddIdArray); i++) 05303 st_insert(psBddIdTable, (char *)(long) array_fetch(int, psBddIdArray, i), 05304 (char *) NULL); 05305 05306 for (i=0; i<=array_n(clusterArray)-1; i++) { 05307 trans = array_fetch(bdd_t*, clusterArray, i); 05308 supportTable = ImgBddGetSupportIdTable(trans); 05309 psCount = 0; 05310 piNdCount = 0; 05311 if (arraySmoothVarBddArray != NIL(array_t)) { 05312 smoothVarBddArray = array_fetch(array_t*, arraySmoothVarBddArray, i); 05313 smoothVarBddIdArray = bdd_get_varids(smoothVarBddArray); 05314 for (j=0; j<array_n(smoothVarBddIdArray);j++) { 05315 if (st_is_member(psBddIdTable, (char *)(long) 05316 array_fetch(int, smoothVarBddIdArray, j))) 05317 psCount++; 05318 else 05319 piNdCount++; 05320 } 05321 } 05322 introducedCount = 0; 05323 st_foreach_item(nsBddIdTable, stgen, &varId, &tmp) { 05324 if (st_is_member(supportTable, (char *)varId)) { 05325 introducedCount++; 05326 st_delete(nsBddIdTable,&varId, NULL); 05327 } 05328 } 05329 (void)fprintf(vis_stdout, 05330 "Tr no = %3d\tSmooth PS # = %3d\tSmooth PI # = %3d\tIntroduced # = %d\n", i, 05331 psCount, piNdCount, introducedCount); 05332 st_free_table(supportTable); 05333 array_free(smoothVarBddIdArray); 05334 } 05335 st_free_table(nsBddIdTable); 05336 st_free_table(psBddIdTable); 05337 } 05338 05348 static void 05349 PrintBddIdFromBddArray(array_t *bddArray) 05350 { 05351 int i; 05352 array_t *idArray = bdd_get_varids(bddArray); 05353 fprintf(vis_stdout, 05354 "**************** printing bdd ids from the bdd array ***********\n"); 05355 fprintf(vis_stdout,"%d::\t", array_n(idArray)); 05356 for (i=0;i<array_n(idArray); i++) { 05357 fprintf(vis_stdout," %d ", (int)array_fetch(int, idArray, i)); 05358 } 05359 fprintf(vis_stdout,"\n******************\n"); 05360 array_free(idArray); 05361 return; 05362 } 05363 05373 static void 05374 PrintBddIdTable(st_table *idTable) 05375 { 05376 st_generator *stgen; 05377 long varId; 05378 fprintf(vis_stdout, 05379 "**************** printing bdd ids from the id table ***********\n"); 05380 fprintf(vis_stdout,"%d::\t", st_count(idTable)); 05381 st_foreach_item(idTable, stgen, &varId, NIL(char *)) { 05382 fprintf(vis_stdout," %d ", (int) varId); 05383 } 05384 fprintf(vis_stdout,"\n******************\n"); 05385 return; 05386 } 05387 05399 static void 05400 PartitionTraverseRecursively(mdd_manager *mddManager, vertex_t *vertex, 05401 int mddId, st_table *vertexTable, 05402 array_t *relationArray, 05403 st_table *domainQuantifyVarMddIdTable, 05404 array_t *quantifyVarMddIdArray) 05405 { 05406 Mvf_Function_t *mvf; 05407 lsList faninEdges; 05408 lsGen gen; 05409 vertex_t *faninVertex; 05410 edge_t *faninEdge; 05411 array_t *varBddRelationArray; 05412 05413 if (st_is_member(vertexTable, (char *)vertex)) return; 05414 st_insert(vertexTable, (char *)vertex, NIL(char)); 05415 if (mddId != -1) { /* This is not the next state function node */ 05416 /* There is an mdd variable associated with this vertex */ 05417 array_insert_last(int, quantifyVarMddIdArray, mddId); 05418 mvf = Part_VertexReadFunction(vertex); 05419 /*relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);*/ 05420 varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, mddId, mvf); 05421 array_append(relationArray, varBddRelationArray); 05422 array_free(varBddRelationArray); 05423 /*array_insert_last(mdd_t *, relationArray, relation);*/ 05424 } 05425 faninEdges = g_get_in_edges(vertex); 05426 if (lsLength(faninEdges) == 0) return; 05427 lsForEachItem(faninEdges, gen, faninEdge) { 05428 faninVertex = g_e_source(faninEdge); 05429 mddId = Part_VertexReadMddId(faninVertex); 05430 if (st_is_member(domainQuantifyVarMddIdTable, (char *)(long)mddId)) { 05431 /* This is either domain var or quantify var */ 05432 /* continue */ 05433 continue; 05434 } 05435 PartitionTraverseRecursively(mddManager, faninVertex, mddId, vertexTable, 05436 relationArray, 05437 domainQuantifyVarMddIdTable, 05438 quantifyVarMddIdArray); 05439 } 05440 } 05441 05442 05452 static void 05453 PrintPartitionRecursively(vertex_t *vertex, st_table *vertexTable, int indent) 05454 { 05455 int i; 05456 lsList faninEdges; 05457 lsGen gen; 05458 vertex_t *faninVertex; 05459 edge_t *faninEdge; 05460 05461 if (st_is_member(vertexTable, (char *)vertex)) return; 05462 st_insert(vertexTable, (char *)vertex, NIL(char)); 05463 for(i=0; i<= indent; i++) fprintf(vis_stdout," "); 05464 fprintf(vis_stdout,"%s %d\n", Part_VertexReadName(vertex), 05465 Part_VertexReadMddId(vertex)); 05466 faninEdges = g_get_in_edges(vertex); 05467 if (lsLength(faninEdges) == 0) return; 05468 lsForEachItem(faninEdges, gen, faninEdge) { 05469 faninVertex = g_e_source(faninEdge); 05470 PrintPartitionRecursively(faninVertex, vertexTable,indent+2); 05471 } 05472 } 05473 05492 static bdd_t * 05493 RecomputeImageIfNecessary(ImgFunctionData_t *functionData, 05494 mdd_manager *mddManager, 05495 bdd_t *domainSubset, 05496 array_t *relationArray, 05497 array_t *arraySmoothVarBddArray, 05498 array_t *smoothVarCubeArray, 05499 int verbosity, 05500 ImgPartialImageOption_t *PIoption, 05501 array_t *toCareSetArray, 05502 boolean *partial, boolean lazySiftFlag) 05503 { 05504 int oldPIThreshold = 0, oldPISize; 05505 double oldClippingFrac = IMG_PI_CLIP_DEPTH; 05506 boolean realRequired = FALSE; 05507 mdd_t *image = NIL(mdd_t); 05508 05509 /* relax values to compute a non-trivial partial image */ 05510 if (PIoption->partialImageMethod == Img_PIApprox_c) { 05511 oldPIThreshold = PIoption->partialImageThreshold; 05512 PIoption->partialImageThreshold *= 2; 05513 if (!PIoption->partialImageThreshold) 05514 PIoption->partialImageThreshold = IMG_PI_SP_THRESHOLD; 05515 } else if (PIoption->partialImageMethod == Img_PIClipping_c) { 05516 oldClippingFrac = PIoption->clippingDepthFrac; 05517 PIoption->clippingDepthFrac = 05518 (PIoption->clippingDepthFrac < IMG_PI_CLIP_DEPTH_FINAL) ? 05519 IMG_PI_CLIP_DEPTH_FINAL : PIoption->clippingDepthFrac; 05520 } 05521 if (((PIoption->partialImageMethod == Img_PIClipping_c) && 05522 (oldClippingFrac != PIoption->clippingDepthFrac)) || 05523 (PIoption->partialImageMethod == Img_PIApprox_c)) { 05524 if (verbosity >= 2) { 05525 fprintf(vis_stdout, 05526 "IMG: No new states, computing image again with relaxed thresholds.\n"); 05527 if (PIoption->partialImageMethod == Img_PIApprox_c) { 05528 fprintf(vis_stdout, "IMG: Relaxed hd_partial_image_threshold to %d\n", 05529 PIoption->partialImageThreshold); 05530 } else if (PIoption->partialImageMethod == Img_PIClipping_c) { 05531 fprintf(vis_stdout, 05532 "IMG: Relaxed hd_partial_image_clipping_depth to %g\n", 05533 PIoption->clippingDepthFrac); 05534 } 05535 } 05536 05537 *partial = TRUE; 05538 /* if values were relaxed, compute image again. */ 05539 image = BddLinearAndSmooth(mddManager, domainSubset, relationArray, 05540 arraySmoothVarBddArray, smoothVarCubeArray, 05541 verbosity, PIoption, partial, lazySiftFlag); 05542 05543 /* check if new states were produced. */ 05544 if (*partial) { 05545 if (bdd_leq_array(image, toCareSetArray, 1, 0)) { 05546 bdd_free(image); 05547 if (PIoption->partialImageMethod == Img_PIApprox_c) { 05548 /* relax approximation values some more. */ 05549 oldPISize = PIoption->partialImageSize; 05550 PIoption->partialImageSize *= 2; 05551 if (!PIoption->partialImageSize) 05552 PIoption->partialImageSize = IMG_PI_SP_THRESHOLD; 05553 05554 if (verbosity >= 2) { 05555 fprintf(vis_stdout, 05556 "IMG: No new states, computing image again with relaxed thresholds.\n"); 05557 fprintf(vis_stdout, "IMG: Relaxed hd_partial_image_size to %d\n", 05558 PIoption->partialImageSize); 05559 } 05560 05561 *partial = TRUE; 05562 image = BddLinearAndSmooth(mddManager, domainSubset, relationArray, 05563 arraySmoothVarBddArray, smoothVarCubeArray, 05564 verbosity, PIoption, partial, 05565 lazySiftFlag); 05566 PIoption->partialImageSize = oldPISize; 05567 05568 /* check if new states were produced. */ 05569 if (*partial) { 05570 if (bdd_leq_array(image, toCareSetArray, 1, 0)) { 05571 bdd_free(image); 05572 realRequired = TRUE; 05573 } 05574 } 05575 } else if (PIoption->partialImageMethod == Img_PIClipping_c) { 05576 /* compute real image since clipping depth cannot be increased. */ 05577 realRequired = TRUE; 05578 } 05579 } 05580 } /* require recomputation */ 05581 } else { /* clipping depth could not be increased. */ 05582 /* compute real image since clipping depth cannot be increased. */ 05583 realRequired = TRUE; 05584 } 05585 05586 /* reset the values to the orginal values. */ 05587 if (PIoption->partialImageMethod == Img_PIClipping_c) { 05588 PIoption->clippingDepthFrac = oldClippingFrac; 05589 } else if (PIoption->partialImageMethod == Img_PIApprox_c) { 05590 PIoption->partialImageThreshold = oldPIThreshold; 05591 } 05592 /* if the actual image is required compute it. */ 05593 if (realRequired) { 05594 if (verbosity >= 2) { 05595 fprintf(vis_stdout, "IMG: No new states, computing exact image.\n"); 05596 } 05597 *partial = FALSE; 05598 image = BddLinearAndSmooth(mddManager, domainSubset, relationArray, 05599 arraySmoothVarBddArray, smoothVarCubeArray, 05600 verbosity, PIoption, partial, lazySiftFlag); 05601 assert(!(*partial)); 05602 } 05603 05604 return (image); 05605 } /* end of RecomputeImageIfNecessary */ 05606 05607 05617 static bdd_t * 05618 ComputeSubsetOfIntermediateProduct(bdd_t *product, 05619 ImgPartialImageOption_t *PIoption) 05620 { 05621 int partialImageSize = PIoption->partialImageSize; 05622 int nvars = PIoption->nvars; 05623 bdd_t *newProduct; 05624 05625 switch (PIoption->partialImageApproxMethod) { 05626 case BDD_APPROX_HB: 05627 { 05628 int tempSize; 05629 tempSize = (partialImageSize < IMG_PI_SP_THRESHOLD) ? 05630 IMG_PI_SP_THRESHOLD : partialImageSize; 05631 newProduct = bdd_approx_hb(product, 05632 (bdd_approx_dir_t)BDD_UNDER_APPROX, 05633 nvars, tempSize); 05634 break; 05635 } 05636 case BDD_APPROX_SP: 05637 { 05638 int tempSize; 05639 tempSize = (partialImageSize < IMG_PI_SP_THRESHOLD) ? 05640 IMG_PI_SP_THRESHOLD : partialImageSize; 05641 newProduct = bdd_approx_sp(product, 05642 (bdd_approx_dir_t)BDD_UNDER_APPROX, 05643 nvars, tempSize, 0); 05644 break; 05645 } 05646 case BDD_APPROX_UA: 05647 newProduct = bdd_approx_ua(product, 05648 (bdd_approx_dir_t)BDD_UNDER_APPROX, 05649 nvars, partialImageSize, 05650 0, PIoption->quality); 05651 break; 05652 case BDD_APPROX_RUA: 05653 newProduct = bdd_approx_remap_ua(product, 05654 (bdd_approx_dir_t)BDD_UNDER_APPROX, 05655 0, partialImageSize, 05656 PIoption->quality); 05657 break; 05658 case BDD_APPROX_COMP: 05659 { 05660 newProduct = bdd_approx_compress(product, 05661 (bdd_approx_dir_t)BDD_UNDER_APPROX, 05662 nvars, partialImageSize); 05663 } 05664 break; 05665 case BDD_APPROX_BIASED_RUA: 05666 newProduct = bdd_approx_biased_rua(product, 05667 (bdd_approx_dir_t)BDD_UNDER_APPROX, 05668 PIoption->bias, 05669 0, partialImageSize, 05670 PIoption->quality, 05671 PIoption->qualityBias); 05672 break; 05673 default : 05674 newProduct = bdd_approx_remap_ua(product, 05675 (bdd_approx_dir_t)BDD_UNDER_APPROX, 05676 0, partialImageSize, 05677 PIoption->quality); 05678 break; 05679 } 05680 return newProduct; 05681 } /* end of ComputeSubsetOfIntermediateProduct */ 05682 05693 static bdd_t * 05694 ComputeClippedAndAbstract(bdd_t *product, 05695 bdd_t *relation, 05696 array_t *smoothVarBddArray, 05697 int nvars, 05698 int clippingDepth, 05699 boolean *partial, 05700 int verbosity) 05701 { 05702 bdd_t *tmpProduct; 05703 05704 /* compute clipped image */ 05705 tmpProduct = bdd_clipping_and_smooth(product, relation, 05706 smoothVarBddArray, clippingDepth, 0); 05707 /* if product is zero, compute clipped image with increased 05708 * clipping depth 05709 */ 05710 if (bdd_is_tautology(tmpProduct, 0)) { 05711 bdd_free(tmpProduct); 05712 tmpProduct = bdd_clipping_and_smooth(product, relation, 05713 smoothVarBddArray, 05714 (int) (nvars*IMG_PI_CLIP_DEPTH_FINAL), 05715 0); 05716 05717 /* if clipped image is zero, compute unclipped image */ 05718 if (bdd_is_tautology(tmpProduct, 0)) { 05719 if (verbosity >= 2) { 05720 fprintf(vis_stdout, 05721 "IMG: Clipping failed, computing exact and-abstract\n"); 05722 } 05723 bdd_free(tmpProduct); 05724 tmpProduct = bdd_and_smooth(product, relation, 05725 smoothVarBddArray); 05726 } else *partial = TRUE; 05727 05728 } else *partial = TRUE; 05729 05730 return tmpProduct; 05731 } /* end of ComputeClippedAndAbstract */ 05732 05733 05743 static array_t * 05744 CopyArrayBddArray(array_t *arrayBddArray) 05745 { 05746 int i, j; 05747 array_t *newArrayBddArray = array_alloc(array_t *, 0); 05748 array_t *bddArray, *newBddArray; 05749 mdd_t *bdd; 05750 05751 for (i = 0; i < array_n(arrayBddArray); i++) { 05752 bddArray = array_fetch(array_t *, arrayBddArray, i); 05753 newBddArray = array_alloc(mdd_t *, 0); 05754 for (j = 0; j < array_n(bddArray); j++) { 05755 bdd = array_fetch(mdd_t *, bddArray, j); 05756 array_insert(mdd_t *, newBddArray, j, bdd_dup(bdd)); 05757 } 05758 array_insert(array_t *, newArrayBddArray, i, newBddArray); 05759 } 05760 05761 return(newArrayBddArray); 05762 } 05763 05764 05774 static void 05775 PrintPartitionedTransitionRelation(mdd_manager *mddManager, 05776 Iwls95Info_t *info, 05777 Img_DirectionType directionType) 05778 { 05779 array_t *relationArray; 05780 array_t *arraySmoothVarBddArray; 05781 05782 if (directionType == Img_Forward_c) { 05783 relationArray = info->fwdClusteredRelationArray; 05784 arraySmoothVarBddArray = info->fwdArraySmoothVarBddArray; 05785 } else if (directionType == Img_Backward_c) { 05786 relationArray = info->bwdClusteredRelationArray; 05787 arraySmoothVarBddArray = info->bwdArraySmoothVarBddArray; 05788 } else { 05789 return; 05790 } 05791 05792 ImgPrintPartitionedTransitionRelation(mddManager, relationArray, 05793 arraySmoothVarBddArray); 05794 } 05795 05796 05806 static void 05807 ReorderPartitionedTransitionRelation(Iwls95Info_t *info, 05808 ImgFunctionData_t *functionData, 05809 Img_DirectionType directionType) 05810 { 05811 array_t *domainVarMddIdArray = functionData->domainVars; 05812 array_t *rangeVarMddIdArray = functionData->rangeVars; 05813 array_t *quantifyVarMddIdArray = array_dup(functionData->quantifyVars); 05814 graph_t *mddNetwork = functionData->mddNetwork; 05815 mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork); 05816 array_t *rangeVarBddArray, *domainVarBddArray, *quantifyVarBddArray; 05817 array_t *clusteredRelationArray; 05818 st_table *varsTable = st_init_table(st_numcmp, st_numhash); 05819 int i, j, k, mddId; 05820 array_t *smoothVarBddArray, *arraySmoothVarBddArray; 05821 mdd_t *mdd; 05822 array_t *supportIdArray; 05823 05824 /* Finds the variables which are neither state variable nor primary input 05825 * from previous smooth variable array, and put those variable into 05826 * quantify variable array. 05827 */ 05828 for (i =0 ; i< array_n(domainVarMddIdArray); i++) { 05829 mddId = array_fetch(int, domainVarMddIdArray, i); 05830 st_insert(varsTable, (char *)(long)mddId, NIL(char)); 05831 } 05832 for (i = 0; i < array_n(rangeVarMddIdArray); i++) { 05833 mddId = array_fetch(int, rangeVarMddIdArray, i); 05834 st_insert(varsTable, (char *)(long)mddId, NIL(char)); 05835 } 05836 for (i = 0; i < array_n(quantifyVarMddIdArray); i++) { 05837 mddId = array_fetch(int, quantifyVarMddIdArray, i); 05838 st_insert(varsTable, (char *)(long)mddId, NIL(char)); 05839 } 05840 if (directionType == Img_Forward_c || directionType == Img_Both_c) 05841 arraySmoothVarBddArray = info->fwdArraySmoothVarBddArray; 05842 else 05843 arraySmoothVarBddArray = info->bwdArraySmoothVarBddArray; 05844 for (i = 0; i < array_n(arraySmoothVarBddArray); i++) { 05845 smoothVarBddArray = array_fetch(array_t *, arraySmoothVarBddArray, i); 05846 for (j = 0; j < array_n(smoothVarBddArray); j++) { 05847 mdd = array_fetch(mdd_t *, smoothVarBddArray, j); 05848 supportIdArray = mdd_get_support(mddManager, mdd); 05849 for (k = 0; k < array_n(supportIdArray); k++) { 05850 mddId = array_fetch(int, supportIdArray, k); 05851 if (!st_lookup(varsTable, (char *)(long)mddId, NIL(char *))) { 05852 array_insert_last(int, quantifyVarMddIdArray, mddId); 05853 st_insert(varsTable, (char *)(long)mddId, NIL(char)); 05854 } 05855 } 05856 array_free(supportIdArray); 05857 } 05858 } 05859 st_free_table(varsTable); 05860 05861 /* Get the Bdds from Mdd Ids */ 05862 rangeVarBddArray = functionData->rangeBddVars; 05863 domainVarBddArray = functionData->domainBddVars; 05864 quantifyVarBddArray = mdd_id_array_to_bdd_array(mddManager, 05865 quantifyVarMddIdArray); 05866 array_free(quantifyVarMddIdArray); 05867 05868 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 05869 clusteredRelationArray = info->fwdClusteredRelationArray; 05870 mdd_array_array_free(info->fwdArraySmoothVarBddArray); 05871 info->fwdClusteredRelationArray = NIL(array_t); 05872 info->fwdArraySmoothVarBddArray = NIL(array_t); 05873 if (info->method == Img_Iwls95_c) { 05874 OrderRelationArray(mddManager, clusteredRelationArray, 05875 domainVarBddArray, quantifyVarBddArray, 05876 rangeVarBddArray, info->option, 05877 &info->fwdClusteredRelationArray, 05878 &info->fwdArraySmoothVarBddArray); 05879 } else if (info->method == Img_Mlp_c) { 05880 ImgMlpOrderRelationArray(mddManager, clusteredRelationArray, 05881 domainVarBddArray, quantifyVarBddArray, 05882 rangeVarBddArray, Img_Forward_c, 05883 &info->fwdClusteredRelationArray, 05884 &info->fwdArraySmoothVarBddArray, 05885 info->option); 05886 } else 05887 assert(0); 05888 mdd_array_free(clusteredRelationArray); 05889 05890 if (functionData->createVarCubesFlag) { 05891 if (info->fwdSmoothVarCubeArray) 05892 mdd_array_free(info->fwdSmoothVarCubeArray); 05893 info->fwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 05894 info->fwdArraySmoothVarBddArray); 05895 } 05896 05897 if (info->option->verbosity > 2) { 05898 PrintPartitionedTransitionRelation(mddManager, info, Img_Forward_c); 05899 } 05900 } 05901 05902 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 05903 clusteredRelationArray = info->bwdClusteredRelationArray; 05904 mdd_array_array_free(info->bwdArraySmoothVarBddArray); 05905 info->bwdClusteredRelationArray = NIL(array_t); 05906 info->bwdArraySmoothVarBddArray = NIL(array_t); 05907 if (info->method == Img_Iwls95_c) { 05908 OrderRelationArray(mddManager, clusteredRelationArray, 05909 rangeVarBddArray, quantifyVarBddArray, 05910 domainVarBddArray, info->option, 05911 &info->bwdClusteredRelationArray, 05912 &info->bwdArraySmoothVarBddArray); 05913 } else if (info->method == Img_Mlp_c) { 05914 ImgMlpOrderRelationArray(mddManager, clusteredRelationArray, 05915 domainVarBddArray, quantifyVarBddArray, 05916 rangeVarBddArray, Img_Backward_c, 05917 &info->bwdClusteredRelationArray, 05918 &info->bwdArraySmoothVarBddArray, info->option); 05919 } else 05920 assert(0); 05921 mdd_array_free(clusteredRelationArray); 05922 05923 if (functionData->createVarCubesFlag) { 05924 if (info->bwdSmoothVarCubeArray) 05925 mdd_array_free(info->bwdSmoothVarCubeArray); 05926 info->bwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 05927 info->bwdArraySmoothVarBddArray); 05928 } 05929 05930 if (info->option->verbosity > 2) { 05931 PrintPartitionedTransitionRelation(mddManager, info, Img_Backward_c); 05932 } 05933 } 05934 05935 /* Free the Bdd arrays */ 05936 mdd_array_free(quantifyVarBddArray); 05937 } 05938 05939 05949 static void 05950 UpdateQuantificationSchedule(Iwls95Info_t *info, 05951 ImgFunctionData_t *functionData, 05952 Img_DirectionType directionType) 05953 { 05954 graph_t *mddNetwork = functionData->mddNetwork; 05955 mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork); 05956 array_t *clusteredRelationArray; 05957 st_table *quantifyVarsTable; 05958 var_set_t *supportVarSet; 05959 int i, j, id, nRelations; 05960 int pos; 05961 long longid; 05962 array_t *smoothVarBddArray, **smoothVarBddArrayPtr; 05963 bdd_t *bdd, *relation; 05964 st_generator *gen; 05965 05966 if (directionType == Img_Forward_c || directionType == Img_Both_c) { 05967 nRelations = array_n(info->fwdClusteredRelationArray); 05968 quantifyVarsTable = st_init_table(st_numcmp, st_numhash); 05969 for (i = 0; i <= nRelations; i++) { 05970 smoothVarBddArray = array_fetch(array_t *, 05971 info->fwdArraySmoothVarBddArray, i); 05972 for (j = 0; j < array_n(smoothVarBddArray); j++) { 05973 bdd = array_fetch(mdd_t *, smoothVarBddArray, j); 05974 id = (int)bdd_top_var_id(bdd); 05975 st_insert(quantifyVarsTable, (char *)(long)id, NIL(char)); 05976 } 05977 } 05978 05979 clusteredRelationArray = info->fwdClusteredRelationArray; 05980 for (i = 0; i < nRelations; i++) { 05981 relation = array_fetch(bdd_t *, clusteredRelationArray, i); 05982 supportVarSet = bdd_get_support(relation); 05983 for (j = 0; j < supportVarSet->n_elts; j++) { 05984 if (var_set_get_elt(supportVarSet, j) == 1) { 05985 if (st_is_member(quantifyVarsTable, (char *)(long)j)) 05986 st_insert(quantifyVarsTable, (char *)(long)j, (char *)(long)(i+1)); 05987 } 05988 } 05989 var_set_free(supportVarSet); 05990 } 05991 05992 mdd_array_array_free(info->fwdArraySmoothVarBddArray); 05993 info->fwdArraySmoothVarBddArray = array_alloc(array_t *, nRelations + 1); 05994 smoothVarBddArrayPtr = ALLOC(array_t *, sizeof(array_t *) * (nRelations+1)); 05995 for (i = 0; i <= nRelations; i++) { 05996 smoothVarBddArray = array_alloc(bdd_t *, 0); 05997 smoothVarBddArrayPtr[i] = smoothVarBddArray; 05998 array_insert(array_t *, info->fwdArraySmoothVarBddArray, i, 05999 smoothVarBddArray); 06000 } 06001 06002 st_foreach_item_int(quantifyVarsTable, gen, &longid, &pos) { 06003 id = (int) longid; 06004 smoothVarBddArray = array_fetch(array_t *, 06005 info->fwdArraySmoothVarBddArray, pos); 06006 bdd = bdd_var_with_index(mddManager, id); 06007 array_insert_last(bdd_t *, smoothVarBddArray, bdd); 06008 } 06009 06010 FREE(smoothVarBddArrayPtr); 06011 st_free_table(quantifyVarsTable); 06012 06013 if (functionData->createVarCubesFlag) { 06014 if (info->fwdSmoothVarCubeArray) 06015 mdd_array_free(info->fwdSmoothVarCubeArray); 06016 info->fwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 06017 info->fwdArraySmoothVarBddArray); 06018 } 06019 06020 if (info->option->verbosity > 2) { 06021 PrintPartitionedTransitionRelation(mddManager, info, Img_Forward_c); 06022 } 06023 } 06024 06025 if (directionType == Img_Backward_c || directionType == Img_Both_c) { 06026 nRelations = array_n(info->bwdClusteredRelationArray); 06027 quantifyVarsTable = st_init_table(st_numcmp, st_numhash); 06028 for (i = 0; i <= nRelations; i++) { 06029 smoothVarBddArray = array_fetch(array_t *, 06030 info->bwdArraySmoothVarBddArray, i); 06031 for (j = 0; j < array_n(smoothVarBddArray); j++) { 06032 bdd = array_fetch(mdd_t *, smoothVarBddArray, j); 06033 id = (int)bdd_top_var_id(bdd); 06034 st_insert(quantifyVarsTable, (char *)(long)id, (char *)(long)0); 06035 } 06036 } 06037 06038 clusteredRelationArray = info->bwdClusteredRelationArray; 06039 for (i = 0; i < nRelations; i++) { 06040 relation = array_fetch(bdd_t *, clusteredRelationArray, i); 06041 supportVarSet = bdd_get_support(relation); 06042 for (j = 0; j < supportVarSet->n_elts; j++) { 06043 if (var_set_get_elt(supportVarSet, j) == 1) { 06044 if (st_is_member(quantifyVarsTable, (char *)(long)j)) 06045 st_insert(quantifyVarsTable, (char *)(long)j, (char *)(long)(i+1)); 06046 } 06047 } 06048 var_set_free(supportVarSet); 06049 } 06050 06051 mdd_array_array_free(info->bwdArraySmoothVarBddArray); 06052 info->bwdArraySmoothVarBddArray = array_alloc(array_t *, nRelations + 1); 06053 smoothVarBddArrayPtr = ALLOC(array_t *, sizeof(array_t *) * (nRelations+1)); 06054 for (i = 0; i <= nRelations; i++) { 06055 smoothVarBddArray = array_alloc(bdd_t *, 0); 06056 smoothVarBddArrayPtr[i] = smoothVarBddArray; 06057 array_insert(array_t *, info->bwdArraySmoothVarBddArray, i, 06058 smoothVarBddArray); 06059 } 06060 06061 st_foreach_item_int(quantifyVarsTable, gen, &longid, &pos) { 06062 id = (int) longid; 06063 smoothVarBddArray = array_fetch(array_t *, 06064 info->bwdArraySmoothVarBddArray, pos); 06065 bdd = bdd_var_with_index(mddManager, id); 06066 array_insert_last(bdd_t *, smoothVarBddArray, bdd); 06067 } 06068 06069 FREE(smoothVarBddArrayPtr); 06070 st_free_table(quantifyVarsTable); 06071 06072 if (functionData->createVarCubesFlag) { 06073 if (info->bwdSmoothVarCubeArray) 06074 mdd_array_free(info->bwdSmoothVarCubeArray); 06075 info->bwdSmoothVarCubeArray = MakeSmoothVarCubeArray(mddManager, 06076 info->bwdArraySmoothVarBddArray); 06077 } 06078 06079 if (info->option->verbosity > 2) { 06080 PrintPartitionedTransitionRelation(mddManager, info, Img_Backward_c); 06081 } 06082 } 06083 } 06084 06085 06095 static array_t * 06096 MakeSmoothVarCubeArray(mdd_manager *mddManager, array_t *arraySmoothVarBddArray) 06097 { 06098 int i, j; 06099 array_t *smoothVarBddArray; 06100 array_t *cubeArray = array_alloc(mdd_t *, 0); 06101 mdd_t *cube, *var, *tmp; 06102 06103 arrayForEachItem(array_t *, arraySmoothVarBddArray, i, smoothVarBddArray) { 06104 cube = mdd_one(mddManager); 06105 arrayForEachItem(mdd_t *, smoothVarBddArray, j, var) { 06106 tmp = mdd_and(cube, var, 1, 1); 06107 mdd_free(cube); 06108 cube = tmp; 06109 } 06110 array_insert_last(mdd_t *, cubeArray, cube); 06111 } 06112 return(cubeArray); 06113 } 06114 06115 06129 static mdd_t * 06130 TrmEliminateDependVars(Img_ImageInfo_t *imageInfo, array_t *relationArray, 06131 mdd_t *states, mdd_t **dependRelations) 06132 { 06133 int nDependVars; 06134 mdd_t *newStates; 06135 Iwls95Info_t *info = (Iwls95Info_t *) imageInfo->methodData; 06136 06137 newStates = ImgTrmEliminateDependVars(&imageInfo->functionData, relationArray, 06138 states, dependRelations, &nDependVars); 06139 if (nDependVars) { 06140 if (imageInfo->verbosity > 0) 06141 (void)fprintf(vis_stdout, "Eliminated %d vars.\n", nDependVars); 06142 info->averageFoundDependVars = (info->averageFoundDependVars * 06143 (float)info->nFoundDependVars + (float)nDependVars) / 06144 (float)(info->nFoundDependVars + 1); 06145 info->nFoundDependVars++; 06146 } 06147 06148 info->nPrevEliminatedFwd = nDependVars; 06149 return(newStates); 06150 } /* end of TfmEliminateDependVars */ 06151 06152 06163 static int 06164 TrmSignatureCompare(int *ptrX, int *ptrY) 06165 { 06166 if (signatures[*ptrY] > signatures[*ptrX]) 06167 return(1); 06168 if (signatures[*ptrY] < signatures[*ptrX]) 06169 return(-1); 06170 return(0); 06171 } /* end of TrmSignatureCompare */ 06172 06173 06183 static void 06184 SetupLazySifting(mdd_manager *mddManager, array_t *bddRelationArray, 06185 array_t *domainVarBddArray, array_t *quantifyVarBddArray, 06186 array_t *rangeVarBddArray, int verbosity) 06187 { 06188 int i, id, psId, nsId, psLevel, nsLevel; 06189 int nVars = bdd_num_vars(mddManager); 06190 int nUngroup = 0; 06191 int nGroup = 0; 06192 int nConst = 0; 06193 int *nonLambda = ALLOC(int, nVars); 06194 int nLambda = 0; 06195 int nDepend1to1 = 0; 06196 int nIndepend1to1 = 0; 06197 int nPairPsOnce = 0; 06198 int pairPsId; 06199 int constFlag; 06200 int dependFlag; 06201 int nDependPs; 06202 int nDependPi; 06203 bdd_t* relation; 06204 var_set_t* supIds; 06205 bdd_t *bdd, *psVar, *nsVar; 06206 06207 bdd_discard_all_var_groups(mddManager); 06208 for (i = 0; i < array_n(quantifyVarBddArray); i++) { 06209 bdd = array_fetch(bdd_t *, quantifyVarBddArray, i); 06210 id = bdd_top_var_id(bdd); 06211 bdd_set_pair_index(mddManager, id, id); 06212 bdd_set_pi_var(mddManager, id); 06213 bdd_reset_var_to_be_grouped(mddManager, id); 06214 } 06215 06216 for (i = 0; i < array_n(rangeVarBddArray); i++) { 06217 psVar = array_fetch(bdd_t *, domainVarBddArray, i); 06218 nsVar = array_fetch(bdd_t *, rangeVarBddArray, i); 06219 psId = bdd_top_var_id(psVar); 06220 nsId = bdd_top_var_id(nsVar); 06221 bdd_set_pair_index(mddManager, psId, nsId); 06222 bdd_set_pair_index(mddManager, nsId, psId); 06223 bdd_set_ps_var(mddManager, psId); 06224 bdd_set_ns_var(mddManager, nsId); 06225 bdd_reset_var_to_be_grouped(mddManager, psId); 06226 bdd_set_var_to_be_grouped(mddManager, nsId); 06227 } 06228 06229 if (array_n(domainVarBddArray) > array_n(rangeVarBddArray)) { 06230 for (i = array_n(rangeVarBddArray); i < array_n(domainVarBddArray); i++) { 06231 bdd = array_fetch(bdd_t *, domainVarBddArray, i); 06232 id = bdd_top_var_id(bdd); 06233 bdd_set_pair_index(mddManager, id, id); 06234 bdd_set_pi_var(mddManager, id); 06235 bdd_reset_var_to_be_grouped(mddManager, id); 06236 } 06237 } 06238 06239 memset(nonLambda, 0, sizeof(int) * nVars); 06240 for (i = 0; i < array_n(bddRelationArray); i++) { 06241 nsId = -1; 06242 pairPsId = -1; 06243 constFlag = 1; 06244 dependFlag = 0; 06245 nDependPs = 0; 06246 nDependPi = 0; 06247 relation = array_fetch(bdd_t *, bddRelationArray, i); 06248 supIds = bdd_get_support(relation); 06249 06250 for (id = 0; id < nVars; id++) { 06251 if (var_set_get_elt(supIds, id) == 1) { 06252 if (bdd_is_ns_var(mddManager, id)) { 06253 pairPsId = bdd_read_pair_index(mddManager, id); 06254 nsId = id; 06255 } else if (bdd_is_ps_var(mddManager, id)) { 06256 constFlag = 0; /* nonconst next sate function */ 06257 nonLambda[id]++; 06258 psId = id; 06259 /* At least one next state function depends on psvar id */ 06260 nDependPs++; 06261 } else { 06262 constFlag = 0; /* nonconst next state function */ 06263 nDependPi++; 06264 } 06265 } 06266 } 06267 if (nsId >= 0) { 06268 /* bitwise transition relation depends on some nsvar */ 06269 for (id = 0; id < nVars; id++) { 06270 if (var_set_get_elt(supIds, id) == 1) { 06271 if (pairPsId == id) { 06272 /* dependendent state pair */ 06273 nGroup++; 06274 dependFlag = 1; 06275 } 06276 } 06277 } 06278 if (dependFlag != 1) { 06279 /* independent state pair */ 06280 nUngroup++; 06281 if (constFlag == 1) { 06282 /* next state function is constant */ 06283 psLevel = bdd_get_level_from_id(mddManager, pairPsId); 06284 nsLevel = bdd_get_level_from_id(mddManager, nsId); 06285 if (psLevel == nsLevel - 1) { 06286 bdd = bdd_var_with_index(mddManager, pairPsId); 06287 bdd_new_var_block(bdd, 2); 06288 bdd_free(bdd); 06289 nConst++; 06290 } else if (psLevel == nsLevel + 1) { 06291 bdd = bdd_var_with_index(mddManager, nsId); 06292 bdd_new_var_block(bdd, 2); 06293 bdd_free(bdd); 06294 nConst++; 06295 } 06296 } else { 06297 bdd_set_var_to_be_ungrouped(mddManager, pairPsId); 06298 bdd_set_var_to_be_ungrouped(mddManager, nsId); 06299 } 06300 } else if (nDependPs == 1) { 06301 psLevel = bdd_get_level_from_id(mddManager, pairPsId); 06302 nsLevel = bdd_get_level_from_id(mddManager, nsId); 06303 if (psLevel == nsLevel - 1) { 06304 bdd = bdd_var_with_index(mddManager, pairPsId); 06305 bdd_new_var_block(bdd, 2); 06306 bdd_free(bdd); 06307 nDepend1to1++; 06308 } else if (psLevel == nsLevel + 1) { 06309 bdd = bdd_var_with_index(mddManager, nsId); 06310 bdd_new_var_block(bdd, 2); 06311 bdd_free(bdd); 06312 nDepend1to1++; 06313 } 06314 } else if (nonLambda[pairPsId] == 1) { 06315 psLevel = bdd_get_level_from_id(mddManager, pairPsId); 06316 nsLevel = bdd_get_level_from_id(mddManager, nsId); 06317 if (psLevel == nsLevel - 1) { 06318 bdd = bdd_var_with_index(mddManager, pairPsId); 06319 bdd_new_var_block(bdd, 2); 06320 bdd_free(bdd); 06321 nPairPsOnce++; 06322 } else if (psLevel == nsLevel + 1) { 06323 bdd = bdd_var_with_index(mddManager, nsId); 06324 bdd_new_var_block(bdd, 2); 06325 bdd_free(bdd); 06326 nPairPsOnce++; 06327 } 06328 } 06329 } else { 06330 /* bitwise transition relation does not depend on any nsvar */ 06331 nUngroup++; 06332 } 06333 var_set_free(supIds); 06334 } 06335 for (i = 0; i < nVars; i++) { 06336 if (bdd_is_ps_var(mddManager, i)) { 06337 if (nonLambda[i] == 0) { 06338 /* no next state function depends on psvar i */ 06339 psId = i; 06340 nsId = bdd_read_pair_index(mddManager, psId); 06341 psLevel = bdd_get_level_from_id(mddManager, psId); 06342 nsLevel = bdd_get_level_from_id(mddManager, nsId); 06343 nLambda++; 06344 if (psLevel == nsLevel - 1) { 06345 bdd = bdd_var_with_index(mddManager, psId); 06346 bdd_new_var_block(bdd, 2); 06347 bdd_free(bdd); 06348 } else if (psLevel == nsLevel + 1) { 06349 bdd = bdd_var_with_index(mddManager, nsId); 06350 bdd_new_var_block(bdd, 2); 06351 bdd_free(bdd); 06352 } 06353 } 06354 } else if (bdd_is_pi_var(mddManager, i)) { 06355 bdd_set_var_to_be_ungrouped(mddManager, i); 06356 } 06357 } 06358 if (verbosity) { 06359 fprintf(vis_stdout, "#grp=%d(#depend1to1=%d,#pairpsonce=%d)", 06360 nGroup, nDepend1to1, nPairPsOnce); 06361 fprintf(vis_stdout, 06362 " #ungrp=%d(#const=%d,#lambda=%d, independ1to1=%d)\n", 06363 nUngroup, nConst, nLambda, nIndepend1to1); 06364 } 06365 FREE(nonLambda); 06366 } 06367 06377 int 06378 Img_IsTransitionRelationOptimized(Img_ImageInfo_t * imageInfo) 06379 { 06380 Iwls95Info_t *info = (Iwls95Info_t *)imageInfo->methodData; 06381 if(info->fwdOptClusteredRelationArray && 06382 info->fwdClusteredRelationArray) return(1); 06383 return(0); 06384 } 06385 06395 static int 06396 MddSizeCompare(const void *ptr1, const void *ptr2) 06397 { 06398 mdd_t *mdd1 = *(mdd_t **)ptr1; 06399 mdd_t *mdd2 = *(mdd_t **)ptr2; 06400 int size1 = mdd_size(mdd1); 06401 int size2 = mdd_size(mdd2); 06402 06403 if (size1 > size2) 06404 return 1; 06405 else if (size1 < size2) 06406 return -1; 06407 else 06408 return 0; 06409 } 06410 06421 void 06422 Img_ForwardImageInfoRecoverFromWinningStrategy( 06423 Img_ImageInfo_t * imageInfo 06424 ) 06425 { 06426 Iwls95Info_t *info; 06427 array_t *new_; 06428 06429 info = (Iwls95Info_t *)imageInfo->methodData; 06430 06431 if(info->fwdOriClusteredRelationArray) { 06432 new_ = info->fwdClusteredRelationArray; 06433 info->fwdClusteredRelationArray = info->fwdOriClusteredRelationArray; 06434 info->fwdOriClusteredRelationArray = 0; 06435 mdd_array_free(new_); 06436 } 06437 } 06438 06449 void 06450 Img_ForwardImageInfoConjoinWithWinningStrategy( 06451 Img_ImageInfo_t * imageInfo, 06452 mdd_t *winningStrategy) 06453 { 06454 Iwls95Info_t *info; 06455 array_t *old, *new_; 06456 int i; 06457 mdd_t *tr, *ntr, *winning; 06458 06459 06460 old = 0; 06461 winning = 0; 06462 new_ = array_alloc(mdd_t *, 0); 06463 info = (Iwls95Info_t *)imageInfo->methodData; 06464 old = info->fwdClusteredRelationArray; 06465 info->fwdClusteredRelationArray = new_; 06466 info->fwdOriClusteredRelationArray = old; 06467 winning = mdd_dup(winningStrategy); 06468 /* winning = ImgSubstitute(winningStrategy, &(imageInfo->functionData), Img_D2R_c);*/ 06469 for(i=0; i<array_n(old); i++) { 06470 tr = array_fetch(mdd_t *, old, i); 06471 ntr = mdd_and(tr, winning, 1, 1); 06472 array_insert_last(mdd_t *, new_, ntr); 06473 } 06474 mdd_free(winning); 06475 } 06476
1.7.3