# The ntr package (Internal)

##

###

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

    STRING_EQUAL(
       s1,
       s2
    )

  Returns 1 if the two arguments are identical strings.

  Side Effects none

Generated automatically by `extdoc` on 1010215