2

I'm using Cudd package http://vlsi.colorado.edu/~fabio/CUDD/ First I got an error states "dead count != deleted" so I started debugging and I encounter a problem that I can't understand.

The following code takes as input a decimal value and it should return the corresponding BDD to this decimal value using variables in the nodes_vector.

DdNode * convert_decimal_to_BDD(unsigned int decimal_value, DdManager * manager, vector<DdNode *> nodes_vector){

DdNode * tmp3;

int nodes_vector_size = nodes_vector.size(); 

vector<bool> binary = get_binary_representation(decimal_value, nodes_vector_size);

DdNode * result = Cudd_ReadOne(manager);
Cudd_Ref(result);

for (int i = 0; i < nodes_vector_size; i++){

    if(binary[i] == 1){
        tmp3 = Cudd_bddAnd(manager,result,nodes_vector[i]);
    }
    else{
        tmp3 = Cudd_bddAnd(manager,result,Cudd_Not(nodes_vector[i]));
    }
    if(tmp3 == NULL){
        printf("convert_decimal_to_BDD: Error 1\n");
        exit(1);
    }
    Cudd_Ref(tmp3);
    printf("convert_decimal_to_BDD: tmp->ref %hu\n", tmp3->ref);
    Cudd_RecursiveDeref(manager,result);
    result = tmp3;
    printf("convert_decimal_to_BDD: result->ref %hu\n", result->ref);
}

printf("NFAOBDD::convert_decimal_to_BDD: result->ref %hu\n", result->ref);

return result;
}

For some cases I get the reference value for the result node and the tmp3 node equal to zero, but I can't understand how can this happen after I call "Cudd_ref(tmp3)"

I would appreciate any explanation to this and why may I get "dead count != deleted" error within a loop although I didn't get the "dead count != deleted" error on the first iterations of that loop.

timrau
  • 22,578
  • 4
  • 51
  • 64
user3060396
  • 163
  • 1
  • 1
  • 5
  • When you write 'nodes_vector[i]' you mean to fetch the i-th variable, right? Usually I do that this way: DdNode *var = Cudd_bddIthVar(manager,i); – Lorenzo Apr 29 '14 at 14:11
  • A few comments (should this still be of relevance): When your function "convert_decimal_to_BDD" returns, the result is already Ref'd. If you also Cudd_ref your result in the procedure that calls the function from above, you are double-referencing, which can cause the dead count problem. Then, you compare a Bool against "1": "if(binary[i] == 1)". Don't do this. Finally, "tmp3 == NULL" can happen when you run out of memory: Initialize the CUDD manager with a higher max memory allowance to avoid this and/or turn on dynamic reordering. – DCTLib Mar 24 '15 at 10:18

0 Answers0