Project links Homepage. Maintainers a. Project description Project details Release history Download files Project description :warning: Note :warning: This is a work in progress; please do not use this repo yet. How to Help As soon as the contributing guide is up, and master is protected, we can start accepting PRs. Dependencies cudd 3. Project details Project links Homepage. Download files Download the file for your platform.
Files for pycudd, version 1. Close Hashes for pycudd Some platforms require specific compiler and linker flags. Refer to the Makefile in the top-level directory of the distribution. An example of a Makefile is the following: Makefile. This function prints out useful statistics including the number of nodes, the number of leaves, and the number of minterms.
The lines below show the statistics dumped to a file:. You should provide an output file pointer, the DD manager, the number of nodes and the node array pointer. The following functions show how to print a DD to a file. Once you generate the. Graphviz is open source graph visualization software. It works very well for representing structural information as diagrams of abstract graphs and networks. GraphViz is available for download here: www.
Just locate the. Common manipulations of BDDs can be accomplished by calling operators on variables. Especially if the application does use the infinities.
See the Makefile for the details. Epsilon : This constant, initially set to , is used in comparing floating point values for equality. Unlike the other constants, it does not correspond to a node. Background The background value is a constant typically used to represent non-existing arcs in graphs. Consider a shortest path problem. Two nodes that are not connected by an arc can be regarded as being joined by an arc of infinite length. In shortest path problems, it is therefore convenient to set the background value to PlusInfinity.
In network flow problems, on the other hand, two nodes not connected by an arc can be regarded as joined by an arc of 0 capacity. For these problems, therefore, it is more convenient to set the background value to 0.
In general, when representing sparse matrices, the background value is the value that is assumed implicitly. At initialization, the background value is set to 0. This function will retrieve the ADD for the desired constant, if it already exist, or it will create a new one.
Obviously, new constants should only be used when manipulating ADDs. Creating Variables Decision diagrams are typically created by combining simpler decision diagrams. The simplest decision diagrams, of course, cannot be created in that way. Constant functions have been discussed in Section 3. In this section we discuss the simple variable functions, also known as projection functions.
A projection function for BDDs consists of an internal node with both outgoing arcs pointing to the constant 1. The else arc is complemented. An ADD projection function, on the other hand, has the else pointer directed to the arithmetic zero function. One should never mix the two types of variables. If the function does not exist, it is created. In addition it allows to specify the position in the variable order at which the new variable should be inserted.
Therefore the ZDDs of the projection functions change when new variables are added. This will be discussed in Section 3. Here we assume that the number of variables is fixed. This function takes three BDDs, , , and , as arguments and computes.
The following fragment of code illustrates how to build the BDD for the function. The new f must be assigned to a temporary variable tmp in this example. One has to be careful, though, to fix the order of conjunction before entering the loop. Otherwise, if reordering takes place, it is possible to use one variable twice and skip another variable.
This function can apply a wide variety of operators to a pair of ADDs. Among the available operators are addition, multiplication, division, minimum, maximum, and boolean operators that work on ADDs whose leaves are restricted to 0 and 1 ADDs. The following fragment of code illustrates how to build the ADD for the function. It is therefore necessary to reference and dereference them. However, it is also possible to build ZDDs by applying boolean operators to other ZDDs, starting from constants and projection functions.
The following fragment of code illustrates how to build the ZDD for the function. We assume that the four variables already exist in the manager when the ZDD for is built. Note the use of De Morgan's law. Complementation is obtained by subtracting from the constant 1 function. These functions expect the two ZDD variables corresponding to the two literals of the function variable to be adjacent.
One has to create variable groups see Section 3. This approach eliminates the difficulties that arise when the number of ZDD variables changes while ZDDs are being built. ZDDs are quite often used for the representation of covers.
This is normally done by associating two ZDD variables to each variable of the function. And hence, typically, to each BDD variable. Suppose, for instance, that two variables are initially created, and that the ZDD for is built. If a third variable is added, say , then the ZDD represents instead. This change in function obviously applies regardless of what use is made of the ZDD. However, if the ZDD is used to represent a cover , the cover itself is not changed by the addition of new variable.
What changes is the characteristic function of the cover. Some of them are slight variations of existing techniques [ 16 , 6 , 2 , 10 , 15 , 11 ]; some others have been developed specifically for this package [ 14 , 13 ]. Reordering affects a unique table. ZDDs, on the other hand, are reordered separately. Reordering for ZDDs is the subject of Section 3. Or it can be automatically triggered by the package when the number of nodes has reached a given threshold. The threshold is initialized and automatically adjusted after each reordering by the package.
For many methods, the reordering procedure is iterated until no further improvement is obtained. We call these methods the converging methods. When constraints are imposed on the relative position of variables see Section 3. The groups themselves are reordered by sifting.
0コメント