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

  FileName    [partInt.h]

  PackageName [part]

  Synopsis [Internal data type definitions and macros to handle the
  structures of the partition package.]

  Author      [Abelardo Pardo]

  Copyright   [This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

  Revision    [$Id: partInt.h,v 1.26 2005/04/16 06:14:54 fabio Exp $]

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

#ifndef _PARTINT
#define _PARTINT

#include <string.h>
#include <time.h>
#include "ntm.h"
#include "ord.h"
#include "cmd.h"
#include "part.h"
#include "img.h"
#include "mc.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
#define PART_SUB_CON_FACTOR 2 
#define PART_SUB_COR_FACTOR 4
#define PART_SUB_AFF_FACTOR 0.5 
#define BIG_NUMBER 10000

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

  Synopsis    [Information stored in the graph representing the partition.]

  Description [The information stored in the graph consists of the following
  fields.  The name of the system from which the partition was obtained. For
  example, if the system is of type Ntk_Network_t, the name stored here is a
  copy of the network's name. The method used to obtain the partition. The
  nameToVertex table provides a associative table to find a vertex in the
  partition by giving a name. The mddIdToVertex table is another hash table to
  find a vertex in the partition given a mddId..]

  SeeAlso     [PartVertexInfo st Part_PartitionMethod]

******************************************************************************/
typedef struct PartPartitionInfo {
  char *name;                         /* Name of the entity from which
				       * the partition was obtained */
  Part_PartitionMethod method;        /* Method used to create the partition */

  mdd_manager *mddManager;            /* manager of mdds for the partition */
  st_table *nameToVertex;             /* Table of name to vertex  */
  st_table *mddIdToVertex;            /* Table of mddId to vertex */
} PartPartitionInfo_t;

/**Struct**********************************************************************

  Synopsis    [Information stored in every vertex of the graph.]

  Description [There are two types of vertices in a partition: single and
  clustered.  A single vertex in the partition graph has a name, a multi-valued
  function and eventually a MddId. A clustered vertex stores an array of
  pointer to single vertices.  In general, a vertex does not need to have a
  name attached to it. There could be different heuristics for partitioning the
  system that could create <em>additional</em> vertices not related to the
  system. In these situations this name will be empty.<p>

  The type field stores the type of the vertex, single or clustered.  The mvf
  field stores the multi-valued function associated with the vertex. The
  vertices representing the variables in the support of this function
  constitute the fanin of this vertex. The MddId is the identifier assigned to
  the variable that this vertex represents (if any). Every vertex with no
  fanout, in principle does not have any variable Id attached to it, but if
  this information exists in the original system, it may be replicated here
  also. The boolean field <tt>isClustered</tt> is used to mark the single nodes
  that are already part of some clustered vertices, to avoid a single vertex
  being part of more than one cluster.]

  SeeAlso     [Part_VertexType PartPartitionInfo]

******************************************************************************/
typedef struct PartVertexInfo {
  Part_VertexType type;      /* Type of vertex */
  char *name;                /* Name of the unit (if the vertex corresponds to
                              * a unit in the system. If the unit is created by
                              * the partition package, this pointer is NULL).
                              */
  union {
    Mvf_Function_t *mvf;     /* Multi-valued function attached to the vertex */
    array_t *clusterMembers; /* Array of vertex_t * for the clustered vertex */
  } functionality;
  int mddId;                 /* Id of the variable attached to the vertex, if
			      * any. */
  boolean isClustered;       /* Boolean that determines if the vertex is part
			      * of a clustered vertex.*/
} PartVertexInfo_t;

/**Struct**********************************************************************

  Synopsis    [Information for cleating the sub-systems]

  SeeAlso     [Part_PartitionSubsystemInfoInit 
               PartBreakingBigConnectedComponent ]

******************************************************************************/
struct PartSubsystemInfo{
  Ntk_Network_t  *network;       /* network */
  array_t        *arrayOfVertex; /* Target vertices to be decomposed into
                                  * sub-systems */ 
  int            numberOfVertex; /* total number of vertices */
  Part_BMethod   partBM;         /* Breaking method */
  int            bound;          /* maximum number of vertices in 
                                  * a sub-system */
  float          threshold;      /* threshold value to determine if
                                  * two vertices are connected or not */
  float          con_factor;     /* weight factor to emphasize the mutual 
                                  * over the single dependency between two 
                                  * vertices */ 
  float          cor_factor;     /* weight factor to lower the value
                                  * of a pair of vertices which are
                                  * only slightly correlated */
  float          aff_factor;     /* weight factor to emphasize either 
                                  * connectivity(aff_factor>0.5)  or 
                                  * correlation(aff_factor<0.5). */  
  int		 verbosity;
  int            corMethod;      /* method for correlation
                                  * 0 : use BDD correlation (default)
                                  * 1 : use support */
  st_table	*dupLatchTable;	 /* stores
				  * (latchInputName, array of latchName) */
  st_table	*latchNameTable; /* stores (latchInputName, latchName) */
};

/**Struct**********************************************************************

  Synopsis    [Structure for each Sub-system]

  SeeAlso     []

******************************************************************************/
struct PartSubsystem{
  st_table *vertexNameTable; /* table containing names of latches in each
				sub-system (not a map)*/  
  array_t  *subsystemFanIn;  /* indices of sub-subsystems which are fanin
                              * of current sub-system */ 
  array_t  *subsystemFanOut; /* indices of sub-subsystems which are fanout 
                              * of current sub-system */
 
};

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


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


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

/**Macro***********************************************************************

  Synopsis     [Internal macro to access the name of the partition.]

  SideEffects  []

  SeeAlso      [PartPartitionInfo]

******************************************************************************/
#define PartPartitionReadName(                            \
  /* graph_t * */ pPtr /* Pointer to a graph structure */ \
)                                                         \
    ((PartPartitionInfo_t *)(pPtr)->user_data)->name

/**Macro***********************************************************************

  Synopsis [Internal macro to access the method used to create the partition.]

  SideEffects  []

  SeeAlso      [PartPartitionInfo]

******************************************************************************/
#define PartPartitionReadMethod(                          \
  /* graph_t * */ pPtr /* Pointer to a graph structure */ \
)                                                         \
    ((PartPartitionInfo_t *)(pPtr)->user_data)->method


/**Macro***********************************************************************

  Synopsis     [Internal macro to access the MDD manager of the partition.]

  SideEffects  []

  SeeAlso      [PartPartitionInfo]

******************************************************************************/
#define PartPartitionReadMddManager(                      \
  /* graph_t * */ pPtr /* Pointer to a graph structure */ \
)                                                         \
    ((PartPartitionInfo_t *)(pPtr)->user_data)->mddManager

/**Macro***********************************************************************

  Synopsis [Internal macro to access the nameToVertex field of the
  partition.]

  SideEffects  []

  SeeAlso      [PartPartiotionInfo]

******************************************************************************/
#define PartPartitionReadNameToVertex(                    \
  /* graph_t * */ pPtr /* Pointer to a graph structure */ \
)                                                         \
    ((PartPartitionInfo_t *)(pPtr)->user_data)->nameToVertex

/**Macro***********************************************************************

  Synopsis [Internal macro to access the mddIdToVertex field of the partition.]

  SideEffects  []

  SeeAlso      [PartPartitionInfo]

******************************************************************************/
#define PartPartitionReadMddIdToVertex(                   \
  /* graph_t * */ pPtr /* Pointer to a graph structure */ \
)                                                         \
    ((PartPartitionInfo_t *)(pPtr)->user_data)->mddIdToVertex

/**Macro***********************************************************************

  Synopsis     [Internal macro to access the type of a vertex.]

  SideEffects  []

  SeeAlso      [PartVertexInfo]

******************************************************************************/
#define PartVertexReadType(                                                 \
  /* vertex_t * */ vPtr /* Pointer to vertex in the graph data structure */ \
)                                                                           \
    ((PartVertexInfo_t *)(vPtr)->user_data)->type

/**Macro***********************************************************************

  Synopsis     [Internal macro to access the name of a vertex.]

  SideEffects  []

  SeeAlso      [PartVertexInfo]

******************************************************************************/
#define PartVertexReadName(                                                 \
  /* vertex_t * */ vPtr /* Pointer to vertex in the graph data structure */ \
)                                                                           \
    ((PartVertexInfo_t *)(vPtr)->user_data)->name

/**Macro***********************************************************************

  Synopsis     [Internal macro to access the clusterMembers of a vertex.]

  SideEffects  []

  SeeAlso      [PartVertexInfo]]

******************************************************************************/
#define PartVertexReadClusterMembers(                                       \
  /* vertex_t * */ vPtr /* Pointer to vertex in the graph data structure */ \
)                                                                           \
    ((PartVertexInfo_t *)(vPtr)->user_data)->functionality.clusterMembers


/**Macro***********************************************************************

  Synopsis [Internal macro to access the multi-valued function of a
  vertex.]

  SideEffects  []

  SeeAlso      [PartVertexInfo]

******************************************************************************/
#define PartVertexReadFunction(                                             \
  /* vertex_t * */ vPtr /* Pointer to vertex in the graph data structure */ \
)                                                                           \
    ((PartVertexInfo_t *)(vPtr)->user_data)->functionality.mvf

/**Macro***********************************************************************

  Synopsis [Internal macro to set the multi-valued function of a
  vertex.]

  SideEffects  []

  SeeAlso      [PartVertexInfo]

******************************************************************************/
#define PartVertexSetFunction(                                          \
  /* vertex_t * */       vPtr     /* Pointer to vertex in the graph */, \
  /* Mvf_Function_t * */ function /* Function to store */               \
)                                                                       \
    ((PartVertexInfo_t *)(vPtr)->user_data)->functionality.mvf = (function)

/**Macro***********************************************************************

  Synopsis     [Internal macro to access the mdd Id of a vertex.]

  SideEffects  []

  SeeAlso      [PartVertexInfo]

******************************************************************************/
#define PartVertexReadMddId(                                                \
  /* vertex_t * */ vPtr /* Pointer to vertex in the graph data structure */ \
)                                                                           \
    ((PartVertexInfo_t *)(vPtr)->user_data)->mddId

/**Macro***********************************************************************

  Synopsis     [Internal macro to access the isClustered of a vertex.]

  SideEffects  []

  SeeAlso      [PartVertexInfo]

******************************************************************************/
#define PartVertexTestIsClustered(                                          \
  /* vertex_t * */ vPtr /* Pointer to vertex in the graph data structure */ \
)                                                                           \
    ((PartVertexInfo_t *)(vPtr)->user_data)->isClustered

/**Macro***********************************************************************

  Synopsis     [Sets the isClustered field of a vertex.]

  SideEffects  []

  SeeAlso      [PartVertexInfo]

******************************************************************************/
#define PartVertexSetIsClustered(                                  \
  /* vertex_t * */ vPtr  /* Pointer to vertex in the graph */,     \
  /* boolean */    value /* Boolean representing IsClustered ?  */ \
)                                                                  \
    ((PartVertexInfo_t *)(vPtr)->user_data)->isClustered = (value)

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

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

EXTERN void partCreateBoundaryNames(Hrc_Node_t *hnode, st_table *tableOfFormalNames);
EXTERN void PartPartitionBoundary(Ntk_Network_t *network, Hrc_Node_t *hnode, graph_t *partition, lsList rootList, lsList leaveList, mdd_t *careSet, int inTermsOfCombInputs);
EXTERN void PartNameFree(lsGeneric name);
EXTERN void PartPartitionFrontier(Ntk_Network_t *network, graph_t *partition, lsList rootList, lsList leaveList, mdd_t *careSet);
EXTERN void PartUpdateFrontier(Ntk_Network_t *network, graph_t *partition, lsList rootList, lsList leaveList, mdd_t *careSet);
EXTERN void PartPrintPartition(graph_t *partition);
EXTERN array_t * PartCreateSubsystem(Part_SubsystemInfo_t *partSubInfo, array_t *arrayOfLatchNames, array_t *arrayOfGroupIndex);
EXTERN void PartPartitionInputsOutputs(Ntk_Network_t *network, graph_t *partition, lsList rootList, lsList leaveList, mdd_t *careSet);
EXTERN int PartPartitionInOutChangeRoots(Ntk_Network_t *network, graph_t *partition, lsList  rootList, int verbosity);
EXTERN PartPartitionInfo_t * PartPartitionInfoCreate(char *name, mdd_manager *manager, Part_PartitionMethod method);
EXTERN void PartPartitionInfoFree(gGeneric partitionInfo);
EXTERN PartVertexInfo_t * PartVertexInfoCreateSingle(char *name, Mvf_Function_t *mvf, int mddId);
EXTERN PartVertexInfo_t * PartVertexInfoCreateCluster(char *name, array_t *vertexArray);
EXTERN void PartVertexInfoFree(gGeneric vertexInfo);
EXTERN void PartPartitionSanityCheck(graph_t *partition, int intensity);
EXTERN st_table * PartCreateFunctionSupportTable(Mvf_Function_t *mvf);
EXTERN void PartPartitionCreateVertexFaninEdges(graph_t *partition, vertex_t *vertexPtr);
EXTERN int PartPartitionPrint(FILE *fp, graph_t *partition);
EXTERN int PartGetLatchInputListFromCTL(Ntk_Network_t *network, array_t *ctlArray, array_t *fairArray, lsList  latchInputList);
EXTERN int PartGetLatchListFromCtlAndLtl(Ntk_Network_t *network, array_t *ctlArray, array_t *ltlArray, array_t *fairArray, lsList  latchInputList, boolean stopAtLatch);
EXTERN int PartGetLatchInputListFromCtlAndLtl(Ntk_Network_t *network, array_t *ctlArray, array_t *ltlArray, array_t *fairArray, lsList  latchInputList, boolean stopAtLatch);
EXTERN void PartPartitionPartial(Ntk_Network_t *network, graph_t *partition, lsList rootList, lsList leaveList, mdd_t *careSet, lsList nodeList, int inTermsOfCombInputs);
EXTERN void PartPartitionTotal(Ntk_Network_t *network, graph_t *partition, lsList rootList, lsList leaveList, mdd_t *careSet, int inTermsOfLeaves);
EXTERN void PartInsertBnvs(Ntk_Network_t *network, st_table *coiLatchTable, st_table *coiBnvTable);
EXTERN void PartPartitionWithExistingBnvs(Ntk_Network_t *network, graph_t *partition, st_table *coiBnvTable, st_table *absLatchTable, st_table *absBnvTable);
EXTERN void PartPartitionUpdateWithExistingBnvs(Ntk_Network_t *network, graph_t *partition, st_table *coiBnvTable, st_table *absLatchTable, st_table *absBnvTable);

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

#endif /* _PARTINT */