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

  FileName    [part.h]

  PackageName [part]

  Synopsis    [Partition of a system and creation of MDDs.]

  Description [Once the description of a system has been read, and the ordering
  of the variables has been assigned, the partition package creates an
  abstracted view of the system in which only information in terms of MDDs is
  stored. The MDDs belong to the MDD manager of the system. Different options
  may be considered when creating this abstracted view. If the system is
  described as a network there are several options to create this partition. As
  a first choice, the system may be considered as a set of functions
  representing the combinational outputs as functions of the combinational
  inputs. In general, the latch functions may be specified as functions of any
  intermediate variables. These intermediate variables are themselves functions
  of other variables, and ultimately the dependency on the combinational inputs
  is achieved. The structure to represent these arbitrary dependencies is a
  DAG. The combinational inputs of the network will be represented as
  vertices. Every other function (either representing a latch or any other
  intermediate node) is represented as a vertex with in-coming edges from the
  vertices representing the function's domain. Hence, the vertices representing
  the combinational inputs will not have any in-coming edges, and conversely,
  the vertices representing the combinational outputs will not have any fanout
  edges.<p>

  The partition may have two types of vertices, called single and
  clustered. Single vertices are the ones that represent, for example, nodes in
  a network. Clustered vertices are used solely for the purpose of grouping
  single vertices into disjoint sets. No clustered vertex can be member of a
  clustered vertex, and every single vertex may be a member of a unique clustered
  vertex. The edges of the graph are connecting only single vertices. Functions
  are provided to access the list of vertices represented by a clustered vertex
  as well as for testing the type of a vertex.<p>

  A partition is the central input to the image computation
  package.  However, it is important to note that there is no network-specific
  information stored in the partition data structure itself.  Hence, it is
  possible that another application (i.e. besides the network application)
  could create a partition, and use that partition as input to the image
  computation 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: part.h,v 1.33 2009/04/11 01:47:18 fabio Exp $]

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

#ifndef _PART
#define _PART

#include "ntk.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
#define PART_NETWORK_APPL_KEY "Part_NetworkApplKey"

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

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

  Synopsis    [Different methods of partitioning a system.]

  SeeAlso     [PartPartitionInputsOutputs PartPartitionTotal
  PartPartitionPartial]

******************************************************************************/
typedef enum {
  Part_Default_c,  /* Default partition. (Right now Outputs as function of
		    * inputs) */
  Part_InOut_c,    /* Outputs as function of inputs */
  Part_Total_c,    /* Replicates the system's structure */
  Part_Partial_c,   /* Preserves certain user-provided nodes */
  Part_Frontier_c,
  Part_Boundary_c,  /* partition nodes are subckt IOs */
  Part_Fine_c   /* partition nodes are subckt IOs */
} Part_PartitionMethod;

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

  Synopsis    [Type of vertex in the partition.]

  Description [There are two types of vertices in the partition: single and
  clustered. A single vertex represents itself and it may have a multi-valued
  function and a MddId attached to it. A clustered vertex represents a set of
  single vertices. The only information stored in this type of vertex is the
  list of single vertices being represented by the cluster. Only one level of
  hierarchy is allowed, that is, clustered vertices may only represent single
  vertices. Every single vertex may only be represented by a unique clustered
  vertex. In other words, a vertex representing a cluster of vertices cannot be
  a member of another cluster.]

  SeeAlso     [PartVertexInfo]

******************************************************************************/
typedef enum {
  Part_VertexCluster_c,  /* Vertex represents a cluster of vertices */
  Part_VertexSingle_c    /* Vertex represents itself */
} Part_VertexType;

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

  Synopsis    [ Methods of Breaking for State Space Decomposition ]

  SeeAlso     []

******************************************************************************/
typedef enum{
  Part_BSRR_s,    /* static round robin seed choice */
  Part_BFix_v     /* fixed order vertex choice */
} Part_BMethod;

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

  Synopsis    [ Method of Correlation calculation. ]

  Description [ Correlation is calculated by ratio of minterm count of XOR.
  If BDD function is not available or try to avoid using MDD operation,
  correaltion can be calculated by second method. Then, support set is
  generated from network and correlation is simply the ration of common support
  to union of two support sets.]

  SeeAlso     []

******************************************************************************/
typedef enum{
  Part_CorrelationWithBDD,    /* correlation is based on BDD correlation */
  Part_CorrelationWithSupport,   /* correlation is based on support */
  Part_CorrelationDefault
} Part_CMethod;

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef struct PartSubsystemInfo Part_SubsystemInfo_t;
typedef struct PartSubsystem Part_Subsystem_t;

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


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


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

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

EXTERN void Part_Init(void);
EXTERN void Part_End(void);
EXTERN array_t * Part_PartitionBuildFunctions(graph_t *partition, array_t *roots, array_t *leaves, mdd_t *careSet);
EXTERN array_t * Part_PartitionCollapse(graph_t *partition, array_t *roots, st_table *leaves, mdd_t *careSet);
EXTERN array_t * Part_PartGroupVeriticesBasedOnHierarchy(Ntk_Network_t *network, array_t *latchDataInputNames);
EXTERN array_t * Part_PartCreateSubsystems(Part_SubsystemInfo_t *subInfo, array_t *arrayOfLatchNames, array_t *arrayOfGroupIndex);
EXTERN array_t * Part_PartCreateSubsystemsWithCTL(Part_SubsystemInfo_t *subInfo, array_t *ctlArray, array_t *fairArray,boolean dynamicIncrease,boolean dynamicAndDependency);
EXTERN array_t * Part_PartCreateSubsystemsWithCtlAndLtl(Part_SubsystemInfo_t *subInfo, array_t *ctlArray, array_t *ltlArray, array_t *fairArray,boolean dynamicIncrease,boolean dynamicAndDependency,boolean strictBound);
EXTERN st_table * Part_PartitionSubsystemReadVertexTable(Part_Subsystem_t *partitionedSubsystem);
EXTERN array_t * Part_PartitionSubsystemReadFanIn(Part_Subsystem_t *partitionedSubsystem);
EXTERN array_t * Part_PartitionSubsystemReadFanOut(Part_Subsystem_t *partitionedSubsystem);
EXTERN Part_SubsystemInfo_t * Part_PartitionSubsystemInfoInit(Ntk_Network_t *network);
EXTERN void Part_PartitionSubsystemInfoFree(Part_SubsystemInfo_t *partSubInfo);
EXTERN void Part_PartitionSubsystemFree(Part_Subsystem_t *partSubsystem);
EXTERN void Part_PartitionSubsystemInfoSetNetwork(Part_SubsystemInfo_t *subInfo, Ntk_Network_t *network);
EXTERN void Part_PartitionSubsystemInfoSetBreakingMethod(Part_SubsystemInfo_t *subInfo, Part_BMethod bMethod);
EXTERN void Part_PartitionSubsystemInfoSetBound(Part_SubsystemInfo_t *subInfo, int bound);
EXTERN void Part_PartitionSubsystemInfoSetThreshold(Part_SubsystemInfo_t *subInfo, float threshold);
EXTERN void Part_PartitionSubsystemInfoSetVerbosity(Part_SubsystemInfo_t *subInfo, int verbosity);
EXTERN void Part_PartitionSubsystemInfoSetCorrelationMethod(Part_SubsystemInfo_t *subInfo, Part_CMethod corMethod);
EXTERN void Part_PartitionSubsystemInfoSetAffinityFactor( Part_SubsystemInfo_t *subInfo, float affinity);
EXTERN Part_Subsystem_t * Part_PartCreateSingleSubSystem( array_t *arrayOfNodes, Ntk_Network_t *network);
EXTERN graph_t * Part_CreatePartitionFromMvfs(mdd_manager *manager, st_table *nameToMvf, st_table *nameToId,  st_table *leafTable,  char *partName);
EXTERN graph_t * Part_NetworkCreatePartitionFromMvfs(Ntk_Network_t *network, st_table *nameToMvf);
EXTERN void Part_PartitionFree(graph_t *partition);
EXTERN void Part_PartitionFreeCallback(void *data);
EXTERN vertex_t * Part_PartitionFindVertexByName(graph_t *partition, char *name);
EXTERN vertex_t * Part_PartitionFindVertexByMddId(graph_t *partition, int mddId);
EXTERN char * Part_PartitionReadName(graph_t *partition);
EXTERN Part_PartitionMethod Part_PartitionReadMethod(graph_t *partition);
EXTERN char * Part_PartitionObtainMethodAsString(graph_t *partition);
EXTERN mdd_manager * Part_PartitionReadMddManager(graph_t *partition);
EXTERN Part_VertexType Part_VertexReadType(vertex_t *vertexPtr);
EXTERN char * Part_VertexReadName(vertex_t *vertexPtr);
EXTERN array_t * Part_VertexReadClusterMembers(vertex_t *vertexPtr);
EXTERN Mvf_Function_t * Part_VertexReadFunction(vertex_t *vertexPtr);
EXTERN void Part_VertexSetFunction(vertex_t *vertexPtr, Mvf_Function_t *mvf);
EXTERN int Part_VertexReadMddId(vertex_t *vertexPtr);
EXTERN boolean Part_VertexTestIsClustered(vertex_t *vertexPtr);
EXTERN graph_t * Part_NetworkCreatePartition(Ntk_Network_t *network, Hrc_Node_t *hnode, char *name, lsList rootList, lsList leaveList, mdd_t *careSet, Part_PartitionMethod method, lsList nodes, boolean inTermsOfLeaves, int verbose, int sanityCheck);
EXTERN graph_t * Part_PartitionDuplicate(graph_t *partition);
EXTERN graph_t * Part_NetworkReadPartition(Ntk_Network_t *network);
EXTERN vertex_t * Part_PartitionCreateClusterVertex(graph_t *partition, char *name, array_t *arrayOfVertices);
EXTERN void Part_UpdatePartitionFrontier(Ntk_Network_t *network, graph_t *partition, lsList rootList, lsList leaveList, mdd_t *careSet);
EXTERN void Part_VertexInfoFreeCluster(vertex_t *vertexPtr);
EXTERN boolean Part_PartitionTestCompletelySp(graph_t *partition, array_t *roots, st_table *leaves);
EXTERN boolean Part_PartitionTestDeterministic(graph_t *partition, array_t *roots, st_table *leaves);
EXTERN graph_t * Part_PartCreatePartitionWithCTL(Hrc_Manager_t ** hmgr, Part_PartitionMethod method, int verbose, int sanityCheck, boolean inTermsOfLeaves, array_t *ctlArray, array_t *fairArray);
EXTERN graph_t * Part_PartCreatePartitionWithCtlAndLtl(Hrc_Manager_t ** hmgr, Part_PartitionMethod method, int verbose, int sanityCheck, boolean inTermsOfLeaves, array_t *ctlArray, array_t *ltlArray, array_t *fairArray);
EXTERN int Part_PartitionChangeRoots(Ntk_Network_t *network, graph_t *partition, lsList rootList, int verbosity);
EXTERN void Part_PartitionPrintStats(FILE *fp, graph_t *partition, boolean printNodeNames);
EXTERN int Part_PartitionGetLatchInputListFromCTL(Ntk_Network_t *network, array_t *ctlArray, array_t *fairArray, lsList latchInputList);
EXTERN int Part_PartitionGetLatchInputListFromCtlAndLtl(Ntk_Network_t *network, array_t *ctlArray, array_t *ltlArray, array_t *fairArray, lsList latchInputList, boolean stopAtLatch);
EXTERN void Part_PartitionReadOrCreateBnvs(Ntk_Network_t *network, st_table *coiLatchTable, st_table *coiBnvTable);
EXTERN void PartPartitionFineGrain( Ntk_Network_t *network, graph_t       *partition, mdd_t *careSet);
EXTERN int Part_CheckLeafNodeCondition(Ntk_Node_t *node, st_table *leafTable, int fanoutFreeLimit, int numVariableLimit);
EXTERN int Img_CutCalcTransitiveFanin(st_table *table, st_table *ownTable, Ntk_Node_t *node, Ntk_Node_t *fanin, int limit);
EXTERN Ntk_Node_t * Part_GetFaninFreeLogic(Ntk_Node_t *node);
EXTERN Ntk_Node_t * Part_GetFanoutFreeLogic(Ntk_Node_t *node);
EXTERN void Part_PartitionWithExistingBnvs(Ntk_Network_t *network, graph_t *partition, st_table *coiBnvTable, st_table *absLatchTable, st_table *absBnvTable);

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

#endif /* _PART */