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

我该怎么办，手册不利于不遵守 ref 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]);
}

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