/**CFile*********************************************************************** FileName [imgLinear.c] PackageName [img] Synopsis [Routines for image computation using Linear Arrangement published in TACAS02.] Description [] SeeAlso [] Author [HoonSang Jin] 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" #include "fsm.h" #include "heap.h" static char rcsid[] UNUSED = "$Id: imgLinear.c,v 1.18 2010/04/10 00:37:06 fabio Exp $"; static char linearVarString[] = "TCNI"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ Cluster_t *__clu; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ #define BACKWARD_REDUCTION_RATE 0.5 #define FORWARD_REDUCTION_RATE 0.5 /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static void ImgLinearUpdateVariableArrayWithId(Relation_t *head, int cindex, int id); static int ImgLinearQuantifyVariablesFromConjunct(Relation_t *head, Conjunct_t *conjunct, array_t *smoothVarBddArray, int *bModified); static void ImgLinearConjunctRefine(Relation_t *head, Conjunct_t *conjunct); static void ImgLinearVariableArrayQuit(Relation_t *head); static void ImgLinearConjunctQuit(Conjunct_t *conjunct); static Conjunct_t ** ImgLinearAddConjunctIntoArray(Conjunct_t **array, int *nArray, Conjunct_t *con); static void ImgLinearFindSameSupportConjuncts(Relation_t *head, int from, int to); static void ImgLinearClusterSameSupportSet(Relation_t *head); static void ImgLinearExpandSameSupportSet(Relation_t *head); static int ImgLinearIsSameConjunct(Relation_t *head, Conjunct_t *con1, Conjunct_t *con2); static bdd_t * ImgLinearClusteringSmooth(Relation_t *head, Cluster_t *clu, int **failureHistory, int andExistLimit, int bddLimit); static int ImgLinearClusterUsingHeap(Relation_t *head, double affinityLimit, int andExistLimit, int varLimit, Img_OptimizeType optDir, int rangeFlag, int (*compare_func)(const void *, const void *)); static void ImgLinearPrintTransitionInfo(Relation_t *head); static void ImgLinearComputeLifeTime(Relation_t *head, double *paal, double *patl); static void ImgLinearFreeSmoothArray(array_t *smoothVarBddArray); static void ImgLinearPrintMatrixFull(Relation_t *head, int matrixIndex); static void ImgLinearPrintMatrix(Relation_t *head); static void ImgLinearCAPOReadVariableOrder(Relation_t *head, char *baseName, int includeNS); static void ImgLinearCAPOInterfaceVariablePl(Relation_t *head, char *baseName, int includeNS); static void ImgLinearCAPOInterfaceVariableScl(Relation_t *head, char *baseName); static void ImgLinearCAPOInterfaceVariableNet(Relation_t *head, char *baseName, int includeNS); static void ImgLinearCAPOInterfaceVariableNodes(Relation_t *head, char *baseName, int includeNS); static void ImgLinearVariableOrder(Relation_t *head, char *baseName, int includeNS); static void ImgLinearCAPOReadConjunctOrder(Relation_t *head, char *baseName); static int ImgLinearCAPORun(char *capoExe, char *baseName, int brief); static void ImgLinearCAPOInterfaceAux(Relation_t *head, char *baseName); static void ImgLinearCAPOInterfaceConjunctPl(Relation_t *head, char *baseName); static void ImgLinearCAPOInterfaceConjunctScl(Relation_t *head, char *baseName); static void ImgLinearCAPOInterfaceConjunctNet(Relation_t *head, char *baseName); static void ImgLinearCAPOInterfaceConjunctNodes(Relation_t *head, char *baseName); static void ImgLinearConjunctionOrder(Relation_t *head, char *baseName, int refineFlag); static void ImgLinearConjunctOrderMain(Relation_t *head, int bRefineConjunctOrder); static void ImgLinearPrintDebugInfo(Relation_t *head); static void ImgLinearPrintVariableProfile(Relation_t *head, char *baseName); static void ImgLinearInsertClusterCandidate(Relation_t *head, int from, int to, int nDead, int nVar, double affinityLimit); static void ImgLinearInsertPairClusterCandidate(Relation_t *head, int from, double affinityLimit, int varLimit, int rangeFlag); static void ImgLinearBuildInitialCandidate(Relation_t *head, double affinityLimit, int varLimit, int rangeFlag, int (*compare_func)(const void *, const void *)); static bdd_t * ImgLinearClusteringPairSmooth(Relation_t *head, Cluster_t *clu, int **failureHistory, int andExistLimit, int bddLimit); static void ImgLinearVariableArrayInit(Relation_t *head); static void ImgLinearSetEffectiveNumberOfStateVariable(Relation_t *head, int *rangeId, int *domainId, int *existStateVariable) ; static void ImgLinearVariableLifeQuit(VarLife_t *var); static void ImgLinearAddNextStateCase(Relation_t *head); static void ImgLinearAddSingletonCase(Relation_t *head); static int ImgLinearCompareDeadAffinityLive(const void *c1, const void *c2); static int ImgLinearCompareDeadLiveAffinity(const void *c1, const void *c2); static int ImgLinearCompareAffinityDeadLive(const void *c1, const void *c2); static int ImgLinearCompareLiveAffinityDead(const void *c1, const void *c2); static int ImgLinearHeapCompareDeadAffinityLive(const void *c1, const void *c2); static int ImgLinearHeapCompareDeadLiveAffinity(const void *c1, const void *c2); static int ImgLinearHeapCompareAffinityDeadLive(const void *c1, const void *c2); static int ImgLinearHeapCompareLiveAffinityDead(const void *c1, const void *c2); static int ImgLinearCompareVarIndex(const void *c1, const void *c2); static int ImgLinearCompareVarSize(const void *c1, const void *c2); static int ImgLinearCompareVarEffFromSmall(const void *c1, const void *c2); static int ImgLinearCompareVarEffFromLarge(const void *c1, const void *c2); static int ImgLinearCompareConjunctDummy(const void *c1, const void *c2); static int ImgLinearCompareConjunctIndex(const void *c1, const void *c2); static int ImgLinearCompareConjunctSize(const void *c1, const void *c2); static int ImgLinearCompareConjunctRangeMinusDomain(const void *c1, const void *c2); static int ImgLinearCompareVarId(const void *c1, const void *c2); static int ImgCheckRangeTestAndOverapproximate(Relation_t *head); static void ImgCountOnsetDisjunctiveArray(Relation_t *head); static int linearCheckRange(const void *tc); static void ImgLinearConjunctArrayRefine(Relation_t *head); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ void ImgLinearConjunctOrderMainCC(Relation_t *head, int refineFlag); int ImgLinearClustering(Relation_t *head, Img_OptimizeType optDir); int ImgLinearPropagateConstant(Relation_t *head, int nextStateFlag); int ImgLinearOptimizeStateVariables(Relation_t *head, Img_OptimizeType optDir); void ImgLinearExtractNextStateCase(Relation_t *head); void ImgLinearExtractSingletonCase(Relation_t *head); /*void ImgLinearClusterRelationArray(mdd_manager *mgr, ImgFunctionData_t *functionData, array_t *relationArray, Img_DirectionType direction, array_t **clusteredRelationArrayPtr, array_t **arraySmoothVarBddArrayPtr, array_t **optClusteredRelationArrayPtr, array_t **optArraySmoothVarBddArrayPtr, ImgTrmOption_t *option); */ void ImgLinearConnectedComponent(Relation_t *head); void ImgLinearBuildConjunctArrayWithQuotientCC(Relation_t *head); void ImgLinearFindConnectedComponent(Relation_t *head, Conjunct_t *conjunct, int cc_index); void ImgLinearAddConjunctIntoClusterArray(Conjunct_t *base, Conjunct_t *con); /**Function******************************************************************** Synopsis [Cluster fine grain transition relation] Description [First the linear arrangement of transition relation that minimze max cut is generated and the iterative clustering is applied on it.] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearClusterRelationArray(mdd_manager *mgr, ImgFunctionData_t *functionData, array_t *relationArray, Img_DirectionType direction, array_t **clusteredRelationArrayPtr, array_t **arraySmoothVarBddArrayPtr, array_t **optClusteredRelationArrayPtr, array_t **optArraySmoothVarBddArrayPtr, ImgTrmOption_t *option) { Img_OptimizeType optDir; int bGroupStateVariable; int bOrderVariable; int includeCS; int includeNS; int quantifyCS; array_t *initRelationArray; int bOptimize; Relation_t *head; bdd_t **smoothCubeArr, **optSmoothCubeArr; array_t *optRelationArr, *optSmoothVarBddArr; array_t *relationArr, *smoothVarBddArr; if(option->linearComputeRange) { option->linearIncludeCS = 0; option->linearIncludeNS = 0; option->linearQuantifyCS = 1; } optRelationArr = relationArr = 0; optSmoothVarBddArr = smoothVarBddArr = 0; includeCS = option->linearIncludeCS; includeNS = option->linearIncludeNS; quantifyCS = option->linearQuantifyCS; if(option->linearFineGrainFlag) includeNS = 1; optDir = option->linearOptimize; bOrderVariable = option->linearOrderVariable; bGroupStateVariable = option->linearGroupStateVariable; head = ImgLinearRelationInit(mgr, relationArray, functionData->domainBddVars, functionData->rangeBddVars, functionData->quantifyBddVars, option); if(head->verbosity >= 5) ImgLinearPrintDebugInfo(head); ImgLinearOptimizeAll(head, Opt_None, 0); ImgLinearRefineRelation(head); initRelationArray = ImgLinearExtractRelationArrayT(head); bOptimize = 0; ImgLinearPrintMatrix(head); if(bOrderVariable) ImgLinearVariableOrder(head, "VarOrder", !bGroupStateVariable); if((direction==0) || (direction==2)) { ImgLinearPrintMatrix(head); bOptimize |= ImgLinearOptimizeAll(head, optDir, 0); ImgLinearRefineRelation(head); ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0); ImgLinearConjunctOrderMainCC(head, 0); ImgLinearPrintMatrix(head); bOptimize |= ImgLinearClustering(head, optDir); ImgLinearRefineRelation(head); ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0); ImgLinearPrintTransitionInfo(head); ImgLinearPrintMatrix(head); ImgLinearPrintMatrixFull(head, 2); if(bOptimize) { optRelationArr = ImgLinearExtractRelationArrayT(head); optSmoothCubeArr = ALLOC(bdd_t *, head->nSize+1); optSmoothVarBddArr = ImgLinearMakeSmoothVarBdd(head, optSmoothCubeArr); } else { optRelationArr = ImgLinearExtractRelationArrayT(head); optSmoothCubeArr = ALLOC(bdd_t *, head->nSize+1); optSmoothVarBddArr = ImgLinearMakeSmoothVarBdd(head, optSmoothCubeArr); relationArr = 0; smoothVarBddArr = 0; } ImgLinearPrintDebugInfo(head); ImgLinearRelationQuit(head); if(bOptimize) { fprintf(vis_stdout, "Get Schedules without optimization\n"); head = ImgLinearRelationInit(mgr, initRelationArray, functionData->domainBddVars, functionData->rangeBddVars, functionData->quantifyBddVars, option); ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0); ImgLinearConjunctOrderMainCC(head, 0); if(head->verbosity >= 5) ImgLinearPrintMatrix(head); ImgLinearClustering(head, Opt_None); relationArr = ImgLinearExtractRelationArrayT(head); smoothCubeArr = ALLOC(bdd_t *, head->nSize+1); smoothVarBddArr = ImgLinearMakeSmoothVarBdd(head, smoothCubeArr); ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0); ImgLinearPrintDebugInfo(head); ImgLinearPrintTransitionInfo(head); ImgLinearRelationQuit(head); } if(optClusteredRelationArrayPtr) *optClusteredRelationArrayPtr = optRelationArr; else mdd_array_free(optRelationArr); if(optArraySmoothVarBddArrayPtr) *optArraySmoothVarBddArrayPtr = optSmoothVarBddArr; else if(optSmoothVarBddArr) ImgLinearFreeSmoothArray(optSmoothVarBddArr); if(clusteredRelationArrayPtr) *clusteredRelationArrayPtr = relationArr; else mdd_array_free(relationArr); if(arraySmoothVarBddArrayPtr) *arraySmoothVarBddArrayPtr = smoothVarBddArr; else if(smoothVarBddArr) ImgLinearFreeSmoothArray(smoothVarBddArr); } if((direction==1) || (direction==2)) { } } /**Function******************************************************************** Synopsis [Initialize the data structure for linear arrangement and clustering.] Description [Build initial data structure] SideEffects [] SeeAlso [] ******************************************************************************/ Relation_t * ImgLinearRelationInit(mdd_manager *mgr, array_t *relationArray, array_t *domainBddVars, array_t *rangeBddVars, array_t *quantifyBddVars, ImgTrmOption_t *option) { Relation_t *head; Conjunct_t *conjunct, **conjunctArray; bdd_t *varBdd; int *domain2range, *range2domain; int *varArrayMap, *varType; bdd_t **constantCase, *relation; int i, j, id, tid, nSize; int *supList, listSize; char *flagValue; int *quantifyVars, nQuantify, *visited; head = ALLOC(Relation_t, 1); memset(head, 0, sizeof(Relation_t)); head->mgr = mgr; head->nVar = bdd_num_vars(head->mgr); head->bddLimit = option->clusterSize; head->verbosity = option->verbosity; flagValue = Cmd_FlagReadByName("linear_verbosity"); if(flagValue) { head->verbosity += atoi(flagValue); } head->includeCS = option->linearIncludeCS; head->includeNS = option->linearIncludeNS; head->quantifyCS = option->linearQuantifyCS; head->computeRange = option->linearComputeRange; head->nInitRange = 0; head->nInitDomain = 0; head->nInitQuantify = 0; head->nEffRange = 0; head->nEffDomain = 0; head->nEffQuantify = 0; head->clusterArray = 0; head->nClusterArray = 0; head->nVarArray = 0; head->varArray = 0; head->nSingletonArray = 0; head->singletonArray = 0; head->nNextStateArray = 0; head->nextStateArray = 0; domain2range = ALLOC(int, head->nVar); head->domain2range = domain2range; memset(domain2range, -1, sizeof(int)*head->nVar); range2domain = ALLOC(int, head->nVar); head->range2domain = range2domain; memset(range2domain, -1, sizeof(int)*head->nVar); varType = ALLOC(int, head->nVar); head->varType = varType; memset(varType, 0, sizeof(int)*head->nVar); head->nRange = array_n(rangeBddVars); head->nDomain = array_n(domainBddVars); head->domainVars = ALLOC(int, head->nDomain); head->rangeVars = ALLOC(int, head->nRange); for(i=0; inDomain; i++) { varBdd = array_fetch(bdd_t *, domainBddVars, i); id = (int)bdd_top_var_id(varBdd); head->domainVars[i] = id; varType[id] = 1; varBdd = array_fetch(bdd_t *, rangeBddVars, i); tid = (int)bdd_top_var_id(varBdd); head->rangeVars[i] = tid; varType[tid] = 2; domain2range[id] = tid; range2domain[tid] = id; } head->quantifyVars = quantifyVars = ALLOC(int, head->nVar); memset(quantifyVars, 0, sizeof(int)*head->nVar); for(nQuantify=0, i=0; inVar); head->varArrayMap = varArrayMap; memset(varArrayMap, -1, sizeof(int)*head->nVar); constantCase = ALLOC(bdd_t *, head->nVar); head->constantCase = constantCase; memset(constantCase, 0, sizeof(bdd_t *)*head->nVar); nSize = array_n(relationArray); conjunctArray = ALLOC(Conjunct_t *, nSize+1); head->nSize = nSize; head->conjunctArray = conjunctArray; visited = ALLOC(int, head->nVar); memset(visited, 0, sizeof(int)*head->nVar); for(i=0; iindex = i; relation = array_fetch(bdd_t *, relationArray, i); conjunct->relation = mdd_dup(relation); supList = ImgLinearGetSupportBddId(head->mgr, relation, &listSize); conjunct->supList = supList; conjunct->nSize = listSize; for(j=0; jnDomain++; else if(varType[id] == 2) conjunct->nRange++; else if(varType[id] == 3) conjunct->nQuantify++; else if(visited[id] == 0) { quantifyVars[nQuantify++] = id; visited[id] = 1; } } conjunctArray[i] = conjunct; } conjunctArray[i] = 0; head->nQuantify= nQuantify; free(visited); ImgLinearVariableArrayInit(head); return(head); } /**Function******************************************************************** Synopsis [Find support varaibles of bdd] Description [Find support varaibles of bdd] SideEffects [] SeeAlso [] ******************************************************************************/ int * ImgLinearGetSupportBddId(mdd_manager *mgr, bdd_t *f, int *nSize) { var_set_t *vset; array_t *bvar_list; int *supList, i, size; bvar_list = mdd_ret_bvar_list(mgr); vset = bdd_get_support(f); size = 0; supList = ALLOC(int, size+1); supList[0] = -1; for(i=0; inSize+1); for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; relationArray[i] = bdd_dup(conjunct->relation); } relationArray[i] = 0; return(relationArray); } /**Function******************************************************************** Synopsis [Create relation array for image computation from Relation_t data structure] Description [Create relation array for image computation from Relation_t data structure] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * ImgLinearExtractRelationArrayT(Relation_t *head) { int i; array_t *relationArray; Conjunct_t *conjunct; relationArray = array_alloc(bdd_t *, head->nSize); for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; array_insert_last(bdd_t *, relationArray, bdd_dup(conjunct->relation)); } return(relationArray); } /**Function******************************************************************** Synopsis [Function for optimizing state varaibles] Description [If the next or current state variables are eleminated after applying clustering and constant propagation then delete corresponding state variable from transition relation.] SideEffects [] SeeAlso [] ******************************************************************************/ int ImgLinearOptimizeAll(Relation_t *head, Img_OptimizeType optDir, int constantNSOpt) { int bOptimize; bOptimize = 0; bOptimize |= ImgLinearPropagateConstant(head, constantNSOpt); bOptimize |= ImgLinearOptimizeStateVariables(head, optDir); ImgLinearOptimizeInternalVariables(head); return(bOptimize); } /**Function******************************************************************** Synopsis [Propagate the constant to simply the transition relation] Description [Propagate the constant to simply the transition relation] SideEffects [] SeeAlso [] ******************************************************************************/ int ImgLinearPropagateConstant(Relation_t *head, int nextStateFlag) { int nSize, i, j; int *supList; Conjunct_t **conjunctArray; Conjunct_t *conjunct; mdd_manager *mgr; bdd_t **constantCase; bdd_t *relation, *simpleRelation; int nConstantCase; int bOptimize; int id, cid, index; int *varType; int size; bOptimize = 0; mgr = head->mgr; constantCase = head->constantCase; varType = head->varType; conjunctArray = head->conjunctArray; nSize = head->nSize; nConstantCase = 0; for(index=0, i=0; irelation == 0) continue; if(conjunct->nSize == 1) { id = conjunct->supList[0]; if(varType[id] == 2) { if(nextStateFlag) { cid = head->range2domain[id]; if(constantCase[cid] == 0) { constantCase[cid] = bdd_dup(conjunct->relation); if(head->verbosity >= 4) fprintf(vis_stdout, "Detect Constant Case %3d(%c)\n", cid, linearVarString[varType[cid]]); nConstantCase++; } } continue; } else { if(constantCase[id] == 0) { constantCase[id] = bdd_dup(conjunct->relation); if(head->verbosity >= 4) fprintf(vis_stdout, "Detect Constant Case %3d(%c)\n", id, linearVarString[varType[id]]); nConstantCase++; } continue; } } } if(nConstantCase > 0) { for(i=0; inSize; i++) { conjunct = conjunctArray[i]; if(conjunct == 0) continue; if(conjunct->relation == 0) continue; relation = conjunct->relation; size = conjunct->nSize; supList = conjunct->supList; for(j=0; jrelation); conjunct->relation = simpleRelation; relation = conjunct->relation; conjunct->bModified = 1; head->bModified = 1; head->bRefineVarArray = 1; if(head->verbosity >= 2) fprintf(vis_stdout, "Constant propagation is applied %3d(%c) to %3d'th relation\n", id, linearVarString[varType[id]], i); } ImgLinearConjunctRefine(head, conjunct); } } return(bOptimize); } /**Function******************************************************************** Synopsis [Remove corresponding current (next) state variables if the next (current state variables are eleminated aftetr clustering] Description [Remove corresponding current (next) state variables if the next (current state variables are eleminated aftetr clustering] SideEffects [] SeeAlso [] ******************************************************************************/ int ImgLinearOptimizeStateVariables(Relation_t *head, Img_OptimizeType optDir) { int *rangeId, *domainId, *existStateVar; int *domain2range; int *range2domain; bdd_t *oneBdd, *varBdd; VarLife_t **varArray, *var; array_t *smoothVarBddArray; Conjunct_t *conjunct; int i, id; int bOptimize; int rangeBound, domainBound; int nRangeReduced, nDomainReduced; if(optDir == Opt_None) return(0); id = 0; ImgLinearVariableArrayInit(head); bOptimize = 0; rangeId = ALLOC(int, head->nRange+1); memset(rangeId, 0, sizeof(int)*(head->nRange+1)); domainId = ALLOC(int, head->nDomain+1); memset(domainId, 0, sizeof(int)*(head->nDomain+1)); existStateVar = ALLOC(int, head->nVar); memset(existStateVar, 0, sizeof(int)*head->nVar); ImgLinearSetEffectiveNumberOfStateVariable(head, rangeId, domainId, existStateVar); rangeBound = (int)((double)head->nInitRange * BACKWARD_REDUCTION_RATE); domainBound = (int)((double)head->nInitDomain * FORWARD_REDUCTION_RATE); if(head->nEffDomain < domainBound) { if(optDir == Opt_Both) optDir = Opt_NS; else if(optDir == Opt_CS) optDir = Opt_None; } if(head->nEffRange < rangeBound) { if(optDir == Opt_Both) optDir = Opt_CS; else if(optDir == Opt_NS) optDir = Opt_None; } if(optDir == Opt_None) return(0); oneBdd = bdd_one(head->mgr); domain2range = head->domain2range; range2domain = head->range2domain; varArray = head->varArray; if(optDir == Opt_Both || optDir == Opt_CS) { smoothVarBddArray = array_alloc(bdd_t *, 0); nDomainReduced = 0; for(i=0; inEffDomain; i++) { id = domainId[i]; if(existStateVar[domain2range[id]]) continue; var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0; if(var) { if(head->nEffDomain-nDomainReduced < domainBound) break; if(var->nSize-head->includeCS == 1) { varBdd = bdd_get_variable(head->mgr, id); array_insert_last(bdd_t *, smoothVarBddArray, varBdd); nDomainReduced++; } } } if(array_n(smoothVarBddArray)) { for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; if(conjunct->nDomain == 0) continue; if(ImgLinearQuantifyVariablesFromConjunct( head, conjunct, smoothVarBddArray, &bOptimize)) { fprintf(vis_stdout, "NOTICE : CS %3d quantified from %d'th relation\n", id, i); } } } mdd_array_free(smoothVarBddArray); } if(optDir == Opt_Both || optDir == Opt_NS) { smoothVarBddArray = array_alloc(bdd_t *, 0); nRangeReduced = 0; for(i=0; inEffRange; i++) { id = rangeId[i]; if(existStateVar[range2domain[id]]) continue; var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0; if(var) { if(head->nEffRange-nRangeReduced < rangeBound) break; if(var->nSize-head->includeNS == 1) { varBdd = bdd_get_variable(head->mgr, id); array_insert_last(bdd_t *, smoothVarBddArray, varBdd); nRangeReduced++; } } } if(array_n(smoothVarBddArray)) { for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; if(conjunct->nRange == 0) continue; if(ImgLinearQuantifyVariablesFromConjunct( head, conjunct, smoothVarBddArray, &bOptimize)) { fprintf(vis_stdout, "NOTICE : NS %3d quantified from %d'th relation\n", id, i); } } } mdd_array_free(smoothVarBddArray); } bdd_free(oneBdd); free(rangeId); free(domainId); free(existStateVar); ImgLinearVariableArrayInit(head); return(bOptimize); } /**Function******************************************************************** Synopsis [Remove intermediate variables after propagating constant.] Description [Remove intermediate variables after propagating constant.] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearOptimizeInternalVariables(Relation_t *head) { bdd_t *oneBdd, *varBdd; VarLife_t **varArray, *var; Conjunct_t **conjunctArray; array_t *smoothVarBddArray; int *varType; int i, bModified; oneBdd = bdd_one(head->mgr); while(1) { bModified = 0; varArray = head->varArray; varType = head->varType; conjunctArray = head->conjunctArray; for(i=0; inVarArray; i++) { var = head->varArray[i]; if(varType[var->id] == 2) continue; if(varType[var->id] == 1 && head->quantifyCS == 0) continue; if(var->from == var->to) { if(conjunctArray[var->from] == 0) continue; varBdd = bdd_get_variable(head->mgr, var->id); smoothVarBddArray = array_alloc(bdd_t *, 0); array_insert_last(bdd_t *, smoothVarBddArray, varBdd); ImgLinearQuantifyVariablesFromConjunct( head, head->conjunctArray[var->from], smoothVarBddArray, &bModified); mdd_array_free(smoothVarBddArray); } } if(bModified == 0) break; ImgLinearVariableArrayInit(head); } bdd_free(oneBdd); return; } /**Function******************************************************************** Synopsis [Refine transition relation.] Description [Clean up the Relation_t data structure after applying linear arrangement of transition relation] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearRefineRelation(Relation_t *head) { ImgLinearConjunctArrayRefine(head); ImgLinearVariableArrayInit(head); } /**Function******************************************************************** Synopsis [Order the fine grain transition relation.] Description [First find the connected component and apply ordering procedure for each component.] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearConjunctOrderMainCC(Relation_t *head, int refineFlag) { Conjunct_t **connectedArray; int i, index; char baseName[1024]; ImgLinearPrintMatrix(head); ImgLinearExtractNextStateCase(head); ImgLinearClusterSameSupportSet(head); ImgLinearRefineRelation(head); ImgLinearExtractSingletonCase(head); ImgLinearRefineRelation(head); ImgLinearConnectedComponent(head); for(i=0; inConnectedComponent; i++) { connectedArray = head->connectedComponent[i]; for(index=0; (long)(connectedArray[index])>0; index++); head->conjunctArray = connectedArray; head->nSize = index; head->bModified = 1; head->bRefineVarArray = 1; qsort(head->conjunctArray, head->nSize, sizeof(Conjunct_t *), ImgLinearCompareConjunctSize); ImgLinearVariableArrayInit(head); ImgLinearConjunctOrderMain(head, 0); fprintf(stdout, "NOTICE : %d'th connected component\n", i); head->connectedComponent[i] = head->conjunctArray; head->conjunctArray = 0; } ImgLinearBuildConjunctArrayWithQuotientCC(head); ImgLinearAddSingletonCase(head); ImgLinearAddNextStateCase(head); ImgLinearExpandSameSupportSet(head); ImgLinearRefineRelation(head); ImgLinearRefineRelation(head); ImgLinearPrintMatrix(head); sprintf(baseName, "profile"); ImgLinearPrintVariableProfile(head, baseName); ImgLinearPrintMatrixFull(head, 2); } /**Function******************************************************************** Synopsis [Order the each connected component] Description [The new Relation_t is created for each connected component] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearBuildConjunctArrayWithQuotientCC(Relation_t *head) { Conjunct_t *conjunct, *tConjunct; Conjunct_t **connectedArray; Conjunct_t **conjunctArray; Conjunct_t **newConjunctArray; st_table *table; int i, j, k, l; int index, id, size; int *varType, *supList; st_generator *gen; char baseName[1024]; if(head->nConnectedComponent == 1) { size = 0; newConjunctArray = ALLOC(Conjunct_t *, size+1); connectedArray = head->connectedComponent[0]; for(j=0; (long)(connectedArray[j])>0; j++) { tConjunct = connectedArray[j]; newConjunctArray[size++] = tConjunct; newConjunctArray = REALLOC(Conjunct_t *, newConjunctArray, size+1); } free(head->conjunctArray); head->nSize = size; head->conjunctArray = newConjunctArray; head->bModified = 1; head->bRefineVarArray = 1; ImgLinearRefineRelation(head); return; } head->includeCS = 1; head->includeNS = 1; varType = head->varType; conjunctArray = ALLOC(Conjunct_t *, head->nConnectedComponent); for(i=0; inConnectedComponent; i++) { connectedArray = head->connectedComponent[i]; table = st_init_table(st_ptrcmp, st_ptrhash); for(j=0; (long)(connectedArray[j])>0; j++) { conjunct = connectedArray[j]; size = conjunct->nSize; supList = conjunct->supList; for(k=0; knCluster; l++) { tConjunct = conjunct->clusterArray[l]; size = tConjunct->nSize; supList = tConjunct->supList; for(k=0; kindex = i; conjunct->dummy = (long)connectedArray; supList = ALLOC(int, table->num_entries); index = 0; st_foreach_item(table, gen, &id, &id) { if(varType[id] == 1) conjunct->nDomain++; else if(varType[id] == 2) conjunct->nRange++; else if(varType[id] == 3) conjunct->nQuantify++; supList[index++] = id; } conjunct->supList = supList; conjunct->nSize = index; conjunctArray[i] = conjunct; conjunct->index = i; conjunct->relation = bdd_zero(head->mgr); } head->nSize = head->nConnectedComponent; head->conjunctArray = conjunctArray; head->bRefineVarArray = 1; ImgLinearVariableArrayInit(head); sprintf(baseName, "TopCon"); ImgLinearCAPOInterfaceConjunctNodes(head, baseName); ImgLinearCAPOInterfaceConjunctNet(head, baseName); ImgLinearCAPOInterfaceConjunctScl(head, baseName); ImgLinearCAPOInterfaceConjunctPl(head, baseName); ImgLinearCAPOInterfaceAux(head, baseName); ImgLinearCAPORun("MetaPlacer", baseName, 0); ImgLinearCAPOReadConjunctOrder(head, baseName); size = 0; newConjunctArray = ALLOC(Conjunct_t *, size+1); conjunctArray = head->conjunctArray; for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; connectedArray = (Conjunct_t **)conjunct->dummy; for(j=0; (long)(connectedArray[j])>0; j++) { tConjunct = connectedArray[j]; newConjunctArray[size++] = tConjunct; newConjunctArray = REALLOC(Conjunct_t *, newConjunctArray, size+1); } ImgLinearConjunctQuit(conjunct); } free(conjunctArray); head->conjunctArray = newConjunctArray; head->nSize = size; head->bModified = 1; head->bRefineVarArray = 1; ImgLinearRefineRelation(head); } /**Function******************************************************************** Synopsis [Find the connected component from fine grain transition relation] Description [Find the connected component from fine grain transition relation] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearConnectedComponent(Relation_t *head) { Conjunct_t *conjunct; Conjunct_t **connectedArray; int i, j, index, cc_index; int pre_index, pre_cc_index; ImgLinearVariableArrayInit(head); for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; conjunct->dummy = 0; } cc_index = 0; for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; if(conjunct->dummy) continue; cc_index++; ImgLinearFindConnectedComponent(head, conjunct, cc_index); } qsort(head->conjunctArray, head->nSize, sizeof(Conjunct_t *), ImgLinearCompareConjunctDummy); head->nConnectedComponent = 0; pre_index = 0; pre_cc_index = 1; for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; if(conjunct->dummy != pre_cc_index) { if((i-pre_index) == 1) { /** singleton case **/ head->singletonArray = ImgLinearAddConjunctIntoArray( head->singletonArray, &(head->nSingletonArray), head->conjunctArray[i-1]); } else { /** connected component case **/ if(head->nConnectedComponent) head->connectedComponent = REALLOC(Conjunct_t **, head->connectedComponent, head->nConnectedComponent+1); else head->connectedComponent = ALLOC(Conjunct_t **, head->nConnectedComponent+1); connectedArray = ALLOC(Conjunct_t *, (i-pre_index+2)); head->connectedComponent[head->nConnectedComponent++] = connectedArray; for(index=0, j=pre_index; jconjunctArray[j]; connectedArray[index] = 0; } pre_cc_index = conjunct->dummy; pre_index = i; } } if((i-pre_index) == 1) { /** singleton case **/ head->singletonArray = ImgLinearAddConjunctIntoArray( head->singletonArray, &(head->nSingletonArray), head->conjunctArray[i-1]); } else { /** connected component case **/ if(head->nConnectedComponent) head->connectedComponent = REALLOC(Conjunct_t **, head->connectedComponent, head->nConnectedComponent+1); else head->connectedComponent = ALLOC(Conjunct_t **, head->nConnectedComponent+1); connectedArray = ALLOC(Conjunct_t *, (i-pre_index+2)); head->connectedComponent[head->nConnectedComponent++] = connectedArray; for(index=0, j=pre_index; jconjunctArray[j]; connectedArray[index] = 0; } free(head->conjunctArray); } /**Function******************************************************************** Synopsis [Find the connected component from fine grain transition relation] Description [Find the connected component from fine grain transition relation] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearFindConnectedComponent(Relation_t *head, Conjunct_t *conjunct, int cc_index) { VarLife_t *var; int *supList; int id, size; int index, i, j; int *relArr; Conjunct_t *tConjunct; if(conjunct->dummy) return; supList = conjunct->supList; size = conjunct->nSize; conjunct->dummy = cc_index; for(i=0; ivarArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0; if(!var) continue; relArr = var->relArr; for(j=0; jnSize; j++) { index = relArr[j]; if(index == MAXINT) continue; if(index == MAXINT-1) continue; tConjunct = head->conjunctArray[index]; if(tConjunct->dummy) continue; ImgLinearFindConnectedComponent(head, tConjunct, cc_index); } } } /**Function******************************************************************** Synopsis [Extract the relation contains only one next state varaible] Description [Extract the relation contains only one next state varaible] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearExtractSingletonCase(Relation_t *head) { int i, j, k, id, index; VarLife_t **varArray, *var; int nSingleton; int *supList, *varType; Conjunct_t *conjunct, **newSingletonArray; int *singletonArray; varType = head->varType; varArray = head->varArray; nSingleton = 0; singletonArray = ALLOC(int , nSingleton+1); for(i=0; inVarArray; i++) { var = varArray[i]; if(var->stateVar == 2) continue; if(var->stateVar == 1) { if(var->nSize - head->includeCS > 1) continue; } else { if(var->nSize > 1) continue; } for(j=0; jnSize; j++) { if(var->relArr[j] == MAXINT) continue; if(var->relArr[j] == MAXINT-1) continue; singletonArray[nSingleton++] = var->relArr[j]; singletonArray = REALLOC(int , singletonArray, nSingleton+1); } } for(i=0; iconjunctArray[singletonArray[i]]; conjunct->bSingleton = 1; } for(i=0; iconjunctArray[singletonArray[i]]; if(conjunct->nRange == conjunct->nSize-conjunct->nRange && conjunct->nSize-conjunct->nRange != 1) { conjunct->bSingleton = 0; continue; } supList = conjunct->supList; for(j=0; jnSize; j++) { id = supList[j]; if(varType[id] == 2) continue; var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0; if(!var) continue; if(var->stateVar == 1) { if(var->nSize - head->includeCS == 1) continue; } else { if(var->nSize == 1) continue; } for(k=0; knSize; k++) { index = var->relArr[k]; if(index == MAXINT) continue; if(index == MAXINT-1) continue; (head->conjunctArray[index])->bSingleton = 0; } } } newSingletonArray = ALLOC(Conjunct_t *, nSingleton); for(index=0, i=0; iconjunctArray[singletonArray[i]]; if(conjunct == 0) continue; if(conjunct->bSingleton) { newSingletonArray[index++] = conjunct; head->conjunctArray[singletonArray[i]] = 0; } } head->nSingletonArray = index; free(singletonArray); qsort(newSingletonArray, head->nSingletonArray, sizeof(Conjunct_t *), ImgLinearCompareConjunctRangeMinusDomain); head->singletonArray = newSingletonArray; if(head->nSingletonArray) { head->bModified = 1; head->bRefineVarArray = 1; } } /**Function******************************************************************** Synopsis [Add Conjunct into Cluster Array] Description [Add Conjunct into Cluster Array] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearAddConjunctIntoClusterArray(Conjunct_t *base, Conjunct_t *con) { if(base->clusterArray == 0) { base->clusterArray = ALLOC(Conjunct_t *, base->nCluster+1); base->clusterArray[base->nCluster++] = con; } else { base->clusterArray = REALLOC(Conjunct_t *, base->clusterArray, base->nCluster+1); base->clusterArray[base->nCluster++] = con; } base->bClustered = 1; } /**Function******************************************************************** Synopsis [Extract the relation that contains next state varaibles only] Description [Extract the relation that contains next state varaibles only] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearExtractNextStateCase(Relation_t *head) { int i, index, flag; Conjunct_t *conjunct; Conjunct_t **nextStateArray; index = 0; flag = 1; nextStateArray = ALLOC(Conjunct_t *, index+1); for(index=0, i=head->nSize-1; i>=0; i--) { conjunct = head->conjunctArray[i]; if(conjunct == 0) continue; if(conjunct->nSize == conjunct->nRange && flag == 0) { nextStateArray[index++] = conjunct; nextStateArray = REALLOC(Conjunct_t *, nextStateArray, index+1); head->conjunctArray[i] = 0; head->bModified = 1; } if(conjunct->nSize != conjunct->nRange) flag = 0; } head->nextStateArray = nextStateArray; head->nNextStateArray = index; ImgLinearRefineRelation(head); } /**Function******************************************************************** Synopsis [Free Relation_t data structure] Description [Free Relation_t data structure] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearRelationQuit(Relation_t *head) { int i; Conjunct_t *conjunct; if(head->varArray) ImgLinearVariableArrayQuit(head); if(head->rangeVars) free(head->rangeVars); if(head->domainVars) free(head->domainVars); if(head->quantifyVars) free(head->quantifyVars); if(head->varType) free(head->varType); if(head->varArrayMap) free(head->varArrayMap); if(head->singletonArray) free(head->singletonArray); if(head->nextStateArray) free(head->nextStateArray); if(head->constantCase) { for(i=0; inVar; i++) if(head->constantCase[i]) bdd_free(head->constantCase[i]); } for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; ImgLinearConjunctQuit(conjunct); } free(head); } /**Function******************************************************************** Synopsis [Apply clustering iteratively] Description [Apply clustering iteratively] SideEffects [] SeeAlso [] ******************************************************************************/ int ImgLinearClusteringIteratively(Relation_t *head, double affinityLimit, int andExistLimit, int varLimit, int includeZeroGain, int useFailureHistory, Img_OptimizeType optDir, int (*compare_func)(const void *, const void *)) { int bddLimit, gainLimit; int clusterLimit; int bOptimize; if(head->nSize < 2) return(0); bOptimize = 0; bddLimit = head->bddLimit; gainLimit = 50; while(1) { if(head->nSize < 50)clusterLimit = head->nSize/2; else clusterLimit = head->nSize/3+1; if(clusterLimit > 50) clusterLimit = 50; /** clusterLimit = head->nSize/5; if(clusterLimit < 1) clusterLimit = 3; **/ ImgLinearClusteringByConstraints(head, includeZeroGain, varLimit, clusterLimit, gainLimit, affinityLimit, andExistLimit, bddLimit, useFailureHistory, compare_func); if(head->bModified) { ImgLinearRefineRelation(head); bOptimize |= ImgLinearOptimizeAll(head, optDir, 0); } else break; } return(bOptimize); } /**Function******************************************************************** Synopsis [Apply clustering with given priority function] Description [Apply clustering with given priority function] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearClusteringByConstraints(Relation_t *head, int includeZeroGain, int varLimit, int clusterLimit, int gainLimit, double affinityLimit, int andExistLimit, int bddLimit, int useFailureHistory, int (*compare_func)(const void *, const void *)) { int size, begin, end; int **nDead, **nVar, **nFailure; int *dirtyBit; int i, j, k, l, index; int start, preGain; int nClusterArray; VarLife_t **varArray, *var; Cluster_t **clusterArray, *clu; Conjunct_t *conjunct; bdd_t *clusteredRelation; int fail_flag; int from, to, splitable; varArray = head->varArray; size = head->nSize; nDead = ALLOC(int *, size); nVar = ALLOC(int *, size); nFailure = 0; if(useFailureHistory) nFailure = ALLOC(int *, size); for(i=0; inVarArray; l++) { var = varArray[l]; begin = var->from; end = var->to; if(var->stateVar == 1) begin = -1; else if(var->stateVar == 2) end = size; for(i=0; i<=begin; i++) for(j=end; jeffTo; i++) { if(i > var->effFrom) { for(k=0; knSize; k++) { index = var->relArr[k]; if(index == MAXINT) continue; if(index == MAXINT-1) continue; if(index >= i) break; } if(index < i) start = var->effTo; else start = index; } else { start = var->effFrom; } for(j=start; j=i; j--) { if(varLimit < nVar[i][j]-nDead[i][j]) continue; if(gainLimit < nDead[i][j]) continue; if(preGain != -1) { if(nDead[i][j] < preGain && nDead[i][j] >= 0) { to = j+1; for(from=i; from < to; from++) { if(nDead[from+1][to] != nDead[from][to]) break; } if(from != i) continue; splitable = 0; for(k=from; knClusterArray == 0) return; qsort(head->clusterArray, head->nClusterArray, sizeof(Cluster_t *), compare_func); dirtyBit = ALLOC(int, size); memset(dirtyBit, 0, sizeof(int)*size); clusterArray = head->clusterArray; nClusterArray = head->nClusterArray; for(i=0; ifrom][clu->to] == 1) continue; } fail_flag = 0; for(j=clu->from; j<=clu->to; j++) { if(dirtyBit[j] == 1) { fail_flag = 1; continue; } } if(fail_flag) continue; clusteredRelation = ImgLinearClusteringSmooth(head, clu, nFailure, andExistLimit, bddLimit); conjunct = 0; if(clusteredRelation) { for(j=clu->from; j<=clu->to; j++) { conjunct = head->conjunctArray[j]; if(conjunct->relation) bdd_free(conjunct->relation); conjunct->relation = 0; } conjunct->relation = clusteredRelation; conjunct->bModified = 1; head->bModified = 1; for(j=clu->from; j<=clu->to; j++) dirtyBit[j] = 1; if(head->verbosity >= 5) fprintf(stdout, "\tClustering Success : %4d -%4d G(%3d) V(%3d) A(%3d)\n", clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity); } fflush(stdout); } for(i=0; iclusterArray = 0; head->nClusterArray = 0; for(i=0; inSize; i++) { free(nDead[i]); free(nVar[i]); if(useFailureHistory) free(nFailure[i]); } free(nDead); free(nVar); if(useFailureHistory) free(nFailure); return; } /**Function******************************************************************** Synopsis [Add candidates for clustering] Description [Add candidates for clustering, each condidate has pair of relation] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearInsertClusterCandidate(Relation_t *head, int from, int to, int nDead, int nVar, double affinityLimit) { Conjunct_t *conjunct; Cluster_t *clu; int *varType, *supList; int i, j, id, size; st_table *table; double affinity, tAffinity; int preSize, postSize, curSize, overlap; varType = head->varType; conjunct = head->conjunctArray[from]; if(conjunct->relation == 0) { return; } supList = conjunct->supList; size = conjunct->nSize; table = st_init_table(st_numcmp, st_numhash); for(i=0; inum_entries; conjunct = head->conjunctArray[i]; if(conjunct->relation == 0) continue; supList = conjunct->supList; size = conjunct->nSize; curSize = 0; for(j=0; jnum_entries; overlap = curSize - (postSize-preSize); if(curSize > preSize) affinity = (double)overlap/(double)preSize; else affinity = (double)overlap/(double)curSize; /** if(affinity < affinityLimit) { st_free_table(table); return; } **/ tAffinity += affinity; } st_free_table(table); tAffinity /= (double)(to-from); clu = ALLOC(Cluster_t, 1); clu->from = from; clu->to = to; clu->nVar = nVar; clu->nDead = nDead; clu->nAffinity = (int)(tAffinity * 100.0); head->clusterArray = REALLOC(Cluster_t *, head->clusterArray, head->nClusterArray+1); head->clusterArray[head->nClusterArray++] = clu; if(head->verbosity >= 5) { fprintf(stdout, "Candidate Cluster : %4d-%4d G(%3d) V(%3d) A(%3d)\n", clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity); fflush(stdout); } } /**Function******************************************************************** Synopsis [Apply clustering while quantifying the variables that are isolated] Description [Apply clustering while quantifying the variables that are isolated] SideEffects [] SeeAlso [] ******************************************************************************/ static bdd_t * ImgLinearClusteringSmooth(Relation_t *head, Cluster_t *clu, int **failureHistory, int andExistLimit, int bddLimit) { int *varType, *supList; array_t *smoothVarBddArray, *smoothArray; Conjunct_t *conjunct; bdd_t *relation, *totalRelation; bdd_t *varBdd, *tempRelation; int i, j, k, tempSize, failFlag; int id, tid; st_table *deadTable; VarLife_t *var; varType = head->varType; smoothVarBddArray = array_alloc(array_t *, 0); for(i=clu->from; i<=clu->to; i++) { smoothArray = array_alloc(bdd_t *, 0); array_insert_last(array_t *, smoothVarBddArray, smoothArray); } deadTable = st_init_table(st_numcmp, st_numhash); for(i=clu->from; i<=clu->to; i++) { conjunct = head->conjunctArray[i]; if(conjunct == 0) continue; if(conjunct->relation == 0) continue; supList = conjunct->supList; for(j=0; jnSize; j++) { id = supList[j]; if(varType[id] == 1 || varType[id] == 2) continue; if(st_lookup(deadTable, (char *)(long)id, &tid)) continue; var = head->varArray[head->varArrayMap[id]]; if(clu->from <= var->from && var->to <= clu->to) { st_insert(deadTable, (char *)(long)id, (char *)(long)id); smoothArray = array_fetch(array_t *, smoothVarBddArray, var->to-clu->from); varBdd = bdd_get_variable(head->mgr, var->id); array_insert_last(bdd_t *, smoothArray, varBdd); } } } st_free_table(deadTable); totalRelation = bdd_one(head->mgr); failFlag = 0; for(i=clu->from; i<=clu->to; i++) { conjunct = head->conjunctArray[i]; if(conjunct == 0) continue; if(conjunct->relation == 0) continue; relation = conjunct->relation; smoothArray = array_fetch(array_t *, smoothVarBddArray, i-clu->from); tempRelation = bdd_and_smooth_with_limit(totalRelation, relation, smoothArray, andExistLimit); if(tempRelation) tempSize = bdd_size(tempRelation); else tempSize = MAXINT; if(tempSize > bddLimit) { bdd_free(totalRelation); if(tempRelation) bdd_free(tempRelation); totalRelation = 0; if(failureHistory) { for(j=0; j<=clu->from; j++) for(k=i; knSize; k++) failureHistory[j][k] = 1; } if(head->verbosity >= 3) fprintf(stdout, "Clustering Failure : %4d-%4d G(%3d) V(%3d) A(%3d) At %3d S(%d)\n", clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity, i, tempSize); break; } bdd_free(totalRelation); totalRelation = tempRelation; } ImgLinearFreeSmoothArray(smoothVarBddArray); if(failFlag) return(0); else return(totalRelation); } /**Function******************************************************************** Synopsis [ Apply clustering with priority queue] Description [ Apply clustering with priority queue] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearClusterUsingHeap(Relation_t *head, double affinityLimit, int andExistLimit, int varLimit, Img_OptimizeType optDir, int rangeFlag, int (*compare_func)(const void *, const void *)) { Cluster_t *clu; int j; Conjunct_t *conjunct; bdd_t *clusteredRelation; Heap_t *heap; int bOptimize; long dummy; bOptimize = 0; ImgLinearBuildInitialCandidate(head, affinityLimit, varLimit, rangeFlag, compare_func); /** need to consider statevariable optimization **/ heap = head->clusterHeap; while(Heap_HeapExtractMin(heap, &clu, &dummy)) { if(clu->flag) { free(clu); continue; } if(clu->to >= head->nSize) { free(clu); continue; } clusteredRelation = ImgLinearClusteringPairSmooth(head, clu, 0, andExistLimit, head->bddLimit); if(clusteredRelation) { if(head->verbosity >= 5) fprintf(stdout, "\tClustering Success : %4d -%4d G(%3d) V(%3d) A(%3d)\n", clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity); fflush(stdout); for(j=clu->from+1; j<=clu->to; j++) { conjunct = head->conjunctArray[j]; if(conjunct == 0) continue; if(conjunct->relation == 0) continue; bdd_free(conjunct->relation); conjunct->relation = 0; } conjunct = head->conjunctArray[clu->from]; if(conjunct->relation) bdd_free(conjunct->relation); conjunct->relation = clusteredRelation; conjunct->bModified = 1; ImgLinearConjunctRefine(head, conjunct); head->bModified = 1; head->bRefineVarArray = 1; Heap_HeapApplyForEachElement(heap, linearCheckRange); /** for(i=0; initems; i++) { tclu = (Cluster_t *)(heap->slots[i].item); if(tclu->from <= clu->from && clu->from <= tclu->to) tclu->flag = 1; if(tclu->from <= clu->to && clu->to <= tclu->to) tclu->flag = 1; } **/ ImgLinearInsertPairClusterCandidate(head, clu->from, affinityLimit, varLimit, rangeFlag); ImgLinearInsertPairClusterCandidate(head, clu->from-1, affinityLimit, varLimit, rangeFlag); } if(clu->nDead && clusteredRelation) { ImgLinearVariableArrayInit(head); bOptimize |= ImgLinearOptimizeAll(head, optDir, 0); } free(clu); } Heap_HeapFree(heap); head->clusterHeap = 0; if(head->bModified) { if(head->verbosity >= 5) ImgLinearPrintMatrix(head); bOptimize |= ImgLinearOptimizeAll(head, optDir, 0); ImgLinearRefineRelation(head); if(head->verbosity >= 5) ImgLinearPrintMatrix(head); } return(bOptimize); } /**Function******************************************************************** Synopsis [compare function for checking range of cluster] Description [compare function for checking range of cluster] SideEffects [] SeeAlso [] ******************************************************************************/ static int linearCheckRange(const void *tc) { Cluster_t *tclu; tclu = (Cluster_t *)tc; if(tclu->from <= __clu->from && __clu->from <= tclu->to) tclu->flag = 1; if(tclu->from <= __clu->to && __clu->to <= tclu->to) tclu->flag = 1; return(1); } /**Function******************************************************************** Synopsis [Clustering pair of transition relation] Description [Clustering pair of transition relation] SideEffects [] SeeAlso [] ******************************************************************************/ static bdd_t * ImgLinearClusteringPairSmooth(Relation_t *head, Cluster_t *clu, int **failureHistory, int andExistLimit, int bddLimit) { int *varType, *supList; array_t *smoothArray; Conjunct_t *conjunct; bdd_t *totalRelation; bdd_t *fromRelation, *toRelation; bdd_t *varBdd; int i, j, k, tempSize; int id, tid, effTo; st_table *deadTable; VarLife_t *var; varType = head->varType; smoothArray = array_alloc(bdd_t *, 0); for(effTo = clu->to+1; effTonSize; effTo++) { conjunct = head->conjunctArray[effTo]; if(conjunct && conjunct->relation) break; } effTo--; deadTable = st_init_table(st_numcmp, st_numhash); for(i=clu->from; i<=clu->to; i++) { conjunct = head->conjunctArray[i]; if(conjunct == 0) continue; if(conjunct->relation == 0) continue; supList = conjunct->supList; for(j=0; jnSize; j++) { id = supList[j]; if(varType[id] == 1 || varType[id] == 2) continue; if(st_lookup(deadTable, (char *)(long)id, &tid)) continue; var = head->varArray[head->varArrayMap[id]]; if(clu->from <= var->from && var->to <= effTo) { st_insert(deadTable, (char *)(long)id, (char *)(long)id); varBdd = bdd_get_variable(head->mgr, var->id); array_insert_last(bdd_t *, smoothArray, varBdd); } } } st_free_table(deadTable); conjunct = head->conjunctArray[clu->from]; fromRelation = conjunct->relation; toRelation = 0; for(i=clu->from+1; i<=clu->to; i++) { conjunct = head->conjunctArray[i]; if(conjunct == 0) continue; if(conjunct->relation == 0) continue; toRelation = conjunct->relation; break; } if(toRelation == 0) { mdd_array_free(smoothArray); return(0); } if(fromRelation == 0 && toRelation == 0) return(0); if(fromRelation == 0) { totalRelation = bdd_dup(toRelation); } else if(toRelation == 0) { totalRelation = bdd_dup(fromRelation); } else { totalRelation = bdd_and_smooth_with_limit(fromRelation, toRelation, smoothArray, andExistLimit); } if(totalRelation) tempSize = bdd_size(totalRelation); else tempSize = MAXINT; if(tempSize > bddLimit) { if(totalRelation) bdd_free(totalRelation); totalRelation = 0; if(failureHistory) { for(j=0; j<=clu->from; j++) for(k=i; knSize; k++) failureHistory[j][k] = 1; } if(head->verbosity >= 3) fprintf(stdout, "Clustering Failure : %4d-%4d G(%3d) V(%3d) A(%3d) At %3d S(%d)\n", clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity, i, tempSize); } mdd_array_free(smoothArray); return(totalRelation); } /**Function******************************************************************** Synopsis [Build data structure for clustering] Description [Build data structure for clustering] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearBuildInitialCandidate(Relation_t *head, double affinityLimit, int varLimit, int rangeFlag, int (*compare_func)(const void *, const void *)) { int size, i; head->clusterHeap = Heap_HeapInitCompare(head->nSize, compare_func); size = head->nSize; for(i=0; inSize-1) return; conjunct = head->conjunctArray[from]; if(conjunct == 0 || conjunct->relation == 0) { for(; from>=0; from--) { conjunct = head->conjunctArray[from]; if(conjunct == 0) continue; if(conjunct->relation == 0) continue; break; } } if(from < 0) return; to = -1; for(i=from+1; inSize; i++) { conjunct = head->conjunctArray[i]; if(!conjunct) continue; if(conjunct->relation == 0) continue; to = i; break; } if(to == -1) return; for(effTo = to+1; effTonSize; effTo++) { conjunct = head->conjunctArray[effTo]; if(conjunct && conjunct->relation) break; } effTo--; varType = head->varType; fromC = head->conjunctArray[from]; toC = head->conjunctArray[to]; if(rangeFlag && (fromC->nSize == fromC->nRange || toC->nSize == toC->nRange)) return; if(fromC->nSize == fromC->nRange && toC->nSize != toC->nRange) return; if(fromC->nSize != fromC->nRange && toC->nSize == toC->nRange) return; nDead = 0; supList = fromC->supList; size = fromC->nSize; table = st_init_table(st_numcmp, st_numhash); for(i=0; ivarArray[head->varArrayMap[id]]; if(from <= var->from && var->to <= effTo) nDead++; } preSize = table->num_entries; supList = toC->supList; size = toC->nSize; curSize = 0; for(j=0; jvarArray[head->varArrayMap[id]]; if(from <= var->from && var->to <= effTo) nDead++; } postSize = table->num_entries; overlap = curSize - (postSize-preSize); if(overlap == 0) affinity = 0.0; else { if(curSize > preSize)affinity = (double)overlap/(double)preSize; else affinity = (double)overlap/(double)curSize; } st_free_table(table); if(affinity < affinityLimit) return; if(affinity == 0.0 && postSize > 10 && (fromC->bSingleton || toC->bSingleton)) return; if(postSize-nDead > varLimit) return; clu = ALLOC(Cluster_t, 1); memset(clu, 0, sizeof(Cluster_t)); clu->from = from; clu->to = to; clu->nVar = postSize; clu->nDead = nDead; clu->nAffinity = (int)(affinity * 100.0); Heap_HeapInsertCompare(head->clusterHeap, (void *)clu, (long)clu); if(head->verbosity >= 5) { fprintf(stdout, "Candidate Cluster : %4d -%4d G(%3d) V(%3d) A(%3d)\n", clu->from, clu->to, clu->nDead, clu->nVar, clu->nAffinity); fflush(stdout); } } /**Function******************************************************************** Synopsis [Print information of debug information] Description [Print information of debug information] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearPrintDebugInfo(Relation_t *head) { int i, j, id; Conjunct_t *conjunct; int *supList; array_t *smoothVarBddArray; array_t *smoothArray; bdd_t *varBdd; int idPerLine; idPerLine = 12; fprintf(vis_stdout, "-----------------------------------------------------\n"); fprintf(vis_stdout, " Debug Information for Transition Relations\n"); fprintf(vis_stdout, "-----------------------------------------------------\n"); fprintf(vis_stdout, "List of Quantify Variables---------------------------\n"); for(i=0; inQuantify; i++) { if(i!=0 && i%idPerLine == 0) fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "%3d ", head->quantifyVars[i]); } fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "List of Domain Variables-----------------------------\n"); for(i=0; inDomain; i++) { if(i!=0 && i%idPerLine == 0) fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "%3d ", head->domainVars[i]); } fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "List of Range Variables------------------------------\n"); for(i=0; inRange; i++) { if(i!=0 && i%idPerLine == 0) fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "%3d ", head->rangeVars[i]); } fprintf(vis_stdout, "\n"); fprintf(vis_stdout, "Varibles in Each Transition Relation-----------------\n"); for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; supList = conjunct->supList; fprintf(vis_stdout, "%3d'th : ", i); for(j=0; jnSize; j++) { if(j!=0 && j%idPerLine == 0) fprintf(vis_stdout, "\n "); fprintf(vis_stdout, "%3d ", supList[j]); } fprintf(vis_stdout, "\n"); } smoothVarBddArray = ImgLinearMakeSmoothVarBdd(head, 0); fprintf(vis_stdout, "Quantified Schedule----------------------------------\n"); for(i=0; i<=head->nSize; i++) { fprintf(vis_stdout, "%3d'th : ", i); smoothArray = array_fetch(array_t *, smoothVarBddArray, i); for(j=0; jincludeCS = 0; ImgLinearConjunctionOrder(head, "FirstCon", bRefineConjunctOrder); ImgLinearComputeLifeTime(head, &aal, &atl); ImgLinearPrintMatrixFull(head, 0); head->includeCS = 1; tempConjunctArray = ALLOC(Conjunct_t *, head->nSize+1); for(i=0; inSize; i++) tempConjunctArray[i] = head->conjunctArray[i]; tempAal = aal; tempAtl = atl; fprintf(stdout, "NOTICE : aal %.3f atl %.3f\n", aal, atl); ImgLinearPrintMatrix(head); **/ ImgLinearConjunctionOrder(head, "SecondCon", bRefineConjunctOrder); ImgLinearComputeLifeTime(head, &aal, &atl); ImgLinearPrintMatrixFull(head, 1); fprintf(stdout, "NOTICE : aal %.3f atl %.3f\n", aal, atl); ImgLinearPrintMatrix(head); /** if(tempAal < aal) { if( (aal-tempAal) > (tempAtl-atl)*2.0 ) { free(head->conjunctArray); head->conjunctArray = tempConjunctArray; head->bModified = 1; head->bRefineVarArray = 1; ImgLinearRefineRelation(head); fprintf(stdout, "includeCS = 0 is taken\n"); } else { fprintf(stdout, "includeCS = 1 is taken\n"); } } else { fprintf(stdout, "includeCS = 1 is taken\n"); } **/ } /**Function******************************************************************** Synopsis [Generate linear arrangement with CAPO] Description [Generate linear arrangement with CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearConjunctionOrder(Relation_t *head, char *baseName, int refineFlag) { Conjunct_t *conjunct; int i, j; if(head->nSize < 2) return; for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; conjunct->dummy = 0; for(j=0; jnSize; j++) conjunct->dummy += conjunct->supList[j]; } qsort(head->conjunctArray, head->nSize, sizeof(Conjunct_t *), ImgLinearCompareConjunctSize); head->bRefineVarArray = 1; ImgLinearRefineRelation(head); ImgLinearCAPOInterfaceConjunctNodes(head, baseName); ImgLinearCAPOInterfaceConjunctNet(head, baseName); ImgLinearCAPOInterfaceConjunctScl(head, baseName); ImgLinearCAPOInterfaceConjunctPl(head, baseName); ImgLinearCAPOInterfaceAux(head, baseName); ImgLinearCAPORun("MetaPlacer", baseName, 0); ImgLinearCAPOReadConjunctOrder(head, baseName); } /**Function******************************************************************** Synopsis [Make interface files for CAPO] Description [Make interface files for CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearCAPOInterfaceConjunctNodes(Relation_t *head, char *baseName) { char filename[1024]; FILE *fout; int i; sprintf(filename, "%s.nodes", baseName); fout = fopen(filename, "w"); fprintf(fout, "UCLA nodes 1.0\n"); if(head->includeNS) { if(head->includeCS) { fprintf(fout, "NumNodes : %d\n", head->nSize+2); fprintf(fout, "NumTerminals : 2\n"); } else { fprintf(fout, "NumNodes : %d\n", head->nSize+1); fprintf(fout, "NumTerminals : 1\n"); } } else if(head->includeCS) { fprintf(fout, "NumNodes : %d\n", head->nSize+1); fprintf(fout, "NumTerminals : 1\n"); } else { fprintf(fout, "NumNodes : %d\n", head->nSize); fprintf(fout, "NumTerminals : 0\n"); } for(i=0; inSize; i++) fprintf(fout, "C%d 1 1\n", i); if(head->includeCS) fprintf(fout, "C%d 1 1 terminal\n", MAXINT-1); if(head->includeNS) fprintf(fout, "C%d 1 1 terminal\n", MAXINT); fclose(fout); } /**Function******************************************************************** Synopsis [Make interface files for CAPO] Description [Make interface files for CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearCAPOInterfaceConjunctNet(Relation_t *head, char *baseName) { char filename[1024]; FILE *fout; VarLife_t **varArray, *var; int i, j, nPin; varArray = head->varArray; sprintf(filename, "%s.nets", baseName); fout = fopen(filename, "w"); fprintf(fout, "UCLA nets 1.0\n"); fprintf(fout, "#NumNets : %d\n", head->nVarArray); qsort(head->varArray, head->nVarArray, sizeof(VarLife_t *), ImgLinearCompareVarId); nPin = 0; for(i=0; inVarArray; i++) { var = varArray[i]; if(var->nSize == 1) nPin += 2; else nPin += var->nSize; } fprintf(fout, "NumPins : %d\n", nPin); for(i=0; inVarArray; i++) { var = varArray[i]; if(var->nSize == 1) fprintf(fout, "NetDegree : %d S%d\n", var->nSize+1, var->id); else fprintf(fout, "NetDegree : %d S%d\n", var->nSize, var->id); for(j=0; jnSize; j++) fprintf(fout, "C%d B\n", var->relArr[j]); if(var->nSize == 1) fprintf(fout, "C%d B\n", var->relArr[0]); } fclose(fout); } /**Function******************************************************************** Synopsis [Make interface files for CAPO] Description [Make interface files for CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearCAPOInterfaceConjunctScl(Relation_t *head, char *baseName) { char filename[1024]; FILE *fout; sprintf(filename, "%s.scl", baseName); fout = fopen(filename, "w"); fprintf(fout, "UCLA scl 1.0\n"); fprintf(fout, "Numrows : 1\n"); fprintf(fout, "CoreRow Horizontal\n"); fprintf(fout, " Coordinate : 1\n"); fprintf(fout, " Height : 1\n"); fprintf(fout, " Sitewidth : 1\n"); fprintf(fout, " Sitespacing : 1\n"); fprintf(fout, " Siteorient : N\n"); fprintf(fout, " Sitesymmetry : Y\n"); fprintf(fout, " SubrowOrigin : 0\n"); fprintf(fout, " Numsites : %d\n", head->nSize*2+2); fprintf(fout, "End\n"); fclose(fout); } /**Function******************************************************************** Synopsis [Make interface files for CAPO] Description [Make interface files for CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearCAPOInterfaceConjunctPl(Relation_t *head, char *baseName) { char filename[1024]; FILE *fout; int i; sprintf(filename, "%s.pl", baseName); fout = fopen(filename, "w"); fprintf(fout, "UCLA pl 1.0\n"); for(i=0; inSize; i++) fprintf(fout, "C%d %d 1\n", i, (i+2)*2+1); if(head->includeCS) fprintf(fout, "C%d 0 1 / N / FIXED\n", MAXINT-1); if(head->includeNS) fprintf(fout, "C%d %d 1 / N / FIXED\n", MAXINT, (head->nSize+2)*2+1); fclose(fout); } /**Function******************************************************************** Synopsis [Make interface files for CAPO] Description [Make interface files for CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearCAPOInterfaceAux(Relation_t *head, char *baseName) { char filename[1024]; FILE *fout; sprintf(filename, "%s.aux", baseName); fout = fopen(filename, "w"); fprintf(fout, "RowBasedPlacement : "); fprintf(fout, "%s.nodes %s.nets %s.pl %s.scl\n", baseName, baseName, baseName, baseName); fclose(fout); } /**Function******************************************************************** Synopsis [Run batch job of CAPO] Description [Run batch job of CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCAPORun(char *capoExe, char *baseName, int brief) { char logFile[1024]; char capoOption[1024]; char command[1024]; char cpCommand[1024]; FILE *fout; int cmdStatus; fout = fopen("seeds.in", "w"); fprintf(fout, "0\n"); fprintf(fout, "460427264\n"); fclose(fout); if(brief) sprintf(capoOption, "-replaceSmallBlocks Never -noRowIroning -save -saveXorder"); else sprintf(capoOption, "-save -saveXorder -clust CutOpt"); sprintf(logFile, "%s.log", baseName); sprintf(command, "%s -f %s.aux %s > %s", capoExe, baseName, capoOption, logFile); cmdStatus = system(command); sprintf(cpCommand, "cp left2right.ord %s.ord", baseName); cmdStatus |= system(cpCommand); unlink("seeds.out"); unlink("left2right.ord"); return (cmdStatus == 0); } /**Function******************************************************************** Synopsis [Read result of CAPO] Description [Read result of CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearCAPOReadConjunctOrder(Relation_t *head, char *baseName) { char ordFile[1024]; char line[1024]; int index, id; char *next; FILE *fin; Conjunct_t *conjunct; sprintf(ordFile, "%s.ord", baseName); if(!(fin = fopen(ordFile, "r"))) { fprintf(stdout, "Can't open order file %s\n", ordFile); exit(0); } index = 0; while(fgets(line, 1024, fin)){ next = strchr(line, 'C'); next++; sscanf(next, "%d", &id); if(id == MAXINT) continue; if(id == MAXINT-1) continue; conjunct = head->conjunctArray[id]; conjunct->index = index; index++; } fclose(fin); qsort(head->conjunctArray, head->nSize, sizeof(Conjunct_t *), ImgLinearCompareConjunctIndex); head->bModified = 1; head->bRefineVarArray = 1; ImgLinearRefineRelation(head); } /**Function******************************************************************** Synopsis [Make interface for variable ordering] Description [Make interface for variable ordering] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearVariableOrder(Relation_t *head, char *baseName, int includeNS) { ImgLinearCAPOInterfaceVariableNodes(head, baseName, includeNS); ImgLinearCAPOInterfaceVariableNet(head, baseName, includeNS); ImgLinearCAPOInterfaceVariableScl(head, baseName); ImgLinearCAPOInterfaceVariablePl(head, baseName, includeNS); ImgLinearCAPOInterfaceAux(head, baseName); ImgLinearCAPORun("MetaPlacer", baseName, 0); ImgLinearCAPOReadVariableOrder(head, baseName, includeNS); } /**Function******************************************************************** Synopsis [Make interface for CAPO] Description [Make interface for CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearCAPOInterfaceVariableNodes(Relation_t *head, char *baseName, int includeNS) { int i, size; VarLife_t **varArray, *var; int *varType; char filename[1024]; FILE *fout; int numUnused; varArray = head->varArray; varType = head->varType; sprintf(filename, "%s.nodes", baseName); fout = fopen(filename, "w"); fprintf(fout, "UCLA nodes 1.0\n"); size = 0; if(includeNS) size = head->nVarArray; else { for(i=0; inVarArray; i++) { if(varType[varArray[i]->id] == 2) continue; size++; } } numUnused = 0; for(i=0; inVar; i++) { if(varType[i] != 1) continue; /* if it is not domain variable **/ var = head->varArrayMap[i] >=0 ? head->varArray[head->varArrayMap[i]] : 0; if(var) continue; numUnused++; } if(includeNS) { for(i=0; inVar; i++) { if(varType[i] != 2) continue; /* if it is not range variable **/ var = head->varArrayMap[i] >=0 ? head->varArray[head->varArrayMap[i]] : 0; if(var) continue; numUnused++; } } fprintf(fout, "NumNodes : %d\n", size+numUnused); fprintf(fout, "NumTerminals : 0\n"); for(i=0; inVarArray; i++) { var = varArray[i]; if(includeNS == 0 && varType[var->id] == 2) continue; fprintf(fout, "C%d 1 1\n", var->id); } for(i=0; inVar; i++) { if(varType[i] != 1) continue; /* if it is not domain variable **/ var = head->varArrayMap[i] >=0 ? head->varArray[head->varArrayMap[i]] : 0; if(var) continue; fprintf(fout, "C%d 1 1\n", i); } if(includeNS) { for(i=0; inVar; i++) { if(varType[i] != 2) continue; /* if it is not range variable **/ var = head->varArrayMap[i] >=0 ? head->varArray[head->varArrayMap[i]] : 0; if(var) continue; fprintf(fout, "C%d 1 1\n", i); } } fclose(fout); } /**Function******************************************************************** Synopsis [Make interface for CAPO] Description [Make interface for CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearCAPOInterfaceVariableNet(Relation_t *head, char *baseName, int includeNS) { int nPin, i, j; int id, size; Conjunct_t *conjunct; bdd_t *relation; int *supList, *varType; char filename[1024]; FILE *fout; nPin = 0; for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; relation = conjunct->relation; if(relation == (mdd_t *)(MAXINT-1)) continue; supList = conjunct->supList; if(includeNS) { if(conjunct->nSize == 1) nPin += 2; else nPin += conjunct->nSize-conjunct->nRange; } else { if(conjunct->nSize-conjunct->nRange == 1) nPin += 2; else nPin += conjunct->nSize-conjunct->nRange; } } nPin += head->nDomain; if(includeNS) nPin += head->nRange; varType = head->varType; sprintf(filename, "%s.nets", baseName); fout = fopen(filename, "w"); fprintf(fout, "UCLA nets 1.0\n"); fprintf(fout, "#NumNets : %d\n", head->nSize); fprintf(fout, "NumPins : %d\n", nPin); for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; relation = conjunct->relation; if(relation == (mdd_t *)(MAXINT-1)) continue; supList = conjunct->supList; if(includeNS) size = conjunct->nSize; else size = conjunct->nSize - conjunct->nRange; if(size == 1) fprintf(fout, "NetDegree : %d \n", 2); else fprintf(fout, "NetDegree : %d \n", size); id = 0; if(includeNS) { for(j=0; jnSize; j++) { id = supList[j]; fprintf(fout, "C%d B\n", id); } } else { for(j=0; jnSize; j++) { id = supList[j]; if(varType[id] == 2) continue; fprintf(fout, "C%d B\n", id); } } if(size == 1) fprintf(fout, "C%d B\n", id); } fprintf(fout, "NetDegree : %d \n", head->nDomain); for(i=0; inVar; i++) { if(varType[i] == 1) fprintf(fout, "C%d B\n", i); } if(includeNS) { fprintf(fout, "NetDegree : %d \n", head->nRange); for(i=0; inVar; i++) { if(varType[i] == 2) fprintf(fout, "C%d B\n", i); } } fclose(fout); } /**Function******************************************************************** Synopsis [Make interface for CAPO] Description [Make interface for CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearCAPOInterfaceVariableScl(Relation_t *head, char *baseName) { char filename[1024]; FILE *fout; sprintf(filename, "%s.scl", baseName); fout = fopen(filename, "w"); fprintf(fout, "UCLA scl 1.0\n"); fprintf(fout, "Numrows : 1\n"); fprintf(fout, "CoreRow Horizontal\n"); fprintf(fout, " Coordinate : 1\n"); fprintf(fout, " Height : 1\n"); fprintf(fout, " Sitewidth : 1\n"); fprintf(fout, " Sitespacing : 1\n"); fprintf(fout, " Siteorient : N\n"); fprintf(fout, " Sitesymmetry : Y\n"); fprintf(fout, " SubrowOrigin : 0\n"); fprintf(fout, " Numsites : %d\n", head->nVarArray*2+2); fprintf(fout, "End\n"); fclose(fout); } /**Function******************************************************************** Synopsis [Make interface for CAPO] Description [Make interface for CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearCAPOInterfaceVariablePl(Relation_t *head, char *baseName, int includeNS) { char filename[1024]; FILE *fout; VarLife_t *var, **varArray; int i, index, *varType; varType = head->varType; sprintf(filename, "%s.pl", baseName); fout = fopen(filename, "w"); fprintf(fout, "UCLA pl 1.0\n"); varArray = head->varArray; for(index=0, i=0; inVarArray; i++) { var = varArray[i]; if(includeNS == 0 && varType[var->id] == 2) continue; fprintf(fout, "C%d %d 1\n", var->id, (index+1)*2+1); index++; } fclose(fout); } /**Function******************************************************************** Synopsis [Read result of CAPO] Description [Read result of CAPO] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearCAPOReadVariableOrder(Relation_t *head, char *baseName, int includeNS) { char ordFile[1024], line[1024]; FILE *fin; char *next; int i, id, index, *permutation, *exist; sprintf(ordFile, "%s.ord", baseName); if(!(fin = fopen(ordFile, "r"))) { fprintf(stdout, "Can't open order file %s\n", ordFile); exit(0); } permutation = ALLOC(int, head->nVar); exist = ALLOC(int, head->nVar); memset(exist, 0, sizeof(int)*head->nVar); index = 0; while(fgets(line, 1024, fin)){ next = strchr(line, 'C'); next++; sscanf(next, "%d", &id); permutation[index++] = id; exist[id] = 1; if(includeNS == 0 && head->varType[id] == 1) { permutation[index++] = head->domain2range[id]; exist[head->domain2range[id]] = 1; } } fclose(fin); for(i=0; inVar; i++) if(exist[i] == 0) permutation[index++] = i; free(exist); bdd_shuffle_heap(head->mgr, permutation); free(permutation); } /**Function******************************************************************** Synopsis [Print profile of variables] Description [Print profile of variables] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearPrintVariableProfile(Relation_t *head, char *baseName) { double aal, atl; char filename[1024]; FILE *fout; st_table *cutSet; int i, j, nDead, id; int *varType; int *supList; Conjunct_t *conjunct; VarLife_t *var; st_generator *gen; ImgLinearVariableArrayInit(head); varType = head->varType; sprintf(filename, "%s.data", baseName); fout = fopen(filename, "w"); cutSet = st_init_table(st_numcmp, st_numhash); for(i=0; inVar; i++) { if(varType[i] == 1) st_insert(cutSet, (char *)(long)i, (char *)(long)i); } for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; supList = conjunct->supList; for(j=0; jnSize; j++) st_insert(cutSet, (char *)(long)supList[j], (char *)(long)supList[j]); nDead = 0; st_foreach_item(cutSet, gen, &id, &id) { if(varType[id] == 2) continue; var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0; if(!var) continue; if(var->to <= i) { nDead++; st_delete(cutSet, (&id), NULL); } } fprintf(fout, "%d %d %d\n", i, cutSet->num_entries, cutSet->num_entries+nDead); } fclose(fout); ImgLinearComputeLifeTime(head, &aal, &atl); sprintf(filename, "%s.gnu", baseName); fout = fopen(filename, "w"); fprintf(fout, "set terminal postscript \n"); fprintf(fout, "set output \"%s.ps\"\n", baseName); fprintf(fout, "set title \"profile of live variable aal %.3f atl %.3f\"\n", aal, atl); fprintf(fout, "plot \"%s.data\" using 1:2 title \"%s\" with lines, \\\n", baseName, "cut"); fprintf(fout, " \"%s.data\" using 1:3 title \"%s\" with lines\n", baseName, "cut+dead"); fclose(fout); } /**Function******************************************************************** Synopsis [Print matrix] Description [Print matrix. Its x axis is varaible and its y axis is relation] SideEffects [Print matrix. Its x axis is varaible and its y axis is relation] SeeAlso [] ******************************************************************************/ void ImgLinearPrintMatrix(Relation_t *head) { int i, j, id, index; int *mapArray; VarLife_t **varArray, *var; VarLife_t **auxArr, **sortArr; int nAuxArr, nSortArr; array_t *smoothVarBddArr, *smoothArray; bdd_t *varBdd; Conjunct_t *conjunct; bdd_t *relation; int *supList, *varType; char *buffer; int maxIndex; if(head->verbosity < 5) return; ImgLinearVariableArrayInit(head); mapArray = ALLOC(int, head->nVar); memset(mapArray, -1, sizeof(int)*head->nVar); varArray = head->varArray; smoothVarBddArr = ImgLinearMakeSmoothVarBdd(head, 0); for(index=0, i=0; ivarArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0; if(var) { auxArr[nAuxArr++] = var; auxArr = REALLOC(VarLife_t *, auxArr, nAuxArr+1); } } qsort(auxArr, nAuxArr, sizeof(VarLife_t *), ImgLinearCompareVarIndex); for(j=0; jid] = index++; free(auxArr); } varArray = head->varArray; nSortArr = 0; sortArr = ALLOC(VarLife_t *, nSortArr+1); for(i=0; inVarArray; i++) { var = varArray[i]; if(var->stateVar == 2) continue; if(mapArray[var->id] >= 0) { var->index = mapArray[var->id]; sortArr[nSortArr++] = var; sortArr = REALLOC(VarLife_t *, sortArr, nSortArr+1); } else { var->index = (double)MAXINT; } } qsort(sortArr, nSortArr, sizeof(VarLife_t *), ImgLinearCompareVarIndex); fprintf(stdout, " "); for(i=0; iindex = (double)i; if(var->stateVar == 1) buffer[i] = 'C'; else buffer[i] = 'T'; } buffer[i] = '\0'; free(sortArr); fprintf(stdout, " %s\n", buffer); maxIndex = i; for(i=0; ivarType; for(index=0,i=head->nSize-1;i>=0; i--) { conjunct = head->conjunctArray[i]; if(conjunct == 0) continue; if(conjunct->relation == 0) continue; relation = conjunct->relation; if(relation == (mdd_t *)(MAXINT-1)) continue; if(relation == 0) continue; supList = conjunct->supList; for(j=0; jnSize; j++) { id = supList[j]; if(varType[id] == 2) continue; var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0; if(!var) continue; if((int)var->index == MAXINT) continue; buffer[(int)var->index] = '1'; } index++; fprintf(stdout, "%4d %s %d %d\n", i, buffer, conjunct->nRange, bdd_size(relation)); fflush(stdout); for(j=0; jnVar); memset(mapArray, -1, sizeof(int)*head->nVar); varArray = head->varArray; smoothVarBddArr = ImgLinearMakeSmoothVarBdd(head, 0); for(index=0, i=0; ivarArrayMap[id] >=0 ? varArray[head->varArrayMap[id]] : 0; if(var) { auxArr[nAuxArr++] = var; auxArr = REALLOC(VarLife_t *, auxArr, nAuxArr+1); } } qsort(auxArr, nAuxArr, sizeof(VarLife_t *), ImgLinearCompareVarIndex); for(j=0; jid] = index++; free(auxArr); } nSortArr = 0; sortArr = ALLOC(VarLife_t *, nSortArr+1); for(i=0; inVarArray; i++) { var = varArray[i]; if(var->stateVar == 2) continue; if(mapArray[var->id] >= 0) { var->index = mapArray[var->id]; sortArr[nSortArr++] = var; sortArr = REALLOC(VarLife_t *, sortArr, nSortArr+1); } else { var->index = (double)MAXINT; } } qsort(sortArr, nSortArr, sizeof(VarLife_t *), ImgLinearCompareVarIndex); free(mapArray); sprintf(filename, "fullmatrix%d.data", matrixIndex); fout = fopen(filename, "w"); min = 0; max = head->nSize+1; for(i=0; istateVar == 1) fprintf(fout, "%d %d\n", (int)var->index, min); } free(sortArr); for(index=0, i=0; inSize; i++) { conjunct = head->conjunctArray[i]; relation = conjunct->relation; if(relation == (mdd_t *)(MAXINT-1)) continue; if(relation == 0) continue; supList = conjunct->supList; for(j=0; jnSize; j++) { id = supList[j]; var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0; if(!var) continue; if(var->stateVar == 2) if((int)var->index == MAXINT) continue; fprintf(fout, "%d %d\n", (int)var->index, index+1); } index++; } fclose(fout); sprintf(filename, "fullmatrix%d.gnu", matrixIndex); fout = fopen(filename, "w"); fprintf(fout, "set terminal postscript \n"); fprintf(fout, "set output \"fullmatrix%d.ps\"\n", matrixIndex); fprintf(fout, "set title \"profile of live variable\"\n"); fprintf(fout, "set yrange [-1:%d]\n", head->nSize+2); fprintf(fout, "plot \"fullmatrix%d.data\" using 1:2 title \"%d\" with point\n", matrixIndex, matrixIndex); fclose(fout); ImgLinearFreeSmoothArray(smoothVarBddArr); } /**Function******************************************************************** Synopsis [Free smooth variable array] Description [Free smooth variable array] SideEffects [] SeeAlso [] ******************************************************************************/ void ImgLinearFreeSmoothArray(array_t *smoothVarBddArray) { int i; array_t *smoothArray; for(i=0; ivarArray; for(i=0; inVarArray; i++) { var = varArray[i]; aal += var->effTo - var->effFrom; if(var->stateVar == 1) atl += var->to+1; else if(var->stateVar == 2) atl += head->nSize+1 - var->from; else atl += var->to - var->from; } atl = atl / (double)(head->nVarArray * head->nSize); aal = aal / (double)(head->nVarArray * head->nSize); *paal = aal; *patl = atl; } /**Function******************************************************************** Synopsis [Print transition relation info] Description [Print transition relation info] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearPrintTransitionInfo(Relation_t *head) { double aal, atl; fprintf(stdout, "SUMMARY : domain variables %d -> %d -> %d\n", head->nDomain, head->nInitDomain, head->nEffDomain); fprintf(stdout, "SUMMARY : range variables %d -> %d -> %d\n", head->nRange, head->nInitRange, head->nEffRange); fprintf(stdout, "SUMMARY : quantify variables %d -> %d -> %d\n", head->nQuantify, head->nInitQuantify, head->nEffQuantify); fprintf(stdout, "SUMMARY : number of transition relation %d\n", head->nSize); ImgLinearComputeLifeTime(head, &aal, &atl); fprintf(stdout, "Active Life Time : %g\n", aal); fprintf(stdout, "Average Life Time : %g\n", atl); } /**Function******************************************************************** Synopsis [Make the array of smooth variables] Description [Make the array of smooth variables] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * ImgLinearMakeSmoothVarBdd(Relation_t *head, bdd_t **smoothCubeArr) { array_t *smoothVarBddArray; array_t *smoothArray; VarLife_t **varArray; int i, j, id; VarLife_t *var; bdd_t *varBdd, *cube, *newCube; smoothVarBddArray = array_alloc(array_t *, 0); for(i=0; i<=head->nSize; i++) { smoothArray = array_alloc(bdd_t *, 0); array_insert_last(array_t *, smoothVarBddArray, smoothArray); } varArray = head->varArray; for(i=0; inVarArray; i++) { var = varArray[i]; if(var->stateVar == 2) continue; smoothArray = array_fetch(array_t *, smoothVarBddArray, var->to+1); varBdd = bdd_get_variable(head->mgr, var->id); array_insert_last(bdd_t *, smoothArray, varBdd); } smoothArray = array_fetch(array_t *, smoothVarBddArray, 0); for(i=0; inDomain; i++) { id = head->domainVars[i]; var = head->varArrayMap[id] >=0 ? head->varArray[head->varArrayMap[id]] : 0; if(var) continue; varBdd = bdd_get_variable(head->mgr, id); array_insert_last(bdd_t *, smoothArray, varBdd); } if(smoothCubeArr) { for(i=0; i<=head->nSize; i++) { smoothArray = array_fetch(array_t *, smoothVarBddArray, i); cube = bdd_one(head->mgr); for(j=0; jeffFrom > con2->effFrom); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareVarDummyLarge(const void *c1, const void *c2) { VarLife_t *con1, *con2; con1 = *(VarLife_t **)c1; con2 = *(VarLife_t **)c2; return(con1->dummy < con2->dummy); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareVarEffFromLarge(const void *c1, const void *c2) { VarLife_t *con1, *con2; con1 = *(VarLife_t **)c1; con2 = *(VarLife_t **)c2; return(con1->effFrom < con2->effFrom); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareVarId(const void *c1, const void *c2) { VarLife_t *con1, *con2; con1 = *(VarLife_t **)c1; con2 = *(VarLife_t **)c2; return(con1->id < con2->id); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareVarSize(const void *c1, const void *c2) { VarLife_t *con1, *con2; con1 = *(VarLife_t **)c1; con2 = *(VarLife_t **)c2; return(con1->nSize > con2->nSize); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareConjunctRangeMinusDomain(const void *c1, const void *c2) { Conjunct_t *con1, *con2; con1 = *(Conjunct_t **)c1; con2 = *(Conjunct_t **)c2; return(con1->nRange-con1->nDomain > con2->nRange-con2->nDomain); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareConjunctDummy(const void *c1, const void *c2) { Conjunct_t *con1, *con2; con1 = *(Conjunct_t **)c1; con2 = *(Conjunct_t **)c2; return(con1->dummy > con2->dummy); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareConjunctIndex(const void *c1, const void *c2) { Conjunct_t *con1, *con2; con1 = *(Conjunct_t **)c1; con2 = *(Conjunct_t **)c2; return(con1->index > con2->index); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareConjunctSize(const void *c1, const void *c2) { Conjunct_t *con1, *con2; con1 = *(Conjunct_t **)c1; con2 = *(Conjunct_t **)c2; if(con1->nSize == con2->nSize) return(con1->dummy < con2->dummy); return(con1->nSize < con2->nSize); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareVarIndex(const void *c1, const void *c2) { VarLife_t *v1, *v2; v1 = *(VarLife_t **)c1; v2 = *(VarLife_t **)c2; return(v1->index < v2->index); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareDeadAffinityLive(const void *c1, const void *c2) { Cluster_t *clu1, *clu2; clu1 = *(Cluster_t **)c1; clu2 = *(Cluster_t **)c2; if(clu1->nDead == clu2->nDead) { if(clu1->nAffinity == clu2->nAffinity) { return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead); } return(clu1->nAffinity < clu2->nAffinity); } return(clu1->nDead < clu2->nDead); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareDeadLiveAffinity(const void *c1, const void *c2) { Cluster_t *clu1, *clu2; clu1 = *(Cluster_t **)c1; clu2 = *(Cluster_t **)c2; if(clu1->nDead == clu2->nDead) { if(clu1->nVar-clu1->nDead == clu2->nVar-clu2->nDead) { return(clu1->nAffinity < clu2->nAffinity); } return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead); } return(clu1->nDead < clu2->nDead); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareAffinityDeadLive(const void *c1, const void *c2) { Cluster_t *clu1, *clu2; clu1 = *(Cluster_t **)c1; clu2 = *(Cluster_t **)c2; if(clu1->nAffinity == clu2->nAffinity) { if(clu1->nDead == clu2->nDead) { return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead); } return(clu1->nDead < clu2->nDead); } return(clu1->nAffinity < clu2->nAffinity); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearCompareLiveAffinityDead(const void *c1, const void *c2) { Cluster_t *clu1, *clu2; clu1 = *(Cluster_t **)c1; clu2 = *(Cluster_t **)c2; if(clu1->nVar-clu1->nDead == clu2->nVar-clu2->nDead) { if(clu1->nAffinity == clu2->nAffinity) { return(clu1->nDead < clu2->nDead); } return(clu1->nAffinity < clu2->nAffinity); } return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearHeapCompareDeadAffinityLive(const void *c1, const void *c2) { Cluster_t *clu1, *clu2; clu1 = (Cluster_t *)c1; clu2 = (Cluster_t *)c2; if(clu1->nDead == clu2->nDead) { if(clu1->nAffinity == clu2->nAffinity) { return((clu1->nVar-clu1->nDead) > (clu2->nVar-clu2->nDead)); } return(clu1->nAffinity < clu2->nAffinity); } return(clu1->nDead < clu2->nDead); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearHeapCompareDeadLiveAffinity(const void *c1, const void *c2) { Cluster_t *clu1, *clu2; clu1 = (Cluster_t *)c1; clu2 = (Cluster_t *)c2; if(clu1->nDead == clu2->nDead) { if((clu1->nVar-clu1->nDead) == (clu2->nVar-clu2->nDead)) { return(clu1->nAffinity < clu2->nAffinity); } return((clu1->nVar-clu1->nDead) > (clu2->nVar-clu2->nDead)); } return(clu1->nDead < clu2->nDead); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearHeapCompareAffinityDeadLive(const void *c1, const void *c2) { Cluster_t *clu1, *clu2; clu1 = (Cluster_t *)c1; clu2 = (Cluster_t *)c2; if(clu1->nAffinity == clu2->nAffinity) { if(clu1->nDead == clu2->nDead) { return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead); } return(clu1->nDead < clu2->nDead); } return(clu1->nAffinity < clu2->nAffinity); } /**Function******************************************************************** Synopsis [Priority function for clutering] Description [Priority function for clutering] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearHeapCompareLiveAffinityDead(const void *c1, const void *c2) { Cluster_t *clu1, *clu2; clu1 = (Cluster_t *)c1; clu2 = (Cluster_t *)c2; if(clu1->nVar-clu1->nDead == clu2->nVar-clu2->nDead) { if(clu1->nAffinity == clu2->nAffinity) { return(clu1->nDead < clu2->nDead); } return(clu1->nAffinity < clu2->nAffinity); } return(clu1->nVar-clu1->nDead > clu2->nVar-clu2->nDead); } /**Function******************************************************************** Synopsis [Initialize variable array] Description [Initialize variable array] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearVariableArrayInit(Relation_t *head) { mdd_manager *mgr; Conjunct_t **conjunctArray, *conjunct; Conjunct_t *tConjunct; bdd_t *relation, *bddOne; VarLife_t **varArray; int *supList, listSize; int *varType, *varArrayMap; int i, j, k, id, nVarArray; int nSize, newNum; if(head->bRefineVarArray) { ImgLinearVariableArrayQuit(head); } if(head->varArray) return; mgr = head->mgr; if(head->nVar != (int)(bdd_num_vars(mgr))) { newNum = bdd_num_vars(head->mgr); head->domain2range = REALLOC(int, head->domain2range, newNum); head->range2domain = REALLOC(int, head->range2domain, newNum); head->varType = REALLOC(int, head->varType, newNum); head->varArrayMap = REALLOC(int, head->varArrayMap, newNum); head->constantCase = REALLOC(bdd_t *, head->constantCase, newNum); head->quantifyVars = REALLOC(int, head->quantifyVars, newNum); for(i=head->nVar; idomain2range[i] = -1; head->range2domain[i] = -1; head->varType[i] = 0; head->varArrayMap[i] = -1; head->constantCase[i] = 0; head->quantifyVars[i] = 0; } head->nVar = bdd_num_vars(head->mgr); } nSize = head->nSize; conjunctArray = head->conjunctArray; varArrayMap = head->varArrayMap; id = 0; nVarArray = 0; varArray = ALLOC(VarLife_t *, nVarArray+1); head->varArray = varArray; head->nVarArray = nVarArray; bddOne = bdd_one(head->mgr); varType = head->varType; for(i=0; irelation; if(relation == 0) continue; if(bdd_equal(bddOne, relation)) continue; supList = conjunct->supList; listSize = conjunct->nSize; for(j=0; jnCluster; k++) { tConjunct = conjunct->clusterArray[k]; supList = tConjunct->supList; listSize = tConjunct->nSize; for(j=0; jbRefineVarArray = 0; } /**Function******************************************************************** Synopsis [Update variable array with id of variable id] Description [Update variable array with id of variable id] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearUpdateVariableArrayWithId(Relation_t *head, int cindex, int id) { VarLife_t *var; int *varType; int *varArrayMap; int nVarArray; VarLife_t **varArray; varType = head->varType; varArrayMap = head->varArrayMap; varArray = head->varArray; nVarArray = head->nVarArray; if(varArrayMap[id] == -1) { var = ALLOC(VarLife_t, 1); var->id = id; var->from = cindex; var->to = cindex; var->effFrom = cindex; var->effTo = cindex; var->stateVar = 0; var->relArr = ALLOC(int, 1); var->nSize = 0; var->index = 0.0; varArrayMap[id] = nVarArray; varArray[nVarArray++] = var; varArray = REALLOC(VarLife_t *, varArray, nVarArray+1); if(varType[id] == 1) { var->stateVar = 1; if(head->includeCS && !head->quantifyCS) { var->relArr = REALLOC(int, var->relArr, var->nSize+1); var->relArr[var->nSize++] = MAXINT-1; var->from = -1; } } else if(varType[id] == 2) { var->stateVar = 2; if(head->includeNS) { var->relArr = REALLOC(int, var->relArr, var->nSize+1); var->relArr[var->nSize++] = MAXINT; var->to = head->nSize; } } } else { var = varArray[varArrayMap[id]]; } if(var->to < cindex) var->to = cindex; if(var->from > cindex) var->from = cindex; if(var->effTo < cindex) var->effTo = cindex; if(var->effFrom > cindex) var->effFrom = cindex; var->relArr = REALLOC(int, var->relArr, var->nSize+1); var->relArr[var->nSize++] = cindex; head->varArray = varArray; head->nVarArray = nVarArray; } /**Function******************************************************************** Synopsis [Apply quantification with candidate variables] Description [Apply quantification with candidate variables] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearQuantifyVariablesFromConjunct(Relation_t *head, Conjunct_t *conjunct, array_t *smoothVarBddArray, int *bModified) { bdd_t *relation, *simpleRelation; if(conjunct == 0) return 1; relation = conjunct->relation; if(relation == 0) return 1; simpleRelation = bdd_smooth(relation, smoothVarBddArray); if(bdd_equal(relation, simpleRelation)) { bdd_free(simpleRelation); return 0; } bdd_free(relation); (*bModified)++; conjunct->relation = simpleRelation; conjunct->bModified = 1; head->bModified = 1; head->bRefineVarArray = 1; ImgLinearConjunctRefine(head, conjunct); return 1; } /**Function******************************************************************** Synopsis [Refine conjunction array to fill the empty slot.] Description [Refine conjunction array to fill the empty slot.] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearConjunctRefine(Relation_t *head, Conjunct_t *conjunct) { int i, id, listSize, *supList; int *varType; if(conjunct->relation == 0) { if(conjunct->supList) free(conjunct->supList); conjunct->supList = 0; return; } if(!conjunct->bModified) return; if(conjunct->supList) { free(conjunct->supList); conjunct->supList = 0; } supList = ImgLinearGetSupportBddId(head->mgr, conjunct->relation, &listSize); if(listSize == 0) { conjunct->relation = 0; if(conjunct->supList) { free(conjunct->supList); conjunct->supList = 0; } return; } else { varType = head->varType; conjunct->supList = supList; conjunct->nSize = listSize; conjunct->bModified = 0; conjunct->nDomain = 0; conjunct->nRange = 0; conjunct->nQuantify = 0; conjunct->from = 0; conjunct->to = 0; conjunct->dummy = 0; for(i=0; inDomain++; else if(varType[id] == 2) conjunct->nRange++; else if(varType[id] == 3) conjunct->nQuantify++; } head->bModified = 1; } return; } /**Function******************************************************************** Synopsis [Refine conjunction array to fill the empty slot.] Description [Refine conjunction array to fill the empty slot.] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearConjunctArrayRefine(Relation_t *head) { int nSize, i; int index; Conjunct_t **conjunctArray, **newConjunctArray; Conjunct_t *conjunct; if(head->bModified == 0) return; conjunctArray = head->conjunctArray; newConjunctArray = ALLOC(Conjunct_t *, head->nSize+1); nSize = head->nSize; for(index=0, i=0; ibRefineVarArray = 1; continue; } if(conjunct->relation == 0) { ImgLinearConjunctQuit(conjunct); head->bRefineVarArray = 1; continue; } if(conjunct->bModified) { ImgLinearConjunctRefine(head, conjunct); head->bRefineVarArray = 1; } if(conjunct == 0) continue; if(conjunct->relation == 0) { ImgLinearConjunctQuit(conjunct); continue; } newConjunctArray[index] = conjunct; conjunct->index = index++; } newConjunctArray[index] = 0; free(conjunctArray); head->conjunctArray = newConjunctArray; head->nSize = index; head->bModified = 0; return; } /**Function******************************************************************** Synopsis [Get the number of state variables after applying optimization] Description [Get the number of state variables after applying optimization] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearSetEffectiveNumberOfStateVariable(Relation_t *head, int *rangeId, int *domainId, int *existStateVariable) { VarLife_t **varArray, *var; int *varType; int nRange, nDomain, nQuantify; int i; varArray = head->varArray; varType = head->varType; nRange = nDomain = nQuantify = 0; for(i=0; inVarArray; i++) { var = varArray[i]; if(varType[var->id] == 1) { if(domainId) domainId[nDomain] = var->id; nDomain++; if(existStateVariable) existStateVariable[var->id] = 1; } else if(varType[var->id] == 2) { if(rangeId) rangeId[nRange] = var->id; nRange++; if(existStateVariable) existStateVariable[var->id] = 1; } else if(varType[var->id] == 3) { nQuantify++; } else nQuantify++; } if(domainId) domainId[nDomain] = -1; if(rangeId) rangeId[nRange] = -1; head->nEffRange = nRange; head->nEffDomain = nDomain; head->nEffQuantify = nQuantify; if(head->nInitRange == 0 && head->nInitDomain == 0 && head->nInitQuantify == 0) { head->nInitRange = nRange; head->nInitDomain = nDomain; head->nInitQuantify = nQuantify; } } /**Function******************************************************************** Synopsis [Find the case that the relation contains only one next state varaible] Description [Find the case that the relation contains only one next state varaible] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearAddSingletonCase(Relation_t *head) { Conjunct_t **newConjunctArray; Conjunct_t **singletonArray; Conjunct_t *conjunct; int i, j, index; int nSingletonArray; int putFlag; nSingletonArray = head->nSingletonArray; singletonArray = head->singletonArray; if(nSingletonArray == 0) return; fprintf(stdout, "NOTICE : %d singleton case will be added\n", nSingletonArray); qsort(singletonArray, nSingletonArray, sizeof(Conjunct_t *), ImgLinearCompareConjunctRangeMinusDomain); index = 0; newConjunctArray = ALLOC(Conjunct_t *, head->nSize + nSingletonArray); putFlag = 0; for(i=0; inRange > conjunct->nSize-conjunct->nRange) { putFlag = 1; for(j=0; jnSize; j++) newConjunctArray[index++] = head->conjunctArray[j]; } newConjunctArray[index++] = singletonArray[i]; } if(putFlag == 0) { for(j=0; jnSize; j++) newConjunctArray[index++] = head->conjunctArray[j]; } head->nSize = index; head->bModified = 1; head->bRefineVarArray = 1; free(head->conjunctArray); head->conjunctArray = newConjunctArray; free(singletonArray); head->singletonArray = 0; head->nSingletonArray = 0; } /**Function******************************************************************** Synopsis [Find transtion relations that have smae support set] Description [Find transtion relations that have smae support set and use this information when finding linear arragement] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearExpandSameSupportSet(Relation_t *head) { int index, i, j; Conjunct_t **newConjunctArray; Conjunct_t *conjunct; newConjunctArray = ALLOC(Conjunct_t *, head->nSize); for(index=0, i=0; inSize; i++) { if(index >= head->nSize) newConjunctArray = REALLOC(Conjunct_t *, newConjunctArray, index+1); conjunct = head->conjunctArray[i]; newConjunctArray[index++] = conjunct; if(conjunct->nCluster) { for(j=0; jnCluster; j++) { if(index >= head->nSize) newConjunctArray = REALLOC(Conjunct_t *, newConjunctArray, index+1); newConjunctArray[index++] = conjunct->clusterArray[j]; } head->bModified = 1; head->bRefineVarArray = 1; conjunct->nCluster = 0; if(conjunct->clusterArray) { free(conjunct->clusterArray); conjunct->clusterArray = 0; } } } free(head->conjunctArray); head->conjunctArray = newConjunctArray; head->nSize = index; } /**Function******************************************************************** Synopsis [Cluster the relation that has same support set] Description [Cluster the relation that has same support set] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearClusterSameSupportSet(Relation_t *head) { int i, j, index, id; int *supList; Conjunct_t *conjunct, *base; int *varType; Conjunct_t **conjunctArray, **newConjunctArray; head->nTotalCluster = 0; varType = head->varType; conjunctArray = head->conjunctArray; for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; supList = conjunct->supList; conjunct->dummy = 0; for(j=0; jnSize; j++) { id = supList[j]; if(varType[id] == 2) continue; conjunct->dummy += id; } conjunct->dummy *= (conjunct->nSize-conjunct->nRange); conjunct->dummy -= conjunct->nDomain; } qsort(conjunctArray, head->nSize, sizeof(Conjunct_t *), ImgLinearCompareConjunctDummy); for(i=0; inSize; i++) { base = head->conjunctArray[i]; for(j=i+1; jnSize; j++) { conjunct = head->conjunctArray[j]; if(base->dummy != conjunct->dummy) { if(j == i+1) break; ImgLinearFindSameSupportConjuncts(head, i, j-1); i = j-1; break; } } } if(head->bModified) { conjunctArray = head->conjunctArray; newConjunctArray = ALLOC(Conjunct_t *, head->nSize); for(index=0, i=0; inSize; i++) { conjunct = conjunctArray[i]; if(conjunct == 0) continue; newConjunctArray[index++] = conjunct; } free(conjunctArray); head->conjunctArray = newConjunctArray; head->nSize = index; head->bModified = 1; head->bRefineVarArray = 1; } conjunctArray = head->conjunctArray; qsort(conjunctArray, head->nSize, sizeof(Conjunct_t *), ImgLinearCompareConjunctIndex); if(head->bModified) { conjunctArray = head->conjunctArray; for(i=0; inSize; i++) { conjunct = conjunctArray[i]; if(conjunct == 0) continue; conjunct->index = i; } } fprintf(stdout, "NOTICE : %d conjunct clustered\n", head->nTotalCluster); head->nTotalCluster = 0; } /**Function******************************************************************** Synopsis [Find the conjuncts that have same support variables.] Description [Find the conjuncts that have same support variables.] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearFindSameSupportConjuncts(Relation_t *head, int from, int to) { Conjunct_t *con1, *con2; int i, j; for(i=from; i<=to; i++) { con1 = head->conjunctArray[i]; if(con1 == 0) continue; for(j=from; j<=to; j++) { if(i == j) continue; con2 = head->conjunctArray[j]; if(con2 == 0) continue; if(ImgLinearIsSameConjunct(head, con1, con2)) { ImgLinearAddConjunctIntoClusterArray(con1, con2); head->conjunctArray[j] = 0; head->bModified = 1; head->bRefineVarArray = 1; head->nTotalCluster++; } } } } /**Function******************************************************************** Synopsis [Check if given conjuncts have same support variables] Description [Check if given conjuncts have same support variables] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgLinearIsSameConjunct(Relation_t *head, Conjunct_t *con1, Conjunct_t *con2) { int i, j; int *sup1, *sup2; int id1, id2; int *varType; if(con1->nDomain != con2->nDomain) return(0); if(con1->nSize-con1->nRange != con2->nSize-con2->nRange) return(0); sup1 = con1->supList; sup2 = con2->supList; varType = head->varType; for(j=0, i=0; inSize; i++) { id1 = sup1[i]; if(varType[id1] == 2)continue; while(1) { id2 = sup2[j]; if(varType[id2] == 2) { j++; continue; } if(id1 != id2) return(0); j++; break; } } return(1); } /**Function******************************************************************** Synopsis [Add conjunct into array] Description [Add conjunct into array] SideEffects [] SeeAlso [] ******************************************************************************/ static Conjunct_t ** ImgLinearAddConjunctIntoArray(Conjunct_t **array, int *nArray, Conjunct_t *con) { if(array) array = REALLOC(Conjunct_t *, array, (*nArray)+1); else array = ALLOC(Conjunct_t *, (*nArray)+1); array[(*nArray)++] = con; return(array); } /**Function******************************************************************** Synopsis [Free conjunct_t data structure] Description [Free conjunct_t data structure] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearConjunctQuit(Conjunct_t *conjunct) { if(conjunct->supList) { free(conjunct->supList); conjunct->supList = 0; } if(conjunct->relation) { bdd_free(conjunct->relation); conjunct->relation = 0; } free(conjunct); } /**Function******************************************************************** Synopsis [Free variable array] Description [Free variable array] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearVariableArrayQuit(Relation_t *head) { int i; VarLife_t **varArray; varArray = head->varArray; for(i=0; inVarArray; i++) ImgLinearVariableLifeQuit(varArray[i]); free(varArray); head->varArray = 0; head->nVarArray = 0; memset(head->varArrayMap, -1, sizeof(int)*head->nVar); } /**Function******************************************************************** Synopsis [Free variable life array] Description [Free variable lifearray] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearVariableLifeQuit(VarLife_t *var) { if(var->relArr) free(var->relArr); free(var); } /**Function******************************************************************** Synopsis [Main function of clustering] Description [Main function of clustering] SideEffects [] SeeAlso [] ******************************************************************************/ int ImgLinearClustering(Relation_t *head, Img_OptimizeType optDir) { int andExistLimit; int useFailureHistory; int includeZeroGain; double affinityLimit; int bOptimize; int varLimit; bOptimize = 0; affinityLimit = 0.99; andExistLimit = 10; varLimit = 200; fprintf(stdout, "Heap DAL affinity %3f, andExist %d\n", affinityLimit, andExistLimit); bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit, varLimit, optDir, 0, ImgLinearHeapCompareDeadAffinityLive); ImgLinearRefineRelation(head); if(head->verbosity >= 5) ImgLinearPrintMatrix(head); ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0); ImgLinearPrintTransitionInfo(head); includeZeroGain = 0; affinityLimit = 0.3; andExistLimit = 5000; varLimit = 50; useFailureHistory = 0; if(head->computeRange) { varLimit = 50; affinityLimit = 0.8; andExistLimit = 5000; fprintf(stdout, "Heap DAL affinity %3f, andExist %d\n", affinityLimit, andExistLimit); bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit, varLimit, optDir, 0, ImgLinearHeapCompareDeadAffinityLive); ImgLinearRefineRelation(head); ImgLinearExtractNextStateCase(head); ImgLinearExtractSingletonCase(head); ImgLinearRefineRelation(head); ImgLinearAddSingletonCase(head); ImgLinearRefineRelation(head); ImgLinearAddNextStateCase(head); ImgLinearRefineRelation(head); } else { fprintf(stdout, "Gain DAL affinity %3f, andExist %d\n", affinityLimit, andExistLimit); bOptimize |= ImgLinearClusteringIteratively(head, affinityLimit, andExistLimit, varLimit, includeZeroGain, useFailureHistory, optDir, ImgLinearCompareDeadAffinityLive); ImgLinearRefineRelation(head); ImgLinearExtractNextStateCase(head); ImgLinearExtractSingletonCase(head); ImgLinearRefineRelation(head); ImgLinearAddSingletonCase(head); ImgLinearRefineRelation(head); ImgLinearAddNextStateCase(head); ImgLinearRefineRelation(head); } includeZeroGain = 1; varLimit = 200; affinityLimit = 0.7; andExistLimit = 5000; fprintf(stdout, "Heap DAL affinity %3f, andExist %d\n", affinityLimit, andExistLimit); bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit, varLimit, optDir, 0, ImgLinearHeapCompareDeadAffinityLive); ImgLinearRefineRelation(head); ImgLinearExtractNextStateCase(head); ImgLinearExtractSingletonCase(head); ImgLinearRefineRelation(head); ImgLinearAddSingletonCase(head); ImgLinearRefineRelation(head); ImgLinearAddNextStateCase(head); ImgLinearRefineRelation(head); if(head->verbosity >= 5) ImgLinearPrintMatrix(head); ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0); ImgLinearPrintTransitionInfo(head); includeZeroGain = 1; affinityLimit = 0.4; andExistLimit = 5000; fprintf(stdout, "Heap DAL affinity %3f, andExist %d\n", affinityLimit, andExistLimit); bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit, varLimit, optDir, 0, ImgLinearHeapCompareDeadAffinityLive); ImgLinearRefineRelation(head); ImgLinearExtractNextStateCase(head); ImgLinearExtractSingletonCase(head); ImgLinearRefineRelation(head); ImgLinearAddSingletonCase(head); ImgLinearRefineRelation(head); ImgLinearAddNextStateCase(head); ImgLinearRefineRelation(head); if(head->verbosity >= 5) ImgLinearPrintMatrix(head); ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0); ImgLinearPrintTransitionInfo(head); affinityLimit = 0.0; andExistLimit = 5000; fprintf(stdout, "Heap DLA affinity %3f, andExist %d\n", affinityLimit, andExistLimit); bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit, varLimit, optDir, 0, ImgLinearHeapCompareDeadLiveAffinity); ImgLinearRefineRelation(head); ImgLinearExtractNextStateCase(head); ImgLinearRefineRelation(head); ImgLinearAddNextStateCase(head); ImgLinearRefineRelation(head); if(head->verbosity >= 5) ImgLinearPrintMatrix(head); ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0); ImgLinearPrintTransitionInfo(head); if(head->computeRange) { includeZeroGain = 0; affinityLimit = 0.0; andExistLimit = andExistLimit; varLimit = MAXINT; head->bddLimit = head->bddLimit * 2; fprintf(stdout, "Heap DLA affinity %3f, andExist %d\n", affinityLimit, andExistLimit); while(1) { bOptimize |= ImgLinearClusterUsingHeap(head, affinityLimit, andExistLimit, varLimit, optDir, 1, ImgLinearHeapCompareDeadLiveAffinity); ImgLinearRefineRelation(head); if(ImgCheckRangeTestAndOverapproximate(head)) break; } ImgCountOnsetDisjunctiveArray(head); ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0); ImgLinearPrintTransitionInfo(head); } return(bOptimize); } /**Function******************************************************************** Synopsis [Count onset of relation array] Description [Count onset of relation array] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgCountOnsetDisjunctiveArray(Relation_t *head) { EpDouble tepd; char strValue[1024]; bdd_t *varBdd; mdd_manager *mgr; array_t *bddVarArray; Conjunct_t *conjunct; int count, i, j, id; double onSet; mgr = head->mgr; count = 0; EpdConvert((double)1.0, &tepd); for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; bddVarArray = array_alloc(bdd_t *, 0); for(j=0; jnSize; j++) { id = conjunct->supList[j]; varBdd = bdd_get_variable(mgr, id); array_insert_last(bdd_t *, bddVarArray, varBdd); } /** bdd_epd_count_onset(conjunct->relation, bddVarArray, &epd); EpdMultiply2(&tepd, &epd); **/ onSet = bdd_count_onset(conjunct->relation, bddVarArray); EpdMultiply(&tepd, onSet); count += conjunct->nSize; mdd_array_free(bddVarArray); } if(count < head->nRange) { EpdMultiply(&tepd, pow(2, (double)(head->nRange-count))); } EpdGetString(&tepd, strValue); (void) fprintf(vis_stdout, "%-20s%10s\n", "range =", strValue); } /**Function******************************************************************** Synopsis [Check range of variables] Description [Check range of variables] SideEffects [] SeeAlso [] ******************************************************************************/ static int ImgCheckRangeTestAndOverapproximate(Relation_t *head) { Conjunct_t *conjunct; VarLife_t **varArray, *var; int nVarArray, i, k, count; int index; int *varType; int allRangeFlag; bdd_t *relation, *simpleRelation, *varBdd; allRangeFlag = 1; for(i=0; inSize; i++) { conjunct = head->conjunctArray[i]; if(conjunct->nRange != conjunct->nSize) { allRangeFlag = 0; break; } } if(allRangeFlag == 1) return(1); varArray = head->varArray; varType = head->varType; nVarArray = head->nVarArray; /** maxIndex = -1; maxSize = 0; for(i=0; iid] == 2) continue; if(var->nSize > maxSize) { maxIndex = i; maxSize = var->nSize; } } if(maxIndex == -1) return(1); **/ count = head->nEffDomain + head->nEffQuantify; if(count == 0) return(1); varArray = ALLOC(VarLife_t *, head->nVarArray); memcpy(varArray, head->varArray, sizeof(VarLife_t *)*head->nVarArray); qsort(varArray, head->nVarArray, sizeof(VarLife_t *), ImgLinearCompareVarSize); if(count != 0) { count = (count / 10); if(count == 0) count = 1; } k=0; index = 0; while(1) { if(index >= count) break; var = varArray[k++]; if(var->stateVar == 2) continue; index++; varBdd = bdd_get_variable(head->mgr, var->id); for(i=0; inSize; i++) { conjunct = head->conjunctArray[var->relArr[i]]; relation = conjunct->relation; simpleRelation = bdd_smooth_with_cube(relation, varBdd); if(bdd_equal(relation, simpleRelation)) { bdd_free(simpleRelation); continue; } bdd_free(relation); conjunct->relation = simpleRelation; conjunct->bModified = 1; head->bModified = 1; head->bRefineVarArray = 1; ImgLinearConjunctRefine(head, conjunct); } } free(varArray); ImgLinearRefineRelation(head); ImgLinearConjunctOrderMainCC(head, 0); ImgLinearRefineRelation(head); ImgLinearSetEffectiveNumberOfStateVariable(head, 0, 0, 0); ImgLinearPrintTransitionInfo(head); return(0); } /**Function******************************************************************** Synopsis [Add singleton next state variable case into array] Description [Add singleton next state variable case into array] SideEffects [] SeeAlso [] ******************************************************************************/ static void ImgLinearAddNextStateCase(Relation_t *head) { Conjunct_t **newConjunctArray; int i, j, index; index = 0; if(head->nNextStateArray) { newConjunctArray = ALLOC(Conjunct_t *, head->nSize + head->nNextStateArray); for(j=0; jnSize; j++) newConjunctArray[index++] = head->conjunctArray[j]; for(i=0; inNextStateArray; i++) newConjunctArray[index++] = head->nextStateArray[i]; head->nSize = index; head->bModified = 1; head->bRefineVarArray = 1; free(head->conjunctArray); head->conjunctArray = newConjunctArray; if(head->nextStateArray) free(head->nextStateArray); head->nextStateArray = 0; } }