img package abstract

AddDontCareToTransitionFunction(): Adds dont cares to function vector or relation.
BddArrayDup(): Duplicates an array of BDDs.
BddLinearAndSmooth(): Returns a BDD after taking the product of fromSet with the BDDs in the relationArray and quantifying out the variables using the schedule given in the arraySmoothVarBddArray.
BlockLowerTriangle(): Makes dependence matrix block lower triangle.
CacheDestroyEntry(): Destroys a cache entry.
CalculateBenefit(): Gets the necessary options for computing the image and returns in the option structure.
CheckCluster(): Checks cluster for sanity.
CheckCtrInfoArray(): Checks the validity of an array of CtrInfoStructs.
CheckCtrInfo(): Checks the validity of a CtrInfoStruct.
CheckIfValidSplitOrGetNew(): Checks the splitting variable is valid and chooses new one if not valid.
CheckImageValidity(): Checks the validity of image
CheckMatrix(): Checks a matrix for sanity.
CheckNondeterminism(): Checks whether the network is nondeterministic.
CheckPreImageVector(): Checks sanity of a vector for preimage.
CheckQuantificationSchedule(): Given an array of BDD's representing the relations and another array of BDD cubes (in the form of array of bdd_t of variable) representing the quantification schedule, this function checks if the schedule is correct.
CheckSortedList(): Checks the sorting list for sanity.
CheckVarInfoArray(): Checks the validity of an array of VarInfoStruct.
ChooseInputSplittingVariable(): Finds a splitting variable for input splitting.
ChooseOutputSplittingVariable(): Finds a splitting variable for output splitting.
ChoosePartialVars(): Chooses variables for static splitting.
ClusterSortedListInsert(): Inserts a cluster in a sorting list.
CompareBddPointer(): Compares two function BDD pointers of components.
CompareIndex(): Compares two variable indices of components.
ComputeClippedAndAbstract(): Clipping and-abstract
ComputeLambdaMlp(): Compute variable lifetime lambda.
ComputeSubsetOfIntermediateProduct(): Approximate intermediate product according to method.
ComputeSupportLambda(): Computes variable lifetime lambda.
CopyArrayBddArray(): Copy an array of bdd array.
CountClusterList(): Returns the number of lists in a cluster list.
CountClusterSortedList(): Returns the number of lists in a sorted cluster list.
CreateBitRelationArray(): Creates the bit relations and the mdd id array for the quantifiable variables and stores it in the ImgIwls95 structure.
CreateClusters(): Forms the clusters of relations based on BDD size heuristic.
CreateInitialCluster(): Creates an initial cluster using ARDC decomposition.
CtrInfoMaxIndexCompare(): Compare function used to sort the ctrInfoStruct based on the maxSmoothVarIndex field.
CtrInfoStructAlloc(): Allocates and initializes memory for ctrInfoStruct.
CtrInfoStructFree(): Frees the memory associated with ctrInfoStruct.
CtrItemStructFree(): Frees the memory associated with CtrItemStruct
DomainCofactoring(): Performs domain cofactoring on a vector and from set with respect to a variable.
FindAndMoveSingletonCols(): Finds and moves singleton columns.
FindAndMoveSingletonRows(): Finds and moves singleton rows.
FindDecomposableVariable(): Finds a decomposable variable (articulation)
FindIntermediateSupport(): Finds all other fanin intermediate functions of a given intermediate function.
FindIntermediateVarsRecursively(): Traverses the partition recursively, creating the functions for the intermediate vertices.
FreeBitRelationArray(): Frees bit relation array and the quantification variables.
FreeClusteredCofactoredRelationArray(): Frees the clusteredcofactoredrelationarray
FreeSccList(): Frees list of connected components.
GetIntermediateRelationsRecursively(): Traverses the partition recursively, creating the relations for the intermediate vertices.
GetRecursionStatistics(): Returns the statistics of recursions of transition function method.
HashIdToBddTable(): Hashes bdd id to bdd in the table.
HookInfoFunction(): Flushes cache entries in a list.
ImageByInputSplit(): Computes an image by input splitting.
ImageByOutputSplit(): Computes an image by output splitting.
ImageByStaticInputSplit(): Computes an image by static input splitting.
ImageComputeMonolithic(): A generic routine for computing the image.
ImageDecomposeAndChooseSplitVar(): Try to decompose function vector and find a splitting variable for each decomposed block.
ImageFast2(): Fast image computation when function vector contains only two functions.
ImageKeyCompare(): Compares two keys.
ImageKeySortCompare(): Compares two keys considering substitution.
ImgAbstractRelationArray(): Smoothes a relation array with respect to a cube.
ImgAbstractTransitionFunction(): Abstracts out given variables from transition function.
ImgAbstractTransitionRelationIwls95(): Abstracts out given variables from transition relation.
ImgAbstractTransitionRelationMono(): Abstracts out given variables from transition relation.
ImgAddDontCareToTransitionFunction(): Adds a dont care set to the transition function and relation.
ImgAddDontCareToTransitionRelationMono(): Add dont care to transition relation.
ImgApproximateTransitionFunction(): Approximate transition function.
ImgApproximateTransitionRelationIwls95(): Approximate transition relation.
ImgApproximateTransitionRelationMono(): Approximates transition relation.
ImgArrayBddArrayCheckValidity(): This function checks the validity of an array of array of BDD nodes.
ImgBddArrayCheckValidity(): This function checks the validity of array of BDD nodes.
ImgBddCheckValidity(): This function checks the validity of a BDD.
ImgBddGetSupportIdTable(): Returns the st_table containing the bdd id of the support variables of the function.
ImgBddLinearAndSmooth(): Returns a BDD after taking the product of fromSet with the BDDs in the relationArray and quantifying out the variables using the schedule given in the arraySmoothVarBddArray.
ImgCacheDestroyTable(): Destroys a cache table.
ImgCacheInitTable(): Initializes a cache table.
ImgCacheInsertTable(): Inserts an entry into cache table.
ImgCacheLookupTable(): Lookups cache table.
ImgCheckConstConstrain(): Quick checking whether the results of constrain between two functions are constant.
ImgCheckEquivalence(): Checks whether a vector is equivalent to a relation array.
ImgCheckMatching(): Checks whether a vector corresponds to its relation array.
ImgCheckRangeTestAndOverapproximate(): Check range of variables
ImgCheckToCareSetArrayChanged(): Checks whether toCareSetArray changed.
ImgChooseTrSplitVar(): Chooses splitting variables for static splitting.
ImgClusterRelationArray(): Clusters relation array and makes quantification schedule.
ImgCofactorRelationArray(): Cofactors a relation array with respect to a function.
ImgCofactorVector(): Cofactors a function vector with respect to a function.
ImgComponentAlloc(): Allocates a component.
ImgComponentCopy(): Copies a component
ImgComponentFree(): Frees a component.
ImgComponentGetSupport(): Gets the supports of a component.
ImgComposeConstIntermediateVars(): Compose the constant intermediate variable functions.
ImgConstConstrain(): Checks whether the result of constrain is constant.
ImgCountBddSupports(): Returns the number of BDD supports in a function.
ImgCountOnsetDisjunctiveArray(): Count onset of relation array
ImgDecideSplitOrConjoin(): Decides whether to split or to conjoin.
ImgDuplicateTransitionFunction(): Duplicates transition function.
ImgDuplicateTransitionRelationIwls95(): Duplicates transition relation.
ImgDuplicateTransitionRelationMono(): Duplicates transition relation.
ImgExistConstIntermediateVar(): Checks whether there is a constant function of intermediate variables.
ImgFlushCache(): Flushes all cache entries.
ImgFreeTrmOptions(): Frees the option structure for transition relation method.
ImgGetAbstractedCofactoredRelationArray(): Smothes and cofactors a relation array.
ImgGetAbstractedRelationArray(): Smoothes a relation array with respect to a cube.
ImgGetCofactoredAbstractedRelationArray(): Cofactors and smooths a relation array.
ImgGetCofactoredRelationArray(): Cofactors a relation array with respect to a function.
ImgGetCofactoredVector(): Cofactors a function vector with respect to a function.
ImgGetComposedFunction(): Returns a function composed all intermediate variables.
ImgGetConstrainedRelationArray(): Constrains a relation array with respect to a constraint.
ImgGetConstrainedVector(): Constrains a function vector with respect to a constraint.
ImgGetLatchComponent(): Returns the first latch component.
ImgGetPartialImageOptions(): Get partial image options.
ImgGetQuantificationSchedule(): Returns quantification schedule for a given relation array.
ImgGetTransitionFunction(): Returns current transition function.
ImgGetTransitionRelationIwls95(): Returns current transition relation.
ImgGetTrmOptions(): Allocates an option structure for transition relation method.
ImgImageAllowPartialImageIwls95(): Sets the flag to allow partial images.
ImgImageByHybridWithStaticSplit(): Computes an image by transition relation.
ImgImageByHybrid(): Computes an image by transition relation.
ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp(): Constrains/Adds dont-cares to the bit relation and creates a new transition relation.
ImgImageConstrainAndClusterTransitionRelationMono(): Constrains/adds dont-cares to the bit relation and creates a new transition relation.
ImgImageConstrainAndClusterTransitionRelationTfm(): Constrains the bit function and relation and creates a new transition function vector and relation.
ImgImageFreeClusteredTransitionRelationIwls95(): Frees current transition relation and associated quantification schedule for the given direction.
ImgImageFreeClusteredTransitionRelationTfm(): Frees current transition function vector and relation for the given direction.
ImgImageInfoComputeBwdIwls95(): Computes the backward image of domainSubset.
ImgImageInfoComputeBwdMono(): Computes the backward image of a set of states between fromLowerBound and fromUpperBound.
ImgImageInfoComputeBwdTfm(): Computes the backward image of domainSubset.
ImgImageInfoComputeBwdWithDomainVarsIwls95(): Computes the backward image of a set of states.
ImgImageInfoComputeBwdWithDomainVarsMono(): Computes the backward image of a set of states between fromLowerBound and fromUpperBound.
ImgImageInfoComputeBwdWithDomainVarsTfm(): Computes the backward image of a set of states.
ImgImageInfoComputeFwdIwls95(): Computes the forward image of a set of states.
ImgImageInfoComputeFwdMono(): Computes the forward image of a set of states between fromLowerBound and fromUpperBound.
ImgImageInfoComputeFwdTfm(): Computes the forward image of a set of states.
ImgImageInfoComputeFwdWithDomainVarsIwls95(): Computes the forward image of a set of states in terms of domain variables.
ImgImageInfoComputeFwdWithDomainVarsMono(): Computes the forward image on domain variables of a set of states between fromLowerBound and fromUpperBound.
ImgImageInfoComputeFwdWithDomainVarsTfm(): Computes the forward image of a set of states in terms of domain variables.
ImgImageInfoFreeIwls95(): Frees the memory associated with imageInfo.
ImgImageInfoFreeMono(): Frees the method data associated with the monolithic method.
ImgImageInfoFreeTfm(): Frees the memory associated with imageInfo.
ImgImageInfoInitializeIwls95(): Initializes an image data structure for image computation using the Iwls95 technique.
ImgImageInfoInitializeMono(): Initializes an image structure for image computation using a monolithic transition relation.
ImgImageInfoInitializeTfm(): Initializes an image data structure for image computation using transition function method.
ImgImageInfoPrintMethodParamsIwls95(): Prints information about the IWLS95 method.
ImgImageInfoPrintMethodParamsMono(): Prints information about the IWLS95 method.
ImgImageInfoPrintMethodParamsTfm(): Prints information about the transition function method.
ImgImageWasPartialIwls95(): Checks if the last image/preimage was partial.
ImgIsPartitionedTransitionRelationTfm(): Check whether transition relation is built in hybrid.
ImgLinearAddConjunctIntoArray(): Add conjunct into array
ImgLinearAddConjunctIntoClusterArray(): Add Conjunct into Cluster Array
ImgLinearAddNextStateCase(): Add singleton next state variable case into array
ImgLinearAddSingletonCase(): Find the case that the relation contains only one next state varaible
ImgLinearBuildConjunctArrayWithQuotientCC(): Order the each connected component
ImgLinearBuildInitialCandidate(): Build data structure for clustering
ImgLinearCAPOInterfaceAux(): Make interface files for CAPO
ImgLinearCAPOInterfaceConjunctNet(): Make interface files for CAPO
ImgLinearCAPOInterfaceConjunctNodes(): Make interface files for CAPO
ImgLinearCAPOInterfaceConjunctPl(): Make interface files for CAPO
ImgLinearCAPOInterfaceConjunctScl(): Make interface files for CAPO
ImgLinearCAPOInterfaceVariableNet(): Make interface for CAPO
ImgLinearCAPOInterfaceVariableNodes(): Make interface for CAPO
ImgLinearCAPOInterfaceVariablePl(): Make interface for CAPO
ImgLinearCAPOInterfaceVariableScl(): Make interface for CAPO
ImgLinearCAPOReadConjunctOrder(): Read result of CAPO
ImgLinearCAPOReadVariableOrder(): Read result of CAPO
ImgLinearCAPORun(): Run batch job of CAPO
ImgLinearClusterRelationArray(): Cluster fine grain transition relation
ImgLinearClusterSameSupportSet(): Cluster the relation that has same support set
ImgLinearClusterUsingHeap(): Apply clustering with priority queue
ImgLinearClusteringByConstraints(): Apply clustering with given priority function
ImgLinearClusteringIteratively(): Apply clustering iteratively
ImgLinearClusteringPairSmooth(): Clustering pair of transition relation
ImgLinearClusteringSmooth(): Apply clustering while quantifying the variables that are isolated
ImgLinearClustering(): Main function of clustering
ImgLinearCompareAffinityDeadLive(): Priority function for clutering
ImgLinearCompareConjunctDummy(): Priority function for clutering
ImgLinearCompareConjunctIndex(): Priority function for clutering
ImgLinearCompareConjunctRangeMinusDomain(): Priority function for clutering
ImgLinearCompareConjunctSize(): Priority function for clutering
ImgLinearCompareDeadAffinityLive(): Priority function for clutering
ImgLinearCompareDeadLiveAffinity(): Priority function for clutering
ImgLinearCompareLiveAffinityDead(): Priority function for clutering
ImgLinearCompareVarDummyLarge(): Priority function for clutering
ImgLinearCompareVarEffFromLarge(): Priority function for clutering
ImgLinearCompareVarEffFromSmall(): Priority function for clutering
ImgLinearCompareVarId(): Priority function for clutering
ImgLinearCompareVarIndex(): Priority function for clutering
ImgLinearCompareVarSize(): Priority function for clutering
ImgLinearComputeLifeTime(): Compute life time of variables
ImgLinearConjunctArrayRefine(): Refine conjunction array to fill the empty slot.
ImgLinearConjunctOrderMainCC(): Order the fine grain transition relation.
ImgLinearConjunctOrderMain(): Main function of linear arrangement
ImgLinearConjunctQuit(): Free conjunct_t data structure
ImgLinearConjunctRefine(): Refine conjunction array to fill the empty slot.
ImgLinearConjunctionOrder(): Generate linear arrangement with CAPO
ImgLinearConnectedComponent(): Find the connected component from fine grain transition relation
ImgLinearExpandSameSupportSet(): Find transtion relations that have smae support set
ImgLinearExtractNextStateCase(): Extract the relation that contains next state varaibles only
ImgLinearExtractRelationArrayT(): Create relation array for image computation from Relation_t data structure
ImgLinearExtractRelationArray(): Create relation array for image computation from Relation_t data structure
ImgLinearExtractSingletonCase(): Extract the relation contains only one next state varaible
ImgLinearFindConnectedComponent(): Find the connected component from fine grain transition relation
ImgLinearFindSameSupportConjuncts(): Find the conjuncts that have same support variables.
ImgLinearFreeSmoothArray(): Free smooth variable array
ImgLinearGetSupportBddId(): Find support varaibles of bdd
ImgLinearHeapCompareAffinityDeadLive(): Priority function for clutering
ImgLinearHeapCompareDeadAffinityLive(): Priority function for clutering
ImgLinearHeapCompareDeadLiveAffinity(): Priority function for clutering
ImgLinearHeapCompareLiveAffinityDead(): Priority function for clutering
ImgLinearInsertClusterCandidate(): Add candidates for clustering
ImgLinearInsertPairClusterCandidate(): Insert initial candidate set
ImgLinearIsSameConjunct(): Check if given conjuncts have same support variables
ImgLinearMakeSmoothVarBdd(): Make the array of smooth variables
ImgLinearOptimizeAll(): Function for optimizing state varaibles
ImgLinearOptimizeInternalVariables(): Remove intermediate variables after propagating constant.
ImgLinearOptimizeStateVariables(): Remove corresponding current (next) state variables if the next (current state variables are eleminated aftetr clustering
ImgLinearPrintDebugInfo(): Print information of debug information
ImgLinearPrintMatrixFull(): Print matrix
ImgLinearPrintMatrix(): Print matrix
ImgLinearPrintTransitionInfo(): Print transition relation info
ImgLinearPrintVariableProfile(): Print profile of variables
ImgLinearPropagateConstant(): Propagate the constant to simply the transition relation
ImgLinearQuantifyVariablesFromConjunct(): Apply quantification with candidate variables
ImgLinearRefineRelation(): Refine transition relation.
ImgLinearRelationInit(): Initialize the data structure for linear arrangement and clustering.
ImgLinearRelationQuit(): Free Relation_t data structure
ImgLinearSetEffectiveNumberOfStateVariable(): Get the number of state variables after applying optimization
ImgLinearUpdateVariableArrayWithId(): Update variable array with id of variable id
ImgLinearVariableArrayInit(): Initialize variable array
ImgLinearVariableArrayQuit(): Free variable array
ImgLinearVariableLifeQuit(): Free variable life array
ImgLinearVariableOrder(): Make interface for variable ordering
ImgMinimizeImageArrayWithCareSetArrayInSitu(): Minimize array of bdds wrt a set of constraints
ImgMinimizeImageArrayWithCareSetArray(): Minimize array of bdds wrt a set of constraints
ImgMinimizeTransitionFunction(): Minimizes transition function with given set of constraints.
ImgMinimizeTransitionRelationIwls95(): Minimizes transition relation with given set of constraints.
ImgMinimizeTransitionRelationMono(): Minimizes transition relation with given constraint.
ImgMlpClusterRelationArray(): Clusters relation array and makes quantification schedule.
ImgMlpComputeLambda(): Compute variables lifetime using MLP.
ImgMlpGetQuantificationSchedule(): Makes a quantification schedule using MLP.
ImgMlpMultiwayAndSmooth(): Performs multiway and_smooth using MLP.
ImgMlpOrderRelationArray(): Orders relation array and makes quantification schedule.
ImgMlpPrintDependenceMatrix(): Prints dependence matrix.
ImgMlpReadClusterFile(): Reads cluster file.
ImgMlpWriteClusterFile(): Writes cluster to a file.
ImgMultiwayLinearAndSmoothWithFrom(): Returns the result after existentially quantifying a set of variables after taking the product of the array of relations.
ImgMultiwayLinearAndSmooth(): Returns the result after existentially quantifying a set of variables after taking the product of the array of relations.
ImgPercentVectorDependency(): Returns the percent of non-zero elements in dependency matrix.
ImgPreImageByHybridWithStaticSplit(): Computes a preimage by transition relation.
ImgPreImageByHybrid(): Computes a preimage by transition relation.
ImgPrintCacheStatistics(): Prints cache statistics for transition function method.
ImgPrintIntegerArray(): Prints integers from an array.
ImgPrintPartialImageOptions(): Prints Partial Image options.
ImgPrintPartitionedTransitionRelation(): Prints info of the partitioned transition relation.
ImgPrintPartition(): Prints the given parition.
ImgPrintVarIdTable(): Prints the content of a table containing integers.
ImgPrintVectorDependency(): Prints vector dependencies with support.
ImgReplaceIthPartitionedTransitionRelationIwls95(): Replace ith partitioned transition relation.
ImgReplaceIthTransitionFunction(): Replace ith transition function.
ImgResetMethodDataLinearComputeRange(): Turn off option to apply linear based image computation by comsidering range of state variables
ImgRestoreTransitionFunction(): Restores original transition function from saved.
ImgRestoreTransitionRelationIwls95(): Restores original transition relation from saved.
ImgRestoreTransitionRelationMono(): Restores original transition relation from saved.
ImgSetMethodDataLinearComputeRange(): Turn on option to apply linear based image computation by comsidering range of state variables
ImgSubstituteArray(): Substitutes variables between domain and range.
ImgSubstitute(): Substitutes variables between domain and range.
ImgSupportClear(): Clears a support array.
ImgSupportCopy(): Copies the supports of a component.
ImgSupportCount(): Returns the number of support of a support array.
ImgSupportPrint(): Prints a support array.
ImgTfmEliminateDependVars(): Eliminates dependent variables from transition function.
ImgTfmGetOptions(): Gets the necessary options for computing the image and returns in the option structure.
ImgTfmImage(): Computes an image with transition function method.
ImgTfmPreImage(): Computes a preimage with transition function method.
ImgTrmEliminateDependVars(): Eliminates dependent variables from transition relation.
ImgUpdateTransitionFunction(): Overwrites transition function with given.
ImgUpdateTransitionRelationIwls95(): Overwrites transition relation with given.
ImgVectorBddSize(): Returns the shared BDD size of a vector.
ImgVectorConstrain(): Constrains a function vector with respect to a constraint.
ImgVectorCopy(): Copies a vector.
ImgVectorFree(): Frees a function vector.
ImgVectorFunctionSize(): Returns the number of functions in a vector.
ImgVectorMinimize(): Minimizes a function vector and a from set with respect to an essential cube.
ImgWriteSupportMatrix(): Writes a gnuplot file with support matrix.
Img_AbstractTransitionRelation(): Abstracts out given variables from transition relation.
Img_AddDontCareToImage(): Adds a dont care set to the given image.
Img_ApproximateImage(): Approximate image.
Img_ApproximateTransitionRelation(): Approximate transition relation.
Img_ClusterRelationArray(): Clusters relation array and returns quantification schedule.
Img_ComposeIntermediateNodes(): Replace partitioned transition relation.
Img_DupTransitionRelation(): Duplicates the transition relation for backup.
Img_End(): End the image package.
Img_ForwardImageInfoConjoinWithWinningStrategy(): Create restricted transition relations by conjoining with winning strategy
Img_ForwardImageInfoRecoverFromWinningStrategy(): Restore original transition relations from restricted transition relations by conjoining with winning strategy
Img_GetNumberOfImageComputation(): Returns number of image/preimage computation.
Img_GetPartitionedTransitionRelation(): Returns current partitioned transition relation.
Img_GuidedSearchReadOverApproxMinimizeMethod(): Returns the guided search minimize method of overapproximating the transition relation.
Img_GuidedSearchReadUnderApproxMinimizeMethod(): Returns the guided search minimize method of underapproximating the transition relation.
Img_ImageAllowPartialImage(): Sets the flag to allow the next image computation to return a subset of the actual image.
Img_ImageConstrainAndClusterTransitionRelation(): Constrains/adds dont-cares to the bit relations with the given constraint and creates a new transtion relation.
Img_ImageGetUnreachableStates(): Get unreachable states
Img_ImageInfoComputeBwdWithDomainVars(): Computes the backward image of a set expressed in terms of domain variables.
Img_ImageInfoComputeBwd(): Computes the backward image of a set.
Img_ImageInfoComputeEXWithDomainVars(): Computes the backward image of a set expressed in terms of domain variables.
Img_ImageInfoComputeFwdWithDomainVars(): Computes the forward image of a set and expresses it in terms of domain variables.
Img_ImageInfoComputeFwd(): Computes the forward image of a set.
Img_ImageInfoComputeImageWithDomainVars(): Computes the forward image of a set and expresses it in terms of domain variables.
Img_ImageInfoComputePreImageWithDomainVars(): Computes the backward image of a set expressed in terms of domain variables.
Img_ImageInfoFreeFAFW(): Frees the memory associated with imageInfo.
Img_ImageInfoFree(): Frees the memory associated with imageInfo.
Img_ImageInfoInitialize(): Initializes an imageInfo structure for the given method and direction.
Img_ImageInfoObtainMethodTypeAsString(): Returns a string giving the method type of an imageInfo.
Img_ImageInfoObtainMethodType(): Returns the method type of an imageInfo.
Img_ImageInfoObtainOptimizeType(): Returns the method type of an imageInfo.
Img_ImageInfoPrintMethodParams(): Prints information about the image technique currently used.
Img_ImageInfoResetLinearComputeRange(): Reset linear compute range flag.
Img_ImageInfoResetUseOptimizedRelationFlag(): reset optimization relation flag .
Img_ImageInfoSetLinearComputeRange(): Set linear compute range flag.
Img_ImageInfoSetUseOptimizedRelationFlag(): set optimization relation flag .
Img_ImageInfoUpdateVariables(): Updates present state and primary input variables.
Img_ImagePrintPartialImageOptions(): Prints partial image options.
Img_ImageWasPartial(): Queries whether the last image computation was partial.
Img_Init(): Initialize the image package.
Img_IsPartitionedTransitionRelation(): Returns 1 if partitioned transition relation is used.
Img_IsQuantifyArraySame(): Check the given address of array+t is same as the functionData.quantifyArray.
Img_IsQuantifyCubeSame(): Check the given address of mdd_t is same as the functionData.quantifyCube.
Img_IsTransitionRelationOptimized(): Check whether the given transition relation is optimized.
Img_MinimizeImageArray(): Minimizes a single bdd with a set of constraint.
Img_MinimizeImage(): Minimizes an image with given constraint.
Img_MinimizeTransitionRelation(): Minimizes transition relation with given constraint if it hasn't been minimized already.
Img_MultiwayLinearAndSmooth(): Returns the result after existentially quantifying a set of variables after taking the product of the array of relations.
Img_PrintHybridOptions(): Prints the options for hybrid image computation.
Img_PrintMlpOptions(): Prints the options for MLP image computation.
Img_PrintPartitionedTransitionRelation(): Prints info of the partitioned transition relation.
Img_PrintTfmOptions(): Prints the options for image computation using transition function method.
Img_ReadMinimizeMethod(): Returns current method of minimizing transition relation.
Img_ReadPrintMinimizeStatus(): Reads the flag whether to print the status of minimizing transition relation.
Img_ReorderPartitionedTransitionRelation(): Reorder partitioned transition relation.
Img_ReplaceIthPartitionedTransitionRelation(): Replace ith partitioned transition relation.
Img_ReplacePartitionedTransitionRelation(): Replace partitioned transition relation.
Img_ResetNumberOfImageComputation(): Resets number of image/preimage computation.
Img_ResetTrMinimizedFlag(): Resets the flag that transition relation is minimized.
Img_RestoreTransitionRelation(): Restores original transition relation from saved.
Img_SetPrintMinimizeStatus(): Sets the flag whether to print the status of minimizing transition relation.
Img_Substitute(): Substitutes variables between domain and range.
Img_TfmCheckGlobalCache(): Checks whether a global cache is used for transition function method.
Img_TfmFlushCache(): Frees all cache contents of image computation using transition function method.
Img_TfmGetCacheStatistics(): Gets the statistics of image cache of transition function method.
Img_TfmGetRecursionStatistics(): Gets the statistics of recursions of transition function method.
Img_TfmPrintCacheStatistics(): Prints the statistics of image cache of transition function method.
Img_TfmPrintRecursionStatistics(): Prints the statistics of recursions for transition function method.
Img_TfmPrintStatistics(): Prints the statistics of image cache and recursions in in transition function method.
Img_UpdateQuantificationSchedule(): Updates quantification schedule.
Img_UserSpecifiedMethod(): Return the image method preferred by the user.
Iwls95InfoStructAlloc(): Allocates and initializes the info structure for IWLS95 technique.
KeyStHash(): Returns hash value of a key for st_table.
MakeSmoothVarCubeArray(): Returns array of cubes of smoothing variables.
MddSizeCompare(): Compare the size of two MDDs.
MinimizeTransitionFunction(): Minimizes function vector or relation with given constraint.
MlpCluster(): Clusters on the ordered bits.
MlpCountSupport(): Counts the number of supports of the list.
MlpDecomposeScc(): Performs connected component decomposition.
MlpNumQuantifyVars(): Retuns the number of variables to be quantified in a list.
MlpPostProcess(): Performs a postprocessing after MLP.
MlpSupportAffinity(): Computes the affinity of two lists.
MoveBestCols(): Finds and moves the best column iteratively.
MoveBestRows(): Finds and moves the best row iteratively.
MoveColToLeft(): Moves a column to the left of the active region.
MoveColToRight(): Moves a column to the tight of the active region.
MoveRowToBottom(): Moves a row to the bottom of the active region.
MoveRowToTop(): Moves a row to the top of the active region.
MoveSingletonCol(): Moves a singleton column.
MoveSingletonRow(): Moves a singleton row.
NumOfSccs(): Returns the number of connected components in the list.
OrderClusterOrder(): Takes an array of relations and does order, cluster, order on it according to the IWLS95 method. This forms a heuristically optimized clustered transition relation, plus a quantification schedule that goes with it.
OrderRelationArrayAux(): An auxiliary routine for orderRelationArray to order the clusters.
OrderRelationArray(): Returns an array of ordered relations and an array of BDD cubes (array of BDDs).
PartitionTraverseRecursively(): Traverses the partition recursively, creating the relations for the intermediate vertices.
PreImageByConstraintCofactoring(): Computes preimage with constraint cofactoring method.
PreImageByDomainCofactoring(): Computes preimage with domain cofactoring method.
PreImageByStaticDomainCofactoring(): Computes a preimage by static input splitting.
PreImageBySubstitution(): Computes a preimage by Filkorn's substitution.
PreImageChooseSplitVar(): Chooses a splitting variable for preimage.
PreImageDeleteOneComponent(): Deletes a component in a vector.
PreImageKeyCompare(): Compares two keys for preimage.
PreImageMakeRelationCanonical(): Makes transition relation canonical for preimage.
PreImageMakeVectorCanonical(): Makes a vector canonical for preimage.
PrintBddIdFromBddArray(): Prints Ids of an array of BDDs.
PrintBddIdTable(): Prints the integers from a symbol table.
PrintClusterMatrix(): Prints cluster information.
PrintCol(): Prints a column.
PrintCtrInfoStruct(): Prints the CtrInfo_t data structure.
PrintFoundVariableStatistics(): Prints statistics of finding essential and dependent variables.
PrintMatrixWithCluster(): Prints a matrix with cluster information.
PrintMatrix(): Prints a maxtrix.
PrintOption(): Prints the option values used in IWLS95 techinique for image computation.
PrintPartitionRecursively(): Prints the partition recursively.
PrintPartitionedTransitionRelation(): Prints info of the partitioned transition relation.
PrintRecursionStatistics(): Prints statistics of recursions for transition function method.
PrintRow(): Prints a row.
PrintSmoothIntroducedCount(): Prints information about the schedule of clusters and the the corresponding smooth cubes.
PrintVarInfoStruct(): Prints the VarInfo_t structure.
PrintVectorDecomposition(): Print the information of the decomposition.
ReadSetBooleanValue(): Reads a set Boolean value.
ReadSetIntValue(): Reads a set integer value.
RebuildTransitionRelation(): Rebuilds transition relation from function vector.
RecomputeImageIfNecessary(): Recompute partial image by relaxing the parameters.
RecursiveCluster(): Clusters recursively with affinity.
RelationArraySmoothLocalVars(): This function takes an array of relations and quantifies out the quantify variables which are local to a particular relation.
RemoveLocalVarsInCluster(): Removes local variables in a cluster.
ReorderPartitionedTransitionRelation(): Reorder partitioned transition relation.
ResetClusteredCofactoredRelationArray(): Reset the clusteredcofactoredrelationarray to the clusteredrelationarray.
SccSortListDecreasingWithArea(): Sorts connected components with area.
SccSortListDecreasingWithRatio(): Sorts connected components with aspect ratio.
SccSortListDecreasingWithVars(): Sorts connected components with the number of variables.
SccSortListIncreasingWithArea(): Sorts connected components with area.
SccSortListIncreasingWithRatio(): Sorts connected components with aspect ratio.
SccSortListIncreasingWithVars(): Sorts connected components with the number of variables.
SccSortRc(): Sorts rows or columns using connected component index.
SetupLazySifting(): Setups lazy sifting.
SetupMlp(): Setups MLP.
SignatureCompare(): Comparison function used by qsort.
SortCol(): Updates matrix information properly.
SortedListAlloc(): Allocates a list for sorting.
SortedListDelete(): Deletes a list from the sorting list.
SortedListFree(): Frees a list used for sorting.
SortedListInsert(): Inserts a list to the sorting list.
SortedListMove(): Moves a list in the sorting list.
SubstituteCacheResultRecur(): Recursive procedure of SubstituteCacheResult.
SubstituteCacheResult(): Substitutes a cache result.
TfmBuildRelationArray(): Builds relation array from function vector or bit relation.
TfmCheckImageValidity(): Checks the support of image.
TfmCreateBitRelationArray(): Creates the bit relations.
TfmCreateBitVector(): Creates function vector.
TfmInfoStructAlloc(): Allocates and initializes the info structure for transition function method.
TfmSetupPartialTransitionRelation(): Builds partial vector and relation array.
TrmEliminateDependVars(): Eliminates dependent variables from transition relation.
TrmGetOptions(): Gets the necessary options for computing the image and returns in the option structure.
TrmSignatureCompare(): Comparison function used by qsort.
UpdateDisapearingPsVarsInCluster(): Finds disappearing present state variables in a cluster.
UpdateDisapearingPsVars(): Finds disappearing present state variables in a row.
UpdateInfoArrays(): This function computes the set of variables which can be smoothed out once a particular cluster is chosen to be multiplied in the product.
UpdateNonappearingNsVars(): Finds non-appearing next state variables.
UpdateQuantificationSchedule(): Updates quantification schedule.
VarInfoStructAlloc(): Allocates and initializes memory for varInfoStruct.
VarInfoStructFree(): Frees the memory associated with varInfoStruct.
VarItemStructFree(): Frees the memory associated with VarItemStruct
VectorCompare(): Compares two vectors.
VectorHash(): Returns hash value of a vector.
VectorSortCompareWithConstraint(): Compares two vectors considering substitution.
VectorSortCompare(): Compares two vectors considering substitution.
VectorStHash(): Returns hash value of a vector for st_table.
WriteMatrix(): Writes a matrix to a file.
WriteOrder(): Writes variable order in coulumn of the matrix.
linearCheckRange(): compare function for checking range of cluster

Last updated on 20050519 00h50