/**CFile*********************************************************************** FileName [imgTfm.c] PackageName [img] Synopsis [Routines for image and preimage computations using transition function method.] Description [Transition function method is implemented as a part of the hybrid image computation (refer to "To Split or to Conjoin: The Question in Image Computation", In-Ho Moon et. al. in the proceedings of DAC00.) The hybrid method starts with transition function method based on splitting, then switches to transition relation method based on conjunctions. The decision is based on computing variable lifetimes from dependence matrix dynamically at every recursion. The transition function method itself also can be used as an image_method, however we do not recommend to use this method for general purpose. This method can be used for experimental purpose. However, this method performs quite well for most approximate reachability and some examples on exact reachability. There are two image computation methods in transition function method; input splitting (default) and output splitting. Also three preimage computation methods in transition function method are implemented; domain cofactoring (default), sequential substitution, and simultaneous substitution. The performance of transition function method is significantly depending on both the choice of splitting variable and the use of image cache. However, the hybrid method does not use image cache by default. Since the recursion depths are bounded (not so deep) in the hybrid method, the cache hit ratio is usually very low. The implementation of the transition function method and the hybrid method is very complicate since there are so many options. For details, try print_tfm_options and print_hybrid_options commands in vis, also more detailed descriptions for all options can be read by using help in vis for the two commands. The hybrid method can start with either only function vector or only transition relation, as well as with both function vector and transition relation. In case of starting with only the function vector, when we switch to conjoin, transition relation is built on demand. This method may consume less memory than the others, but it may take more time since it is a big overhead to build transition relation at every conjunction. To reduce this overhead, the hybrid method can start with both function vector and transition relation (default). In the presense of non-determinism, the hybrid mehtod also can start with only transition relation without the function vector.] SeeAlso [imgTfmFwd.c imgTfmBwd.c imgTfmUtil.c imgTfmCache.c] Author [In-Ho Moon] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software. IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] ******************************************************************************/ #include "imgInt.h" static char rcsid[] UNUSED = "$Id: imgTfm.c,v 1.93 2005/04/23 14:30:54 jinh Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ static st_table *HookInfoList; /* adds a hook function to flush image cache before veriable reordering */ static int nHookInfoList; /* the number of hook functions */ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static ImgTfmInfo_t * TfmInfoStructAlloc(Img_MethodType method); static int CompareIndex(const void *e1, const void *e2); static int HookInfoFunction(bdd_manager *mgr, char *str, void *method); static array_t * ChoosePartialVars(ImgTfmInfo_t *info, array_t *vector, int nPartialVars, int partialMethod); static void PrintRecursionStatistics(ImgTfmInfo_t *info, int preFlag); static void PrintFoundVariableStatistics(ImgTfmInfo_t *info, int preFlag); static void GetRecursionStatistics(ImgTfmInfo_t *info, int preFlag, int *nRecurs, int *nLeaves, int *nTurns, float *averageDepth, int *maxDepth, int *nDecomps, int *topDecomp, int *maxDecomp, float *averageDecomp); static int ReadSetIntValue(char *string, int l, int u, int defaultValue); static boolean ReadSetBooleanValue(char *string, boolean defaultValue); static void FindIntermediateVarsRecursively(ImgTfmInfo_t *info, mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *vector, st_table *domainQuantifyVarMddIdTable, array_t *intermediateVarMddIdArray); static void GetIntermediateRelationsRecursively(mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *relationArray, st_table *domainQuantifyVarMddIdTable, array_t *intermediateVarMddIdArray); static int CheckNondeterminism(Ntk_Network_t *network); static array_t * TfmCreateBitVector(ImgTfmInfo_t *info, int composeIntermediateVars, int findIntermediateVars); static array_t * TfmCreateBitRelationArray(ImgTfmInfo_t *info, int composeIntermediateVars, int findIntermediateVars); static void TfmSetupPartialTransitionRelation(ImgTfmInfo_t *info, array_t **partialRelationArray); static void TfmBuildRelationArray(ImgTfmInfo_t *info, ImgFunctionData_t *functionData, array_t *bitRelationArray, Img_DirectionType directionType, int writeMatrix); static void RebuildTransitionRelation(ImgTfmInfo_t *info, Img_DirectionType directionType); static void MinimizeTransitionFunction(array_t *vector, array_t *relationArray, mdd_t *constrain, Img_MinimizeType minimizeMethod, int printStatus); static void AddDontCareToTransitionFunction(array_t *vector, array_t *relationArray, mdd_t *constrain, Img_MinimizeType minimizeMethod, int printStatus); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Gets the statistics of recursions of transition function method.] Description [Gets the statistics of recursions of transition function method.] SideEffects [] SeeAlso [] ******************************************************************************/ int Img_TfmGetRecursionStatistics(Img_ImageInfo_t *imageInfo, int preFlag, int *nRecurs, int *nLeaves, int *nTurns, float *averageDepth, int *maxDepth, int *nDecomps, int *topDecomp, int *maxDecomp, float *averageDecomp) { ImgTfmInfo_t *info; if (imageInfo->methodType != Img_Tfm_c && imageInfo->methodType != Img_Hybrid_c) { return(0); } info = (ImgTfmInfo_t *)imageInfo->methodData; if (preFlag) { *nRecurs = info->nRecursionB; *nLeaves = info->nLeavesB; *nTurns = info->nTurnsB; *averageDepth = info->averageDepthB; *maxDepth = info->maxDepthB; *nDecomps = 0; *topDecomp = 0; *maxDecomp = 0; *averageDecomp = 0.0; } else { *nRecurs = info->nRecursion; *nLeaves = info->nLeaves; *nTurns = info->nTurns; *averageDepth = info->averageDepth; *maxDepth = info->maxDepth; *nDecomps = info->nDecomps; *topDecomp = info->topDecomp; *maxDecomp = info->maxDecomp; *averageDecomp = info->averageDecomp; } return(1); } /**Function******************************************************************** Synopsis [Prints the statistics of image cache and recursions in in transition function method.] Description [Prints the statistics of image cache and recursions in in transition function method.] SideEffects [] SeeAlso [] ******************************************************************************/ void Img_TfmPrintStatistics(Img_ImageInfo_t *imageInfo, Img_DirectionType dir) { if (dir == Img_Forward_c || dir == Img_Both_c) { Img_TfmPrintCacheStatistics(imageInfo, 0); Img_TfmPrintRecursionStatistics(imageInfo, 0); } if (dir == Img_Backward_c || dir == Img_Both_c) { Img_TfmPrintCacheStatistics(imageInfo, 1); Img_TfmPrintRecursionStatistics(imageInfo, 1); } } /**Function******************************************************************** Synopsis [Prints the statistics of recursions for transition function method.] Description [Prints the statistics of recursions for transition function method.] SideEffects [] SeeAlso [] ******************************************************************************/ void Img_TfmPrintRecursionStatistics(Img_ImageInfo_t *imageInfo, int preFlag) { float avgDepth, avgDecomp; int nRecurs, nLeaves, nTurns, nDecomps, topDecomp, maxDecomp; int maxDepth; (void) Img_TfmGetRecursionStatistics(imageInfo, preFlag, &nRecurs, &nLeaves, &nTurns, &avgDepth, &maxDepth, &nDecomps, &topDecomp, &maxDecomp, &avgDecomp); if (preFlag) fprintf(vis_stdout, "** recursion statistics of splitting (preImg) **\n"); else fprintf(vis_stdout, "** recursion statistics of splitting (img) **\n"); fprintf(vis_stdout, "# recursions = %d\n", nRecurs); fprintf(vis_stdout, "# leaves = %d\n", nLeaves); fprintf(vis_stdout, "# turns = %d\n", nTurns); fprintf(vis_stdout, "# average recursion depth = %g (max = %d)\n", avgDepth, maxDepth); if (!preFlag) { fprintf(vis_stdout, "# decompositions = %d (top = %d, max = %d, average = %g)\n", nDecomps, topDecomp, maxDecomp, avgDecomp); } } /**Function******************************************************************** Synopsis [Prints the options for image computation using transition function method.] Description [Prints the options for image computation using transition function method.] SideEffects [] SeeAlso [] ******************************************************************************/ void Img_PrintTfmOptions(void) { ImgTfmOption_t *options; Img_MethodType method; char *flagValue, dummy[40]; flagValue = Cmd_FlagReadByName("image_method"); if (flagValue) { if (strcmp(flagValue, "hybrid") == 0) method = Img_Hybrid_c; else method = Img_Tfm_c; } else method = Img_Tfm_c; options = ImgTfmGetOptions(method); switch (options->splitMethod) { case 0 : sprintf(dummy, "input split"); break; case 1 : sprintf(dummy, "output split"); break; case 2 : sprintf(dummy, "mixed"); break; case 3 : sprintf(dummy, "hybrid"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_split_method = %d (%s)\n", options->splitMethod, dummy); switch (options->inputSplit) { case 0 : sprintf(dummy, "support before splitting"); break; case 1 : sprintf(dummy, "support after splitting"); break; case 2 : sprintf(dummy, "estimate BDD size after splitting"); break; case 3 : sprintf(dummy, "top variable"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_input_split = %d (%s)\n", options->inputSplit, dummy); if (options->piSplitFlag) sprintf(dummy, "yes"); else sprintf(dummy, "no"); fprintf(vis_stdout, "TFM: tfm_pi_split_flag = %s\n", dummy); /* whether to convert image computation to range computation */ switch (options->rangeComp) { case 0 : sprintf(dummy, "do not convert"); break; case 1 : sprintf(dummy, "convert to range computation"); break; case 2 : sprintf(dummy, "convert with threshold"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_range_comp = %d (%s)\n", options->rangeComp, dummy); fprintf(vis_stdout, "TFM: tfm_range_threshold = %d\n", options->rangeThreshold); fprintf(vis_stdout, "TFM: tfm_range_try_threshold = %d\n", options->rangeTryThreshold); if (options->rangeCheckReorder) sprintf(dummy, "yes"); else sprintf(dummy, "no"); fprintf(vis_stdout, "TFM: tfm_range_check_reorder = %s\n", dummy); switch (options->tieBreakMode) { case 0 : sprintf(dummy, "closest variable to top"); break; case 1 : sprintf(dummy, "smallest BDD size after splitting"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_tie_break_mode = %d (%s)\n", options->tieBreakMode, dummy); switch (options->outputSplit) { case 0 : sprintf(dummy, "smallest BDD size"); break; case 1 : sprintf(dummy, "largest BDD size"); break; case 2 : sprintf(dummy, "top variable"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_output_split = %d (%s)\n", options->outputSplit, dummy); fprintf(vis_stdout, "TFM: tfm_turn_depth = %d\n", options->turnDepth); if (options->findDecompVar) sprintf(dummy, "yes"); else sprintf(dummy, "no"); fprintf(vis_stdout, "TFM: tfm_find_decomp_var = %s\n", dummy); if (options->sortVectorFlag) sprintf(dummy, "yes"); else sprintf(dummy, "no"); fprintf(vis_stdout, "TFM: tfm_sort_vector_flag = %s\n", dummy); if (options->printStatistics) sprintf(dummy, "yes"); else sprintf(dummy, "no"); fprintf(vis_stdout, "TFM: tfm_print_stats = %s\n", dummy); if (options->printBddSize) sprintf(dummy, "yes"); else sprintf(dummy, "no"); fprintf(vis_stdout, "TFM: tfm_print_bdd_size = %s\n", dummy); if (options->splitCubeFunc) sprintf(dummy, "yes"); else sprintf(dummy, "no"); fprintf(vis_stdout, "TFM: tfm_split_cube_func = %s\n", dummy); switch (options->findEssential) { case 0 : sprintf(dummy, "off"); break; case 1 : sprintf(dummy, "on"); break; case 2 : sprintf(dummy, "dynamic"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_find_essential = %d (%s)\n", options->findEssential, dummy); switch (options->printEssential) { case 0 : sprintf(dummy, "off"); break; case 1 : sprintf(dummy, "at the end"); break; case 2 : sprintf(dummy, "at every image computation"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_print_essential = %d (%s)\n", options->printEssential, dummy); switch (options->useCache) { case 0 : sprintf(dummy, "off"); break; case 1 : sprintf(dummy, "on"); break; case 2 : sprintf(dummy, "store all intermediate"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_use_cache = %d (%s)\n", options->useCache, dummy); if (options->globalCache) sprintf(dummy, "yes"); else sprintf(dummy, "no"); fprintf(vis_stdout, "TFM: tfm_global_cache = %s\n", dummy); fprintf(vis_stdout, "TFM: tfm_max_chain_length = %d\n", options->maxChainLength); fprintf(vis_stdout, "TFM: tfm_init_cache_size = %d\n", options->initCacheSize); switch (options->autoFlushCache) { case 0 : sprintf(dummy, "when requested"); break; case 1 : sprintf(dummy, "at the end of image computation"); break; case 2 : sprintf(dummy, "before reordering"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_auto_flush_cache = %d (%s)\n", options->autoFlushCache, dummy); if (options->composeIntermediateVars) sprintf(dummy, "yes"); else sprintf(dummy, "no"); fprintf(vis_stdout, "TFM: tfm_compose_intermediate_vars = %s\n", dummy); switch (options->preSplitMethod) { case 0 : sprintf(dummy, "input split"); break; case 1 : sprintf(dummy, "output split"); break; case 2 : sprintf(dummy, "mixed"); break; case 3 : sprintf(dummy, "substitution"); break; case 4 : sprintf(dummy, "hybrid"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_pre_split_method = %d (%s)\n", options->preSplitMethod, dummy); switch (options->preInputSplit) { case 0 : sprintf(dummy, "support before splitting"); break; case 1 : sprintf(dummy, "support after splitting"); break; case 2 : sprintf(dummy, "estimate BDD size after splitting"); break; case 3 : sprintf(dummy, "top variable"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_pre_input_split = %d (%s)\n", options->preInputSplit, dummy); switch (options->preOutputSplit) { case 0 : sprintf(dummy, "smallest BDD size"); break; case 1 : sprintf(dummy, "largest BDD size"); break; case 2 : sprintf(dummy, "top variable"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_pre_output_split = %d (%s)\n", options->preOutputSplit, dummy); switch (options->preDcLeafMethod) { case 0 : sprintf(dummy, "substitution"); break; case 1 : sprintf(dummy, "constraint cofactoring"); break; case 2 : sprintf(dummy, "hybrid"); break; default : sprintf(dummy, "invalid"); break; } fprintf(vis_stdout, "TFM: tfm_pre_dc_leaf_method = %d (%s)\n", options->preDcLeafMethod, dummy); if (options->preMinimize) sprintf(dummy, "yes"); else sprintf(dummy, "no"); fprintf(vis_stdout, "TFM: tfm_pre_minimize = %s\n", dummy); fprintf(vis_stdout, "TFM: tfm_verbosity = %d\n", options->verbosity); FREE(options); } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Initializes an image data structure for image computation using transition function method.] Description [Initialized an image data structure for image computation using transition function method.] SideEffects [] ******************************************************************************/ void * ImgImageInfoInitializeTfm(void *methodData, ImgFunctionData_t * functionData, Img_DirectionType directionType, Img_MethodType method) { int i; int latches; int variables, nVars; array_t *vector; graph_t *mddNetwork; mdd_manager *mddManager; array_t *rangeVarMddIdArray; ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; int index; mdd_t *var; char *flagValue; char filename[20]; int composeIntermediateVars, findIntermediateVars; int nonDeterministic; if (info) { if (info->option->useCache) { if (directionType == Img_Forward_c || directionType == Img_Both_c) { if (!info->imgCache) ImgCacheInitTable(info, info->option->initCacheSize, info->option->globalCache, FALSE); } if (directionType == Img_Backward_c || directionType == Img_Both_c) { if (!info->preCache) ImgCacheInitTable(info, info->option->initCacheSize, info->option->globalCache, TRUE); } } if (info->buildTR && (((directionType == Img_Forward_c || directionType == Img_Both_c) && !info->fwdClusteredRelationArray) || ((directionType == Img_Backward_c || directionType == Img_Both_c) && !info->bwdClusteredRelationArray))) { TfmBuildRelationArray(info, functionData, NIL(array_t), directionType, 0); } return((void *)info); } mddNetwork = functionData->mddNetwork; mddManager = Part_PartitionReadMddManager(mddNetwork); rangeVarMddIdArray = functionData->rangeVars; nonDeterministic = CheckNondeterminism(functionData->network); if (nonDeterministic) info = TfmInfoStructAlloc(Img_Hybrid_c); else info = TfmInfoStructAlloc(method); info->nonDeterministic = nonDeterministic; info->functionData = functionData; info->quantifyVarsTable = st_init_table(st_numcmp, st_numhash); for (i = 0; i < array_n(functionData->quantifyBddVars); i++) { var = array_fetch(mdd_t *, functionData->quantifyBddVars, i); index = (int)bdd_top_var_id(var); st_insert(info->quantifyVarsTable, (char *)(long)index, NIL(char)); } info->rangeVarsTable = st_init_table(st_numcmp, st_numhash); for (i = 0; i < array_n(functionData->rangeBddVars); i++) { var = array_fetch(mdd_t *, functionData->rangeBddVars, i); index = (int)bdd_top_var_id(var); st_insert(info->rangeVarsTable, (char *)(long)index, NIL(char)); } latches = 2 * mdd_get_number_of_bdd_vars(mddManager, rangeVarMddIdArray); nVars = latches + mdd_get_number_of_bdd_vars(mddManager, functionData->quantifyVars); variables = bdd_num_vars(mddManager); /* real number of variables */ info->nRealVars = nVars; info->nVars = variables; if (info->nonDeterministic) { if (method == Img_Tfm_c) { fprintf(vis_stdout, "** tfm warning: The circuit may have nondeterminism.\n"); fprintf(vis_stdout, "\tautomatically switched to hybrid mode = 2.\n"); info->method = Img_Hybrid_c; } else { if (info->option->hybridMode == 2) { if (info->option->buildPartialTR) { fprintf(vis_stdout, "** hyb warning: The circuit may have nondeterminism.\n"); fprintf(vis_stdout, "\tdid not use partial transition relation.\n"); } else { fprintf(vis_stdout, "** hyb info: The circuit may have nondeterminism.\n"); } } else { fprintf(vis_stdout, "** hyb warning: The circuit may have nondeterminism.\n"); fprintf(vis_stdout, "\tautomatically switched to hybrid mode = 2.\n"); } } } if (info->nonDeterministic || (info->option->hybridMode > 0 && (info->option->splitMethod == 3 || info->option->preSplitMethod == 4))) { if (info->option->hybridMode == 2 || info->nonDeterministic) info->buildTR = 2; else info->buildTR = 1; } if (info->buildTR == 2 && info->option->buildPartialTR && info->nonDeterministic == 0 && info->option->useCache == 0) { info->buildPartialTR = TRUE; } info->imgKeepPiInTr = info->option->imgKeepPiInTr; if (info->option->useCache) info->preKeepPiInTr = TRUE; else info->preKeepPiInTr = info->option->preKeepPiInTr; if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c && nVars != variables) { if (info->option->composeIntermediateVars) { composeIntermediateVars = 1; findIntermediateVars = 0; } else { composeIntermediateVars = 0; findIntermediateVars = 1; } } else { composeIntermediateVars = 0; findIntermediateVars = 0; } if (info->buildTR != 2 || info->buildPartialTR) { /* deterministic */ vector = TfmCreateBitVector(info, composeIntermediateVars, findIntermediateVars); } else vector = NIL(array_t); info->manager = mddManager; if (info->buildPartialTR) info->fullVector = vector; else info->vector = vector; if (info->buildTR == 2) info->useConstraint = 1; else if (info->option->splitMethod == 1) info->useConstraint = 0; else { if (info->option->rangeComp == 2) info->useConstraint = 2; else if (info->option->rangeComp == 0) info->useConstraint = 1; else info->useConstraint = 0; } if (info->option->useCache) { if (directionType == Img_Forward_c || directionType == Img_Both_c) { ImgCacheInitTable(info, info->option->initCacheSize, info->option->globalCache, FALSE); } if (directionType == Img_Backward_c || directionType == Img_Both_c) { ImgCacheInitTable(info, info->option->initCacheSize, info->option->globalCache, TRUE); } if (info->option->autoFlushCache == 2) { if (nHookInfoList == 0) { HookInfoList = st_init_table(st_ptrcmp, st_ptrhash); bdd_add_hook(info->manager, HookInfoFunction, BDD_PRE_REORDERING_HOOK); st_insert(HookInfoList, (char *)info, NIL(char)); } else { if (info->option->globalCache == 0) st_insert(HookInfoList, (char *)info, NIL(char)); } nHookInfoList++; } } info->trmOption = ImgGetTrmOptions(); info->domainVarBddArray = functionData->domainBddVars; info->quantifyVarBddArray = functionData->quantifyBddVars; info->rangeVarBddArray = functionData->rangeBddVars; if (info->vector && info->option->sortVectorFlag && info->option->useCache) array_sort(info->vector, CompareIndex); if (info->buildPartialTR) TfmSetupPartialTransitionRelation(info, NIL(array_t *)); if (info->buildTR) TfmBuildRelationArray(info, functionData, NIL(array_t), directionType, 1); if (info->buildTR == 1) { ImgPrintVectorDependency(info, info->vector, info->option->verbosity); if (info->option->writeSupportMatrix == 1) { sprintf(filename, "support%d.mat", info->option->supportFileCount++); ImgWriteSupportMatrix(info, info->vector, NIL(array_t), filename); } } if (info->option->writeSupportMatrixAndStop) exit(0); flagValue = Cmd_FlagReadByName("image_eliminate_depend_vars"); if (flagValue == NIL(char)) info->eliminateDepend = 0; /* the default value */ else info->eliminateDepend = atoi(flagValue); if (info->eliminateDepend && bdd_get_package_name() != CUDD) { fprintf(vis_stderr, "** tfm error : image_eliminate_depend_vars is available for only CUDD.\n"); info->eliminateDepend = 0; } info->nPrevEliminatedFwd = -1; flagValue = Cmd_FlagReadByName("image_verbosity"); if (flagValue) info->imageVerbosity = atoi(flagValue); if (info->option->printEssential) { info->foundEssentials = ALLOC(int, IMG_TF_MAX_PRINT_DEPTH); memset(info->foundEssentials, 0, sizeof(int) * IMG_TF_MAX_PRINT_DEPTH); } if (info->option->debug) info->debugCareSet = bdd_one(mddManager); else info->debugCareSet = NIL(mdd_t); return((void *)info); } /**Function******************************************************************** Synopsis [Computes the forward image of a set of states.] Description [Computes the forward image of a set of states.] SideEffects [] SeeAlso [ImgImageInfoComputeFwdWithDomainVarsTfm] ******************************************************************************/ mdd_t * ImgImageInfoComputeFwdTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) { ImgTfmInfo_t *info = (ImgTfmInfo_t *)imageInfo->methodData; mdd_t *image, *domainSubset; if (info->vector == NIL(array_t) && !(info->buildTR == 2 && info->fwdClusteredRelationArray)) { fprintf(vis_stderr, "** img error: The data structure has not been "); fprintf(vis_stderr, "initialized for image computation\n"); return(NIL(mdd_t)); } info->updatedFlag = FALSE; domainSubset = bdd_between(fromLowerBound, fromUpperBound); image = ImgTfmImage(info, domainSubset); mdd_free(domainSubset); return(image); } /**Function******************************************************************** Synopsis [Computes the forward image of a set of states in terms of domain variables.] Description [Identical to ImgImageInfoComputeFwdTfm.] SideEffects [] SeeAlso [ImgImageInfoComputeFwdTfm] ******************************************************************************/ mdd_t * ImgImageInfoComputeFwdWithDomainVarsTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) { mdd_t *image; image = ImgImageInfoComputeFwdTfm(functionData, imageInfo , fromLowerBound, fromUpperBound, toCareSetArray); return(image); } /**Function******************************************************************** Synopsis [Computes the backward image of domainSubset.] Description [Computes the backward image of domainSubset.] SideEffects [] SeeAlso [ImgImageInfoComputeBwdWithDomainVarsTfm] ******************************************************************************/ mdd_t * ImgImageInfoComputeBwdTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) { ImgTfmInfo_t *info = (ImgTfmInfo_t *)imageInfo->methodData; mdd_t *image, *domainSubset, *simplifiedImage; array_t *replace; if (info->vector == NIL(array_t) && !(info->buildTR == 2 && info->bwdClusteredRelationArray)) { fprintf(vis_stderr, "** img error: The data structure has not been "); fprintf(vis_stderr, "initialized for backward image computation\n"); return(NIL(mdd_t)); } info->updatedFlag = FALSE; domainSubset = bdd_between(fromLowerBound, fromUpperBound); if (info->toCareSetArray) replace = info->toCareSetArray; else { replace = NIL(array_t); info->toCareSetArray = toCareSetArray; } image = ImgTfmPreImage(info, domainSubset); info->toCareSetArray = replace; mdd_free(domainSubset); simplifiedImage = bdd_minimize_array(image, toCareSetArray); bdd_free(image); return(simplifiedImage); } /**Function******************************************************************** Synopsis [Computes the backward image of a set of states.] Description [Identical to ImgImageInfoComputeBwdTfm.] SideEffects [] SeeAlso [ImgImageInfoComputeBwdTfm] ******************************************************************************/ mdd_t * ImgImageInfoComputeBwdWithDomainVarsTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) { mdd_t *image; image = ImgImageInfoComputeBwdTfm(functionData, imageInfo, fromLowerBound, fromUpperBound, toCareSetArray); return(image); } /**Function******************************************************************** Synopsis [Frees the memory associated with imageInfo.] Description [Frees the memory associated with imageInfo.] SideEffects [] ******************************************************************************/ void ImgImageInfoFreeTfm(void *methodData) { ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; if (info == NIL(ImgTfmInfo_t)) { fprintf(vis_stderr, "** img error: Trying to free the NULL image info\n"); return; } if (info->option->printStatistics) { if (info->nRecursion) { if (info->imgCache) ImgPrintCacheStatistics(info->imgCache); PrintRecursionStatistics(info, 0); PrintFoundVariableStatistics(info, 0); } if (info->nRecursionB) { if (info->preCache) ImgPrintCacheStatistics(info->preCache); PrintRecursionStatistics(info, 1); PrintFoundVariableStatistics(info, 1); } } if (info->vector != NIL(array_t)) ImgVectorFree(info->vector); if (info->toCareSetArray != NIL(array_t)) mdd_array_free(info->toCareSetArray); if (info->imgCache) ImgCacheDestroyTable(info->imgCache, info->option->globalCache); if (info->preCache) ImgCacheDestroyTable(info->preCache, info->option->globalCache); st_free_table(info->quantifyVarsTable); st_free_table(info->rangeVarsTable); if (info->intermediateVarsTable) { st_free_table(info->intermediateVarsTable); info->intermediateVarsTable = NIL(st_table); } if (info->intermediateBddVars) { mdd_array_free(info->intermediateBddVars); info->intermediateBddVars= NIL(array_t); } if (info->newQuantifyBddVars) { mdd_array_free(info->newQuantifyBddVars); info->newQuantifyBddVars = NIL(array_t); } if (info->option->useCache) { if (info->option->autoFlushCache == 2) { nHookInfoList--; st_delete(HookInfoList, &info, NULL); if (nHookInfoList == 0) { st_free_table(HookInfoList); bdd_remove_hook(info->manager, HookInfoFunction, BDD_PRE_REORDERING_HOOK); } } } if (info->option != NULL) FREE(info->option); if (info->fwdClusteredRelationArray) mdd_array_free(info->fwdClusteredRelationArray); if (info->bwdClusteredRelationArray) mdd_array_free(info->bwdClusteredRelationArray); if (info->fwdArraySmoothVarBddArray) mdd_array_array_free(info->fwdArraySmoothVarBddArray); if (info->bwdArraySmoothVarBddArray) mdd_array_array_free(info->bwdArraySmoothVarBddArray); if (info->fwdSmoothVarCubeArray) mdd_array_free(info->fwdSmoothVarCubeArray); if (info->bwdSmoothVarCubeArray) mdd_array_free(info->bwdSmoothVarCubeArray); if (info->trmOption) ImgFreeTrmOptions(info->trmOption); if (info->partialBddVars) mdd_array_free(info->partialBddVars); if (info->partialVarFlag) FREE(info->partialVarFlag); if (info->fullVector != NIL(array_t)) ImgVectorFree(info->fullVector); if (info->foundEssentials) FREE(info->foundEssentials); if (info->debugCareSet) mdd_free(info->debugCareSet); if (info->savedArraySmoothVarBddArray != NIL(array_t)) mdd_array_array_free(info->savedArraySmoothVarBddArray); if (info->savedSmoothVarCubeArray != NIL(array_t)) mdd_array_free(info->savedSmoothVarCubeArray); FREE(info); } /**Function******************************************************************** Synopsis [Prints information about the transition function method.] Description [This function is used to obtain the information about the parameters used to initialize the imageInfo.] SideEffects [] ******************************************************************************/ void ImgImageInfoPrintMethodParamsTfm(void *methodData, FILE *fp) { ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; if (fp == NULL) return; if (info->vector) ImgPrintVectorDependency(info, info->vector, 1); if (info->method == Img_Tfm_c) { fprintf(vis_stdout, "For the options in tfm method, try print_tfm_options.\n"); return; } if (info->fwdClusteredRelationArray != NIL(array_t)) { fprintf(fp, "Shared size of transition relation for forward image"); fprintf(fp, " computation is %10ld BDD nodes (%-4d components)\n", bdd_size_multiple(info->fwdClusteredRelationArray), array_n(info->fwdClusteredRelationArray)); } if (info->bwdClusteredRelationArray != NIL(array_t)) { fprintf(fp, "Shared size of transition relation for backward image"); fprintf(fp, " computation is %10ld BDD nodes (%-4d components)\n", bdd_size_multiple(info->bwdClusteredRelationArray), array_n(info->bwdClusteredRelationArray)); } fprintf(vis_stdout, "For the options in hybrid method,"); fprintf(vis_stdout, " try print_hybrid_options and print_tfm_options.\n"); } /**Function******************************************************************** Synopsis [Restores original transition function from saved.] Description [Restores original transition function from saved.] SideEffects [] ******************************************************************************/ void ImgRestoreTransitionFunction(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) { ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)imageInfo->methodData; if (tfmInfo->vector) { ImgVectorFree(tfmInfo->vector); tfmInfo->vector = (array_t *)imageInfo->savedRelation; imageInfo->savedRelation = NIL(void); } if (tfmInfo->fwdClusteredRelationArray) { if (directionType == Img_Forward_c || directionType == Img_Both_c) { mdd_array_free(tfmInfo->fwdClusteredRelationArray); tfmInfo->fwdClusteredRelationArray = tfmInfo->fwdSavedRelation; tfmInfo->fwdSavedRelation = NIL(array_t); } } if (tfmInfo->bwdClusteredRelationArray) { if (directionType == Img_Backward_c || directionType == Img_Both_c) { mdd_array_free(tfmInfo->bwdClusteredRelationArray); tfmInfo->bwdClusteredRelationArray = tfmInfo->bwdSavedRelation; tfmInfo->bwdSavedRelation = NIL(array_t); } } } /**Function******************************************************************** Synopsis [Duplicates transition function.] Description [Duplicates transition function.] SideEffects [] ******************************************************************************/ void ImgDuplicateTransitionFunction(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) { array_t *copiedVector; array_t *copiedRelation; ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)imageInfo->methodData; if (tfmInfo->vector) { copiedVector = ImgVectorCopy(tfmInfo, tfmInfo->vector); assert(!imageInfo->savedRelation); imageInfo->savedRelation = (void *)tfmInfo->vector; tfmInfo->vector = copiedVector; } if (tfmInfo->fwdClusteredRelationArray) { if (directionType == Img_Forward_c || directionType == Img_Both_c) { copiedRelation = mdd_array_duplicate(tfmInfo->fwdClusteredRelationArray); tfmInfo->fwdSavedRelation = tfmInfo->fwdClusteredRelationArray; tfmInfo->fwdClusteredRelationArray = copiedRelation; } } if (tfmInfo->bwdClusteredRelationArray) { if (directionType == Img_Backward_c || directionType == Img_Both_c) { copiedRelation = mdd_array_duplicate(tfmInfo->bwdClusteredRelationArray); tfmInfo->bwdSavedRelation = tfmInfo->bwdClusteredRelationArray; tfmInfo->bwdClusteredRelationArray = copiedRelation; } } } /**Function******************************************************************** Synopsis [Minimizes transition function with given set of constraints.] Description [Minimizes transition function with given set of constraints.] SideEffects [] ******************************************************************************/ void ImgMinimizeTransitionFunction(void *methodData, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, int printStatus) { ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; int i, j; bdd_t *function, *simplifiedFunction; bdd_t *constrain; bdd_t *relation, *simplifiedRelation; int size = 0; long sizeConstrain; ImgComponent_t *comp; if (printStatus) sizeConstrain = bdd_size_multiple(constrainArray); else sizeConstrain = 0; if (info->vector) { if (printStatus) size = ImgVectorBddSize(info->vector); arrayForEachItem(ImgComponent_t *, info->vector, i, comp) { function = mdd_dup(comp->func); arrayForEachItem(bdd_t *, constrainArray, j, constrain) { if (bdd_is_tautology(constrain, 1)) continue; simplifiedFunction = Img_MinimizeImage(function, constrain, minimizeMethod, TRUE); if (printStatus == 2) { (void) fprintf(vis_stdout, "IMG Info: minimized function %d | %d => %d in component %d\n", bdd_size(function), bdd_size(constrain), bdd_size(simplifiedFunction), i); } mdd_free(function); function = simplifiedFunction; } if (mdd_equal(function, comp->func)) mdd_free(function); else { mdd_free(comp->func); comp->func = function; ImgSupportClear(info, comp->support); ImgComponentGetSupport(comp); } } if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized function [%d | %ld => %ld] with %d components\n", size, sizeConstrain, ImgVectorBddSize(info->vector), array_n(info->vector)); } } if (info->buildTR == 0) return; else if (info->buildTR == 1 && info->option->synchronizeTr) { if (info->fwdClusteredRelationArray && (directionType == Img_Forward_c || directionType == Img_Both_c)) { RebuildTransitionRelation(info, Img_Forward_c); } if (info->bwdClusteredRelationArray && (directionType == Img_Backward_c || directionType == Img_Both_c)) { RebuildTransitionRelation(info, Img_Backward_c); } return; } if (info->fwdClusteredRelationArray && (directionType == Img_Forward_c || directionType == Img_Both_c)) { if (printStatus) size = bdd_size_multiple(info->fwdClusteredRelationArray); arrayForEachItem(bdd_t *, constrainArray, i, constrain) { if (bdd_is_tautology(constrain, 1)) continue; arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, j, relation) { simplifiedRelation = Img_MinimizeImage(relation, constrain, minimizeMethod, TRUE); if (printStatus == 2) { (void) fprintf(vis_stdout, "IMG Info: minimized fwd relation %d | %d => %d in component %d\n", bdd_size(relation), bdd_size(constrain), bdd_size(simplifiedRelation), j); } mdd_free(relation); array_insert(bdd_t*, info->fwdClusteredRelationArray, j, simplifiedRelation); } } if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized fwd relation [%d | %ld => %ld] with %d components\n", size, sizeConstrain, bdd_size_multiple(info->fwdClusteredRelationArray), array_n(info->fwdClusteredRelationArray)); } } if (info->bwdClusteredRelationArray && (directionType == Img_Backward_c || directionType == Img_Both_c)) { if (printStatus) size = bdd_size_multiple(info->bwdClusteredRelationArray); arrayForEachItem(bdd_t *, constrainArray, i, constrain) { if (bdd_is_tautology(constrain, 1)) continue; arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, j, relation) { simplifiedRelation = Img_MinimizeImage(relation, constrain, minimizeMethod, TRUE); if (printStatus == 2) { (void) fprintf(vis_stdout, "IMG Info: minimized bwd relation %d | %d => %d in component %d\n", bdd_size(relation), bdd_size(constrain), bdd_size(simplifiedRelation), j); } mdd_free(relation); array_insert(bdd_t*, info->bwdClusteredRelationArray, j, simplifiedRelation); } } if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized bwd relation [%d | %ld => %ld] with %d components\n", size, sizeConstrain, bdd_size_multiple(info->bwdClusteredRelationArray), array_n(info->bwdClusteredRelationArray)); } } } /**Function******************************************************************** Synopsis [Adds a dont care set to the transition function and relation.] Description [Adds a dont care set to the transition function and relation. This function is called during guided search.] SideEffects [] ******************************************************************************/ void ImgAddDontCareToTransitionFunction(void *methodData, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, int printStatus) { ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; int i, j; bdd_t *function, *simplifiedFunction; bdd_t *constrain; bdd_t *relation, *simplifiedRelation; int size = 0; long sizeConstrain; ImgComponent_t *comp; if (printStatus) sizeConstrain = bdd_size_multiple(constrainArray); else sizeConstrain = 0; if (info->vector) { if (printStatus) size = ImgVectorBddSize(info->vector); arrayForEachItem(ImgComponent_t *, info->vector, i, comp) { function = mdd_dup(comp->func); arrayForEachItem(bdd_t *, constrainArray, j, constrain) { if (bdd_is_tautology(constrain, 1)) continue; simplifiedFunction = Img_AddDontCareToImage(function, constrain, minimizeMethod); if (printStatus == 2) { (void) fprintf(vis_stdout, "IMG Info: minimized function %d | %d => %d in component %d\n", bdd_size(function), bdd_size(constrain), bdd_size(simplifiedFunction), i); } mdd_free(function); function = simplifiedFunction; } if (mdd_equal(function, comp->func)) mdd_free(function); else { mdd_free(comp->func); comp->func = function; ImgSupportClear(info, comp->support); ImgComponentGetSupport(comp); } } if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized function [%d | %ld => %ld] with %d components\n", size, sizeConstrain, ImgVectorBddSize(info->vector), array_n(info->vector)); } } if (info->buildTR == 0) return; else if (info->buildTR == 1 && info->option->synchronizeTr) { if (info->fwdClusteredRelationArray && (directionType == Img_Forward_c || directionType == Img_Both_c)) { RebuildTransitionRelation(info, Img_Forward_c); } if (info->bwdClusteredRelationArray && (directionType == Img_Backward_c || directionType == Img_Both_c)) { RebuildTransitionRelation(info, Img_Backward_c); } return; } if (info->fwdClusteredRelationArray && (directionType == Img_Forward_c || directionType == Img_Both_c)) { if (printStatus) size = bdd_size_multiple(info->fwdClusteredRelationArray); arrayForEachItem(bdd_t *, constrainArray, i, constrain) { if (bdd_is_tautology(constrain, 1)) continue; arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, j, relation) { simplifiedRelation = Img_AddDontCareToImage(relation, constrain, minimizeMethod); if (printStatus == 2) { (void) fprintf(vis_stdout, "IMG Info: minimized fwd relation %d | %d => %d in component %d\n", bdd_size(relation), bdd_size(constrain), bdd_size(simplifiedRelation), j); } mdd_free(relation); array_insert(bdd_t*, info->fwdClusteredRelationArray, j, simplifiedRelation); } } if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized fwd relation [%d | %ld => %ld] with %d components\n", size, sizeConstrain, bdd_size_multiple(info->fwdClusteredRelationArray), array_n(info->fwdClusteredRelationArray)); } } if (info->bwdClusteredRelationArray && (directionType == Img_Backward_c || directionType == Img_Both_c)) { if (printStatus) size = bdd_size_multiple(info->bwdClusteredRelationArray); arrayForEachItem(bdd_t *, constrainArray, i, constrain) { if (bdd_is_tautology(constrain, 1)) continue; arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, j, relation) { simplifiedRelation = Img_AddDontCareToImage(relation, constrain, minimizeMethod); if (printStatus == 2) { (void) fprintf(vis_stdout, "IMG Info: minimized bwd relation %d | %d => %d in component %d\n", bdd_size(relation), bdd_size(constrain), bdd_size(simplifiedRelation), j); } mdd_free(relation); array_insert(bdd_t*, info->bwdClusteredRelationArray, j, simplifiedRelation); } } if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized bwd relation [%d | %ld => %ld] with %d components\n", size, sizeConstrain, bdd_size_multiple(info->bwdClusteredRelationArray), array_n(info->bwdClusteredRelationArray)); } } } /**Function******************************************************************** Synopsis [Abstracts out given variables from transition function.] Description [Abstracts out given variables from transition function. abstractVars should be an array of bdd variables.] SideEffects [] ******************************************************************************/ void ImgAbstractTransitionFunction(Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, Img_DirectionType directionType, int printStatus) { ImgTfmInfo_t *info = (ImgTfmInfo_t *)imageInfo->methodData; int i, size = 0; bdd_t *abstractedFunction; ImgComponent_t *comp; array_t *vector; int flag = 0; int fwd_size = 0, bwd_size = 0; bdd_t *relation, *abstractedRelation; if (!abstractVars || array_n(abstractVars) == 0) return; if (info->vector) { if (printStatus) size = ImgVectorBddSize(info->vector); arrayForEachItem(ImgComponent_t *, info->vector, i, comp) { if (bdd_is_tautology(comp->func, 1)) continue; if (abstractCube) abstractedFunction = bdd_smooth_with_cube(comp->func, abstractCube); else abstractedFunction = bdd_smooth(comp->func, abstractVars); if (bdd_is_tautology(abstractedFunction, 1)) { comp->flag = 1; flag = 1; continue; } if (mdd_equal(abstractedFunction, comp->func)) mdd_free(abstractedFunction); else { if (printStatus == 2) { (void) fprintf(vis_stdout, "IMG Info: abstracted function %d => %d in component %d\n", bdd_size(comp->func), bdd_size(abstractedFunction), i); } mdd_free(comp->func); comp->func = abstractedFunction; ImgSupportClear(info, comp->support); ImgComponentGetSupport(comp); } } if (flag) { vector = info->vector; info->vector = array_alloc(ImgComponent_t *, 0); arrayForEachItem(ImgComponent_t *, vector, i, comp) { if (comp->flag) { ImgComponentFree(comp); continue; } array_insert_last(ImgComponent_t *, info->vector, comp); } array_free(vector); } if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: abstracted function [%d => %ld] with %d components\n", size, ImgVectorBddSize(info->vector), array_n(info->vector)); } } if (info->buildTR == 0) return; else if (info->buildTR == 1 && info->option->synchronizeTr) { if (info->fwdClusteredRelationArray && (directionType == Img_Forward_c || directionType == Img_Both_c)) { RebuildTransitionRelation(info, Img_Forward_c); } if (info->bwdClusteredRelationArray && (directionType == Img_Backward_c || directionType == Img_Both_c)) { RebuildTransitionRelation(info, Img_Backward_c); } return; } if (printStatus) { if (directionType == Img_Forward_c || directionType == Img_Both_c) fwd_size = bdd_size_multiple(info->fwdClusteredRelationArray); if (directionType == Img_Backward_c || directionType == Img_Both_c) bwd_size = bdd_size_multiple(info->bwdClusteredRelationArray); } if (info->fwdClusteredRelationArray && (directionType == Img_Forward_c || directionType == Img_Both_c)) { arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) { if (abstractCube) abstractedRelation = bdd_smooth_with_cube(relation, abstractCube); else abstractedRelation = bdd_smooth(relation, abstractVars); if (printStatus == 2) { (void) fprintf(vis_stdout, "IMG Info: abstracted fwd relation %d => %d in component %d\n", bdd_size(relation), bdd_size(abstractedRelation), i); } mdd_free(relation); array_insert(bdd_t*, info->fwdClusteredRelationArray, i, abstractedRelation); } } if (info->bwdClusteredRelationArray && (directionType == Img_Backward_c || directionType == Img_Both_c)) { arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) { if (abstractCube) abstractedRelation = bdd_smooth_with_cube(relation, abstractCube); else abstractedRelation = bdd_smooth(relation, abstractVars); if (printStatus == 2) { (void) fprintf(vis_stdout, "IMG Info: abstracted bwd relation %d => %d in component %d\n", bdd_size(relation), bdd_size(abstractedRelation), i); } mdd_free(relation); array_insert(bdd_t*, info->bwdClusteredRelationArray, i, abstractedRelation); } } if (printStatus) { if (directionType == Img_Forward_c || directionType == Img_Both_c) { (void) fprintf(vis_stdout, "IMG Info: abstracted fwd relation [%d => %ld] with %d components\n", fwd_size, bdd_size_multiple(info->fwdClusteredRelationArray), array_n(info->fwdClusteredRelationArray)); } if (directionType == Img_Backward_c || directionType == Img_Both_c) { (void) fprintf(vis_stdout, "IMG Info: abstracted bwd relation [%d => %ld] with %d components\n", bwd_size, bdd_size_multiple(info->bwdClusteredRelationArray), array_n(info->bwdClusteredRelationArray)); } } } /**Function******************************************************************** Synopsis [Approximate transition function.] Description [Approximate transition function.] SideEffects [] ******************************************************************************/ int ImgApproximateTransitionFunction(mdd_manager *mgr, void *methodData, bdd_approx_dir_t approxDir, bdd_approx_type_t approxMethod, int approxThreshold, double approxQuality, double approxQualityBias, Img_DirectionType directionType, mdd_t *bias) { ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; int i; bdd_t *approxFunction; int unchanged = 0; ImgComponent_t *comp; bdd_t *relation, *approxRelation; if (info->vector) { arrayForEachItem(ImgComponent_t *, info->vector, i, comp) { approxFunction = Img_ApproximateImage(mgr, comp->func, approxDir, approxMethod, approxThreshold, approxQuality, approxQualityBias, bias); if (bdd_is_tautology(approxFunction, 1)) { fprintf(vis_stdout, "** img warning : bdd_one from subsetting in [%d].\n", i); mdd_free(approxFunction); unchanged++; } else if (bdd_is_tautology(approxFunction, 0)) { fprintf(vis_stdout, "** img warning : bdd_zero from subsetting in [%d].\n", i); mdd_free(approxFunction); unchanged++; } else if (mdd_equal(approxFunction, comp->func)) { mdd_free(approxFunction); unchanged++; } else { mdd_free(comp->func); comp->func = approxFunction; ImgSupportClear(info, comp->support); ImgComponentGetSupport(comp); } } } if (info->buildTR == 0) return(unchanged); else if (info->buildTR == 1 && info->option->synchronizeTr) { if (info->fwdClusteredRelationArray && (directionType == Img_Forward_c || directionType == Img_Both_c)) { RebuildTransitionRelation(info, Img_Forward_c); } if (info->bwdClusteredRelationArray && (directionType == Img_Backward_c || directionType == Img_Both_c)) { RebuildTransitionRelation(info, Img_Backward_c); } return(unchanged); } if (info->fwdClusteredRelationArray && (directionType == Img_Forward_c || directionType == Img_Both_c)) { arrayForEachItem(bdd_t*, info->fwdClusteredRelationArray, i, relation) { approxRelation = Img_ApproximateImage(mgr, relation, approxDir, approxMethod, approxThreshold, approxQuality, approxQualityBias, bias); if (bdd_is_tautology(approxRelation, 1)) { fprintf(vis_stdout, "** img warning : bdd_one from subsetting in fwd[%d].\n", i); mdd_free(approxRelation); unchanged++; } else if (bdd_is_tautology(approxRelation, 0)) { fprintf(vis_stdout, "** img warning : bdd_zero from subsetting in fwd[%d].\n", i); mdd_free(approxRelation); unchanged++; } else if (mdd_equal(approxRelation, relation)) { mdd_free(approxRelation); unchanged++; } else { mdd_free(relation); array_insert(bdd_t*, info->fwdClusteredRelationArray, i, approxRelation); } } } if (info->bwdClusteredRelationArray && (directionType == Img_Backward_c || directionType == Img_Both_c)) { arrayForEachItem(bdd_t*, info->bwdClusteredRelationArray, i, relation) { approxRelation = Img_ApproximateImage(mgr, relation, approxDir, approxMethod, approxThreshold, approxQuality, approxQualityBias, bias); if (bdd_is_tautology(approxRelation, 1)) { fprintf(vis_stdout, "** img warning : bdd_one from subsetting in bwd[%d].\n", i); mdd_free(approxRelation); unchanged++; } else if (bdd_is_tautology(approxRelation, 0)) { fprintf(vis_stdout, "** img warning : bdd_zero from subsetting in bwd[%d].\n", i); mdd_free(approxRelation); unchanged++; } else if (mdd_equal(approxRelation, relation)) { mdd_free(approxRelation); unchanged++; } else { mdd_free(relation); array_insert(bdd_t*, info->bwdClusteredRelationArray, i, approxRelation); } } } return(unchanged); } /**Function******************************************************************** Synopsis [Returns current transition function.] Description [Returns current transition function.] SideEffects [] ******************************************************************************/ array_t * ImgGetTransitionFunction(void *methodData, Img_DirectionType directionType) { ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)methodData; if (tfmInfo->vector) return(tfmInfo->vector); if (directionType == Img_Forward_c) return(tfmInfo->fwdClusteredRelationArray); return(tfmInfo->bwdClusteredRelationArray); } /**Function******************************************************************** Synopsis [Overwrites transition function with given.] Description [Overwrites transition function with given.] SideEffects [] ******************************************************************************/ void ImgUpdateTransitionFunction(void *methodData, array_t *vector, Img_DirectionType directionType) { ImgTfmInfo_t *tfmInfo = (ImgTfmInfo_t *)methodData; if (tfmInfo->vector) tfmInfo->vector = vector; else if (directionType == Img_Forward_c) tfmInfo->fwdClusteredRelationArray = vector; else tfmInfo->bwdClusteredRelationArray = vector; } /**Function******************************************************************** Synopsis [Replace ith transition function.] Description [Replace ith transition function.] SideEffects [] ******************************************************************************/ void ImgReplaceIthTransitionFunction(void *methodData, int i, mdd_t *function, Img_DirectionType directionType) { ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; array_t *relationArray; ImgComponent_t *comp; mdd_t *old; if (info->vector) { comp = array_fetch(ImgComponent_t *, info->vector, i); mdd_free(comp->func); comp->func = function; ImgSupportClear(info, comp->support); ImgComponentGetSupport(comp); return; } if (directionType == Img_Forward_c) relationArray = info->fwdClusteredRelationArray; else relationArray = info->bwdClusteredRelationArray; old = array_fetch(mdd_t *, relationArray, i); mdd_free(old); array_insert(mdd_t *, relationArray, i, function); } /**Function******************************************************************** Synopsis [Gets the necessary options for computing the image and returns in the option structure.] Description [Gets the necessary options for computing the image and returns in the option structure.] SideEffects [] ******************************************************************************/ ImgTfmOption_t * ImgTfmGetOptions(Img_MethodType method) { char *flagValue; ImgTfmOption_t *option; option = ALLOC(ImgTfmOption_t, 1); memset(option, 0, sizeof(ImgTfmOption_t)); option->debug = ReadSetBooleanValue("tfm_debug", FALSE); option->checkEquivalence = ReadSetBooleanValue("tfm_check_equivalence", FALSE); option->writeSupportMatrix = ReadSetIntValue("tfm_write_support_matrix", 0, 2, 0); option->writeSupportMatrixWithYvars = ReadSetBooleanValue("tfm_write_support_matrix_with_y", FALSE); option->writeSupportMatrixAndStop = ReadSetBooleanValue("tfm_write_support_matrix_and_stop", FALSE); option->writeSupportMatrixReverseRow = ReadSetBooleanValue("tfm_write_support_matrix_reverse_row", TRUE); option->writeSupportMatrixReverseCol = ReadSetBooleanValue("tfm_write_support_matrix_reverse_col", TRUE); option->verbosity = ReadSetIntValue("tfm_verbosity", 0, 2, 0); if (method == Img_Tfm_c) option->splitMethod = ReadSetIntValue("tfm_split_method", 0, 3, 0); else option->splitMethod = 3; /* the default value */ option->inputSplit = ReadSetIntValue("tfm_input_split", 0, 3, 0); option->piSplitFlag = ReadSetBooleanValue("tfm_pi_split_flag", TRUE); if (method == Img_Tfm_c) option->rangeComp = ReadSetIntValue("tfm_range_comp", 0, 2, 1); else option->rangeComp = ReadSetIntValue("tfm_range_comp", 0, 2, 2); flagValue = Cmd_FlagReadByName("tfm_range_threshold"); if (flagValue == NIL(char)) option->rangeThreshold = 10; /* the default value */ else option->rangeThreshold = atoi(flagValue); flagValue = Cmd_FlagReadByName("tfm_range_try_threshold"); if (flagValue == NIL(char)) option->rangeTryThreshold = 2; /* the default value */ else option->rangeTryThreshold = atoi(flagValue); option->rangeCheckReorder = ReadSetBooleanValue("tfm_range_check_reorder", FALSE); option->tieBreakMode = ReadSetIntValue("tfm_tie_break", 0, 1, 0); option->outputSplit = ReadSetIntValue("tfm_output_split", 0, 2, 0); flagValue = Cmd_FlagReadByName("tfm_turn_depth"); if (flagValue == NIL(char)) { if (method == Img_Tfm_c) option->turnDepth = 5; /* the default for tfm */ else option->turnDepth = -1; /* the default for hybrid */ } else option->turnDepth = atoi(flagValue); option->findDecompVar = ReadSetBooleanValue("tfm_find_decomp_var", FALSE); option->globalCache = ReadSetBooleanValue("tfm_global_cache", TRUE); flagValue = Cmd_FlagReadByName("tfm_use_cache"); if (flagValue == NIL(char)) { if (method == Img_Tfm_c) option->useCache = 1; else option->useCache = 0; } else option->useCache = atoi(flagValue); flagValue = Cmd_FlagReadByName("tfm_max_chain_length"); if (flagValue == NIL(char)) option->maxChainLength = 2; /* the default value */ else option->maxChainLength = atoi(flagValue); flagValue = Cmd_FlagReadByName("tfm_init_cache_size"); if (flagValue == NIL(char)) option->initCacheSize = 1001; /* the default value */ else option->initCacheSize = atoi(flagValue); option->autoFlushCache = ReadSetIntValue("tfm_auto_flush_cache", 0, 2, 1); if (method == Img_Tfm_c) option->sortVectorFlag = ReadSetBooleanValue("tfm_sort_vector", TRUE); else option->sortVectorFlag = ReadSetBooleanValue("tfm_sort_vector", FALSE); option->printStatistics = ReadSetBooleanValue("tfm_print_stats", FALSE); option->printBddSize = ReadSetBooleanValue("tfm_print_bdd_size", FALSE); flagValue = Cmd_FlagReadByName("tfm_max_essential_depth"); if (flagValue == NIL(char)) option->maxEssentialDepth = 5; /* the default value */ else option->maxEssentialDepth = atoi(flagValue); option->findEssential = ReadSetIntValue("tfm_find_essential", 0, 2, 0); if (option->findEssential && bdd_get_package_name() != CUDD) { fprintf(vis_stderr, "** tfm error: tfm_find_essential is available for only CUDD.\n"); option->findEssential = 0; } option->printEssential = ReadSetIntValue("tfm_print_essential", 0, 2, 0); option->splitCubeFunc = ReadSetBooleanValue("tfm_split_cube_func", FALSE); option->composeIntermediateVars = ReadSetBooleanValue("tfm_compose_intermediate_vars", FALSE); if (method == Img_Tfm_c) option->preSplitMethod = ReadSetIntValue("tfm_pre_split_method", 0, 4, 0); else option->preSplitMethod = 4; option->preInputSplit = ReadSetIntValue("tfm_pre_input_split", 0, 3, 0); option->preOutputSplit = ReadSetIntValue("tfm_pre_output_split", 0, 2, 0); option->preDcLeafMethod = ReadSetIntValue("tfm_pre_dc_leaf_method", 0, 2, 0); option->preMinimize = ReadSetBooleanValue("tfm_pre_minimize", FALSE); option->trSplitMethod = ReadSetIntValue("hybrid_tr_split_method", 0, 1, 0); option->hybridMode = ReadSetIntValue("hybrid_mode", 0, 2, 1); option->buildPartialTR = ReadSetBooleanValue("hybrid_build_partial_tr", FALSE); flagValue = Cmd_FlagReadByName("hybrid_partial_num_vars"); if (flagValue == NIL(char)) option->nPartialVars = 8; /* the default value */ else option->nPartialVars = atoi(flagValue); option->partialMethod = ReadSetIntValue("hybrid_partial_method", 0, 1, 0); option->delayedSplit = ReadSetBooleanValue("hybrid_delayed_split", FALSE); flagValue = Cmd_FlagReadByName("hybrid_split_min_depth"); if (flagValue == NIL(char)) option->splitMinDepth = 1; /* the default value */ else option->splitMinDepth = atoi(flagValue); flagValue = Cmd_FlagReadByName("hybrid_split_max_depth"); if (flagValue == NIL(char)) option->splitMaxDepth = 5; /* the default value */ else option->splitMaxDepth = atoi(flagValue); flagValue = Cmd_FlagReadByName("hybrid_pre_split_min_depth"); if (flagValue == NIL(char)) option->preSplitMinDepth = 0; /* the default value */ else option->preSplitMinDepth = atoi(flagValue); flagValue = Cmd_FlagReadByName("hybrid_pre_split_max_depth"); if (flagValue == NIL(char)) option->preSplitMaxDepth = 4; /* the default value */ else option->preSplitMaxDepth = atoi(flagValue); flagValue = Cmd_FlagReadByName("hybrid_lambda_threshold"); if (flagValue == NIL(char)) option->lambdaThreshold = 0.6; /* the default value */ else sscanf(flagValue, "%f", &option->lambdaThreshold); flagValue = Cmd_FlagReadByName("hybrid_pre_lambda_threshold"); if (flagValue == NIL(char)) option->preLambdaThreshold = 0.65; /* the default value */ else sscanf(flagValue, "%f", &option->preLambdaThreshold); flagValue = Cmd_FlagReadByName("hybrid_conjoin_vector_size"); if (flagValue == NIL(char)) option->conjoinVectorSize = 10; /* the default value */ else option->conjoinVectorSize = atoi(flagValue); flagValue = Cmd_FlagReadByName("hybrid_conjoin_relation_size"); if (flagValue == NIL(char)) option->conjoinRelationSize = 1; /* the default value */ else option->conjoinRelationSize = atoi(flagValue); flagValue = Cmd_FlagReadByName("hybrid_conjoin_relation_bdd_size"); if (flagValue == NIL(char)) option->conjoinRelationBddSize = 200; /* the default value */ else option->conjoinRelationBddSize = atoi(flagValue); flagValue = Cmd_FlagReadByName("hybrid_improve_lambda"); if (flagValue == NIL(char)) option->improveLambda = 0.1; /* the default value */ else sscanf(flagValue, "%f", &option->improveLambda); flagValue = Cmd_FlagReadByName("hybrid_improve_vector_size"); if (flagValue == NIL(char)) option->improveVectorSize = 3; /* the default value */ else option->improveVectorSize = atoi(flagValue); flagValue = Cmd_FlagReadByName("hybrid_improve_vector_bdd_size"); if (flagValue == NIL(char)) option->improveVectorBddSize = 30.0; /* the default value */ else sscanf(flagValue, "%f", &option->improveVectorBddSize); option->decideMode = ReadSetIntValue("hybrid_decide_mode", 0, 3, 3); option->reorderWithFrom = ReadSetBooleanValue("hybrid_reorder_with_from", TRUE); option->preReorderWithFrom = ReadSetBooleanValue("hybrid_pre_reorder_with_from", FALSE); option->lambdaMode = ReadSetIntValue("hybrid_lambda_mode", 0, 2, 0); option->preLambdaMode = ReadSetIntValue("hybrid_pre_lambda_mode", 0, 3, 2); option->lambdaWithFrom = ReadSetBooleanValue("hybrid_lambda_with_from", TRUE); option->lambdaWithTr = ReadSetBooleanValue("hybrid_lambda_with_tr", TRUE); option->lambdaWithClustering = ReadSetBooleanValue("hybrid_lambda_with_clustering", FALSE); option->synchronizeTr = ReadSetBooleanValue("hybrid_synchronize_tr", FALSE); option->imgKeepPiInTr = ReadSetBooleanValue("hybrid_img_keep_pi", FALSE); option->preKeepPiInTr = ReadSetBooleanValue("hybrid_pre_keep_pi", FALSE); flagValue = Cmd_FlagReadByName("hybrid_tr_method"); if (flagValue == NIL(char)) option->trMethod = Img_Iwls95_c; /* the default value */ else { if (strcmp(flagValue, "iwls95") == 0) option->trMethod = Img_Iwls95_c; else if (strcmp(flagValue, "mlp") == 0) option->trMethod = Img_Mlp_c; else { fprintf(vis_stderr, "** tfm error : invalid value %s for hybrid_tr_method\n", flagValue); option->trMethod = Img_Iwls95_c; } } option->preCanonical = ReadSetBooleanValue("hybrid_pre_canonical", FALSE); option->printLambda = ReadSetBooleanValue("hybrid_print_lambda", FALSE); return(option); } /**Function******************************************************************** Synopsis [Frees current transition function vector and relation for the given direction.] Description [Frees current transition function vector and relation for the given direction.] SideEffects [] ******************************************************************************/ void ImgImageFreeClusteredTransitionRelationTfm(void *methodData, Img_DirectionType directionType) { ImgTfmInfo_t *info = (ImgTfmInfo_t *)methodData; if (info->vector) { ImgVectorFree(info->vector); info->vector = NIL(array_t); } if (info->fullVector) { ImgVectorFree(info->fullVector); info->fullVector = NIL(array_t); } if (info->partialBddVars) mdd_array_free(info->partialBddVars); if (info->partialVarFlag) FREE(info->partialVarFlag); if (info->fwdClusteredRelationArray != NIL(array_t)) { mdd_array_free(info->fwdClusteredRelationArray); info->fwdClusteredRelationArray = NIL(array_t); } if (info->bwdClusteredRelationArray != NIL(array_t)) { mdd_array_free(info->bwdClusteredRelationArray); info->bwdClusteredRelationArray = NIL(array_t); } } /**Function******************************************************************** Synopsis [Constrains the bit function and relation and creates a new transition function vector and relation.] Description [Constrains the bit function and relation and creates a new transition function vector and relation. First, the existing transition function vector and relation is freed. The bit relation is created if it isnt stored already. The bit relation is then copied into the Clustered relation of the given direction and constrained by the given constraint. The bit relation is clustered. In the case of the backward relation, the clustered relation is minimized with respect to the care set.] SideEffects [Frees current transition relation] ******************************************************************************/ void ImgImageConstrainAndClusterTransitionRelationTfm(Img_ImageInfo_t *imageInfo, Img_DirectionType direction, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus) { ImgFunctionData_t *functionData = &(imageInfo->functionData); ImgTfmInfo_t *info = (ImgTfmInfo_t *)imageInfo->methodData; graph_t *mddNetwork; mdd_manager *mddManager = Part_PartitionReadMddManager( functionData->mddNetwork); int composeIntermediateVars, findIntermediateVars; array_t *relationArray; /* free existing function vector and/or relation */ ImgImageFreeClusteredTransitionRelationTfm(imageInfo->methodData, direction); if (forceReorder) bdd_reorder(mddManager); mddNetwork = functionData->mddNetwork; /* create function vector or bit relation */ if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c && info->nVars != info->nRealVars) { if (info->option->composeIntermediateVars) { composeIntermediateVars = 1; findIntermediateVars = 0; } else { composeIntermediateVars = 0; findIntermediateVars = 1; } } else { composeIntermediateVars = 0; findIntermediateVars = 0; } if (info->buildTR == 2) { /* non-deterministic */ if (info->buildPartialTR) { info->fullVector = TfmCreateBitVector(info, composeIntermediateVars, findIntermediateVars); TfmSetupPartialTransitionRelation(info, &relationArray); } else { info->vector = NIL(array_t); relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars, findIntermediateVars); } } else { info->vector = TfmCreateBitVector(info, composeIntermediateVars, findIntermediateVars); if (info->buildTR == 0 || info->option->synchronizeTr) relationArray = NIL(array_t); else { relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars, findIntermediateVars); } } /* apply the constrain to the bit relation */ if (constrain) { if (underApprox) { MinimizeTransitionFunction(info->vector, relationArray, constrain, minimizeMethod, printStatus); } else { AddDontCareToTransitionFunction(info->vector, relationArray, constrain, minimizeMethod, printStatus); } } if (info->vector && info->option->sortVectorFlag && info->option->useCache) array_sort(info->vector, CompareIndex); if (info->buildTR) { TfmBuildRelationArray(info, functionData, relationArray, direction, 0); if (relationArray) mdd_array_free(relationArray); } /* Print information */ if (info->option->verbosity > 0){ if (info->method == Img_Tfm_c) fprintf(vis_stdout,"Computing Image Using tfm technique.\n"); else fprintf(vis_stdout,"Computing Image Using hybrid technique.\n"); fprintf(vis_stdout,"Total # of domain binary variables = %3d\n", array_n(functionData->domainBddVars)); fprintf(vis_stdout,"Total # of range binary variables = %3d\n", array_n(functionData->rangeBddVars)); fprintf(vis_stdout,"Total # of quantify binary variables = %3d\n", array_n(functionData->quantifyBddVars)); if (info->vector) { (void) fprintf(vis_stdout, "Shared size of transition function vector for image "); (void) fprintf(vis_stdout, "computation is %10ld BDD nodes (%-4d components)\n", ImgVectorBddSize(info->vector), array_n(info->vector)); } if (((direction == Img_Forward_c) || (direction == Img_Both_c)) && (info->fwdClusteredRelationArray != NIL(array_t))) { (void) fprintf(vis_stdout, "Shared size of transition relation for forward image "); (void) fprintf(vis_stdout, "computation is %10ld BDD nodes (%-4d components)\n", bdd_size_multiple(info->fwdClusteredRelationArray), array_n(info->fwdClusteredRelationArray)); } if (((direction == Img_Backward_c) || (direction == Img_Both_c)) && (info->bwdClusteredRelationArray != NIL(array_t))) { (void) fprintf(vis_stdout, "Shared size of transition relation for backward image "); (void) fprintf(vis_stdout, "computation is %10ld BDD nodes (%-4d components)\n", bdd_size_multiple(info->bwdClusteredRelationArray), array_n(info->bwdClusteredRelationArray)); } } } /**Function******************************************************************** Synopsis [Check whether transition relation is built in hybrid.] Description [Check whether transition relation is built in hybrid.] SideEffects [] ******************************************************************************/ int ImgIsPartitionedTransitionRelationTfm(Img_ImageInfo_t *imageInfo) { ImgTfmInfo_t *info = (ImgTfmInfo_t *)imageInfo->methodData; if (info->buildTR) return(1); else return(0); } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Allocates and initializes the info structure for transition function method.] Description [Allocates and initializes the info structure for transition function method.] SideEffects [] ******************************************************************************/ static ImgTfmInfo_t * TfmInfoStructAlloc(Img_MethodType method) { ImgTfmInfo_t *info; info = ALLOC(ImgTfmInfo_t, 1); memset(info, 0, sizeof(ImgTfmInfo_t)); info->method = method; info->option = ImgTfmGetOptions(method); return(info); } /**Function******************************************************************** Synopsis [Compares two variable indices of components.] Description [Compares two variable indices of components.] SideEffects [] ******************************************************************************/ static int CompareIndex(const void *e1, const void *e2) { ImgComponent_t *c1, *c2; int id1, id2; c1 = *((ImgComponent_t **)e1); c2 = *((ImgComponent_t **)e2); id1 = (int)bdd_top_var_id(c1->var); id2 = (int)bdd_top_var_id(c2->var); if (id1 > id2) return(1); else if (id1 < id2) return(-1); else return(0); } /**Function******************************************************************** Synopsis [Flushes cache entries in a list.] Description [Flushes cache entries in a list.] SideEffects [] ******************************************************************************/ static int HookInfoFunction(bdd_manager *mgr, char *str, void *method) { ImgTfmInfo_t *info; st_generator *stGen; if (HookInfoList) { st_foreach_item(HookInfoList, stGen, &info, NULL) { if (info->imgCache) ImgFlushCache(info->imgCache); if (info->preCache) ImgFlushCache(info->preCache); } } return(0); } /**Function******************************************************************** Synopsis [Chooses variables for static splitting.] Description [Chooses variables for static splitting. partialMethod is set by hybrid_partial_method. Refer to print_hybrid_options command.] SideEffects [] ******************************************************************************/ static array_t * ChoosePartialVars(ImgTfmInfo_t *info, array_t *vector, int nPartialVars, int partialMethod) { int i, j, nVars; ImgComponent_t *comp; char *support; int *varCost; int big, small, nChosen, insert, id; mdd_t *var; int *partialVars = ALLOC(int, nPartialVars); array_t *partialBddVars = array_alloc(mdd_t *, 0); nVars = info->nVars; varCost = ALLOC(int, nVars); memset(varCost, 0, sizeof(int) * nVars); if (partialMethod == 0) { /* chooses the variable whose function has the largest bdd size */ for (i = 0; i < array_n(vector); i++) { comp = array_fetch(ImgComponent_t *, vector, i); id = (int)bdd_top_var_id(comp->var); varCost[id] = bdd_size(comp->func); } } else { /* chooses the variable that appears the most frequently */ for (i = 0; i < array_n(vector); i++) { comp = array_fetch(ImgComponent_t *, vector, i); support = comp->support; for (j = 0; j < nVars; j++) { if (support[j]) varCost[j]++; } } } nChosen = 0; big = small = -1; for (i = 0; i < nVars; i++) { if (varCost[i] == 0) continue; if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *))) continue; if (info->intermediateVarsTable && st_lookup(info->intermediateVarsTable, (char *)(long)i, NIL(char *))) { continue; } if (nChosen == 0) { partialVars[0] = i; nChosen = 1; big = small = varCost[i]; } else if (varCost[i] < small) { if (nChosen < nPartialVars) { partialVars[nChosen] = i; nChosen++; small = varCost[i]; } else continue; } else if (varCost[i] > big) { if (nChosen < nPartialVars) { for (j = nChosen; j > 0; j--) partialVars[j] = partialVars[j - 1]; partialVars[0] = i; nChosen++; big = varCost[i]; } else { for (j = nPartialVars - 1; j > 0; j--) partialVars[j] = partialVars[j - 1]; partialVars[0] = i; big = varCost[i]; small = varCost[partialVars[nPartialVars - 1]]; } } else { insert = nChosen; for (j = 0; j < nChosen; j++) { if (varCost[i] > varCost[partialVars[j]]) { insert = j; break; } } if (nChosen < nPartialVars) { for (j = nChosen; j > insert; j--) partialVars[j] = partialVars[j - 1]; partialVars[insert] = i; nChosen++; } else if (insert < nChosen) { for (j = nPartialVars - 1; j > insert; j--) partialVars[j] = partialVars[j - 1]; partialVars[insert] = i; small = varCost[partialVars[nPartialVars - 1]]; } } } FREE(varCost); for (i = 0; i < nChosen; i++) { var = bdd_var_with_index(info->manager, partialVars[i]); array_insert_last(mdd_t *, partialBddVars, var); } FREE(partialVars); return(partialBddVars); } /**Function******************************************************************** Synopsis [Prints statistics of recursions for transition function method.] Description [Prints statistics of recursions for transition function method.] SideEffects [] SeeAlso [] ******************************************************************************/ static void PrintRecursionStatistics(ImgTfmInfo_t *info, int preFlag) { float avgDepth, avgDecomp; int nRecurs, nLeaves, nTurns, nDecomps, topDecomp, maxDecomp, maxDepth; GetRecursionStatistics(info, preFlag, &nRecurs, &nLeaves, &nTurns, &avgDepth, &maxDepth, &nDecomps, &topDecomp, &maxDecomp, &avgDecomp); if (preFlag) fprintf(vis_stdout, "** recursion statistics of splitting (preImg) **\n"); else fprintf(vis_stdout, "** recursion statistics of splitting (img) **\n"); fprintf(vis_stdout, "# recursions = %d\n", nRecurs); fprintf(vis_stdout, "# leaves = %d\n", nLeaves); fprintf(vis_stdout, "# turns = %d\n", nTurns); fprintf(vis_stdout, "# average recursion depth = %g (max = %d)\n", avgDepth, maxDepth); if (!preFlag) { fprintf(vis_stdout, "# decompositions = %d (top = %d, max = %d, average = %g)\n", nDecomps, topDecomp, maxDecomp, avgDecomp); } } /**Function******************************************************************** Synopsis [Prints statistics of finding essential and dependent variables.] Description [Prints statistics of finding essential and dependent variables.] SideEffects [] SeeAlso [] ******************************************************************************/ static void PrintFoundVariableStatistics(ImgTfmInfo_t *info, int preFlag) { int i, maxDepth; if (preFlag) { fprintf(vis_stdout, "# split = %d, conjoin = %d\n", info->nSplitsB, info->nConjoinsB); return; } fprintf(vis_stdout, "# found essential vars = %d (top = %d, average = %g, averageDepth = %g)\n", info->nFoundEssentials, info->topFoundEssentialDepth, info->averageFoundEssential, info->averageFoundEssentialDepth); if (info->option->printEssential == 1) { maxDepth = info->maxDepth < IMG_TF_MAX_PRINT_DEPTH ? info->maxDepth : IMG_TF_MAX_PRINT_DEPTH; fprintf(vis_stdout, "foundEssential:"); for (i = 0; i < maxDepth; i++) fprintf(vis_stdout, " [%d]%d", i, info->foundEssentials[i]); fprintf(vis_stdout, "\n"); } if (info->useConstraint == 2) fprintf(vis_stdout, "# range computations = %d\n", info->nRangeComps); fprintf(vis_stdout, "# found dependent vars = %d (average = %g)\n", info->nFoundDependVars, info->averageFoundDependVars); fprintf(vis_stdout, "# tautologous subimage = %d\n", info->nEmptySubImage); fprintf(vis_stdout, "# split = %d, conjoin = %d, cubeSplit = %d\n", info->nSplits, info->nConjoins, info->nCubeSplits); } /**Function******************************************************************** Synopsis [Returns the statistics of recursions of transition function method.] Description [Returns the statistics of recursions of transition function method.] SideEffects [] SeeAlso [] ******************************************************************************/ static void GetRecursionStatistics(ImgTfmInfo_t *info, int preFlag, int *nRecurs, int *nLeaves, int *nTurns, float *averageDepth, int *maxDepth, int *nDecomps, int *topDecomp, int *maxDecomp, float *averageDecomp) { if (preFlag) { *nRecurs = info->nRecursionB; *nLeaves = info->nLeavesB; *nTurns = info->nTurnsB; *averageDepth = info->averageDepthB; *maxDepth = info->maxDepthB; *nDecomps = 0; *topDecomp = 0; *maxDecomp = 0; *averageDecomp = 0.0; } else { *nRecurs = info->nRecursion; *nLeaves = info->nLeaves; *nTurns = info->nTurns; *averageDepth = info->averageDepth; *maxDepth = info->maxDepth; *nDecomps = info->nDecomps; *topDecomp = info->topDecomp; *maxDecomp = info->maxDecomp; *averageDecomp = info->averageDecomp; } } /**Function******************************************************************** Synopsis [Reads a set integer value.] Description [Reads a set integer value.] SideEffects [] SeeAlso [] ******************************************************************************/ static int ReadSetIntValue(char *string, int l, int u, int defaultValue) { char *flagValue; int tmp; int value = defaultValue; flagValue = Cmd_FlagReadByName(string); if (flagValue != NIL(char)) { sscanf(flagValue, "%d", &tmp); if (tmp >= l && (tmp <= u || u == 0)) value = tmp; else { fprintf(vis_stderr, "** tfm error: invalid value %d for %s[%d-%d]. **\n", tmp, string, l, u); } } return(value); } /**Function******************************************************************** Synopsis [Reads a set Boolean value.] Description [Reads a set Boolean value.] SideEffects [] SeeAlso [] ******************************************************************************/ static boolean ReadSetBooleanValue(char *string, boolean defaultValue) { char *flagValue; boolean value = defaultValue; flagValue = Cmd_FlagReadByName(string); if (flagValue != NIL(char)) { if (strcmp(flagValue, "yes") == 0) value = TRUE; else if (strcmp(flagValue, "no") == 0) value = FALSE; else { fprintf(vis_stderr, "** tfm error: invalid value %s for %s[yes/no]. **\n", flagValue, string); } } return(value); } /**Function******************************************************************** Synopsis [Traverses the partition recursively, creating the functions for the intermediate vertices.] Description [Traverses the partition recursively, creating the functions for the intermediate vertices. This function is originated from PartitionTraverseRecursively in imgIwls95.c] SideEffects [] ******************************************************************************/ static void FindIntermediateVarsRecursively(ImgTfmInfo_t *info, mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *vector, st_table *domainQuantifyVarMddIdTable, array_t *intermediateVarMddIdArray) { Mvf_Function_t *mvf; lsList faninEdges; lsGen gen; vertex_t *faninVertex; edge_t *faninEdge; array_t *varBddFunctionArray, *bddArray; int i; mdd_t *var, *func; ImgComponent_t *comp; if (st_is_member(vertexTable, (char *)vertex)) return; st_insert(vertexTable, (char *)vertex, NIL(char)); if (mddId != -1) { /* This is not the next state function node */ /* There is an mdd variable associated with this vertex */ array_insert_last(int, intermediateVarMddIdArray, mddId); mvf = Part_VertexReadFunction(vertex); varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mddManager, mddId, mvf); bddArray = mdd_id_to_bdd_array(mddManager, mddId); assert(array_n(varBddFunctionArray) == array_n(bddArray)); for (i = 0; i < array_n(bddArray); i++) { var = array_fetch(mdd_t *, bddArray, i); func = array_fetch(mdd_t *, varBddFunctionArray, i); comp = ImgComponentAlloc(info); comp->var = var; comp->func = func; comp->intermediate = 1; ImgComponentGetSupport(comp); array_insert_last(ImgComponent_t *, vector, comp); } array_free(varBddFunctionArray); array_free(bddArray); } faninEdges = g_get_in_edges(vertex); if (lsLength(faninEdges) == 0) return; lsForEachItem(faninEdges, gen, faninEdge) { faninVertex = g_e_source(faninEdge); mddId = Part_VertexReadMddId(faninVertex); if (st_is_member(domainQuantifyVarMddIdTable, (char *)(long)mddId)) { /* This is either domain var or quantify var */ continue; } FindIntermediateVarsRecursively(info, mddManager, faninVertex, mddId, vertexTable, vector, domainQuantifyVarMddIdTable, intermediateVarMddIdArray); } } /**Function******************************************************************** Synopsis [Traverses the partition recursively, creating the relations for the intermediate vertices.] Description [Traverses the partition recursively, creating the relations for the intermediate vertices. This function is a copy of PartitionTraverseRecursively from imgIwls95.c.] SideEffects [] ******************************************************************************/ static void GetIntermediateRelationsRecursively(mdd_manager *mddManager, vertex_t *vertex, int mddId, st_table *vertexTable, array_t *relationArray, st_table *domainQuantifyVarMddIdTable, array_t *intermediateVarMddIdArray) { Mvf_Function_t *mvf; lsList faninEdges; lsGen gen; vertex_t *faninVertex; edge_t *faninEdge; array_t *varBddRelationArray; if (st_is_member(vertexTable, (char *)vertex)) return; st_insert(vertexTable, (char *)vertex, NIL(char)); if (mddId != -1) { /* This is not the next state function node */ /* There is an mdd variable associated with this vertex */ array_insert_last(int, intermediateVarMddIdArray, mddId); mvf = Part_VertexReadFunction(vertex); varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, mddId, mvf); array_append(relationArray, varBddRelationArray); array_free(varBddRelationArray); } faninEdges = g_get_in_edges(vertex); if (lsLength(faninEdges) == 0) return; lsForEachItem(faninEdges, gen, faninEdge) { faninVertex = g_e_source(faninEdge); mddId = Part_VertexReadMddId(faninVertex); if (st_is_member(domainQuantifyVarMddIdTable, (char *)(long)mddId)) { /* This is either domain var or quantify var */ continue; } GetIntermediateRelationsRecursively(mddManager, faninVertex, mddId, vertexTable, relationArray, domainQuantifyVarMddIdTable, intermediateVarMddIdArray); } } /**Function******************************************************************** Synopsis [Checks whether the network is nondeterministic.] Description [Checks whether the network is nondeterministic. However, current implementatin is just checking whether the network has multi-valued variables.] SideEffects [] SeeAlso [] ******************************************************************************/ static int CheckNondeterminism(Ntk_Network_t *network) { Ntk_Node_t *node; lsGen gen; Var_Variable_t *var; int numValues; Ntk_NetworkForEachNode(network, gen, node) { var = Ntk_NodeReadVariable(node); numValues = Var_VariableReadNumValues(var); if (numValues > 2) { lsFinish(gen); return 1; } } return 0; } /**Function******************************************************************** Synopsis [Creates function vector.] Description [Creates function vector.] SideEffects [] SeeAlso [ImgImageInfoInitializeTfm] ******************************************************************************/ static array_t * TfmCreateBitVector(ImgTfmInfo_t *info, int composeIntermediateVars, int findIntermediateVars) { int i, j; array_t *vector; graph_t *mddNetwork; mdd_manager *mddManager; array_t *roots; array_t *rangeVarMddIdArray; int index; mdd_t *var; ImgComponent_t *comp; st_table *vertexTable; st_table *domainQuantifyVarMddIdTable; array_t *intermediateVarMddIdArray, *intermediateBddVars; int mddId; ImgFunctionData_t *functionData = info->functionData; mddNetwork = functionData->mddNetwork; mddManager = Part_PartitionReadMddManager(mddNetwork); roots = functionData->roots; rangeVarMddIdArray = functionData->rangeVars; if (findIntermediateVars) { vertexTable = st_init_table(st_ptrcmp, st_ptrhash); domainQuantifyVarMddIdTable = st_init_table(st_numcmp, st_numhash); intermediateVarMddIdArray = array_alloc(int, 0); arrayForEachItem(int, functionData->domainVars, i, mddId) { st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char)); } arrayForEachItem(int, functionData->quantifyVars, i, mddId) { st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char)); } } else { vertexTable = NIL(st_table); domainQuantifyVarMddIdTable = NIL(st_table); intermediateVarMddIdArray = NIL(array_t); } vector = array_alloc(ImgComponent_t *, 0); /* * Iterate over the function of all the root nodes. */ for (i = 0; i < array_n(roots); i++) { mdd_t *func; char *nodeName = array_fetch(char*, roots, i); vertex_t *vertex = Part_PartitionFindVertexByName(mddNetwork, nodeName); Mvf_Function_t *mvf = Part_VertexReadFunction(vertex); int mddId = array_fetch(int, rangeVarMddIdArray, i); array_t *varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mddManager, mddId, mvf); array_t *bddArray = mdd_id_to_bdd_array(mddManager, mddId); assert(array_n(varBddFunctionArray) == array_n(bddArray)); if (info->option->debug) { mdd_t *rel1, *rel2; array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, mddId, mvf); for (j = 0; j < array_n(bddArray); j++) { var = array_fetch(mdd_t *, bddArray, j); func = array_fetch(mdd_t *, varBddFunctionArray, j); rel1 = array_fetch(mdd_t *, varBddRelationArray, j); rel2 = mdd_xnor(var, func); if (!mdd_equal(rel1, rel2)) { if (mdd_lequal(rel1, rel2, 1, 1)) fprintf(vis_stdout, "** %d(%d): rel < funcRel\n", i, j); else if (mdd_lequal(rel2, rel1, 1, 1)) fprintf(vis_stdout, "** %d(%d): rel > funcRel\n", i, j); else fprintf(vis_stdout, "** %d(%d): rel != funcRel\n", i, j); } mdd_free(rel1); mdd_free(rel2); } array_free(varBddRelationArray); } for (j = 0; j < array_n(bddArray); j++) { var = array_fetch(mdd_t *, bddArray, j); func = array_fetch(mdd_t *, varBddFunctionArray, j); if (array_n(bddArray) == 1 && bdd_is_tautology(func, 1)) { array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, mddId, mvf); mdd_t *relation = array_fetch(mdd_t *, varBddRelationArray, 0); /* non-deterministic constant */ if (bdd_is_tautology(relation, 1)) { mdd_array_free(varBddRelationArray); mdd_free(func); break; } mdd_array_free(varBddRelationArray); } comp = ImgComponentAlloc(info); comp->var = ImgSubstitute(var, functionData, Img_R2D_c); if (composeIntermediateVars) { comp->func = Img_ComposeIntermediateNodes(functionData->mddNetwork, func, functionData->domainVars, functionData->rangeVars, functionData->quantifyVars); mdd_free(func); } else comp->func = func; ImgComponentGetSupport(comp); array_insert_last(ImgComponent_t *, vector, comp); } if (findIntermediateVars) { int n1, n2; n1 = array_n(vector); FindIntermediateVarsRecursively(info, mddManager, vertex, -1, vertexTable, vector, domainQuantifyVarMddIdTable, intermediateVarMddIdArray); n2 = array_n(vector); info->nIntermediateVars += n2 - n1; } array_free(varBddFunctionArray); mdd_array_free(bddArray); } if (findIntermediateVars) { int nonExistFlag; /* checks whether intermediate variables are already found */ if (info->intermediateVarsTable && info->intermediateBddVars && info->newQuantifyBddVars) { nonExistFlag = 0; } else { assert(!info->intermediateVarsTable); assert(!info->intermediateBddVars); assert(!info->newQuantifyBddVars); nonExistFlag = 1; } if (info->option->verbosity) { (void)fprintf(vis_stdout, "** img info: %d intermediate variables\n", info->nIntermediateVars); } st_free_table(vertexTable); st_free_table(domainQuantifyVarMddIdTable); if (nonExistFlag) { intermediateBddVars = mdd_id_array_to_bdd_array(mddManager, intermediateVarMddIdArray); } else intermediateBddVars = NIL(array_t); array_free(intermediateVarMddIdArray); if (nonExistFlag) { info->intermediateVarsTable = st_init_table(st_numcmp, st_numhash); for (i = 0; i < array_n(intermediateBddVars); i++) { var = array_fetch(mdd_t *, intermediateBddVars, i); index = (int)bdd_top_var_id(var); st_insert(info->intermediateVarsTable, (char *)(long)index, NIL(char)); } info->newQuantifyBddVars = mdd_array_duplicate( functionData->quantifyBddVars); for (i = 0; i < array_n(intermediateBddVars); i++) { var = array_fetch(mdd_t *, intermediateBddVars, i); array_insert_last(mdd_t *, info->newQuantifyBddVars, mdd_dup(var)); } info->intermediateBddVars = intermediateBddVars; } } return(vector); } /**Function******************************************************************** Synopsis [Creates the bit relations.] Description [Creates the bit relations.] SideEffects [] SeeAlso [ImgImageInfoInitializeTfm] ******************************************************************************/ static array_t * TfmCreateBitRelationArray(ImgTfmInfo_t *info, int composeIntermediateVars, int findIntermediateVars) { array_t *bddRelationArray = array_alloc(mdd_t*, 0); ImgFunctionData_t *functionData = info->functionData; array_t *domainVarMddIdArray = functionData->domainVars; array_t *rangeVarMddIdArray = functionData->rangeVars; array_t *quantifyVarMddIdArray = functionData->quantifyVars; graph_t *mddNetwork = functionData->mddNetwork; array_t *roots = functionData->roots; int i, j, n1, n2, mddId, nIntermediateVars = 0; mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork); st_table *vertexTable = st_init_table(st_ptrcmp, st_ptrhash); st_table *domainQuantifyVarMddIdTable = st_init_table(st_numcmp, st_numhash); char *nodeName; mdd_t *relation, *composedRelation; array_t *intermediateVarMddIdArray, *intermediateBddVars; int index; mdd_t *var; if (findIntermediateVars) intermediateVarMddIdArray = array_alloc(int, 0); else intermediateVarMddIdArray = NIL(array_t); arrayForEachItem(int, domainVarMddIdArray, i, mddId) { st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char)); } arrayForEachItem(int, quantifyVarMddIdArray, i, mddId) { st_insert(domainQuantifyVarMddIdTable, (char *)(long)mddId, NIL(char)); } arrayForEachItem(char *, roots, i, nodeName) { vertex_t *vertex = Part_PartitionFindVertexByName(mddNetwork, nodeName); Mvf_Function_t *mvf = Part_VertexReadFunction(vertex); int mddId = array_fetch(int, rangeVarMddIdArray, i); array_t *varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mddManager, mddId, mvf); if (composeIntermediateVars) { for (j = 0; j < array_n(varBddRelationArray); j++) { relation = array_fetch(mdd_t *, varBddRelationArray, j); composedRelation = Img_ComposeIntermediateNodes( functionData->mddNetwork, relation, functionData->domainVars, functionData->rangeVars, functionData->quantifyVars); mdd_free(relation); array_insert(mdd_t *, varBddRelationArray, j, composedRelation); } array_append(bddRelationArray, varBddRelationArray); array_free(varBddRelationArray); } else { array_append(bddRelationArray, varBddRelationArray); array_free(varBddRelationArray); if (findIntermediateVars) { if (info->option->verbosity) n1 = array_n(bddRelationArray); GetIntermediateRelationsRecursively(mddManager, vertex, -1, vertexTable, bddRelationArray, domainQuantifyVarMddIdTable, intermediateVarMddIdArray); if (info->option->verbosity) { n2 = array_n(bddRelationArray); nIntermediateVars += n2 - n1; } } } } st_free_table(vertexTable); st_free_table(domainQuantifyVarMddIdTable); if (findIntermediateVars) { int nonExistFlag; /* checks whether intermediate variables are already found */ if (info->intermediateVarsTable && info->intermediateBddVars && info->newQuantifyBddVars) { nonExistFlag = 0; } else { assert(!info->intermediateVarsTable); assert(!info->intermediateBddVars); assert(!info->newQuantifyBddVars); nonExistFlag = 1; } if (info->option->verbosity) { (void)fprintf(vis_stdout, "** img info: %d intermediate variables\n", info->nIntermediateVars); } if (nonExistFlag) { intermediateBddVars = mdd_id_array_to_bdd_array(mddManager, intermediateVarMddIdArray); } else intermediateBddVars = NIL(array_t); array_free(intermediateVarMddIdArray); if (nonExistFlag) { info->intermediateVarsTable = st_init_table(st_numcmp, st_numhash); for (i = 0; i < array_n(intermediateBddVars); i++) { var = array_fetch(mdd_t *, intermediateBddVars, i); index = (int)bdd_top_var_id(var); st_insert(info->intermediateVarsTable, (char *)(long)index, NIL(char)); } info->newQuantifyBddVars = mdd_array_duplicate( functionData->quantifyBddVars); for (i = 0; i < array_n(intermediateBddVars); i++) { var = array_fetch(mdd_t *, intermediateBddVars, i); array_insert_last(mdd_t *, info->newQuantifyBddVars, mdd_dup(var)); } info->intermediateBddVars = intermediateBddVars; } } return(bddRelationArray); } /**Function******************************************************************** Synopsis [Builds partial vector and relation array.] Description [Builds partial vector and relation array.] SideEffects [] SeeAlso [ImgImageInfoInitializeTfm] ******************************************************************************/ static void TfmSetupPartialTransitionRelation(ImgTfmInfo_t *info, array_t **partialRelationArray) { int i, id; mdd_t *var, *relation; ImgComponent_t *comp, *newComp; array_t *partialVector; ImgFunctionData_t *functionData = info->functionData; if (!info->buildPartialTR) return; info->partialBddVars = ChoosePartialVars(info, info->fullVector, info->option->nPartialVars, info->option->partialMethod); info->partialVarFlag = ALLOC(char, info->nVars); memset(info->partialVarFlag, 0, sizeof(char) * info->nVars); for (i = 0; i < array_n(info->partialBddVars); i++) { var = array_fetch(mdd_t *, info->partialBddVars, i); id = (int)bdd_top_var_id(var); info->partialVarFlag[id] = 1; } partialVector = array_alloc(ImgComponent_t *, 0); if (partialRelationArray) *partialRelationArray = array_alloc(mdd_t *, 0); for (i = 0; i < array_n(info->fullVector); i++) { comp = array_fetch(ImgComponent_t *, info->fullVector, i); id = (int)bdd_top_var_id(comp->var); if (info->partialVarFlag[id]) { newComp = ImgComponentCopy(info, comp); array_insert_last(ImgComponent_t *, partialVector, newComp); if (newComp->intermediate) relation = mdd_xnor(newComp->var, newComp->func); else { var = ImgSubstitute(newComp->var, functionData, Img_D2R_c); relation = mdd_xnor(var, newComp->func); mdd_free(var); } array_insert_last(mdd_t *, *partialRelationArray, relation); } } info->vector = partialVector; } /**Function******************************************************************** Synopsis [Builds relation array from function vector or bit relation.] Description [Builds relation array from function vector or bit relation.] SideEffects [] SeeAlso [ImgImageInfoInitializeTfm] ******************************************************************************/ static void TfmBuildRelationArray(ImgTfmInfo_t *info, ImgFunctionData_t *functionData, array_t *bitRelationArray, Img_DirectionType directionType, int writeMatrix) { int i; mdd_t *var, *relation; array_t *relationArray; ImgComponent_t *comp; int id; array_t *domainVarBddArray, *quantifyVarBddArray; mdd_t *one, *res1, *res2; char filename[20]; int composeIntermediateVars, findIntermediateVars; if ((info->buildTR == 1 && info->option->synchronizeTr) || info->buildPartialTR) { relationArray = array_alloc(mdd_t *, 0); if (info->fullVector) { for (i = 0; i < array_n(info->fullVector); i++) { comp = array_fetch(ImgComponent_t *, info->fullVector, i); id = (int)bdd_top_var_id(comp->var); if (!info->partialVarFlag[id]) { if (comp->intermediate) relation = mdd_xnor(comp->var, comp->func); else { var = ImgSubstitute(comp->var, functionData, Img_D2R_c); relation = mdd_xnor(var, comp->func); mdd_free(var); } array_insert_last(mdd_t *, relationArray, relation); } } } else { for (i = 0; i < array_n(info->vector); i++) { comp = array_fetch(ImgComponent_t *, info->vector, i); if (comp->intermediate) relation = mdd_xnor(comp->var, comp->func); else { var = ImgSubstitute(comp->var, functionData, Img_D2R_c); relation = mdd_xnor(var, comp->func); mdd_free(var); } array_insert_last(mdd_t *, relationArray, relation); } } if (directionType == Img_Forward_c || directionType == Img_Both_c) { if (info->imgKeepPiInTr) { if (info->intermediateBddVars) quantifyVarBddArray = info->intermediateBddVars; else quantifyVarBddArray = array_alloc(mdd_t *, 0); domainVarBddArray = array_join(info->domainVarBddArray, info->quantifyVarBddArray); } else { if (info->newQuantifyBddVars) quantifyVarBddArray = info->newQuantifyBddVars; else quantifyVarBddArray = info->quantifyVarBddArray; domainVarBddArray = info->domainVarBddArray; } info->fwdClusteredRelationArray = ImgClusterRelationArray( info->manager, info->functionData, info->option->trMethod, Img_Forward_c, info->trmOption, relationArray, domainVarBddArray, quantifyVarBddArray, info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray, &info->fwdSmoothVarCubeArray, 0); if (writeMatrix && info->option->writeSupportMatrix == 3) { sprintf(filename, "support%d.mat", info->option->supportFileCount++); ImgWriteSupportMatrix(info, info->vector, info->fwdClusteredRelationArray, filename); } else if (writeMatrix && info->option->writeSupportMatrix == 2) { sprintf(filename, "support%d.mat", info->option->supportFileCount++); ImgWriteSupportMatrix(info, NIL(array_t), info->fwdClusteredRelationArray, filename); } if (info->imgKeepPiInTr) { if (!info->intermediateBddVars) array_free(quantifyVarBddArray); array_free(domainVarBddArray); } if (info->option->checkEquivalence && (!info->fullVector)) { assert(ImgCheckEquivalence(info, info->vector, info->fwdClusteredRelationArray, NIL(mdd_t), NIL(mdd_t), 0)); } if (info->option->debug) { one = mdd_one(info->manager); if (info->fullVector) { res1 = ImgImageByHybrid(info, info->fullVector, one); res2 = ImgImageByHybridWithStaticSplit(info, info->vector, one, info->fwdClusteredRelationArray, NIL(mdd_t), NIL(mdd_t)); } else { res1 = ImgImageByHybrid(info, info->vector, one); res2 = ImgImageByHybridWithStaticSplit(info, NIL(array_t), one, info->fwdClusteredRelationArray, NIL(mdd_t), NIL(mdd_t)); } assert(mdd_equal(res1, res2)); mdd_free(one); mdd_free(res1); mdd_free(res2); } } if (directionType == Img_Backward_c || directionType == Img_Both_c) { if (info->preKeepPiInTr) { if (info->intermediateBddVars) quantifyVarBddArray = info->intermediateBddVars; else quantifyVarBddArray = array_alloc(mdd_t *, 0); domainVarBddArray = array_join(info->domainVarBddArray, info->quantifyVarBddArray); } else { if (info->newQuantifyBddVars) quantifyVarBddArray = info->newQuantifyBddVars; else quantifyVarBddArray = info->quantifyVarBddArray; domainVarBddArray = info->domainVarBddArray; } info->bwdClusteredRelationArray = ImgClusterRelationArray( info->manager, info->functionData, info->option->trMethod, Img_Backward_c, info->trmOption, relationArray, domainVarBddArray, quantifyVarBddArray, info->rangeVarBddArray, &info->bwdArraySmoothVarBddArray, &info->bwdSmoothVarCubeArray, 0); if (writeMatrix && info->option->writeSupportMatrix == 3) { sprintf(filename, "support%d.mat", info->option->supportFileCount++); ImgWriteSupportMatrix(info, info->vector, info->bwdClusteredRelationArray, filename); } else if (writeMatrix && info->option->writeSupportMatrix == 2) { sprintf(filename, "support%d.mat", info->option->supportFileCount++); ImgWriteSupportMatrix(info, NIL(array_t), info->bwdClusteredRelationArray, filename); } if (info->preKeepPiInTr) { if (!info->intermediateBddVars) array_free(quantifyVarBddArray); array_free(domainVarBddArray); } if (info->option->checkEquivalence && (!info->fullVector)) { assert(ImgCheckEquivalence(info, info->vector, info->bwdClusteredRelationArray, NIL(mdd_t), NIL(mdd_t), 1)); } if (info->option->debug) { one = mdd_one(info->manager); if (info->fullVector) { res1 = ImgImageByHybrid(info, info->fullVector, one); res2 = ImgImageByHybridWithStaticSplit(info, info->vector, one, info->bwdClusteredRelationArray, NIL(mdd_t), NIL(mdd_t)); } else { res1 = ImgImageByHybrid(info, info->vector, one); res2 = ImgImageByHybridWithStaticSplit(info, NIL(array_t), one, info->bwdClusteredRelationArray, NIL(mdd_t), NIL(mdd_t)); } assert(mdd_equal(res1, res2)); mdd_free(one); mdd_free(res1); mdd_free(res2); } } mdd_array_free(relationArray); } else { graph_t *mddNetwork = functionData->mddNetwork; if (bitRelationArray) relationArray = bitRelationArray; else { if (Part_PartitionReadMethod(mddNetwork) == Part_Frontier_c && info->nVars != info->nRealVars) { if (info->option->composeIntermediateVars) { composeIntermediateVars = 1; findIntermediateVars = 0; } else { composeIntermediateVars = 0; findIntermediateVars = 1; } } else { composeIntermediateVars = 0; findIntermediateVars = 0; } relationArray = TfmCreateBitRelationArray(info, composeIntermediateVars, findIntermediateVars); } if (directionType == Img_Forward_c || directionType == Img_Both_c) { if (info->imgKeepPiInTr) { if (info->intermediateBddVars) quantifyVarBddArray = info->intermediateBddVars; else quantifyVarBddArray = array_alloc(mdd_t *, 0); domainVarBddArray = array_join(info->domainVarBddArray, info->quantifyVarBddArray); } else { if (info->newQuantifyBddVars) quantifyVarBddArray = info->newQuantifyBddVars; else quantifyVarBddArray = info->quantifyVarBddArray; domainVarBddArray = info->domainVarBddArray; } info->fwdClusteredRelationArray = ImgClusterRelationArray( info->manager, info->functionData, info->option->trMethod, Img_Forward_c, info->trmOption, relationArray, domainVarBddArray, quantifyVarBddArray, info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray, &info->fwdSmoothVarCubeArray, 0); if (writeMatrix && info->option->writeSupportMatrix >= 2) { sprintf(filename, "support%d.mat", info->option->supportFileCount++); ImgWriteSupportMatrix(info, NIL(array_t), info->fwdClusteredRelationArray, filename); } if (info->imgKeepPiInTr) { if (!info->intermediateBddVars) array_free(quantifyVarBddArray); array_free(domainVarBddArray); } } if (directionType == Img_Backward_c || directionType == Img_Both_c) { if (info->preKeepPiInTr) { if (info->intermediateBddVars) quantifyVarBddArray = info->intermediateBddVars; else quantifyVarBddArray = array_alloc(mdd_t *, 0); domainVarBddArray = array_join(info->domainVarBddArray, info->quantifyVarBddArray); } else { if (info->newQuantifyBddVars) quantifyVarBddArray = info->newQuantifyBddVars; else quantifyVarBddArray = info->quantifyVarBddArray; domainVarBddArray = info->domainVarBddArray; } info->bwdClusteredRelationArray = ImgClusterRelationArray( info->manager, info->functionData, info->option->trMethod, Img_Backward_c, info->trmOption, relationArray, domainVarBddArray, quantifyVarBddArray, info->rangeVarBddArray, &info->bwdArraySmoothVarBddArray, &info->bwdSmoothVarCubeArray, 0); if (writeMatrix && info->option->writeSupportMatrix >= 2) { sprintf(filename, "support%d.mat", info->option->supportFileCount++); ImgWriteSupportMatrix(info, NIL(array_t), info->bwdClusteredRelationArray, filename); } if (info->preKeepPiInTr) { if (!info->intermediateBddVars) array_free(quantifyVarBddArray); array_free(domainVarBddArray); } } if (!bitRelationArray) mdd_array_free(relationArray); } } /**Function******************************************************************** Synopsis [Rebuilds transition relation from function vector.] Description [Rebuilds transition relation from function vector.] SideEffects [] SeeAlso [] ******************************************************************************/ static void RebuildTransitionRelation(ImgTfmInfo_t *info, Img_DirectionType directionType) { int i; mdd_t *var, *relation; ImgComponent_t *comp; array_t *relationArray; array_t *quantifyVarBddArray, *domainVarBddArray; relationArray = array_alloc(mdd_t *, 0); for (i = 0; i < array_n(info->vector); i++) { comp = array_fetch(ImgComponent_t *, info->vector, i); var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c); relation = mdd_xnor(var, comp->func); array_insert_last(mdd_t *, relationArray, relation); mdd_free(var); } if (directionType == Img_Forward_c || directionType == Img_Both_c) { mdd_array_free(info->fwdClusteredRelationArray); if (info->imgKeepPiInTr) { if (info->intermediateBddVars) quantifyVarBddArray = info->intermediateBddVars; else quantifyVarBddArray = array_alloc(mdd_t *, 0); domainVarBddArray = array_join(info->domainVarBddArray, info->quantifyVarBddArray); } else { if (info->newQuantifyBddVars) quantifyVarBddArray = info->newQuantifyBddVars; else quantifyVarBddArray = info->quantifyVarBddArray; domainVarBddArray = info->domainVarBddArray; } info->fwdClusteredRelationArray = ImgClusterRelationArray( info->manager, info->functionData, info->option->trMethod, Img_Forward_c, info->trmOption, relationArray, domainVarBddArray, quantifyVarBddArray, info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray, &info->fwdSmoothVarCubeArray, 0); if (info->imgKeepPiInTr) { if (!info->intermediateBddVars) array_free(quantifyVarBddArray); array_free(domainVarBddArray); } } if (directionType == Img_Backward_c || directionType == Img_Both_c) { mdd_array_free(info->bwdClusteredRelationArray); if (info->preKeepPiInTr) { if (info->intermediateBddVars) quantifyVarBddArray = info->intermediateBddVars; else quantifyVarBddArray = array_alloc(mdd_t *, 0); domainVarBddArray = array_join(info->domainVarBddArray, info->quantifyVarBddArray); } else { if (info->newQuantifyBddVars) quantifyVarBddArray = info->newQuantifyBddVars; else quantifyVarBddArray = info->quantifyVarBddArray; domainVarBddArray = info->domainVarBddArray; } info->bwdClusteredRelationArray = ImgClusterRelationArray( info->manager, info->functionData, info->option->trMethod, Img_Backward_c, info->trmOption, relationArray, domainVarBddArray, quantifyVarBddArray, info->rangeVarBddArray, &info->fwdArraySmoothVarBddArray, &info->fwdSmoothVarCubeArray, 0); if (info->preKeepPiInTr) { if (!info->intermediateBddVars) array_free(quantifyVarBddArray); array_free(domainVarBddArray); } } mdd_array_free(relationArray); } /**Function******************************************************************** Synopsis [Minimizes function vector or relation with given constraint.] Description [Minimizes function vector or relation with given constraint.] SideEffects [] ******************************************************************************/ static void MinimizeTransitionFunction(array_t *vector, array_t *relationArray, mdd_t *constrain, Img_MinimizeType minimizeMethod, int printStatus) { int i; bdd_t *relation, *simplifiedRelation, *simplifiedFunc; long sizeConstrain = 0, size = 0; ImgComponent_t *comp; if (bdd_is_tautology(constrain, 1)) return; if (vector) { if (printStatus) { size = ImgVectorBddSize(vector); sizeConstrain = bdd_size(constrain); } arrayForEachItem(ImgComponent_t *, vector, i, comp) { simplifiedFunc = Img_MinimizeImage(comp->func, constrain, minimizeMethod, TRUE); if (printStatus == 2) { (void)fprintf(vis_stdout, "IMG Info: minimized function %d | %ld => %d in component %d\n", bdd_size(comp->func), sizeConstrain, bdd_size(simplifiedFunc), i); } mdd_free(comp->func); comp->func = simplifiedFunc; } if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized function [%ld | %ld => %ld] with %d components\n", size, sizeConstrain, ImgVectorBddSize(vector), array_n(vector)); } } if (relationArray) { if (printStatus) { size = bdd_size_multiple(relationArray); sizeConstrain = bdd_size(constrain); } arrayForEachItem(bdd_t*, relationArray, i, relation) { simplifiedRelation = Img_MinimizeImage(relation, constrain, minimizeMethod, TRUE); if (printStatus == 2) { (void)fprintf(vis_stdout, "IMG Info: minimized relation %d | %ld => %d in component %d\n", bdd_size(relation), sizeConstrain, bdd_size(simplifiedRelation), i); } mdd_free(relation); array_insert(bdd_t *, relationArray, i, simplifiedRelation); } if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized relation [%ld | %ld => %ld] with %d components\n", size, sizeConstrain, bdd_size_multiple(relationArray), array_n(relationArray)); } } } /**Function******************************************************************** Synopsis [Adds dont cares to function vector or relation.] Description [Adds dont cares to function vector or relation.] SideEffects [] ******************************************************************************/ static void AddDontCareToTransitionFunction(array_t *vector, array_t *relationArray, mdd_t *constrain, Img_MinimizeType minimizeMethod, int printStatus) { int i; bdd_t *relation, *simplifiedRelation, *simplifiedFunc; long sizeConstrain = 0, size = 0; ImgComponent_t *comp; if (bdd_is_tautology(constrain, 1)) return; if (vector) { if (printStatus) { size = ImgVectorBddSize(vector); sizeConstrain = bdd_size(constrain); } arrayForEachItem(ImgComponent_t *, vector, i, comp) { simplifiedFunc = Img_AddDontCareToImage(comp->func, constrain, minimizeMethod); if (printStatus == 2) { (void)fprintf(vis_stdout, "IMG Info: minimized function %d | %ld => %d in component %d\n", bdd_size(comp->func), sizeConstrain, bdd_size(simplifiedFunc), i); } mdd_free(comp->func); comp->func = simplifiedFunc; } if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized function [%ld | %ld => %ld] with %d components\n", size, sizeConstrain, ImgVectorBddSize(vector), array_n(vector)); } } if (relationArray) { if (printStatus) { size = bdd_size_multiple(relationArray); sizeConstrain = bdd_size(constrain); } arrayForEachItem(bdd_t*, relationArray, i, relation) { simplifiedRelation = Img_AddDontCareToImage(relation, constrain, minimizeMethod); if (printStatus == 2) { (void)fprintf(vis_stdout, "IMG Info: minimized relation %d | %ld => %d in component %d\n", bdd_size(relation), sizeConstrain, bdd_size(simplifiedRelation), i); } mdd_free(relation); array_insert(bdd_t *, relationArray, i, simplifiedRelation); } if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized relation [%ld | %ld => %ld] with %d components\n", size, sizeConstrain, bdd_size_multiple(relationArray), array_n(relationArray)); } } }