source: vis_dev/vis-2.3/src/part/partPart.c

/**CFile************************************************************************

  FileName    [partPart.c]

  PackageName [part]

  Synopsis [Routines to initialize the command <em>build_partition_mdds</em>,
  create and delete internal data structures of the partition, and print
  information about the partition.]

  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.]

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

#include "partInt.h"

static char rcsid[] UNUSED = "$Id: partPart.c,v 1.45 2009/04/11 01:47:18 fabio Exp $";

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

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static void PrintVertexDescription(FILE *fp, vertex_t *vertexPtr, int order);

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

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis [Deletes the graph created for the partition and all the information
  attached to it.]

  SideEffects []

  SeeAlso     [PartPartitionInfoFree PartVertexInfoFree]

******************************************************************************/
void
Part_PartitionFree(
   graph_t *partition)
{
  /* Delete the graph information */
  g_free(partition, PartPartitionInfoFree, PartVertexInfoFree,
         (void (*)(gGeneric))0);
} /* End of Part_PartitionFree */


/**Function********************************************************************

  Synopsis    [Call-back function to free a partition.]

  Description [This function will be stored in the network together with the
  pointer to the structure. Whenever the network deletes the partitioning
  information, this function is called and it will deallocate the partition and
  the information attached to it.]

  SideEffects []

  SeeAlso     [Ntk_NetworkAddApplInfo]

******************************************************************************/
void
Part_PartitionFreeCallback(
   void *data)
{
  Part_PartitionFree((graph_t *) data);
} /* End of Part_PartitionFreeCallback */

/**Function********************************************************************

  Synopsis    [Finds a vertex in the graph with a certain name.]

  Description [Given a name, it returns a pointer to a vertex structure if
  there is a vertex with that name in the partition. Otherwise it returns a
  NULL pointer.]

  SideEffects []

  SeeAlso     [PartPartitionInfo]

******************************************************************************/
vertex_t *
Part_PartitionFindVertexByName(
  graph_t *partition,
  char *name)
{
  vertex_t *result = NIL(vertex_t);
  st_table *table = PartPartitionReadNameToVertex(partition);

  if (table != NIL(st_table)) {
    st_lookup(table, name, &result);
  } /* End of if */

  return result;
} /* End of Part_PartitionFindVertexByName */

/**Function********************************************************************

  Synopsis    [Finds a vertex in the graph with a certain MddId.]

  Description [Given a MddId, it returns a pointer to a vertex structure if
  there is a vertex with that mddId in the partition. Otherwise it returns a
  NULL pointer.]

  SideEffects []

  SeeAlso     [PartVertexInfo]

******************************************************************************/
vertex_t *
Part_PartitionFindVertexByMddId(
  graph_t *partition,
  int mddId)
{
  vertex_t *result = NIL(vertex_t);
  st_table *table = PartPartitionReadMddIdToVertex(partition);

  if (table != NIL(st_table)) {
    st_lookup(table, (char *)(long)mddId, &result);
  } /* End of if */

  return result;
} /* End of Part_PartitionFindVertexByMddId */

/**Function********************************************************************

  Synopsis [Returns the name of the entity from which the partition
  was created.]

  SideEffects []

  SeeAlso     [PartPartitionInfo]

******************************************************************************/
char *
Part_PartitionReadName(
   graph_t *partition)
{
  return PartPartitionReadName(partition);
} /* End of Part_PartitionReadName */

/**Function********************************************************************

  Synopsis [Returns the method which was used to create the partition graph.]

  SideEffects []

  SeeAlso     [PartPartitionInfo]

******************************************************************************/
Part_PartitionMethod
Part_PartitionReadMethod(
  graph_t *partition)
{
  Part_PartitionMethod  method;

  method = PartPartitionReadMethod(partition);
  if (method == Part_Default_c)
    method = Part_Frontier_c;
  return(method);
} /* End of Part_PartitionReadMethod */

/**Function********************************************************************

  Synopsis    [Returns the partition method as a string.]

  Description [Returns the method stored in the partition as a new
  string. The caller of the function has the responsibility of freeing
  the string. The possible values of the string are: "Inputs-Outputs",
  "Total", "Partial" or "Frontier".]

  SideEffects []

  SeeAlso     [Part_PartitionPrintStats]

******************************************************************************/
char *
Part_PartitionObtainMethodAsString(
  graph_t *partition)
{
  char *resultString;

  assert(partition != NIL(graph_t));

  switch(PartPartitionReadMethod(partition)) {
    case Part_Total_c:
      resultString = util_strsav("Total");
      break;
    case Part_Partial_c:
      resultString = util_strsav("Partial");
      break;
    case Part_InOut_c:
      resultString = util_strsav("Inputs-Outputs");
      break;
    case Part_Frontier_c:
    case Part_Default_c:
      resultString = util_strsav("Frontier");
      break;
    case Part_Boundary_c:
      resultString = util_strsav("Boundary");
      break;
    case Part_Fine_c:
      resultString = util_strsav("Fine");
      break;
    default:
      fail("Unexpected Partition method.");
  }

  return resultString;
} /* End of Part_PartitionObtainMethodAsString */

/**Function********************************************************************

  Synopsis    [Function to read the manager attached to the partition.]

  SideEffects []

  SeeAlso     [PartPartitionInfo]

******************************************************************************/
mdd_manager *
Part_PartitionReadMddManager(
  graph_t *partition)
{
  return PartPartitionReadMddManager(partition);
} /* End of Part_PartitionReadMddManager */

/**Function********************************************************************

  Synopsis    [Returns the type of a vertex.]

  SideEffects []

  SeeAlso     [PartVertexInfo Part_VertexType]

******************************************************************************/
Part_VertexType
Part_VertexReadType(
  vertex_t *vertexPtr)
{
  return PartVertexReadType(vertexPtr);
} /* End of Part_VertexReadType */

/**Function********************************************************************

  Synopsis    [Reads the name attached to a vertex.]

  SideEffects []

  SeeAlso     [PartVertexInfo]

******************************************************************************/
char *
Part_VertexReadName(
  vertex_t *vertexPtr)
{
  return PartVertexReadName(vertexPtr);
} /* End of Part_VertexReadName */

/**Function********************************************************************

  Synopsis    [Reads the clusterMembers field  of a vertex.]

  Description [This function does not make sure that the vertex is of clustered
  type. It is the responsibility of the caller to guarantee that.]

  SideEffects []

  SeeAlso     [PartVertexInfo]

******************************************************************************/
array_t *
Part_VertexReadClusterMembers(
  vertex_t *vertexPtr)
{
  return PartVertexReadClusterMembers(vertexPtr);
} /* End of Part_VertexReadClusterMembers */

/**Function********************************************************************

  Synopsis    [Reads the multi-valued function attached to a vertex.]

  Description [This function does not make sure that the vertex is of single
  type.  It is the responsibility of the caller to guarantee that.]

  SideEffects []

  SeeAlso     [PartVertexInfo]

******************************************************************************/
Mvf_Function_t *
Part_VertexReadFunction(
  vertex_t *vertexPtr)
{
    return PartVertexReadFunction(vertexPtr);
} /* End of Part_VertexReadFunction */


/**Function********************************************************************

  Synopsis    [Sets the multi-valued function of a vertex.]

  SideEffects []

  SeeAlso     [PartVertexInfo]

******************************************************************************/
void
Part_VertexSetFunction(
  vertex_t *vertexPtr,
  Mvf_Function_t *mvf)
{
  assert(PartVertexReadType(vertexPtr) != Part_VertexCluster_c);

  PartVertexSetFunction(vertexPtr, mvf);
} /* End of Part_VertexSetFunction */


/**Function********************************************************************

  Synopsis    [Reads the MddId attached to a vertex.]

  SideEffects []

  SeeAlso     [PartVertexInfo]

******************************************************************************/
int
Part_VertexReadMddId(
  vertex_t *vertexPtr)
{
    return PartVertexReadMddId(vertexPtr);
} /* End of Part_VertexReadMddId */

/**Function********************************************************************

  Synopsis    [Test of a vertex is member of a cluster.]

  SideEffects []

  SeeAlso     [PartVertexInfo Part_VertexReadType]

******************************************************************************/
boolean
Part_VertexTestIsClustered(
  vertex_t *vertexPtr)
{
  return PartVertexTestIsClustered(vertexPtr);
} /* End of Part_VertexTestIsClustered */

/**Function********************************************************************

  Synopsis    [Executes the selected partitioning method.]

  Description [Given a network, and a method, the function creates a partition
  by using the specified method. This function may be called from any point in
  the code to create a partition.  In particular, the command partition uses
  this function to create the partition and store it in the network.<p>

  The function receives two lists of pointers to network nodes, the roots and
  the leaves. The function will create the partition of the subnetwork between
  the root and the leave nodes. As a special case, if both lists are passed NIL
  values, the root and leave lists default to combinational outputs and
  combinational inputs respectively.

  The parameter <tt>careSet</tt> specifies which minterms in the input space are
  considered.

  The <tt>nodes</tt> parameter is an optional list of nodes that may be
  specified in case the <tt>partial</tt> method is used. It represents the set
  of nodes in the network to be preserved when building the partition. The
  boolean variable <tt>inTermsOfLeaves</tt> is valid only in the case of
  the <tt>total</tt> method and provides the option of creating the functions
  attached to the vertices in terms of the combinational inputs or in terms of
  their immediate fanin.  Two additional parameters are provided to control the
  verbosity and the intensity of the sanity check applied to the computation.<p>

  This function is called by the command build_partition_mdds which has a
  time-out option.  In the event of the execution time going over the time out,
  the control is returned to the prompt and all the memory allocated by the
  internal procedures is leaked.]

  SideEffects []

  SeeAlso     [part.h]

******************************************************************************/
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)
{
  graph_t    *partition;
  long       lap = 0;

  if (verbose) {
    lap = util_cpu_time();
  } /* End of if */

  /* Create the new graph to represent the partition */
  partition = g_alloc();
  partition->user_data =
    (gGeneric)PartPartitionInfoCreate(name,
                                      Ntk_NetworkReadMddManager(network),
                                      method);

  switch (method) {
    case Part_Partial_c:
      if (verbose) {
        (void) fprintf(vis_stdout, "Partitioning the system by the Partial");
        (void) fprintf(vis_stdout, " method\n");
      } /* End of if */
      PartPartitionPartial(network, partition, rootList, leaveList, careSet,
                           nodes, inTermsOfLeaves);
      break;
    case Part_Boundary_c:
      if (verbose) {
        (void) fprintf(vis_stdout, "Partitioning the system by the Boundary");
        (void) fprintf(vis_stdout, " method\n");
      } /* End of if */
      PartPartitionBoundary(network, hnode, partition, rootList, leaveList, careSet,
                           inTermsOfLeaves);
      break;
    case Part_Total_c:
      if (verbose) {
        (void) fprintf(vis_stdout, "Partitioning the circuit by the Total");
        (void) fprintf(vis_stdout, " method\n");
      } /* End of if */
      PartPartitionTotal(network, partition, rootList, leaveList, careSet,
                         inTermsOfLeaves);
      break;
    case Part_Frontier_c:
    case Part_Default_c:
      if (verbose) {
        (void) fprintf(vis_stdout, "Partitioning the circuit by the Frontier");
        (void) fprintf(vis_stdout, " method\n");
      } /* End of if */
      PartPartitionFrontier(network, partition, rootList, leaveList, careSet);
      break;
    case Part_Fine_c:
      if (verbose) {
        (void) fprintf(vis_stdout, "Partitioning the circuit for the fine-grain");
        (void) fprintf(vis_stdout, " method\n");
      } /* End of if */
      PartPartitionFineGrain(network, partition, careSet);
      break;
    case Part_InOut_c:
      if (verbose) {
        (void) fprintf(vis_stdout, "Partitioning the circuit by the");
        (void) fprintf(vis_stdout, " Input-Output method\n");
      } /* End of if */
      PartPartitionInputsOutputs(network, partition, rootList,
                                 leaveList, careSet);
      break;
    default:
      (void) fprintf(vis_stdout, "Partition method not implemented yet\n");
      break;
  }

  if (sanityCheck >0) {
    PartPartitionSanityCheck(partition, sanityCheck);
  }

  if (verbose) {
    (void) fprintf(vis_stdout, "%.2f (secs) spent in partitioning.\n",
                   (util_cpu_time() - lap)/1000.0);
  } /* End of if */

  return partition;
} /* End of Part_NetworkCreatePartition */

/**Function********************************************************************

  Synopsis    [Creates a duplicate of a partition.]

  SideEffects []

  SeeAlso     [PartVertexInfo, PartPartitionInfo]

******************************************************************************/
graph_t *
Part_PartitionDuplicate(
  graph_t *partition)
{
  graph_t          *result;
  lsGen            gen;
  vertex_t         *fromVertex;
  vertex_t         *toVertex;
  edge_t           *edgePtr;

  result = g_alloc();
  result->user_data =
    (gGeneric)PartPartitionInfoCreate(PartPartitionReadName(partition),
                                      PartPartitionReadMddManager(partition),
                                      PartPartitionReadMethod(partition));
  foreach_vertex(partition, gen, fromVertex) {
    char *name;
    int  mddId;

    name = PartVertexReadName(fromVertex);
    mddId = PartVertexReadMddId(fromVertex);
    toVertex = g_add_vertex(result);

    st_insert(PartPartitionReadNameToVertex(result), name, (char *)toVertex);

    if (mddId != NTK_UNASSIGNED_MDD_ID) {
      st_insert(PartPartitionReadMddIdToVertex(result), (char *)(long)mddId,
                (char *)toVertex);
    } /* End of if */

    if (PartVertexReadType(fromVertex) == Part_VertexSingle_c) {
      Mvf_Function_t *mdd;

      mdd = Mvf_FunctionDuplicate(PartVertexReadFunction(fromVertex));
      toVertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, mdd,
                                                                 mddId);
    }
    if (PartVertexReadType(fromVertex) == Part_VertexCluster_c) {
      toVertex->user_data =
        (gGeneric)PartVertexInfoCreateCluster(name, Part_VertexReadClusterMembers(fromVertex));
    }
  }

  foreach_edge(partition, gen, edgePtr) {
    vertex_t *fromVertexCopy;
    vertex_t *toVertexCopy;

    fromVertex = g_e_source(edgePtr);
    toVertex = g_e_dest(edgePtr);

    st_lookup(PartPartitionReadNameToVertex(result),
              PartVertexReadName(fromVertex), &fromVertexCopy);
    st_lookup(PartPartitionReadNameToVertex(result),
              PartVertexReadName(toVertex), &toVertexCopy);

    g_add_edge(fromVertexCopy, toVertexCopy);
  }

  return result;
} /* End of Part_PartitionDuplicate */


/**Function********************************************************************

  Synopsis    [Create reduced partition according to given CTL formulae]

  Comments    [Combinational root and leave nodes are combinational support
  nodes of given CTL properties.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
graph_t *
Part_PartCreatePartitionWithCTL(
  Hrc_Manager_t **hmgr,
  Part_PartitionMethod method,
  int verbose,
  int sanityCheck,
  boolean inTermsOfLeaves,
  array_t *ctlArray,
  array_t *fairArray)
{
  return Part_PartCreatePartitionWithCtlAndLtl(hmgr, method, verbose,
                                               sanityCheck, inTermsOfLeaves,
                                               ctlArray, NIL(array_t),
                                               fairArray);
}

/**Function********************************************************************

  Synopsis    [Create reduced partition according to given CTL formulae]

  Comments    [Combinational root and leave nodes are combinational support
  nodes of given CTL properties.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
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)
{
  char          *modelName;
  Hrc_Node_t    *currentNode;
  graph_t       *partition;
  lsList        latchInputList;
  lsGen         gen;
  Ntk_Node_t    *node;
  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);

  latchInputList = lsCreate();
  currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
  modelName = Hrc_NodeReadModelName(currentNode);

  if (method != Part_InOut_c){
    return NIL(graph_t);
  }

  PartGetLatchInputListFromCtlAndLtl(network, ctlArray, ltlArray, fairArray,
                                     latchInputList, FALSE);

  Ntk_NetworkForEachCombOutput(network, gen, node){
    if (Ntk_NodeTestIsLatchInitialInput(node)){
      lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
    }
  }

  /*
   * Execute the partition algorithm. If rootList and leaveList are null,
   * graph includes all network nodes
   */
  partition = Part_NetworkCreatePartition(network, currentNode, modelName,
                 latchInputList, (lsList)0, NIL(mdd_t), method, (lsList)0,
                 inTermsOfLeaves, verbose, sanityCheck);

  lsDestroy(latchInputList, (void (*)(lsGeneric))0);
  return partition;
}


/**Function********************************************************************

  Synopsis    [Change partition to include new vertex in root list]

  Comments    [Current partition in increased to include all next state
  functions for all members in rootList.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Part_PartitionChangeRoots(
  Ntk_Network_t *network,
  graph_t *partition,
  lsList  rootList,
  int verbosity)
{
  if (Part_PartitionReadMethod(partition) != Part_InOut_c){
    return 0;
  }

  return
   PartPartitionInOutChangeRoots(network, partition, rootList, verbosity);
}


/**Function********************************************************************

  Synopsis    [Reads the partition attached to a network.]

  SideEffects []

  SeeAlso     [CommandBuildPartitionMdds]

******************************************************************************/
graph_t *
Part_NetworkReadPartition(
  Ntk_Network_t *network)
{
  return (graph_t *)Ntk_NetworkReadApplInfo(network, PART_NETWORK_APPL_KEY);
} /* End of Part_NetworkReadPartition */


/**Function********************************************************************

  Synopsis    [Adds a vertex to the partition representing a set of vertices.]

  SideEffects []

  SeeAlso     [PartVertexInfo]

******************************************************************************/
vertex_t *
Part_PartitionCreateClusterVertex(
  graph_t *partition,
  char *name,
  array_t *arrayOfVertices)
{
  vertex_t *newVertex;

  newVertex = g_add_vertex(partition);
  newVertex->user_data = (gGeneric)PartVertexInfoCreateCluster(name,
                                                               arrayOfVertices);

  return(newVertex);

} /* End of Part_PartitionCreateClusterVertex */

/**Function********************************************************************

  Synopsis    [ Partition by adding vertices for the nodes in rootList
  and leaveList.  A node in leaveList may already have a corresponding
  vertex in the partition graph -- Only creating the new vertex if not exists.
  Nodes in rootList should NOT have existing vertices in the partition graph.
  (The caller should guarantee this)

  This routine is for the use in the 'ltl' package. We assume the partition
  method is Part_Frontier_c.]

  SideEffects [partition might be changed.]

  SeeAlso     [PartPartitionFrontier]

******************************************************************************/
void
Part_UpdatePartitionFrontier(
  Ntk_Network_t *network,
  graph_t *partition,
  lsList  rootList,
  lsList  leaveList,
  mdd_t   *careSet)
{
  PartUpdateFrontier(network, partition, rootList, leaveList, careSet);
}

/**Function********************************************************************

  Synopsis    [Removes a cluster vertex from the partition.]

  SideEffects []

  SeeAlso     [PartVertexInfo]

******************************************************************************/
void
Part_VertexInfoFreeCluster(
  vertex_t *vertexPtr)
{
  if (PartVertexReadType(vertexPtr) == Part_VertexCluster_c) {
    g_delete_vertex(vertexPtr, PartVertexInfoFree, (void (*)(gGeneric))0);
  } /* End of then */
  else {
    (void) fprintf(vis_stderr, "Warning -- Inconsistent vertex deletion in");
    (void) fprintf(vis_stderr, " partition package\n");
  }
} /* End of Part_VertexInfoFreeCluster */

/**Function********************************************************************

  Synopsis [Test if the functions attached to a set of vertices in the
  partition are completely specified.]

  Description [Given a set of vertices (roots) build their functions in terms
  of a second set of vertices (leaves) and test if the functions are
  completely specified.]

  SideEffects []

  SeeAlso     [Part_PartitionTestDeterministic]

******************************************************************************/
boolean
Part_PartitionTestCompletelySp(
  graph_t *partition,
  array_t *roots,
  st_table *leaves)
{
  array_t *mvfFunctions;
  vertex_t *vertexPtr;
  Mvf_Function_t *functionPtr;
  boolean result = TRUE;
  int i;
  char *vertexName;

  mvfFunctions = Part_PartitionCollapse(partition, roots, leaves, NIL(mdd_t));

  arrayForEachItem(Mvf_Function_t *, mvfFunctions, i, functionPtr) {
    vertexPtr = array_fetch(vertex_t *, roots, i);
    vertexName = PartVertexReadName(vertexPtr);
    if (!Mvf_FunctionTestIsCompletelySpecified(functionPtr)) {
      error_append("Vertex ");
      error_append(vertexName);
      error_append(" is not completely specified\n");
      result = FALSE;
    } /* End of if */

    /* We don't need the Mvf_Function any more, so we delete it */
    Mvf_FunctionFree(functionPtr);
  }

  /* Clean up*/
  array_free(mvfFunctions);

  return result;
} /* End of Part_PartitionTestCompletelySp */

/**Function********************************************************************

  Synopsis    [Test if the functions attached to a set of vertices in the
  partition are deterministic.]

  Description [Given a set of vertices (roots) build their functions in terms
  of a second set of vertices (leaves) and test if the functions are
  deterministic.]

  SideEffects []

  SeeAlso     [Part_PartitionTestCompletelySp]

******************************************************************************/
boolean
Part_PartitionTestDeterministic(
  graph_t *partition,
  array_t *roots,
  st_table *leaves)
{
  array_t *mvfFunctions;
  vertex_t *vertexPtr;
  Mvf_Function_t *functionPtr;
  boolean result = TRUE;
  int i;
  char *vertexName;

  mvfFunctions = Part_PartitionCollapse(partition, roots, leaves, NIL(mdd_t));

  arrayForEachItem(Mvf_Function_t *, mvfFunctions, i, functionPtr) {
    vertexPtr = array_fetch(vertex_t *, roots, i);
    vertexName = PartVertexReadName(vertexPtr);
    if (!Mvf_FunctionTestIsDeterministic(functionPtr)) {
      error_append("Vertex ");
      error_append(vertexName);
      error_append(" is non-deterministic\n");
      result = FALSE;
    } /* End of if */

    /* We don't need the Mvf_Function any more, so we delete it */
    Mvf_FunctionFree(functionPtr);
  }

  /* Clean up*/
  array_free(mvfFunctions);

  return result;
} /* End of Part_PartitionTestDeterministic */

/**Function********************************************************************

  Synopsis    [Create latch input nodes list from CTL properties and fairness
  constraints]

  Comments    []

  SideEffects [latchInputList is changed]

  SeeAlso     []

******************************************************************************/
int
Part_PartitionGetLatchInputListFromCTL(
  Ntk_Network_t *network,
  array_t *ctlArray,
  array_t *fairArray,
  lsList  latchInputList)
{
  return PartGetLatchInputListFromCTL( network, ctlArray, fairArray,
                                       latchInputList);
}

/**Function********************************************************************

  Synopsis    [Create latch input nodes list from CTL properties and fairness
  constraints]

  Comments    []

  SideEffects [latchInputList is changed]

  SeeAlso     []

******************************************************************************/
int
Part_PartitionGetLatchInputListFromCtlAndLtl(
  Ntk_Network_t *network,
  array_t *ctlArray,
  array_t *ltlArray,
  array_t *fairArray,
  lsList  latchInputList,
  boolean stopAtLatch)
{
  return PartGetLatchInputListFromCtlAndLtl( network, ctlArray, ltlArray,
                                             fairArray,
                                             latchInputList, stopAtLatch);
}

/**Function********************************************************************

  Synopsis    [Prints statistics about the partition DAG.]

  Comments    [If the parameter printNodeNames is true, the function prints
  names of the network nodes represented by vertices in the partition graph.]

  SideEffects []

  SeeAlso     [PartPartitionInfo]

******************************************************************************/
void
Part_PartitionPrintStats(
  FILE *fp,
  graph_t *partition,
  boolean printNodeNames)
{
  lsList vertexList = g_get_vertices(partition);
  vertex_t *vertexPtr;
  array_t *functions;
  Mvf_Function_t* vertexFunction;
  mdd_t *mddPtr;
  lsGen gen;
  char *methodName;
  int numVertices = lsLength(vertexList);
  int numSources;
  int numSinks;
  int i;

  /* Obtain the method name as a string */
  methodName = Part_PartitionObtainMethodAsString(partition);

  /*
   * Count the number of sources and sinks and at the same time store all the
   * bdd_t of every vertex in a common array to compute the shared size.
   */
  numSources = 0;
  numSinks = 0;
  functions = array_alloc(mdd_t *, 0);
  if (printNodeNames) {
    (void) fprintf(fp, "Network nodes represented as vertices in the ");
    (void) fprintf(fp, "partition:\n");
  }
  foreach_vertex(partition, gen, vertexPtr) {
    if (lsLength(g_get_in_edges(vertexPtr)) == 0) {
      numSources++;
    } /* End of if */
    if (lsLength(g_get_out_edges(vertexPtr)) == 0) {
      numSinks++;
    } /* End of if */
    if (PartVertexReadType(vertexPtr) == Part_VertexSingle_c) {
      if (printNodeNames) {
        if (PartVertexReadName(vertexPtr) != NIL(char)) {
          (void) fprintf(fp, "%s\n", PartVertexReadName(vertexPtr));
        }
      }
      vertexFunction = PartVertexReadFunction(vertexPtr);
      if (vertexFunction != NIL(Mvf_Function_t)) {
        Mvf_FunctionForEachComponent(vertexFunction, i, mddPtr) {
          array_insert_last(mdd_t *, functions, mddPtr);
        }
      } /* End of if */
    } /* End of if */
  } /* foreach_vertex*/

  /* Print results */
  (void)fprintf(fp, "Method %s, %d sinks, %d sources,", methodName, numSinks, numSources);
  (void)fprintf(fp, " %d total vertices,", numVertices);
  (void)fprintf(fp, " %ld mdd nodes\n", bdd_size_multiple(functions));

  /* Clean up */
  FREE(methodName);
  array_free(functions);

  return;
} /* End of Part_PartitionPrintStats */

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis [Initializes the information attached to the graph of the
  partition.]

  Description [Allocates the memory needed for the information attached to the
  graph structure.]

  SideEffects []

  SeeAlso     [PartPartitionInfo PartPartitionInfoFree]

******************************************************************************/
PartPartitionInfo_t *
PartPartitionInfoCreate(
  char *name,
  mdd_manager *manager,
  Part_PartitionMethod method)
{
  PartPartitionInfo_t *recordPartition = ALLOC(PartPartitionInfo_t, 1);

  recordPartition->name          = util_strsav(name);
  recordPartition->method        = method;
  recordPartition->mddManager    = manager;
  recordPartition->nameToVertex  = st_init_table(strcmp,st_strhash);
  recordPartition->mddIdToVertex = st_init_table(st_numcmp, st_numhash);

  return recordPartition;
} /* End of PartPartitionInfoCreate */

/**Function********************************************************************

  Synopsis [Deallocates the user information in the graph.]

  Description [Deallocates the user information in the graph. Does not free the
  MDD manager associated with the partition.]

  SideEffects []

  SeeAlso     [PartPartitionInfoCreate]

******************************************************************************/
void
PartPartitionInfoFree(
  gGeneric partitionInfo)
{
  if (((PartPartitionInfo_t *)partitionInfo)->name != NIL(char)) {
    FREE(((PartPartitionInfo_t *)partitionInfo)->name);
  }

  st_free_table(((PartPartitionInfo_t *)partitionInfo)->nameToVertex);
  st_free_table(((PartPartitionInfo_t *)partitionInfo)->mddIdToVertex);

  FREE(partitionInfo);
} /* End of PartPartitionInfoFree */

/**Function********************************************************************

  Synopsis [Initializes the information attached to a single vertex.]

  SideEffects []

  SeeAlso     [PartVertexInfo]

******************************************************************************/
PartVertexInfo_t *
PartVertexInfoCreateSingle(
  char *name,
  Mvf_Function_t *mvf,
  int mddId)
{
  PartVertexInfo_t *result;

  result                    = ALLOC(PartVertexInfo_t, 1);
  result->type              = Part_VertexSingle_c;
  result->name              = util_strsav(name);
  result->functionality.mvf = mvf;
  result->mddId             = mddId;
  result->isClustered       = 0;

  return result;
} /* End of PartVertexInfoCreateSingle */

/**Function********************************************************************

  Synopsis    [Creates a cluster vertex in the partition.]

  SideEffects []

  SeeAlso     [PartVertexInfo]

******************************************************************************/
PartVertexInfo_t *
PartVertexInfoCreateCluster(
  char *name,
  array_t *vertexArray)
{
  PartVertexInfo_t *result;
  vertex_t *auxPtr;
  int i;

  /* Make sure all the nodes are simple nodes */
  for(i = 0; i < array_n(vertexArray); i++) {
    auxPtr = array_fetch(vertex_t *, vertexArray, i);
    if (PartVertexReadType(auxPtr) == Part_VertexCluster_c) {
      fail("Only one level of hierarchy allowed in the partition");
    } /* End of if */
    if (PartVertexTestIsClustered(auxPtr)) {
      fail("Partition: Clustering vertex already member of another cluster");
    } /* End of then */
    else {
      PartVertexSetIsClustered(auxPtr, 1);
    }
  } /* End of for */

  result                               = ALLOC(PartVertexInfo_t, 1);
  result->type                         = Part_VertexCluster_c;
  result->name                         = util_strsav(name);
  result->functionality.clusterMembers = array_dup(vertexArray);

  result->mddId                        = NTK_UNASSIGNED_MDD_ID;
  result->isClustered                  = 0;

  return result;
} /* End of PartVertexInfoCreateCluster */

/**Function********************************************************************

  Synopsis [Deallocates the user information attached to a vertex.]

  SideEffects []

  SeeAlso     [PartVertexInfo]

******************************************************************************/
void
PartVertexInfoFree(
  gGeneric vertexInfo
   )
{
  if (((PartVertexInfo_t *)vertexInfo)->type == Part_VertexSingle_c) {
    /* Free the function attached to the node if any */
    if (((PartVertexInfo_t *)vertexInfo)->functionality.mvf !=
        NIL(Mvf_Function_t)) {
      Mvf_FunctionFree(((PartVertexInfo_t *)vertexInfo)->functionality.mvf);
    } /* End of if */
  } /* End of then */
  else {
    if (((PartVertexInfo_t *)vertexInfo)->functionality.clusterMembers !=
        NIL(array_t)) {
      array_free(((PartVertexInfo_t *)vertexInfo)->functionality.clusterMembers);
    } /* End of if */
  } /* End of if-then-else */

  if (((PartVertexInfo_t *)vertexInfo)->name != NIL(char)) {
    FREE(((PartVertexInfo_t *)vertexInfo)->name);
  }

  FREE(vertexInfo);
} /* End of PartVertexInfoFree */

/**Function********************************************************************

  Synopsis [Verifies that the information in the nameToVertex table of
  a graph is consistent.]

  SideEffects []

  SeeAlso     [PartPartitionInfo]

******************************************************************************/
void
PartPartitionSanityCheck(
  graph_t *partition,
  int intensity)
{
  st_table *table;
  lsList vertexList = g_get_vertices(partition);
  lsGen lgen;
  vertex_t *vertex, *rvertex;

  /* Consistency in the nameToVertex table */
  table = PartPartitionReadNameToVertex(partition);

  /*
   * The number of elements in the nameToVertex table and the number
   * of vertices agrees
   */
  if (lsLength(g_get_vertices(partition)) != st_count(table)) {
    (void) fprintf(vis_stderr, "Warning -- NameToVertex table incomplete in ");
    (void) fprintf(vis_stderr, " graph\n");
    if (intensity > 1) {
      (void) fprintf(vis_stderr, "  %d vertices in the graph and %d entries",
                     lsLength(g_get_vertices(partition)),
                     st_count(table));
      (void) fprintf(vis_stderr, " in the nameToVertex table\n");
    } /* End of if */
  } /* End of if */

  lsForEachItem(vertexList, lgen, vertex) {
    char *name = PartVertexReadName(vertex);
    if (!st_lookup(table, name, &rvertex) ||
        strcmp(PartVertexReadName(vertex),PartVertexReadName(rvertex)) != 0) {
      (void) fprintf(vis_stderr, "Warning -- Inconsistency detected in");
      (void) fprintf(vis_stderr, " the partition data-base\n");
    }
  }

  /* Consistency in the mddIdToVertexTable */
  table = PartPartitionReadMddIdToVertex(partition);
  lsForEachItem(vertexList, lgen, vertex) {
    int mddId = PartVertexReadMddId(vertex);
    if((mddId != NTK_UNASSIGNED_MDD_ID) &&
       (!st_lookup(table, (char *)(long)mddId, &rvertex) ||
        PartVertexReadMddId(vertex) != PartVertexReadMddId(rvertex))) {
      (void) fprintf(vis_stderr, "Warning -- Inconsistency detected in the");
      (void) fprintf(vis_stderr, " partition data-base\n");
    }
  }

  /*
   * Make sure that the mdd Id NTK_UNASSIGNED_MDD_ID does not appear in the
   * mddIdToVertex node.
   */
  table = PartPartitionReadMddIdToVertex(partition);
  if (st_is_member(table, (char *) NTK_UNASSIGNED_MDD_ID)) {
    (void) fprintf(vis_stderr, "Warning -- Inconsistency detected in the");
    (void) fprintf(vis_stderr, " partition data-base\n");
  } /* End of if */

  /* Check the Mvfs in the vertices of the partition.*/
  if (intensity > 1) {
    lsForEachItem(vertexList, lgen, vertex) {
      Mvf_Function_t *function = PartVertexReadFunction(vertex);
      int i;

      (void) fprintf(vis_stderr, "Vertex: %s, mddId: %d, Clustered: %c\n",
                     PartVertexReadName(vertex),
                     PartVertexReadMddId(vertex),
                     (PartVertexReadType(vertex) == Part_VertexCluster_c)?'t':'f');
      for(i = 0; i < Mvf_FunctionReadNumComponents(function); i ++) {
        mdd_t *unit = Mvf_FunctionObtainComponent(function, i);
        boolean x;

        if (intensity > 2) {
          (void) fprintf(vis_stderr, "BDD_T: %lx, %lx\n",
                         (unsigned long) bdd_get_node(unit, &x),
                         (unsigned long) mdd_get_manager(unit));
        }
      } /* End of for */
    }
  } /* End of if */

  /* ToDo: Check for redundant name in the list of vertices */
} /* End of PartPartitionSanityCheck */

/**Function********************************************************************

  Synopsis    [Computes the support of an array of mdds.]

  Description [Computes the support of a multi-valued function. It is
  just the union of the supports of every component of the function.]

  Comment [The reason why is it returned in a table is because it's very likely
  that questions such as, "is certain Id part of the support ?"  will happen.]

  SideEffects []

  SeeAlso     [PartVertexCreateFaninEdges]

******************************************************************************/
st_table *
PartCreateFunctionSupportTable(
  Mvf_Function_t *mvf)
{
  mdd_manager  *mddManager;        /* Manager for the MDDs */
  array_t      *support;
  st_table     *mddSupport = st_init_table(st_numcmp, st_numhash);
  int          numComponents = Mvf_FunctionReadNumComponents(mvf);
  int          j, k;
  mdd_t        *unit;

  assert(numComponents!= 0);

  mddManager = Mvf_FunctionReadMddManager(mvf);

  /*
   * compute the support of an mdd as the union of supports of every
   * function component
   */
  for(j = 0; j < numComponents; j++) {
    unit = Mvf_FunctionReadComponent(mvf, j);
    support = mdd_get_support(mddManager, unit);

    /* For every element of its support */
    for(k = 0; k < array_n(support); k++) {
      st_insert(mddSupport, (char *)(long)array_fetch(int, support, k), (char *)0);
    } /* End of for */
    array_free(support);
  } /* End of for */

  return mddSupport;
} /* End of PartCreateFunctionSupportTable */

/**Function********************************************************************

  Synopsis [Creates fanin edges of a vertex based on MDD support.]

  Description [Computes the support of the function attached to a vertex and
  adds to the graph the edges from the vertices representing those variables
  to the given vertex.]

  SideEffects []

******************************************************************************/
void
PartPartitionCreateVertexFaninEdges(
  graph_t  *partition,
  vertex_t *vertexPtr)
{
  vertex_t       *fromVertex;
  Mvf_Function_t *vertexFunction;
  st_table       *support;
  st_table       *mddIdToVertex;
  st_generator   *stGen;
  long            mddId;

  mddIdToVertex = PartPartitionReadMddIdToVertex(partition);
  vertexFunction = PartVertexReadFunction(vertexPtr);
  support = PartCreateFunctionSupportTable(vertexFunction);

  /* Create the edges for every element in support */
  st_foreach_item(support, stGen, &mddId, NULL) {
    st_lookup(mddIdToVertex, (char *)mddId, &fromVertex);
    /* Make sure no self loops are created */
    if (fromVertex != vertexPtr) {
      g_add_edge(fromVertex, vertexPtr);
    } /* End of if */
  }

  st_free_table(support);
} /* End of PartPartitionCreateVertexFaninEdges */

/**Function********************************************************************

  Synopsis [Prints information about the Partition through standard output.]

  Description [ The format used for printing is <b>dot</b>, a tool for
  graph visualization developed at AT&T. It can be obtained from <a
  href="http://www.research.att.com/orgs/ssr/book/reuse">
  http://www.research.att.com/orgs/ssr/book/reuse</a>. The function
  receives as a parameter a file pointer in case the print wants to be
  redirected. This function is used by the command routine
  CommandPrintPartition.]

  SideEffects []

******************************************************************************/
int
PartPartitionPrint(
  FILE *fp,
  graph_t *partition)
{
  lsGen      gen;           /* To iterate over edges */
  edge_t     *edgePtr;      /* Will hold the edge being processed */
  vertex_t   *fromVertex;   /* Will hold the vertex source of the edge */
  vertex_t   *toVertex;     /* Will hold the destination of the edge */
  st_table   *vertexToId;   /* To lookup the ordinal of a vertex */
  time_t      now           = time(0);
  struct tm  *nowStructPtr  = localtime(& now);
  char       *nowTxt        = asctime(nowStructPtr);
  char       *partitionName = PartPartitionReadName(partition);
  int        vertexId;
  int        clusterId;

  /*
   * Write out the header for the output file.
   */

  (void) fprintf(fp, "# %s\n", Vm_VisReadVersion());
  (void) fprintf(fp, "# partition name: %s\n", partitionName);
  (void) fprintf(fp, "# generated: %s", nowTxt);
  (void) fprintf(fp, "#\n");

  (void) fprintf(fp, "# Partition with %d vertices and %d edges\n",
                 lsLength(g_get_vertices(partition)),
                 lsLength(g_get_edges(partition)));

  (void) fprintf(fp, "digraph \"%s\" {\n  rotate=90;\n", partitionName);
  (void) fprintf(fp, "  margin=0.5;\n  label=\"%s\";\n", partitionName);
  (void) fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");


  vertexToId = st_init_table(st_ptrcmp, st_ptrhash);

  vertexId = 0;
  clusterId = 0;
  foreach_vertex(partition, gen, fromVertex) {
    if (PartVertexReadType(fromVertex) == Part_VertexCluster_c) {
      array_t *members = PartVertexReadClusterMembers(fromVertex);
      vertex_t *auxPtr;
      int i;

      (void) fprintf(fp, "  subgraph cluster%d {\n", clusterId++);
      (void) fprintf(fp, "    label = \"%s\";\n",
                     PartVertexReadName(fromVertex));
      arrayForEachItem(vertex_t *, members, i, auxPtr) {
        (void) fprintf(fp, "  ");
        st_insert(vertexToId, (char *)auxPtr, (char *)(long)vertexId);
        PrintVertexDescription(fp, auxPtr, vertexId++);
      }
      (void) fprintf(fp, "  }\n");
    } /* End of then */
    else if (!PartVertexTestIsClustered(fromVertex)) {
      st_insert(vertexToId, (char *)fromVertex, (char *)(long)vertexId);
      PrintVertexDescription(fp, fromVertex, vertexId++);
    }

  }

  foreach_edge(partition, gen, edgePtr) {
    fromVertex = g_e_source(edgePtr);
    toVertex = g_e_dest(edgePtr);

    st_lookup_int(vertexToId, (char *)fromVertex, &vertexId);
    (void) fprintf(fp, "  node%d -> ", vertexId);

    st_lookup_int(vertexToId, (char *)toVertex, &vertexId);
    (void) fprintf(fp, "node%d;\n", vertexId);
  } /* End of foreach_edge */

  (void) fprintf(fp, "}\n");

  st_free_table(vertexToId);

  return 1;
} /* End of PartPartitionPrint */


/**Function********************************************************************

  Synopsis    [Create latch nodes list and leave nodes list form
  CTL properties and fairness constraints]

  Comments    []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
PartGetLatchInputListFromCTL(
  Ntk_Network_t *network,
  array_t *ctlArray,
  array_t *fairArray,
  lsList  latchInputList)
{
  return PartGetLatchInputListFromCtlAndLtl(network, ctlArray, NIL(array_t),
                                            fairArray, latchInputList,
                                            FALSE);
}

/**Function********************************************************************

  Synopsis [Create latch inputs list form properties and fairness
  constraints]

  Comments [Return all the Cone-Of-Influence nodes if stopAtLatch is
  FALSE; otherwise, return only the nodes up to the immediate
  support.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
PartGetLatchInputListFromCtlAndLtl(
  Ntk_Network_t *network,
  array_t *ctlArray,
  array_t *ltlArray,
  array_t *fairArray,
  lsList  latchInputList,
  boolean stopAtLatch)
{
  int i;
  Ctlp_Formula_t  *ctlFormula;
  Ctlsp_Formula_t *ltlFormula;
  st_table *formulaNodes;
  st_generator *stGen;
  array_t *nodeArray;
  array_t *formulaCombNodes;
  Ntk_Node_t *node;


  formulaNodes = st_init_table( st_ptrcmp, st_ptrhash );

  if ( formulaNodes == NIL(st_table)){
    return 0;
  }

 /*
  * Extract nodes in CTL/LTL properties
  */
  if ( ctlArray != NIL(array_t)){
    arrayForEachItem( Ctlp_Formula_t *, ctlArray, i, ctlFormula ) {
      Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes );
    }
  }
  if ( ltlArray != NIL(array_t)){
    arrayForEachItem( Ctlsp_Formula_t *, ltlArray, i, ltlFormula ) {
      Mc_NodeTableAddLtlFormulaNodes( network, ltlFormula, formulaNodes );
    }
  }

 /*
  * Extract nodes in fairness properties
  */
  if ( fairArray != NIL(array_t)){
    arrayForEachItem( Ctlp_Formula_t *, fairArray, i, ctlFormula ) {
      Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes );
    }
  }

  nodeArray = array_alloc( Ntk_Node_t *, 0 );
  st_foreach_item( formulaNodes, stGen, &node, NULL) {
    array_insert_last( Ntk_Node_t *, nodeArray, node );
  }

  st_free_table( formulaNodes );

 /*
  * Get all combinational support nodes in network from formula nodes
  */
  formulaCombNodes = Ntk_NodeComputeCombinationalSupport( network,
                     nodeArray, stopAtLatch );
  array_free(nodeArray);
 /*
  * Root list includes latch data input nodes
  */
  arrayForEachItem( Ntk_Node_t *, formulaCombNodes, i, node ) {
    if ( Ntk_NodeTestIsLatch( node ) ) {
      Ntk_Node_t *tempNode = Ntk_LatchReadDataInput( node );
      lsNewEnd(latchInputList, (lsGeneric)tempNode, LS_NH);
    }
  }

  array_free(formulaCombNodes);

  return 1;
}

/**Function********************************************************************

  Synopsis [Create latch nodes list form properties and fairness
  constraints]

  Comments [Return all the Cone-Of-Influence nodes if stopAtLatch is
  FALSE; otherwise, return only the nodes up to the immediate
  support.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
PartGetLatchListFromCtlAndLtl(
  Ntk_Network_t *network,
  array_t *ctlArray,
  array_t *ltlArray,
  array_t *fairArray,
  lsList  latchInputList,
  boolean stopAtLatch)
{
  int i;
  Ctlp_Formula_t  *ctlFormula;
  Ctlsp_Formula_t *ltlFormula;
  st_table *formulaNodes;
  st_generator *stGen;
  array_t *nodeArray;
  array_t *formulaCombNodes;
  Ntk_Node_t *node;


  formulaNodes = st_init_table( st_ptrcmp, st_ptrhash );

  if ( formulaNodes == NIL(st_table)){
    return 0;
  }

 /*
  * Extract nodes in CTL/LTL properties
  */
  if ( ctlArray != NIL(array_t)){
    arrayForEachItem( Ctlp_Formula_t *, ctlArray, i, ctlFormula ) {
      Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes );
    }
  }
  if ( ltlArray != NIL(array_t)){
    arrayForEachItem( Ctlsp_Formula_t *, ltlArray, i, ltlFormula ) {
      Mc_NodeTableAddLtlFormulaNodes( network, ltlFormula, formulaNodes );
    }
  }

 /*
  * Extract nodes in fairness properties
  */
  if ( fairArray != NIL(array_t)){
    arrayForEachItem( Ctlp_Formula_t *, fairArray, i, ctlFormula ) {
      Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes );
    }
  }

  nodeArray = array_alloc( Ntk_Node_t *, 0 );
  st_foreach_item( formulaNodes, stGen, &node, NULL) {
    array_insert_last( Ntk_Node_t *, nodeArray, node );
  }

  st_free_table( formulaNodes );

 /*
  * Get all combinational support nodes in network from formula nodes
  */
  formulaCombNodes = Ntk_NodeComputeCombinationalSupport( network,
                     nodeArray, stopAtLatch );
  array_free(nodeArray);
 /*
  * Root list includes latch data input nodes
  */
  arrayForEachItem( Ntk_Node_t *, formulaCombNodes, i, node ) {
    if ( Ntk_NodeTestIsLatch( node ) ) {
      lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
    }
  }

  array_free(formulaCombNodes);

  return 1;
}

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Prints the declaration of a vertex in dot format.]

  SideEffects []

  SeeAlso     [Part_PartitionPrint]

******************************************************************************/
static void
PrintVertexDescription(
  FILE *fp,
  vertex_t *vertexPtr,
  int order)
{
  char *name = PartVertexReadName(vertexPtr);

  (void) fprintf(fp, "  node%d [label=", order);
  if (name != NIL(char)) {
    (void) fprintf(fp, "\"%s\"", name);
  }
  else {
    (void) fprintf(fp, "\"None\"");
  }
  (void) fprintf(fp, "]; \n");
} /* End of PrintVertexDescription */