dddmp.h

External header file

dddmpInt.h

Internal header file

dddmpBinary.c

Input and output BDD codes and integers from/to file

dddmpConvert.c

Conversion between ASCII and binary formats

dddmpDbg.c

Functions to display BDD files

dddmpDdNodeBdd.c

Functions to handle BDD node infos and numbering

dddmpDdNodeCnf.c

Functions to handle BDD node infos and numbering while storing a CNF formula from a BDD or an array of BDDs

dddmpLoad.c

Functions to read in bdds to file

dddmpLoadCnf.c

Functions to read in CNF from file as BDDs.

dddmpNodeAdd.c

Functions to handle ADD node infos and numbering

dddmpNodeBdd.c

Functions to handle BDD node infos and numbering

dddmpNodeCnf.c

Functions to handle BDD node infos and numbering while storing a CNF formula from a BDD or an array of BDDs

dddmpStoreAdd.c

Functions to write ADDs to file.

dddmpStoreBdd.c

Functions to write BDDs to file.

dddmpStoreCnf.c

Functions to write out BDDs to file in a CNF format

dddmpStoreMisc.c

Functions to write out bdds to file in prefixed and in Blif form.

dddmpUtil.c

Util Functions for the dddmp package

By: Gianpiero Cabodi and Stefano Quer

()

Checks for fatal bugs

()

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

()

Checks for fatal bugs and return the DDDMP_FAILURE flag.

()

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

By: Gianpiero Cabodi and Stefano Quer

()

Memory Allocation Macro for DDDMP

()

Memory Free Macro for DDDMP

By: Gianpiero Cabodi and Stefano Quer

Input and output BDD codes and integers from/to file in binary mode. DD node codes are written as one byte. Integers of any length are written as sequences of "linked" bytes. For each byte 7 bits are used for data and one (MSBit) as link with a further byte (MSB = 1 means one more byte). Low level read/write of bytes filter , and with escape sequences.

DddmpWriteCode()

Writes 1 byte node code

DddmpReadCode()

Reads a 1 byte node code

DddmpWriteInt()

Writes a "packed integer"

DddmpReadInt()

Reads a "packed integer"

WriteByteBinary()

Writes a byte to file filtering , and

ReadByteBinary()

Reads a byte from file with escaped , and

By: Gianpiero Cabodi and Stefano Quer

Conversion between ASCII and binary formats is presently supported by loading a BDD in the source format and storing it in the target one. We plan to introduce ad hoc procedures avoiding explicit BDD node generation.

Dddmp_Text2Bin()

Converts from ASCII to binary format

Dddmp_Bin2Text()

Converts from binary to ASCII format

By: Gianpiero Cabodi and Stefano Quer

Functions to display BDD files in binary format

Dddmp_cuddBddDisplayBinary()

Display a binary dump file in a text file

By: Gianpiero Cabodi and Stefano Quer

Functions to handle BDD node infos and numbering.

DddmpNumberDdNodes()

Removes nodes from unique table and number them

DddmpUnnumberDdNodes()

Restores nodes in unique table, loosing numbering

DddmpWriteNodeIndex()

Write index to node

DddmpReadNodeIndex()

Reads the index of a node

DddmpVisited()

Returns true if node is visited

DddmpSetVisited()

Marks a node as visited

DddmpClearVisited()

Marks a node as not visited

NumberNodeRecur()

Number nodes recursively in post-order

RemoveFromUniqueRecur()

Removes a node from unique table

RestoreInUniqueRecur()

Restores a node in unique table

By: Gianpiero Cabodi and Stefano Quer

Functions to handle BDD node infos and numbering while storing a CNF formula from a BDD or an array of BDDs.

DddmpNumberDdNodesCnf()

Removes nodes from unique table and numbers them

DddmpDdNodesCountEdgesAndNumber()

Removes nodes from unique table and numbers each node according to the number of its incoming BDD edges.

DddmpUnnumberDdNodesCnf()

Restores nodes in unique table, loosing numbering

DddmpPrintBddAndNext()

Prints debug information

DddmpWriteNodeIndexCnfBis()

Write index to node

DddmpWriteNodeIndexCnf()

Write index to node

DddmpReadNodeIndexCnf()

Reads the index of a node

DddmpClearVisitedCnfRecur()

Mark ALL nodes as not visited

DddmpVisitedCnf()

Returns true if node is visited

DddmpSetVisitedCnf()

Marks a node as visited

DddmpClearVisitedCnf()

Marks a node as not visited

NumberNodeRecurCnf()

Number nodes recursively in post-order

DddmpDdNodesCheckIncomingAndScanPath()

Number nodes recursively in post-order

DddmpDdNodesNumberEdgesRecur()

Number nodes recursively in post-order

DddmpDdNodesResetCountRecur()

Resets counter and visited flag for ALL nodes of a BDD

DddmpDdNodesCountEdgesRecur()

Counts the number of incoming edges for each node of a BDD

RemoveFromUniqueRecurCnf()

Removes a node from unique table

RestoreInUniqueRecurCnf()

Restores a node in unique table

DddmpPrintBddAndNextRecur()

Prints debug info

By: Gianpiero Cabodi and Stefano Quer

Functions to read in bdds to file. BDDs are represended on file either in text or binary format under the following rules. A file contains a forest of BDDs (a vector of Boolean functions). BDD nodes are numbered with contiguous numbers, from 1 to NNodes (total number of nodes on a file). 0 is not used to allow negative node indexes for complemented edges. A file contains a header, including information about variables and roots to BDD functions, followed by the list of nodes. BDD nodes are listed according to their numbering, and in the present implementation numbering follows a post-order strategy, in such a way that a node is never listed before its Then/Else children.

Dddmp_cuddBddLoad()

Reads a dump file representing the argument BDD.

Dddmp_cuddBddArrayLoad()

Reads a dump file representing the argument BDDs.

Dddmp_cuddAddLoad()

Reads a dump file representing the argument ADD.

Dddmp_cuddAddArrayLoad()

Reads a dump file representing the argument ADDs.

Dddmp_cuddHeaderLoad()

Reads the header of a dump file representing the argument BDDs

DddmpCuddDdArrayLoad()

Reads a dump file representing the argument BDDs.

DddmpBddReadHeader()

Reads a the header of a dump file representing the argument BDDs.

DddmpFreeHeader()

Frees the internal header structure.

By: Gianpiero Cabodi and Stefano Quer

Functions to read in CNF from file as BDDs.

Dddmp_cuddBddLoadCnf()

Reads a dump file in a CNF format.

Dddmp_cuddBddArrayLoadCnf()

Reads a dump file in a CNF format.

Dddmp_cuddHeaderLoadCnf()

Reads the header of a dump file representing the argument BDDs

DddmpCuddDdArrayLoadCnf()

Reads a dump file representing the argument BDDs in CNF format.

DddmpBddReadHeaderCnf()

Reads a the header of a dump file representing the argument BDDs.

DddmpFreeHeaderCnf()

Frees the internal header structure.

DddmpReadCnfClauses()

Read the CNF clauses from the file in the standard DIMACS format.

DddmpCnfClauses2Bdd()

Transforms CNF clauses into BDDs.

By: Gianpiero Cabodi and Stefano Quer

Functions to handle ADD node infos and numbering.

DddmpNumberAddNodes()

Removes nodes from unique table and number them

DddmpUnnumberAddNodes()

Restores nodes in unique table, loosing numbering

DddmpWriteNodeIndexAdd()

Write index to node

DddmpReadNodeIndexAdd()

Reads the index of a node

DddmpVisitedAdd()

Returns true if node is visited

DddmpSetVisitedAdd()

Marks a node as visited

DddmpClearVisitedAdd()

Marks a node as not visited

NumberNodeRecurAdd()

Number nodes recursively in post-order

RemoveFromUniqueRecurAdd()

Removes a node from unique table

RestoreInUniqueRecurAdd()

Restores a node in unique table

By: Gianpiero Cabodi and Stefano Quer

Functions to handle BDD node infos and numbering.

DddmpNumberBddNodes()

Removes nodes from unique table and number them

DddmpUnnumberBddNodes()

Restores nodes in unique table, loosing numbering

DddmpWriteNodeIndexBdd()

Write index to node

DddmpReadNodeIndexBdd()

Reads the index of a node

DddmpVisitedBdd()

Returns true if node is visited

DddmpSetVisitedBdd()

Marks a node as visited

DddmpClearVisitedBdd()

Marks a node as not visited

NumberNodeRecurBdd()

Number nodes recursively in post-order

RemoveFromUniqueRecurBdd()

Removes a node from unique table

RestoreInUniqueRecurBdd()

Restores a node in unique table

By: Gianpiero Cabodi and Stefano Quer

Functions to handle BDD node infos and numbering while storing a CNF formula from a BDD or an array of BDDs.

DddmpNumberDdNodesCnf()

Removes nodes from unique table and numbers them

DddmpDdNodesCountEdgesAndNumber()

Removes nodes from unique table and numbers each node according to the number of its incoming BDD edges.

DddmpUnnumberDdNodesCnf()

Restores nodes in unique table, loosing numbering

DddmpPrintBddAndNext()

Prints debug information

DddmpWriteNodeIndexCnf()

Write index to node

DddmpVisitedCnf()

Returns true if node is visited

DddmpSetVisitedCnf()

Marks a node as visited

DddmpReadNodeIndexCnf()

Reads the index of a node

DddmpWriteNodeIndexCnfWithTerminalCheck()

Write index to node

DddmpClearVisitedCnfRecur()

Mark ALL nodes as not visited

DddmpClearVisitedCnf()

Marks a node as not visited

NumberNodeRecurCnf()

Number nodes recursively in post-order

DddmpDdNodesCheckIncomingAndScanPath()

Number nodes recursively in post-order

DddmpDdNodesNumberEdgesRecur()

Number nodes recursively in post-order

DddmpDdNodesResetCountRecur()

Resets counter and visited flag for ALL nodes of a BDD

DddmpDdNodesCountEdgesRecur()

Counts the number of incoming edges for each node of a BDD

RemoveFromUniqueRecurCnf()

Removes a node from unique table

RestoreInUniqueRecurCnf()

Restores a node in unique table

DddmpPrintBddAndNextRecur()

Prints debug info

By: Gianpiero Cabodi and Stefano Quer

Functions to write ADDs to file. ADDs are represended on file either in text or binary format under the following rules. A file contains a forest of ADDs (a vector of Boolean functions). ADD nodes are numbered with contiguous numbers, from 1 to NNodes (total number of nodes on a file). 0 is not used to allow negative node indexes for complemented edges. A file contains a header, including information about variables and roots to ADD functions, followed by the list of nodes. ADD nodes are listed according to their numbering, and in the present implementation numbering follows a post-order strategy, in such a way that a node is never listed before its Then/Else children.

Dddmp_cuddAddStore()

Writes a dump file representing the argument ADD.

Dddmp_cuddAddArrayStore()

Writes a dump file representing the argument Array of ADDs.

DddmpCuddDdArrayStoreBdd()

Writes a dump file representing the argument Array of BDDs/ADDs.

NodeStoreRecurAdd()

Performs the recursive step of Dddmp_bddStore.

NodeTextStoreAdd()

Store One Single Node in Text Format.

By: Gianpiero Cabodi and Stefano Quer

Functions to write BDDs to file. BDDs are represended on file either in text or binary format under the following rules. A file contains a forest of BDDs (a vector of Boolean functions). BDD nodes are numbered with contiguous numbers, from 1 to NNodes (total number of nodes on a file). 0 is not used to allow negative node indexes for complemented edges. A file contains a header, including information about variables and roots to BDD functions, followed by the list of nodes. BDD nodes are listed according to their numbering, and in the present implementation numbering follows a post-order strategy, in such a way that a node is never listed before its Then/Else children.

Dddmp_cuddBddStore()

Writes a dump file representing the argument BDD.

Dddmp_cuddBddArrayStore()

Writes a dump file representing the argument Array of BDDs.

DddmpCuddBddArrayStore()

Writes a dump file representing the argument Array of BDDs.

NodeStoreRecurBdd()

Performs the recursive step of Dddmp_bddStore.

NodeTextStoreBdd()

Store One Single Node in Text Format.

NodeBinaryStoreBdd()

Store One Single Node in Binary Format.

By: Gianpiero Cabodi and Stefano Quer

Functions to write out BDDs to file in a CNF format.

Dddmp_cuddBddStoreCnf()

Writes a dump file representing the argument BDD in a CNF format.

Dddmp_cuddBddArrayStoreCnf()

Writes a dump file representing the argument array of BDDs in CNF format.

DddmpCuddBddArrayStoreCnf()

Writes a dump file representing the argument Array of BDDs in the CNF standard format.

StoreCnfNodeByNode()

Store the BDD as CNF clauses.

StoreCnfNodeByNodeRecur()

Performs the recursive step of Dddmp_bddStore.

StoreCnfOneNode()

Store One Single BDD Node.

StoreCnfMaxtermByMaxterm()

Prints a disjoint sum of products.

StoreCnfBest()

Prints a disjoint sum of products with intermediate cutting points.

StoreCnfMaxtermByMaxtermRecur()

Performs the recursive step of Print Maxterm.

StoreCnfBestNotSharedRecur()

Performs the recursive step of Print Best on Not Shared sub-BDDs.

StoreCnfBestSharedRecur()

Performs the recursive step of Print Best on Shared sub-BDDs.

printCubeCnf()

Print One Cube in CNF Format.

By: Gianpiero Cabodi and Stefano Quer

Functions to write out bdds to file. BDDs are represended on file in text format. Each node is stored as a multiplexer in a prefix notation format for the prefix notation file or in PLA format for the blif file.

Dddmp_cuddBddStorePrefix()

Writes a dump file representing the argument BDD in a prefix notation.

Dddmp_cuddBddArrayStorePrefix()

Writes a dump file representing the argument BDD in a prefix notation.

Dddmp_cuddBddStoreBlif()

Writes a dump file representing the argument BDD in a Blif/Exlif notation.

Dddmp_cuddBddArrayStoreBlif()

Writes a dump file representing the argument BDD in a Blif/Exlif notation.

Dddmp_cuddBddStoreSmv()

Writes a dump file representing the argument BDD in a prefix notation.

Dddmp_cuddBddArrayStoreSmv()

Writes a dump file representing the argument BDD in a prefix notation.

DddmpCuddDdArrayStorePrefix()

Internal function to writes a dump file representing the argument BDD in a prefix notation.

DddmpCuddDdArrayStorePrefixBody()

Internal function to writes a dump file representing the argument BDD in a prefix notation. Writes the body of the file.

DddmpCuddDdArrayStorePrefixStep()

Performs the recursive step of DddmpCuddDdArrayStorePrefixBody.

DddmpCuddDdArrayStoreBlif()

Writes a blif file representing the argument BDDs.

DddmpCuddDdArrayStoreBlifBody()

Writes a blif body representing the argument BDDs.

DddmpCuddDdArrayStoreBlifStep()

Performs the recursive step of DddmpCuddDdArrayStoreBlif.

DddmpCuddDdArrayStoreSmv()

Internal function to writes a dump file representing the argument BDD in a SMV notation.

DddmpCuddDdArrayStoreSmvBody()

Internal function to writes a dump file representing the argument BDD in a SMV notation. Writes the body of the file.

DddmpCuddDdArrayStoreSmvStep()

Performs the recursive step of DddmpCuddDdArrayStoreSmvBody.

By: Gianpiero Cabodi and Stefano Quer

Functions to manipulate arrays.

QsortStrcmp()

String compare for qsort

FindVarname()

Performs binary search of a name within a sorted array

DddmpStrDup()

Duplicates a string

DddmpStrArrayDup()

Duplicates an array of strings

DddmpStrArrayRead()

Inputs an array of strings

DddmpStrArrayWrite()

Outputs an array of strings

DddmpStrArrayFree()

Frees an array of strings

DddmpIntArrayDup()

Duplicates an array of ints

DddmpIntArrayRead()

Inputs an array of ints

DddmpIntArrayWrite()

Outputs an array of ints