/**CHeaderFile***************************************************************** FileName [imgInt.h] PackageName [img] Synopsis [Internal declarations for img package.] Description [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.] SeeAlso [fsm] Author [Rajeev Ranjan, Tom Shiple, Abelardo Pardo, In-Ho Moon] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software. IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] Revision [$Id: imgInt.h,v 1.76 2005/05/18 18:11:57 jinh Exp $] ******************************************************************************/ #ifndef _IMGINT #define _IMGINT #include "img.h" #include "mvf.h" #include "cmd.h" #include "part.h" #include "heap.h" #include /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ #define IMGDEFAULT_METHOD Img_Iwls95_c; /* Default image method */ #define IMG_PI_CLIP_DEPTH 0.4 /* partial image default clipping depth fraction for and-abstract */ #define IMG_PI_CLIP_DEPTH_FINAL 0.8 /* partial image default clipping depth fraction for and-abstract if the original clipping depth fails */ #define IMG_PI_SP_THRESHOLD 10000 /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ typedef struct ImgFunctionDataStruct ImgFunctionData_t; typedef mdd_t * (*ImgImageComputeProc) ARGS((ImgFunctionData_t *, Img_ImageInfo_t *, mdd_t *, mdd_t *, array_t *)); typedef void (*ImgImageFreeProc) ARGS((void *)); typedef void (*ImgImagePrintMethodParamsProc) ARGS((void *, FILE*)); typedef struct DomainCacheValueStruct ImgDomainCacheValue_t; typedef struct ImgPartialImageOptionStruct ImgPartialImageOption_t; typedef struct ImgTrmOptionStruct ImgTrmOption_t; typedef struct ImgTfmInfo_s ImgTfmInfo_t; typedef struct ImgTfmOption_s ImgTfmOption_t; typedef struct ImgComponent_s ImgComponent_t; typedef struct ImgCacheTable_s ImgCacheTable_t; typedef struct ImgCacheEntry_s ImgCacheEntry_t; typedef struct ImgCacheStKey_s ImgCacheStKey_t; typedef struct VarLifeStruct VarLife_t; typedef struct RelationStruct Relation_t; typedef struct ClusterStruct Cluster_t; typedef struct ConjunctStruct Conjunct_t; /**Enum************************************************************************ Synopsis [Partial image methods] ******************************************************************************/ typedef enum { Img_PIApprox_c, Img_PIClipping_c } Img_PartialImageMethod; /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [Functions and variables to compute images.] Description [This data structure provides all the information about the functions that are to be used to do image computations. For a thorough explanation of the fields of this structure, see the description of the function Img_ImageInfoInitialize. None of the data structures stored in this structure belong to the image package, therefore only a pointer to them is kept. A cube here is the product of bdd variables and createVarCubeFlag is the flag whether to create cubes and this is used for just efficiency.] SeeAlso [Img_ImageInfoInitialize] ******************************************************************************/ struct ImgFunctionDataStruct { graph_t *mddNetwork; /* graph representing the functions and dependencies */ array_t *roots; /* of char *; functions on which image is computed */ array_t *domainVars; /* array of mddIds of domain variables */ array_t *rangeVars; /* array of mddIds of range variables */ array_t *quantifyVars;/* array of mddIds of variables to be quantified */ mdd_t *domainCube; /* cube of domain bdd variables */ mdd_t *rangeCube; /* cube of range bdd variables */ mdd_t *quantifyCube; /* cube of input bdd variables */ array_t *domainBddVars; /* array of bdd_t of domain bdd variables */ array_t *rangeBddVars; /* array of bdd_t of range bdd variables */ array_t *quantifyBddVars; /* array of bdd_t of primary input bdd variables */ int *permutD2R; /* permutation for substitution from domain to range */ int *permutR2D; /* permutation for substitution from range to domain */ boolean createVarCubesFlag; boolean FAFWFlag; mdd_t *Winning; Ntk_Network_t *network; }; /**Struct********************************************************************** Synopsis [Information for method-specific image computation.] Description [Information for method-specific image computation. Along with user-specified state subsets, this structure contains all the information that an image computation method needs to perform the forward or backward image of a function vector. In particular, the methodData is used to allow the image computation to carry information from one image computation to the next (for example, when image computations are done from within a fixed point loop).] ******************************************************************************/ struct ImgImageInfoStruct { Img_MethodType methodType; /* method initialized to */ Img_DirectionType directionType; /* types of computation Fwd/Bwd allowed */ ImgFunctionData_t functionData; /* information about the functions */ void *methodData; /* method-dependent data structure */ ImgImageComputeProc imageComputeFwdProc;/* function to compute Fwd Image */ ImgImageComputeProc imageComputeBwdProc;/* function to compute Bwd Image */ ImgImageComputeProc imageComputeFwdWithDomainVarsProc; /* function to compute Fwd Image on Domain Vars*/ ImgImageComputeProc imageComputeBwdWithDomainVarsProc; /* function to compute Bwd Image on Domain Vars*/ ImgImageFreeProc imageFreeProc; /* function to free the method-dependent data structure */ ImgImagePrintMethodParamsProc imagePrintMethodParamsProc; boolean fwdTrMinimizedFlag; /* set when TR is minimized with DC */ boolean bwdTrMinimizedFlag; /* set when TR is minimized with DC */ int printMinimizeStatus; /* print status during minimizing * 0 : not print * 1 : print all info * 2 : print final info */ int verbosity; int useOptimizedRelationFlag; int linearComputeRange; Img_OptimizeType linearOptimize; void *savedRelation; /* copy of method-dependent data structure */ }; /**Struct********************************************************************** Synopsis [This structure contains the required options for partial image computation.] Description [This structure contains the required options for partial image computation. partialImageMethod can take the values PI_APPROX or PI_CLIPPING. partialImageThreshold is the threshold that triggers approximation. partialImageSize is the size that the approximation is required to reduce to. partialImageApproxMethod specified the approximation method to apply: BDD_APPROX_HB, BDD_APPROX_SP, BDD_APPROX_UA, BDD_APPROX_RUA, BDD_APPROX_BIASED_RUA BDD_APPROX_COMP. clippingDepthFrac is the only parameter required for PI_CLIPPING. nvars is the number of domain vars + range vars + quantify vars. The bias function is used in BDD_APPROX_BIASED_RUA. The qualityBias is also used for BDD_APPROX_BIASED_RUA. ] ******************************************************************************/ struct ImgPartialImageOptionStruct { int nvars; /* domain vars + range vars + quantify vars */ Img_PartialImageMethod partialImageMethod; int partialImageThreshold; /* pertains to PI_APPROX */ int partialImageSize; /* pertains to PI_APPROX */ bdd_approx_type_t partialImageApproxMethod; /* pertains to PI_APPROX */ double quality; /* pertains to PI_APPROX */ mdd_t *bias; /* bias function for BDD_APPROX_BIASED_RUA: pertains to PI_APPROX */ double qualityBias; /* quality for bias in BDD_APPROX_BIASED_RUA: pertains to PI_APPROX */ double clippingDepthFrac; /* pertains to PI_CLIPPING */ }; /**Struct********************************************************************** Synopsis [This structure contains the required options for filling in the data structure.] Description ["clusterSize" is the threshold value used to create clusters. "W1", "W2" etc are the weights used in the heuristic algorithms to order the cluster processing for early quantification. VerbosityLevel controls the amount of information printed during image computation.] ******************************************************************************/ struct ImgTrmOptionStruct { int clusterSize; int verbosity; int W1; int W2; /* Weights attached to various parameters. */ int W3; /* For details please refer to {1} */ int W4; int printDepMatrix; /* Print dependence matrix after building transition relation (default = 0) */ /* The following options are to read and write cluster file */ int readReorderCluster; /* Reorder clusters after reading (default = 0) */ char *readCluster; /* cluster file name to read */ char *writeCluster; /* cluster file name to write */ char *writeDepMatrix; /* file name to write dependence matrix*/ /* The following options starting with mlp is for MLP method */ int mlpMethod; /* 0 : Find singletons with iterative looping (default) 1 : Find singletons with sorted list by index 2 : Find singletons with sorted list by the number of 1's in active region */ int mlpCluster; /* 0 : sequential conjunctions 1 : affinity based tree clustering (default) */ int mlpClusterDynamic; /* Update affinity dynamically (default = 1) */ float mlpAffinityThreshold; /* Find best candidate when its affinity is at least equal or larger than this threshold (default = 0.0) */ int mlpClusterQuantifyVars; /* 0 : Find best candidate in clustering with the highest affinity, and in case of tie, use smaller number of quantify variables. (default) 1 : Find best candidate in clustering with the smallest number of quantify variables, and in case of tie, use bigger affinity 2 : In addition 1, update the number of quanity variables dynamically. */ int mlpClusterSortedList; /* Use sorted list for clustering (default = 1) */ int mlpInitialCluster; /* Try SSD based initial clustering (default = 0) */ int mlpCsFirst; /* Find column singletons first (default = 0) */ int mlpSkipRs; /* Skip finding row singletons (default = 0) */ int mlpSkipCs; /* Skip finding column singletons (default = 1) */ int mlpRowBased; /* Move rows instead of columns after singletons (default = 0) */ int mlpReorder; /* for image computation 0 : no reordering after clustering (default) 1 : reorder using MLP after clustering (inside) 2 : reorder using MLP after clustering (outside) 3 : reorder using IWLS95 after clustering */ int mlpPreReorder; /* for preimage 0 : no reordering after clustering (default) 1 : reorder using MLP after clustering (inside) 2 : reorder using MLP after clustering (outside) 3 : reorder using IWLS95 after clustering */ int mlpPostProcess; /* 0 : no postprocessing (default) 1 : do postprocessing after ordering 2 : do postprocessing after clustering or reordering 3 : both 1 and 2 */ int mlpDecomposeScc; /* Decompose dependence matrix with SCCs (default = 1) */ int mlpClusterScc; /* Cluster only inside each SCC (default = 1) */ int mlpSortScc; /* 0 : no sorting SCCs 1 : sort SCCs by increasing size (default) 2 : sort SCCs by decreasing size */ int mlpSortSccMode; /* 0 : with area of SCCs 1 : with the number of variable 2 : with ratio (nCols/nRows, default) */ int mlpClusterMerge; /* Try to merge with a cluster which is already done (default = 0) */ int mlpMultiway; /* Quanity out all smooth variables during MLP clustering (default = 0) */ int mlpLambdaMode; /* 0 : Use the number of final support variables (default) 1 : Use the number of initial support variables */ int mlpSortedRows; /* Use a sorted row list for finding best columns (default = 1) */ int mlpSortedCols; /* Use a sorted row list for finding best columns (default = 1) */ int mlpPreSwapStateVars; /* Swap present and next state vars for MLP in preimage computation. (default = 0) */ int mlpPrintMatrix; /* Print dependence matrix during MLP (default = 0) */ char *mlpWriteOrder; /* file name to write a variable order from MLP */ int mlpVerbosity; /* Verbosity for MLP (default = 0) */ int mlpDebug; /* Debug for MLP (default = 0) */ int linearFineGrainFlag; int linearGroupStateVariable; int linearOrderVariable; int linearIncludeCS; int linearIncludeNS; int linearQuantifyCS; int linearComputeRange; Img_OptimizeType linearOptimize; }; /**Struct********************************************************************** Synopsis [This structure stores the information needed for transition function method based on splitting and hybrid method combining splitting and conjunction.] Description [The hybrid method also refers to this structure. Some fields are common for image and preimage computations and some are only for image or preimage computation.] ******************************************************************************/ struct ImgTfmInfo_s { mdd_manager *manager; Img_MethodType method; array_t *vector; /* array of ImgComponent_t */ array_t *toCareSetArray; /* array of bdd_t */ int nComponents; int nVars; /* number of all variables in bdd manager */ int nRealVars; /* number of pi, ps, and ns */ ImgTfmOption_t *option; ImgCacheTable_t *imgCache; /* image cache */ ImgCacheTable_t *preCache; /* preimage cache */ ImgCacheTable_t *cache; /* points either imgCache or preCache */ int useConstraint; /* only for image computation */ int nRecursion; /* number of recursions(splits) */ int nRecursionB; /* for preimage */ int nLeaves; /* number of leaves during splitting */ int nLeavesB; /* for preimage */ int nTurns; /* number of cases that switch from splitting to conjunction */ int nTurnsB; /* for preimage */ float averageDepth; float averageDepthB; /* for preimage */ int maxDepth; int maxDepthB; /* for preimage */ int nDecomps; int topDecomp; int maxDecomp; float averageDecomp; int nFoundEssentials; float averageFoundEssential; float averageFoundEssentialDepth; int topFoundEssentialDepth; int *foundEssentials; int foundEssentialDepth; int lastFoundEssentialDepth; int nEmptySubImage; int nSplits; int nSplitsB; /* for preimage */ int nConjoins; int nConjoinsB; /* for preimage */ int nCubeSplits; ImgFunctionData_t *functionData; st_table *quantifyVarsTable; st_table *rangeVarsTable; st_table *intermediateVarsTable; array_t *intermediateBddVars; array_t *newQuantifyBddVars; int buildTR; boolean buildPartialTR; array_t *fwdClusteredRelationArray; /* array of bdd_t */ array_t *bwdClusteredRelationArray; /* array of bdd_t */ array_t *fwdArraySmoothVarBddArray; /* array of array_t */ array_t *bwdArraySmoothVarBddArray; /* array of array_t */ array_t *fwdSmoothVarCubeArray; /* array of bdd_t */ array_t *bwdSmoothVarCubeArray; /* array of bdd_t */ array_t *domainVarBddArray; /* array of bdd_t */ array_t *quantifyVarBddArray; /* array of bdd_t */ array_t *rangeVarBddArray; /* array of bdd_t */ ImgTrmOption_t *trmOption; array_t *partialBddVars; /* array of bdd_t */ char *partialVarFlag; array_t *fullVector; /* array of ImgComponent_t */ int eliminateDepend; /* 0 : do not perform this 1 : eliminates dependent variables from constraint and modifies function vector by composition at every image computation. 2 : once the number of eliminated variables becomes zero, do not perform. */ int nFoundDependVars; float averageFoundDependVars; int nPrevEliminatedFwd; int imageVerbosity; array_t *fwdSavedRelation; /* array of bdd_t */ array_t *bwdSavedRelation; /* array of bdd_t */ array_t *savedArraySmoothVarBddArray; /* array of array_t */ array_t *savedSmoothVarCubeArray; /* array of bdd_t */ int nImageComps; int nRangeComps; int maxIntermediateSize; long prevVectorBddSize; int prevVectorSize; float prevLambda; int prevTotal; int nIntermediateVars; int nonDeterministic; boolean imgKeepPiInTr; /* keep local primary input variables in building forward transition relation */ boolean preKeepPiInTr; /* keep local primary input variables in building backward transition relation */ boolean updatedFlag; /* tells whether the function vector or the transition relation changed from the originals during recursions */ mdd_t *debugCareSet; }; /**Struct********************************************************************** Synopsis [This structure contains all options for trnasition function method and also for hybrid method.] Description [Most fields are commonly used for both image and preimage computations, unless there are two separated fields. For some field, there are two default values: one for transition function method and the other is for hybrid method.] ******************************************************************************/ struct ImgTfmOption_s { int verbosity; int splitMethod; /* 0 : input splitting (default for tfm) 1 : output splitting 2 : mixed (input split + output split) 3 : hybrid (input split + transition relation) */ int inputSplit; /* 0 : support before splitting (default) 1 : support after splitting 2 : estimate bdd size after splitting 3 : top variable */ boolean piSplitFlag; /* If set, primary input variables can be chosen as a splitting variable, otherwise only state variables are chosen (default = TRUE) */ int rangeComp; /* 0 : do not convert to range computation 1 : convert image computation into range computation (default) 2 : use a threshold (rangeThreshold, default for hybrid) */ int rangeThreshold; /* When rangeComp = 2, if the size of resulting BDDs of applying constrain is larger than the size of original vector times this threshold, then perform image computation. (default = 10) */ int rangeTryThreshold; /* The number of consecutive fails allowed in converting image to range computation, then force to keep image computation (default = 2) */ boolean rangeCheckReorder; /* If set, force to reorder before checking whether to convert image to range computation (default = FALSE) */ int tieBreakMode; /* 0 : the closest variable to top (default) 1 : the smallest BDD size after splitting */ int outputSplit; /* 0 : smallest BDD size (default) 1 : largest BDD size 2 : top variable */ int turnDepth; /* recursion depth when to change to the other method. -1 means dynamic decision for hybrid method. (default = 5, -1 for hybrid) */ boolean findDecompVar; /* If it is set, before we find a best splitting variable, we try to find a variable which can decompose function vector after splitting. (default = FALSE) */ boolean sortVectorFlag; /* If set, sort vector for better caching (default = TRUE for tfm, FALSE for hybrid) */ boolean printStatistics; /* If set, print statistics for cache and recursions (default = FALSE) */ boolean printBddSize; /* If set, print BDD size of all intermediate products (default = FALSE) */ boolean splitCubeFunc; /* If set, find a cube function element, then apply output splitting in input splitting (default = FALSE) */ int findEssential; /* If set, find essential variabels from constraint and minimize function vector and relation. 0 : off (default) 1 : on 2 : on and off dynamically */ int printEssential; /* 0 : don't print (default) 1 : print only at end 2 : print at every image computation */ int maxEssentialDepth;/* (default = 5, but not an option) */ /* The followings are used for image cache */ int useCache; /* 0 : no cache (default for hybrid) 1 : cache (default for tfm) 2 : st cache (stores all intermediate results) */ boolean globalCache; /* If set, keeps only one global cache, otherwise one cache per each submachine. (default = TRUE) */ int maxChainLength; /* default = 2 */ int initCacheSize; /* default = 1001 */ int autoFlushCache; /* 0 : frees only when requested 1 : frees all cache contents at the end of one whole image computation (default) 2 : frees all cache contents before reordering */ boolean composeIntermediateVars; /* If set, compose all intermediate variables (default = TRUE) */ /* The following options are just for pre-image computation */ int preSplitMethod; /* 0 : input splitting (default) 1 : output splitting 2 : mixed 3 : substitution 4 : hybrid (input split + transition relation) */ int preInputSplit; /* 0 : support before splitting (default) 1 : support after splitting 2 : estimate bdd size after splitting 3 : top variable */ int preOutputSplit; /* 0 : smallest BDD size (default) 1 : largest BDD size 2 : top variable */ int preDcLeafMethod; /* 0 : substitution (default) 1 : constraint cofactoring 2 : hybrid */ boolean preMinimize; /* If set, everytime we split function vector in output split method for pre-image, we try to minimize all functions in the vector with respect to the chosen function. (default = FALSE) */ /* The following options are used for hybrid method */ int hybridMode; /* 0 : start with only transition function and build transition relation on demand 1 : start with both transition function and relation (default) 2 : start with only transition relation */ int trSplitMethod; /* This is just for hybridMode = 2. 0 : use support (default) 1 : use estimate cofactored BDD size */ boolean buildPartialTR; /* If set, build partial transition relations of the variables that are not supposed to be chosen as a splitting variable (default = FALSE). This is just for hybridMode = 2. */ int nPartialVars; /* default = 8 */ int partialMethod; /* 0 : use BDD size (default) 1 : use support */ boolean delayedSplit; /* If set, just keep cofactor variables and abstract variables as cubes until depth becomes threshold (default = FALSE) This is just for hybridMethod = 1. */ int splitMinDepth; /* minimum depth for checking whether split or not (default = 1) */ int splitMaxDepth; /* maximum depth for checking whether split or not (default = 5) */ int preSplitMinDepth; /* minimum depth for preimage (default = 1) */ int preSplitMaxDepth; /* maximum depth for preimage (default = 5) */ float lambdaThreshold; /* (default = 0.6) */ float preLambdaThreshold; /* (default = 0.6) */ float improveLambda; /* (default = 0.1) */ int improveVectorSize; /* (default = 3) */ float improveVectorBddSize; /* (default = 30.0) */ int conjoinVectorSize; /* (default = 10 ) */ int conjoinRelationSize; /* (default = 1) */ int conjoinRelationBddSize; /* (default = 200) */ int decideMode; /* 0 : use only lambda threshold 1 : use also checking special condition to conjoin 2 : use also checking improvement 3 : use both (default) */ boolean reorderWithFrom; /* reorder relation array with from to conjoin (default = TRUE) */ boolean preReorderWithFrom; /* reorder relation array with from to conjoin (default = FALSE) */ int lambdaMode; /* 0 : total lifetime (lambda, default) 1 : active lifetime (alpha) 2 : total lifetime with introduced variables (this is just for analysis) */ int preLambdaMode; /* 0 : total lifetime (lambda, default) 1 : active lifetime (alpha) 2 : total lifetime with introduced variables (this is just for analysis) */ boolean lambdaFromMlp; /* compute lambda from MLP directly, otherwise from quantification schedule (default = FALSE) */ boolean lambdaWithFrom; /* compute lambda with from (default = TRUE) */ boolean lambdaWithTr; /* compute lambda with transition relation when both function and relation exist (default = TRUE) */ boolean lambdaWithClustering; /* compute lambda with clustering (default = FALSE) */ boolean synchronizeTr; /* when hybrid mode is 1, wnenever function vector changes, rebuild transition relation from the changed function vector (default = FALSE) */ boolean imgKeepPiInTr; /* If set, we keep all primary input variables in transition relation, otherwise, we quantify out local primary input variables from the transition relation. This affects only to forward transition relation. (default = FALSE) */ boolean preKeepPiInTr; /* If set, we keep all primary input variables in transition relation, otherwise, we quantify out local primary input variables from the transition relation. This affects only to backward transition relation. Unlike imgKeepPiInTr, we keep all primary inputs, we also keep the primary input variables in preimages. If image cache is used, this is automatically set to TRUE. (default = FALSE) */ Img_MethodType trMethod; /* transition relation method (default = Img_Iwls95_c) */ boolean preCanonical; /* The following options are just for debugging and development */ boolean debug; boolean checkEquivalence; boolean printLambda; int writeSupportMatrix; /* 0 : none 1 : with only function vector 2 : with transition relation 3 : with function vector and relation */ boolean writeSupportMatrixWithYvars; boolean writeSupportMatrixAndStop; boolean writeSupportMatrixReverseRow; boolean writeSupportMatrixReverseCol; int supportFileCount; }; /**Struct********************************************************************** Synopsis [This structure stores all information of each next state function or a function of intermediate variable.] Description [If the field intermediate is 1, it is an intermediate variable, otherwise it is a next state function. This structure is used for tfm and hybrid methods.] ******************************************************************************/ struct ImgComponent_s { mdd_t *var; mdd_t *func; char *support; short id; unsigned int intermediate: 8; unsigned int flag: 8; }; /**Struct********************************************************************** Synopsis [This structure stores one intermediate result of image or preimage.] Description [The field constraint can be null when the result is of a range computation. This structure is used for tfm and hybrid methods.] ******************************************************************************/ struct ImgCacheEntry_s { array_t *vector; bdd_t *constraint; bdd_t *result; struct ImgCacheEntry_s *next; }; /**Struct********************************************************************** Synopsis [This structure stores all information of an image cache table.] Description [We keep image and preimage cache separately for higher hit ratio. This structure is used for tfm and hybrid methods.] ******************************************************************************/ struct ImgCacheTable_s { unsigned int nSlots; boolean preImgFlag; double lookups; double hits; double inserts; double entries; int maxChainLength; ImgCacheEntry_t **slot; st_table *stTable; int (*compareFunc)(array_t *, array_t *); int useConstraint; /* copy of ImgTfmInfo_t */ }; /**Struct********************************************************************** Synopsis [This structure is an entry for keeping all intermediate results using st_table.] Description [This structure is used as a key for st_table. This structure is used for tfm and hybrid methods.] ******************************************************************************/ struct ImgCacheStKey_s { array_t *vector; bdd_t *constraint; }; /**Struct********************************************************************** Synopsis [ ] Description [ ] ******************************************************************************/ struct VarLifeStruct { double index; int from; int to; int effFrom; int effTo; int id; int stateVar; int *relArr; int nSize; int flag; int dummy; int dummy1; }; /**Struct********************************************************************** Synopsis [ ] Description [ ] ******************************************************************************/ struct RelationStruct { mdd_manager *mgr; struct ConjunctStruct **conjunctArray; int nSize; struct ConjunctStruct ***connectedComponent; int nConnectedComponent; int *rangeVars; int nRange; int *domainVars; int nDomain; int *quantifyVars; int nQuantify; int *domain2range; int *range2domain; int *varType; bdd_t **constantCase; int nVar; int *varArrayMap; struct VarLifeStruct **varArray; int nVarArray; int nEffRange; int nEffDomain; int nEffQuantify; int nInitRange; int nInitDomain; int nInitQuantify; int bddLimit; struct ConjunctStruct **singletonArray; int nSingletonArray; struct ConjunctStruct **pseudoSingletonArray; int nPseudoSingletonArray; struct ConjunctStruct **nextStateArray; int nNextStateArray; struct ConjunctStruct **allQuantifiedArray; int nAllQuantifiedArray; struct ConjunctStruct **containedArray; int nContainedArray; int nTotalCluster; struct ClusterStruct **clusterArray; int nClusterArray; Heap_t *clusterHeap; int bModified; int bRefineVarArray; int includeCS; int includeNS; int quantifyCS; int computeRange; int verbosity; int dummy; }; /**Struct********************************************************************** Synopsis [ ] Description [ ] ******************************************************************************/ struct ClusterStruct { int from; int to; int nVar; int nDead; int nAffinity; int flag; }; /**Struct********************************************************************** Synopsis [ ] Description [ ] ******************************************************************************/ struct ConjunctStruct { int index; int nRange; int nDomain; int nQuantify; int nLive; int from; int to; bdd_t *relation; int *supList; int nSize; int bModified; int bClustered; struct ConjunctStruct **clusterArray; int nCluster; int bSingleton; long dummy; }; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ #define IMG_TF_MAX_INT 2000000000 #define IMG_TF_MAX_PRINT_DEPTH 100 /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN 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); EXTERN 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); EXTERN 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); EXTERN 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); EXTERN 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); EXTERN 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); EXTERN void ImgMlpWriteClusterFile(FILE *fout, mdd_manager *mddManager, array_t *relationArray, array_t *psVarBddArray, array_t *nsVarBddArray); EXTERN 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); EXTERN void * ImgImageInfoInitializeApprox(ImgFunctionData_t *functionData, Img_DirectionType directionType); EXTERN mdd_t * ImgImageInfoComputeFwdApprox(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet); EXTERN mdd_t * ImgImageInfoComputeFwdWithDomainVarsApprox(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet); EXTERN mdd_t * ImgImageInfoComputeBwdWithDomainVarsApprox(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet); EXTERN mdd_t * ImgImageInfoComputeBwdApprox(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet); EXTERN void ImgImageInfoPrintMethodParamsApprox(void *methodData, FILE *fp); EXTERN void ImgImageInfoFreeApprox(void *methodData); EXTERN mdd_t * ImgImageInfoComputeFwdFwdGrad(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet); EXTERN mdd_t * ImgImageInfoComputeFwdWithDomainVarsFwdGrad(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet); EXTERN void ImgImageInfoFreeFwdGradual(void *methodData); EXTERN void * ImgImageInfoInitializeGradual(void *methodData, ImgFunctionData_t * functionData, Img_DirectionType directionType); EXTERN void ImgImageInfoPrintMethodParamsFwdGrad(void *methodData, FILE *fp); EXTERN 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); EXTERN mdd_t * ImgImageByHybrid(ImgTfmInfo_t *info, array_t *vector, mdd_t *from); EXTERN mdd_t * ImgImageByHybridWithStaticSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube); EXTERN mdd_t * ImgPreImageByHybrid(ImgTfmInfo_t *info, array_t *vector, mdd_t *from); EXTERN mdd_t * ImgPreImageByHybridWithStaticSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube); EXTERN int ImgCheckEquivalence(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int preFlag); EXTERN int ImgCheckMatching(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray); EXTERN mdd_t* ImgMultiwayLinearAndSmooth(mdd_manager *mddManager, array_t *relationArray, array_t *smoothVarBddArray, array_t *introducedVarBddArray, Img_MethodType method, Img_DirectionType direction, ImgTrmOption_t *option); EXTERN 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); EXTERN mdd_t* ImgBddLinearAndSmooth(mdd_manager *mddManager, mdd_t *from, array_t *relationArray, array_t *arraySmoothVarBddArray, array_t *smoothVarCubeArray, int verbosity); EXTERN 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); EXTERN 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); EXTERN ImgTrmOption_t * ImgGetTrmOptions(void); EXTERN void ImgFreeTrmOptions(ImgTrmOption_t *option); EXTERN void * ImgImageInfoInitializeIwls95(void *methodData, ImgFunctionData_t *functionData, Img_DirectionType directionType, Img_MethodType method); EXTERN mdd_t * ImgImageInfoComputeFwdIwls95(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray); EXTERN mdd_t * ImgImageInfoComputeFwdWithDomainVarsIwls95(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray); EXTERN mdd_t * ImgImageInfoComputeBwdIwls95(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray); EXTERN mdd_t * ImgImageInfoComputeBwdWithDomainVarsIwls95(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray); EXTERN void ImgImageInfoFreeIwls95(void *methodData); EXTERN void ImgImageInfoPrintMethodParamsIwls95(void *methodData, FILE *fp); EXTERN st_table * ImgBddGetSupportIdTable(bdd_t *function); EXTERN boolean ImgImageWasPartialIwls95(void *methodData); EXTERN void ImgImageAllowPartialImageIwls95(void *methodData, boolean value); EXTERN void ImgRestoreTransitionRelationIwls95(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType); EXTERN void ImgDuplicateTransitionRelationIwls95(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType); EXTERN void ImgMinimizeTransitionRelationIwls95(void *methodData, ImgFunctionData_t *functionData, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, boolean reorderClusters, int printStatus); EXTERN void ImgAbstractTransitionRelationIwls95(Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, Img_DirectionType directionType, int printStatus); EXTERN 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); EXTERN array_t * ImgGetTransitionRelationIwls95(void *methodData, Img_DirectionType directionType); EXTERN void ImgUpdateTransitionRelationIwls95(void *methodData, array_t *relationArray, Img_DirectionType directionType); EXTERN void ImgReplaceIthPartitionedTransitionRelationIwls95(void *methodData, int i, mdd_t *relation, Img_DirectionType directionType); EXTERN void ImgImageFreeClusteredTransitionRelationIwls95(void *methodData, Img_DirectionType directionType); EXTERN void ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp(Img_ImageInfo_t *imageInfo, Img_DirectionType direction, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus); EXTERN void ImgPrintIntegerArray(array_t *idArray); EXTERN void ImgPrintPartition(graph_t *partition); EXTERN void ImgPrintPartitionedTransitionRelation(mdd_manager *mddManager, array_t *relationArray, array_t *arraySmoothVarBddArray); EXTERN mdd_t * ImgTrmEliminateDependVars(ImgFunctionData_t *functionData, array_t *relationArray, mdd_t *states, mdd_t **dependRelations, int *nDependVars); EXTERN void * ImgImageInfoInitializeMono(void *methodData, ImgFunctionData_t * functionData, Img_DirectionType directionType); EXTERN mdd_t * ImgImageInfoComputeFwdMono(ImgFunctionData_t * functionData, Img_ImageInfo_t * imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t * toCareSetArray); EXTERN mdd_t * ImgImageInfoComputeFwdWithDomainVarsMono(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray); EXTERN mdd_t * ImgImageInfoComputeBwdMono(ImgFunctionData_t * functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray); EXTERN mdd_t * ImgImageInfoComputeBwdWithDomainVarsMono(ImgFunctionData_t * functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray); EXTERN void ImgImageInfoFreeMono(void * methodData); EXTERN void ImgImageInfoPrintMethodParamsMono(void *methodData, FILE *fp); EXTERN void ImgRestoreTransitionRelationMono(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType); EXTERN void ImgDuplicateTransitionRelationMono(Img_ImageInfo_t *imageInfo); EXTERN void ImgMinimizeTransitionRelationMono(Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, int printStatus); EXTERN void ImgAddDontCareToTransitionRelationMono(Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, int printStatus); EXTERN void ImgAbstractTransitionRelationMono(Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, int printStatus); EXTERN 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); EXTERN void ImgImageConstrainAndClusterTransitionRelationMono(Img_ImageInfo_t *imageInfo, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus); EXTERN void * ImgImageInfoInitializeTfm(void *methodData, ImgFunctionData_t * functionData, Img_DirectionType directionType, Img_MethodType method); EXTERN mdd_t * ImgImageInfoComputeFwdTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray); EXTERN mdd_t * ImgImageInfoComputeFwdWithDomainVarsTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray); EXTERN mdd_t * ImgImageInfoComputeBwdTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray); EXTERN mdd_t * ImgImageInfoComputeBwdWithDomainVarsTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray); EXTERN void ImgImageInfoFreeTfm(void *methodData); EXTERN void ImgImageInfoPrintMethodParamsTfm(void *methodData, FILE *fp); EXTERN void ImgRestoreTransitionFunction(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType); EXTERN void ImgDuplicateTransitionFunction(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType); EXTERN void ImgMinimizeTransitionFunction(void *methodData, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, int printStatus); EXTERN void ImgAddDontCareToTransitionFunction(void *methodData, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, int printStatus); EXTERN void ImgAbstractTransitionFunction(Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, Img_DirectionType directionType, int printStatus); EXTERN 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); EXTERN array_t * ImgGetTransitionFunction(void *methodData, Img_DirectionType directionType); EXTERN void ImgUpdateTransitionFunction(void *methodData, array_t *vector, Img_DirectionType directionType); EXTERN void ImgReplaceIthTransitionFunction(void *methodData, int i, mdd_t *function, Img_DirectionType directionType); EXTERN ImgTfmOption_t * ImgTfmGetOptions(Img_MethodType method); EXTERN void ImgImageFreeClusteredTransitionRelationTfm(void *methodData, Img_DirectionType directionType); EXTERN void ImgImageConstrainAndClusterTransitionRelationTfm(Img_ImageInfo_t *imageInfo, Img_DirectionType direction, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus); EXTERN int ImgIsPartitionedTransitionRelationTfm(Img_ImageInfo_t *imageInfo); EXTERN bdd_t * ImgTfmPreImage(ImgTfmInfo_t *info, bdd_t *image); EXTERN void ImgCacheInitTable(ImgTfmInfo_t *info, int num_slot, int globalCache, boolean preImgFlag); EXTERN void ImgCacheDestroyTable(ImgCacheTable_t *table, int globalCache); EXTERN bdd_t * ImgCacheLookupTable(ImgTfmInfo_t *info, ImgCacheTable_t *table, array_t *delta, bdd_t *constraint); EXTERN void ImgCacheInsertTable(ImgCacheTable_t *table, array_t *delta, bdd_t *constraint, bdd_t *result); EXTERN void ImgFlushCache(ImgCacheTable_t *table); EXTERN void ImgPrintCacheStatistics(ImgCacheTable_t *cache); EXTERN mdd_t * ImgTfmImage(ImgTfmInfo_t *info, mdd_t *from); EXTERN mdd_t * ImgChooseTrSplitVar(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, int trSplitMethod, int piSplitFlag); EXTERN 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); EXTERN 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); EXTERN void ImgVectorFree(array_t *vector); EXTERN int ImgVectorFunctionSize(array_t *vector); EXTERN long ImgVectorBddSize(array_t *vector); EXTERN array_t * ImgVectorCopy(ImgTfmInfo_t *info, array_t *vector); EXTERN ImgComponent_t * ImgComponentAlloc(ImgTfmInfo_t *info); EXTERN ImgComponent_t * ImgComponentCopy(ImgTfmInfo_t *info, ImgComponent_t *comp); EXTERN void ImgComponentFree(ImgComponent_t *comp); EXTERN void ImgComponentGetSupport(ImgComponent_t *comp); EXTERN void ImgSupportCopy(ImgTfmInfo_t *info, char *dsupport, char *ssupport); EXTERN void ImgSupportClear(ImgTfmInfo_t *info, char *support); EXTERN void ImgSupportPrint(ImgTfmInfo_t *info, char *support); EXTERN int ImgSupportCount(ImgTfmInfo_t *info, char *support); EXTERN array_t * ImgGetConstrainedRelationArray(ImgTfmInfo_t *info, array_t *relationArray, mdd_t *constraint); EXTERN array_t * ImgGetCofactoredRelationArray(array_t *relationArray, mdd_t *func); EXTERN void ImgCofactorRelationArray(array_t *relationArray, mdd_t *func); EXTERN array_t * ImgGetAbstractedRelationArray(mdd_manager *manager, array_t *relationArray, mdd_t *cube); EXTERN void ImgAbstractRelationArray(mdd_manager *manager, array_t *relationArray, mdd_t *cube); EXTERN array_t * ImgGetCofactoredAbstractedRelationArray(mdd_manager *manager, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube); EXTERN array_t * ImgGetAbstractedCofactoredRelationArray(mdd_manager *manager, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube); EXTERN array_t * ImgGetConstrainedVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint); EXTERN array_t * ImgGetCofactoredVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *func); EXTERN void ImgCofactorVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *func); EXTERN mdd_t * ImgTfmEliminateDependVars(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, mdd_t *states, array_t **newVector, mdd_t **dependRelations); EXTERN int ImgExistConstIntermediateVar(array_t *vector); EXTERN mdd_t * ImgGetComposedFunction(array_t *vector); EXTERN ImgComponent_t * ImgGetLatchComponent(array_t *vector); EXTERN array_t * ImgComposeConstIntermediateVars(ImgTfmInfo_t *info, array_t *vector, mdd_t *constIntermediate, mdd_t **cofactorCube, mdd_t **abstractCube, mdd_t **and_, mdd_t **from); EXTERN int ImgCountBddSupports(mdd_t *func); EXTERN void ImgCheckConstConstrain(mdd_t *f1, mdd_t *f2, int *f21p, int *f21n); EXTERN int ImgConstConstrain(mdd_t *func, mdd_t *constraint); EXTERN void ImgPrintVectorDependency(ImgTfmInfo_t *info, array_t *vector, int verbosity); EXTERN float ImgPercentVectorDependency(ImgTfmInfo_t *info, array_t *vector, int length, int *nLongs); EXTERN void ImgWriteSupportMatrix(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, char *string); EXTERN array_t * ImgMinimizeImageArrayWithCareSetArray(array_t *imageArray, array_t *careSetArray, Img_MinimizeType minimizeMethod, boolean underapprox, boolean printInfo, Img_DirectionType dir); EXTERN void ImgMinimizeImageArrayWithCareSetArrayInSitu(array_t *imageArray, array_t *careSetArray, Img_MinimizeType minimizeMethod, boolean underapprox, boolean printInfo, Img_DirectionType dir); EXTERN mdd_t * ImgSubstitute(mdd_t *f, ImgFunctionData_t *functionData, Img_SubstituteDir dir); EXTERN array_t * ImgSubstituteArray(array_t *f_array, ImgFunctionData_t *functionData, Img_SubstituteDir dir); EXTERN void ImgPrintPartialImageOptions(void); EXTERN ImgPartialImageOption_t * ImgGetPartialImageOptions(void); EXTERN int ImgArrayBddArrayCheckValidity(array_t *arrayBddArray); EXTERN int ImgBddArrayCheckValidity(array_t *bddArray); EXTERN int ImgBddCheckValidity(bdd_t *bdd); EXTERN void ImgPrintVarIdTable(st_table *table); EXTERN int ImgCheckToCareSetArrayChanged(array_t *toCareSetArray1, array_t *toCareSetArray2); EXTERN Relation_t * ImgLinearRelationInit(mdd_manager *mgr, array_t *relationArray, array_t *domainBddVars, array_t *rangeBddVars, array_t *qunatifyBddVars, ImgTrmOption_t *option); EXTERN void ImgLinearRelationQuit(Relation_t *head); EXTERN void ImgLinearRefineRelation(Relation_t *head); EXTERN array_t * ImgLinearExtractRelationArrayT(Relation_t *head); EXTERN bdd_t ** ImgLinearExtractRelationArray(Relation_t *head); EXTERN array_t * ImgLinearMakeSmoothVarBdd(Relation_t *head, bdd_t **smoothCubeArr); EXTERN int * ImgLinearGetSupportBddId(mdd_manager *mgr, bdd_t *f, int *nSize); EXTERN void ImgLinearOptimizeInternalVariables(Relation_t *head); EXTERN 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 *)); EXTERN 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 *)); EXTERN 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); EXTERN int ImgLinearOptimizeAll(Relation_t *head, Img_OptimizeType optDir, int constantNSOpt); EXTERN void ImgResetMethodDataLinearComputeRange(void *methodData); EXTERN void ImgSetMethodDataLinearComputeRange(void *methodData); /**AutomaticEnd***************************************************************/ #endif /* _INT */