Storing BDD in a file using CUDD/DDDMP package?

Question

I have successfully created BDD using CUDD package. I am also able to visualize it using some already built tool. I am interested in storing BDD in a file using DDDMP package of CUDD. I read that Dddmp_cuddBddStore() is doing that for us. I am not able to find any examples of using that function. Its arguments are a little complex. Any small example using that function will be a great help.

Answer 1

An interface to the DDDMP package is available with the Cython bindings to CUDD of the Python package dd. An example that creates the BDD of a Boolean function, saves it to a DDDMP file, and then loads it from that file, is the following.

from dd import cudd as _bdd

bdd = _bdd.BDD()
bdd.declare('x', 'y')

# The BDD node for the conjunction of variables x and y
u = bdd.add_expr('x /\ y')

# save to a DDDMP file (the file extension matters,
# for example a PDF extension would result in plotting
# a diagram using GraphViz)
bdd.dump('storage.dddmp', [u])

# load the BDD from the DDDMP file
u_ = bdd.load('storage.dddmp')
assert u == u_, (u, u_)

The source code of the Cython module dd/cudd.pyx includes an example of how to use the functions Dddmp_cuddBddStore and Dddmp_cuddBddLoad

https://github.com/tulip-control/dd/blob/b625dd46120e2e1f5a12190332e6191d07681ee8/dd/cudd.pyx#L1157-L1222

Installation of dd with the module dd.cudd is described here and could be summarized as

pip download dd --no-deps
tar -xzf dd-*.tar.gz
cd dd-*/
python setup.py install --fetch --cudd

This will download and build CUDD, and build and install the Cython bindings of dd to CUDD.

Answer 2

I am a bit late here. Still this may useful. Storing BDD in a file is trivial and can be done by either CUDD itself or any of the wrappers available (Python's DD for instance). However I have found no working reading example. After some digging of dddmp tests I have made a quick and dirty solution to read dddmp file. Sample below reads test.dddmp and saves it as test.dot (Graphviz format) without complemented edges.

//parts adapted from cudd/dddmp/testdddmp.c and cudd/dddmp/dddmpInt.h
// ReSharper disable CppDeprecatedEntity
// ReSharper disable CppClangTidyCertErr33C
#include <iostream>
#include <stdio.h>
#include <stdexcept>
#include <stdlib.h>
#include <stdexcept>
#include "cudd.h"
#include "dddmp.h"

using namespace std;

#define MY_MAX_STRING_LENGTH 80


/**Macro***********************************************************************

  Synopsis     [Memory Free Macro for DDDMP]

  Description  []

  SideEffects  [None]

  SeeAlso      []

******************************************************************************/
#ifdef FREE
#define DDDMP_FREE(p)  (FREE(p))
#else
#define DDDMP_FREE(p)   \
    ((p)!=NULL)?(free(p)):0)
#endif


/**Macro***********************************************************************

  Synopsis     [Memory Allocation Macro for DDDMP]

  Description  []

  SideEffects  [None]

  SeeAlso      []

******************************************************************************/
#ifdef ALLOC
#  define DDDMP_ALLOC(type, num)    ALLOC(type,num)
#else
#  define DDDMP_ALLOC(type, num)    \
     ((type *) malloc(sizeof(type) * (num)))
#endif


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/
using dddmpVarInfo_t = struct dddmpVarInfo
{
    /*
     *  Local Information
     */

    int nDdVars; /* Local Manager Number of Variables */
    char** rootNames; /* Root Names */

    /*
     *  Header File Information
     */

    Dddmp_DecompType ddType;

    int nVars; /* File Manager Number of Variables */
    int nSuppVars; /* File Structure Number of Variables */

    int varNamesFlagUpdate; /* 0 to NOT Update */
    char** suppVarNames;
    char** orderedVarNames;

    int varIdsFlagUpdate; /* 0 to NOT Update */
    int* varIds; /* File ids - nSuppVars size */
    int* varIdsAll; /* ALL ids - nVars size */

    int varComposeIdsFlagUpdate; /* 0 to NOT Update */
    int* varComposeIds; /* File permids - nSuppVars size */
    int* varComposeIdsAll; /* ALL permids - nVars size */

    int varAuxIdsFlagUpdate; /* 0 to NOT Update */
    int* varAuxIds; /* File auxids - nSuppVars size */
    int* varAuxIdsAll; /* ALL auxids  - nVars size */

    int nRoots;
};


/**
* Writes a dot file representing the argument DDs
* @param gbm node object
* @param dd
* @param filename file name; stdout if null
* @param var_names
* @param start_node_names
*/
void write_dot(
    DdManager* gbm
    , DdNode* dd
    , char* filename = nullptr
    , char* var_names[] = nullptr
    , char* start_node_names[] = nullptr)
{
    FILE* outfile = nullptr; // output file pointer for .dot file
    bool err = false;
    try
    {
        if (filename == nullptr)
        {
            outfile = stdout;
        }
        else
        {
            const errno_t err1 = fopen_s(&outfile, filename, "w");
            if (err1 != 0) { throw invalid_argument("Cannot open output file for writing"); }
        }

        const int res = Cudd_DumpDot(gbm, 1, &dd, var_names, start_node_names, outfile);
        // dump the function to .dot file
        if (res != 1) { throw invalid_argument("Cudd_DumpDot failed"); }
    }
    catch (invalid_argument& e)
    {
        std::cerr << e.what() << endl;
        err = true;
    }
    try
    {
        if (outfile != nullptr && outfile != stdout)
        {
            const int res = fclose(outfile); // close the file */
            if (res != 0) throw runtime_error("file closing error");
        }
    }
    catch (...)
    {
        std::cerr << "file closing error" << endl;
        err = true;
    }
    if (!err)
    {
        printf("File %s written successfully\n", (filename == nullptr ? "stdout" : filename));
    }
}


/**Function********************************************************************

  Synopsis     [Create a CUDD Manager with nVars variables.]

  Description  [Create a CUDD Manager with nVars variables.]

  SideEffects  []

  SeeAlso      []

******************************************************************************/
static DdManager*
init_ddmanager(
    dddmpVarInfo_t* varInfo
    , int nVars = 50)
{
    DdManager* dd_mgr;

    /*----------------------- Init Var Information Structure ------------------*/

    varInfo->nDdVars = nVars;

    varInfo->rootNames = nullptr;
    varInfo->ddType = DDDMP_NONE;
    varInfo->nVars = (-1);
    varInfo->nSuppVars = (-1);
    varInfo->varNamesFlagUpdate = 1;
    varInfo->suppVarNames = nullptr;
    varInfo->orderedVarNames = nullptr;
    varInfo->varIdsFlagUpdate = 1;
    varInfo->varIds = nullptr;
    varInfo->varIdsAll = nullptr;
    varInfo->varComposeIdsFlagUpdate = 1;
    varInfo->varComposeIds = nullptr;
    varInfo->varComposeIdsAll = nullptr;
    varInfo->varAuxIdsFlagUpdate = 1;
    varInfo->varAuxIds = nullptr;
    varInfo->varAuxIdsAll = nullptr;
    varInfo->nRoots = (-1);

    /*------------------------------ Init DD Manager --------------------------*/

    dd_mgr = Cudd_Init(
        nVars
        , 0
        ,CUDD_UNIQUE_SLOTS
        ,CUDD_CACHE_SLOTS
        , 0);

    Dddmp_CheckAndReturn(dd_mgr==NULL, "DdManager NOT inizializated.");

    return (dd_mgr);
}


/**Function********************************************************************

  Synopsis    [Frees an array of strings]

  Description [Frees memory for strings and the array of pointers]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static void
util_dddmp_str_array_free(
    char** array /* IN: array of strings */,
    int n /* IN: size of the array */
)
{
    int i;

    if (array == nullptr)
    {
        return;
    }

    for (i = 0; i < n; i++)
    {
        DDDMP_FREE(array[i]);
    }

    DDDMP_FREE(array);
}


/**Function********************************************************************

  Synopsis     [Complete the internal manager structure for subsequent
    BDD/ADD/CNF operations.
  ]

  Description  [Complete the internal manager structure for subsequent
    BDD/ADD/CNF operations.
    The phylosophy is simple: to have proper names and ids it is necessary
    to load an header before each actual load/store operation.
    An header load should initialize variable names, variable ids,
    variable compose ids, and variable auxiliary ids for all variables
    stored in the file.
    This information has to be extended for all variables in the
    *current* CUDD manager (before any store operation).
    CompleteInfoStruct does this job.
    Arrays varIds, varComposeIds, and varAuxIds contain information for
    all the variable in the BDD/ADD/CNF while arrays varIdsAll,
    varComposeIdsAll, and varAuxIdsAll contain information for *all*
    variable in the current CUDD manager.
  ]


  SideEffects  []

  SeeAlso      []

******************************************************************************/
static int
util_fillup_varinfo_struct(
    Dddmp_DecompType ddType /* IN: selects the proper decomp type */,
    int nVars /* IN: number of DD variables */,
    int nSuppVars /* IN: number of support variables */,
    char** suppVarNames /* IN: array of support variable names */,
    char** orderedVarNames /* IN: array of variable names */,
    int* varIds /* IN: array of variable ids */,
    int* varComposeIds /* IN: array of permids ids */,
    int* varAuxIds /* IN: array of variable aux ids */,
    int nRoots /* IN: number of root in the file */,
    dddmpVarInfo_t* varInfo /* IN: Variable Information */
)
{
    int i;
    char tmpString[MY_MAX_STRING_LENGTH];

    /*------------------------- Updates Variable Names ------------------------*/

    util_dddmp_str_array_free(varInfo->suppVarNames, varInfo->nSuppVars);
    varInfo->suppVarNames = suppVarNames;

    if (varInfo->varNamesFlagUpdate == 1)
    {
        util_dddmp_str_array_free(varInfo->orderedVarNames, varInfo->nVars);

        if (orderedVarNames != nullptr)
        {
            varInfo->orderedVarNames = orderedVarNames;
        }
        else
        {
            varInfo->orderedVarNames = DDDMP_ALLOC(char*, nVars);
            Dddmp_CheckAndReturn(varInfo->orderedVarNames == NULL,
                                 "Allocation error.");

            for (i = 0; i < nVars; i++)
            {
                varInfo->orderedVarNames[i] = nullptr;
            }

            if (varInfo->suppVarNames != nullptr)
            {
                for (i = 0; i < nSuppVars; i++)
                {
                    varInfo->orderedVarNames[i] = DDDMP_ALLOC(char,
                                                              (strlen(varInfo->suppVarNames[i]) + 1));
                    strcpy(varInfo->orderedVarNames[i], varInfo->suppVarNames[i]);
                }
            }

            for (i = 0; i < nVars; i++)
            {
                if (varInfo->orderedVarNames[i] == nullptr)
                {
                    sprintf(tmpString, "DUMMY%d", i);
                    varInfo->orderedVarNames[i] = DDDMP_ALLOC(char,
                                                              (strlen(tmpString) + 1));
                    strcpy(varInfo->orderedVarNames[i], tmpString);
                }
            }
        }
    }

    /*------------------------------ Updates IDs ------------------------------*/

    DDDMP_FREE(varInfo->varIds);
    varInfo->varIds = varIds;

    if (varInfo->varIdsFlagUpdate == 1)
    {
        /* Free Previously Allocated Memory */
        DDDMP_FREE(varInfo->varIdsAll);

        /* Allocate New Memory and Check */
        varInfo->varIdsAll = DDDMP_ALLOC(int, nVars);
        Dddmp_CheckAndReturn(varInfo->varIdsAll == NULL, "Allocation error.");

        /* Set New Values */
        for (i = 0; i < nVars; i++)
        {
            varInfo->varIdsAll[i] = (-1);
        }

        if (varInfo->varIds != nullptr)
        {
            for (i = 0; i < nSuppVars; i++)
            {
                varInfo->varIdsAll[varInfo->varIds[i]] = varInfo->varIds[i];
            }
        }
    }


    /*-------------------------- Updates Compose IDs --------------------------*/

    DDDMP_FREE(varInfo->varComposeIds);
    varInfo->varComposeIds = varComposeIds;

    if (varInfo->varComposeIdsFlagUpdate == 1)
    {
        /* Free Previously Allocated Memory */
        DDDMP_FREE(varInfo->varComposeIdsAll);

        /* Allocate New Memory and Check */
        varInfo->varComposeIdsAll = DDDMP_ALLOC(int, nVars);
        Dddmp_CheckAndReturn(varInfo->varComposeIdsAll == NULL,
                             "Allocation error.");

        /* Set New Values */
        for (i = 0; i < nVars; i++)
        {
            varInfo->varComposeIdsAll[i] = (-1);
        }

        if (varInfo->varComposeIds != nullptr)
        {
            for (i = 0; i < nSuppVars; i++)
            {
                varInfo->varComposeIdsAll[varInfo->varIds[i]] =
                    varInfo->varComposeIds[i];
            }
        }
    }

    /*------------------------- Updates Auxiliary IDs -------------------------*/

    DDDMP_FREE(varInfo->varAuxIds);
    varInfo->varAuxIds = varAuxIds;

    if (varInfo->varAuxIdsFlagUpdate == 1)
    {
        /* Free Previously Allocated Memory */
        DDDMP_FREE(varInfo->varAuxIdsAll);

        /* Allocate New Memory and Check */
        varInfo->varAuxIdsAll = DDDMP_ALLOC(int, nVars);
        Dddmp_CheckAndReturn(varInfo->varAuxIdsAll == NULL, "Allocation error.");

        /* Set New Values */
        for (i = 0; i < nVars; i++)
        {
            varInfo->varAuxIdsAll[i] = (-1);
        }

        if (varInfo->varAuxIds != nullptr)
        {
            for (i = 0; i < nSuppVars; i++)
            {
                varInfo->varAuxIdsAll[varInfo->varIds[i]] = varInfo->varAuxIds[i];
            }
        }
    }

    /*----------------------------- Updates Sizes -----------------------------*/

    varInfo->ddType = ddType;
    varInfo->nVars = nVars;
    varInfo->nSuppVars = nSuppVars;
    Dddmp_CheckAndReturn(varInfo->nDdVars < varInfo->nVars,
                         "Local Manager with Not Enough Variables.");
    varInfo->nRoots = nRoots;

    return (DDDMP_SUCCESS);
}


/**Function********************************************************************

  Synopsis     [Read the Header of a file containing a BDD.]

  Description  [File name Selection.]

  SideEffects  []

  SeeAlso      []

******************************************************************************/
static int
load_header_from_dddmp_file(
    dddmpVarInfo_t* varInfo /* IN/OUT: Variable Information */
    , char* fileName
)
{
    Dddmp_DecompType ddType;
    int retValue, nRoots, nVars, nSuppVars;
    int* tmpVarIds = nullptr;
    int* tmpVarAuxIds = nullptr;
    int* tmpVarComposeIds = nullptr;
    char** tmpOrderedVarNames = nullptr;
    char** tmpSuppVarNames = nullptr;

    /*------------------------ Read Operation Operands ------------------------*/

    retValue = Dddmp_cuddHeaderLoad(&ddType, &nVars, &nSuppVars,
                                    &tmpSuppVarNames, &tmpOrderedVarNames, &tmpVarIds, &tmpVarComposeIds,
                                    &tmpVarAuxIds, &nRoots, fileName, nullptr);

    if (retValue == DDDMP_FAILURE)
    {
        return (DDDMP_FAILURE);
    }

    /*---------------------------- Tail Operations ----------------------------*/

    util_fillup_varinfo_struct(ddType, nVars, nSuppVars,
                               tmpSuppVarNames, tmpOrderedVarNames, tmpVarIds, tmpVarComposeIds,
                               tmpVarAuxIds, nRoots, varInfo);

    return (DDDMP_SUCCESS);
}


/**Function********************************************************************

  Synopsis     [Load a BDD from a file.]

  Description  [Load a BDD from a file.]

  SideEffects  []

  SeeAlso      []

******************************************************************************/
static DdNode*
load_data_from_dddmp_file(
    DdManager* ddMgr /* IN: CUDD Manager */
    , dddmpVarInfo_t* varInfo /* IN/OUT: Variable Information */
    , char* fileName)
{
    Dddmp_VarMatchType varmatchmode = DDDMP_VAR_MATCHIDS;
    DdNode* f;


    /*-------------------------------- Load BDD -------------------------------*/

    fprintf(stdout, "Loading %s ...\n", fileName);

    f = Dddmp_cuddBddLoad(
        ddMgr
        , varmatchmode
        //,DDDMP_VAR_MATCHNAMES
        , varInfo->orderedVarNames
        , varInfo->varIdsAll
        , varInfo->varComposeIdsAll
        //,DDDMP_MODE_DEFAULT
        ,DDDMP_MODE_TEXT
        , fileName
        , nullptr);

    if (f == nullptr)
    {
        fprintf(stderr, "Dddmp load Error : %s is not loaded from file\n", fileName);
    }

    return (f);
}


/**Function********************************************************************

  Synopsis     [Quit a CUDD Manager.]
  
  Description  [Quit a CUDD Manager.]
  
  SideEffects  []
  
  SeeAlso      []

******************************************************************************/
static void
dispose_ddmanager(
    DdManager** ddMgrPtr /* IN: CUDD Manager */,
    dddmpVarInfo_t* varInfo /* IN: Internal Manager */
)
{
    if (*ddMgrPtr == nullptr)
    {
        return;
    }

    fprintf(stdout, "Quitting CUDD Manager.\n");
    Cudd_Quit(*ddMgrPtr);
    *ddMgrPtr = nullptr;

    util_dddmp_str_array_free(varInfo->rootNames, varInfo->nRoots);
    util_dddmp_str_array_free(varInfo->suppVarNames, varInfo->nSuppVars);
    util_dddmp_str_array_free(varInfo->orderedVarNames, varInfo->nVars);
    DDDMP_FREE(varInfo->varIds);
    DDDMP_FREE(varInfo->varIdsAll);
    DDDMP_FREE(varInfo->varComposeIds);
    DDDMP_FREE(varInfo->varComposeIdsAll);
    DDDMP_FREE(varInfo->varAuxIds);
    DDDMP_FREE(varInfo->varAuxIdsAll);

    varInfo->nDdVars = (-1);
    varInfo->rootNames = nullptr;
    varInfo->ddType = DDDMP_NONE;
    varInfo->nVars = (-1);
    varInfo->nSuppVars = (-1);
    varInfo->varNamesFlagUpdate = 1;
    varInfo->suppVarNames = nullptr;
    varInfo->orderedVarNames = nullptr;
    varInfo->varIdsFlagUpdate = 1;
    varInfo->varIds = nullptr;
    varInfo->varIdsAll = nullptr;
    varInfo->varComposeIdsFlagUpdate = 1;
    varInfo->varComposeIds = nullptr;
    varInfo->varComposeIdsAll = nullptr;
    varInfo->varAuxIdsFlagUpdate = 1;
    varInfo->varAuxIds = nullptr;
    varInfo->varAuxIdsAll = nullptr;
    varInfo->nRoots = (-1);
}


int main(int argc, char* argv[])
{
    DdManager* dd_mgr;
    dddmpVarInfo_t varInfo;
    constexpr char srcFile[] = "../test.dddmp";

    dd_mgr = init_ddmanager(&varInfo);
    Dddmp_CheckAndReturn(dd_mgr==NULL, "Fatal, exiting");

    auto ret = load_header_from_dddmp_file(&varInfo, const_cast<char*>(srcFile));
    Dddmp_CheckAndReturn(ret!=DDDMP_SUCCESS, "Problems loading file header.");

    auto bdd = load_data_from_dddmp_file(dd_mgr, &varInfo, const_cast<char*>(srcFile));
    Dddmp_CheckAndReturn(bdd==NULL, "Fatal, exiting");

    constexpr char destFile[] = "../test.dot";

    Cudd_Ref(bdd); /*Update the reference count for the node just created.*/

    bdd = Cudd_BddToAdd(dd_mgr, bdd); /*Convert BDD to ADD for display purpose*/

    write_dot(dd_mgr, bdd, const_cast<char*>(destFile), varInfo.orderedVarNames);

    /*-------------------------------- Free Memory ----------------------------*/
    dispose_ddmanager(&dd_mgr, &varInfo); //calls Cudd_Quit(ddMgr) as well

    return 0;
}

PS. Tested with CMAKE CUDD build using both gcc and msvc.