src/part/partPart.c

Go to the documentation of this file.

#include "partInt.h"

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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


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

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


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

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

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

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


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);
}

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;
}


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);
}


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


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

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

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

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

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

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

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);
}

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

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

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

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

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

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

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

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

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

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


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

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;
}

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


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