0

是否有使用 CUDD（不要与 CUDA 混淆）来操作 BDD 的经验的人知道为什么我可能不断收到可怕的“分段错误（转储核心）”。我怀疑这可能与引用取消引用有关，我承认我不完全理解。任何提示指针表示赞赏。我（评论了我一直在尝试的一些事情）：

#include <stdio.h>
#include <stdlib.h>
#include "cudd.h"

int main(int argc, char* argv[])
{
    /*char filename[30];*/
    DdManager * gbm; /* Global BDD manager. */
    gbm = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); /* Initialize a new BDD manager with defaults. */
    int const n = 3;
    int i, j;
    DdNode *var, *tmp, *tmp2, *BDD, *BDD_t;

    BDD_t = Cudd_ReadLogicZero(gbm);
    /*Cudd_Ref(BDD_t);*/
    
    /* Outter loop: disjunction of the n terms*/
    for (j = 0; j <= n - 1; j++) {

        BDD = Cudd_ReadOne(gbm); /*Returns the logic one constant of the manager*/
       /* Cudd_Ref(BDD);*/

    /* Inner loop: assemble each of the n conjunctions */
        for (i = j * (n - 1); i >= (j - 1) * (n - 1); i--) {
            
            var = Cudd_bddIthVar(gbm, i); /*Create a new BDD variable*/
            tmp = Cudd_bddAnd(gbm, var, BDD); /*Perform AND boolean operation*/
            BDD = tmp;
        }

        tmp2 = Cudd_bddOr(gbm, BDD, BDD_t); /*Perform OR boolean operation*/
        /*Cudd_RecursiveDeref(gbm, tmp);*/
        BDD_t = tmp2;
    }

    Cudd_PrintSummary(gbm, BDD_t, 4, 0);
    /* Cudd_bddPrintCover(mgr, BDD_t, BDD);*/
    /* BDD = Cudd_BddToAdd(gbm, BDD_t);*/
    /* printf(gbm,BDD_t, 2, 4);*/
    Cudd_Quit(gbm);
    return 0;
}
4

2 回答 2

0

谢谢，@DCTLib。我发现 C++ 接口对于制定布尔表达式要方便得多。唯一的问题是如何在 C 和 C++ 接口之间来回切换，因为最终我仍然需要 C 来打印最小项（在我居住的世界中称为割集，Reliability Eng。让我在单独的条目中提出这个问题。它看来你很了解 CUDD。你应该维护那个 repo！它是一个很棒的产品，但很少有文档记录或与之交互。

于 2020-07-16T20:58:46.887 回答
0

虽然您认为 Cudd_Ref'find 和 Cudd_RecursiveDeref'ing 在您的代码中不正确（但），但当前和第一个问题实际上是不同的。

您永远不会检查 CUDD 函数的返回值。其中一些在错误时返回 NULL (0)，并且您的代码没有检测到这种情况。事实上，对“Cudd_bddIthVar”的调用至少返回了一次NULL(0)，然后随后调用BDD AND函数使CUDD库访问内存地址0+4处的内存，导致分段错误。

有多种方法可以解决此问题：

  1. 最好的方法是始终检查 NULL 返回值，然后将问题通知给程序用户。由于这是您的 main() 函数，因此可能会打印一条错误消息并返回 1

  2. 至少，您可以添加 assert(...) 语句，这样至少在调试模式下，问题会变得很明显。通常不建议这样做，因为在非调试模式下编译时，此类问题可能会被忽视。

  3. 在 C++ 中，也有可能处理异常 - 但您似乎没有使用 C++。

现在为什么“Cudd_bddIthVar(gbm, i)”返回 NULL？因为在第二次迭代中，循环的变量“i”的值为 -1。

现在就 Ref'fing 和 Deref'fing 而言：

  • 在调用下一个 Cudd 函数之前，您需要对要使用的每个 BDD 变量调用 Cudd_Ref(...)。异常是常量是变量。
  • 您需要在您最初引用但不再需要的每个 BDD 节点上调用 Cudd_RecursiveDeref(...)。

这是因为每个 BDD 节点都有一个计数器，告诉您它当前使用的频率。一旦计数器达到 0，BDD 节点可能会被回收。在使用节点时进行引用确保在使用节点时不会发生这种情况。

您的程序可以固定如下：

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include "cudd.h"

int main(int argc, char* argv[])
{
    /*char filename[30];*/
    DdManager * gbm; /* Global BDD manager. */
    gbm = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); /* Initialize a new BDD manager with defaults. */
    assert(gbm!=0);
    int const n = 3;
    int i, j;
    DdNode *var, *tmp, *tmp2, *BDD, *BDD_t;

    BDD_t = Cudd_ReadLogicZero(gbm);
    assert(BDD_t!=0);
    Cudd_Ref(BDD_t);
    
    /* Outter loop: disjunction of the n terms*/
    for (j = 0; j <= n - 1; j++) {

        BDD = Cudd_ReadOne(gbm); /*Returns the logic one constant of the manager*/
        assert(BDD!=0);
        Cudd_Ref(BDD);

    /* Inner loop: assemble each of the n conjunctions */
        for (i = j * (n - 1); i >= (j) * (n - 1); i--) {
            var = Cudd_bddIthVar(gbm, i); /*Create a new BDD variable*/
            assert(var!=0);
            tmp = Cudd_bddAnd(gbm, var, BDD); /*Perform AND boolean operation*/
            assert(tmp!=0);
            Cudd_Ref(tmp);
            Cudd_RecursiveDeref(gbm,BDD);
            BDD = tmp;
        }

        tmp2 = Cudd_bddOr(gbm, BDD, BDD_t); /*Perform OR boolean operation*/
        assert(tmp2!=0);
        Cudd_Ref(tmp2);
        Cudd_RecursiveDeref(gbm, BDD_t);
        Cudd_RecursiveDeref(gbm, BDD);
        BDD_t = tmp2;
    }

    Cudd_PrintSummary(gbm, BDD_t, 4, 0);
    /* Cudd_bddPrintCover(mgr, BDD_t, BDD);*/
    /* BDD = Cudd_BddToAdd(gbm, BDD_t);*/
    /* printf(gbm,BDD_t, 2, 4);*/
    Cudd_RecursiveDeref(gbm,BDD_t);
    assert(Cudd_CheckZeroRef(gbm)==0);
    Cudd_Quit(gbm);
    return 0;
}

为简洁起见，我使用 assert(...) 语句来检查条件。不要在生产代码中使用它——这只是为了在学习过程中保持代码更短。还要在 CUDD 文档中查找哪些调用实际上可以返回 NULL。那些不能不需要这样的检查。但大多数调用可以返回 0。

注意：

  • Cudd_bddIthVar 的返回值不是 Cudd_Ref 的 - 它不需要。
  • Cudd_ReadLogicZero(gbm) 的返回值是Cudd_Ref'd - 这是因为变量被稍后必须 Ref'd 的节点覆盖，因此在这种情况下代码需要调用 RecursiveDeref(...) . 为了使 Ref 和 Deref 对称，节点是不必要的 Ref'd（这是允许的）。
  • 最后一个 assert 语句检查是否有任何节点仍在使用 - 如果在调用 Cudd_Quit 之前是这种情况，这会告诉您您的代码没有正确取消引用，这应该被修复。如果您注释掉任何 RecursiveDeref 行并运行代码，那么 assert 语句应该会停止执行。
  • 我已经重写了您的 for 循环条件，以确保不会出现负变量数。但是您的代码可能无法执行它现在应该执行的操作。
于 2020-07-01T11:55:19.727 回答