CUDD BDDs: building a boolean as disjunction of conjunctions but get runtime error: segmentation fault

Question

Does anyone with experience using CUDD (not be confused with CUDA) for manipulating BDDs know why possibly I keep getting the dreaded "segmentation error (dumped core)". I suspect it could be related to referencing de-referencing which I confess I don't fully understand. Any hints pointers appreciated. I (commented out some things I have been trying):

#include <stdio.h>
#include <stdlib.h>
#include "cudd.h"

int main(int argc, char* argv[])
{
    /*char filename[30];*/
    DdManager * gbm; /* Global BDD manager. */
    gbm = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); /* Initialize a new BDD manager with defaults. */
    int const n = 3;
    int i, j;
    DdNode *var, *tmp, *tmp2, *BDD, *BDD_t;

    BDD_t = Cudd_ReadLogicZero(gbm);
    /*Cudd_Ref(BDD_t);*/
    
    /* Outter loop: disjunction of the n terms*/
    for (j = 0; j <= n - 1; j++) {

        BDD = Cudd_ReadOne(gbm); /*Returns the logic one constant of the manager*/
       /* Cudd_Ref(BDD);*/

    /* Inner loop: assemble each of the n conjunctions */
        for (i = j * (n - 1); i >= (j - 1) * (n - 1); i--) {
            
            var = Cudd_bddIthVar(gbm, i); /*Create a new BDD variable*/
            tmp = Cudd_bddAnd(gbm, var, BDD); /*Perform AND boolean operation*/
            BDD = tmp;
        }

        tmp2 = Cudd_bddOr(gbm, BDD, BDD_t); /*Perform OR boolean operation*/
        /*Cudd_RecursiveDeref(gbm, tmp);*/
        BDD_t = tmp2;
    }

    Cudd_PrintSummary(gbm, BDD_t, 4, 0);
    /* Cudd_bddPrintCover(mgr, BDD_t, BDD);*/
    /* BDD = Cudd_BddToAdd(gbm, BDD_t);*/
    /* printf(gbm,BDD_t, 2, 4);*/
    Cudd_Quit(gbm);
    return 0;
}

Answer 1

Thanks, @DCTLib. I've found that the C++ interface is much more convenient for formulating Boolean expressions. The only problem is how to go back and forth between the C and C++ interfaces, since ultimately I still need C for printing out the minterms (called cutsets in the world I inhabit, Reliability Eng. Let me pose the question in separate entry. It seems you know CUDD quite well. You should be maintaining that repo! It's a great product but sparsely documented or interacted with.

Answer 2

While you are correc that Cudd_Ref'find and Cudd_RecursiveDeref'ing is not correct in your code (yet), the current and first problem is actually a different one.

You never check the return values of the CUDD function. Some of them return NULL (0) on error, and your code does not detect such cases. In fact, the call to "Cudd_bddIthVar" returns NULL (0) at least once, and then the subsequent call to the BDD AND function makes the CUDD library access the memory at memory address 0+4, causing the segmentation fault.

There are multiple ways to fix this:

1. The best way is to always check for NULL return values and then notify the user of the program of the problem. Since this is your main() function, this could be printing an error message and the returning 1

2. At the very bare minimum, you can add assert(...) statements, so that at least in debug mode, the problem will become obvious. This is not recommended in general, as when compiling not in debug mode, such problems may go unnoticed.

3. In C++, there is also the possibility to work with exception - but you don't seem to be using C++.

Now why does "Cudd_bddIthVar(gbm, i)" return NULL? Because in the second iteration, variable "i" of the loop has value -1.

Now as far as Ref'fing and Deref'fing is concerned:

• You need to call Cudd_Ref(...) to every BDD variable that you want to use until after calling the next Cudd function. Exceptions are constants are variables.
• You need to call Cudd_RecursiveDeref(...) on every BDD node that you initially Ref'd that is no longer needed.

This is because every BDD node has a counter telling you how often it is currently in use. Once the counter hits 0, the BDD node may be recycled. Ref'fing while the node is in use makes sure that it does not happen while the node is in use.

You program could be fixed as follows:

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include "cudd.h"

int main(int argc, char* argv[])
{
    /*char filename[30];*/
    DdManager * gbm; /* Global BDD manager. */
    gbm = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); /* Initialize a new BDD manager with defaults. */
    assert(gbm!=0);
    int const n = 3;
    int i, j;
    DdNode *var, *tmp, *tmp2, *BDD, *BDD_t;

    BDD_t = Cudd_ReadLogicZero(gbm);
    assert(BDD_t!=0);
    Cudd_Ref(BDD_t);
    
    /* Outter loop: disjunction of the n terms*/
    for (j = 0; j <= n - 1; j++) {

        BDD = Cudd_ReadOne(gbm); /*Returns the logic one constant of the manager*/
        assert(BDD!=0);
        Cudd_Ref(BDD);

    /* Inner loop: assemble each of the n conjunctions */
        for (i = j * (n - 1); i >= (j) * (n - 1); i--) {
            var = Cudd_bddIthVar(gbm, i); /*Create a new BDD variable*/
            assert(var!=0);
            tmp = Cudd_bddAnd(gbm, var, BDD); /*Perform AND boolean operation*/
            assert(tmp!=0);
            Cudd_Ref(tmp);
            Cudd_RecursiveDeref(gbm,BDD);
            BDD = tmp;
        }

        tmp2 = Cudd_bddOr(gbm, BDD, BDD_t); /*Perform OR boolean operation*/
        assert(tmp2!=0);
        Cudd_Ref(tmp2);
        Cudd_RecursiveDeref(gbm, BDD_t);
        Cudd_RecursiveDeref(gbm, BDD);
        BDD_t = tmp2;
    }

    Cudd_PrintSummary(gbm, BDD_t, 4, 0);
    /* Cudd_bddPrintCover(mgr, BDD_t, BDD);*/
    /* BDD = Cudd_BddToAdd(gbm, BDD_t);*/
    /* printf(gbm,BDD_t, 2, 4);*/
    Cudd_RecursiveDeref(gbm,BDD_t);
    assert(Cudd_CheckZeroRef(gbm)==0);
    Cudd_Quit(gbm);
    return 0;
}

For brevity, I used assert(...) statements to check the conditions. Don't use this in production code - this is only to keep the code shorter during learning. Also look up in the CUDD documentation which calls can actually return NULL. Those that cannot do not need such a check. But most calls can return 0.

Note that:

• The return value of Cudd_bddIthVar is not Cudd_Ref's - it doesn't need to.
• The return value of Cudd_ReadLogicZero(gbm) is Cudd_Ref'd - this is because the variable is overwritten with nodes that have to be Ref'd later, and hence the code needs to have a call to RecursiveDeref(...) in that case. To make Ref's and Deref's symmetric, the node is needlessly Ref'd (which is allowed).
• The last assert statement checks if there are any nodes still in use -- if that is the case before calling Cudd_Quit, this tells you that your code doesn't Deref correctly, which should be fixed. If you comment out any RecursiveDeref line and run the code, the assert statement should halt execution then.
• I've rewritten your for-loop condition to ensure that no negative variable numbers occur. But your code may not do what it is supposed to now.