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

我该怎么办，手册帮不上忙，不去引用xk，nxk…

Answer 1

任何Cudd操作都会删除未引用的每个BDD节点。如果您希望确保存储在数组中的所有节点都保持有效，则需要在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]);
}

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