CUDD с использованием not-gate

Question

Я пытаюсь построить BDD для монотонного умножения и нужно использовать отрицание входных битов.

Я использую следующий код:

DdNode *x[N], *y[N], *nx[N], *ny[N];

gbm = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0); /* Initialize a new BDD manager. */

for(k=0;k<N;k++)
{
   x[k] = Cudd_bddNewVar(gbm);
   nx[k] = Cudd_Not(x[k]);  
   y[k] = Cudd_bddNewVar(gbm);
   ny[k] = Cudd_Not(y[k]);  
}

Ошибка, которую я получаю:

cuddGarbageCollect: problem in table 0
  dead count != deleted
  This problem is often due to a missing call to Cudd_Ref
  or to an extra call to Cudd_RecursiveDeref.
  See the CUDD Programmer's Guide for additional details.Aborted (core dumped)

Множитель компилируется и работает нормально, когда я использую

   x[k] = Cudd_bddNewVar(gbm);
   nx[k] = Cudd_bddNewVar(gbm);  
   y[k] = Cudd_bddNewVar(gbm);
   ny[k] = Cudd_bddNewVar(gbm);  

Что делать, инструкция не помогает не переосмысливая ref x[k],nx[k]...

Answer 1

Каждый узел BDD, на который нет ссылки, подлежит удалению любой операцией Cudd. Если вы хотите убедиться, что все узлы, хранящиеся в вашем массиве, остаются действительными, вам нужно Cudd_Ref их сразу после того, как они возвращены CUDD. Следовательно, вам нужно исправить свой код так:

for(k=0;k<N;k++)
{
   x[k] = Cudd_bddNewVar(gbm);
   Cudd_Ref(x[k]);
   nx[k] = Cudd_Not(x[k]);  
   Cudd_Ref(nx[k]);
   y[k] = Cudd_bddNewVar(gbm);
   Cudd_Ref(y[k]);
   ny[k] = Cudd_Not(y[k]);  
   Cudd_Ref(yn[k]);
}

Перед освобождением менеджера Cudd вам необходимо разыменовать узлы:

for(k=0;k<N;k++)
{
   Cudd_RecursiveDeref(gbm,x[k]);
   Cudd_RecursiveDeref(gbm,nx[k]);
   Cudd_RecursiveDeref(gbm,y[k]);
   Cudd_RecursiveDeref(gbm,ny[k]);
}

Обратите внимание, что тот факт, что ваш код работает при выделении большего количества переменных, не показывает, что ссылки не нужны. Возможно, вы просто не используете достаточно узлов для запуска сборщика мусора, и до этого проблема не обнаруживается.