#include "partInt.h"

Include dependency graph for partPart.c:

Functions
static void	PrintVertexDescription (FILE fp, vertex_t vertexPtr, int order)
void	Part_PartitionFree (graph_t *partition)
void	Part_PartitionFreeCallback (void *data)
vertex_t *	Part_PartitionFindVertexByName (graph_t partition, char name)
vertex_t *	Part_PartitionFindVertexByMddId (graph_t *partition, int mddId)
char *	Part_PartitionReadName (graph_t *partition)
Part_PartitionMethod	Part_PartitionReadMethod (graph_t *partition)
char *	Part_PartitionObtainMethodAsString (graph_t *partition)
mdd_manager *	Part_PartitionReadMddManager (graph_t *partition)
Part_VertexType	Part_VertexReadType (vertex_t *vertexPtr)
char *	Part_VertexReadName (vertex_t *vertexPtr)
array_t *	Part_VertexReadClusterMembers (vertex_t *vertexPtr)
Mvf_Function_t *	Part_VertexReadFunction (vertex_t *vertexPtr)
void	Part_VertexSetFunction (vertex_t vertexPtr, Mvf_Function_t mvf)
int	Part_VertexReadMddId (vertex_t *vertexPtr)
boolean	Part_VertexTestIsClustered (vertex_t *vertexPtr)
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 *	Part_PartitionDuplicate (graph_t *partition)
graph_t *	Part_PartCreatePartitionWithCTL (Hrc_Manager_t *hmgr, Part_PartitionMethod method, int verbose, int sanityCheck, boolean inTermsOfLeaves, array_t ctlArray, 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)
int	Part_PartitionChangeRoots (Ntk_Network_t network, graph_t partition, lsList rootList, int verbosity)
graph_t *	Part_NetworkReadPartition (Ntk_Network_t *network)
vertex_t *	Part_PartitionCreateClusterVertex (graph_t partition, char name, array_t *arrayOfVertices)
void	Part_UpdatePartitionFrontier (Ntk_Network_t network, graph_t partition, lsList rootList, lsList leaveList, mdd_t *careSet)
void	Part_VertexInfoFreeCluster (vertex_t *vertexPtr)
boolean	Part_PartitionTestCompletelySp (graph_t partition, array_t roots, st_table *leaves)
boolean	Part_PartitionTestDeterministic (graph_t partition, array_t roots, st_table *leaves)
int	Part_PartitionGetLatchInputListFromCTL (Ntk_Network_t network, array_t ctlArray, array_t *fairArray, lsList latchInputList)
int	Part_PartitionGetLatchInputListFromCtlAndLtl (Ntk_Network_t network, array_t ctlArray, array_t ltlArray, array_t fairArray, lsList latchInputList, boolean stopAtLatch)
void	Part_PartitionPrintStats (FILE fp, graph_t partition, boolean printNodeNames)
PartPartitionInfo_t *	PartPartitionInfoCreate (char name, mdd_manager manager, Part_PartitionMethod method)
void	PartPartitionInfoFree (gGeneric partitionInfo)
PartVertexInfo_t *	PartVertexInfoCreateSingle (char name, Mvf_Function_t mvf, int mddId)
PartVertexInfo_t *	PartVertexInfoCreateCluster (char name, array_t vertexArray)
void	PartVertexInfoFree (gGeneric vertexInfo)
void	PartPartitionSanityCheck (graph_t *partition, int intensity)
st_table *	PartCreateFunctionSupportTable (Mvf_Function_t *mvf)
void	PartPartitionCreateVertexFaninEdges (graph_t partition, vertex_t vertexPtr)
int	PartPartitionPrint (FILE fp, graph_t partition)
int	PartGetLatchInputListFromCTL (Ntk_Network_t network, array_t ctlArray, array_t *fairArray, lsList latchInputList)
int	PartGetLatchInputListFromCtlAndLtl (Ntk_Network_t network, array_t ctlArray, array_t ltlArray, array_t fairArray, lsList latchInputList, boolean stopAtLatch)
int	PartGetLatchListFromCtlAndLtl (Ntk_Network_t network, array_t ctlArray, array_t ltlArray, array_t fairArray, lsList latchInputList, boolean stopAtLatch)
Variables
static char rcsid[]	UNUSED = "$Id: partPart.c,v 1.45 2009/04/11 01:47:18 fabio Exp $"

Function Documentation

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
	)

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.

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 careSet specifies which minterms in the input space are considered.

The nodes parameter is an optional list of nodes that may be specified in case the partial method is used. It represents the set of nodes in the network to be preserved when building the partition. The boolean variable inTermsOfLeaves is valid only in the case of the total 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.

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]

Definition at line 399 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

graph_t* Part_NetworkReadPartition ( Ntk_Network_t * network )

Function********************************************************************

Synopsis [Reads the partition attached to a network.]

SideEffects []

SeeAlso [CommandBuildPartitionMdds]

Definition at line 689 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

graph_t* Part_PartCreatePartitionWithCTL	(	Hrc_Manager_t **	hmgr,
		Part_PartitionMethod	method,
		int	verbose,
		int	sanityCheck,
		boolean	inTermsOfLeaves,
		array_t *	ctlArray,
		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 []

Definition at line 575 of file partPart.c.

{
  return Part_PartCreatePartitionWithCtlAndLtl(hmgr, method, verbose,
                                               sanityCheck, inTermsOfLeaves,
                                               ctlArray, NIL(array_t),
                                               fairArray);
}

Here is the call graph for this function:

Here is the caller graph for this function:

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
	)

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

Definition at line 603 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Part_PartitionChangeRoots	(	Ntk_Network_t *	network,
		graph_t *	partition,
		lsList	rootList,
		int	verbosity
	)

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

Definition at line 664 of file partPart.c.

{
  if (Part_PartitionReadMethod(partition) != Part_InOut_c){
    return 0;
  }

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

Here is the call graph for this function:

Here is the caller graph for this function:

vertex_t* Part_PartitionCreateClusterVertex	(	graph_t *	partition,
		char *	name,
		array_t *	arrayOfVertices
	)

Function********************************************************************

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

SideEffects []

SeeAlso [PartVertexInfo]

Definition at line 706 of file partPart.c.

{
  vertex_t *newVertex;

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

  return(newVertex);

} /* End of Part_PartitionCreateClusterVertex */

Here is the call graph for this function:

graph_t* Part_PartitionDuplicate ( graph_t * partition )

Function********************************************************************

Synopsis [Creates a duplicate of a partition.]

SideEffects []

SeeAlso [PartVertexInfo, PartPartitionInfo]

Definition at line 501 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

vertex_t* Part_PartitionFindVertexByMddId	(	graph_t *	partition,
		int	mddId
	)

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]

Definition at line 121 of file partPart.c.

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

Here is the caller graph for this function:

vertex_t* Part_PartitionFindVertexByName	(	graph_t *	partition,
		char *	name
	)

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]

Definition at line 93 of file partPart.c.

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

Here is the caller graph for this function:

void Part_PartitionFree ( graph_t * partition )

AutomaticEnd Function********************************************************************

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

SideEffects []

SeeAlso [PartPartitionInfoFree PartVertexInfoFree]

Definition at line 49 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void Part_PartitionFreeCallback ( void * data )

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]

Definition at line 73 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Part_PartitionGetLatchInputListFromCTL	(	Ntk_Network_t *	network,
		array_t *	ctlArray,
		array_t *	fairArray,
		lsList	latchInputList
	)

Function********************************************************************

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

Comments []

SideEffects [latchInputList is changed]

SeeAlso []

Definition at line 881 of file partPart.c.

{
  return PartGetLatchInputListFromCTL( network, ctlArray, fairArray,
                                       latchInputList);
}

Here is the call graph for this function:

Here is the caller graph for this function:

int Part_PartitionGetLatchInputListFromCtlAndLtl	(	Ntk_Network_t *	network,
		array_t *	ctlArray,
		array_t *	ltlArray,
		array_t *	fairArray,
		lsList	latchInputList,
		boolean	stopAtLatch
	)

Function********************************************************************

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

Comments []

SideEffects [latchInputList is changed]

SeeAlso []

Definition at line 904 of file partPart.c.

{
  return PartGetLatchInputListFromCtlAndLtl( network, ctlArray, ltlArray,
                                             fairArray,
                                             latchInputList, stopAtLatch);
}

Here is the call graph for this function:

char* Part_PartitionObtainMethodAsString ( graph_t * partition )

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]

Definition at line 188 of file partPart.c.

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

Here is the caller graph for this function:

void Part_PartitionPrintStats	(	FILE *	fp,
		graph_t *	partition,
		boolean	printNodeNames
	)

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]

Definition at line 930 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

mdd_manager* Part_PartitionReadMddManager ( graph_t * partition )

Function********************************************************************

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

SideEffects []

SeeAlso [PartPartitionInfo]

Definition at line 232 of file partPart.c.

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

Here is the caller graph for this function:

Part_PartitionMethod Part_PartitionReadMethod ( graph_t * partition )

Function********************************************************************

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

SideEffects []

SeeAlso [PartPartitionInfo]

Definition at line 162 of file partPart.c.

{
  Part_PartitionMethod  method;

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

Here is the caller graph for this function:

char* Part_PartitionReadName ( graph_t * partition )

Function********************************************************************

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

SideEffects []

SeeAlso [PartPartitionInfo]

Definition at line 146 of file partPart.c.

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

boolean Part_PartitionTestCompletelySp	(	graph_t *	partition,
		array_t *	roots,
		st_table *	leaves
	)

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]

Definition at line 785 of file partPart.c.

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

Here is the call graph for this function:

boolean Part_PartitionTestDeterministic	(	graph_t *	partition,
		array_t *	roots,
		st_table *	leaves
	)

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]

Definition at line 834 of file partPart.c.

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

Here is the call graph for this function:

void Part_UpdatePartitionFrontier	(	Ntk_Network_t *	network,
		graph_t *	partition,
		lsList	rootList,
		lsList	leaveList,
		mdd_t *	careSet
	)

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]

Definition at line 738 of file partPart.c.

{
  PartUpdateFrontier(network, partition, rootList, leaveList, careSet);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Part_VertexInfoFreeCluster ( vertex_t * vertexPtr )

Function********************************************************************

Synopsis [Removes a cluster vertex from the partition.]

SideEffects []

SeeAlso [PartVertexInfo]

Definition at line 758 of file partPart.c.

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

Here is the call graph for this function:

array_t* Part_VertexReadClusterMembers ( vertex_t * vertexPtr )

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]

Definition at line 283 of file partPart.c.

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

Here is the caller graph for this function:

Mvf_Function_t* Part_VertexReadFunction ( vertex_t * vertexPtr )

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]

Definition at line 302 of file partPart.c.

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

Here is the caller graph for this function:

int Part_VertexReadMddId ( vertex_t * vertexPtr )

Function********************************************************************

Synopsis [Reads the MddId attached to a vertex.]

SideEffects []

SeeAlso [PartVertexInfo]

Definition at line 339 of file partPart.c.

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

Here is the caller graph for this function:

char* Part_VertexReadName ( vertex_t * vertexPtr )

Function********************************************************************

Synopsis [Reads the name attached to a vertex.]

SideEffects []

SeeAlso [PartVertexInfo]

Definition at line 264 of file partPart.c.

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

Here is the caller graph for this function:

Part_VertexType Part_VertexReadType ( vertex_t * vertexPtr )

Function********************************************************************

Synopsis [Returns the type of a vertex.]

SideEffects []

SeeAlso [PartVertexInfo Part_VertexType]

Definition at line 248 of file partPart.c.

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

void Part_VertexSetFunction	(	vertex_t *	vertexPtr,
		Mvf_Function_t *	mvf
	)

Function********************************************************************

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

SideEffects []

SeeAlso [PartVertexInfo]

Definition at line 319 of file partPart.c.

{
  assert(PartVertexReadType(vertexPtr) != Part_VertexCluster_c);

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

Here is the caller graph for this function:

boolean Part_VertexTestIsClustered ( vertex_t * vertexPtr )

Function********************************************************************

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

SideEffects []

SeeAlso [PartVertexInfo Part_VertexReadType]

Definition at line 355 of file partPart.c.

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

st_table* PartCreateFunctionSupportTable ( Mvf_Function_t * mvf )

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]

Definition at line 1271 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int PartGetLatchInputListFromCTL	(	Ntk_Network_t *	network,
		array_t *	ctlArray,
		array_t *	fairArray,
		lsList	latchInputList
	)

Function********************************************************************

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

Comments []

SideEffects []

SeeAlso []

Definition at line 1451 of file partPart.c.

{
  return PartGetLatchInputListFromCtlAndLtl(network, ctlArray, NIL(array_t),
                                            fairArray, latchInputList,
                                            FALSE);
}

Here is the call graph for this function:

Here is the caller graph for this function:

int PartGetLatchInputListFromCtlAndLtl	(	Ntk_Network_t *	network,
		array_t *	ctlArray,
		array_t *	ltlArray,
		array_t *	fairArray,
		lsList	latchInputList,
		boolean	stopAtLatch
	)

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

Definition at line 1477 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int PartGetLatchListFromCtlAndLtl	(	Ntk_Network_t *	network,
		array_t *	ctlArray,
		array_t *	ltlArray,
		array_t *	fairArray,
		lsList	latchInputList,
		boolean	stopAtLatch
	)

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

Definition at line 1567 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void PartPartitionCreateVertexFaninEdges	(	graph_t *	partition,
		vertex_t *	vertexPtr
	)

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

Definition at line 1315 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

PartPartitionInfo_t* PartPartitionInfoCreate	(	char *	name,
		mdd_manager *	manager,
		Part_PartitionMethod	method
	)

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]

Definition at line 1013 of file partPart.c.

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

Here is the caller graph for this function:

void PartPartitionInfoFree ( gGeneric partitionInfo )

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]

Definition at line 1042 of file partPart.c.

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

Here is the caller graph for this function:

int PartPartitionPrint	(	FILE *	fp,
		graph_t *	partition
	)

Function********************************************************************

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

Description [ The format used for printing is dot, a tool for graph visualization developed at AT&T. It can be obtained from http://www.research.att.com/orgs/ssr/book/reuse. 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 []

Definition at line 1358 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void PartPartitionSanityCheck	(	graph_t *	partition,
		int	intensity
	)

Function********************************************************************

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

SideEffects []

SeeAlso [PartPartitionInfo]

Definition at line 1171 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

PartVertexInfo_t* PartVertexInfoCreateCluster	(	char *	name,
		array_t *	vertexArray
	)

Function********************************************************************

Synopsis [Creates a cluster vertex in the partition.]

SideEffects []

SeeAlso [PartVertexInfo]

Definition at line 1092 of file partPart.c.

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

Here is the caller graph for this function:

PartVertexInfo_t* PartVertexInfoCreateSingle	(	char *	name,
		Mvf_Function_t *	mvf,
		int	mddId
	)

Function********************************************************************

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

SideEffects []

SeeAlso [PartVertexInfo]

Definition at line 1065 of file partPart.c.

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

Here is the caller graph for this function:

void PartVertexInfoFree ( gGeneric vertexInfo )

Function********************************************************************

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

SideEffects []

SeeAlso [PartVertexInfo]

Definition at line 1135 of file partPart.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static void PrintVertexDescription	(	FILE *	fp,
		vertex_t *	vertexPtr,
		int	order
	)		`[static]`

AutomaticStart

Function********************************************************************

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

SideEffects []

SeeAlso [Part_PartitionPrint]

Definition at line 1656 of file partPart.c.

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

Here is the caller graph for this function:

Variable Documentation

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

CFile************************************************************************

FileName [partPart.c]

PackageName [part]

Synopsis [Routines to initialize the command build_partition_mdds, 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.]

Definition at line 22 of file partPart.c.

src/part/partPart.c File Reference

Functions

Variables

Function Documentation

Variable Documentation