The ntr package

Simple-minded package to do traversal.

• External abstracts

• All abstracts

• External functions

• All functions

int 
Ntr_ClosureTrav(
  DdManager * dd, DD manager
  BnetNetwork * net, network
  NtrOptions * option options
)

Traversal procedure. based on the transitive closure of the transition relation. Returns 1 in case of success; 0 otherwise.

Side Effects None

See Also Ntr_Trav

int 
Ntr_Envelope(
  DdManager * dd, DD manager
  NtrPartTR * TR, transition relation
  FILE * dfp, pointer to file for DD dump
  NtrOptions * option program options
)

Poor man's outer envelope computation based on the monolithic transition relation. Returns 1 in case of success; 0 otherwise.

Side Effects None

void 
Ntr_FreeHeap(
  NtrHeap * heap 
)

Frees a priority queue.

Side Effects None

See Also Ntr_InitHeap

NtrHeap * 
Ntr_HeapClone(
  NtrHeap * source 
)

Clones a priority queue.

Side Effects None

See Also Ntr_InitHeap

int 
Ntr_HeapCount(
  NtrHeap * heap 
)

Returns the number of items in a priority queue.

Side Effects None

int 
Ntr_HeapExtractMin(
  NtrHeap * heap, 
  void ** item, 
  int * key 
)

Extracts the element with the minimum key from a priority queue. Returns 1 if successful; 0 otherwise.

Side Effects The minimum key and the associated item are returned as side effects.

See Also Ntr_HeapInsert

int 
Ntr_HeapInsert(
  NtrHeap * heap, 
  void * item, 
  int  key 
)

Inserts an item in a priority queue. Returns 1 if successful; 0 otherwise.

Side Effects None

See Also Ntr_HeapExtractMin

NtrHeap * 
Ntr_InitHeap(
  int  size 
)

Initializes a priority queue. Returns a pointer to the heap if successful; NULL otherwise.

Side Effects None

See Also Ntr_FreeHeap

int 
Ntr_SCC(
  DdManager * dd, DD manager
  BnetNetwork * net, network
  NtrOptions * option options
)

Computes the strongly connected components of the state transition graph. Only the first 10 SCCs are computed. Returns 1 in case of success; 0 otherwise.

Side Effects None

See Also Ntr_Trav

int 
Ntr_ShortestPaths(
  DdManager * dd, 
  BnetNetwork * net, 
  NtrOptions * option 
)

Computes shortest paths in the state transition graph of a network. Three methods are availabe:

• Bellman-Ford algorithm for single-source shortest paths; the algorithm computes the distance (number of transitions) from the initial states to all states.
• Floyd-Warshall algorithm for all-pair shortest paths.
• Repeated squaring algorithm for all-pair shortest paths.

The function returns 1 in case of success; 0 otherwise.

Side Effects ADD variables are created in the manager.

int 
Ntr_TestClipping(
  DdManager * dd, 
  BnetNetwork * net1, 
  BnetNetwork * net2, 
  NtrOptions * option 
)

Tests BDD clipping functions. Returns 1 if successful; 0 otherwise.

Side Effects None

int 
Ntr_TestClosestCube(
  DdManager * dd, 
  BnetNetwork * net, 
  NtrOptions * option 
)

Tests the Cudd_bddClosestCube function. Returns 1 if successful; 0 otherwise.

Side Effects None

int 
Ntr_TestCofactorEstimate(
  DdManager * dd, 
  BnetNetwork * net, 
  NtrOptions * option 
)

Tests BDD cofactor estimate functions. Returns 1 if successful; 0 otherwise.

Side Effects None

int 
Ntr_TestDecomp(
  DdManager * dd, 
  BnetNetwork * net1, 
  NtrOptions * option 
)

Tests BDD decomposition functions. Returns 1 if successful; 0 otherwise.

Side Effects None

int 
Ntr_TestDensity(
  DdManager * dd, 
  BnetNetwork * net1, 
  NtrOptions * option 
)

Tests BDD density-related functions. Returns 1 if successful; 0 otherwise.

Side Effects None

int 
Ntr_TestEquivAndContain(
  DdManager * dd, 
  BnetNetwork * net1, 
  BnetNetwork * net2, 
  NtrOptions * option 
)

Tests functions for BDD equivalence and containment with don't cares, including Cudd_EquivDC and Cudd_bddLeqUnless. This function uses as care set the first output of net2 and checkes equivalence and containment for of all the output pairs of net1. Returns 1 if successful; 0 otherwise.

Side Effects None

int 
Ntr_TestHeap(
  NtrHeap * heap, 
  int  i 
)

Tests the heap property of a priority queue. Returns 1 if Successful; 0 otherwise.

Side Effects None

int 
Ntr_TestMinimization(
  DdManager * dd, 
  BnetNetwork * net1, 
  BnetNetwork * net2, 
  NtrOptions * option 
)

Tests BDD minimization functions, including leaf-identifying compaction, squeezing, and restrict. This function uses as constraint the first output of net2 and computes positive and negative cofactors of all the outputs of net1. For each cofactor, it checks whether compaction was safe (cofactor not larger than original function) and that the expansion based on each minimization function (used as a generalized cofactor) equals the original function. Returns 1 if successful; 0 otherwise.

Side Effects None

DdNode * 
Ntr_TransitiveClosure(
  DdManager * dd, 
  NtrPartTR * TR, 
  NtrOptions * option 
)

Builds the transitive closure of a transition relation. Returns a BDD if successful; NULL otherwise. Uses a simple squaring algorithm.

Side Effects None

int 
Ntr_Trav(
  DdManager * dd, DD manager
  BnetNetwork * net, network
  NtrOptions * option options
)

Poor man's traversal procedure. based on the monolithic transition relation. Returns 1 in case of success; 0 otherwise.

Side Effects None

See Also Ntr_ClosureTrav

int 
Ntr_VerifyEquivalence(
  DdManager * dd, 
  BnetNetwork * net1, 
  BnetNetwork * net2, 
  NtrOptions * option 
)

Verify equivalence of combinational networks. Returns 1 if successful and if the networks are equivalent; -1 if successful, but the networks are not equivalent; 0 otherwise. The two networks are supposed to have the same names for inputs and outputs. The only exception is that the second network may miss output buffers that are present in the first network. This function tries to match both the output and the input of the buffer.

Side Effects None

int 
Ntr_buildDDs(
  BnetNetwork * net, network for which DDs are to be built
  DdManager * dd, DD manager
  NtrOptions * option, option structure
  BnetNetwork * net2 companion network with which inputs may be shared
)

Builds DDs for a network outputs and next state functions. The method is really brain-dead, but it is very simple. Returns 1 in case of success; 0 otherwise. Some inputs to the network may be shared with another network whose DDs have already been built. In this case we want to share the DDs as well.

Side Effects the dd fields of the network nodes are modified. Uses the count fields of the nodes.

NtrPartTR * 
Ntr_buildTR(
  DdManager * dd, manager
  BnetNetwork * net, network
  NtrOptions * option, options
  int  image image type: monolithic ...
)

Builds the transition relation for a network. Returns a pointer to the transition relation structure if successful; NULL otherwise.

Side Effects None

NtrPartTR * 
Ntr_cloneTR(
  NtrPartTR * TR 
)

Makes a copy of a transition relation. Returns a pointer to the copy if successful; NULL otherwise.

Side Effects None

See Also Ntr_buildTR Ntr_freeTR

void 
Ntr_freeTR(
  DdManager * dd, 
  NtrPartTR * TR 
)

Frees the transition relation for a network.

Side Effects None

DdNode * 
Ntr_getStateCube(
  DdManager * dd, 
  BnetNetwork * net, 
  char * filename, 
  int  pr 
)

Reads a state cube from a file or create a random one. Returns a pointer to the BDD of the sink nodes if successful; NULL otherwise.

Side Effects None

DdNode * 
Ntr_initState(
  DdManager * dd, 
  BnetNetwork * net, 
  NtrOptions * option 
)

Builds the BDD of the initial state(s). Returns a BDD if successful; NULL otherwise.

Side Effects None

int 
Ntr_maxflow(
  DdManager * dd, 
  BnetNetwork * net, 
  NtrOptions * option 
)

Maximum 0-1 flow between source and sink states. Returns 1 in case of success; 0 otherwise.

Side Effects Creates two new sets of variables.

double 
Ntr_maximum01Flow(
  DdManager * bdd, manager
  DdNode * sx, source node
  DdNode * ty, sink node
  DdNode * E, edge relation
  DdNode ** F, flow relation
  DdNode ** cut, cutset relation
  DdNode ** x, array of row variables
  DdNode ** y, array of column variables
  DdNode ** z, arrays of auxiliary variables
  int  n, number of variables in each array
  int  pr verbosity level
)

This function implements Dinits's algorithm for (0-1) max flow, using BDDs and a symbolic technique to trace multiple edge-disjoint augmenting paths to complete a phase. The outer forever loop is over phases, and the inner forever loop is to propagate a (not yet) maximal flow of edge-disjoint augmenting paths from one layer to the previous. The subprocedure call implements a least fixed point iteration to compute a (not yet) maximal flow update between layers. At the end of each phase (except the last one) the flow is actually pushed from the source to the sink. Data items:

• sx(ty) BDD representations of s(t).
• x(y) The variables encoding the from(to)-node u(v) of an edge (u,v) in the given digraph.
• z Another set of variables.
• E(x,y) The edge relation.
• F(x,y) BDD representation of the current flow, initialized to 0 for each arc, and updated by +1, -1, or 0 at the end of each phase.
• Ms Mt The maximum flow, that is, the cardinality of a minimum cut, measured at the source and at the sink, respectively. The two values should be identical.
• reached The set of nodes already visited in the BFS of the digraph.
• fos fanout of the source node s.
• fit fanin of the sink node t.

Side Effects The flow realtion F and the cutset relation cut are returned as side effects.

int 
Ntr_testISOP(
  DdManager * dd, 
  BnetNetwork * net, 
  NtrOptions * option 
)

Builds ZDD covers.

Side Effects Creates ZDD variables in the manager.

int 
Ntr_testZDD(
  DdManager * dd, 
  BnetNetwork * net, 
  NtrOptions * option 
)

Tests ZDDs. Returns 1 if successful; 0 otherwise.

Side Effects Creates ZDD variables in the manager.