/**CHeaderFile*****************************************************************

  FileName    [img.h]

  PackageName [img]

  Synopsis    [Methods for performing image computations.]

  Description [The image package is used to compute the image (forward or
  backward) of a set under a vector of functions.  The functions are given by
  a graph of multi-valued functions (MVFs). This graph is built using the
  partition package. Each vertex in this graph has an MVF and an MDD id.  The
  fanins of a vertex v give those vertices upon which the MVF at v depends.
  The vector of functions to use for an image computation, the "roots", is
  specified by an array of (names of) vertices of the graph.  The domain
  variables are the variables over which "from" sets are defined for forward
  images, and "to" sets are defined for backward images.  The range variables
  are the variables over which "to" sets are defined for forward images, and
  "from" sets are defined for backward images.  The quantify variables are
  additional variables over which the functions are defined; this set is
  disjoint from domain variables.  These variables are existentially
  quantified from the results of backward image computation. <p>
  
  Computing images is fundamental to many symbolic analysis techniques, and
  methods for computing images efficiently is an area of ongoing research.
  For this reason, the image package has been designed with lots of
  flexibility to easily allow new methods to be integrated (to add a new
  method, see the instructions in imgInt.h).  Applications that use the image
  package can switch among different image methods simply by specifying the
  method type in the image initialization routine.  By using the returned
  structure (Img_ImageInfo_t) from the initialization routine, all subsequent
  (forward or backward) image computations will be done using the specified
  method.<p>
  
  VIS users can control which image method is used by appropriately setting
  the "image_method" flag.  Also, VIS users can set flags to control
  parameters for different image computation methods.  Because the user has
  the ability to change the values of these flags, Img_ImageInfo_t structs
  should be freed and re-initialized whenever the VIS user changes the value
  of these flags.<p>
  
  Following are descriptions of the methods implemented. In the descriptions,
  x=x_1,...x_n is the set of domain variables, u=u_1,...,u_k is the set of
  quantify variables, y=y_1,...,y_m is the set of range variables, and
  f=f_1(x,u),...,f_m(x,u) is the set of functions under which we wish to
  compute images.<p>
  
  <b>Monolithic:</b> This is the most naive approach possible.  A single
  relation T(x,y) is constructed during the initialization phase, using the
  computation (exists u (prod_i(y_i = f_i(x,u)))). To compute the forward
  image, where fromUpperBound=U(x), fromLowerBound=L(x), and toCareSet=C(y),
  we first compute a set A(x) between U(x) and L(x).  Then, T(x,y) is
  simplified with respect to A(x) and C(y) to get T*.  Finally, x is
  quantified from T* to produce the final answer.  Backward images are
  computed analogously.  The monolithic method does not recognize any
  user-settable flags for image computation.<p>

  <b>IWLS95:</b> This technique is based on the early quantification heuristic.
  The initialization process consists of following steps:   
  <UL>
  <LI> Create the relation of the roots at the bit level
  in terms of the quantify and domain variables.
  <LI> Order the bit level relations.
  <LI> Group the relations of bits together, making a cluster
  whenever the BDD size reaches a threshold.
  <LI> For each cluster, quantify out the quantify variables which
  are local to that particular cluster.
  <LI> Order the clusters using the algorithm given in
  "Efficient BDD Algorithms for FSM Synthesis and
  Verification", by R. K. Ranjan et. al. in the proceedings of
  IWLS'95{1}. 
  <LI> The orders of the clusters for forward and backward image are
  calculated and stored. Also stored is the schedule of
  variables for early quantification. 
  </UL>
  For forward and backward image computation the corresponding
  routines are called with appropriate ordering of clusters and
  early quantification schedule. <p>]

  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: img.h,v 1.50 2005/05/15 01:03:36 jinh Exp $]

******************************************************************************/

#ifndef _IMG
#define _IMG

#include "vm.h"
#include "ntk.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/* This is a threshold for finding dependent variables. */
#define	IMG_MAX_DEP_SIZE	20

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef struct ImgImageInfoStruct Img_ImageInfo_t;

/**Enum************************************************************************

  Synopsis    [Methods for image computation.  See the description in img.h.]

******************************************************************************/
typedef enum {
  Img_Monolithic_c,
  Img_Iwls95_c,
  Img_Mlp_c,
  Img_Tfm_c, /* transition function method */
  Img_Hybrid_c, /* hybrid image comutation */
  Img_Linear_c,
  Img_Linear_Range_c,
  Img_Default_c
} Img_MethodType;


/**Enum************************************************************************

  Synopsis    [Type to indicate the direction of image computation.]

  Description [Type to indicate the direction of image computation.  When an
  imageInfo structure is initialized, the application must specify what
  "directions" of image computation will be performed: forward, backward, or
  both.]

******************************************************************************/
typedef enum {
  Img_Forward_c,
  Img_Backward_c,
  Img_Both_c
} Img_DirectionType;


/**Enum************************************************************************

  Synopsis    [Type to indicate image minimization method.]

  Description [Type to indicate image minimization method.]

******************************************************************************/
typedef enum {
  Img_Restrict_c, /* default */
  Img_Constrain_c,
  Img_Compact_c,
  Img_Squeeze_c,
  Img_And_c,
  Img_OrNot_c,
  Img_DefaultMinimizeMethod_c /* refer to img_minimize_method */
} Img_MinimizeType;

/**Enum************************************************************************

  Synopsis    [Image substitute direction]

******************************************************************************/
typedef enum {
  Img_D2R_c,	/* domain to range */
  Img_R2D_c	/* range to domain */
} Img_SubstituteDir;

/**Enum************************************************************************

  Synopsis    [State variables optimization direction]

******************************************************************************/
typedef enum {
  Opt_None,
  Opt_CS,
  Opt_NS,
  Opt_Both
} Img_OptimizeType;

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

EXTERN int Img_ImageBuildFwdLFPRelation(Ntk_Network_t *network, Img_ImageInfo_t *imageInfo, mdd_t *constraint, int whichTime, int *maxTime, int *numBlocks);
EXTERN void Img_PrintHybridOptions(void);
EXTERN mdd_t* Img_MultiwayLinearAndSmooth(mdd_manager *mddManager, array_t *relationArray, array_t *smoothVarMddIdArray, array_t *introducedVarMddIdArray, Img_MethodType method, Img_DirectionType direction);
EXTERN void Img_PrintPartitionedTransitionRelation(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
EXTERN void Img_ReorderPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
EXTERN void Img_UpdateQuantificationSchedule(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
EXTERN void Img_ClusterRelationArray(mdd_manager *mddManager, Img_MethodType method, Img_DirectionType direction, array_t *relationArray, array_t *domainVarMddIdArray, array_t *rangeVarMddIdArray, array_t *quantifyVarMddIdArray, array_t **clusteredRelationArray, array_t **arraySmoothVarBddArray, array_t **smoothVarCubeArray, boolean freeRelationArray);
EXTERN void Img_PrintMlpOptions(void);
EXTERN int Img_TfmGetRecursionStatistics(Img_ImageInfo_t *imageInfo, int preFlag, int *nRecurs, int *nLeaves, int *nTurns, float *averageDepth, int *maxDepth, int *nDecomps, int *topDecomp, int *maxDecomp, float *averageDecomp);
EXTERN void Img_TfmPrintStatistics(Img_ImageInfo_t *imageInfo, Img_DirectionType dir);
EXTERN void Img_TfmPrintRecursionStatistics(Img_ImageInfo_t *imageInfo, int preFlag);
EXTERN void Img_PrintTfmOptions(void);
EXTERN int Img_TfmGetCacheStatistics(Img_ImageInfo_t *imageInfo, int preFlag, double *inserts, double *lookups, double *hits, double *entries, int *nSlots, int *maxChainLength);
EXTERN int Img_TfmCheckGlobalCache(int preFlag);
EXTERN void Img_TfmPrintCacheStatistics(Img_ImageInfo_t *imageInfo, int preFlag);
EXTERN void Img_TfmFlushCache(Img_ImageInfo_t *imageInfo, int preFlag);
EXTERN void Img_Init(void);
EXTERN void Img_End(void);
EXTERN Img_MethodType Img_UserSpecifiedMethod(void);
EXTERN Img_ImageInfo_t * Img_ImageInfoInitialize(Img_ImageInfo_t *imageInfo, graph_t * mddNetwork, array_t * roots, array_t * domainVars, array_t * rangeVars, array_t * quantifyVars, mdd_t * domainCube, mdd_t * rangeCube, mdd_t * quantifyCube, Ntk_Network_t * network, Img_MethodType methodType, Img_DirectionType directionType, int FAFWFlag, mdd_t *winning);
EXTERN void Img_ImageInfoUpdateVariables(Img_ImageInfo_t *imageInfo, graph_t * mddNetwork, array_t * domainVars, array_t * quantifyVars, mdd_t * domainCube, mdd_t * quantifyCube);
EXTERN void Img_ImageAllowPartialImage(Img_ImageInfo_t *info, boolean value);
EXTERN void Img_ImagePrintPartialImageOptions(void);
EXTERN boolean Img_ImageWasPartial(Img_ImageInfo_t *info);
EXTERN mdd_t * Img_ImageInfoComputeImageWithDomainVars(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray);
EXTERN mdd_t * Img_ImageInfoComputeFwdWithDomainVars(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, mdd_t * toCareSet);
EXTERN mdd_t * Img_ImageInfoComputeFwd(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray);
EXTERN mdd_t * Img_ImageInfoComputePreImageWithDomainVars(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray);
EXTERN mdd_t * Img_ImageInfoComputeEXWithDomainVars(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray);
EXTERN mdd_t * Img_ImageInfoComputeBwdWithDomainVars(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, mdd_t * toCareSet);
EXTERN mdd_t * Img_ImageInfoComputeBwd(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray);
EXTERN void Img_ImageInfoFree(Img_ImageInfo_t * imageInfo);
EXTERN char * Img_ImageInfoObtainMethodTypeAsString(Img_ImageInfo_t * imageInfo);
EXTERN Img_MethodType Img_ImageInfoObtainMethodType(Img_ImageInfo_t * imageInfo);
EXTERN void Img_ImageInfoPrintMethodParams(Img_ImageInfo_t *imageInfo, FILE *fp);
EXTERN void Img_ResetTrMinimizedFlag(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
EXTERN Img_MinimizeType Img_ReadMinimizeMethod(void);
EXTERN void Img_MinimizeTransitionRelation(Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, boolean reorderIwls95Clusters);
EXTERN mdd_t * Img_MinimizeImage(mdd_t *image, mdd_t *constraint, Img_MinimizeType method, boolean underapprox);
EXTERN mdd_t * Img_AddDontCareToImage(mdd_t *image, mdd_t *constraint, Img_MinimizeType method);
EXTERN mdd_t * Img_MinimizeImageArray(mdd_t *image, array_t *constraintArray, Img_MinimizeType method, boolean underapprox);
EXTERN void Img_SetPrintMinimizeStatus(Img_ImageInfo_t *imageInfo, int status);
EXTERN int Img_ReadPrintMinimizeStatus(Img_ImageInfo_t *imageInfo);
EXTERN void Img_AbstractTransitionRelation(Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, Img_DirectionType directionType);
EXTERN void Img_DupTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
EXTERN void Img_RestoreTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
EXTERN int Img_ApproximateTransitionRelation(Img_ImageInfo_t *imageInfo, bdd_approx_dir_t approxDir, bdd_approx_type_t approxMethod, int approxThreshold, double approxQuality, double approxQualityBias, Img_DirectionType directionType, mdd_t *bias);
EXTERN mdd_t * Img_ApproximateImage(mdd_manager *mgr, mdd_t *image, bdd_approx_dir_t approxDir, bdd_approx_type_t approxMethod, int approxThreshold, double approxQuality, double approxQualityBias, mdd_t *bias);
EXTERN int Img_IsPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo);
EXTERN void Img_ResetNumberOfImageComputation(Img_DirectionType imgDir);
EXTERN int Img_GetNumberOfImageComputation(Img_DirectionType imgDir);
EXTERN array_t * Img_GetPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType);
EXTERN void Img_ReplaceIthPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, int i, mdd_t *relation, Img_DirectionType directionType);
EXTERN void Img_ReplacePartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, array_t *relationArray, Img_DirectionType directionType);
EXTERN mdd_t * Img_ComposeIntermediateNodes(graph_t *partition, mdd_t *node, array_t *psVars, array_t *nsVars, array_t *inputVars);
EXTERN void Img_ImageConstrainAndClusterTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType direction, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus);
EXTERN Img_MinimizeType Img_GuidedSearchReadUnderApproxMinimizeMethod(void);
EXTERN Img_MinimizeType Img_GuidedSearchReadOverApproxMinimizeMethod(void);
EXTERN mdd_t * Img_Substitute(Img_ImageInfo_t *imageInfo, mdd_t *f, Img_SubstituteDir dir);
EXTERN mdd_t * Img_ImageGetUnreachableStates(Img_ImageInfo_t * imageInfo);
EXTERN void Img_ImageInfoSetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo);
EXTERN void Img_ImageInfoResetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo);
EXTERN void Img_ImageInfoResetLinearComputeRange(Img_ImageInfo_t * imageInfo);
EXTERN void Img_ImageInfoSetLinearComputeRange(Img_ImageInfo_t * imageInfo);
EXTERN int Img_IsTransitionRelationOptimized(Img_ImageInfo_t * imageInfo);
EXTERN void Img_ForwardImageInfoConjoinWithWinningStrategy( Img_ImageInfo_t * imageInfo, mdd_t *winningStrategy);
EXTERN void Img_ForwardImageInfoRecoverFromWinningStrategy( Img_ImageInfo_t * imageInfo);
EXTERN Img_OptimizeType Img_ImageInfoObtainOptimizeType(Img_ImageInfo_t * imageInfo);
EXTERN int Img_IsQuantifyCubeSame( Img_ImageInfo_t *imageInfo, mdd_t *quantifyCube);
EXTERN int Img_IsQuantifyArraySame( Img_ImageInfo_t *imageInfo, array_t *quantifyArray);
EXTERN void Img_ImageInfoFreeFAFW(Img_ImageInfo_t * imageInfo);




/**
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);
**/



/**AutomaticEnd***************************************************************/

#endif /* _IMG */