Cudd_BDD опорное значение нулевого узла

Я использую пакет Cudd http://vlsi.colorado.edu/~fabio/CUDD/
Сначала я получил сообщение об ошибке «dead count! = Удалено», поэтому я начал отладку и столкнулся с проблемой, которую не могу понять.

Следующий код принимает в качестве входных данных десятичное значение, и оно должно возвращать соответствующий BDD к этому десятичному значению, используя переменные в node_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;
}

В некоторых случаях я получаю эталонное значение для результирующего узла и узла tmp3 равным нулю, но я не могу понять, как это может произойти после того, как я вызываю «Cudd_ref (tmp3)»

Я был бы признателен за любое объяснение этого и почему я могу получить ошибку «мертвый счет! = Удаленный» в цикле, хотя я не получил ошибку «мертвый счет! = Удаленный» на первых итерациях этого цикла.

2

Решение

Задача ещё не решена.

Другие решения