CUDD 使用非门

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);  

我该怎么办，手册无助于不引用 x[k]，nx[k]...

Answer 1

每个未引用的 BDD 节点都会被任何 Cudd 操作删除。如果要确保存储在数组中的所有节点都保持有效，则需要在CUDD返回它们后立即Cudd_Ref它们。因此，您需要更正代码以：

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]);
}

请注意，代码在分配更多变量时工作的事实并不表示不需要引用。可能只是因为您没有使用足够的节点来触发垃圾收集器 - 在此之前，没有检测到问题。