A set of internal low-level routines of the dddmp package doing: 

static Dddmp_Hdr_t * 
DddmpBddReadHeaderCnf(
  char * file, IN: file name
  FILE * fp IN: file pointer
)
Reads the header of a dump file. Builds a Dddmp_Hdr_t struct containing all infos in the header, for next manipulations.

Side Effects none

Defined in dddmpLoadCnf.c 

static Dddmp_Hdr_t * 
DddmpBddReadHeader(
  char * file, IN: file name
  FILE * fp IN: file pointer
)
Reads the header of a dump file. Builds a Dddmp_Hdr_t struct containing all infos in the header, for next manipulations.

Side Effects none

Defined in dddmpLoad.c 

void 
DddmpClearVisitedAdd(
  DdNode * f IN: BDD node to be marked (as not visited)
)
Marks a node as not visited

Side Effects None

See Also DddmpVisitedAdd () DddmpSetVisitedAdd ()
Defined in dddmpNodeAdd.c 

void 
DddmpClearVisitedBdd(
  DdNode * f IN: BDD node to be marked (as not visited)
)
Marks a node as not visited

Side Effects None

See Also DddmpVisited () DddmpSetVisited ()
Defined in dddmpNodeBdd.c 

static int 
DddmpClearVisitedCnfRecur(
  DdNode * f IN: root of the BDD to be marked
)
Mark ALL nodes as not visited (it recurs on the node children)

Side Effects None

See Also DddmpVisitedCnf () DddmpSetVisitedCnf ()
Defined in dddmpDdNodeCnf.c 

static int 
DddmpClearVisitedCnfRecur(
  DdNode * f IN: root of the BDD to be marked
)
Mark ALL nodes as not visited (it recurs on the node children)

Side Effects None

See Also DddmpVisitedCnf () DddmpSetVisitedCnf ()
Defined in dddmpNodeCnf.c 

static void 
DddmpClearVisitedCnf(
  DdNode * f IN: BDD node to be marked (as not visited)
)
Marks a node as not visited

Side Effects None

See Also DddmpVisitedCnf () DddmpSetVisitedCnf ()
Defined in dddmpDdNodeCnf.c 

static void 
DddmpClearVisitedCnf(
  DdNode * f IN: BDD node to be marked (as not visited)
)
Marks a node as not visited

Side Effects None

See Also DddmpVisitedCnf () DddmpSetVisitedCnf ()
Defined in dddmpNodeCnf.c 

void 
DddmpClearVisited(
  DdNode * f IN: BDD node to be marked (as not visited)
)
Marks a node as not visited

Side Effects None

See Also DddmpVisited () DddmpSetVisited ()
Defined in dddmpDdNodeBdd.c 

static int 
DddmpCnfClauses2Bdd(
  Dddmp_Hdr_t * Hdr, IN: file header
  DdManager * ddMgr, IN: DD Manager
  int ** cnfTable, IN: CNF table for clauses
  int  mode, IN: computation mode
  DdNode *** rootsPtrPtr OUT: array of returned BDD roots (by reference)
)
Transforms CNF clauses into BDDs. Clauses are stored in an internal structure previously read. The results can be given in different format according to the mode selection: IFF mode == 0 Return the Clauses without Conjunction IFF mode == 1 Return the sets of BDDs without Quantification IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification

Defined in dddmpLoadCnf.c 

static int 
DddmpCuddBddArrayStoreCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDD roots to be stored
  int  rootN, IN: # of output BDD roots to be stored
  Dddmp_DecompCnfStoreType  mode, IN: format selection
  int  noHeader, IN: do not store header iff 1
  char ** varNames, IN: array of variable names (or NULL)
  int * bddIds, IN: array of BDD node Ids (or NULL)
  int * bddAuxIds, IN: array of BDD Aux Ids (or NULL)
  int * cnfIds, IN: array of CNF ids (or NULL)
  int  idInitial, IN: starting id for cutting variables
  int  edgeInTh, IN: Max # Incoming Edges
  int  pathLengthTh, IN: Max Path Length
  char * fname, IN: file name
  FILE * fp, IN: pointer to the store file
  int * clauseNPtr, OUT: number of clause stored
  int * varNewNPtr OUT: number of new variable created
)
Dumps the argument array of BDDs/ADDs to file in CNF format. The following arrays: varNames, bddIds, bddAuxIds, and cnfIds fix the correspondence among variable names, BDD ids, BDD auxiliary ids and the ids used to store the CNF problem. All these arrays are automatically created iff NULL. Auxiliary variable, iff necessary, are created starting from value idInitial. Iff idInitial is <= 0 its value is selected as the number of internal CUDD variable + 2. Auxiliary variables, i.e., cut points are inserted following these criterias: * edgeInTh indicates the maximum number of incoming edges up to which no cut point (auxiliary variable) is inserted. If edgeInTh: * is equal to -1 no cut point due to incoming edges are inserted (MaxtermByMaxterm method.) * is equal to 0 a cut point is inserted for each node with a single incoming edge, i.e., each node, (NodeByNode method). * is equal to n a cut point is inserted for each node with (n+1) incoming edges. * pathLengthTh indicates the maximum length path up to which no cut points (auxiliary variable) is inserted. If the path length between two nodes exceeds this value, a cut point is inserted. If pathLengthTh: * is equal to -1 no cut point due path length are inserted (MaxtermByMaxterm method.) * is equal to 0 a cut point is inserted for each node (NodeByNode method). * is equal to n a cut point is inserted on path whose length is equal to (n+1). Notice that the maximum number of literals in a clause is equal to (pathLengthTh + 2), i.e., for each path we have to keep into account a CNF variable for each node plus 2 added variables for the bottom and top-path cut points.

Side Effects Nodes are temporarily removed from the unique hash table. They are re-linked after the store operation in a modified order.

See Also Dddmp_cuddBddStore
Defined in dddmpStoreCnf.c 

int 
DddmpCuddBddArrayStore(
  Dddmp_DecompType  ddType, IN: Selects the decomp type BDD
  DdManager * ddMgr, IN: DD Manager
  char * ddname, IN: DD name (or NULL)
  int  nRoots, IN: number of output BDD roots to be stored
  DdNode ** f, IN: array of DD roots to be stored
  char ** rootnames, IN: array of root names (or NULL)
  char ** varnames, IN: array of variable names (or NULL)
  int * auxids, IN: array of converted var IDs
  int  mode, IN: storing mode selector
  Dddmp_VarInfoType  varinfo, IN: extra info for variables in text mode
  char * fname, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument array of BDDs to file. Internal function doing inner steps of store for BDDs.

Side Effects Nodes are temporarily removed from the unique hash table. They are re-linked after the store operation in a modified order.

See Also Dddmp_cuddBddStore Dddmp_cuddBddLoad Dddmp_cuddBddArrayLoad
Defined in dddmpStoreBdd.c 

static int 
DddmpCuddDdArrayLoadCnf(
  DdManager * ddMgr, IN: DD Manager
  Dddmp_RootMatchType  rootmatchmode, IN: storing mode selector
  char ** rootmatchnames, IN: sorted names for loaded roots
  Dddmp_VarMatchType  varmatchmode, IN: storing mode selector
  char ** varmatchnames, IN: array of variable names, by ids
  int * varmatchauxids, IN: array of variable auxids, by ids
  int * varcomposeids, IN: array of new ids, by ids
  int  mode, IN: computation mode
  char * file, IN: file name
  FILE * fp, IN: file pointer
  DdNode *** rootsPtrPtr, OUT: array of BDD roots
  int * nRoots OUT: number of BDDs returned
)
Reads a dump file representing the argument BDDs in CNF format. IFF mode == 0 Return the Clauses without Conjunction IFF mode == 1 Return the sets of BDDs without Quantification IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification

Side Effects A vector of pointers to DD nodes is allocated and freed.

See Also Dddmp_cuddBddArrayLoad
Defined in dddmpLoadCnf.c 

static int 
DddmpCuddDdArrayLoad(
  Dddmp_DecompType  ddType, IN: Selects decomp type
  DdManager * ddMgr, IN: DD Manager
  Dddmp_RootMatchType  rootMatchMode, IN: storing mode selector
  char ** rootmatchnames, IN: sorted names for loaded roots
  Dddmp_VarMatchType  varMatchMode, IN: storing mode selector
  char ** varmatchnames, IN: array of variable names, by ids
  int * varmatchauxids, IN: array of variable auxids, by ids
  int * varcomposeids, IN: array of new ids, by ids
  int  mode, IN: requested input file format
  char * file, IN: file name
  FILE * fp, IN: file pointer
  DdNode *** pproots OUT: array BDD roots (by reference)
)
Reads a dump file representing the argument BDDs. The header is common to both text and binary mode. The node list is either in text or binary format. A dynamic vector of DD pointers is allocated to support conversion from DD indexes to pointers. Several criteria are supported for variable match between file and dd manager. Several changes/permutations/compositions are allowed for variables while loading DDs. Variable of the dd manager are allowed to match with variables on file on ids, permids, varnames, varauxids; also direct composition between ids and composeids is supported. More in detail:
  1. varMatchMode=DDDMP_VAR_MATCHIDS

    allows the loading of a DD keeping variable IDs unchanged (regardless of the variable ordering of the reading manager); this is useful, for example, when swapping DDs to file and restoring them later from file, after possible variable reordering activations.

  2. varMatchMode=DDDMP_VAR_MATCHPERMIDS

    is used to allow variable match according to the position in the ordering.

  3. varMatchMode=DDDMP_VAR_MATCHNAMES

    requires a non NULL varmatchnames parameter; this is a vector of strings in one-to-one correspondence with variable IDs of the reading manager. Variables in the DD file read are matched with manager variables according to their name (a non NULL varnames parameter was required while storing the DD file).

  4. varMatchMode=DDDMP_VAR_MATCHIDS

    has a meaning similar to DDDMP_VAR_MATCHNAMES, but integer auxiliary IDs are used instead of strings; the additional non NULL varmatchauxids parameter is needed.

  5. varMatchMode=DDDMP_VAR_COMPOSEIDS

    uses the additional varcomposeids parameter is used as array of variable ids to be composed with ids stored in file.

In the present implementation, the array varnames (3), varauxids (4) and composeids (5) need to have one entry for each variable in the DD manager (NULL pointers are allowed for unused variables in varnames). Hence variables need to be already present in the manager. All arrays are sorted according to IDs.

Side Effects A vector of pointers to DD nodes is allocated and freed.

See Also Dddmp_cuddBddArrayStore
Defined in dddmpLoad.c 

int 
DddmpCuddDdArrayStoreBdd(
  Dddmp_DecompType  ddType, IN: Selects the decomp type: BDD or ADD
  DdManager * ddMgr, IN: DD Manager
  char * ddname, IN: DD name (or NULL)
  int  nRoots, IN: number of output BDD roots to be stored
  DdNode ** f, IN: array of DD roots to be stored
  char ** rootnames, IN: array of root names (or NULL)
  char ** varnames, IN: array of variable names (or NULL)
  int * auxids, IN: array of converted var IDs
  int  mode, IN: storing mode selector
  Dddmp_VarInfoType  varinfo, IN: extra info for variables in text mode
  char * fname, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument array of BDDs/ADDs to file. Internal function doing inner steps of store for BDDs and ADDs. ADD store is presently supported only with the text format.

Side Effects Nodes are temporarily removed from the unique hash table. They are re-linked after the store operation in a modified order.

See Also Dddmp_cuddBddStore Dddmp_cuddBddLoad Dddmp_cuddBddArrayLoad
Defined in dddmpStoreAdd.c 

static int 
DddmpCuddDdArrayStoreBlifBody(
  DdManager * ddMgr, IN: Manager
  int  n, IN: Number of output nodes to be dumped
  DdNode ** f, IN: Array of output nodes to be dumped
  char ** inputNames, IN: Array of input names (or NULL)
  char ** outputNames, IN: Array of output names (or NULL)
  FILE * fp IN: Pointer to the dump file
)
Writes a blif body representing the argument BDDs as a network of multiplexers. One multiplexer is written for each BDD node. It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file system full, or an ADD with constants different from 0 and 1). DddmpCuddDdArrayStoreBlif does not close the file: This is the caller responsibility. DddmpCuddDdArrayStoreBlif uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inputNames is non-null, it is assumed to hold the pointers to the names of the inputs. Similarly for outputNames. This function prints out only .names part.

Side Effects None

Defined in dddmpStoreMisc.c 

static int 
DddmpCuddDdArrayStoreBlifStep(
  DdManager * ddMgr, 
  DdNode * f, 
  FILE * fp, 
  st_table * visited, 
  char ** names 
)
Performs the recursive step of DddmpCuddDdArrayStoreBlif. Traverses the BDD f and writes a multiplexer-network description to the file pointed by fp in blif format. f is assumed to be a regular pointer and DddmpCuddDdArrayStoreBlifStep guarantees this assumption in the recursive calls.

Side Effects None

Defined in dddmpStoreMisc.c 

static int 
DddmpCuddDdArrayStoreBlif(
  DdManager * ddMgr, IN: Manager
  int  n, IN: Number of output nodes to be dumped
  DdNode ** f, IN: Array of output nodes to be dumped
  char ** inputNames, IN: Array of input names (or NULL)
  char ** outputNames, IN: Array of output names (or NULL)
  char * modelName, IN: Model name (or NULL)
  FILE * fp IN: Pointer to the dump file
)
Writes a blif file representing the argument BDDs as a network of multiplexers. One multiplexer is written for each BDD node. It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file system full, or an ADD with constants different from 0 and 1). DddmpCuddDdArrayStoreBlif does not close the file: This is the caller responsibility. DddmpCuddDdArrayStoreBlif uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inames is non-null, it is assumed to hold the pointers to the names of the inputs. Similarly for outputNames. It prefixes the string "NODE" to each nome to have "regular" names for each elements.

Side Effects None

See Also DddmpCuddDdArrayStoreBlifBody Cudd_DumpBlif
Defined in dddmpStoreMisc.c 

static int 
DddmpCuddDdArrayStorePrefixBody(
  DdManager * ddMgr, IN: Manager
  int  n, IN: Number of output nodes to be dumped
  DdNode ** f, IN: Array of output nodes to be dumped
  char ** inputNames, IN: Array of input names (or NULL)
  char ** outputNames, IN: Array of output names (or NULL)
  FILE * fp IN: Pointer to the dump file
)
One multiplexer is written for each BDD node. It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file system full, or an ADD with constants different from 0 and 1). It does not close the file: This is the caller responsibility. It uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inputNames is non-null, it is assumed to hold the pointers to the names of the inputs. Similarly for outputNames. For each BDD node of function f, variable v, then child T, and else child E it stores: f = v * T + v' * E that is (OR f (AND v T) (AND (NOT v) E)) If E is a complemented child this results in the following (OR f (AND v T) (AND (NOT v) (NOT E)))

Side Effects None

See Also DddmpCuddDdArrayStoreBlif
Defined in dddmpStoreMisc.c 

static int 
DddmpCuddDdArrayStorePrefixStep(
  DdManager * ddMgr, 
  DdNode * f, 
  FILE * fp, 
  st_table * visited, 
  char ** names 
)
Performs the recursive step of DddmpCuddDdArrayStorePrefixBody. Traverses the BDD f and writes a multiplexer-network description to the file pointed by fp. For each BDD node of function f, variable v, then child T, and else child E it stores: f = v * T + v' * E that is (OR f (AND v T) (AND (NOT v) E)) If E is a complemented child this results in the following (OR f (AND v T) (AND (NOT v) (NOT E))) f is assumed to be a regular pointer and the function guarantees this assumption in the recursive calls.

Side Effects None

Defined in dddmpStoreMisc.c 

static int 
DddmpCuddDdArrayStorePrefix(
  DdManager * ddMgr, IN: Manager
  int  n, IN: Number of output nodes to be dumped
  DdNode ** f, IN: Array of output nodes to be dumped
  char ** inputNames, IN: Array of input names (or NULL)
  char ** outputNames, IN: Array of output names (or NULL)
  char * modelName, IN: Model name (or NULL)
  FILE * fp IN: Pointer to the dump file
)
One multiplexer is written for each BDD node. It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file system full, or an ADD with constants different from 0 and 1). It does not close the file: This is the caller responsibility. It uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inputNames is non-null, it is assumed to hold the pointers to the names of the inputs. Similarly for outputNames. For each BDD node of function f, variable v, then child T, and else child E it stores: f = v * T + v' * E that is (OR f (AND v T) (AND (NOT v) E)) If E is a complemented child this results in the following (OR f (AND v T) (AND (NOT v) (NOT E))) Comments (COMMENT) are added at the beginning of the description to describe inputs and outputs of the design. A buffer (BUF) is add on the output to cope with complemented functions.

Side Effects None

See Also DddmpCuddDdArrayStoreBlif
Defined in dddmpStoreMisc.c 

static int 
DddmpCuddDdArrayStoreSmvBody(
  DdManager * ddMgr, IN: Manager
  int  n, IN: Number of output nodes to be dumped
  DdNode ** f, IN: Array of output nodes to be dumped
  char ** inputNames, IN: Array of input names (or NULL)
  char ** outputNames, IN: Array of output names (or NULL)
  FILE * fp IN: Pointer to the dump file
)
One multiplexer is written for each BDD node. It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file system full, or an ADD with constants different from 0 and 1). It does not close the file: This is the caller responsibility. It uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inputNames is non-null, it is assumed to hold the pointers to the names of the inputs. Similarly for outputNames. For each BDD node of function f, variable v, then child T, and else child E it stores: f = v * T + v' * E that is (OR f (AND v T) (AND (NOT v) E)) If E is a complemented child this results in the following (OR f (AND v T) (AND (NOT v) (NOT E)))

Side Effects None

See Also DddmpCuddDdArrayStoreBlif
Defined in dddmpStoreMisc.c 

static int 
DddmpCuddDdArrayStoreSmvStep(
  DdManager * ddMgr, 
  DdNode * f, 
  FILE * fp, 
  st_table * visited, 
  char ** names 
)
Performs the recursive step of DddmpCuddDdArrayStoreSmvBody. Traverses the BDD f and writes a multiplexer-network description to the file pointed by fp. For each BDD node of function f, variable v, then child T, and else child E it stores: f = v * T + v' * E that is (OR f (AND v T) (AND (NOT v) E)) If E is a complemented child this results in the following (OR f (AND v T) (AND (NOT v) (NOT E))) f is assumed to be a regular pointer and the function guarantees this assumption in the recursive calls.

Side Effects None

Defined in dddmpStoreMisc.c 

static int 
DddmpCuddDdArrayStoreSmv(
  DdManager * ddMgr, IN: Manager
  int  n, IN: Number of output nodes to be dumped
  DdNode ** f, IN: Array of output nodes to be dumped
  char ** inputNames, IN: Array of input names (or NULL)
  char ** outputNames, IN: Array of output names (or NULL)
  char * modelName, IN: Model name (or NULL)
  FILE * fp IN: Pointer to the dump file
)
One multiplexer is written for each BDD node. It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file system full, or an ADD with constants different from 0 and 1). It does not close the file: This is the caller responsibility. It uses a minimal unique subset of the hexadecimal address of a node as name for it. If the argument inputNames is non-null, it is assumed to hold the pointers to the names of the inputs. Similarly for outputNames. For each BDD node of function f, variable v, then child T, and else child E it stores: f = v * T + v' * E that is (OR f (AND v T) (AND (NOT v) E)) If E is a complemented child this results in the following (OR f (AND v T) (AND (NOT v) (NOT E))) Comments (COMMENT) are added at the beginning of the description to describe inputs and outputs of the design. A buffer (BUF) is add on the output to cope with complemented functions.

Side Effects None

See Also DddmpCuddDdArrayStoreBlif
Defined in dddmpStoreMisc.c 

static void 
DddmpDdNodesCheckIncomingAndScanPath(
  DdNode * f, IN: BDD node to be numbered
  int  pathLengthCurrent, IN: Current Path Length
  int  edgeInTh, IN: Max # In-Edges, after a Insert Cut Point
  int  pathLengthTh IN: Max Path Length (after, Insert a Cut Point)
)
Number nodes recursively in post-order. The "visited" flag is used with the right polarity. The node is assigned to a new CNF variable only if it is a "shared" node (i.e. the number of its incoming edges is greater than 1).

Side Effects "visited" flags are set.

Defined in dddmpDdNodeCnf.c 

static void 
DddmpDdNodesCheckIncomingAndScanPath(
  DdNode * f, IN: BDD node to be numbered
  int  pathLengthCurrent, IN: Current Path Length
  int  edgeInTh, IN: Max # In-Edges, after a Insert Cut Point
  int  pathLengthTh IN: Max Path Length (after, Insert a Cut Point)
)
Number nodes recursively in post-order. The "visited" flag is used with the right polarity. The node is assigned to a new CNF variable only if it is a "shared" node (i.e. the number of its incoming edges is greater than 1).

Side Effects "visited" flags are set.

Defined in dddmpNodeCnf.c 

int 
DddmpDdNodesCountEdgesAndNumber(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: Array of BDDs
  int  rootN, IN: Number of BDD roots in the array of BDDs
  int  edgeInTh, IN: Max # In-Edges, after a Insert Cut Point
  int  pathLengthTh, IN: Max Path Length (after, Insert a Cut Point)
  int * cnfIds, OUT: CNF identifiers for variables
  int  id OUT: Number of Temporary Variables Introduced
)
Removes nodes from unique table and numbers each node according to the number of its incoming BDD edges.

Side Effects Nodes are temporarily removed from unique table

See Also RemoveFromUniqueRecurCnf()
Defined in dddmpDdNodeCnf.c 

int 
DddmpDdNodesCountEdgesAndNumber(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: Array of BDDs
  int  rootN, IN: Number of BDD roots in the array of BDDs
  int  edgeInTh, IN: Max # In-Edges, after a Insert Cut Point
  int  pathLengthTh, IN: Max Path Length (after, Insert a Cut Point)
  int * cnfIds, OUT: CNF identifiers for variables
  int  id OUT: Number of Temporary Variables Introduced
)
Removes nodes from unique table and numbers each node according to the number of its incoming BDD edges.

Side Effects Nodes are temporarily removed from unique table

See Also RemoveFromUniqueRecurCnf()
Defined in dddmpNodeCnf.c 

static int 
DddmpDdNodesCountEdgesRecur(
  DdNode * f IN: root of the BDD
)
Counts (recursively) the number of incoming edges for each node of a BDD. This number is stored in the index field.

Side Effects "visited" flags remain untouched.

Defined in dddmpDdNodeCnf.c 

static int 
DddmpDdNodesCountEdgesRecur(
  DdNode * f IN: root of the BDD
)
Counts (recursively) the number of incoming edges for each node of a BDD. This number is stored in the index field.

Side Effects "visited" flags remain untouched.

Defined in dddmpNodeCnf.c 

static int 
DddmpDdNodesNumberEdgesRecur(
  DdNode * f, IN: BDD node to be numbered
  int * cnfIds, IN: possible source for numbering
  int  id IN/OUT: possible source for numbering
)
Number nodes recursively in post-order. The "visited" flag is used with the inverse polarity. Numbering follows the subsequent strategy: * if the index = 0 it remains so * if the index >= 1 it gets enumerated. This implies that the node is assigned to a new CNF variable only if it is not a terminal node otherwise it is assigned the index of the BDD variable.

Side Effects "visited" flags are reset.

Defined in dddmpDdNodeCnf.c 

static int 
DddmpDdNodesNumberEdgesRecur(
  DdNode * f, IN: BDD node to be numbered
  int * cnfIds, IN: possible source for numbering
  int  id IN/OUT: possible source for numbering
)
Number nodes recursively in post-order. The "visited" flag is used with the inverse polarity. Numbering follows the subsequent strategy: * if the index = 0 it remains so * if the index >= 1 it gets enumerated. This implies that the node is assigned to a new CNF variable only if it is not a terminal node otherwise it is assigned the index of the BDD variable.

Side Effects "visited" flags are reset.

Defined in dddmpNodeCnf.c 

static int 
DddmpDdNodesResetCountRecur(
  DdNode * f IN: root of the BDD whose counters are reset
)
Resets counter and visited flag for ALL nodes of a BDD (it recurs on the node children). The index field of the node is used as counter.

Defined in dddmpDdNodeCnf.c 

static int 
DddmpDdNodesResetCountRecur(
  DdNode * f IN: root of the BDD whose counters are reset
)
Resets counter and visited flag for ALL nodes of a BDD (it recurs on the node children). The index field of the node is used as counter.

Defined in dddmpNodeCnf.c 

static void 
DddmpFreeHeaderCnf(
  Dddmp_Hdr_t * Hdr IN: pointer to header
)
Frees the internal header structure by freeing all internal fields first.

Defined in dddmpLoadCnf.c 

static void 
DddmpFreeHeader(
  Dddmp_Hdr_t * Hdr IN: pointer to header
)
Frees the internal header structureby freeing all internal fields first.

Defined in dddmpLoad.c 

int * 
DddmpIntArrayDup(
  int * array, IN: array of ints to be duplicated
  int  n IN: size of the array
)
Allocates memory and copies source array

Side Effects None

Defined in dddmpUtil.c 

int * 
DddmpIntArrayRead(
  FILE * fp, IN: input file
  int  n IN: size of the array
)
Allocates memory and inputs source array

Side Effects None

Defined in dddmpUtil.c 

int 
DddmpIntArrayWrite(
  FILE * fp, IN: output file
  int * array, IN: array of ints
  int  n IN: size of the array
)
Outputs an array of ints to a specified file

Side Effects None

Defined in dddmpUtil.c 

int 
DddmpNumberAddNodes(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs
  int  n IN: number of BDD roots in the array of BDDs
)
Node numbering is required to convert pointers to integers. Since nodes are removed from unique table, no new nodes should be generated before re-inserting nodes in the unique table (DddmpUnnumberDdNodes()).

Side Effects Nodes are temporarily removed from unique table

See Also RemoveFromUniqueRecurAdd () NumberNodeRecurAdd () DddmpUnnumberDdNodesAdd ()
Defined in dddmpNodeAdd.c 

int 
DddmpNumberBddNodes(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs
  int  n IN: number of BDD roots in the array of BDDs
)
Node numbering is required to convert pointers to integers. Since nodes are removed from unique table, no new nodes should be generated before re-inserting nodes in the unique table (DddmpUnnumberBddNodes ()).

Side Effects Nodes are temporarily removed from unique table

See Also RemoveFromUniqueRecur() NumberNodeRecur() DddmpUnnumberBddNodes ()
Defined in dddmpNodeBdd.c 

int 
DddmpNumberDdNodesCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs
  int  rootN, IN: number of BDD roots in the array of BDDs
  int * cnfIds, OUT: CNF identifiers for variables
  int  id OUT: number of Temporary Variables Introduced
)
Node numbering is required to convert pointers to integers. Since nodes are removed from unique table, no new nodes should be generated before re-inserting nodes in the unique table (DddmpUnnumberDdNodesCnf()).

Side Effects Nodes are temporarily removed from unique table

See Also RemoveFromUniqueRecurCnf() NumberNodeRecurCnf() DddmpUnnumberDdNodesCnf()
Defined in dddmpDdNodeCnf.c 

int 
DddmpNumberDdNodesCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs
  int  rootN, IN: number of BDD roots in the array of BDDs
  int * cnfIds, OUT: CNF identifiers for variables
  int  id OUT: number of Temporary Variables Introduced
)
Node numbering is required to convert pointers to integers. Since nodes are removed from unique table, no new nodes should be generated before re-inserting nodes in the unique table (DddmpUnnumberDdNodesCnf()).

Side Effects Nodes are temporarily removed from unique table

See Also RemoveFromUniqueRecurCnf() NumberNodeRecurCnf() DddmpUnnumberDdNodesCnf()
Defined in dddmpNodeCnf.c 

int 
DddmpNumberDdNodes(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs
  int  n IN: number of BDD roots in the array of BDDs
)
Node numbering is required to convert pointers to integers. Since nodes are removed from unique table, no new nodes should be generated before re-inserting nodes in the unique table (DddmpUnnumberDdNodes()).

Side Effects Nodes are temporarily removed from unique table

See Also RemoveFromUniqueRecur() NumberNodeRecur() DddmpUnnumberDdNodes()
Defined in dddmpDdNodeBdd.c 

static int 
DddmpPrintBddAndNextRecur(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be displayed
)
Prints debug info for a BDD on the screen. It recurs on node's children.

Defined in dddmpDdNodeCnf.c 

static int 
DddmpPrintBddAndNextRecur(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be displayed
)
Prints debug info for a BDD on the screen. It recurs on node's children.

Defined in dddmpNodeCnf.c 

int 
DddmpPrintBddAndNext(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: Array of BDDs to be displayed
  int  rootN IN: Number of BDD roots in the array of BDDs
)
Prints debug information for an array of BDDs on the screen

Side Effects None

Defined in dddmpDdNodeCnf.c 

int 
DddmpPrintBddAndNext(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: Array of BDDs to be displayed
  int  rootN IN: Number of BDD roots in the array of BDDs
)
Prints debug information for an array of BDDs on the screen

Side Effects None

Defined in dddmpNodeCnf.c 

static int 
DddmpReadCnfClauses(
  Dddmp_Hdr_t * Hdr, IN: file header
  int *** cnfTable, OUT: CNF table for clauses
  FILE * fp IN: source file
)
Read the CNF clauses from the file in the standard DIMACS format. Store all the clauses in an internal structure for future transformation into BDDs.

Defined in dddmpLoadCnf.c 

int 
DddmpReadCode(
  FILE * fp, IN: file where to read the code
  struct binary_dd_code * pcode OUT: the read code
)
Reads a 1 byte node code. See DddmpWriteCode() for code description.

Side Effects None

See Also DddmpWriteCode()
Defined in dddmpBinary.c 

int 
DddmpReadInt(
  FILE * fp, IN: file where to read the integer
  int * pid OUT: the read integer
)
Reads an integer coded on a sequence of bytes. See DddmpWriteInt() for format.

Side Effects None

See Also DddmpWriteInt()
Defined in dddmpBinary.c 

int 
DddmpReadNodeIndexAdd(
  DdNode * f IN: BDD node
)
Reads the index of a node. LSB is skipped (used as visited flag).

Side Effects None

See Also DddmpWriteNodeIndexAdd () DddmpSetVisitedAdd () DddmpVisitedAdd ()
Defined in dddmpNodeAdd.c 

int 
DddmpReadNodeIndexBdd(
  DdNode * f IN: BDD node
)
Reads the index of a node. LSB is skipped (used as visited flag).

Side Effects None

See Also DddmpWriteNodeIndexBdd () DddmpSetVisitedBdd () DddmpVisitedBdd ()
Defined in dddmpNodeBdd.c 

int 
DddmpReadNodeIndexCnf(
  DdNode * f IN: BDD node
)
Reads the index of a node. LSB is skipped (used as visited flag).

Side Effects None

See Also DddmpWriteNodeIndexCnf() DddmpSetVisitedCnf () DddmpVisitedCnf ()
Defined in dddmpNodeCnf.c 

static int 
DddmpReadNodeIndexCnf(
  DdNode * f IN: BDD node
)
Reads the index of a node. LSB is skipped (used as visited flag).

Side Effects None

See Also DddmpWriteNodeIndexCnf() DddmpSetVisitedCnf () DddmpVisitedCnf ()
Defined in dddmpDdNodeCnf.c 

int 
DddmpReadNodeIndex(
  DdNode * f IN: BDD node
)
Reads the index of a node. LSB is skipped (used as visited flag).

Side Effects None

See Also DddmpWriteNodeIndex() DddmpSetVisited () DddmpVisited ()
Defined in dddmpDdNodeBdd.c 

void 
DddmpSetVisitedAdd(
  DdNode * f IN: BDD node to be marked (as visited)
)
Marks a node as visited

Side Effects None

See Also DddmpVisitedAdd () DddmpClearVisitedAdd ()
Defined in dddmpNodeAdd.c 

void 
DddmpSetVisitedBdd(
  DdNode * f IN: BDD node to be marked (as visited)
)
Marks a node as visited

Side Effects None

See Also DddmpVisitedBdd () DddmpClearVisitedBdd ()
Defined in dddmpNodeBdd.c 

static void 
DddmpSetVisitedCnf(
  DdNode * f IN: BDD node to be marked (as visited)
)
Marks a node as visited

Side Effects None

See Also DddmpVisitedCnf () DddmpClearVisitedCnf ()
Defined in dddmpDdNodeCnf.c 

void 
DddmpSetVisitedCnf(
  DdNode * f IN: BDD node to be marked (as visited)
)
Marks a node as visited

Side Effects None

See Also DddmpVisitedCnf () DddmpClearVisitedCnf ()
Defined in dddmpNodeCnf.c 

void 
DddmpSetVisited(
  DdNode * f IN: BDD node to be marked (as visited)
)
Marks a node as visited

Side Effects None

See Also DddmpVisited () DddmpClearVisited ()
Defined in dddmpDdNodeBdd.c 

char ** 
DddmpStrArrayDup(
  char ** array, IN: array of strings to be duplicated
  int  n IN: size of the array
)
Allocates memory and copies source array

Side Effects None

Defined in dddmpUtil.c 

void 
DddmpStrArrayFree(
  char ** array, IN: array of strings
  int  n IN: size of the array
)
Frees memory for strings and the array of pointers

Side Effects None

Defined in dddmpUtil.c 

char ** 
DddmpStrArrayRead(
  FILE * fp, IN: input file
  int  n IN: size of the array
)
Allocates memory and inputs source array

Side Effects None

Defined in dddmpUtil.c 

int 
DddmpStrArrayWrite(
  FILE * fp, IN: output file
  char ** array, IN: array of strings
  int  n IN: size of the array
)
Outputs an array of strings to a specified file

Side Effects None

Defined in dddmpUtil.c 

char * 
DddmpStrDup(
  char * str IN: string to be duplicated
)
Allocates memory and copies source string

Side Effects None

Defined in dddmpUtil.c 

void 
DddmpUnnumberAddNodes(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs
  int  n IN: number of BDD roots in the array of BDDs
)
Node indexes are no more needed. Nodes are re-linked in the unique table.

Side Effects None

See Also DddmpNumberDdNodeAdd ()
Defined in dddmpNodeAdd.c 

void 
DddmpUnnumberBddNodes(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs
  int  n IN: number of BDD roots in the array of BDDs
)
Node indexes are no more needed. Nodes are re-linked in the unique table.

Side Effects None

See Also DddmpNumberBddNode ()
Defined in dddmpNodeBdd.c 

void 
DddmpUnnumberDdNodesCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs
  int  rootN IN: number of BDD roots in the array of BDDs
)
Node indexes are no more needed. Nodes are re-linked in the unique table.

Side Effects None

See Also DddmpNumberDdNode()
Defined in dddmpDdNodeCnf.c 

void 
DddmpUnnumberDdNodesCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs
  int  rootN IN: number of BDD roots in the array of BDDs
)
Node indexes are no more needed. Nodes are re-linked in the unique table.

Side Effects None

See Also DddmpNumberDdNode()
Defined in dddmpNodeCnf.c 

void 
DddmpUnnumberDdNodes(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs
  int  n IN: number of BDD roots in the array of BDDs
)
Node indexes are no more needed. Nodes are re-linked in the unique table.

Side Effects None

See Also DddmpNumberDdNode()
Defined in dddmpDdNodeBdd.c 

int 
DddmpVisitedAdd(
  DdNode * f IN: BDD node to be tested
)
Returns true if node is visited

Side Effects None

See Also DddmpSetVisitedAdd () DddmpClearVisitedAdd ()
Defined in dddmpNodeAdd.c 

int 
DddmpVisitedBdd(
  DdNode * f IN: BDD node to be tested
)
Returns true if node is visited

Side Effects None

See Also DddmpSetVisitedBdd () DddmpClearVisitedBdd ()
Defined in dddmpNodeBdd.c 

int 
DddmpVisitedCnf(
  DdNode * f IN: BDD node to be tested
)
Returns true if node is visited

Side Effects None

See Also DddmpSetVisitedCnf () DddmpClearVisitedCnf ()
Defined in dddmpNodeCnf.c 

static int 
DddmpVisitedCnf(
  DdNode * f IN: BDD node to be tested
)
Returns true if node is visited

Side Effects None

See Also DddmpSetVisitedCnf () DddmpClearVisitedCnf ()
Defined in dddmpDdNodeCnf.c 

int 
DddmpVisited(
  DdNode * f IN: BDD node to be tested
)
Returns true if node is visited

Side Effects None

See Also DddmpSetVisited () DddmpClearVisited ()
Defined in dddmpDdNodeBdd.c 

int 
DddmpWriteCode(
  FILE * fp, IN: file where to write the code
  struct binary_dd_code  code IN: the code to be written
)
outputs a 1 byte node code using the following format: 
     Unused      : 1 bit;
     V           : 2 bits;     (variable code)
     T           : 2 bits;     (Then code)
     Ecompl      : 1 bit;      (Else complemented)
     E           : 2 bits;     (Else code)
Ecompl is set with complemented edges.

Side Effects None

See Also DddmpReadCode()
Defined in dddmpBinary.c 

int 
DddmpWriteInt(
  FILE * fp, IN: file where to write the integer
  int  id IN: integer to be written
)
Writes an integer as a sequence of bytes (MSByte first). For each byte 7 bits are used for data and one (LSBit) as link with a further byte (LSB = 1 means one more byte).

Side Effects None

See Also DddmpReadInt()
Defined in dddmpBinary.c 

void 
DddmpWriteNodeIndexAdd(
  DdNode * f, IN: BDD node
  int  id IN: index to be written
)
The index of the node is written in the "next" field of a DdNode struct. LSB is not used (set to 0). It is used as "visited" flag in DD traversals.

Side Effects None

See Also DddmpReadNodeIndexAdd () DddmpSetVisitedAdd () DddmpVisitedAdd ()
Defined in dddmpNodeAdd.c 

void 
DddmpWriteNodeIndexBdd(
  DdNode * f, IN: BDD node
  int  id IN: index to be written
)
The index of the node is written in the "next" field of a DdNode struct. LSB is not used (set to 0). It is used as "visited" flag in DD traversals.

Side Effects None

See Also DddmpReadNodeIndexBdd() DddmpSetVisitedBdd () DddmpVisitedBdd ()
Defined in dddmpNodeBdd.c 

int 
DddmpWriteNodeIndexCnfBis(
  DdNode * f, IN: BDD node
  int  id IN: index to be written
)
The index of the node is written in the "next" field of a DdNode struct. LSB is not used (set to 0). It is used as "visited" flag in DD traversals.

Side Effects None

See Also DddmpReadNodeIndexCnf() DddmpSetVisitedCnf () DddmpVisitedCnf ()
Defined in dddmpDdNodeCnf.c 

static int 
DddmpWriteNodeIndexCnfWithTerminalCheck(
  DdNode * f, IN: BDD node
  int * cnfIds, IN: possible source for the index to be written
  int  id IN: possible source for the index to be written
)
The index of the node is written in the "next" field of a DdNode struct. LSB is not used (set to 0). It is used as "visited" flag in DD traversals. The index corresponds to the BDD node variable if both the node's children are a constant node, otherwise a new CNF variable is used.

Side Effects None

See Also DddmpReadNodeIndexCnf() DddmpSetVisitedCnf () DddmpVisitedCnf ()
Defined in dddmpNodeCnf.c 

int 
DddmpWriteNodeIndexCnf(
  DdNode * f, IN: BDD node
  int  id IN: index to be written
)
The index of the node is written in the "next" field of a DdNode struct. LSB is not used (set to 0). It is used as "visited" flag in DD traversals.

Side Effects None

See Also DddmpReadNodeIndexCnf() DddmpSetVisitedCnf () DddmpVisitedCnf ()
Defined in dddmpNodeCnf.c 

static int 
DddmpWriteNodeIndexCnf(
  DdNode * f, IN: BDD node
  int * cnfIds, IN: possible source for the index to be written
  int  id IN: possible source for the index to be written
)
The index of the node is written in the "next" field of a DdNode struct. LSB is not used (set to 0). It is used as "visited" flag in DD traversals. The index corresponds to the BDD node variable if both the node's children are a constant node, otherwise a new CNF variable is used.

Side Effects None

See Also DddmpReadNodeIndexCnf() DddmpSetVisitedCnf () DddmpVisitedCnf ()
Defined in dddmpDdNodeCnf.c 

void 
DddmpWriteNodeIndex(
  DdNode * f, IN: BDD node
  int  id IN: index to be written
)
The index of the node is written in the "next" field of a DdNode struct. LSB is not used (set to 0). It is used as "visited" flag in DD traversals.

Side Effects None

See Also DddmpReadNodeIndex() DddmpSetVisited () DddmpVisited ()
Defined in dddmpDdNodeBdd.c 

int 
Dddmp_Bin2Text(
  char * filein, IN: name of binary file
  char * fileout IN: name of ASCII file
)
Converts from binary to ASCII format. A BDD array is loaded and and stored to the target file.

Side Effects None

See Also Dddmp_Text2Bin()
Defined in dddmpConvert.c 

int 
Dddmp_Text2Bin(
  char * filein, IN: name of ASCII file
  char * fileout IN: name of binary file
)
Converts from ASCII to binary format. A BDD array is loaded and and stored to the target file.

Side Effects None

See Also Dddmp_Bin2Text()
Defined in dddmpConvert.c 

int 
Dddmp_cuddAddArrayLoad(
  DdManager * ddMgr, IN: DD Manager
  Dddmp_RootMatchType  rootMatchMode, IN: storing mode selector
  char ** rootmatchnames, IN: sorted names for loaded roots
  Dddmp_VarMatchType  varMatchMode, IN: storing mode selector
  char ** varmatchnames, IN: array of variable names, by ids
  int * varmatchauxids, IN: array of variable auxids, by ids
  int * varcomposeids, IN: array of new ids, by ids
  int  mode, IN: requested input file format
  char * file, IN: file name
  FILE * fp, IN: file pointer
  DdNode *** pproots OUT: array of returned BDD roots
)
Reads a dump file representing the argument ADDs. See BDD load functions for detailed explanation.

Side Effects A vector of pointers to DD nodes is allocated and freed.

See Also Dddmp_cuddBddArrayStore
Defined in dddmpLoad.c 

int 
Dddmp_cuddAddArrayStore(
  DdManager * ddMgr, IN: DD Manager
  char * ddname, IN: DD name (or NULL)
  int  nRoots, IN: number of output BDD roots to be stored
  DdNode ** f, IN: array of ADD roots to be stored
  char ** rootnames, IN: array of root names (or NULL)
  char ** varnames, IN: array of variable names (or NULL)
  int * auxids, IN: array of converted var IDs
  int  mode, IN: storing mode selector
  Dddmp_VarInfoType  varinfo, IN: extra info for variables in text mode
  char * fname, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument array of ADDs to file. Dumping is either in text or binary form. see the corresponding BDD dump function for further details.

Side Effects Nodes are temporarily removed from the unique hash table. They are re-linked after the store operation in a modified order.

See Also Dddmp_cuddAddStore Dddmp_cuddAddLoad Dddmp_cuddAddArrayLoad
Defined in dddmpStoreAdd.c 

DdNode * 
Dddmp_cuddAddLoad(
  DdManager * ddMgr, IN: Manager
  Dddmp_VarMatchType  varMatchMode, IN: storing mode selector
  char ** varmatchnames, IN: array of variable names by IDs
  int * varmatchauxids, IN: array of variable auxids by IDs
  int * varcomposeids, IN: array of new ids by IDs
  int  mode, IN: requested input file format
  char * file, IN: file name
  FILE * fp IN: file pointer
)
Reads a dump file representing the argument ADD. Dddmp_cuddAddArrayLoad is used through a dummy array.

Side Effects A vector of pointers to DD nodes is allocated and freed.

See Also Dddmp_cuddAddStore Dddmp_cuddAddArrayLoad
Defined in dddmpLoad.c 

int 
Dddmp_cuddAddStore(
  DdManager * ddMgr, IN: DD Manager
  char * ddname, IN: DD name (or NULL)
  DdNode * f, IN: ADD root to be stored
  char ** varnames, IN: array of variable names (or NULL)
  int * auxids, IN: array of converted var ids
  int  mode, IN: storing mode selector
  Dddmp_VarInfoType  varinfo, IN: extra info for variables in text mode
  char * fname, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument ADD to file. Dumping is done through Dddmp_cuddAddArrayStore, And a dummy array of 1 ADD root is used for this purpose.

Side Effects Nodes are temporarily removed from unique hash. They are re-linked after the store operation in a modified order.

See Also Dddmp_cuddAddLoad Dddmp_cuddAddArrayLoad
Defined in dddmpStoreAdd.c 

int 
Dddmp_cuddBddArrayLoadCnf(
  DdManager * ddMgr, IN: DD Manager
  Dddmp_RootMatchType  rootmatchmode, IN: storing mode selector
  char ** rootmatchnames, IN: sorted names for loaded roots
  Dddmp_VarMatchType  varmatchmode, IN: storing mode selector
  char ** varmatchnames, IN: array of variable names, by IDs
  int * varmatchauxids, IN: array of variable auxids, by IDs
  int * varcomposeids, IN: array of new ids, by IDs
  int  mode, IN: computation Mode
  char * file, IN: file name
  FILE * fp, IN: file pointer
  DdNode *** rootsPtrPtr, OUT: array of returned BDD roots
  int * nRoots OUT: number of BDDs returned
)
Reads a dump file representing the argument BDD in a CNF formula.

Side Effects A vector of pointers to DD nodes is allocated and freed.

See Also Dddmp_cuddBddArrayLoad
Defined in dddmpLoadCnf.c 

int 
Dddmp_cuddBddArrayLoad(
  DdManager * ddMgr, IN: DD Manager
  Dddmp_RootMatchType  rootMatchMode, IN: storing mode selector
  char ** rootmatchnames, IN: sorted names for loaded roots
  Dddmp_VarMatchType  varMatchMode, IN: storing mode selector
  char ** varmatchnames, IN: array of variable names, by ids
  int * varmatchauxids, IN: array of variable auxids, by ids
  int * varcomposeids, IN: array of new ids, by ids
  int  mode, IN: requested input file format
  char * file, IN: file name
  FILE * fp, IN: file pointer
  DdNode *** pproots OUT: array of returned BDD roots
)
Reads a dump file representing the argument BDDs. The header is common to both text and binary mode. The node list is either in text or binary format. A dynamic vector of DD pointers is allocated to support conversion from DD indexes to pointers. Several criteria are supported for variable match between file and dd manager. Several changes/permutations/compositions are allowed for variables while loading DDs. Variable of the dd manager are allowed to match with variables on file on ids, permids, varnames, varauxids; also direct composition between ids and composeids is supported. More in detail:
  1. varMatchMode=DDDMP_VAR_MATCHIDS

    allows the loading of a DD keeping variable IDs unchanged (regardless of the variable ordering of the reading manager); this is useful, for example, when swapping DDs to file and restoring them later from file, after possible variable reordering activations.

  2. varMatchMode=DDDMP_VAR_MATCHPERMIDS

    is used to allow variable match according to the position in the ordering.

  3. varMatchMode=DDDMP_VAR_MATCHNAMES

    requires a non NULL varmatchnames parameter; this is a vector of strings in one-to-one correspondence with variable IDs of the reading manager. Variables in the DD file read are matched with manager variables according to their name (a non NULL varnames parameter was required while storing the DD file).

  4. varMatchMode=DDDMP_VAR_MATCHIDS

    has a meaning similar to DDDMP_VAR_MATCHNAMES, but integer auxiliary IDs are used instead of strings; the additional non NULL varmatchauxids parameter is needed.

  5. varMatchMode=DDDMP_VAR_COMPOSEIDS

    uses the additional varcomposeids parameter is used as array of variable ids to be composed with ids stored in file.

In the present implementation, the array varnames (3), varauxids (4) and composeids (5) need to have one entry for each variable in the DD manager (NULL pointers are allowed for unused variables in varnames). Hence variables need to be already present in the manager. All arrays are sorted according to IDs. All the loaded BDDs are referenced before returning them.

Side Effects A vector of pointers to DD nodes is allocated and freed.

See Also Dddmp_cuddBddArrayStore
Defined in dddmpLoad.c 

int 
Dddmp_cuddBddArrayStoreBlif(
  DdManager * ddMgr, IN: DD Manager
  int  nroots, IN: number of output BDD roots to be stored
  DdNode ** f, IN: array of BDD roots to be stored
  char ** inputNames, IN: array of variable names (or NULL)
  char ** outputNames, IN: array of root names (or NULL)
  char * modelName, IN: Model Name
  char * fname, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument BDD to file. Dumping is done through Dddmp_cuddBddArrayStoreBLif. A dummy array of 1 BDD root is used for this purpose.

See Also Dddmp_cuddBddArrayStorePrefix
Defined in dddmpStoreMisc.c 

int 
Dddmp_cuddBddArrayStoreCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDD roots to be stored
  int  rootN, IN: # output BDD roots to be stored
  Dddmp_DecompCnfStoreType  mode, IN: format selection
  int  noHeader, IN: do not store header iff 1
  char ** varNames, IN: array of variable names (or NULL)
  int * bddIds, IN: array of converted var IDs
  int * bddAuxIds, IN: array of BDD node Auxiliary Ids
  int * cnfIds, IN: array of converted var IDs
  int  idInitial, IN: starting id for cutting variables
  int  edgeInTh, IN: Max # Incoming Edges
  int  pathLengthTh, IN: Max Path Length
  char * fname, IN: file name
  FILE * fp, IN: pointer to the store file
  int * clauseNPtr, OUT: number of clause stored
  int * varNewNPtr OUT: number of new variable created
)
Dumps the argument array of BDDs to file.

Side Effects Nodes are temporarily removed from the unique hash table. They are re-linked after the store operation in a modified order. Three methods are allowed: * NodeByNode method: Insert a cut-point for each BDD node (but the terminal nodes) * MaxtermByMaxterm method: Insert no cut-points, i.e. the off-set of trhe function is stored * Best method: Tradeoff between the previous two methods. Auxiliary variables, i.e., cut points are inserted following these criterias: * edgeInTh indicates the maximum number of incoming edges up to which no cut point (auxiliary variable) is inserted. If edgeInTh: * is equal to -1 no cut point due to incoming edges are inserted (MaxtermByMaxterm method.) * is equal to 0 a cut point is inserted for each node with a single incoming edge, i.e., each node, (NodeByNode method). * is equal to n a cut point is inserted for each node with (n+1) incoming edges. * pathLengthTh indicates the maximum length path up to which no cut points (auxiliary variable) is inserted. If the path length between two nodes exceeds this value, a cut point is inserted. If pathLengthTh: * is equal to -1 no cut point due path length are inserted (MaxtermByMaxterm method.) * is equal to 0 a cut point is inserted for each node (NodeByNode method). * is equal to n a cut point is inserted on path whose length is equal to (n+1). Notice that the maximum number of literals in a clause is equal to (pathLengthTh + 2), i.e., for each path we have to keep into account a CNF variable for each node plus 2 added variables for the bottom and top-path cut points. The stored file can contain a file header or not depending on the noHeader parameter (IFF 0, usual setting, the header is usually stored. This option can be useful in storing multiple BDDs, as separate BDDs, on the same file leaving the opening of the file to the caller.

Defined in dddmpStoreCnf.c 

int 
Dddmp_cuddBddArrayStorePrefix(
  DdManager * ddMgr, IN: DD Manager
  int  nroots, IN: number of output BDD roots to be stored
  DdNode ** f, IN: array of BDD roots to be stored
  char ** inputNames, IN: array of variable names (or NULL)
  char ** outputNames, IN: array of root names (or NULL)
  char * modelName, IN: Model Name
  char * fname, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument BDD to file. Dumping is done through Dddmp_cuddBddArrayStorePrefix. A dummy array of 1 BDD root is used for this purpose.

See Also Dddmp_cuddBddArrayStore
Defined in dddmpStoreMisc.c 

int 
Dddmp_cuddBddArrayStoreSmv(
  DdManager * ddMgr, IN: DD Manager
  int  nroots, IN: number of output BDD roots to be stored
  DdNode ** f, IN: array of BDD roots to be stored
  char ** inputNames, IN: array of variable names (or NULL)
  char ** outputNames, IN: array of root names (or NULL)
  char * modelName, IN: Model Name
  char * fname, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument BDD to file. Dumping is done through Dddmp_cuddBddArrayStorePrefix. A dummy array of 1 BDD root is used for this purpose.

See Also Dddmp_cuddBddArrayStore
Defined in dddmpStoreMisc.c 

int 
Dddmp_cuddBddArrayStore(
  DdManager * ddMgr, IN: DD Manager
  char * ddname, IN: dd name (or NULL)
  int  nRoots, IN: number of output BDD roots to be stored
  DdNode ** f, IN: array of BDD roots to be stored
  char ** rootnames, IN: array of root names (or NULL)
  char ** varnames, IN: array of variable names (or NULL)
  int * auxids, IN: array of converted var IDs
  int  mode, IN: storing mode selector
  Dddmp_VarInfoType  varinfo, IN: extra info for variables in text mode
  char * fname, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument array of BDDs to file. Dumping is either in text or binary form. BDDs are stored to the fp (already open) file if not NULL. Otherwise the file whose name is fname is opened in write mode. The header has the same format for both textual and binary dump. Names are allowed for input variables (vnames) and for represented functions (rnames). For sake of generality and because of dynamic variable ordering both variable IDs and permuted IDs are included. New IDs are also supported (auxids). Variables are identified with incremental numbers. according with their positiom in the support set. In text mode, an extra info may be added, chosen among the following options: name, ID, PermID, or an auxiliary id. Since conversion from DD pointers to integers is required, DD nodes are temporarily removed from the unique hash table. This allows the use of the next field to store node IDs.

Side Effects Nodes are temporarily removed from the unique hash table. They are re-linked after the store operation in a modified order.

See Also Dddmp_cuddBddStore Dddmp_cuddBddLoad Dddmp_cuddBddArrayLoad
Defined in dddmpStoreBdd.c 

int 
Dddmp_cuddBddDisplayBinary(
  char * fileIn, IN: name of binary file
  char * fileOut IN: name of text file
)
Display a binary dump file in a text file

Side Effects None

See Also Dddmp_cuddBddStore Dddmp_cuddBddLoad
Defined in dddmpDbg.c 

int 
Dddmp_cuddBddLoadCnf(
  DdManager * ddMgr, IN: DD Manager
  Dddmp_VarMatchType  varmatchmode, IN: storing mode selector
  char ** varmatchnames, IN: array of variable names, by IDs
  int * varmatchauxids, IN: array of variable auxids, by IDs
  int * varcomposeids, IN: array of new ids accessed, by IDs
  int  mode, IN: computation mode
  char * file, IN: file name
  FILE * fp, IN: file pointer
  DdNode *** rootsPtrPtr, OUT: array of returned BDD roots
  int * nRoots OUT: number of BDDs returned
)
Reads a dump file representing the argument BDD in a CNF formula. Dddmp_cuddBddArrayLoadCnf is used through a dummy array. The results is returned in different formats depending on the mode selection: IFF mode == 0 Return the Clauses without Conjunction IFF mode == 1 Return the sets of BDDs without Quantification IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification

Side Effects A vector of pointers to DD nodes is allocated and freed.

See Also Dddmp_cuddBddLoad Dddmp_cuddBddArrayLoad
Defined in dddmpLoadCnf.c 

DdNode * 
Dddmp_cuddBddLoad(
  DdManager * ddMgr, IN: DD Manager
  Dddmp_VarMatchType  varMatchMode, IN: storing mode selector
  char ** varmatchnames, IN: array of variable names - by IDs
  int * varmatchauxids, IN: array of variable auxids - by IDs
  int * varcomposeids, IN: array of new ids accessed - by IDs
  int  mode, IN: requested input file format
  char * file, IN: file name
  FILE * fp IN: file pointer
)
Reads a dump file representing the argument BDD. Dddmp_cuddBddArrayLoad is used through a dummy array (see this function's description for more details). Mode, the requested input file format, is checked against the file format. The loaded BDDs is referenced before returning it.

Side Effects A vector of pointers to DD nodes is allocated and freed.

See Also Dddmp_cuddBddStore Dddmp_cuddBddArrayLoad
Defined in dddmpLoad.c 

int 
Dddmp_cuddBddStoreBlif(
  DdManager * ddMgr, IN: DD Manager
  int  nRoots, IN: Number of BDD roots
  DdNode * f, IN: BDD root to be stored
  char ** inputNames, IN: Array of variable names
  char ** outputNames, IN: Array of root names
  char * modelName, IN: Model Name
  char * fileName, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument BDD to file. Dumping is done through Dddmp_cuddBddArrayStoreBlif. A dummy array of 1 BDD root is used for this purpose.

See Also Dddmp_cuddBddStorePrefix
Defined in dddmpStoreMisc.c 

int 
Dddmp_cuddBddStoreCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f, IN: BDD root to be stored
  Dddmp_DecompCnfStoreType  mode, IN: format selection
  int  noHeader, IN: do not store header iff 1
  char ** varNames, IN: array of variable names (or NULL)
  int * bddIds, IN: array of var ids
  int * bddAuxIds, IN: array of BDD node Auxiliary Ids
  int * cnfIds, IN: array of CNF var ids
  int  idInitial, IN: starting id for cutting variables
  int  edgeInTh, IN: Max # Incoming Edges
  int  pathLengthTh, IN: Max Path Length
  char * fname, IN: file name
  FILE * fp, IN: pointer to the store file
  int * clauseNPtr, OUT: number of clause stored
  int * varNewNPtr OUT: number of new variable created
)
Dumps the argument BDD to file. This task is performed by calling the function Dddmp_cuddBddArrayStoreCnf.

Side Effects Nodes are temporarily removed from unique hash. They are re-linked after the store operation in a modified order.

See Also Dddmp_cuddBddArrayStoreCnf
Defined in dddmpStoreCnf.c 

int 
Dddmp_cuddBddStorePrefix(
  DdManager * ddMgr, IN: DD Manager
  int  nRoots, IN: Number of BDD roots
  DdNode * f, IN: BDD root to be stored
  char ** inputNames, IN: Array of variable names
  char ** outputNames, IN: Array of root names
  char * modelName, IN: Model Name
  char * fileName, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument BDD to file. Dumping is done through Dddmp_cuddBddArrayStorePrefix. A dummy array of 1 BDD root is used for this purpose.

See Also Dddmp_cuddBddStore
Defined in dddmpStoreMisc.c 

int 
Dddmp_cuddBddStoreSmv(
  DdManager * ddMgr, IN: DD Manager
  int  nRoots, IN: Number of BDD roots
  DdNode * f, IN: BDD root to be stored
  char ** inputNames, IN: Array of variable names
  char ** outputNames, IN: Array of root names
  char * modelName, IN: Model Name
  char * fileName, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument BDD to file. Dumping is done through Dddmp_cuddBddArrayStorePrefix. A dummy array of 1 BDD root is used for this purpose.

See Also Dddmp_cuddBddStore
Defined in dddmpStoreMisc.c 

int 
Dddmp_cuddBddStore(
  DdManager * ddMgr, IN: DD Manager
  char * ddname, IN: DD name (or NULL)
  DdNode * f, IN: BDD root to be stored
  char ** varnames, IN: array of variable names (or NULL)
  int * auxids, IN: array of converted var ids
  int  mode, IN: storing mode selector
  Dddmp_VarInfoType  varinfo, IN: extra info for variables in text mode
  char * fname, IN: File name
  FILE * fp IN: File pointer to the store file
)
Dumps the argument BDD to file. Dumping is done through Dddmp_cuddBddArrayStore. A dummy array of 1 BDD root is used for this purpose.

Side Effects Nodes are temporarily removed from unique hash. They are re-linked after the store operation in a modified order.

See Also Dddmp_cuddBddLoad Dddmp_cuddBddArrayLoad
Defined in dddmpStoreBdd.c 

int 
Dddmp_cuddHeaderLoadCnf(
  int * nVars, OUT: number of DD variables
  int * nsuppvars, OUT: number of support variables
  char *** suppVarNames, OUT: array of support variable names
  char *** orderedVarNames, OUT: array of variable names
  int ** varIds, OUT: array of variable ids
  int ** varComposeIds, OUT: array of permids ids
  int ** varAuxIds, OUT: array of variable aux ids
  int * nRoots, OUT: number of root in the file
  char * file, IN: file name
  FILE * fp IN: file pointer
)
Reads the header of a dump file representing the argument BDDs. Returns main information regarding DD type stored in the file, the variable ordering used, the number of variables, etc. It reads only the header of the file NOT the BDD/ADD section.

See Also Dddmp_cuddBddArrayLoad
Defined in dddmpLoadCnf.c 

int 
Dddmp_cuddHeaderLoad(
  Dddmp_DecompType * ddType, OUT: selects the proper decomp type
  int * nVars, OUT: number of DD variables
  int * nsuppvars, OUT: number of support variables
  char *** suppVarNames, OUT: array of support variable names
  char *** orderedVarNames, OUT: array of variable names
  int ** varIds, OUT: array of variable ids
  int ** varComposeIds, OUT: array of permids ids
  int ** varAuxIds, OUT: array of variable aux ids
  int * nRoots, OUT: number of root in the file
  char * file, IN: file name
  FILE * fp IN: file pointer
)
Reads the header of a dump file representing the argument BDDs. Returns main information regarding DD type stored in the file, the variable ordering used, the number of variables, etc. It reads only the header of the file NOT the BDD/ADD section.

See Also Dddmp_cuddBddArrayLoad
Defined in dddmpLoad.c 

int 
FindVarname(
  char * name, IN: name to look for
  char ** array, IN: search array
  int  n IN: size of the array
)
Binary search of a name within a sorted array of strings. Used when matching names of variables.

Side Effects None

Defined in dddmpUtil.c 

static int 
NodeBinaryStoreBdd(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f, IN: DD node to be stored
  int  mode, IN: store mode
  int * supportids, IN: internal ids for variables
  char ** varnames, IN: names of variables: to be stored with nodes
  int * outids, IN: output ids for variables
  FILE * fp, IN: store file
  int  idf, IN: index of the node
  int  vf, IN: variable of the node
  int  idT, IN: index of the Then node
  int  idE, IN: index of the Else node
  int  vT, IN: variable of the Then node
  int  vE, IN: variable of the Else node
  DdNode * T, IN: Then node
  DdNode * E IN: Else node
)
Store 1 0 0 for the terminal node. Store id, left child pointer, right pointer for all the other nodes. Store every information as coded binary values.

Side Effects None

See Also NodeTextStoreBdd
Defined in dddmpStoreBdd.c 

static int 
NodeStoreRecurAdd(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f, IN: DD node to be stored
  int  mode, IN: store mode
  int * supportids, IN: internal ids for variables
  char ** varnames, IN: names of variables: to be stored with nodes
  int * outids, IN: output ids for variables
  FILE * fp IN: store file
)
Stores a node to file in either test or binary mode. In text mode a node is represented (on a text line basis) as
  • node-index [var-extrainfo] var-index Then-index Else-index
where all indexes are integer numbers and var-extrainfo (optional redundant field) is either an integer or a string (variable name). Node-index is redundant (due to the node ordering) but we keep it for readability.

In binary mode nodes are represented as a sequence of bytes, representing var-index, Then-index, and Else-index in an optimized way. Only the first byte (code) is mandatory. Integer indexes are represented in absolute or relative mode, where relative means offset wrt. a Then/Else node info. Suppose Var(NodeId), Then(NodeId) and Else(NodeId) represent infos about a given node.

The generic "NodeId" node is stored as

  • code-byte
  • [var-info]
  • [Then-info]
  • [Else-info]
where code-byte contains bit fields
  • Unused : 1 bit
  • Variable: 2 bits, one of the following codes
    • DDDMP_ABSOLUTE_ID var-info = Var(NodeId) follows
    • DDDMP_RELATIVE_ID Var(NodeId) is represented in relative form as var-info = Min(Var(Then(NodeId)),Var(Else(NodeId))) -Var(NodeId)
    • DDDMP_RELATIVE_1 No var-info follows, because Var(NodeId) = Min(Var(Then(NodeId)),Var(Else(NodeId)))-1
    • DDDMP_TERMINAL Node is a terminal, no var info required
  • T : 2 bits, with codes similar to V
    • DDDMP_ABSOLUTE_ID Then-info = Then(NodeId) follows
    • DDDMP_RELATIVE_ID Then(NodeId) is represented in relative form as Then-info = Nodeid-Then(NodeId)
    • DDDMP_RELATIVE_1 No info on Then(NodeId) follows, because Then(NodeId) = NodeId-1
    • DDDMP_TERMINAL Then Node is a terminal, no info required (for BDDs)
  • Ecompl : 1 bit, if 1 means complemented edge
  • E : 2 bits, with codes and meanings as for the Then edge
var-info, Then-info, Else-info (if required) are represented as unsigned integer values on a sufficient set of bytes (MSByte first).

Side Effects None

Defined in dddmpStoreAdd.c 

static int 
NodeStoreRecurBdd(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f, IN: DD node to be stored
  int  mode, IN: store mode
  int * supportids, IN: internal ids for variables
  char ** varnames, IN: names of variables: to be stored with nodes
  int * outids, IN: output ids for variables
  FILE * fp IN: store file
)
Stores a node to file in either test or binary mode. In text mode a node is represented (on a text line basis) as
  • node-index [var-extrainfo] var-index Then-index Else-index
where all indexes are integer numbers and var-extrainfo (optional redundant field) is either an integer or a string (variable name). Node-index is redundant (due to the node ordering) but we keep it for readability.

In binary mode nodes are represented as a sequence of bytes, representing var-index, Then-index, and Else-index in an optimized way. Only the first byte (code) is mandatory. Integer indexes are represented in absolute or relative mode, where relative means offset wrt. a Then/Else node info. Suppose Var(NodeId), Then(NodeId) and Else(NodeId) represent infos about a given node.

The generic "NodeId" node is stored as

  • code-byte
  • [var-info]
  • [Then-info]
  • [Else-info]
where code-byte contains bit fields
  • Unused : 1 bit
  • Variable: 2 bits, one of the following codes
    • DDDMP_ABSOLUTE_ID var-info = Var(NodeId) follows
    • DDDMP_RELATIVE_ID Var(NodeId) is represented in relative form as var-info = Min(Var(Then(NodeId)),Var(Else(NodeId))) -Var(NodeId)
    • DDDMP_RELATIVE_1 No var-info follows, because Var(NodeId) = Min(Var(Then(NodeId)),Var(Else(NodeId)))-1
    • DDDMP_TERMINAL Node is a terminal, no var info required
  • T : 2 bits, with codes similar to V
    • DDDMP_ABSOLUTE_ID Then-info = Then(NodeId) follows
    • DDDMP_RELATIVE_ID Then(NodeId) is represented in relative form as Then-info = Nodeid-Then(NodeId)
    • DDDMP_RELATIVE_1 No info on Then(NodeId) follows, because Then(NodeId) = NodeId-1
    • DDDMP_TERMINAL Then Node is a terminal, no info required (for BDDs)
  • Ecompl : 1 bit, if 1 means complemented edge
  • E : 2 bits, with codes and meanings as for the Then edge
var-info, Then-info, Else-info (if required) are represented as unsigned integer values on a sufficient set of bytes (MSByte first).

Side Effects None

Defined in dddmpStoreBdd.c 

static int 
NodeTextStoreAdd(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f, IN: DD node to be stored
  int  mode, IN: store mode
  int * supportids, IN: internal ids for variables
  char ** varnames, IN: names of variables: to be stored with nodes
  int * outids, IN: output ids for variables
  FILE * fp, IN: Store file
  int  idf, IN: index of the current node
  int  vf, IN: variable of the current node
  int  idT, IN: index of the Then node
  int  idE IN: index of the Else node
)
Store 1 0 0 for the terminal node. Store id, left child pointer, right pointer for all the other nodes.

Side Effects None

See Also NodeBinaryStore
Defined in dddmpStoreAdd.c 

static int 
NodeTextStoreBdd(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f, IN: DD node to be stored
  int  mode, IN: store mode
  int * supportids, IN: internal ids for variables
  char ** varnames, IN: names of variables: to be stored with nodes
  int * outids, IN: output ids for variables
  FILE * fp, IN: Store file
  int  idf, IN: index of the current node
  int  vf, IN: variable of the current node
  int  idT, IN: index of the Then node
  int  idE IN: index of the Else node
)
Store 1 0 0 for the terminal node. Store id, left child pointer, right pointer for all the other nodes.

Side Effects None

See Also NodeBinaryStoreBdd
Defined in dddmpStoreBdd.c 

static int 
NumberNodeRecurAdd(
  DdNode * f, IN: root of the BDD to be numbered
  int  id IN/OUT: index to be assigned to the node
)
Number nodes recursively in post-order. The "visited" flag is used with inverse polarity, because all nodes were set "visited" when removing them from unique.

Side Effects "visited" flags are reset.

Defined in dddmpNodeAdd.c 

static int 
NumberNodeRecurBdd(
  DdNode * f, IN: root of the BDD to be numbered
  int  id IN/OUT: index to be assigned to the node
)
Number nodes recursively in post-order. The "visited" flag is used with inverse polarity, because all nodes were set "visited" when removing them from unique.

Side Effects "visited" flags are reset.

Defined in dddmpNodeBdd.c 

static int 
NumberNodeRecurCnf(
  DdNode * f, IN: root of the BDD to be numbered
  int * cnfIds, IN: possible source for numbering
  int  id IN/OUT: possible source for numbering
)
Number nodes recursively in post-order. The "visited" flag is used with inverse polarity, because all nodes were set "visited" when removing them from unique.

Side Effects "visited" flags are reset.

Defined in dddmpDdNodeCnf.c 

static int 
NumberNodeRecurCnf(
  DdNode * f, IN: root of the BDD to be numbered
  int * cnfIds, IN: possible source for numbering
  int  id IN/OUT: possible source for numbering
)
Number nodes recursively in post-order. The "visited" flag is used with inverse polarity, because all nodes were set "visited" when removing them from unique.

Side Effects "visited" flags are reset.

Defined in dddmpNodeCnf.c 

static int 
NumberNodeRecur(
  DdNode * f, IN: root of the BDD to be numbered
  int  id IN/OUT: index to be assigned to the node
)
Number nodes recursively in post-order. The "visited" flag is used with inverse polarity, because all nodes were set "visited" when removing them from unique.

Side Effects "visited" flags are reset.

Defined in dddmpDdNodeBdd.c 

int 
QsortStrcmp(
  const void * ps1, IN: pointer to the first string
  const void * ps2 IN: pointer to the second string
)
String compare for qsort

Side Effects None

Defined in dddmpUtil.c 

static int 
ReadByteBinary(
  FILE * fp, IN: file where to read the byte
  unsigned char * cp OUT: the read byte
)
inputs a byte to file fp. 0x00 has been used as escape character to filter , and . This is done for compatibility between unix and dos/windows systems.

Side Effects None

See Also WriteByteBinary()
Defined in dddmpBinary.c 

static void 
RemoveFromUniqueRecurAdd(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be extracted
)
Removes a node from the unique table by locating the proper subtable and unlinking the node from it. It recurs on the children of the node. Constants remain untouched.

Side Effects Nodes are left with the "visited" flag true.

See Also RestoreInUniqueRecurAdd ()
Defined in dddmpNodeAdd.c 

static void 
RemoveFromUniqueRecurBdd(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be extracted
)
Removes a node from the unique table by locating the proper subtable and unlinking the node from it. It recurs on the children of the node. Constants remain untouched.

Side Effects Nodes are left with the "visited" flag true.

See Also RestoreInUniqueRecurBdd ()
Defined in dddmpNodeBdd.c 

static void 
RemoveFromUniqueRecurCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be extracted
)
Removes a node from the unique table by locating the proper subtable and unlinking the node from it. It recurs on on the children of the node. Constants remain untouched.

Side Effects Nodes are left with the "visited" flag true.

See Also RestoreInUniqueRecurCnf()
Defined in dddmpNodeCnf.c 

static void 
RemoveFromUniqueRecurCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be extracted
)
Removes a node from the unique table by locating the proper subtable and unlinking the node from it. It recurs on son nodes.

Side Effects Nodes are left with the "visited" flag true.

See Also RestoreInUniqueRecurCnf()
Defined in dddmpDdNodeCnf.c 

static void 
RemoveFromUniqueRecur(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be extracted
)
Removes a node from the unique table by locating the proper subtable and unlinking the node from it. It recurs on the children of the node.

Side Effects Nodes are left with the "visited" flag true.

See Also RestoreInUniqueRecur()
Defined in dddmpDdNodeBdd.c 

static void 
RestoreInUniqueRecurAdd(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be restored
)
Restores a node in unique table (recursively)

Side Effects Nodes are not restored in the same order as before removal

See Also RemoveFromUniqueAdd ()
Defined in dddmpNodeAdd.c 

static void 
RestoreInUniqueRecurBdd(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be restored
)
Restores a node in unique table (recursively)

Side Effects Nodes are not restored in the same order as before removal

See Also RemoveFromUnique()
Defined in dddmpNodeBdd.c 

static void 
RestoreInUniqueRecurCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be restored
)
Restores a node in unique table (recursive)

Side Effects Nodes are not restored in the same order as before removal

See Also RemoveFromUnique()
Defined in dddmpDdNodeCnf.c 

static void 
RestoreInUniqueRecurCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be restored
)
Restores a node in unique table (recursive)

Side Effects Nodes are not restored in the same order as before removal

See Also RemoveFromUnique()
Defined in dddmpNodeCnf.c 

static void 
RestoreInUniqueRecur(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f IN: root of the BDD to be restored
)
Restores a node in unique table (recursively)

Side Effects Nodes are not restored in the same order as before removal

See Also RemoveFromUnique()
Defined in dddmpDdNodeBdd.c 

static int 
StoreCnfBestNotSharedRecur(
  DdManager * ddMgr, IN: DD Manager
  DdNode * node, IN: BDD to store
  int  idf, IN: Id to store
  int * bddIds, IN: BDD identifiers
  int * cnfIds, IN: corresponding CNF identifiers
  FILE * fp, IN: file pointer
  int * list, IN: temporary array to store cubes
  int * clauseN, OUT: number of stored clauses
  int * varMax OUT: maximum identifier of the variables created
)
Performs the recursive step of Print Best on Not Shared sub-BDDs, i.e., print out information for the nodes belonging to BDDs not shared (whose root has just one incoming edge).

Side Effects None

Defined in dddmpStoreCnf.c 

static int 
StoreCnfBestSharedRecur(
  DdManager * ddMgr, IN: DD Manager
  DdNode * node, IN: BDD to store
  int * bddIds, IN: BDD identifiers
  int * cnfIds, IN: corresponding CNF identifiers
  FILE * fp, IN: file pointer
  int * list, IN: temporary array to store cubes
  int * clauseN, OUT: number of stored clauses
  int * varMax OUT: maximum identifier of the variables created
)
Performs the recursive step of Print Best on Not Shared sub-BDDs, i.e., print out information for the nodes belonging to BDDs not shared (whose root has just one incoming edge).

Side Effects None

Defined in dddmpStoreCnf.c 

static int 
StoreCnfBest(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs to store
  int  rootN, IN: number of BDD in the array
  int * bddIds, IN: BDD identifiers
  int * cnfIds, IN: corresponding CNF identifiers
  int  idInitial, IN: initial value for numbering new CNF variables
  FILE * fp, IN: file pointer
  int * varMax, OUT: maximum identifier of the variables created
  int * clauseN, OUT: number of stored clauses
  int * rootStartLine OUT: line where root starts
)
Prints a disjoint sum of product cover for the function rooted at node intorducing cutting points whenever necessary. Each product corresponds to a path from node a leaf node different from the logical zero, and different from the background value. Uses the standard output. Returns 1 if successful, 0 otherwise.

Side Effects None

See Also StoreCnfMaxtermByMaxterm
Defined in dddmpStoreCnf.c 

static void 
StoreCnfMaxtermByMaxtermRecur(
  DdManager * ddMgr, IN: DD Manager
  DdNode * node, IN: BDD to store
  int * bddIds, IN: BDD identifiers
  int * cnfIds, IN: corresponding CNF identifiers
  FILE * fp, IN: file pointer
  int * list, IN: temporary array to store cubes
  int * clauseN, OUT: number of stored clauses
  int * varMax OUT: maximum identifier of the variables created
)
Performs the recursive step of Print Maxterm. Traverse a BDD a print out a cube in CNF format each time a terminal node is reached.

Side Effects None

Defined in dddmpStoreCnf.c 

static int 
StoreCnfMaxtermByMaxterm(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: array of BDDs to store
  int  rootN, IN: number of BDDs in the array
  int * bddIds, IN: BDD Identifiers
  int * cnfIds, IN: corresponding CNF Identifiers
  int  idInitial, IN: initial value for numbering new CNF variables
  FILE * fp, IN: file pointer
  int * varMax, OUT: maximum identifier of the variables created
  int * clauseN, OUT: number of stored clauses
  int * rootStartLine OUT: line where root starts
)
Prints a disjoint sum of product cover for the function rooted at node. Each product corresponds to a path from node a leaf node different from the logical zero, and different from the background value. Uses the standard output. Returns 1 if successful, 0 otherwise.

Side Effects None

See Also StoreCnfBest
Defined in dddmpStoreCnf.c 

static int 
StoreCnfNodeByNodeRecur(
  DdManager * ddMgr, IN: DD Manager
  DdNode * f, IN: BDD node to be stored
  int * bddIds, IN: BDD ids for variables
  int * cnfIds, IN: CNF ids for variables
  FILE * fp, IN: store file
  int * clauseN, OUT: number of clauses written in the CNF file
  int * varMax OUT: maximum value of id written in the CNF file
)
Performs the recursive step of Dddmp_bddStore. Traverse the BDD and store a CNF formula for each "terminal" node.

Side Effects None

Defined in dddmpStoreCnf.c 

static int 
StoreCnfNodeByNode(
  DdManager * ddMgr, IN: DD Manager
  DdNode ** f, IN: BDD array to be stored
  int  rootN, IN: number of BDDs in the array
  int * bddIds, IN: BDD ids for variables
  int * cnfIds, IN: CNF ids for variables
  FILE * fp, IN: store file
  int * clauseN, IN/OUT: number of clauses written in the CNF file
  int * varMax, IN/OUT: maximum value of id written in the CNF file
  int * rootStartLine OUT: CNF line where root starts
)
Store the BDD as CNF clauses. Use a multiplexer description for each BDD node.

Side Effects None

Defined in dddmpStoreCnf.c 

static int 
StoreCnfOneNode(
  DdNode * f, IN: node to be stored
  int  idf, IN: node CNF Index
  int  vf, IN: node BDD Index
  int  idT, IN: Then CNF Index with sign = inverted edge
  int  idE, IN: Else CNF Index with sign = inverted edge
  FILE * fp, IN: store file
  int * clauseN, OUT: number of clauses
  int * varMax OUT: maximun Index of variable stored
)
Store One Single BDD Node translating it as a multiplexer.

Side Effects None

Defined in dddmpStoreCnf.c 

static int 
WriteByteBinary(
  FILE * fp, IN: file where to write the byte
  unsigned char  c IN: the byte to be written
)
outputs a byte to file fp. Uses 0x00 as escape character to filter , and . This is done for compatibility between unix and dos/windows systems.

Side Effects None

See Also ReadByteBinary()
Defined in dddmpBinary.c 

static int 
printCubeCnf(
  DdManager * ddMgr, IN: DD Manager
  DdNode * node, IN: BDD to store
  int * cnfIds, IN: CNF identifiers
  FILE * fp, IN: file pointer
  int * list, IN: temporary array to store cubes
  int * varMax OUT: maximum identifier of the variables created
)
Print One Cube in CNF Format. Return DDDMP_SUCCESS if something is printed out, DDDMP_FAILURE is nothing is printed out.

Side Effects None

Defined in dddmpStoreCnf.c 

 
(
    
)
Checks for Warnings: If expr==1 it prints out the warning on stderr.

Side Effects None

Defined in dddmp.h 

 
(
    
)
Checks for fatal bugs and go to the label to deal with the error.

Side Effects None

Defined in dddmp.h 

 
(
    
)
Checks for fatal bugs and return the DDDMP_FAILURE flag.

Side Effects None

Defined in dddmp.h 

 
(
    
)
Conditional safety assertion. It prints out the file name and line number where the fatal error occurred. Messages are printed out on stderr.

Side Effects None

Defined in dddmp.h 

 
(
    
)
Memory Allocation Macro for DDDMP

Side Effects None

Defined in dddmpInt.h 

 
(
    
)
Memory Free Macro for DDDMP

Side Effects None

Defined in dddmpInt.h
Last updated on 1040218 17h14