1

我正在尝试使用 CUDD 查找 Shared-BDD 中的节点总数。 我已经使用 BuDDy-2.4 编写了 C 代码并且运行良好但是当我使用 CUDD 而不是 BuDDy 时，我的程序显示错误。

我的 BuDDY C 文件是：

//BuDDY_C Code for Node Count:    

#define X1 (a&b&c&d)|(!c&d&f)|(g&!g)    //Define Function-1 here
#define X2 (a&b&d&!c)|(!c&!c&d)^(g) //Define Function-2 here


#include<bdd.h>
#include<stdio.h>
#include<stdlib.h>

int main(void)
{
bdd z[2],a,b,c,d,e,f,g,h;
int i,INPUT=8,node_count,order[8]={2,5,1,6,0,4,3,7};

printf("\nGiven Variable Order:\t ");
    for(i=0;i<INPUT;i++)
        printf("%d \t",order[i]); 

   bdd_init(1000,100);
   bdd_setvarnum(INPUT);

        a = bdd_ithvar(order[0]);  //Assign Variable order stored in order[0] to a
        b = bdd_ithvar(order[1]);  //Assign Variable order stored in order[1] to b
        c = bdd_ithvar(order[2]);  //Assign Variable order stored in order[2] to c
        d = bdd_ithvar(order[3]);  //Assign Variable order stored in order[3] to d
        e = bdd_ithvar(order[4]);  //Assign Variable order stored in order[4] to e
        f = bdd_ithvar(order[5]);  //Assign Variable order stored in order[5] to f
        g = bdd_ithvar(order[6]);  //Assign Variable order stored in order[6] to g
        h = bdd_ithvar(order[7]);  //Assign Variable order stored in order[7] to h


    z[0]=X1; 
    z[1]=X2;
   node_count=bdd_anodecount(z,2);
   bdd_done();
   printf("\n Total no of nodes are %d\n",node_count);
   return 0;

}

我的 CUDD C 程序是：

//CUDD_C Code for Node Count
#define X1 (a&b&c&d)|(!c&d&f)|(g&!g)    //Define Function-1 here
#define X2 (a&b&d&!c)|(!c&!c&d)^(g) //Define Function-2 here

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

int main(void) {
DdNode *z[2],*a,*b,*c,*d,*e,*f,*g,*h;
int i,INPUT=8,node_count,order[8]={2,5,1,6,0,4,3,7};

printf("\nGiven Variable Order:\t ");
    for(i=0;i<INPUT;i++)
        printf("%d \t",order[i]); 

DdManager * mgr = Cudd_Init(INPUT,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);


 a = Cudd_bddIthVar(mgr, order[0]);  //Assign Variable order stored in order[0] to a
 b = Cudd_bddIthVar(mgr, order[1]);  //Assign Variable order stored in order[0] to b
 c = Cudd_bddIthVar(mgr, order[2]);  //Assign Variable order stored in order[0] to c
 d = Cudd_bddIthVar(mgr, order[3]);  //Assign Variable order stored in order[0] to d
 e = Cudd_bddIthVar(mgr, order[4]);  //Assign Variable order stored in order[0] to e
 f = Cudd_bddIthVar(mgr, order[5]);  //Assign Variable order stored in order[0] to f
 g = Cudd_bddIthVar(mgr, order[6]);  //Assign Variable order stored in order[0] to g
 h = Cudd_bddIthVar(mgr, order[7]);  //Assign Variable order stored in order[0] to h


    z[0]=X1; 
    z[1]=X2;


  Cudd_Ref(z[0]);
  Cudd_Ref(z[1]);
/*-----Calculate no of nodes and number of shared nodes*/

        node_count= Cudd_SharingSize( z, 2);   
    printf("\n Total no of nodes are %d\n",node_count);

  int err = Cudd_CheckZeroRef(mgr);
  Cudd_Quit(mgr);
  return err;
}

但是这个 CUDD C 程序显示错误

balal@balal-HP-H710：~/Desktop/cudd-3.0.0 $ g++ -o test test2_cudd.c -lbdd
 test2_cudd.c：在函数'<b>int main()'中：
 test2_cudd.c:2:14 : 错误: '<b>DdNode*' 和 '<b>DdNode*' 类型的无效操作数到二进制 '<b>operator&'
 #define X1 ( a&b &c&d)|(!c&d&f)|(g&!g) //在这里定义 Function-1
              ~^~ 
test2_cudd.c:30:7: 注意：在宏 '<b>X1' 的扩展中
  z[0]= X1 ;
       ^~ 
test2_cudd.c:2:25: 错误： '<b>bool' 和 '<b>DdNode*' 类型的无效操作数到二进制 '<b>operator&'
 #define X1 (a&b&c&d)|( !c&d &f)|(g&!g) //在这里定义 Function-1
                        ~~^~ 
test2_cudd.c:30:7: 注意：在宏 '<b>X1' 的扩展中
  z[0]= X1 ;
       ^~ 
test2_cudd.c:2:33: 错误: '<b>DdNode*' 和 '<b>bool' 类型的无效操作数到二进制 '<b>operator&'
 #define X1 (a&b&c&d)|(!c&d&f)|( g&!g ) //在这里定义 Function-1
                                 ~^~~ 
test2_cudd.c:30:7: 注意：在宏 '<b>X1' 的扩展中
  z[0]= X1 ;
       ^~ 
test2_cudd.c:3:14: 错误： '<b>DdNode*' 和 '<b>DdNode*' 类型的无效操作数到二进制 '<b>operator&'
 #define X2 ( a&b &d&!c)|(!c&!c&d)^(g) //在这里定义 Function-2
              ~^~ 
test2_cudd.c:31:7: 注意：在宏 '<b>X2' 的扩展中
  z[1]= X2 ;
       ^~ 
test2_cudd.c:3:29: 错误： '<b>int' 和 '<b>DdNode*' 类型的无效操作数到二进制 '<b>operator&'
 #define X2 (a&b&d&!c)|( !c&!c&d )^(g) //在这里定义 Function-2
                         ~~~~~~^~ 
test2_cudd.c:31:7: 注意：在宏的扩展中 '<b >X2'
  z[1]= X2 ;
       ^~ 
balal@balal-HP-H710 : ~/Desktop/cudd-3.0.0 $
4

2 回答 2

0

另一种可能性是使用 Python 包中包含的 CUDD 的 Cython 接口dd。这里描述dd了使用模块的安装，可以总结为dd.cudd

pip download dd --no-deps
tar -xzf dd-*.tar.gz
cd dd-*/
python setup.py install --fetch --cudd

这将下载和构建 CUDD，并构建和安装到 CUDD 的 Cython 绑定dd。dd也有 Cython 与 BuDDy 的绑定，并且可以类似地构建，用户下载和构建BuDDy，然后传递--buddy给 script setup.py。

示例代码可以转换为以下 Python 代码。

from dd import cudd as _bdd

bdd = _bdd.BDD()
bdd.declare('a', 'b', 'c', 'd', 'e', 'f', 'g', 'h')
# /\ is conjunction in TLA+, \/ disjunction, ~ negation
X1 = bdd.add_expr('(a /\ b /\ c /\ d) \/ (~ c /\ d /\ f) \/ (g /\ ~ g)')
    # note that g /\ ~ g is FALSE
X2 = bdd.add_expr('(a /\ b /\ d /\ ~ c) \/ ((~ c /\ ~ c /\ d) ^ g)')
    # note that ~ c /\ ~ c is ~ c


# using the operators &, |, ! for conjunction, disjunction, and negation
X1_ = bdd.add_expr('(a & b & c & d) \/ (!c & d & f) \/ (g & !g)')
X2_ = bdd.add_expr('(a & b & d & !c) \/ ((!c & !c & d) ^ g)')
assert X1 == X1_, (X1, X1_)
assert X2 == X2_, (X2, X2_)


def descendants(roots):
    """Return nodes reachable from `roots`.

    Nodes in `roots` are included.
    """
    if not roots:
        return set()
    visited = set()
    for u in roots:
        _descendants(u, visited)
    assert set(roots).issubset(visited), (roots, visited)
    return visited

def _descendants(u, visited):
    v, w = u.low, u.high
    # terminal node or visited ?
    if u.low is None or u in visited:
        return
    _descendants(v, visited)
    _descendants(w, visited)
    visited.add(u)


r = descendants([X1, X2])
print(len(r))

# plot diagrams of the results using GraphViz
bdd.dump('X1.pdf', [X1])
bdd.dump('X2.pdf', [X2])

该函数descendants计算从给定节点（由X1和引用的节点X2）可到达的节点集，包括给定节点。在我的运行中，变量顺序的答案是 16 个节点。布尔函数X1和BDD 的图表X2如下。

布尔函数的 BDDX1

布尔函数 <code>X1</code>

布尔函数的 BDDX2

布尔函数 <code>X2</code>

于 2020-02-23T13:21:16.843 回答
0

在用 C 编写程序时，您正尝试在 BDD 节点上使用“&”运算符。由于 C 不支持运算符重载，因此这不起作用，因为“&”运算符最多意味着采用按位与地址，这不是你想要的。

为了计算两个 BDD 的 AND，您必须使用 Cudd_bddAnd 函数。例如，请参见此处的示例。请注意，您的宏会以这种方式变得更长，并且需要包含除作用域之外的局部变量。

另一种方法是使用 CUDD 的 C++ 接口，其中 BDD 可以封装到支持运算符重载的对象中。

注意

z[0]=X1; 
z[1]=X2;
Cudd_Ref(z[0]);
Cudd_Ref(z[1]);

也可能造成麻烦。在 CUDD 中，在调用任何其他可以创建新节点的 CUDD 函数之前，必须使用 Cudd_Ref(...) 引用节点。由于您的 X2 宏包含对 BDD 的操作，因此可能会发生这种情况。因此，最好立即使用 Cudd_Ref(...) BDD。以下看起来更好：

z[0]=X1; 
Cudd_Ref(z[0]);
z[1]=X2;
Cudd_Ref(z[1]);

请注意，出于同样的原因，您的好友代码也是错误的。但是，由于 BDD 类型被定义为“typedef int BDD;” 编译器在 BDD 节点号上使用了按位 AND 和 OR，这就是为什么它编译为产生错误结果的代码的原因。

于 2020-02-12T07:41:49.027 回答