Rendering CUDD Diagrams with GraphViz (C++ API)

Instructions and tips for rendering [A/B/Z]DDs as GraphViz dot files with CUDD's C++ API.

// The array of variable names (inputs).
const char* inames[2] = {"x", "y"};            // Replace as appropriate.
// The array of function names (outputs).
const char* onames[3] = {"f", "g", "h"};       // Replace as appropriate.

// Create a vector (dynamically sized array in C++) of
// the BDDs to include in the graph.
std::vector<BDD> diagrams = {f, g, h};         // Replace as appropriate.

// Open the file and write the graph.
FILE* output = fopen("preview.dot", "w");
bddManager.DumpDot(diagrams, inames, onames, output);
fclose(output);
    

You can then use the following command to convert the .dot file to a .pdf file:

dot -Tpdf preview.dot > preview.pdf

Or, alternatively, to a .png file:

dot -Tpng preview.dot > preview.png

DumpDot

DumpDot takes four parameters:

1. diagrams The std::vector of diagrams to render. (This is either a vector of BDDs, ADDs or ZDDs).

2. inames (input names) The names of atomic variables. These should be in the same order as the variables are defined.

3. onames (output names) The names of the functions being rendered (i.e., for each diagram in diagrams, specify the name - in the order they are defined in diagrams).

4. output (the output file) The FILE* pointer that the output should be written to. This should be created with a call to fopen, and subsequently closed with fclose after the call to DumpDot.

Cudd bddManager = Cudd(0, 0);

// ...

bddManager.DumpDot(
    diagrams,    // The vector of diagrams to render.
                 // A C++ vector is a way of representing dynamically
                 // sized arrays in C++.
                 
    inames,      // The names of variables (input values).
    onames,      // The names of functions (output values).

    output       // The output file.
);

Some compilers allow diagrams to be defined short-hand, e.g.,

bddManager.DumpDot({a, b, c}, /* ... */);

However some compilers report conflicting types when this occurs, which can be mitigated by specifying the vector on a line of its own with the type (either std::vector<bdd>, std::vector<add> or std::vector<zdd>:

std::vector<BDD> diagrams = {a, b, c};
bddManager.DumpDot(diagrams, /* ... */);

Example

The above example is shown here for greater compatibility.

Figure 1: Output of the BDD DumpDot code.

Note that:

• onames are counter-intuitively seen at the top of the graph, because the term outputs indicates the resulting truth values of the functions (i.e., the BDDs that were selected to be rendered).

• inames are shown on the LHS, as this indicates the atomic variables defined. All nodes on the same level indicate the same variable.

Rendering (Binary Decision Diagrams) BDDs as (Algebraic Decision Diagrams) ADDs

As seen in the previous example, the output is a single leaf node. CUDD's Binary Decision Diagrams use complemented edges for a more compact representation. The (dashed) "else" nodes are formed by negating low edges (and annotating them as dashed).

The main, most noticeable impact of this, as seen in the example above is that there is only one leaf node (for true; on account of the fact that high edges are, naturally, not negated).

Algebraic Decision Diagrams, ADDs, have a range of more than false/0 and true/1 which means computing complemented edges is impossible (or, at least, has no benefit), so to view a BDD with both leaf nodes for false and true, simply render the BDDs as ADDs, to produce the result as follows:

Figure 2: The previous BDD example, converted to ADD.

// Assuming that a, b and c are BDDs, the following will convert
// each to an ADD and create a vector from it.
std::vector<ADD> diagrams = {a.Add(), b.Add(), c.Add()};
bddManager.DumpDot(diagrams, /* ... */);

Another approach to automaticaly convert a vector of BDDs to ADDs, using std::transform is as follows:

// ...
std::vector<BDD> bdds = {f, g, h};  // e.g., diagrams from the
                                    // previous example.
    
// Convert BDDs to ADDs
std::vector<ADD> adds;      // Initialize vector for ADDs.
adds.resize(bdds.size());   // Resize ADDs vector to size of BDDs vector.

std::transform(
    bdds.begin(), bdds.end(),    // Start and end of original vector.
    adds.begin(),                // Start of new vector.
    // Lambda that converts a BDD to an ADD.
    // Simply by calling .Add() on the BDD (as above).
    [](BDD bdd) -> ADD { return bdd.Add(); }
);

Tips

Alternatively on *nix systems (i.e., Linux and macOS), include the following in the C++ code to automatically convert the .dot file to a .pdf file as part of the program invocation:

system("/path/to/dot -Tpdf preview.dot > preview.pdf");

You can install Skim on macOS, which has the ability to automatically reload PDF files as they change (click for instructions).

Note, naturally, that preview.dot refers to the file opened with fopen in the first code block. preview.pdf is the name of the output file (once converted by the dot command and may be whatever you choose).

Your C++ program does not necessarily run with your user PATH. So if you just use dot instead of the full path to the dot command on your system, you will likely get an error due to the missing file.

You can run which dot in the Terminal to find the full path to the dot command.