To add a new method, called "foo", follow these steps. 1) describe the foo method in the Description field at the top of img.h. 2) Add Img_Foo_c to the Img_MethodType enumerated type. 3) Create a file, imgFoo.c, and define the following functions: ImgImageInfoInitializeFoo, ImgImageInfoComputeFwdFoo, ImgImageInfoComputeBwdFoo, ImgImageInfoFreeFoo. 4) In the function Img_ImageInfoInitialize, add the case "foo" for the "image_method" flag, and add the case Img_Foo_c to the switch for initialization. 

static void 
AddDontCareToTransitionFunction(
  array_t * vector, 
  array_t * relationArray, 
  mdd_t * constrain, 
  Img_MinimizeType  minimizeMethod, 
  int  printStatus 
)
Adds dont cares to function vector or relation.

Defined in imgTfm.c 

static array_t * 
BddArrayDup(
  array_t * bddArray 
)
Duplicates an array of BDDs.

Defined in imgIwls95.c 

static mdd_t * 
BddLinearAndSmooth(
  mdd_manager * mddManager, 
  bdd_t * fromSet, 
  array_t * relationArray, 
  array_t * arraySmoothVarBddArray, 
  array_t * smoothVarCubeArray, 
  int  verbosity, 
  ImgPartialImageOption_t * PIoption, 
  boolean * partial, 
  boolean  lazySiftFlag 
)
The product is taken from the left, i.e., fromSet is multiplied with relationArray[0

Side Effects partial is set when some approximation is applied

Defined in imgIwls95.c 

static void 
BlockLowerTriangle(
  char ** xy, 
  int  nRows, 
  int  nCols, 
  int  nActiveRows, 
  int  nActiveCols, 
  SccList_t * sccList, 
  int * rowOrder, 
  int * colOrder, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  ImgTrmOption_t * option 
)
Makes dependence matrix block lower triangle by pivoting rows and columns.

Defined in imgMlp.c 

static void 
CacheDestroyEntry(
  ImgCacheEntry_t * entry, 
  boolean  freeEntry 
)
Destroys a cache entry.

Defined in imgTfmCache.c 

static float 
CalculateBenefit(
  CtrInfo_t * ctrInfo, 
  int  maxNumLocalSmoothVars, 
  int  maxNumSmoothVars, 
  int  maxIndex, 
  int  maxNumIntroducedVars, 
  ImgTrmOption_t * option 
)
The strategy Choose the cost function: The objective function attached with each Ti is Ci = W1 C1i + W2 C2i + W3 C3i - W4C4i where: W1 = weight attached with variable getting smoothed W2 = weight attached with the support count of the Ti W3 = weight attached with the max id of the Ti W4 = weight attached with variable getting introduced C1i = Ui/Vi C2i = Vi/Wi C3i = Mi/Max C4i = Xi/Yi Ui = number of variables getting smoothed Vi = number of ps support variables of Ti Wi = total number of ps variables remaining which have not been smoothed out Mi = value of Max id of Ti Max = value of Max id across all the Ti's remaining to be multiplied Xi = number of ns variables introduced Yi = total number of ns variables which have not been introduced so far. Get the weights from the global option

Defined in imgIwls95.c 

static void 
CheckCluster(
  ClusterList_t * headCluster, 
  int  nCols, 
  RcInfo_t * colInfo, 
  int * colOrder 
)
Checks cluster for sanity.

Defined in imgMlp.c 

static int 
CheckCtrInfoArray(
  array_t * ctrInfoArray, 
  int  numDomainVars, 
  int  numQuantifyVars, 
  int  numRangeVars 
)
Checks the validity of an array of CtrInfoStructs.

Defined in imgIwls95.c 

static int 
CheckCtrInfo(
  CtrInfo_t * ctrInfo, 
  int  numDomainVars, 
  int  numQuantifyVars, 
  int  numRangeVars 
)
Checks the validity of a CtrInfoStruct.

Defined in imgIwls95.c 

static int 
CheckIfValidSplitOrGetNew(
  ImgTfmInfo_t * info, 
  int  split, 
  array_t * vector, 
  array_t * relationArray, 
  mdd_t * from 
)
Checks the splitting variable is already quantified from the transition relation. If yes, chooses new splitting variable. If there is no valid splitting variable, returns -1.

Defined in imgTfmFwd.c 

static int 
CheckImageValidity(
  mdd_manager * mddManager, 
  mdd_t * image, 
  array_t * domainVarMddIdArray, 
  array_t * quantifyVarMddIdArray 
)
In a properly formed image, there should not be any domain or quantify variables in its support. This function checks for that fact.

Defined in imgUtil.c 

static void 
CheckMatrix(
  char ** xy, 
  SccList_t * sccList, 
  int  nRows, 
  int  nCols, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  int  startFunc, 
  int  lastFunc, 
  int  startVar, 
  int  lastVar, 
  int  local 
)
Checks a matrix for sanity.

Defined in imgMlp.c 

static int 
CheckNondeterminism(
  Ntk_Network_t * network 
)
Checks whether the network is nondeterministic. However, current implementatin is just checking whether the network has multi-valued variables.

Defined in imgTfm.c 

static int 
CheckPreImageVector(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * image 
)
Checks sanity of a vector for preimage.

Defined in imgTfmBwd.c 

static int 
CheckQuantificationSchedule(
  array_t * relationArray, 
  array_t * arraySmoothVarBddArray 
)
Assume Ci represents the ith cube in the array and the Ti represents the ith relation. The correctness of the schedule is defined as follows: a. For all Tj: j > i, SUP(Tj) and SUP(Ci) do not intersect, i.e., the variables which are quantified in Ci should not appear in the Tj for j>i. b. For any i, j, SUP(Ci) and SUP(Cj) do not intersect. However this is not true for the last cube (Cn-1). This is because the last cube contains all the smooth variables.

Defined in imgIwls95.c 

static void 
CheckSortedList(
  RcListInfo_t * candList, 
  RcInfo_t * info, 
  int  method 
)
Checks the sorting list for sanity.

Defined in imgMlp.c 

static int 
CheckVarInfoArray(
  array_t * varInfoArray, 
  int  numRelation 
)
Checks the validity of an array of VarInfoStruct.

Defined in imgIwls95.c 

static int 
ChooseInputSplittingVariable(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * from, 
  int  splitMethod, 
  int  decompose, 
  int  piSplitFlag, 
  int * varOccur 
)
Finds a splitting variable for input splitting.

Defined in imgTfmFwd.c 

static int 
ChooseOutputSplittingVariable(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  int  splitMethod 
)
Finds a splitting variable for output splitting.

Defined in imgTfmFwd.c 

static array_t * 
ChoosePartialVars(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  int  nPartialVars, 
  int  partialMethod 
)
Chooses variables for static splitting. partialMethod is set by hybrid_partial_method. Refer to print_hybrid_options command.

Defined in imgTfm.c 

static ClusterSortedList_t * 
ClusterSortedListInsert(
  ClusterSortedList_t * clusterSortedList, 
  ClusterList_t * list, 
  int  useQuantifyVars 
)
Inserts a cluster in a sorting list.

Defined in imgMlp.c 

static int 
CompareBddPointer(
  const void * e1, 
  const void * e2 
)
Compares two function BDD pointers of components.

Defined in imgTfmUtil.c 

static int 
CompareIndex(
  const void * e1, 
  const void * e2 
)
Compares two variable indices of components.

Defined in imgTfm.c 

static bdd_t * 
ComputeClippedAndAbstract(
  bdd_t * product, 
  bdd_t * relation, 
  array_t * smoothVarBddArray, 
  int  nvars, 
  int  clippingDepth, 
  boolean * partial, 
  int  verbosity 
)
Compute clipping and-abstract. Try twice. If fail, compute exact and-abstract

Side Effects partial flag is modified.

Defined in imgIwls95.c 

static float 
ComputeLambdaMlp(
  char ** xy, 
  int  nVars, 
  int  nRows, 
  int  nCols, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  Img_DirectionType  direction, 
  int  mode, 
  int  asIs, 
  ImgTrmOption_t * option 
)
Compute variable lifetime lambda.

Defined in imgMlp.c 

static bdd_t * 
ComputeSubsetOfIntermediateProduct(
  bdd_t * product, 
  ImgPartialImageOption_t * PIoption 
)
Approximate intermediate product according to method.

Defined in imgIwls95.c 

static float 
ComputeSupportLambda(
  ImgTfmInfo_t * info, 
  array_t * relationArray, 
  mdd_t * cofactorCube, 
  mdd_t * abstractCube, 
  mdd_t * from, 
  array_t * vector, 
  int  newRelationFlag, 
  int  preFlag, 
  float * improvedLambda 
)
Computes variable lifetime lambda. newRelationFlag is 1 when relationArray is made from the function vector directly, in other words, relationArray is an array of next state functions in this case.

Defined in imgHybrid.c 

static array_t * 
CopyArrayBddArray(
  array_t * arrayBddArray 
)
Copy an array of bdd array.

Defined in imgIwls95.c 

static int 
CountClusterList(
  ClusterList_t * clusterList 
)
Returns the number of lists in a cluster list.

Defined in imgMlp.c 

static int 
CountClusterSortedList(
  ClusterSortedList_t * clusterSortedList 
)
Returns the number of lists in a sorted cluster list.

Defined in imgMlp.c 

static void 
CreateBitRelationArray(
  Iwls95Info_t * info, 
  ImgFunctionData_t * functionData 
)
Creates the bit relations and the mdd id array for the quantifiable variables and stores it in the ImgIwls95 structure. This is identical to the initialize procedure. Read the roots (next state mdds), compute the bit relations for each root. If there are some intermediate variables, add them to quantifiable vars.

Side Effects bitRelationArray and quantifyVarMddIdArray fields are modified of the Iwls95Info_t struct.

See Also ImgImageInfoInitializeIwls95
Defined in imgIwls95.c 

static array_t * 
CreateClusters(
  bdd_manager * bddManager, 
  array_t * relationArray, 
  ImgTrmOption_t * option 
)
The clusters are formed by taking the product in order. Once the BDD size of the cluster reaches a threshold, a new cluster is started.

Defined in imgIwls95.c 

static array_t * 
CreateInitialCluster(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  ImgFunctionData_t * functionData, 
  array_t * nsVarBddArray, 
  ImgTrmOption_t * option 
)
Creates an initial cluster using ARDC decomposition.

Defined in imgMlp.c 

static int 
CtrInfoMaxIndexCompare(
  const void * p1, 
  const void * p2 
)
This function is used to sort the array of clusters based on the maximum index of the support variable.

Defined in imgIwls95.c 

static CtrInfo_t * 
CtrInfoStructAlloc(
    
)
Allocates and initializes memory for ctrInfoStruct.

Defined in imgIwls95.c 

static void 
CtrInfoStructFree(
  CtrInfo_t * ctrInfo 
)
Frees the memory associated with ctrInfoStruct.

Defined in imgIwls95.c 

static void 
CtrItemStructFree(
  CtrItem_t * ctrItem 
)
Frees the memory associated with CtrItemStruct

Defined in imgIwls95.c 

static mdd_t * 
DomainCofactoring(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * from, 
  array_t * relationArray, 
  mdd_t * c, 
  array_t ** newVector, 
  array_t ** newRelationArray, 
  mdd_t ** cofactorCube, 
  mdd_t ** abstractCube 
)
Performs domain cofactoring on a vector and from set with respect to a variable.

Defined in imgTfmBwd.c 

static void 
FindAndMoveSingletonCols(
  char ** xy, 
  SccList_t * sccList, 
  int  nRows, 
  int  nCols, 
  int * startFunc, 
  int * lastFunc, 
  int * startVar, 
  int * lastVar, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  ImgTrmOption_t * option 
)
Finds and moves singleton columns.

Defined in imgMlp.c 

static void 
FindAndMoveSingletonRows(
  char ** xy, 
  SccList_t * sccList, 
  int  nRows, 
  int  nCols, 
  int * startFunc, 
  int * lastFunc, 
  int * startVar, 
  int * lastVar, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  ImgTrmOption_t * option 
)
Finds and moves singleton rows.

Defined in imgMlp.c 

static int 
FindDecomposableVariable(
  ImgTfmInfo_t * info, 
  array_t * vector 
)
Finds a decomposable variable (articulation)

Defined in imgTfmFwd.c 

static void 
FindIntermediateSupport(
  array_t * vector, 
  ImgComponent_t * comp, 
  int  nVars, 
  int  nGroups, 
  int * stack, 
  char * stackFlag, 
  int * funcGroup, 
  int * size, 
  char * intermediateVarFlag, 
  int * intermediateVarFuncMap 
)
Finds all other fanin intermediate functions of a given intermediate function. Adds the only intermediate functions are not in the stack. Updates the stack information.

Defined in imgTfmFwd.c 

static void 
FindIntermediateVarsRecursively(
  ImgTfmInfo_t * info, 
  mdd_manager * mddManager, 
  vertex_t * vertex, 
  int  mddId, 
  st_table * vertexTable, 
  array_t * vector, 
  st_table * domainQuantifyVarMddIdTable, 
  array_t * intermediateVarMddIdArray 
)
Traverses the partition recursively, creating the functions for the intermediate vertices. This function is originated from PartitionTraverseRecursively in imgIwls95.c

Defined in imgTfm.c 

static void 
FreeBitRelationArray(
  Iwls95Info_t * info 
)
Frees bit relation array and quantification variables. Important: to set these field to NIL in case of reuse.

Side Effects Also frees the quantifVarMddIdArray field.

Defined in imgIwls95.c 

static void 
FreeClusteredCofactoredRelationArray(
  Iwls95Info_t * info 
)
Frees the clusteredCofactoredRelationArray, and the careSetArray, and sets them to NIL to signify that they are invalid.

Defined in imgIwls95.c 

static void 
FreeSccList(
  SccList_t * sccHeadList 
)
Frees list of connected components.

Defined in imgMlp.c 

static void 
GetIntermediateRelationsRecursively(
  mdd_manager * mddManager, 
  vertex_t * vertex, 
  int  mddId, 
  st_table * vertexTable, 
  array_t * relationArray, 
  st_table * domainQuantifyVarMddIdTable, 
  array_t * intermediateVarMddIdArray 
)
Traverses the partition recursively, creating the relations for the intermediate vertices. This function is a copy of PartitionTraverseRecursively from imgIwls95.c.

Defined in imgTfm.c 

static void 
GetRecursionStatistics(
  ImgTfmInfo_t * info, 
  int  preFlag, 
  int * nRecurs, 
  int * nLeaves, 
  int * nTurns, 
  float * averageDepth, 
  int * maxDepth, 
  int * nDecomps, 
  int * topDecomp, 
  int * maxDecomp, 
  float * averageDecomp 
)
Returns the statistics of recursions of transition function method.

Defined in imgTfm.c 

static void 
HashIdToBddTable(
  st_table * table, 
  array_t * idArray, 
  array_t * bddArray 
)
The elements of the input array should be in one to one correpondence, i.e., idArray[i

Defined in imgIwls95.c 

static int 
HookInfoFunction(
  bdd_manager * mgr, 
  char * str, 
  void * method 
)
Flushes cache entries in a list.

Defined in imgTfm.c 

static mdd_t * 
ImageByInputSplit(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * constraint, 
  mdd_t * from, 
  array_t * relationArray, 
  mdd_t * cofactorCube, 
  mdd_t * abstractCube, 
  int  splitMethod, 
  int  turnDepth, 
  int  depth 
)
Computes an image by input splitting.

Defined in imgTfmFwd.c 

static mdd_t * 
ImageByOutputSplit(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * constraint, 
  int  depth 
)
Computes an image by output splitting.

Defined in imgTfmFwd.c 

static mdd_t * 
ImageByStaticInputSplit(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * from, 
  array_t * relationArray, 
  int  turnDepth, 
  int  depth 
)
Computes an image by static input splitting.

Defined in imgTfmFwd.c 

static mdd_t * 
ImageComputeMonolithic(
  mdd_t * methodData, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray, 
  array_t * smoothVars, 
  mdd_t * smoothCube 
)
This is a routine for image computation which is called by both forward image and backward image computation. The frontier set (the set of states for which the image is computed) is obtained by finding a small size BDD between lower and upper bounds. The transition relation is simplified by cofactoring it with the domainSubset (frontier set) and with the toCareSet. The order in which this simplification is unimportant from functionality point of view, but the order might effect the BDD size of the optimizedRelation. smoothVars should be an array of bdd variables.

Defined in imgMonolithic.c 

static int 
ImageDecomposeAndChooseSplitVar(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * from, 
  int  splitMethod, 
  int  split, 
  int  piSplitFlag, 
  array_t * vectorArray, 
  array_t * varArray, 
  mdd_t ** singles, 
  array_t * relationArray, 
  array_t ** newRelationArray, 
  mdd_t ** cofactorCube, 
  mdd_t ** abstractCube 
)
Try to decompose function vector and find a splitting variable for each decomposed block.

Defined in imgTfmFwd.c 

static mdd_t * 
ImageFast2(
  ImgTfmInfo_t * info, 
  array_t * vector 
)
Fast image computation when function vector contains only two functions.

Defined in imgTfmFwd.c 

static int 
ImageKeyCompare(
  ImgCacheStKey_t * key1, 
  ImgCacheStKey_t * key2 
)
Compares two keys.

Defined in imgTfmCache.c 

static int 
ImageKeySortCompare(
  ImgCacheStKey_t * key1, 
  ImgCacheStKey_t * key2 
)
Compares two keys considering substitution.

Defined in imgTfmCache.c 

void 
ImgAbstractRelationArray(
  mdd_manager * manager, 
  array_t * relationArray, 
  mdd_t * cube 
)
Smoothes a relation array with respect to a cube.

Defined in imgTfmUtil.c 

void 
ImgAbstractTransitionFunction(
  Img_ImageInfo_t * imageInfo, 
  array_t * abstractVars, 
  mdd_t * abstractCube, 
  Img_DirectionType  directionType, 
  int  printStatus 
)
Abstracts out given variables from transition function. abstractVars should be an array of bdd variables.

Defined in imgTfm.c 

void 
ImgAbstractTransitionRelationIwls95(
  Img_ImageInfo_t * imageInfo, 
  array_t * abstractVars, 
  mdd_t * abstractCube, 
  Img_DirectionType  directionType, 
  int  printStatus 
)
Abstracts out given variables from transition relation. abstractVars should be an array of bdd variables. This invalidates the bwdclusteredcofactoredrelationarray.

See Also ImgMinimizeTransitionRelationIwls95 ImgApproximateTransitionRelationIwls95 ImgAbstractTransitionRelationIwls95
Defined in imgIwls95.c 

void 
ImgAbstractTransitionRelationMono(
  Img_ImageInfo_t * imageInfo, 
  array_t * abstractVars, 
  mdd_t * abstractCube, 
  int  printStatus 
)
Abstracts out given variables from transition relation. abstractVars should be an array of bdd variables.

Defined in imgMonolithic.c 

void 
ImgAddDontCareToTransitionFunction(
  void * methodData, 
  array_t * constrainArray, 
  Img_MinimizeType  minimizeMethod, 
  Img_DirectionType  directionType, 
  int  printStatus 
)
Adds a dont care set to the transition function and relation. This function is called during guided search.

Defined in imgTfm.c 

void 
ImgAddDontCareToTransitionRelationMono(
  Img_ImageInfo_t * imageInfo, 
  array_t * constrainArray, 
  Img_MinimizeType  minimizeMethod, 
  int  printStatus 
)
Add dont care to transition relation. The constrain array contains care sets.

Defined in imgMonolithic.c 

int 
ImgApproximateTransitionFunction(
  mdd_manager * mgr, 
  void * methodData, 
  bdd_approx_dir_t  approxDir, 
  bdd_approx_type_t  approxMethod, 
  int  approxThreshold, 
  double  approxQuality, 
  double  approxQualityBias, 
  Img_DirectionType  directionType, 
  mdd_t * bias 
)
Approximate transition function.

Defined in imgTfm.c 

int 
ImgApproximateTransitionRelationIwls95(
  mdd_manager * mgr, 
  void * methodData, 
  bdd_approx_dir_t  approxDir, 
  bdd_approx_type_t  approxMethod, 
  int  approxThreshold, 
  double  approxQuality, 
  double  approxQualityBias, 
  Img_DirectionType  directionType, 
  mdd_t * bias 
)
Approximate transition relation. This invalidates the bwdclusteredcofactoredrelationarray.

Side Effects ImgMinimizeTransitionRelationIwls95, ImgApproximateTransitionRelationIwls95, ImgAbstractTransitionRelationIwls95, Img_ApproximateImage

Defined in imgIwls95.c 

int 
ImgApproximateTransitionRelationMono(
  mdd_manager * mgr, 
  Img_ImageInfo_t * imageInfo, 
  bdd_approx_dir_t  approxDir, 
  bdd_approx_type_t  approxMethod, 
  int  approxThreshold, 
  double  approxQuality, 
  double  approxQualityBias, 
  mdd_t * bias 
)
Approximates transition relation.

Defined in imgMonolithic.c 

int 
ImgArrayBddArrayCheckValidity(
  array_t * arrayBddArray 
)
This function checks the validity of an array of array of BDD nodes.

See Also ImgBddCheckValidity
Defined in imgUtil.c 

int 
ImgBddArrayCheckValidity(
  array_t * bddArray 
)
This function checks the validity of array of BDD nodes.

See Also ImgBddCheckValidity
Defined in imgUtil.c 

int 
ImgBddCheckValidity(
  bdd_t * bdd 
)
[This function checks the validity of a BDD. Three checks are done: 1. The BDD should not be freed. "free" field should be 0. 2. The node pointer of the BDD should be a valid pointer. 3. The manager pointer of the BDD should be a valid pointer. The assumption for 2 and 3 is that, the value of a valid pointer should be > 0xf.

Defined in imgUtil.c 

st_table * 
ImgBddGetSupportIdTable(
  bdd_t * function 
)
Returns the st_table containing the bdd id of the support variables of the function.

Defined in imgIwls95.c 

mdd_t* 
ImgBddLinearAndSmooth(
  mdd_manager * mddManager, 
  mdd_t * from, 
  array_t * relationArray, 
  array_t * arraySmoothVarBddArray, 
  array_t * smoothVarCubeArray, 
  int  verbosity 
)
The product is taken from the left, i.e., fromSet is multiplied with relationArray[0

Side Effects None

Defined in imgIwls95.c 

void 
ImgCacheDestroyTable(
  ImgCacheTable_t * table, 
  int  globalCache 
)
Destroys a cache table.

Defined in imgTfmCache.c 

void 
ImgCacheInitTable(
  ImgTfmInfo_t * info, 
  int  num_slot, 
  int  globalCache, 
  boolean  preImgFlag 
)
Initializes a cache table.

Defined in imgTfmCache.c 

void 
ImgCacheInsertTable(
  ImgCacheTable_t * table, 
  array_t * delta, 
  bdd_t * constraint, 
  bdd_t * result 
)
Inserts an entry into cache table.

Defined in imgTfmCache.c 

bdd_t * 
ImgCacheLookupTable(
  ImgTfmInfo_t * info, 
  ImgCacheTable_t * table, 
  array_t * delta, 
  bdd_t * constraint 
)
Lookups cache table.

Defined in imgTfmCache.c 

void 
ImgCheckConstConstrain(
  mdd_t * f1, 
  mdd_t * f2, 
  int * f21p, 
  int * f21n 
)
Quick checking whether the results of constrain between two functions are constant. Assumes that 1) f1 != f2 and f1 != f2', and 2) neither f1 nor f2 is constant.

Defined in imgTfmUtil.c 

int 
ImgCheckEquivalence(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  array_t * relationArray, 
  mdd_t * cofactorCube, 
  mdd_t * abstractCube, 
  int  preFlag 
)
Checks whether a vector is equivalent to a relation array.

Defined in imgHybrid.c 

int 
ImgCheckMatching(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  array_t * relationArray 
)
Checks whether a vector corresponds to its relation array. This function is used only for debugging with image_cluster_size = 1. Checks each function vector whether its relation exists in the transition relation.

Defined in imgHybrid.c 

static int 
ImgCheckRangeTestAndOverapproximate(
  Relation_t * head 
)
Check range of variables

Defined in imgLinear.c 

int 
ImgCheckToCareSetArrayChanged(
  array_t * toCareSetArray1, 
  array_t * toCareSetArray2 
)
Checks whether toCareSetArray changed.

Defined in imgUtil.c 

mdd_t * 
ImgChooseTrSplitVar(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  array_t * relationArray, 
  int  trSplitMethod, 
  int  piSplitFlag 
)
Chooses splitting variables for static splitting.

Defined in imgTfmFwd.c 

array_t * 
ImgClusterRelationArray(
  mdd_manager * mddManager, 
  ImgFunctionData_t * functionData, 
  Img_MethodType  method, 
  Img_DirectionType  direction, 
  ImgTrmOption_t * option, 
  array_t * relationArray, 
  array_t * domainVarBddArray, 
  array_t * quantifyVarBddArray, 
  array_t * rangeVarBddArray, 
  array_t ** arraySmoothVarBddArray, 
  array_t ** smoothVarCubeArray, 
  boolean  freeRelationArray 
)
Orders and clusters relation array and makes quantification schedule. (Order/Cluster/Order.)

Defined in imgIwls95.c 

void 
ImgCofactorRelationArray(
  array_t * relationArray, 
  mdd_t * func 
)
Cofactors a relation array with respect to a function.

Defined in imgTfmUtil.c 

void 
ImgCofactorVector(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * func 
)
Cofactors a function vector with respect to a function.

Defined in imgTfmUtil.c 

ImgComponent_t * 
ImgComponentAlloc(
  ImgTfmInfo_t * info 
)
Allocates a component.

Defined in imgTfmUtil.c 

ImgComponent_t * 
ImgComponentCopy(
  ImgTfmInfo_t * info, 
  ImgComponent_t * comp 
)
Copies a component

Defined in imgTfmUtil.c 

void 
ImgComponentFree(
  ImgComponent_t * comp 
)
Frees a component.

Defined in imgTfmUtil.c 

void 
ImgComponentGetSupport(
  ImgComponent_t * comp 
)
Gets the supports of a component.

Defined in imgTfmUtil.c 

array_t * 
ImgComposeConstIntermediateVars(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * constIntermediate, 
  mdd_t ** cofactorCube, 
  mdd_t ** abstractCube, 
  mdd_t ** and_, 
  mdd_t ** from 
)
Compose the constant intermediate variable functions.

Defined in imgTfmUtil.c 

int 
ImgConstConstrain(
  mdd_t * func, 
  mdd_t * constraint 
)
Checks whether the result of constrain is constant.

Defined in imgTfmUtil.c 

int 
ImgCountBddSupports(
  mdd_t * func 
)
Returns the number of BDD supports in a function.

Defined in imgTfmUtil.c 

static void 
ImgCountOnsetDisjunctiveArray(
  Relation_t * head 
)
Count onset of relation array

Defined in imgLinear.c 

int 
ImgDecideSplitOrConjoin(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * from, 
  int  preFlag, 
  array_t * relationArray, 
  mdd_t * cofactorCube, 
  mdd_t * abstractCube, 
  int  useBothFlag, 
  int  depth 
)
Decides whether to split or to conjoin.

Defined in imgHybrid.c 

void 
ImgDuplicateTransitionFunction(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Duplicates transition function.

Defined in imgTfm.c 

void 
ImgDuplicateTransitionRelationIwls95(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Duplicates transition relation. Assumes that the Transition Relation is an array.

See Also ImgRestoreTransitionRelationIwls95
Defined in imgIwls95.c 

void 
ImgDuplicateTransitionRelationMono(
  Img_ImageInfo_t * imageInfo 
)
Duplicates transition relation. Assumes that the Transition Relation is a MDD.

Defined in imgMonolithic.c 

int 
ImgExistConstIntermediateVar(
  array_t * vector 
)
Checks whether there is a constant function of intermediate variables.

Defined in imgTfmUtil.c 

void 
ImgFlushCache(
  ImgCacheTable_t * table 
)
Flushes all cache entries.

Defined in imgTfmCache.c 

void 
ImgFreeTrmOptions(
  ImgTrmOption_t * option 
)
Frees the option structure for transition relation method.

Defined in imgIwls95.c 

array_t * 
ImgGetAbstractedCofactoredRelationArray(
  mdd_manager * manager, 
  array_t * relationArray, 
  mdd_t * cofactorCube, 
  mdd_t * abstractCube 
)
Smothes and cofactors a relation array. Returns new relation array.

Defined in imgTfmUtil.c 

array_t * 
ImgGetAbstractedRelationArray(
  mdd_manager * manager, 
  array_t * relationArray, 
  mdd_t * cube 
)
Smoothes a relation array with respect to a cube.

Defined in imgTfmUtil.c 

array_t * 
ImgGetCofactoredAbstractedRelationArray(
  mdd_manager * manager, 
  array_t * relationArray, 
  mdd_t * cofactorCube, 
  mdd_t * abstractCube 
)
Cofactors and smooths a relation array. Returns new relation array.

Defined in imgTfmUtil.c 

array_t * 
ImgGetCofactoredRelationArray(
  array_t * relationArray, 
  mdd_t * func 
)
Cofactors a relation array with respect to a function. Returns new relation array.

Defined in imgTfmUtil.c 

array_t * 
ImgGetCofactoredVector(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * func 
)
Cofactors a function vector with respect to a function. Returns new function vector.

Defined in imgTfmUtil.c 

mdd_t * 
ImgGetComposedFunction(
  array_t * vector 
)
Returns a function composed all intermediate variables.

Defined in imgTfmUtil.c 

array_t * 
ImgGetConstrainedRelationArray(
  ImgTfmInfo_t * info, 
  array_t * relationArray, 
  mdd_t * constraint 
)
Constrains a relation array with respect to a constraint. Returns new relation array.

Defined in imgTfmUtil.c 

array_t * 
ImgGetConstrainedVector(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * constraint 
)
Constrains a function vector with respect to a constraint. Returns new function vector.

Defined in imgTfmUtil.c 

ImgComponent_t * 
ImgGetLatchComponent(
  array_t * vector 
)
Returns the first latch component.

Defined in imgTfmUtil.c 

ImgPartialImageOption_t * 
ImgGetPartialImageOptions(
    
)
Get partial image options.

Defined in imgUtil.c 

array_t * 
ImgGetQuantificationSchedule(
  mdd_manager * mddManager, 
  ImgFunctionData_t * functionData, 
  Img_MethodType  method, 
  Img_DirectionType  direction, 
  ImgTrmOption_t * option, 
  array_t * relationArray, 
  array_t * smoothVarBddArray, 
  array_t * domainVarBddArray, 
  array_t * introducedVarBddArray, 
  boolean  withClustering, 
  array_t ** orderedRelationArrayPtr 
)
Returns quantification schedule for a given relation array.

Defined in imgIwls95.c 

array_t * 
ImgGetTransitionFunction(
  void * methodData, 
  Img_DirectionType  directionType 
)
Returns current transition function.

Defined in imgTfm.c 

array_t * 
ImgGetTransitionRelationIwls95(
  void * methodData, 
  Img_DirectionType  directionType 
)
Returns current transition relation.

Defined in imgIwls95.c 

ImgTrmOption_t * 
ImgGetTrmOptions(
    
)
Allocates an option structure for transition relation method.

Defined in imgIwls95.c 

void 
ImgImageAllowPartialImageIwls95(
  void * methodData, 
  boolean  value 
)
Sets the flag to allow partial images. Default is to not allow partial image computations. This flag is reset at the end of every image/preimage computation i.e., has to be specified before every image/preimage computation if partial image is desired.

Side Effects Flag is reset at the end of every image/preimage computation.

See Also ImgImageWasPartialIwls95
Defined in imgIwls95.c 

mdd_t * 
ImgImageByHybridWithStaticSplit(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * from, 
  array_t * relationArray, 
  mdd_t * cofactorCube, 
  mdd_t * abstractCube 
)
Computes an image by transition relation.

Defined in imgHybrid.c 

mdd_t * 
ImgImageByHybrid(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * from 
)
Computes an image by transition relation.

Defined in imgHybrid.c 

void 
ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  direction, 
  mdd_t * constrain, 
  Img_MinimizeType  minimizeMethod, 
  boolean  underApprox, 
  boolean  cleanUp, 
  boolean  forceReorder, 
  int  printStatus 
)
Constrains/adds dont-cares to the bit relation and creates a new transition relation. First, the existing transition relation is freed. The bit relation is created if it isn't stored already. The bit relation is then copied into the clustered relation field of the given direction. Then, it is constrained by the given constraint (underapprox) or the complement of the constraint is added (overapprox) to the bit relation. Then the modified bit relation is clustered. The underApprox flag indicates whether to create an over or an underapproximation of the transition relation (TRUE for underapproximation, FALSE for overapproximation). Although the procedure Img_MinimizeImage is used, the minimizeMethod flag for underapproximations should be generated by Img_GuidedSearchReadUnderApproxMinimizeMethod. The clean up flag indicates freeing of the bit relations. If the forceReorder flag is set, variable reordering is fired after freeing old relations and before creating new relations.

Side Effects Frees current transition relation and quantification schedule. Frees bit relations if indicated.

See Also Img_MultiwayLinearAndSmooth ImgImageInfoInitializeMono Img_MinimizeImage
Defined in imgIwls95.c 

void 
ImgImageConstrainAndClusterTransitionRelationMono(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * constrain, 
  Img_MinimizeType  minimizeMethod, 
  boolean  underApprox, 
  boolean  cleanUp, 
  boolean  forceReorder, 
  int  printStatus 
)
Constrains/adds dont-cares to the bit relation and creates a new transition relation. First, the existing transition relation is freed. The bit relation is created and constrained by the given constraint (underapprox) or its complement is add to the bit relation (overapprox) depending on the underApprox flag. Then the modified bit relation is clustered. The code is similar to ImgImageInfoInitializeMono. An over or under approximation of the transition relation may be created. The underApprox flag should be TRUE for an underapproximation and FALSE for an overapproximation. Although Img_MinimizeImage is used the minimizeMethod flag for underapproximations has to be passed by Img_GuidedSearchReadUnderApproxMinimizeMethod. The cleanUp flag is currently useless but is maintained for uniformity with other Image computation methods incase methodData changes in the future to store bitRelations. The flag

Side Effects Current transition relation and quantification schedule are freed. Bit relations are freed if indicated.

See Also Img_MultiwayLinearAndSmooth ImgImageInfoInitializeMono Img_MinimizeImage Img_AddDontCareToImage
Defined in imgMonolithic.c 

void 
ImgImageConstrainAndClusterTransitionRelationTfm(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  direction, 
  mdd_t * constrain, 
  Img_MinimizeType  minimizeMethod, 
  boolean  underApprox, 
  boolean  cleanUp, 
  boolean  forceReorder, 
  int  printStatus 
)
Constrains the bit function and relation and creates a new transition function vector and relation. First, the existing transition function vector and relation is freed. The bit relation is created if it isnt stored already. The bit relation is then copied into the Clustered relation of the given direction and constrained by the given constraint. The bit relation is clustered. In the case of the backward relation, the clustered relation is minimized with respect to the care set.

Side Effects Frees current transition relation

Defined in imgTfm.c 

void 
ImgImageFreeClusteredTransitionRelationIwls95(
  void * methodData, 
  Img_DirectionType  directionType 
)
Frees current transition relation and associated quantification schedule for the given direction.

Defined in imgIwls95.c 

void 
ImgImageFreeClusteredTransitionRelationTfm(
  void * methodData, 
  Img_DirectionType  directionType 
)
Frees current transition function vector and relation for the given direction.

Defined in imgTfm.c 

mdd_t * 
ImgImageInfoComputeBwdIwls95(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
First bdd_cofactor is used to compute the simplified set of states to compute the image of. Next, this simplified set is multiplied with the relation arrays given in the bwdClusteredRelationArray in order and the variables are quantified according to the schedule in bwdArraySmoothVarBddArray.

See Also ImgImageInfoComputeBwdWithDomainVarsIwls95
Defined in imgIwls95.c 

mdd_t * 
ImgImageInfoComputeBwdMono(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the backward image of a set of states between fromLowerBound and fromUpperBound. First a set of states between fromLowerBound and fromUpperBound is computed. Then, the transition relation is simplified by cofactoring it wrt to the set of states found in the first step, and wrt the toCareSet.

See Also ImgImageInfoComputeFwdMono ImgImageInfoComputeBwdWithDomainVarsMono
Defined in imgMonolithic.c 

mdd_t * 
ImgImageInfoComputeBwdTfm(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the backward image of domainSubset.

See Also ImgImageInfoComputeBwdWithDomainVarsTfm
Defined in imgTfm.c 

mdd_t * 
ImgImageInfoComputeBwdWithDomainVarsIwls95(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Identical to ImgImageInfoComputeBwdIwls95 except in the fromLowerBound and fromUpperBound, domainVars are substituted by rangeVars.

See Also ImgImageInfoComputeBwdIwls95
Defined in imgIwls95.c 

mdd_t * 
ImgImageInfoComputeBwdWithDomainVarsMono(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Identical to ImgImageInfoComputeBwdMono except that fromLowerBound and fromUpperBound and given in terms of domain variables, hence we need to substitute the range variables first.

See Also ImgImageInfoComputeBwdMono
Defined in imgMonolithic.c 

mdd_t * 
ImgImageInfoComputeBwdWithDomainVarsTfm(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Identical to ImgImageInfoComputeBwdTfm.

See Also ImgImageInfoComputeBwdTfm
Defined in imgTfm.c 

mdd_t * 
ImgImageInfoComputeFwdIwls95(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the forward image of a set of states. If partial image requested and the first image computed doesn't intersect toCareSet, then recompute image. ASSUME that toCareSet is in terms of functionData->domainVars.

Side Effects IMPORTANT NOTE: image may be in terms of domain variables even when the reverse is expected IF partial images are allowed. The clean way would be to convert toCareset in terms of functionData->rangeVars but it may end up being quite inefficient.

See Also ImgImageInfoComputeFwdWithDomainVarsIwls95
Defined in imgIwls95.c 

mdd_t * 
ImgImageInfoComputeFwdMono(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the forward image of a set of states between fromLowerBound and fromUpperBound. First a set of states between fromLowerBound and fromUpperBound is computed. Then, the transition relation is simplified by cofactoring it wrt to the set of states found in the first step, and wrt the toCareSet.

See Also ImgImageInfoComputeBwdMono ImgImageInfoComputeFwdWithDomainVarsMono
Defined in imgMonolithic.c 

mdd_t * 
ImgImageInfoComputeFwdTfm(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the forward image of a set of states.

See Also ImgImageInfoComputeFwdWithDomainVarsTfm
Defined in imgTfm.c 

mdd_t * 
ImgImageInfoComputeFwdWithDomainVarsIwls95(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
First the forward image computation function is called which returns an image on range vars. Later, variable substitution is used to obtain image on domain vars.

See Also ImgImageInfoComputeFwdIwls95
Defined in imgIwls95.c 

mdd_t * 
ImgImageInfoComputeFwdWithDomainVarsMono(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Identical to ImgImageInfoComputeFwdMono except 1. toCareSet is in terms of domain vars and hence range vars are substituted first. 2. Before returning the image, range vars are substituted with domain vars.

See Also ImgImageInfoComputeFwdMono
Defined in imgMonolithic.c 

mdd_t * 
ImgImageInfoComputeFwdWithDomainVarsTfm(
  ImgFunctionData_t * functionData, 
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Identical to ImgImageInfoComputeFwdTfm.

See Also ImgImageInfoComputeFwdTfm
Defined in imgTfm.c 

void 
ImgImageInfoFreeIwls95(
  void * methodData 
)
Frees the memory associated with imageInfo.

See Also ImgImageInfoInitializeIwls95
Defined in imgIwls95.c 

void 
ImgImageInfoFreeMono(
  void * methodData 
)
Frees the method data associated with the monolithic method.

Defined in imgMonolithic.c 

void 
ImgImageInfoFreeTfm(
  void * methodData 
)
Frees the memory associated with imageInfo.

Defined in imgTfm.c 

void * 
ImgImageInfoInitializeIwls95(
  void * methodData, 
  ImgFunctionData_t * functionData, 
  Img_DirectionType  directionType, 
  Img_MethodType  method 
)
This process consists of following steps. 1. The transition functions are built. 2. An array of bit level relations are built using the function mdd_fn_array_to_bdd_rel_array. 3. The relations are clustered using the threshold value. 4. The clustered relations are ordered.

See Also ImgImageInfoFreeIwls95
Defined in imgIwls95.c 

void * 
ImgImageInfoInitializeMono(
  void * methodData, 
  ImgFunctionData_t * functionData, 
  Img_DirectionType  directionType 
)
This function computes the monolithic transition relation characterizing the behavior of the system from the individual functions.

See Also Img_MultiwayLinearAndSmooth
Defined in imgMonolithic.c 

void * 
ImgImageInfoInitializeTfm(
  void * methodData, 
  ImgFunctionData_t * functionData, 
  Img_DirectionType  directionType, 
  Img_MethodType  method 
)
Initialized an image data structure for image computation using transition function method.

Defined in imgTfm.c 

void 
ImgImageInfoPrintMethodParamsIwls95(
  void * methodData, 
  FILE * fp 
)
This function is used to obtain the information about the parameters used to initialize the imageInfo. If the file pointer argument is not NULL, the options are printed out. The shared size of the transition relation is printed out on vis_stdout.

Defined in imgIwls95.c 

void 
ImgImageInfoPrintMethodParamsMono(
  void * methodData, 
  FILE * fp 
)
This function is used to obtain the information about the parameters used to initialize the imageInfo.

Defined in imgMonolithic.c 

void 
ImgImageInfoPrintMethodParamsTfm(
  void * methodData, 
  FILE * fp 
)
This function is used to obtain the information about the parameters used to initialize the imageInfo.

Defined in imgTfm.c 

boolean 
ImgImageWasPartialIwls95(
  void * methodData 
)
Checks if the last image/preimage was partial. This flag is valid only for the last image/preimage computation. Reset before every image/preimage computation.

Side Effects Reset before every image/preimage computation.

See Also ImgImageAllowPartialImageIwls95
Defined in imgIwls95.c 

int 
ImgIsPartitionedTransitionRelationTfm(
  Img_ImageInfo_t * imageInfo 
)
Check whether transition relation is built in hybrid.

Defined in imgTfm.c 

static Conjunct_t ** 
ImgLinearAddConjunctIntoArray(
  Conjunct_t ** array, 
  int * nArray, 
  Conjunct_t * con 
)
Add conjunct into array

Defined in imgLinear.c 

void 
ImgLinearAddConjunctIntoClusterArray(
  Conjunct_t * base, 
  Conjunct_t * con 
)
Add Conjunct into Cluster Array

Defined in imgLinear.c 

static void 
ImgLinearAddNextStateCase(
  Relation_t * head 
)
Add singleton next state variable case into array

Defined in imgLinear.c 

static void 
ImgLinearAddSingletonCase(
  Relation_t * head 
)
Find the case that the relation contains only one next state varaible

Defined in imgLinear.c 

void 
ImgLinearBuildConjunctArrayWithQuotientCC(
  Relation_t * head 
)
The new Relation_t is created for each connected component

Defined in imgLinear.c 

static void 
ImgLinearBuildInitialCandidate(
  Relation_t * head, 
  double  affinityLimit, 
  int  varLimit, 
  int  rangeFlag, 
  int  (*compare_func)(const void *, const void *) 
)
Build data structure for clustering

Defined in imgLinear.c 

static void 
ImgLinearCAPOInterfaceAux(
  Relation_t * head, 
  char * baseName 
)
Make interface files for CAPO

Defined in imgLinear.c 

static void 
ImgLinearCAPOInterfaceConjunctNet(
  Relation_t * head, 
  char * baseName 
)
Make interface files for CAPO

Defined in imgLinear.c 

static void 
ImgLinearCAPOInterfaceConjunctNodes(
  Relation_t * head, 
  char * baseName 
)
Make interface files for CAPO

Defined in imgLinear.c 

static void 
ImgLinearCAPOInterfaceConjunctPl(
  Relation_t * head, 
  char * baseName 
)
Make interface files for CAPO

Defined in imgLinear.c 

static void 
ImgLinearCAPOInterfaceConjunctScl(
  Relation_t * head, 
  char * baseName 
)
Make interface files for CAPO

Defined in imgLinear.c 

static void 
ImgLinearCAPOInterfaceVariableNet(
  Relation_t * head, 
  char * baseName, 
  int  includeNS 
)
Make interface for CAPO

Defined in imgLinear.c 

void 
ImgLinearCAPOInterfaceVariableNodes(
  Relation_t * head, 
  char * baseName, 
  int  includeNS 
)
Make interface for CAPO

Defined in imgLinear.c 

static void 
ImgLinearCAPOInterfaceVariablePl(
  Relation_t * head, 
  char * baseName, 
  int  includeNS 
)
Make interface for CAPO

Defined in imgLinear.c 

static void 
ImgLinearCAPOInterfaceVariableScl(
  Relation_t * head, 
  char * baseName 
)
Make interface for CAPO

Defined in imgLinear.c 

static void 
ImgLinearCAPOReadConjunctOrder(
  Relation_t * head, 
  char * baseName 
)
Read result of CAPO

Defined in imgLinear.c 

static void 
ImgLinearCAPOReadVariableOrder(
  Relation_t * head, 
  char * baseName, 
  int  includeNS 
)
Read result of CAPO

Defined in imgLinear.c 

static int 
ImgLinearCAPORun(
  char * capoExe, 
  char * baseName, 
  int  brief 
)
Run batch job of CAPO

Defined in imgLinear.c 

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 
)
First the linear arrangement of transition relation that minimze max cut is generated and the iterative clustering is applied on it.

Defined in imgLinear.c 

static void 
ImgLinearClusterSameSupportSet(
  Relation_t * head 
)
Cluster the relation that has same support set

Defined in imgLinear.c 

static int 
ImgLinearClusterUsingHeap(
  Relation_t * head, 
  double  affinityLimit, 
  int  andExistLimit, 
  int  varLimit, 
  Img_OptimizeType  optDir, 
  int  rangeFlag, 
  int  (*compare_func)(const void *, const void *) 
)
Apply clustering with priority queue

Defined in imgLinear.c 

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 *) 
)
Apply clustering with given priority function

Defined in imgLinear.c 

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 *) 
)
Apply clustering iteratively

Defined in imgLinear.c 

static bdd_t * 
ImgLinearClusteringPairSmooth(
  Relation_t * head, 
  Cluster_t * clu, 
  int ** failureHistory, 
  int  andExistLimit, 
  int  bddLimit 
)
Clustering pair of transition relation

Defined in imgLinear.c 

static bdd_t * 
ImgLinearClusteringSmooth(
  Relation_t * head, 
  Cluster_t * clu, 
  int ** failureHistory, 
  int  andExistLimit, 
  int  bddLimit 
)
Apply clustering while quantifying the variables that are isolated

Defined in imgLinear.c 

int 
ImgLinearClustering(
  Relation_t * head, 
  Img_OptimizeType  optDir 
)
Main function of clustering

Defined in imgLinear.c 

static int 
ImgLinearCompareAffinityDeadLive(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareConjunctDummy(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareConjunctIndex(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareConjunctRangeMinusDomain(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareConjunctSize(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareDeadAffinityLive(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareDeadLiveAffinity(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareLiveAffinityDead(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareVarDummyLarge(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareVarEffFromLarge(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareVarEffFromSmall(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareVarId(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareVarIndex(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearCompareVarSize(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

void 
ImgLinearComputeLifeTime(
  Relation_t * head, 
  double * paal, 
  double * patl 
)
Compute life time of variables

Defined in imgLinear.c 

static void 
ImgLinearConjunctArrayRefine(
  Relation_t * head 
)
Refine conjunction array to fill the empty slot.

Defined in imgLinear.c 

void 
ImgLinearConjunctOrderMainCC(
  Relation_t * head, 
  int  refineFlag 
)
First find the connected component and apply ordering procedure for each component.

Defined in imgLinear.c 

static void 
ImgLinearConjunctOrderMain(
  Relation_t * head, 
  int  bRefineConjunctOrder 
)
Main function of linear arrangement

Defined in imgLinear.c 

static void 
ImgLinearConjunctQuit(
  Conjunct_t * conjunct 
)
Free conjunct_t data structure

Defined in imgLinear.c 

static void 
ImgLinearConjunctRefine(
  Relation_t * head, 
  Conjunct_t * conjunct 
)
Refine conjunction array to fill the empty slot.

Defined in imgLinear.c 

static void 
ImgLinearConjunctionOrder(
  Relation_t * head, 
  char * baseName, 
  int  refineFlag 
)
Generate linear arrangement with CAPO

Defined in imgLinear.c 

void 
ImgLinearConnectedComponent(
  Relation_t * head 
)
Find the connected component from fine grain transition relation

Defined in imgLinear.c 

static void 
ImgLinearExpandSameSupportSet(
  Relation_t * head 
)
Find transtion relations that have smae support set and use this information when finding linear arragement

Defined in imgLinear.c 

void 
ImgLinearExtractNextStateCase(
  Relation_t * head 
)
Extract the relation that contains next state varaibles only

Defined in imgLinear.c 

array_t * 
ImgLinearExtractRelationArrayT(
  Relation_t * head 
)
Create relation array for image computation from Relation_t data structure

Defined in imgLinear.c 

bdd_t ** 
ImgLinearExtractRelationArray(
  Relation_t * head 
)
Create relation array for image computation from Relation_t data structure

Defined in imgLinear.c 

void 
ImgLinearExtractSingletonCase(
  Relation_t * head 
)
Extract the relation contains only one next state varaible

Defined in imgLinear.c 

void 
ImgLinearFindConnectedComponent(
  Relation_t * head, 
  Conjunct_t * conjunct, 
  int  cc_index 
)
Find the connected component from fine grain transition relation

Defined in imgLinear.c 

static void 
ImgLinearFindSameSupportConjuncts(
  Relation_t * head, 
  int  from, 
  int  to 
)
Find the conjuncts that have same support variables.

Defined in imgLinear.c 

void 
ImgLinearFreeSmoothArray(
  array_t * smoothVarBddArray 
)
Free smooth variable array

Defined in imgLinear.c 

int * 
ImgLinearGetSupportBddId(
  mdd_manager * mgr, 
  bdd_t * f, 
  int * nSize 
)
Find support varaibles of bdd

Defined in imgLinear.c 

static int 
ImgLinearHeapCompareAffinityDeadLive(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearHeapCompareDeadAffinityLive(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearHeapCompareDeadLiveAffinity(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static int 
ImgLinearHeapCompareLiveAffinityDead(
  const void * c1, 
  const void * c2 
)
Priority function for clutering

Defined in imgLinear.c 

static void 
ImgLinearInsertClusterCandidate(
  Relation_t * head, 
  int  from, 
  int  to, 
  int  nDead, 
  int  nVar, 
  double  affinityLimit 
)
Add candidates for clustering, each condidate has pair of relation

Defined in imgLinear.c 

static void 
ImgLinearInsertPairClusterCandidate(
  Relation_t * head, 
  int  from, 
  double  affinityLimit, 
  int  varLimit, 
  int  rangeFlag 
)
Insert initial candidate set

Defined in imgLinear.c 

static int 
ImgLinearIsSameConjunct(
  Relation_t * head, 
  Conjunct_t * con1, 
  Conjunct_t * con2 
)
Check if given conjuncts have same support variables

Defined in imgLinear.c 

array_t * 
ImgLinearMakeSmoothVarBdd(
  Relation_t * head, 
  bdd_t ** smoothCubeArr 
)
Make the array of smooth variables

Defined in imgLinear.c 

int 
ImgLinearOptimizeAll(
  Relation_t * head, 
  Img_OptimizeType  optDir, 
  int  constantNSOpt 
)
If the next or current state variables are eleminated after applying clustering and constant propagation then delete corresponding state variable from transition relation.

Defined in imgLinear.c 

void 
ImgLinearOptimizeInternalVariables(
  Relation_t * head 
)
Remove intermediate variables after propagating constant.

Defined in imgLinear.c 

int 
ImgLinearOptimizeStateVariables(
  Relation_t * head, 
  Img_OptimizeType  optDir 
)
Remove corresponding current (next) state variables if the next (current state variables are eleminated aftetr clustering

Defined in imgLinear.c 

static void 
ImgLinearPrintDebugInfo(
  Relation_t * head 
)
Print information of debug information

Defined in imgLinear.c 

void 
ImgLinearPrintMatrixFull(
  Relation_t * head, 
  int  matrixIndex 
)
Print matrix

Defined in imgLinear.c 

void 
ImgLinearPrintMatrix(
  Relation_t * head 
)
Print matrix. Its x axis is varaible and its y axis is relation

Side Effects Print matrix. Its x axis is varaible and its y axis is relation

Defined in imgLinear.c 

static void 
ImgLinearPrintTransitionInfo(
  Relation_t * head 
)
Print transition relation info

Defined in imgLinear.c 

static void 
ImgLinearPrintVariableProfile(
  Relation_t * head, 
  char * baseName 
)
Print profile of variables

Defined in imgLinear.c 

int 
ImgLinearPropagateConstant(
  Relation_t * head, 
  int  nextStateFlag 
)
Propagate the constant to simply the transition relation

Defined in imgLinear.c 

static int 
ImgLinearQuantifyVariablesFromConjunct(
  Relation_t * head, 
  Conjunct_t * conjunct, 
  array_t * smoothVarBddArray, 
  int * bModified 
)
Apply quantification with candidate variables

Defined in imgLinear.c 

void 
ImgLinearRefineRelation(
  Relation_t * head 
)
Clean up the Relation_t data structure after applying linear arrangement of transition relation

Defined in imgLinear.c 

Relation_t * 
ImgLinearRelationInit(
  mdd_manager * mgr, 
  array_t * relationArray, 
  array_t * domainBddVars, 
  array_t * rangeBddVars, 
  array_t * quantifyBddVars, 
  ImgTrmOption_t * option 
)
Build initial data structure

Defined in imgLinear.c 

void 
ImgLinearRelationQuit(
  Relation_t * head 
)
Free Relation_t data structure

Defined in imgLinear.c 

static void 
ImgLinearSetEffectiveNumberOfStateVariable(
  Relation_t * head, 
  int * rangeId, 
  int * domainId, 
  int * existStateVariable 
)
Get the number of state variables after applying optimization

Defined in imgLinear.c 

static void 
ImgLinearUpdateVariableArrayWithId(
  Relation_t * head, 
  int  cindex, 
  int  id 
)
Update variable array with id of variable id

Defined in imgLinear.c 

static void 
ImgLinearVariableArrayInit(
  Relation_t * head 
)
Initialize variable array

Defined in imgLinear.c 

static void 
ImgLinearVariableArrayQuit(
  Relation_t * head 
)
Free variable array

Defined in imgLinear.c 

static void 
ImgLinearVariableLifeQuit(
  VarLife_t * var 
)
Free variable lifearray

Defined in imgLinear.c 

static void 
ImgLinearVariableOrder(
  Relation_t * head, 
  char * baseName, 
  int  includeNS 
)
Make interface for variable ordering

Defined in imgLinear.c 

void 
ImgMinimizeImageArrayWithCareSetArrayInSitu(
  array_t * imageArray, 
  array_t * careSetArray, 
  Img_MinimizeType  minimizeMethod, 
  boolean  underapprox, 
  boolean  printInfo, 
  Img_DirectionType  dir 
)
Compute a new array, such that every element corresponds to an element of imageArray minimized with all elements of careSetArray successively, using minimizeMethod. This function can be used for any array of bdds.

If underapprox is 1, the the bdds are underapproximated. If it is 0, they are overapproximated, and the minimizeMethod has to be either ornot or squeeze.

In-situ variant of ImgMinimizeImageArrayWithCareSetArray. Probably saves space.

See Also Img_MinimizeImage ImgMinimizeImageArrayWithCareSetArray
Defined in imgUtil.c 

array_t * 
ImgMinimizeImageArrayWithCareSetArray(
  array_t * imageArray, 
  array_t * careSetArray, 
  Img_MinimizeType  minimizeMethod, 
  boolean  underapprox, 
  boolean  printInfo, 
  Img_DirectionType  dir 
)
Compute a new array, such that every element corresponds to an element of imageArray minimized with all elements of careSetArray successively, using minimizeMethod. This function can be used for any array of bdds.

If underapprox is 1, the the bdds are underapproximated. If it is 0, they are overapproximated, and the minimizeMethod has to be either ornot or squeeze.

See Also Img_MinimizeImage ImgMinimizeImageArrayWithCareSetArrayInSitu
Defined in imgUtil.c 

void 
ImgMinimizeTransitionFunction(
  void * methodData, 
  array_t * constrainArray, 
  Img_MinimizeType  minimizeMethod, 
  Img_DirectionType  directionType, 
  int  printStatus 
)
Minimizes transition function with given set of constraints.

Defined in imgTfm.c 

void 
ImgMinimizeTransitionRelationIwls95(
  void * methodData, 
  ImgFunctionData_t * functionData, 
  array_t * constrainArray, 
  Img_MinimizeType  minimizeMethod, 
  Img_DirectionType  directionType, 
  boolean  reorderClusters, 
  int  printStatus 
)
Minimizes transition relation with given set of constraints. This invalidates the bwdclusteredcofactoredrelationarray.

RB: Can Kavita or In-Ho please explain the difference between these four related functions?? (other three in SeeAlso) The constraint should be in terms of present-state and input variables only. This function takes care that the quantification schedule is correct afterwards. If reorderClusters is true, the clusters are reordered after minimization.

See Also ImgMinimizeTransitionRelationIwls95 ImgApproximateTransitionRelationIwls95 ImgAbstractTransitionRelationIwls95 Img_MinimizeImage
Defined in imgIwls95.c 

void 
ImgMinimizeTransitionRelationMono(
  Img_ImageInfo_t * imageInfo, 
  array_t * constrainArray, 
  Img_MinimizeType  minimizeMethod, 
  int  printStatus 
)
Minimizes transition relation with given constraint.

Defined in imgMonolithic.c 

void 
ImgMlpClusterRelationArray(
  mdd_manager * mddManager, 
  ImgFunctionData_t * functionData, 
  array_t * relationArray, 
  array_t * domainVarBddArray, 
  array_t * quantifyVarBddArray, 
  array_t * rangeVarBddArray, 
  Img_DirectionType  direction, 
  array_t ** clusteredRelationArrayPtr, 
  array_t ** arraySmoothVarBddArrayPtr, 
  ImgTrmOption_t * option 
)
Clusters relation array and makes quantification schedule.

Side Effects ImgClusterRelationArray

Defined in imgMlp.c 

float 
ImgMlpComputeLambda(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  array_t * domainVarBddArray, 
  array_t * quantifyVarBddArray, 
  array_t * rangeVarBddArray, 
  Img_DirectionType  direction, 
  int  mode, 
  int  asIs, 
  int * prevArea, 
  float * improvedLambda, 
  ImgTrmOption_t * option 
)
Compute variables lifetime using MLP.

Defined in imgMlp.c 

void 
ImgMlpGetQuantificationSchedule(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  array_t * domainVarBddArray, 
  array_t * quantifyVarBddArray, 
  array_t * rangeVarBddArray, 
  array_t ** clusteredRelationArrayPtr, 
  array_t ** arraySmoothVarBddArrayPtr, 
  Img_DirectionType  direction, 
  ImgTrmOption_t * option 
)
Makes a quantification schedule using MLP.

Defined in imgMlp.c 

bdd_t * 
ImgMlpMultiwayAndSmooth(
  mdd_manager * mddManager, 
  ImgFunctionData_t * functionData, 
  array_t * relationArray, 
  array_t * domainVarBddArray, 
  array_t * quantifyVarBddArray, 
  array_t * rangeVarBddArray, 
  Img_DirectionType  direction, 
  ImgTrmOption_t * option 
)
Performs multiway and_smooth using MLP.

Defined in imgMlp.c 

void 
ImgMlpOrderRelationArray(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  array_t * domainVarBddArray, 
  array_t * quantifyVarBddArray, 
  array_t * rangeVarBddArray, 
  Img_DirectionType  direction, 
  array_t ** orderedRelationArrayPtr, 
  array_t ** arraySmoothVarBddArrayPtr, 
  ImgTrmOption_t * option 
)
Orders relation array and makes quantification schedule.

Defined in imgMlp.c 

void 
ImgMlpPrintDependenceMatrix(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  array_t * domainVarBddArray, 
  array_t * quantifyVarBddArray, 
  array_t * rangeVarBddArray, 
  Img_DirectionType  direction, 
  int  printFlag, 
  FILE * fout, 
  ImgTrmOption_t * option 
)
Prints dependence matrix.

Defined in imgMlp.c 

void 
ImgMlpReadClusterFile(
  FILE * fin, 
  mdd_manager * mddManager, 
  ImgFunctionData_t * functionData, 
  array_t * relationArray, 
  array_t * psVarBddArray, 
  array_t * nsVarBddArray, 
  array_t * quantifyVarBddArray, 
  Img_DirectionType  direction, 
  array_t ** clusteredRelationArrayPtr, 
  array_t ** arraySmoothVarBddArrayPtr, 
  ImgTrmOption_t * option 
)
Reads cluster file.

Defined in imgMlp.c 

void 
ImgMlpWriteClusterFile(
  FILE * fout, 
  mdd_manager * mddManager, 
  array_t * relationArray, 
  array_t * psVarBddArray, 
  array_t * nsVarBddArray 
)
Writes cluster to a file.

Defined in imgMlp.c 

mdd_t* 
ImgMultiwayLinearAndSmoothWithFrom(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  mdd_t * from, 
  array_t * smoothVarBddArray, 
  array_t * domainVarBddArray, 
  array_t * introducedVarBddArray, 
  Img_MethodType  method, 
  Img_DirectionType  direction, 
  ImgTrmOption_t * option 
)
"relationArray" is an array of mdd's which need to be multiplied and the variables in the "smoothVarBddArray" need to be quantified out from the product. "introducedVarBddArray" is the array of the bdd variables (other than the variables to be quantified out) in the support of the relations. This array is used to compute the product order such that the number of new variables introduced in the product is minimized. However passing an empty array or an array of mddIds of partial support will not result in any error (some optimality will be lost though). The computation consists of 2 phases. In phase 1, an ordering of the relations and a schedule of quantifying variables is found (based on IWLS95) heuristic. In phase 2, the relations are multiplied in order and the quantifying variables are quantified according to the schedule. If "from" is not nil, we first order "relationArray" and make quantification schedule, then we multiply with "from". In this case, "domainVarBddArray" should contain the state variables to be quantified out. If "from" is nil, then "domainVarBddArray" should be an empty array.

Side Effects None

Defined in imgIwls95.c 

mdd_t* 
ImgMultiwayLinearAndSmooth(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  array_t * smoothVarBddArray, 
  array_t * introducedVarBddArray, 
  Img_MethodType  method, 
  Img_DirectionType  direction, 
  ImgTrmOption_t * option 
)
"relationArray" is an array of mdd's which need to be multiplied and the variables in the "smoothVarBddArray" need to be quantified out from the product. "introducedVarBddArray" is the array of the bdd variables (other than the variables to be quantified out) in the support of the relations. This array is used to compute the product order such that the number of new variables introduced in the product is minimized. However passing an empty array or an array of mddIds of partial support will not result in any error (some optimality will be lost though). The computation consists of 2 phases. In phase 1, an ordering of the relations and a schedule of quantifying variables is found (based on IWLS95) heuristic. In phase 2, the relations are multiplied in order and the quantifying variables are quantified according to the schedule.

Side Effects None

Defined in imgIwls95.c 

float 
ImgPercentVectorDependency(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  int  length, 
  int * nLongs 
)
Returns the percent of non-zero elements in dependency matrix.

Defined in imgTfmUtil.c 

mdd_t * 
ImgPreImageByHybridWithStaticSplit(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * from, 
  array_t * relationArray, 
  mdd_t * cofactorCube, 
  mdd_t * abstractCube 
)
Computes a preimage by transition relation.

Defined in imgHybrid.c 

mdd_t * 
ImgPreImageByHybrid(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * from 
)
Computes a preimage by transition relation.

Defined in imgHybrid.c 

void 
ImgPrintCacheStatistics(
  ImgCacheTable_t * cache 
)
Prints cache statistics for transition function method.

Defined in imgTfmCache.c 

void 
ImgPrintIntegerArray(
  array_t * idArray 
)
Prints integers from an array.

Defined in imgIwls95.c 

void 
ImgPrintPartialImageOptions(
    
)
Prints Partial Image options.

Defined in imgUtil.c 

void 
ImgPrintPartitionedTransitionRelation(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  array_t * arraySmoothVarBddArray 
)
Prints info of the partitioned transition relation.

Defined in imgIwls95.c 

void 
ImgPrintPartition(
  graph_t * partition 
)
Prints the given parition.

Defined in imgIwls95.c 

void 
ImgPrintVarIdTable(
  st_table * table 
)
Prints the content of a table containing integers.

Defined in imgUtil.c 

void 
ImgPrintVectorDependency(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  int  verbosity 
)
Prints vector dependencies with support.

Defined in imgTfmUtil.c 

void 
ImgReplaceIthPartitionedTransitionRelationIwls95(
  void * methodData, 
  int  i, 
  mdd_t * relation, 
  Img_DirectionType  directionType 
)
Replace ith partitioned transition relation.

Defined in imgIwls95.c 

void 
ImgReplaceIthTransitionFunction(
  void * methodData, 
  int  i, 
  mdd_t * function, 
  Img_DirectionType  directionType 
)
Replace ith transition function.

Defined in imgTfm.c 

void 
ImgResetMethodDataLinearComputeRange(
  void * methodData 
)
Turn off option to apply linear based image computation by comsidering range of state variables.

See Also ImgImageInfoFreeIwls95
Defined in imgIwls95.c 

void 
ImgRestoreTransitionFunction(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Restores original transition function from saved.

Defined in imgTfm.c 

void 
ImgRestoreTransitionRelationIwls95(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Restores original transition relation from saved.

See Also ImgDuplicateTransitionRelationIwls95
Defined in imgIwls95.c 

void 
ImgRestoreTransitionRelationMono(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Restores original transition relation from saved.

Defined in imgMonolithic.c 

void 
ImgSetMethodDataLinearComputeRange(
  void * methodData 
)
Turn on option to apply linear based image computation by comsidering range of state variables.

Defined in imgIwls95.c 

array_t * 
ImgSubstituteArray(
  array_t * f_array, 
  ImgFunctionData_t * functionData, 
  Img_SubstituteDir  dir 
)
Substitutes variables between domain and range.

Defined in imgUtil.c 

mdd_t * 
ImgSubstitute(
  mdd_t * f, 
  ImgFunctionData_t * functionData, 
  Img_SubstituteDir  dir 
)
Substitutes variables between domain and range.

Defined in imgUtil.c 

void 
ImgSupportClear(
  ImgTfmInfo_t * info, 
  char * support 
)
Clears a support array.

Defined in imgTfmUtil.c 

void 
ImgSupportCopy(
  ImgTfmInfo_t * info, 
  char * dsupport, 
  char * ssupport 
)
Copies the supports of a component. Here support is an array of char.

Defined in imgTfmUtil.c 

int 
ImgSupportCount(
  ImgTfmInfo_t * info, 
  char * support 
)
Returns the number of support of a support array.

Defined in imgTfmUtil.c 

void 
ImgSupportPrint(
  ImgTfmInfo_t * info, 
  char * support 
)
Prints a support array.

Defined in imgTfmUtil.c 

mdd_t * 
ImgTfmEliminateDependVars(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  array_t * relationArray, 
  mdd_t * states, 
  array_t ** newVector, 
  mdd_t ** dependRelations 
)
Eliminates dependent variables from a transition function. Returns a simplified copy of the given states if successful; NULL otherwise.

Side Effects vector is also modified.

Defined in imgTfmUtil.c 

ImgTfmOption_t * 
ImgTfmGetOptions(
  Img_MethodType  method 
)
Gets the necessary options for computing the image and returns in the option structure.

Defined in imgTfm.c 

mdd_t * 
ImgTfmImage(
  ImgTfmInfo_t * info, 
  mdd_t * from 
)
Computes an image with transition function method.

Defined in imgTfmFwd.c 

bdd_t * 
ImgTfmPreImage(
  ImgTfmInfo_t * info, 
  bdd_t * image 
)
Computes a preimage with transition function method.

Defined in imgTfmBwd.c 

mdd_t * 
ImgTrmEliminateDependVars(
  ImgFunctionData_t * functionData, 
  array_t * relationArray, 
  mdd_t * states, 
  mdd_t ** dependRelations, 
  int * nDependVars 
)
Eliminates dependent variables from a transition relation. Returns a simplified copy of the given states if successful; NULL otherwise.

Side Effects relationArray is also modified.

Defined in imgIwls95.c 

void 
ImgUpdateTransitionFunction(
  void * methodData, 
  array_t * vector, 
  Img_DirectionType  directionType 
)
Overwrites transition function with given.

Defined in imgTfm.c 

void 
ImgUpdateTransitionRelationIwls95(
  void * methodData, 
  array_t * relationArray, 
  Img_DirectionType  directionType 
)
Overwrites transition relation with given.

Defined in imgIwls95.c 

long 
ImgVectorBddSize(
  array_t * vector 
)
Returns the shared BDD size of a vector.

Defined in imgTfmUtil.c 

void 
ImgVectorConstrain(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * constraint, 
  array_t * relationArray, 
  array_t ** newVector, 
  mdd_t ** cube, 
  array_t ** newRelationArray, 
  mdd_t ** cofactorCube, 
  mdd_t ** abstractCube, 
  boolean  singleVarFlag 
)
Constrains a function vector with respect to a constraint.

Defined in imgTfmUtil.c 

array_t * 
ImgVectorCopy(
  ImgTfmInfo_t * info, 
  array_t * vector 
)
Copies a vector.

Defined in imgTfmUtil.c 

void 
ImgVectorFree(
  array_t * vector 
)
Frees a function vector.

Defined in imgTfmUtil.c 

int 
ImgVectorFunctionSize(
  array_t * vector 
)
Returns the number of functions in a vector. Excludes the number of intermediate functions.

Defined in imgTfmUtil.c 

mdd_t * 
ImgVectorMinimize(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * constraint, 
  mdd_t * from, 
  array_t * relationArray, 
  array_t ** newVector, 
  mdd_t ** cube, 
  array_t ** newRelationArray, 
  mdd_t ** cofactorCube, 
  mdd_t ** abstractCube 
)
Minimizes a function vector and a from set with respect to an essential cube. This function is called during eliminating dependent variables.

Defined in imgTfmUtil.c 

void 
ImgWriteSupportMatrix(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  array_t * relationArray, 
  char * string 
)
Writes a gnuplot file with support matrix.

Defined in imgTfmUtil.c 

void 
Img_AbstractTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  array_t * abstractVars, 
  mdd_t * abstractCube, 
  Img_DirectionType  directionType 
)
Abstracts out given variables from transition relation. abstractVars should be an array of bdd variables.

Defined in imgUtil.c 

mdd_t * 
Img_AddDontCareToImage(
  mdd_t * image, 
  mdd_t * constraint, 
  Img_MinimizeType  method 
)
Adds a dont care set to the given image.

Defined in imgUtil.c 

mdd_t * 
Img_ApproximateImage(
  mdd_manager * mgr, 
  mdd_t * image, 
  bdd_approx_dir_t  approxDir, 
  bdd_approx_type_t  approxMethod, 
  int  approxThreshold, 
  double  approxQuality, 
  double  approxQualityBias, 
  mdd_t * bias 
)
Approximate image.

Defined in imgUtil.c 

int 
Img_ApproximateTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  bdd_approx_dir_t  approxDir, 
  bdd_approx_type_t  approxMethod, 
  int  approxThreshold, 
  double  approxQuality, 
  double  approxQualityBias, 
  Img_DirectionType  directionType, 
  mdd_t * bias 
)
Approximate transition relation.

Defined in imgUtil.c 

void 
Img_ClusterRelationArray(
  mdd_manager * mddManager, 
  Img_MethodType  method, 
  Img_DirectionType  direction, 
  array_t * relationArray, 
  array_t * domainVarMddIdArray, 
  array_t * rangeVarMddIdArray, 
  array_t * quantifyVarMddIdArray, 
  array_t ** clusteredRelationArray, 
  array_t ** arraySmoothVarBddArray, 
  array_t ** smoothVarCubeArray, 
  boolean  freeRelationArray 
)
Clusters relation array and returns quantification schedule.

Defined in imgIwls95.c 

mdd_t * 
Img_ComposeIntermediateNodes(
  graph_t * partition, 
  mdd_t * node, 
  array_t * psVars, 
  array_t * nsVars, 
  array_t * inputVars 
)
Replace partitioned transition relation.

Defined in imgUtil.c 

void 
Img_DupTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Duplicates the transition relation for backup. Copies transition relation as well as quantification schedule for temporary use.

Defined in imgUtil.c 

void 
Img_End(
    
)
End the image package.

See Also Img_Init
Defined in imgUtil.c 

void 
Img_ForwardImageInfoConjoinWithWinningStrategy(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * winningStrategy 
)
Create restricted transition relations by conjoining with winning strategy.

Defined in imgIwls95.c 

void 
Img_ForwardImageInfoRecoverFromWinningStrategy(
  Img_ImageInfo_t * imageInfo 
)
Restore original transition relations from restricted transition relations by conjoining with winning strategy

Defined in imgIwls95.c 

int 
Img_GetNumberOfImageComputation(
  Img_DirectionType  imgDir 
)
Returns number of image/preimage computation.

Defined in imgUtil.c 

array_t * 
Img_GetPartitionedTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Returns current partitioned transition relation.

Defined in imgUtil.c 

Img_MinimizeType 
Img_GuidedSearchReadOverApproxMinimizeMethod(
    
)
Returns the guided search minimize method of overapproximating the transition relation. Default is OrNot.

Defined in imgUtil.c 

Img_MinimizeType 
Img_GuidedSearchReadUnderApproxMinimizeMethod(
    
)
Returns the guided search minimize method of underapproximating the transition relation. Default is And.

Defined in imgUtil.c 

void 
Img_ImageAllowPartialImage(
  Img_ImageInfo_t * info, 
  boolean  value 
)
Sets the flag to allow the next image computation to return a subset of the actual image. Default is to not allow partial image computations. This flag is reset at the end of every image/preimage computation i.e., has to be specified before every image/preimage computation if partial image is desired.

Side Effects Flag is reset at the end of every image/preimage computation.

See Also Img_ImageWasPartialImage
Defined in imgUtil.c 

void 
Img_ImageConstrainAndClusterTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  direction, 
  mdd_t * constrain, 
  Img_MinimizeType  minimizeMethod, 
  boolean  underApprox, 
  boolean  cleanUp, 
  boolean  forceReorder, 
  int  printStatus 
)
Constrains/adds dont-cares to the bit relations with the given constraint and creates a new transition relation in the direction indicated. This procedure will incur the cost of creating the bit relations if they dont already exist. An over/under approximation of the transition relation may be created according to the underApprox flag. The flag is TRUE for underapproximations and FALSE for over approximation. An underapproximation of the transition relation will be in the interval [T.C, T

Side Effects Current transition relation and quantification schedule are freed. Bit relations are freed if indicated by the cleanUp flag.

See Also Img_GuidedSearchReadUnderApproxMinimizeMethod Img_GuidedSearchReadOverApproxMinimizeMethod
Defined in imgUtil.c 

mdd_t * 
Img_ImageGetUnreachableStates(
  Img_ImageInfo_t * imageInfo 
)
Return unreachable states

Defined in imgIwls95.c 

mdd_t * 
Img_ImageInfoComputeBwdWithDomainVars(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  mdd_t * toCareSet 
)
Computes the backward image of a set expressed in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSet are expressed in terms of domain variables. See Img_ImageInfoComputeBwd for more information. This function takes a care set, as opposed to ComputeBwd, which takes a care-set array.

See Also Img_ImageInfoComputeBwd
Defined in imgUtil.c 

mdd_t * 
Img_ImageInfoComputeBwd(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the backward image of a set, under the function vector in imageInfo, using the image computation method specified in imageInfo. The set for which the backward image is computed is some set containing fromLowerBound and contained in fromUpperBound. The exact set used is chosen to simplify the computation. ToCareSet specifies those backward image points of interest; any points not in this set may or may not belong to the returned set. The MDDs fromLowerBound and fromUpperBound are defined over the range variables. The MDD toCareSet and the returned MDD are defined over the domain variables. If fromLowerBound is zero, then zero will be returned.

See Also Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoFree Img_ImageInfoComputeBwdWithDomainVars
Defined in imgUtil.c 

mdd_t * 
Img_ImageInfoComputeEXWithDomainVars(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the backward image of a set expressed in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSetArray are expressed in terms of domain variables. See Img_ImageInfoComputeBwd for more information. This function takes a care-set array, as opposed to Img_ImageInfoComputeBwdWithDomainVars, which takes a care set.

See Also Img_ImageInfoComputeBwd
Defined in imgUtil.c 

mdd_t * 
Img_ImageInfoComputeFwdWithDomainVars(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  mdd_t * toCareSet 
)
Computes the forward image of a set and expresses it in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSet are expressed in terms of domain variables. See Img_ImageInfoComputeFwd for more information. (Takes care states as a set.)

See Also Img_ImageInfoComputeFwd
Defined in imgUtil.c 

mdd_t * 
Img_ImageInfoComputeFwd(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the forward image of a set, under the function vector in imageInfo, using the image computation method specified in imageInfo. The set for which the forward image is computed is some set containing fromLowerBound and contained in fromUpperBound. The exact set used is chosen to simplify the computation. ToCareSet specifies those forward image points of interest; any points not in this set may or may not belong to the returned set. The MDDs fromLowerBound and fromUpperBound are defined over the domain variables. The MDD toCareSet and the returned MDD are defined over the range variables. If fromLowerBound is zero, then zero will be returned. (Takes care states as an array.)

See Also Img_ImageInfoInitialize Img_ImageInfoComputeBwd Img_ImageInfoFree Img_ImageInfoComputeFwdWithDomainVars
Defined in imgUtil.c 

mdd_t * 
Img_ImageInfoComputeImageWithDomainVars(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the forward image of a set and expresses it in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSet are expressed in terms of domain variables. See Img_ImageInfoComputeFwd for more information. (Takes care set as an array.)

See Also Img_ImageInfoComputeFwd
Defined in imgUtil.c 

mdd_t * 
Img_ImageInfoComputePreImageWithDomainVars(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the backward image of a set expressed in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSetArray are expressed in terms of domain variables. See Img_ImageInfoComputeBwd for more information. This function takes a care-set array, as opposed to Img_ImageInfoComputeBwdWithDomainVars, which takes a care set.

See Also Img_ImageInfoComputeBwd
Defined in imgUtil.c 

void 
Img_ImageInfoFreeFAFW(
  Img_ImageInfo_t * imageInfo 
)
Frees the memory associated with imageInfo.

See Also Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd
Defined in imgUtil.c 

void 
Img_ImageInfoFree(
  Img_ImageInfo_t * imageInfo 
)
Frees the memory associated with imageInfo.

See Also Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd
Defined in imgUtil.c 

Img_ImageInfo_t * 
Img_ImageInfoInitialize(
  Img_ImageInfo_t * imageInfo, 
  graph_t * mddNetwork, 
  array_t * roots, 
  array_t * domainVars, 
  array_t * rangeVars, 
  array_t * quantifyVars, 
  mdd_t * domainCube, 
  mdd_t * rangeCube, 
  mdd_t * quantifyCube, 
  Ntk_Network_t * network, 
  Img_MethodType  methodType, 
  Img_DirectionType  directionType, 
  int  FAFWFlag, 
  mdd_t * Winning 
)
Initializes an imageInfo structure. MethodType specifies which image computation method to use. If methodType is Img_Default_c, then if the user-settable flag "image_method" has been set, then this method is used, otherwise some default is used. DirectionType specifies which types of image computations will be performed (forward, backward, or both). Method-specific initialization takes into account the value of relevant parameters in the global flag table.

MddNetwork is a graph representing the functions to be used. Each vertex of the graph contains a multi-valued function (MVF) and an MDD id. The MVF gives the function of the vertex in terms of the MDD ids of the immediate fanins of the vertex.

Roots is an array of char* specifying the vertices of the graph which represent those functions for which we want to compute the image (it must not be empty); for example, for an FSM, roots represent the next state functions. DomainVars is an array of mddIds; for an FSM, these are the present state variables. Subsets of the domain are defined over these variables. RangeVars is an array of mddIds over which the range is expressed; for an FSM, these are the next state variables. This array must be in one-to-one correspondence with the array of roots. QuantifyVars is an array of mddIds, representing variables to be quantified from results of backward images; for an FSM, these are the input variables. This array may be empty. No copies are made of any of the input parameters, and thus it is the application's responsibility to free this data *after* the returned Img_ImageInfo_t is freed.

See Also Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd Img_ImageInfoFree
Defined in imgUtil.c 

char * 
Img_ImageInfoObtainMethodTypeAsString(
  Img_ImageInfo_t * imageInfo 
)
Returns a string giving the method type of an imageInfo. It is the user's responsibility to free this string.

See Also Img_ImageInfoInitialize
Defined in imgUtil.c 

Img_MethodType 
Img_ImageInfoObtainMethodType(
  Img_ImageInfo_t * imageInfo 
)
Returns the method type of an imageInfo.

See Also Img_ImageInfoInitialize
Defined in imgUtil.c 

Img_OptimizeType 
Img_ImageInfoObtainOptimizeType(
  Img_ImageInfo_t * imageInfo 
)
Returns the method type of an imageInfo.

See Also Img_ImageInfoInitialize
Defined in imgUtil.c 

void 
Img_ImageInfoPrintMethodParams(
  Img_ImageInfo_t * imageInfo, 
  FILE * fp 
)
Prints information about the image technique currently used.

Side Effects None.

Defined in imgUtil.c 

void 
Img_ImageInfoResetLinearComputeRange(
  Img_ImageInfo_t * imageInfo 
)
Reset linear compute range flag.

See Also Img_ImageInfoInitialize
Defined in imgUtil.c 

void 
Img_ImageInfoResetUseOptimizedRelationFlag(
  Img_ImageInfo_t * imageInfo 
)
reset optimization relation flag .

See Also Img_ImageInfoInitialize
Defined in imgUtil.c 

void 
Img_ImageInfoSetLinearComputeRange(
  Img_ImageInfo_t * imageInfo 
)
Set linear compute range flag.

See Also Img_ImageInfoInitialize
Defined in imgUtil.c 

void 
Img_ImageInfoSetUseOptimizedRelationFlag(
  Img_ImageInfo_t * imageInfo 
)
set optimization relation flag .

See Also Img_ImageInfoInitialize
Defined in imgUtil.c 

void 
Img_ImageInfoUpdateVariables(
  Img_ImageInfo_t * imageInfo, 
  graph_t * mddNetwork, 
  array_t * domainVars, 
  array_t * quantifyVars, 
  mdd_t * domainCube, 
  mdd_t * quantifyCube 
)
Updates present state and primary input variables. This function is called after calling ImageInfoInitialize for a subFsm.

See Also Img_ImageInfoInitialize
Defined in imgUtil.c 

void 
Img_ImagePrintPartialImageOptions(
    
)
Prints partial image options.

Defined in imgUtil.c 

boolean 
Img_ImageWasPartial(
  Img_ImageInfo_t * info 
)
Queries whether the last image computation was partial. Reset before every image/preimage computation i.e., this information is valid for only the previous image/preimage computation.

Side Effects Reset before every image/preimage computation.

See Also Img_ImageAllowPartialImage
Defined in imgUtil.c 

void 
Img_Init(
    
)
Initialize the image package.

See Also Img_End
Defined in imgUtil.c 

int 
Img_IsPartitionedTransitionRelation(
  Img_ImageInfo_t * imageInfo 
)
Returns 1 if partitioned transition relation is used.

Defined in imgUtil.c 

int 
Img_IsQuantifyArraySame(
  Img_ImageInfo_t * imageInfo, 
  array_t * quantifyArray 
)
This function is for remove memory leakage.

See Also Img_ImageInfoInitialize
Defined in imgUtil.c 

int 
Img_IsQuantifyCubeSame(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * quantifyCube 
)
This function is for remove memory leakage.

See Also Img_ImageInfoInitialize
Defined in imgUtil.c 

int 
Img_IsTransitionRelationOptimized(
  Img_ImageInfo_t * imageInfo 
)
Check whether the given transition relation is optimized.

Defined in imgIwls95.c 

mdd_t * 
Img_MinimizeImageArray(
  mdd_t * image, 
  array_t * constraintArray, 
  Img_MinimizeType  method, 
  boolean  underapprox 
)
Minimizes a bdd with given set of constraints. Underapproximates if underapprox is true, otherwise overapproximated (in which case method has to be ornot or squeeze).

Side Effects Img_MinimizeImage

Defined in imgUtil.c 

mdd_t * 
Img_MinimizeImage(
  mdd_t * image, 
  mdd_t * constraint, 
  Img_MinimizeType  method, 
  boolean  underapprox 
)
Minimizes an image with given constraint. This function can be used to minimize any BDDs.

If underapprox is 1, the the bdds are underapproximated. If it is 0, they are overapproximated, and the minimizeMethod has to be either ornot or squeeze.

Defined in imgUtil.c 

void 
Img_MinimizeTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  array_t * constrainArray, 
  Img_MinimizeType  minimizeMethod, 
  Img_DirectionType  directionType, 
  boolean  reorderIwls95Clusters 
)
Minimizes transition relation with given constraint if it hasn't been minimized already (does nothing otherwise). The constraint is expressed as an array of conjuncts of BDDs, The transition relation is minimized with each one of the conjuncts.

The boolean reorderIwls95Clusters is only relevant to the iwls95 image method. It causes the clusters to be ordered again after minimization.

The conjuncts have to be in terms of present-state variables or inputs. Next-state variables are not allowed.

For the hybrid and tfm methods, for image, we can only minimize wrt a set that includes any possible argument. For preimage, the result is only correct for as far as it lies within the set that the TR is minimized with. That means that reachability info can be usefully applied here.

For the other methods, we can also minimize wrt different sets. The edges in the TR that are outgoing from states not in this set may then get removed.

Defined in imgUtil.c 

mdd_t* 
Img_MultiwayLinearAndSmooth(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  array_t * smoothVarMddIdArray, 
  array_t * introducedVarMddIdArray, 
  Img_MethodType  method, 
  Img_DirectionType  direction 
)
"relationArray" is an array of mdd's which need to be multiplied and the variables in the "smoothVarMddIdArray" need to be quantified out from the product. "introducedVarMddIdArray" is the array of mddIds of the variables (other than the variables to be quantified out) in the support of the relations. This array is used to compute the product order such that the number of new variables introduced in the product is minimized. However passing an empty array or an array of mddIds of partial support will not result in any error (some optimality will be lost though). The computation consists of 2 phases. In phase 1, an ordering of the relations and a schedule of quantifying variables is found (based on IWLS95) heuristic. In phase 2, the relations are multiplied in order and the quantifying variables are quantified according to the schedule.

Side Effects None

Defined in imgIwls95.c 

void 
Img_PrintHybridOptions(
    
)
Prints the options for hybrid image computation.

Defined in imgHybrid.c 

void 
Img_PrintMlpOptions(
    
)
Prints the options for MLP image computation.

Defined in imgMlp.c 

void 
Img_PrintPartitionedTransitionRelation(
  mdd_manager * mddManager, 
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Prints info of the partitioned transition relation.

Defined in imgIwls95.c 

void 
Img_PrintTfmOptions(
    
)
Prints the options for image computation using transition function method.

Defined in imgTfm.c 

Img_MinimizeType 
Img_ReadMinimizeMethod(
    
)
Returns current method of minimizing transition relation. Default is restrict.

Defined in imgUtil.c 

int 
Img_ReadPrintMinimizeStatus(
  Img_ImageInfo_t * imageInfo 
)
Reads the flag whether to print the status of minimizing transition relation.

Defined in imgUtil.c 

void 
Img_ReorderPartitionedTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Reorder partitioned transition relation.

Defined in imgIwls95.c 

void 
Img_ReplaceIthPartitionedTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  int  i, 
  mdd_t * relation, 
  Img_DirectionType  directionType 
)
Replace ith partitioned transition relation.

Defined in imgUtil.c 

void 
Img_ReplacePartitionedTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  array_t * relationArray, 
  Img_DirectionType  directionType 
)
Replace partitioned transition relation.

Defined in imgUtil.c 

void 
Img_ResetNumberOfImageComputation(
  Img_DirectionType  imgDir 
)
Resets number of image/preimage computation.

Defined in imgUtil.c 

void 
Img_ResetTrMinimizedFlag(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Resets the flag that transition relation is minimized.

Defined in imgUtil.c 

void 
Img_RestoreTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Restores original transition relation from saved.

Defined in imgUtil.c 

void 
Img_SetPrintMinimizeStatus(
  Img_ImageInfo_t * imageInfo, 
  int  status 
)
Sets the flag whether to print the status of minimizing transition relation.

Defined in imgUtil.c 

mdd_t * 
Img_Substitute(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * f, 
  Img_SubstituteDir  dir 
)
Substitutes variables between domain and range.

Defined in imgUtil.c 

int 
Img_TfmCheckGlobalCache(
  int  preFlag 
)
Checks whether a global cache is used for transition function method. If it is, returns 1, otherwise returns 0. A global cache can be used when all image-info structs store the results into one image cache. A local cache is used for each image-info struct stores its results into its own image cache.

Defined in imgTfmCache.c 

void 
Img_TfmFlushCache(
  Img_ImageInfo_t * imageInfo, 
  int  preFlag 
)
Frees all cache contents of image computation using transition function method. This function is to free the cache contents only when requested and when tfm_auto_flush_cache is off.

Defined in imgTfmCache.c 

int 
Img_TfmGetCacheStatistics(
  Img_ImageInfo_t * imageInfo, 
  int  preFlag, 
  double * inserts, 
  double * lookups, 
  double * hits, 
  double * entries, 
  int * nSlots, 
  int * maxChainLength 
)
Gets the statistics of image cache of transition function method

Defined in imgTfmCache.c 

int 
Img_TfmGetRecursionStatistics(
  Img_ImageInfo_t * imageInfo, 
  int  preFlag, 
  int * nRecurs, 
  int * nLeaves, 
  int * nTurns, 
  float * averageDepth, 
  int * maxDepth, 
  int * nDecomps, 
  int * topDecomp, 
  int * maxDecomp, 
  float * averageDecomp 
)
Gets the statistics of recursions of transition function method.

Defined in imgTfm.c 

void 
Img_TfmPrintCacheStatistics(
  Img_ImageInfo_t * imageInfo, 
  int  preFlag 
)
Prints the statistics of image cache of transition function method.

Defined in imgTfmCache.c 

void 
Img_TfmPrintRecursionStatistics(
  Img_ImageInfo_t * imageInfo, 
  int  preFlag 
)
Prints the statistics of recursions for transition function method.

Defined in imgTfm.c 

void 
Img_TfmPrintStatistics(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  dir 
)
Prints the statistics of image cache and recursions in in transition function method.

Defined in imgTfm.c 

void 
Img_UpdateQuantificationSchedule(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Updates quantification schedule.

Defined in imgIwls95.c 

Img_MethodType 
Img_UserSpecifiedMethod(
    
)
Returns the method selected by Img_ImageInfoInitialize if Img_Default_c is passed in. Note that this may change if the user changes the definition of the image_method set flag.

See Also Img_ImageInfoIninitialize
Defined in imgUtil.c 

static Iwls95Info_t * 
Iwls95InfoStructAlloc(
  Img_MethodType  method 
)
Allocates and initializes the info structure for IWLS95 technique.

Defined in imgIwls95.c 

static int 
KeyStHash(
  char * key, 
  int  modulus 
)
Returns hash value of a key for st_table.

Defined in imgTfmCache.c 

static array_t * 
MakeSmoothVarCubeArray(
  mdd_manager * mddManager, 
  array_t * arraySmoothVarBddArray 
)
Returns array of cubes of smoothing variables.

Defined in imgIwls95.c 

static int 
MddSizeCompare(
  const void * ptr1, 
  const void * ptr2 
)
Compare the size of two MDDs.

Defined in imgIwls95.c 

static void 
MinimizeTransitionFunction(
  array_t * vector, 
  array_t * relationArray, 
  mdd_t * constrain, 
  Img_MinimizeType  minimizeMethod, 
  int  printStatus 
)
Minimizes function vector or relation with given constraint.

Defined in imgTfm.c 

static void 
MlpCluster(
  mdd_manager * mddManager, 
  char ** xy, 
  int  nRows, 
  int  nCols, 
  int  nActiveRows, 
  int  nActiveCols, 
  int * nClusterRows, 
  int * nClusterCols, 
  int * rowOrder, 
  int * colOrder, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  array_t * clusterArray, 
  array_t * arraySmoothVarBddArray, 
  Img_DirectionType  direction, 
  int * cRowOrder, 
  array_t * nsVarBddArray, 
  int * sccBorder, 
  int * varPos, 
  ImgTrmOption_t * option 
)
Clusters on the ordered bits.

Defined in imgMlp.c 

static int 
MlpCountSupport(
  ClusterList_t * list, 
  int * colOrder, 
  int  nActiveCols 
)
Counts the number of supports of the list.

Defined in imgMlp.c 

static SccList_t * 
MlpDecomposeScc(
  mdd_manager * mddManager, 
  char ** xy, 
  int  nRows, 
  int  nActiveRows, 
  int  nActiveCols, 
  int * rowOrder, 
  int * colOrder, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int  clusteredFlag, 
  ImgTrmOption_t * option 
)
Performs connected component decomposition.

Defined in imgMlp.c 

static int 
MlpNumQuantifyVars(
  ClusterList_t * list, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * colOrder, 
  int  nClusterCols 
)
Retuns the number of variables to be quantified in a list.

Defined in imgMlp.c 

static void 
MlpPostProcess(
  char ** xy, 
  SccList_t * sccList, 
  int  nVars, 
  int  nRows, 
  int  nCols, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  Img_DirectionType  direction, 
  ImgTrmOption_t * option 
)
Performs a postprocessing after MLP. Tries to exchange adjacent two rows if the exchange lowers variable lifetime.

Defined in imgMlp.c 

static float 
MlpSupportAffinity(
  ClusterList_t * curList, 
  ClusterList_t * nextList, 
  RcInfo_t * colInfo, 
  int * colOrder, 
  int  nActiveCols, 
  int  clusterMethod 
)
Computes the affinity of two lists.

Defined in imgMlp.c 

static void 
MoveBestCols(
  char ** xy, 
  SccList_t * sccList, 
  int  nRows, 
  int  nCols, 
  int  nActiveRows, 
  int  nActiveCols, 
  int * rowOrder, 
  int * colOrder, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int  startFunc, 
  int  lastFunc, 
  int  startVar, 
  int  lastVar, 
  ImgTrmOption_t * option 
)
Finds and moves the best column iteratively.

Defined in imgMlp.c 

static void 
MoveBestRows(
  char ** xy, 
  SccList_t * sccList, 
  int  nRows, 
  int  nCols, 
  int * rowOrder, 
  int * colOrder, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int  startFunc, 
  int  lastFunc, 
  int  startVar, 
  int  lastVar, 
  ImgTrmOption_t * option 
)
Finds and moves the best row iteratively.

Defined in imgMlp.c 

static void 
MoveColToLeft(
  char ** xy, 
  int  y, 
  int  startFunc, 
  int  lastFunc, 
  int  startVar, 
  int  lastVar, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  RcListInfo_t * candList, 
  int  method 
)
Moves a column to the left of the active region.

Defined in imgMlp.c 

static void 
MoveColToRight(
  char ** xy, 
  int  y, 
  int  startFunc, 
  int  lastFunc, 
  int  startVar, 
  int  lastVar, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  RcListInfo_t * candList, 
  int  method 
)
Moves a column to the tight of the active region.

Defined in imgMlp.c 

static void 
MoveRowToBottom(
  char ** xy, 
  int  x, 
  int  startFunc, 
  int  lastFunc, 
  int  startVar, 
  int  lastVar, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  RcListInfo_t * candList, 
  int  method 
)
Moves a row to the bottom of the active region.

Defined in imgMlp.c 

static void 
MoveRowToTop(
  char ** xy, 
  int  x, 
  int  startFunc, 
  int  lastFunc, 
  int  startVar, 
  int  lastVar, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  RcListInfo_t * candList, 
  int  method 
)
Moves a row to the top of the active region.

Defined in imgMlp.c 

static int 
MoveSingletonCol(
  char ** xy, 
  SccList_t * sccList, 
  int  nRows, 
  int  nCols, 
  int  y, 
  int * startFunc, 
  int * lastFunc, 
  int * startVar, 
  int * lastVar, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  RcListInfo_t * candList, 
  ImgTrmOption_t * option 
)
Moves a singleton column.

Defined in imgMlp.c 

static int 
MoveSingletonRow(
  char ** xy, 
  SccList_t * sccList, 
  int  nRows, 
  int  nCols, 
  int  x, 
  int * startFunc, 
  int * lastFunc, 
  int * startVar, 
  int * lastVar, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  RcListInfo_t * candList, 
  ImgTrmOption_t * option 
)
Moves a singleton row.

Defined in imgMlp.c 

static int 
NumOfSccs(
  SccList_t * sccHeadList 
)
Returns the number of connected components in the list.

Defined in imgMlp.c 

static void 
OrderClusterOrder(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  array_t * fromVarBddArray, 
  array_t * toVarBddArray, 
  array_t * quantifyVarBddArray, 
  array_t ** orderedClusteredRelationArrayPtr, 
  array_t ** smoothVarBddArrayPtr, 
  ImgTrmOption_t * option, 
  boolean  freeRelationArray 
)
Takes an array of relations and does order, cluster, order on it. This forms a heuristically optimized clustered transition relation, plus a quantification schedule that goes with it. Requires the relation array, quantify variables, a "from" variable array (contained in the quantify variables), a "to" variable array and direction of computation (image or preimage). Eventually orderedClusteredRelationArray holds an ordered-clustered-ordered version of the relationArray and smoothVarBddArrayPtr holds the quantification schedule that goes with orderClusteredRelationArray. If the freeRelationArray flag is set, the relationArray is freed. This code is identical to ImgInfoInitialize.

Side Effects The existing contents of orderedClusteredRelationArrayPtr or smoothVarBddArrayPtr are lost (not freed). relationArray is freed if the freeRelationArray flag is set.

See Also ImgImageInfoInitializeIwls95
Defined in imgIwls95.c 

static void 
OrderRelationArrayAux(
  array_t * relationArray, 
  lsList  remainingCtrInfoList, 
  array_t * ctrInfoArray, 
  array_t * varInfoArray, 
  int * sortedMaxIndexVector, 
  int  numSmoothVarsRemaining, 
  int  numIntroducedVarsRemaining, 
  st_table * bddIdToBddTable, 
  ImgTrmOption_t * option, 
  array_t * domainAndQuantifyVarBddArray, 
  array_t ** orderedRelationArrayPtr, 
  array_t ** arraySmoothVarBddArrayPtr, 
  array_t * arrayDomainQuantifyVarsWithZeroNumCtr 
)
This routine is called by orderRelationArray after the initialization is complete and the cluster relations are simplified wrt to the quantify variable local to the cluster. The algorithm is: While (there exists a cluster to be ordered) { Calculate benefit for each unordered cluster. Choose the cluster with the maximum benefit. Update the cost function parameters. }

Side Effects ctrInfo and varInfo structures are modified.

Defined in imgIwls95.c 

static void 
OrderRelationArray(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  array_t * domainVarBddArray, 
  array_t * quantifyVarBddArray, 
  array_t * rangeVarBddArray, 
  ImgTrmOption_t * option, 
  array_t ** orderedRelationArrayPtr, 
  array_t ** arraySmoothVarBddArrayPtr 
)
This function returns an array of ordered relations and an array of BDD cubes (array of BDDs). This consists of following steps: a. Initialize the array of ctrInfoStructs and varInfoStructs. b. Fill in the list of varItemStruct's of ctrInfo's and ctrItemStruct's of varInfo's. c. Simplify the relations by quantifying out the quantify variables local to a particular relation. d. Order the relations according to the cost function described in "CalculateRelationBenefit".

Defined in imgIwls95.c 

static void 
PartitionTraverseRecursively(
  mdd_manager * mddManager, 
  vertex_t * vertex, 
  int  mddId, 
  st_table * vertexTable, 
  array_t * relationArray, 
  st_table * domainQuantifyVarMddIdTable, 
  array_t * quantifyVarMddIdArray 
)
Traverses the partition recursively, creating the relations for the intermediate vertices.

Defined in imgIwls95.c 

static bdd_t * 
PreImageByConstraintCofactoring(
  ImgTfmInfo_t * info, 
  array_t * delta, 
  bdd_t * image, 
  int  splitMethod, 
  int  turnDepth, 
  int  depth 
)
Computes preimage with constraint cofactoring method.

Defined in imgTfmBwd.c 

static bdd_t * 
PreImageByDomainCofactoring(
  ImgTfmInfo_t * info, 
  array_t * delta, 
  bdd_t * image, 
  array_t * relationArray, 
  mdd_t * cofactorCube, 
  mdd_t * abstractCube, 
  int  splitMethod, 
  int  turnDepth, 
  int  depth 
)
Computes preimage with domain cofactoring method.

Defined in imgTfmBwd.c 

static mdd_t * 
PreImageByStaticDomainCofactoring(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * from, 
  array_t * relationArray, 
  int  turnDepth, 
  int  depth 
)
Computes a preimage by static input splitting.

Defined in imgTfmBwd.c 

static mdd_t * 
PreImageBySubstitution(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  mdd_t * from 
)
Computes a preimage by Filkorn's substitution.

Defined in imgTfmBwd.c 

static int 
PreImageChooseSplitVar(
  ImgTfmInfo_t * info, 
  array_t * delta, 
  bdd_t * img, 
  int  splitMethod, 
  int  split 
)
Chooses a splitting variable for preimage.

Defined in imgTfmBwd.c 

static bdd_t * 
PreImageDeleteOneComponent(
  ImgTfmInfo_t * info, 
  array_t * delta, 
  int  index, 
  array_t ** newDelta 
)
Deletes a component in a vector. Deletes index-th component out of delta and copy it into newDelta.

Defined in imgTfmBwd.c 

static int 
PreImageKeyCompare(
  ImgCacheStKey_t * key1, 
  ImgCacheStKey_t * key2 
)
Compares two keys for preimage.

Defined in imgTfmCache.c 

static bdd_t * 
PreImageMakeRelationCanonical(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  bdd_t * image, 
  array_t * relationArray, 
  array_t ** newVector, 
  array_t ** newRelationArray 
)
Makes transition relation canonical for preimage. Quantifies out the next state variables that do not occur in the image, and when a vector exists, delete the components which do not appear in the image. If a component is constant, simplify the image with the constant value and delete the corresponding component from delta Side effect on delta. Return new image.

Defined in imgTfmBwd.c 

static bdd_t * 
PreImageMakeVectorCanonical(
  ImgTfmInfo_t * info, 
  array_t * vector, 
  bdd_t * image, 
  array_t * relationArray, 
  array_t ** newVector, 
  array_t ** newRelationArray, 
  mdd_t ** cofactorCube, 
  mdd_t ** abstractCube 
)
Makes a vector canonical for preimage. Delete all the components which doesn't appear as a support in the image. If a component is constant, simplify the image with the constant value and delete the corresponding component from delta Side effect on delta. Return new image.

Defined in imgTfmBwd.c 

static void 
PrintBddIdFromBddArray(
  array_t * bddArray 
)
Prints Ids of an array of BDDs.

Defined in imgIwls95.c 

static void 
PrintBddIdTable(
  st_table * idTable 
)
Prints the integers from a symbol table.

Defined in imgIwls95.c 

static void 
PrintClusterMatrix(
  ClusterList_t * headCluster, 
  int  nCols, 
  int * colOrder, 
  Img_DirectionType  direction 
)
Prints cluster information.

Defined in imgMlp.c 

static void 
PrintCol(
  char ** xy, 
  int  nRows, 
  int  nCols, 
  int * rowOrder, 
  int * colOrder, 
  int  from, 
  int  to 
)
Prints a column.

Defined in imgMlp.c 

static void 
PrintCtrInfoStruct(
  CtrInfo_t * ctrInfo 
)
Prints the CtrInfo_t data structure.

Defined in imgIwls95.c 

static void 
PrintFoundVariableStatistics(
  ImgTfmInfo_t * info, 
  int  preFlag 
)
Prints statistics of finding essential and dependent variables.

Defined in imgTfm.c 

static void 
PrintMatrixWithCluster(
  char ** xy, 
  ClusterList_t * headCluster, 
  int  nCols, 
  int * rowOrder, 
  int * colOrder, 
  Img_DirectionType  direction 
)
Prints a matrix with cluster information.

Defined in imgMlp.c 

static void 
PrintMatrix(
  char ** xy, 
  int  nRows, 
  int  nCols, 
  int * rowOrder, 
  int * colOrder, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int  startFunc, 
  int  lastFunc, 
  int  startVar, 
  int  lastVar 
)
Prints a maxtrix.

Defined in imgMlp.c 

static void 
PrintOption(
  Img_MethodType  method, 
  ImgTrmOption_t * option, 
  FILE * fp 
)
Prints the option values used in IWLS95 techinique for image computation.

Defined in imgIwls95.c 

static void 
PrintPartitionRecursively(
  vertex_t * vertex, 
  st_table * vertexTable, 
  int  indent 
)
Prints the partition recursively.

Defined in imgIwls95.c 

static void 
PrintPartitionedTransitionRelation(
  mdd_manager * mddManager, 
  Iwls95Info_t * info, 
  Img_DirectionType  directionType 
)
Prints info of the partitioned transition relation.

Defined in imgIwls95.c 

static void 
PrintRecursionStatistics(
  ImgTfmInfo_t * info, 
  int  preFlag 
)
Prints statistics of recursions for transition function method.

Defined in imgTfm.c 

static void 
PrintRow(
  char ** xy, 
  int  nRows, 
  int  nCols, 
  int * rowOrder, 
  int * colOrder, 
  int  from, 
  int  to 
)
Prints a row.

Defined in imgMlp.c 

static void 
PrintSmoothIntroducedCount(
  array_t * clusterArray, 
  array_t ** arraySmoothVarBddArrayPtr, 
  array_t * psBddIdArray, 
  array_t * nsBddIdArray 
)
This function is used to print information about the cluster sequence and the sequence of smooth cubes. For each cluster in sequence, it prints the number of variables quantified and the number of variables introduced.

Defined in imgIwls95.c 

static void 
PrintVarInfoStruct(
  VarInfo_t * varInfo 
)
Prints the VarInfo_t structure.

Defined in imgIwls95.c 

static void 
PrintVectorDecomposition(
  ImgTfmInfo_t * info, 
  array_t * vectorArray, 
  array_t * varArray 
)
Print the information of the decomposition.

Defined in imgTfmFwd.c 

static boolean 
ReadSetBooleanValue(
  char * string, 
  boolean  defaultValue 
)
Reads a set Boolean value.

Defined in imgTfm.c 

static int 
ReadSetIntValue(
  char * string, 
  int  l, 
  int  u, 
  int  defaultValue 
)
Reads a set integer value.

Defined in imgTfm.c 

static void 
RebuildTransitionRelation(
  ImgTfmInfo_t * info, 
  Img_DirectionType  directionType 
)
Rebuilds transition relation from function vector.

Defined in imgTfm.c 

static bdd_t * 
RecomputeImageIfNecessary(
  ImgFunctionData_t * functionData, 
  mdd_manager * mddManager, 
  bdd_t * domainSubset, 
  array_t * relationArray, 
  array_t * arraySmoothVarBddArray, 
  array_t * smoothVarCubeArray, 
  int  verbosity, 
  ImgPartialImageOption_t * PIoption, 
  array_t * toCareSetArray, 
  boolean * partial, 
  boolean  lazySiftFlag 
)
Recompute partial image by relaxing the parameters. First the threshold to trigger approximation is increased and then the threshold to approximate is increased. If both fail to produce new states, the exact image is computed (no approximations).Partial flag comes in indicating whether partial images are allowed, and leave indicating whether the image was partial or not. ASSUME that toCareSet is in terms of function->domainVars.

Side Effects partial flag is modified with each image computation. IMPORTANT NOTE: image may be in terms of domain variables even when the reverse is expected.

Defined in imgIwls95.c 

static int 
RecursiveCluster(
  mdd_manager * mddManager, 
  ClusterList_t * headCluster, 
  ClusterSortedList_t * clusterSortedList, 
  char ** xy, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  int  nActiveRows, 
  int  nClusterCols, 
  Img_DirectionType  direction, 
  int * varPos, 
  int  moveFlag, 
  ImgTrmOption_t * option 
)
Clusters recursively with affinity.

Defined in imgMlp.c 

static array_t * 
RelationArraySmoothLocalVars(
  array_t * relationArray, 
  array_t * ctrInfoArray, 
  array_t * varInfoArray, 
  st_table * bddIdToBddTable 
)
This function takes an array of relations and quantifies out the quantify variables which are local to a particular relation.

Side Effects This function fills in the "numSmoothVars", "numLocalSmoothVars", "numIntroducedVars", "maxSmoothVarIndex" fields of ctrInfoStruct corresponding to each relation. It also alters the "numCtr" and "ctrItemList" field of those quantify variables which are quantified out in this function.

Defined in imgIwls95.c 

static int 
RemoveLocalVarsInCluster(
  mdd_manager * mddManager, 
  char ** xy, 
  ClusterList_t * list, 
  int  nActiveRows, 
  int  nClusterCols, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder, 
  int  moveFlag, 
  ImgTrmOption_t * option 
)
Removes local variables in a cluster.

Defined in imgMlp.c 

static void 
ReorderPartitionedTransitionRelation(
  Iwls95Info_t * info, 
  ImgFunctionData_t * functionData, 
  Img_DirectionType  directionType 
)
Reorder partitioned transition relation.

Defined in imgIwls95.c 

static void 
ResetClusteredCofactoredRelationArray(
  mdd_manager * mddManager, 
  Iwls95Info_t * info 
)
Copy the clustered array into the clusteredcofactored array, and set the caresetarray to (1). Assumes either both the caresetarray and the cofactoredarray are NIL, or that they both contain sensible data.

Defined in imgIwls95.c 

static int 
SccSortListDecreasingWithArea(
  const void * p1, 
  const void * p2 
)
Sorts connected components with area.

Defined in imgMlp.c 

static int 
SccSortListDecreasingWithRatio(
  const void * p1, 
  const void * p2 
)
Sorts connected components with aspect ratio.

Defined in imgMlp.c 

static int 
SccSortListDecreasingWithVars(
  const void * p1, 
  const void * p2 
)
Sorts connected components with the number of variables.

Defined in imgMlp.c 

static int 
SccSortListIncreasingWithArea(
  const void * p1, 
  const void * p2 
)
Sorts connected components with area.

Defined in imgMlp.c 

static int 
SccSortListIncreasingWithRatio(
  const void * p1, 
  const void * p2 
)
Sorts connected components with aspect ratio.

Defined in imgMlp.c 

static int 
SccSortListIncreasingWithVars(
  const void * p1, 
  const void * p2 
)
Sorts connected components with the number of variables.

Defined in imgMlp.c 

static int 
SccSortRc(
  const void * p1, 
  const void * p2 
)
Sorts rows or columns using connected component index.

Defined in imgMlp.c 

static void 
SetupLazySifting(
  mdd_manager * mddManager, 
  array_t * bddRelationArray, 
  array_t * domainVarBddArray, 
  array_t * quantifyVarBddArray, 
  array_t * rangeVarBddArray, 
  int  verbosity 
)
Setups lazy sifting.

Side Effects None

Defined in imgIwls95.c 

static void 
SetupMlp(
  mdd_manager * mddManager, 
  char ** xy, 
  int  nRows, 
  int  nCols, 
  int * rowOrder, 
  int * colOrder, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * varPos, 
  array_t * nsVarBddArray, 
  int * nActiveRows, 
  int * nActiveCols, 
  array_t * nonAppearingVarBddArray, 
  Img_DirectionType  direction, 
  ImgTrmOption_t * option 
)
Setups MLP.

Defined in imgMlp.c 

static int 
SignatureCompare(
  int * ptrX, 
  int * ptrY 
)
Comparison function used by qsort to order the variables according to their signatures.

Side Effects None

Defined in imgTfmUtil.c 

static void 
SortCol(
  char ** xy, 
  int  nRows, 
  int  nCols, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int * rowOrder, 
  int * colOrder 
)
Updates matrix information properly.

Defined in imgMlp.c 

static RcListInfo_t * 
SortedListAlloc(
    
)
Allocates a list for sorting.

Defined in imgMlp.c 

static void 
SortedListDelete(
  RcListInfo_t * candList, 
  int  index 
)
Deletes a list from the sorting list.

Defined in imgMlp.c 

static void 
SortedListFree(
  RcListInfo_t * candList 
)
Frees a list used for sorting.

Defined in imgMlp.c 

static void 
SortedListInsert(
  RcListInfo_t * candList, 
  int  index, 
  int  otherIndex, 
  RcInfo_t * otherInfo, 
  int  method 
)
Inserts a list to the sorting list.

Defined in imgMlp.c 

static void 
SortedListMove(
  RcListInfo_t * candList, 
  RcInfo_t * info, 
  int  index, 
  int  method 
)
Moves a list in the sorting list.

Defined in imgMlp.c 

static mdd_t * 
SubstituteCacheResultRecur(
  mdd_t * result, 
  array_t * varArray, 
  array_t * funcArray, 
  int  pos 
)
Recursive procedure of SubstituteCacheResult.

Defined in imgTfmCache.c 

static mdd_t * 
SubstituteCacheResult(
  ImgTfmInfo_t * info, 
  array_t * keyVector, 
  array_t * cacheVector, 
  mdd_t * result 
)
Substitutes a cache result.

Defined in imgTfmCache.c 

static void 
TfmBuildRelationArray(
  ImgTfmInfo_t * info, 
  ImgFunctionData_t * functionData, 
  array_t * bitRelationArray, 
  Img_DirectionType  directionType, 
  int  writeMatrix 
)
Builds relation array from function vector or bit relation.

See Also ImgImageInfoInitializeTfm
Defined in imgTfm.c 

static int 
TfmCheckImageValidity(
  ImgTfmInfo_t * info, 
  mdd_t * image 
)
Checks the support of image.

Defined in imgTfmFwd.c 

static array_t * 
TfmCreateBitRelationArray(
  ImgTfmInfo_t * info, 
  int  composeIntermediateVars, 
  int  findIntermediateVars 
)
Creates the bit relations.

See Also ImgImageInfoInitializeTfm
Defined in imgTfm.c 

static array_t * 
TfmCreateBitVector(
  ImgTfmInfo_t * info, 
  int  composeIntermediateVars, 
  int  findIntermediateVars 
)
Creates function vector.

See Also ImgImageInfoInitializeTfm
Defined in imgTfm.c 

static ImgTfmInfo_t * 
TfmInfoStructAlloc(
  Img_MethodType  method 
)
Allocates and initializes the info structure for transition function method.

Defined in imgTfm.c 

static void 
TfmSetupPartialTransitionRelation(
  ImgTfmInfo_t * info, 
  array_t ** partialRelationArray 
)
Builds partial vector and relation array.

See Also ImgImageInfoInitializeTfm
Defined in imgTfm.c 

static mdd_t * 
TrmEliminateDependVars(
  Img_ImageInfo_t * imageInfo, 
  array_t * relationArray, 
  mdd_t * states, 
  mdd_t ** dependRelations 
)
Eliminates dependent variables from a transition relation. Returns a simplified copy of the given states if successful; NULL otherwise.

Side Effects relationArray is also modified.

Defined in imgIwls95.c 

static ImgTrmOption_t * 
TrmGetOptions(
    
)
Gets the necessary options for computing the image and returns in the option structure.

Defined in imgIwls95.c 

static int 
TrmSignatureCompare(
  int * ptrX, 
  int * ptrY 
)
Comparison function used by qsort to order the variables according to their signatures.

Side Effects None

Defined in imgIwls95.c 

static void 
UpdateDisapearingPsVarsInCluster(
  mdd_manager * mddManager, 
  char ** xy, 
  int  nActiveRows, 
  int  nActiveCols, 
  int * rowOrder, 
  int * colOrder, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  ClusterList_t * list, 
  int  moveFlag, 
  ImgTrmOption_t * option 
)
Finds disappearing present state variables in a cluster.

Defined in imgMlp.c 

static void 
UpdateDisapearingPsVars(
  mdd_manager * mddManager, 
  char ** xy, 
  int  nActiveRows, 
  int  nActiveCols, 
  int * rowOrder, 
  int * colOrder, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo, 
  int  row, 
  ImgTrmOption_t * option 
)
Finds disappearing present state variables in a row.

Defined in imgMlp.c 

static array_t * 
UpdateInfoArrays(
  CtrInfo_t * ctrInfo, 
  st_table * bddIdToBddTable, 
  int * numSmoothVarsRemainingPtr, 
  int * numIntroducedVarsRemainingPtr 
)
The support variable list (varItemList) of the cluster (ctrInfo) is traversed and depending upon the type of the variable and the number of unordered clustered relations which depend on that variable following actions are taken: a. If the variable is of range type: This implies that this variable is appearing for the first time in the product. Since it is already introduced in the product, the cost function of any other unordered relation which depends on this variable will get modified. The numIntroducedVariables field of each of the cluster which depends on this variable is decreased by 1. Also this varItemStruct corresponding to this variable is removed from the varItemList field of the cluster. b. If the variable is of domain or quantify type: b1. If number of clusters which depend on this variable is 1 (numCtr == 1): In this case, this variable can be quantified out once the chosen cluster is multiplied in the product. Hence the variable is put in the smoothVarBddArray. b2. If (numCtr == 2) In this case, there is one more unordered cluster which depends on this variable. But once the current cluster is multiplied in the product, the "numLocalSmoothVars" field of ctrInfo corresponding to the other dependent cluster needs to be increased by 1. b3. If (numCtr > 2) In this case, we just need to decrease the numCtr of the variable by 1. In any case, for each varInfo in the support variable list (varItemList) of the cluster (ctrInfo) the following invariant is maintained: varInfo->numCtr == lsLength(varInfo->ctrItemList)

Side Effects The fields of ctrInfo and varInfo are changed as mentioned above.

Defined in imgIwls95.c 

static void 
UpdateNonappearingNsVars(
  mdd_manager * mddManager, 
  array_t * nsVarBddArray, 
  int  nRows, 
  RcInfo_t * rowInfo, 
  int * rowOrder, 
  array_t * nonAppearingVarBddArray 
)
Finds non-appearing next state variables.

Defined in imgMlp.c 

static void 
UpdateQuantificationSchedule(
  Iwls95Info_t * info, 
  ImgFunctionData_t * functionData, 
  Img_DirectionType  directionType 
)
Updates quantification schedule.

Defined in imgIwls95.c 

static VarInfo_t * 
VarInfoStructAlloc(
    
)
Allocates and initializes memory for varInfoStruct.

Defined in imgIwls95.c 

static void 
VarInfoStructFree(
  VarInfo_t * varInfo 
)
Frees the memory associated with varInfoStruct.

Defined in imgIwls95.c 

static void 
VarItemStructFree(
  VarItem_t * varItem 
)
Frees the memory associated with VarItemStruct

Defined in imgIwls95.c 

static int 
VectorCompare(
  array_t * vector1, 
  array_t * vector2 
)
Compares two vectors.

Defined in imgTfmCache.c 

static int 
VectorHash(
  ImgCacheTable_t * table, 
  array_t * delta, 
  bdd_t * constraint 
)
Returns hash value of a vector.

Defined in imgTfmCache.c 

static int 
VectorSortCompareWithConstraint(
  array_t * vector1, 
  array_t * vector2 
)
Compares two vectors considering substitution.

Defined in imgTfmCache.c 

static int 
VectorSortCompare(
  array_t * vector1, 
  array_t * vector2 
)
Compares two vectors considering substitution.

Defined in imgTfmCache.c 

static int 
VectorStHash(
  char * key, 
  int  modulus 
)
Returns hash value of a vector for st_table.

Defined in imgTfmCache.c 

static void 
WriteMatrix(
  FILE * fout, 
  char ** xy, 
  int  nRows, 
  int  nCols, 
  int * rowOrder, 
  int * colOrder, 
  RcInfo_t * rowInfo, 
  RcInfo_t * colInfo 
)
Writes a matrix to a file.

Defined in imgMlp.c 

static void 
WriteOrder(
  FILE * fout, 
  int  nCols, 
  int * colOrder, 
  RcInfo_t * colInfo 
)
Writes variable order in coulumn of the matrix.

Defined in imgMlp.c 

static int 
linearCheckRange(
  const void * tc 
)
compare function for checking range of cluster

Defined in imgLinear.c
Last updated on 20050519 00h50