CUDD с использованием не-гейта

Я пытаюсь построить 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);

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


cudd
person Yosi Ben-Asher    schedule 30.12.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Каждый узел 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]);
}

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

person DCTLib    schedule 31.12.2018
comment
спасибо, я просто Cudd_Ref() ноды, которые использовали не-гейты, и это сработало. - person Yosi Ben-Asher; 01.01.2019
comment
@YosiBen-Asher Это работает в этом особом случае, поскольку CUDD узлы x[k] и nx[k] на самом деле являются одними и теми же узлами, за исключением того, что CUDD хранит отрицательный флаг в DdNode для nx[k]. Поскольку они являются одним и тем же узлом, достаточно выполнить Ref'fing одного из них, при условии, что позже вы также сделаете DeRef только один из них, а не оба. - person DCTLib; 01.01.2019