source: vis_dev/vis-2.3/src/img/imgInt.h @ 67

Last change on this file since 67 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 54.4 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [imgInt.h]
4
5  PackageName [img]
6
7  Synopsis    [Internal declarations for img package.]
8
9  Description [To add a new method, called "foo", follow these steps. 1)
10  describe the foo method in the Description field at the top of img.h. 2) Add
11  Img_Foo_c to the Img_MethodType enumerated type. 3) Create a file, imgFoo.c,
12  and define the following functions: ImgImageInfoInitializeFoo,
13  ImgImageInfoComputeFwdFoo, ImgImageInfoComputeBwdFoo,
14  ImgImageInfoFreeFoo. 4) In the function Img_ImageInfoInitialize, add the
15  case "foo" for the "image_method" flag, and add the case Img_Foo_c to the
16  switch for initialization.]
17 
18  SeeAlso     [fsm]
19
20  Author      [Rajeev Ranjan, Tom Shiple, Abelardo Pardo, In-Ho Moon]
21
22  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
23  All rights reserved.
24
25  Permission is hereby granted, without written agreement and without license
26  or royalty fees, to use, copy, modify, and distribute this software and its
27  documentation for any purpose, provided that the above copyright notice and
28  the following two paragraphs appear in all copies of this software.
29
30  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
31  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
32  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
33  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
34
35  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
36  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
37  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
38  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
39  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
40
41  Revision    [$Id: imgInt.h,v 1.76 2005/05/18 18:11:57 jinh Exp $]
42
43******************************************************************************/
44
45#ifndef _IMGINT
46#define _IMGINT
47
48#include "img.h"
49#include "mvf.h"
50#include "cmd.h"
51#include "part.h"
52#include "heap.h"
53#include <string.h>
54
55/*---------------------------------------------------------------------------*/
56/* Constant declarations                                                     */
57/*---------------------------------------------------------------------------*/
58
59#define IMGDEFAULT_METHOD Img_Iwls95_c; /* Default image method */
60#define IMG_PI_CLIP_DEPTH 0.4 /* partial image default clipping depth
61                                 fraction for and-abstract */
62#define IMG_PI_CLIP_DEPTH_FINAL 0.8 /* partial image default clipping depth
63                                       fraction for and-abstract if the
64                                    original clipping depth fails */
65#define IMG_PI_SP_THRESHOLD 10000
66
67/*---------------------------------------------------------------------------*/
68/* Type declarations                                                         */
69/*---------------------------------------------------------------------------*/
70typedef struct ImgFunctionDataStruct ImgFunctionData_t;
71typedef mdd_t * (*ImgImageComputeProc) ARGS((ImgFunctionData_t *,
72                                             Img_ImageInfo_t *,
73                                             mdd_t *, mdd_t *, array_t *));
74typedef void    (*ImgImageFreeProc)    ARGS((void *));
75typedef void    (*ImgImagePrintMethodParamsProc) ARGS((void *, FILE*));
76
77typedef struct DomainCacheValueStruct ImgDomainCacheValue_t;
78typedef struct ImgPartialImageOptionStruct ImgPartialImageOption_t;
79typedef struct ImgTrmOptionStruct ImgTrmOption_t;
80typedef struct ImgTfmInfo_s ImgTfmInfo_t;
81typedef struct ImgTfmOption_s ImgTfmOption_t;
82typedef struct ImgComponent_s ImgComponent_t;
83typedef struct ImgCacheTable_s ImgCacheTable_t;
84typedef struct ImgCacheEntry_s ImgCacheEntry_t;
85typedef struct ImgCacheStKey_s ImgCacheStKey_t;
86typedef struct VarLifeStruct VarLife_t;
87typedef struct RelationStruct Relation_t;
88typedef struct ClusterStruct Cluster_t;
89typedef struct ConjunctStruct Conjunct_t;
90
91
92
93/**Enum************************************************************************
94
95  Synopsis    [Partial image methods]
96
97******************************************************************************/
98typedef enum {
99  Img_PIApprox_c,
100  Img_PIClipping_c
101} Img_PartialImageMethod;
102
103/*---------------------------------------------------------------------------*/
104/* Structure declarations                                                     */
105/*---------------------------------------------------------------------------*/
106
107/**Struct**********************************************************************
108
109  Synopsis    [Functions and variables to compute images.]
110
111  Description [This data structure provides all the information about the
112  functions that are to be used to do image computations.  For a thorough
113  explanation of the fields of this structure, see the description of the
114  function Img_ImageInfoInitialize.  None of the data structures stored in
115  this structure belong to the image package, therefore only a pointer to them
116  is kept. A cube here is the product of bdd variables and
117  createVarCubeFlag is the flag whether to create cubes and this is used
118  for just efficiency.]
119
120  SeeAlso     [Img_ImageInfoInitialize]
121
122******************************************************************************/
123struct ImgFunctionDataStruct {
124  graph_t *mddNetwork;  /* graph representing the functions and dependencies */
125  array_t *roots;       /* of char *; functions on which image is computed */
126  array_t *domainVars;  /* array of mddIds of domain variables */
127  array_t *rangeVars;   /* array of mddIds of range variables */
128  array_t *quantifyVars;/* array of mddIds of variables to be quantified */
129  mdd_t   *domainCube;  /* cube of domain bdd variables */
130  mdd_t   *rangeCube;   /* cube of range bdd variables */
131  mdd_t   *quantifyCube; /* cube of input bdd variables */
132  array_t *domainBddVars;  /* array of bdd_t of domain bdd variables */
133  array_t *rangeBddVars;   /* array of bdd_t of range bdd variables */
134  array_t *quantifyBddVars; /* array of bdd_t of primary input bdd variables */
135  int     *permutD2R; /* permutation for substitution from domain to range */
136  int     *permutR2D; /* permutation for substitution from range to domain */
137  boolean createVarCubesFlag;
138  boolean FAFWFlag;
139  mdd_t   *Winning;
140  Ntk_Network_t *network;
141};
142
143
144/**Struct**********************************************************************
145
146  Synopsis    [Information for method-specific image computation.]
147
148  Description [Information for method-specific image computation.  Along with
149  user-specified state subsets, this structure contains all the information
150  that an image computation method needs to perform the forward or backward
151  image of a function vector.  In particular, the methodData is used to allow
152  the image computation to carry information from one image computation to the
153  next (for example, when image computations are done from within a fixed
154  point loop).]
155
156******************************************************************************/
157struct ImgImageInfoStruct {
158  Img_MethodType       methodType;    /* method initialized to */   
159  Img_DirectionType    directionType; /* types of computation Fwd/Bwd allowed */
160  ImgFunctionData_t    functionData;       /* information about the functions */
161  void                *methodData;         /* method-dependent data structure */
162  ImgImageComputeProc  imageComputeFwdProc;/* function to compute Fwd Image */
163  ImgImageComputeProc  imageComputeBwdProc;/* function to compute Bwd Image */
164  ImgImageComputeProc  imageComputeFwdWithDomainVarsProc;
165                        /* function to compute Fwd Image on Domain Vars*/
166  ImgImageComputeProc  imageComputeBwdWithDomainVarsProc;
167                        /* function to compute Bwd Image on Domain Vars*/
168  ImgImageFreeProc     imageFreeProc;      /* function to free the
169                                              method-dependent data structure */
170  ImgImagePrintMethodParamsProc   imagePrintMethodParamsProc;
171  boolean fwdTrMinimizedFlag;   /* set when TR is minimized with DC */
172  boolean bwdTrMinimizedFlag;   /* set when TR is minimized with DC */
173  int printMinimizeStatus;      /* print status during minimizing
174                                 * 0 : not print
175                                 * 1 : print all info
176                                 * 2 : print final info */
177  int verbosity;
178  int useOptimizedRelationFlag;
179  int linearComputeRange;
180  Img_OptimizeType linearOptimize;
181  void *savedRelation; /* copy of method-dependent data structure */
182};
183
184
185/**Struct**********************************************************************
186
187  Synopsis    [This structure contains the required options for partial
188               image computation.]
189
190  Description [This structure contains the required options for
191  partial image computation. partialImageMethod can take the values
192  PI_APPROX or PI_CLIPPING. partialImageThreshold is the threshold
193  that triggers approximation. partialImageSize is the size that the
194  approximation is required to reduce to. partialImageApproxMethod
195  specified the approximation method to apply: BDD_APPROX_HB,
196  BDD_APPROX_SP, BDD_APPROX_UA, BDD_APPROX_RUA, BDD_APPROX_BIASED_RUA
197  BDD_APPROX_COMP. clippingDepthFrac is the only parameter required
198  for PI_CLIPPING. nvars is the number of domain vars + range vars +
199  quantify vars. The bias function is used in
200  BDD_APPROX_BIASED_RUA. The qualityBias is also used for
201  BDD_APPROX_BIASED_RUA. ]
202
203******************************************************************************/
204struct ImgPartialImageOptionStruct {
205  int nvars; /* domain vars + range vars + quantify vars */
206  Img_PartialImageMethod partialImageMethod;
207  int partialImageThreshold; /* pertains to PI_APPROX */
208  int partialImageSize; /* pertains to PI_APPROX */
209  bdd_approx_type_t partialImageApproxMethod; /* pertains to PI_APPROX */
210  double quality; /* pertains to PI_APPROX */
211  mdd_t *bias; /* bias function for BDD_APPROX_BIASED_RUA: pertains to PI_APPROX */
212  double qualityBias; /* quality for bias in BDD_APPROX_BIASED_RUA:
213                         pertains to PI_APPROX */
214  double clippingDepthFrac; /* pertains to PI_CLIPPING */
215};
216
217
218/**Struct**********************************************************************
219
220  Synopsis    [This structure contains the required options for filling in
221               the data structure.]
222
223  Description ["clusterSize" is the threshold value used to
224               create clusters. "W1", "W2" etc are the weights used in the
225               heuristic algorithms to order the cluster processing for early
226               quantification. VerbosityLevel  controls the amount of
227               information printed during image computation.]
228
229******************************************************************************/
230struct ImgTrmOptionStruct {
231  int clusterSize;
232  int verbosity;
233  int W1;
234  int W2; /* Weights attached to various parameters. */
235  int W3; /* For details please refer to {1} */
236  int W4;
237  int printDepMatrix; /* Print dependence matrix after building transition
238                         relation (default = 0)
239                      */
240  /* The following options are to read and write cluster file */
241  int readReorderCluster; /* Reorder clusters after reading (default = 0) */
242  char *readCluster; /* cluster file name to read */
243  char *writeCluster; /* cluster file name to write */
244  char *writeDepMatrix; /* file name to write dependence matrix*/
245  /* The following options starting with mlp is for MLP method */
246  int mlpMethod; /* 0 : Find singletons with iterative looping (default)
247                    1 : Find singletons with sorted list by index
248                    2 : Find singletons with sorted list by the number of 1's
249                        in active region
250                 */
251  int mlpCluster; /* 0 : sequential conjunctions
252                     1 : affinity based tree clustering (default)
253                  */
254  int mlpClusterDynamic; /* Update affinity dynamically (default = 1) */
255  float mlpAffinityThreshold; /* Find best candidate when its affinity is
256                                 at least equal or larger than this threshold
257                                 (default = 0.0)
258                              */
259  int mlpClusterQuantifyVars; /* 0 : Find best candidate in clustering with the
260                                     highest affinity, and in case of tie,
261                                     use smaller number of quantify variables.
262                                     (default)
263                                 1 : Find best candidate in clustering with the
264                                     smallest number of quantify variables, and
265                                     in case of tie, use bigger affinity
266                                 2 : In addition 1, update the number of quanity
267                                     variables dynamically.
268                              */
269  int mlpClusterSortedList; /* Use sorted list for clustering (default = 1) */
270  int mlpInitialCluster; /* Try SSD based initial clustering (default = 0) */
271  int mlpCsFirst; /* Find column singletons first (default = 0) */
272  int mlpSkipRs; /* Skip finding row singletons (default = 0) */
273  int mlpSkipCs; /* Skip finding column singletons (default = 1) */
274  int mlpRowBased; /* Move rows instead of columns after singletons
275                      (default = 0)
276                   */
277  int mlpReorder; /* for image computation
278                     0 : no reordering after clustering (default)
279                     1 : reorder using MLP after clustering (inside)
280                     2 : reorder using MLP after clustering (outside)
281                     3 : reorder using IWLS95 after clustering
282                  */
283  int mlpPreReorder; /* for preimage
284                        0 : no reordering after clustering (default)
285                        1 : reorder using MLP after clustering (inside)
286                        2 : reorder using MLP after clustering (outside)
287                        3 : reorder using IWLS95 after clustering
288                     */
289  int mlpPostProcess; /* 0 : no postprocessing (default)
290                         1 : do postprocessing after ordering
291                         2 : do postprocessing after clustering or reordering
292                         3 : both 1 and 2
293                      */
294  int mlpDecomposeScc; /* Decompose dependence matrix with SCCs (default = 1) */
295  int mlpClusterScc; /* Cluster only inside each SCC (default = 1) */
296  int mlpSortScc; /* 0 : no sorting SCCs
297                     1 : sort SCCs by increasing size (default)
298                     2 : sort SCCs by decreasing size
299                  */
300  int mlpSortSccMode; /* 0 : with area of SCCs
301                         1 : with the number of variable
302                         2 : with ratio (nCols/nRows, default)
303                      */
304  int mlpClusterMerge; /* Try to merge with a cluster which is already done
305                          (default = 0)
306                        */
307  int mlpMultiway; /* Quanity out all smooth variables during MLP clustering
308                      (default = 0)
309                   */
310  int mlpLambdaMode; /* 0 : Use the number of final support variables (default)
311                        1 : Use the number of initial support variables
312                     */
313  int mlpSortedRows; /* Use a sorted row list for finding best columns
314                        (default = 1)
315                     */
316  int mlpSortedCols; /* Use a sorted row list for finding best columns
317                        (default = 1)
318                     */
319  int mlpPreSwapStateVars; /* Swap present and next state vars for MLP
320                              in preimage computation. (default = 0)
321                           */
322  int mlpPrintMatrix; /* Print dependence matrix during MLP (default = 0) */
323  char *mlpWriteOrder; /* file name to write a variable order from MLP */
324  int mlpVerbosity; /* Verbosity for MLP (default = 0) */
325  int mlpDebug; /* Debug for MLP (default = 0) */
326  int linearFineGrainFlag;
327  int linearGroupStateVariable;
328  int linearOrderVariable;
329  int linearIncludeCS;
330  int linearIncludeNS;
331  int linearQuantifyCS;
332  int linearComputeRange;
333  Img_OptimizeType linearOptimize;
334};
335
336
337/**Struct**********************************************************************
338
339  Synopsis    [This structure stores the information needed for transition
340  function method based on splitting and hybrid method combining splitting
341  and conjunction.]
342
343  Description [The hybrid method also refers to this structure. Some fields
344  are common for image and preimage computations and some are only for
345  image or preimage computation.]
346
347******************************************************************************/
348struct ImgTfmInfo_s {
349  mdd_manager           *manager;
350  Img_MethodType        method;
351  array_t               *vector; /* array of ImgComponent_t */
352  array_t               *toCareSetArray; /* array of bdd_t */
353  int                   nComponents;
354  int                   nVars; /* number of all variables in bdd manager */
355  int                   nRealVars; /* number of pi, ps, and ns */
356  ImgTfmOption_t        *option;
357  ImgCacheTable_t       *imgCache; /* image cache */
358  ImgCacheTable_t       *preCache; /* preimage cache */
359  ImgCacheTable_t       *cache; /* points either imgCache or preCache */
360  int                   useConstraint;  /* only for image computation */
361  int                   nRecursion; /* number of recursions(splits) */
362  int                   nRecursionB; /* for preimage */
363  int                   nLeaves; /* number of leaves during splitting */
364  int                   nLeavesB; /* for preimage */
365  int                   nTurns; /* number of cases that switch from
366                                   splitting to conjunction */
367  int                   nTurnsB; /* for preimage */
368  float                 averageDepth;
369  float                 averageDepthB; /* for preimage */
370  int                   maxDepth;
371  int                   maxDepthB; /* for preimage */
372  int                   nDecomps;
373  int                   topDecomp;
374  int                   maxDecomp;
375  float                 averageDecomp;
376  int                   nFoundEssentials;
377  float                 averageFoundEssential;
378  float                 averageFoundEssentialDepth;
379  int                   topFoundEssentialDepth;
380  int                   *foundEssentials;
381  int                   foundEssentialDepth;
382  int                   lastFoundEssentialDepth;
383  int                   nEmptySubImage;
384  int                   nSplits;
385  int                   nSplitsB; /* for preimage */
386  int                   nConjoins;
387  int                   nConjoinsB; /* for preimage */
388  int                   nCubeSplits;
389  ImgFunctionData_t     *functionData;
390  st_table              *quantifyVarsTable;
391  st_table              *rangeVarsTable;
392  st_table              *intermediateVarsTable;
393  array_t               *intermediateBddVars;
394  array_t               *newQuantifyBddVars;
395  int                   buildTR;
396  boolean               buildPartialTR;
397  array_t               *fwdClusteredRelationArray; /* array of bdd_t */
398  array_t               *bwdClusteredRelationArray; /* array of bdd_t */
399  array_t               *fwdArraySmoothVarBddArray; /* array of array_t */
400  array_t               *bwdArraySmoothVarBddArray; /* array of array_t */
401  array_t               *fwdSmoothVarCubeArray; /* array of bdd_t */
402  array_t               *bwdSmoothVarCubeArray; /* array of bdd_t */
403  array_t               *domainVarBddArray; /* array of bdd_t */
404  array_t               *quantifyVarBddArray; /* array of bdd_t */
405  array_t               *rangeVarBddArray; /* array of bdd_t */
406  ImgTrmOption_t        *trmOption;
407  array_t               *partialBddVars; /* array of bdd_t */
408  char                  *partialVarFlag;
409  array_t               *fullVector; /* array of ImgComponent_t */
410  int                   eliminateDepend;
411                        /* 0 : do not perform this
412                           1 : eliminates dependent variables from
413                                constraint and modifies function vector by
414                                composition at every image computation.
415                           2 : once the number of eliminated variables
416                                becomes zero, do not perform.
417                        */
418  int                   nFoundDependVars;
419  float                 averageFoundDependVars;
420  int                   nPrevEliminatedFwd;
421  int                   imageVerbosity;
422  array_t               *fwdSavedRelation; /* array of bdd_t */
423  array_t               *bwdSavedRelation; /* array of bdd_t */
424  array_t               *savedArraySmoothVarBddArray; /* array of array_t */
425  array_t               *savedSmoothVarCubeArray; /* array of bdd_t */
426  int                   nImageComps;
427  int                   nRangeComps;
428  int                   maxIntermediateSize;
429  long                  prevVectorBddSize;
430  int                   prevVectorSize;
431  float                 prevLambda;
432  int                   prevTotal;
433  int                   nIntermediateVars;
434  int                   nonDeterministic;
435  boolean               imgKeepPiInTr; /* keep local primary input variables
436                                          in building forward transition
437                                          relation */
438  boolean               preKeepPiInTr; /* keep local primary input variables
439                                          in building backward transition
440                                          relation */
441  boolean               updatedFlag; /* tells whether the function vector or
442                                        the transition relation changed
443                                        from the originals during recursions */
444  mdd_t                 *debugCareSet;
445};
446
447
448/**Struct**********************************************************************
449
450  Synopsis    [This structure contains all options for trnasition function
451  method and also for hybrid method.]
452
453  Description [Most fields are commonly used for both image and preimage
454  computations, unless there are two separated fields. For some field,
455  there are two default values: one for transition function method and
456  the other is for hybrid method.]
457
458******************************************************************************/
459struct ImgTfmOption_s {
460  int verbosity;
461  int splitMethod;      /* 0 : input splitting (default for tfm)
462                           1 : output splitting
463                           2 : mixed (input split + output split)
464                           3 : hybrid (input split + transition relation)
465                        */
466  int inputSplit;       /* 0 : support before splitting (default)
467                           1 : support after splitting
468                           2 : estimate bdd size after splitting
469                           3 : top variable
470                        */
471  boolean piSplitFlag;  /* If set, primary input variables can be chosen
472                           as a splitting variable, otherwise only
473                           state variables are chosen (default = TRUE)
474                        */
475  int rangeComp;        /* 0 : do not convert to range computation
476                           1 : convert image computation into
477                               range computation (default)
478                           2 : use a threshold (rangeThreshold,
479                                default for hybrid)
480                        */
481  int rangeThreshold;   /* When rangeComp = 2, if the size of resulting BDDs
482                           of applying constrain is larger than the size of
483                           original vector times this threshold, then perform
484                           image computation. (default = 10)
485                        */
486  int rangeTryThreshold; /* The number of consecutive fails allowed in
487                            converting image to range computation,
488                            then force to keep image computation (default = 2)
489                         */
490  boolean rangeCheckReorder; /* If set, force to reorder before checking whether
491                                to convert image to range computation
492                                (default = FALSE)
493                             */
494  int tieBreakMode;     /* 0 : the closest variable to top (default)
495                           1 : the smallest BDD size after splitting
496                        */
497  int outputSplit;      /* 0 : smallest BDD size (default)
498                           1 : largest BDD size
499                           2 : top variable
500                        */
501  int turnDepth;        /* recursion depth when to change to the other method.
502                           -1 means dynamic decision for hybrid method.
503                           (default = 5, -1 for hybrid)
504                        */
505  boolean findDecompVar; /* If it is set, before we find a best splitting
506                            variable, we try to find a variable which can
507                            decompose function vector after splitting.
508                            (default = FALSE)
509                         */
510  boolean sortVectorFlag; /* If set, sort vector for better caching
511                             (default = TRUE for tfm, FALSE for hybrid)
512                          */
513  boolean printStatistics; /* If set, print statistics for cache and
514                                recursions (default = FALSE)
515                           */
516  boolean printBddSize; /* If set, print BDD size of all intermediate
517                           products (default = FALSE)
518                        */
519  boolean splitCubeFunc; /* If set, find a cube function element,
520                            then apply output splitting in input splitting
521                            (default = FALSE)
522                         */
523  int findEssential;    /* If set, find essential variabels from constraint
524                           and minimize function vector and relation.
525                           0 : off (default)
526                           1 : on
527                           2 : on and off dynamically
528                        */
529  int printEssential;   /* 0 : don't print (default)
530                           1 : print only at end
531                           2 : print at every image computation
532                        */
533  int maxEssentialDepth;/* (default = 5, but not an option) */
534
535  /* The followings are used for image cache */
536  int useCache;         /* 0 : no cache (default for hybrid)
537                           1 : cache (default for tfm)
538                           2 : st cache (stores all intermediate results)
539                        */
540  boolean globalCache;  /* If set, keeps only one global cache,
541                           otherwise one cache per each submachine.
542                           (default = TRUE)
543                        */
544  int maxChainLength;   /* default = 2 */
545  int initCacheSize;    /* default = 1001 */
546  int autoFlushCache;   /* 0 : frees only when requested
547                           1 : frees all cache contents at the end of one
548                                whole image computation (default)
549                           2 : frees all cache contents before reordering
550                        */
551  boolean composeIntermediateVars;
552                        /* If set, compose all intermediate variables
553                           (default = TRUE)
554                        */
555
556  /* The following options are just for pre-image computation */
557  int preSplitMethod;   /* 0 : input splitting (default)
558                           1 : output splitting
559                           2 : mixed
560                           3 : substitution
561                           4 : hybrid (input split + transition relation)
562                        */
563  int preInputSplit;    /* 0 : support before splitting (default)
564                           1 : support after splitting
565                           2 : estimate bdd size after splitting
566                           3 : top variable
567                        */
568  int preOutputSplit;   /* 0 : smallest BDD size (default)
569                           1 : largest BDD size
570                           2 : top variable
571                        */
572  int preDcLeafMethod;  /* 0 : substitution (default)
573                           1 : constraint cofactoring
574                           2 : hybrid
575                        */
576  boolean preMinimize;  /* If set, everytime we split function vector
577                           in output split method for pre-image,
578                           we try to minimize all functions in the vector
579                           with respect to the chosen function.
580                           (default = FALSE)
581                        */
582
583  /* The following options are used for hybrid method */
584  int hybridMode;       /* 0 : start with only transition function and
585                                build transition relation on demand
586                           1 : start with both transition function and
587                                relation (default)
588                           2 : start with only transition relation
589                        */
590  int trSplitMethod;    /* This is just for hybridMode = 2.
591                           0 : use support (default)
592                           1 : use estimate cofactored BDD size
593                        */
594  boolean buildPartialTR; /* If set, build partial transition relations of
595                            the variables that are not supposed to be
596                            chosen as a splitting variable (default = FALSE).
597                            This is just for hybridMode = 2.
598                          */
599  int nPartialVars;     /* default = 8 */
600  int partialMethod;    /* 0 : use BDD size (default)
601                           1 : use support
602                        */
603  boolean delayedSplit; /* If set, just keep cofactor variables and abstract
604                           variables as cubes until depth becomes threshold
605                           (default = FALSE)
606                           This is just for hybridMethod = 1.
607                        */
608  int splitMinDepth;    /* minimum depth for checking whether split or not
609                           (default = 1)
610                        */
611  int splitMaxDepth;    /* maximum depth for checking whether split or not
612                           (default = 5)
613                        */
614  int preSplitMinDepth; /* minimum depth for preimage (default = 1) */
615  int preSplitMaxDepth; /* maximum depth for preimage (default = 5) */
616  float lambdaThreshold; /* (default = 0.6) */
617  float preLambdaThreshold; /* (default = 0.6) */
618  float improveLambda; /* (default = 0.1) */
619  int improveVectorSize; /* (default = 3) */
620  float improveVectorBddSize; /* (default = 30.0) */
621  int conjoinVectorSize; /* (default = 10 ) */
622  int conjoinRelationSize; /* (default = 1) */
623  int conjoinRelationBddSize; /* (default = 200) */
624  int decideMode; /* 0 : use only lambda threshold
625                     1 : use also checking special condition to conjoin
626                     2 : use also checking improvement
627                     3 : use both (default)
628                 */
629  boolean reorderWithFrom; /* reorder relation array with from to conjoin
630                              (default = TRUE)
631                           */
632  boolean preReorderWithFrom; /* reorder relation array with from to conjoin
633                                 (default = FALSE)
634                              */
635  int lambdaMode; /* 0 : total lifetime (lambda, default)
636                     1 : active lifetime (alpha)
637                     2 : total lifetime with introduced variables
638                         (this is just for analysis)
639                  */
640  int preLambdaMode; /* 0 : total lifetime (lambda, default)
641                        1 : active lifetime (alpha)
642                        2 : total lifetime with introduced variables
643                            (this is just for analysis)
644                     */
645  boolean lambdaFromMlp; /* compute lambda from MLP directly, otherwise from
646                            quantification schedule (default = FALSE)
647                         */
648  boolean lambdaWithFrom; /* compute lambda with from (default = TRUE) */
649  boolean lambdaWithTr; /* compute lambda with transition relation
650                           when both function and relation exist
651                           (default = TRUE)
652                        */
653  boolean lambdaWithClustering; /* compute lambda with clustering
654                                   (default = FALSE)
655                                */
656  boolean synchronizeTr; /* when hybrid mode is 1, wnenever function vector
657                            changes, rebuild transition relation from the
658                            changed function vector
659                            (default = FALSE)
660                         */
661  boolean imgKeepPiInTr; /* If set, we keep all primary input variables in
662                            transition relation, otherwise, we quantify out
663                            local primary input variables from the
664                            transition relation. This affects only to
665                            forward transition relation.
666                            (default = FALSE)
667                         */
668  boolean preKeepPiInTr; /* If set, we keep all primary input variables in
669                            transition relation, otherwise, we quantify out
670                            local primary input variables from the
671                            transition relation. This affects only to
672                            backward transition relation. Unlike imgKeepPiInTr,
673                            we keep all primary inputs, we also keep the
674                            primary input variables in preimages. If image
675                            cache is used, this is automatically set to TRUE.
676                            (default = FALSE)
677                         */
678  Img_MethodType trMethod; /* transition relation method
679                              (default = Img_Iwls95_c)
680                           */
681  boolean preCanonical;
682
683  /* The following options are just for debugging and development */
684  boolean debug;
685  boolean checkEquivalence;
686  boolean printLambda;
687  int writeSupportMatrix; /* 0 : none
688                             1 : with only function vector
689                             2 : with transition relation
690                             3 : with function vector and relation
691                          */
692  boolean writeSupportMatrixWithYvars;
693  boolean writeSupportMatrixAndStop;
694  boolean writeSupportMatrixReverseRow;
695  boolean writeSupportMatrixReverseCol;
696  int supportFileCount;
697};
698
699
700/**Struct**********************************************************************
701
702  Synopsis    [This structure stores all information of each next state
703  function or a function of intermediate variable.]
704
705  Description [If the field intermediate is 1, it is an intermediate
706  variable, otherwise it is a next state function. This structure is used
707  for tfm and hybrid methods.]
708
709******************************************************************************/
710struct ImgComponent_s {
711  mdd_t         *var;
712  mdd_t         *func;
713  char          *support;
714  short         id;
715  unsigned int  intermediate: 8;
716  unsigned int  flag: 8;
717};
718
719
720/**Struct**********************************************************************
721
722  Synopsis    [This structure stores one intermediate result of image or
723  preimage.]
724
725  Description [The field constraint can be null when the result is of a
726  range computation. This structure is used for tfm and hybrid methods.]
727
728******************************************************************************/
729struct ImgCacheEntry_s {
730  array_t                       *vector;
731  bdd_t                         *constraint;
732  bdd_t                         *result;
733  struct ImgCacheEntry_s        *next;
734};
735
736
737/**Struct**********************************************************************
738
739  Synopsis    [This structure stores all information of an image cache table.]
740
741  Description [We keep image and preimage cache separately for higher hit
742  ratio. This structure is used for tfm and hybrid methods.]
743
744******************************************************************************/
745struct ImgCacheTable_s {
746  unsigned int          nSlots;
747  boolean               preImgFlag;
748  double                lookups;
749  double                hits;
750  double                inserts;
751  double                entries;
752  int                   maxChainLength;
753  ImgCacheEntry_t       **slot;
754  st_table              *stTable;
755  int                   (*compareFunc)(array_t *, array_t *);
756  int                   useConstraint;  /* copy of ImgTfmInfo_t */
757};
758
759
760/**Struct**********************************************************************
761
762  Synopsis    [This structure is an entry for keeping all intermediate results
763  using st_table.]
764
765  Description [This structure is used as a key for st_table. This structure
766  is used for tfm and hybrid methods.]
767
768******************************************************************************/
769struct ImgCacheStKey_s {
770  array_t       *vector;
771  bdd_t         *constraint;
772};
773
774/**Struct**********************************************************************
775 
776  Synopsis    [ ]
777
778  Description [ ]
779
780******************************************************************************/
781struct VarLifeStruct {
782    double index;
783    int from;
784    int to;
785    int effFrom;
786    int effTo;
787    int id;
788    int stateVar;
789    int *relArr;
790    int nSize;
791    int flag;
792    int dummy;
793    int dummy1;
794};
795
796/**Struct**********************************************************************
797 
798  Synopsis    [ ]
799
800  Description [ ]
801
802******************************************************************************/
803struct RelationStruct {
804    mdd_manager *mgr;
805    struct ConjunctStruct  **conjunctArray;
806    int nSize;
807    struct ConjunctStruct  ***connectedComponent;
808    int nConnectedComponent;
809    int *rangeVars;
810    int nRange;
811    int *domainVars;
812    int nDomain;
813    int *quantifyVars;
814    int nQuantify;
815    int *domain2range;
816    int *range2domain;
817    int *varType;
818    bdd_t **constantCase;
819    int nVar;
820    int *varArrayMap;
821    struct VarLifeStruct **varArray;
822    int nVarArray;
823    int nEffRange;
824    int nEffDomain;
825    int nEffQuantify;
826    int nInitRange;
827    int nInitDomain;
828    int nInitQuantify;
829
830    int bddLimit;
831
832    struct ConjunctStruct  **singletonArray;
833    int nSingletonArray;
834    struct ConjunctStruct  **pseudoSingletonArray;
835    int nPseudoSingletonArray;
836    struct ConjunctStruct  **nextStateArray;
837    int nNextStateArray;
838    struct ConjunctStruct  **allQuantifiedArray;
839    int nAllQuantifiedArray;
840    struct ConjunctStruct  **containedArray;
841    int nContainedArray;
842    int nTotalCluster;
843    struct ClusterStruct **clusterArray;
844    int nClusterArray;
845    Heap_t *clusterHeap;
846    int bModified;
847    int bRefineVarArray;
848    int includeCS;
849    int includeNS;
850    int quantifyCS;
851    int computeRange;
852
853    int verbosity;
854    int dummy;
855};
856
857/**Struct**********************************************************************
858 
859  Synopsis    [ ]
860
861  Description [ ]
862
863******************************************************************************/
864struct ClusterStruct {
865    int from;
866    int to;
867    int nVar;
868    int nDead;
869    int nAffinity;
870    int flag;
871};
872
873/**Struct**********************************************************************
874 
875  Synopsis    [ ]
876
877  Description [ ]
878
879******************************************************************************/
880struct ConjunctStruct {
881    int index;
882    int nRange;
883    int nDomain;
884    int nQuantify;
885    int nLive;
886    int from;
887    int to;
888    bdd_t *relation;
889    int *supList;
890    int nSize;
891    int bModified;
892    int bClustered;
893    struct ConjunctStruct **clusterArray;
894    int nCluster;
895    int bSingleton;
896    long dummy;
897};
898
899
900/*---------------------------------------------------------------------------*/
901/* Variable declarations                                                     */
902/*---------------------------------------------------------------------------*/
903
904
905/*---------------------------------------------------------------------------*/
906/* Macro declarations                                                        */
907/*---------------------------------------------------------------------------*/
908
909#define IMG_TF_MAX_INT          2000000000
910#define IMG_TF_MAX_PRINT_DEPTH  100
911
912/**AutomaticStart*************************************************************/
913
914/*---------------------------------------------------------------------------*/
915/* Function prototypes                                                       */
916/*---------------------------------------------------------------------------*/
917
918EXTERN 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);
919EXTERN 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);
920EXTERN 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);
921EXTERN 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);
922EXTERN 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);
923EXTERN 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);
924EXTERN void ImgMlpWriteClusterFile(FILE *fout, mdd_manager *mddManager, array_t *relationArray, array_t *psVarBddArray, array_t *nsVarBddArray);
925EXTERN 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);
926EXTERN void * ImgImageInfoInitializeApprox(ImgFunctionData_t *functionData, Img_DirectionType directionType);
927EXTERN mdd_t * ImgImageInfoComputeFwdApprox(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet);
928EXTERN mdd_t * ImgImageInfoComputeFwdWithDomainVarsApprox(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet);
929EXTERN mdd_t * ImgImageInfoComputeBwdWithDomainVarsApprox(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet);
930EXTERN mdd_t * ImgImageInfoComputeBwdApprox(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet);
931EXTERN void ImgImageInfoPrintMethodParamsApprox(void *methodData, FILE *fp);
932EXTERN void ImgImageInfoFreeApprox(void *methodData);
933EXTERN mdd_t * ImgImageInfoComputeFwdFwdGrad(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet);
934EXTERN mdd_t * ImgImageInfoComputeFwdWithDomainVarsFwdGrad(ImgFunctionData_t *functionData, void *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, mdd_t *toCareSet);
935EXTERN void ImgImageInfoFreeFwdGradual(void *methodData);
936EXTERN void * ImgImageInfoInitializeGradual(void *methodData, ImgFunctionData_t * functionData, Img_DirectionType directionType);
937EXTERN void ImgImageInfoPrintMethodParamsFwdGrad(void *methodData, FILE *fp);
938EXTERN 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);
939EXTERN mdd_t * ImgImageByHybrid(ImgTfmInfo_t *info, array_t *vector, mdd_t *from);
940EXTERN mdd_t * ImgImageByHybridWithStaticSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube);
941EXTERN mdd_t * ImgPreImageByHybrid(ImgTfmInfo_t *info, array_t *vector, mdd_t *from);
942EXTERN mdd_t * ImgPreImageByHybridWithStaticSplit(ImgTfmInfo_t *info, array_t *vector, mdd_t *from, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube);
943EXTERN int ImgCheckEquivalence(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube, int preFlag);
944EXTERN int ImgCheckMatching(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray);
945EXTERN mdd_t* ImgMultiwayLinearAndSmooth(mdd_manager *mddManager, array_t *relationArray, array_t *smoothVarBddArray, array_t *introducedVarBddArray, Img_MethodType method, Img_DirectionType direction, ImgTrmOption_t *option);
946EXTERN 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);
947EXTERN mdd_t* ImgBddLinearAndSmooth(mdd_manager *mddManager, mdd_t *from, array_t *relationArray, array_t *arraySmoothVarBddArray, array_t *smoothVarCubeArray, int verbosity);
948EXTERN 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);
949EXTERN 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);
950EXTERN ImgTrmOption_t * ImgGetTrmOptions(void);
951EXTERN void ImgFreeTrmOptions(ImgTrmOption_t *option);
952EXTERN void * ImgImageInfoInitializeIwls95(void *methodData, ImgFunctionData_t *functionData, Img_DirectionType directionType, Img_MethodType method);
953EXTERN mdd_t * ImgImageInfoComputeFwdIwls95(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
954EXTERN mdd_t * ImgImageInfoComputeFwdWithDomainVarsIwls95(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
955EXTERN mdd_t * ImgImageInfoComputeBwdIwls95(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
956EXTERN mdd_t * ImgImageInfoComputeBwdWithDomainVarsIwls95(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
957EXTERN void ImgImageInfoFreeIwls95(void *methodData);
958EXTERN void ImgImageInfoPrintMethodParamsIwls95(void *methodData, FILE *fp);
959EXTERN st_table * ImgBddGetSupportIdTable(bdd_t *function);
960EXTERN boolean ImgImageWasPartialIwls95(void *methodData);
961EXTERN void ImgImageAllowPartialImageIwls95(void *methodData, boolean value);
962EXTERN void ImgRestoreTransitionRelationIwls95(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
963EXTERN void ImgDuplicateTransitionRelationIwls95(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
964EXTERN void ImgMinimizeTransitionRelationIwls95(void *methodData, ImgFunctionData_t *functionData, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, boolean reorderClusters, int printStatus);
965EXTERN void ImgAbstractTransitionRelationIwls95(Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, Img_DirectionType directionType, int printStatus);
966EXTERN 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);
967EXTERN array_t * ImgGetTransitionRelationIwls95(void *methodData, Img_DirectionType directionType);
968EXTERN void ImgUpdateTransitionRelationIwls95(void *methodData, array_t *relationArray, Img_DirectionType directionType);
969EXTERN void ImgReplaceIthPartitionedTransitionRelationIwls95(void *methodData, int i, mdd_t *relation, Img_DirectionType directionType);
970EXTERN void ImgImageFreeClusteredTransitionRelationIwls95(void *methodData, Img_DirectionType directionType);
971EXTERN void ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp(Img_ImageInfo_t *imageInfo, Img_DirectionType direction, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus);
972EXTERN void ImgPrintIntegerArray(array_t *idArray);
973EXTERN void ImgPrintPartition(graph_t *partition);
974EXTERN void ImgPrintPartitionedTransitionRelation(mdd_manager *mddManager, array_t *relationArray, array_t *arraySmoothVarBddArray);
975EXTERN mdd_t * ImgTrmEliminateDependVars(ImgFunctionData_t *functionData, array_t *relationArray, mdd_t *states, mdd_t **dependRelations, int *nDependVars);
976EXTERN void * ImgImageInfoInitializeMono(void *methodData, ImgFunctionData_t * functionData, Img_DirectionType directionType);
977EXTERN mdd_t * ImgImageInfoComputeFwdMono(ImgFunctionData_t * functionData, Img_ImageInfo_t * imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t * toCareSetArray);
978EXTERN mdd_t * ImgImageInfoComputeFwdWithDomainVarsMono(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
979EXTERN mdd_t * ImgImageInfoComputeBwdMono(ImgFunctionData_t * functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
980EXTERN mdd_t * ImgImageInfoComputeBwdWithDomainVarsMono(ImgFunctionData_t * functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
981EXTERN void ImgImageInfoFreeMono(void * methodData);
982EXTERN void ImgImageInfoPrintMethodParamsMono(void *methodData, FILE *fp);
983EXTERN void ImgRestoreTransitionRelationMono(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
984EXTERN void ImgDuplicateTransitionRelationMono(Img_ImageInfo_t *imageInfo);
985EXTERN void ImgMinimizeTransitionRelationMono(Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, int printStatus);
986EXTERN void ImgAddDontCareToTransitionRelationMono(Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, int printStatus);
987EXTERN void ImgAbstractTransitionRelationMono(Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, int printStatus);
988EXTERN 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);
989EXTERN void ImgImageConstrainAndClusterTransitionRelationMono(Img_ImageInfo_t *imageInfo, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus);
990EXTERN void * ImgImageInfoInitializeTfm(void *methodData, ImgFunctionData_t * functionData, Img_DirectionType directionType, Img_MethodType method);
991EXTERN mdd_t * ImgImageInfoComputeFwdTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
992EXTERN mdd_t * ImgImageInfoComputeFwdWithDomainVarsTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
993EXTERN mdd_t * ImgImageInfoComputeBwdTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
994EXTERN mdd_t * ImgImageInfoComputeBwdWithDomainVarsTfm(ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
995EXTERN void ImgImageInfoFreeTfm(void *methodData);
996EXTERN void ImgImageInfoPrintMethodParamsTfm(void *methodData, FILE *fp);
997EXTERN void ImgRestoreTransitionFunction(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
998EXTERN void ImgDuplicateTransitionFunction(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
999EXTERN void ImgMinimizeTransitionFunction(void *methodData, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, int printStatus);
1000EXTERN void ImgAddDontCareToTransitionFunction(void *methodData, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, int printStatus);
1001EXTERN void ImgAbstractTransitionFunction(Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, Img_DirectionType directionType, int printStatus);
1002EXTERN 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);
1003EXTERN array_t * ImgGetTransitionFunction(void *methodData, Img_DirectionType directionType);
1004EXTERN void ImgUpdateTransitionFunction(void *methodData, array_t *vector, Img_DirectionType directionType);
1005EXTERN void ImgReplaceIthTransitionFunction(void *methodData, int i, mdd_t *function, Img_DirectionType directionType);
1006EXTERN ImgTfmOption_t * ImgTfmGetOptions(Img_MethodType method);
1007EXTERN void ImgImageFreeClusteredTransitionRelationTfm(void *methodData, Img_DirectionType directionType);
1008EXTERN void ImgImageConstrainAndClusterTransitionRelationTfm(Img_ImageInfo_t *imageInfo, Img_DirectionType direction, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus);
1009EXTERN int ImgIsPartitionedTransitionRelationTfm(Img_ImageInfo_t *imageInfo);
1010EXTERN bdd_t * ImgTfmPreImage(ImgTfmInfo_t *info, bdd_t *image);
1011EXTERN void ImgCacheInitTable(ImgTfmInfo_t *info, int num_slot, int globalCache, boolean preImgFlag);
1012EXTERN void ImgCacheDestroyTable(ImgCacheTable_t *table, int globalCache);
1013EXTERN bdd_t * ImgCacheLookupTable(ImgTfmInfo_t *info, ImgCacheTable_t *table, array_t *delta, bdd_t *constraint);
1014EXTERN void ImgCacheInsertTable(ImgCacheTable_t *table, array_t *delta, bdd_t *constraint, bdd_t *result);
1015EXTERN void ImgFlushCache(ImgCacheTable_t *table);
1016EXTERN void ImgPrintCacheStatistics(ImgCacheTable_t *cache);
1017EXTERN mdd_t * ImgTfmImage(ImgTfmInfo_t *info, mdd_t *from);
1018EXTERN mdd_t * ImgChooseTrSplitVar(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, int trSplitMethod, int piSplitFlag);
1019EXTERN 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);
1020EXTERN 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);
1021EXTERN void ImgVectorFree(array_t *vector);
1022EXTERN int ImgVectorFunctionSize(array_t *vector);
1023EXTERN long ImgVectorBddSize(array_t *vector);
1024EXTERN array_t * ImgVectorCopy(ImgTfmInfo_t *info, array_t *vector);
1025EXTERN ImgComponent_t * ImgComponentAlloc(ImgTfmInfo_t *info);
1026EXTERN ImgComponent_t * ImgComponentCopy(ImgTfmInfo_t *info, ImgComponent_t *comp);
1027EXTERN void ImgComponentFree(ImgComponent_t *comp);
1028EXTERN void ImgComponentGetSupport(ImgComponent_t *comp);
1029EXTERN void ImgSupportCopy(ImgTfmInfo_t *info, char *dsupport, char *ssupport);
1030EXTERN void ImgSupportClear(ImgTfmInfo_t *info, char *support);
1031EXTERN void ImgSupportPrint(ImgTfmInfo_t *info, char *support);
1032EXTERN int ImgSupportCount(ImgTfmInfo_t *info, char *support);
1033EXTERN array_t * ImgGetConstrainedRelationArray(ImgTfmInfo_t *info, array_t *relationArray, mdd_t *constraint);
1034EXTERN array_t * ImgGetCofactoredRelationArray(array_t *relationArray, mdd_t *func);
1035EXTERN void ImgCofactorRelationArray(array_t *relationArray, mdd_t *func);
1036EXTERN array_t * ImgGetAbstractedRelationArray(mdd_manager *manager, array_t *relationArray, mdd_t *cube);
1037EXTERN void ImgAbstractRelationArray(mdd_manager *manager, array_t *relationArray, mdd_t *cube);
1038EXTERN array_t * ImgGetCofactoredAbstractedRelationArray(mdd_manager *manager, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube);
1039EXTERN array_t * ImgGetAbstractedCofactoredRelationArray(mdd_manager *manager, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube);
1040EXTERN array_t * ImgGetConstrainedVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint);
1041EXTERN array_t * ImgGetCofactoredVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *func);
1042EXTERN void ImgCofactorVector(ImgTfmInfo_t *info, array_t *vector, mdd_t *func);
1043EXTERN mdd_t * ImgTfmEliminateDependVars(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, mdd_t *states, array_t **newVector, mdd_t **dependRelations);
1044EXTERN int ImgExistConstIntermediateVar(array_t *vector);
1045EXTERN mdd_t * ImgGetComposedFunction(array_t *vector);
1046EXTERN ImgComponent_t * ImgGetLatchComponent(array_t *vector);
1047EXTERN array_t * ImgComposeConstIntermediateVars(ImgTfmInfo_t *info, array_t *vector, mdd_t *constIntermediate, mdd_t **cofactorCube, mdd_t **abstractCube, mdd_t **and_, mdd_t **from);
1048EXTERN int ImgCountBddSupports(mdd_t *func);
1049EXTERN void ImgCheckConstConstrain(mdd_t *f1, mdd_t *f2, int *f21p, int *f21n);
1050EXTERN int ImgConstConstrain(mdd_t *func, mdd_t *constraint);
1051EXTERN void ImgPrintVectorDependency(ImgTfmInfo_t *info, array_t *vector, int verbosity);
1052EXTERN float ImgPercentVectorDependency(ImgTfmInfo_t *info, array_t *vector, int length, int *nLongs);
1053EXTERN void ImgWriteSupportMatrix(ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, char *string);
1054EXTERN array_t * ImgMinimizeImageArrayWithCareSetArray(array_t *imageArray, array_t *careSetArray, Img_MinimizeType minimizeMethod, boolean underapprox, boolean printInfo, Img_DirectionType dir);
1055EXTERN void ImgMinimizeImageArrayWithCareSetArrayInSitu(array_t *imageArray, array_t *careSetArray, Img_MinimizeType minimizeMethod, boolean underapprox, boolean printInfo, Img_DirectionType dir);
1056EXTERN mdd_t * ImgSubstitute(mdd_t *f, ImgFunctionData_t *functionData, Img_SubstituteDir dir);
1057EXTERN array_t * ImgSubstituteArray(array_t *f_array, ImgFunctionData_t *functionData, Img_SubstituteDir dir);
1058EXTERN void ImgPrintPartialImageOptions(void);
1059EXTERN ImgPartialImageOption_t * ImgGetPartialImageOptions(void);
1060EXTERN int ImgArrayBddArrayCheckValidity(array_t *arrayBddArray);
1061EXTERN int ImgBddArrayCheckValidity(array_t *bddArray);
1062EXTERN int ImgBddCheckValidity(bdd_t *bdd);
1063EXTERN void ImgPrintVarIdTable(st_table *table);
1064EXTERN int ImgCheckToCareSetArrayChanged(array_t *toCareSetArray1, array_t *toCareSetArray2);
1065
1066EXTERN Relation_t * ImgLinearRelationInit(mdd_manager *mgr, array_t *relationArray, array_t *domainBddVars, array_t *rangeBddVars, array_t *qunatifyBddVars, ImgTrmOption_t *option);
1067EXTERN void ImgLinearRelationQuit(Relation_t *head);
1068EXTERN void ImgLinearRefineRelation(Relation_t *head);
1069
1070EXTERN array_t * ImgLinearExtractRelationArrayT(Relation_t *head);
1071EXTERN bdd_t ** ImgLinearExtractRelationArray(Relation_t *head);
1072EXTERN array_t * ImgLinearMakeSmoothVarBdd(Relation_t *head, bdd_t **smoothCubeArr);
1073EXTERN int * ImgLinearGetSupportBddId(mdd_manager *mgr, bdd_t *f, int *nSize);
1074EXTERN void ImgLinearOptimizeInternalVariables(Relation_t *head);
1075EXTERN 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 *));
1076EXTERN 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 *));
1077
1078
1079EXTERN 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);
1080
1081EXTERN int ImgLinearOptimizeAll(Relation_t *head, Img_OptimizeType optDir, int constantNSOpt);
1082
1083EXTERN void ImgResetMethodDataLinearComputeRange(void *methodData);
1084EXTERN void ImgSetMethodDataLinearComputeRange(void *methodData);
1085
1086
1087/**AutomaticEnd***************************************************************/
1088
1089#endif /* _INT */
Note: See TracBrowser for help on using the repository browser.