隐藏：访问 BDD 子项

Question

我正在使用 CUDD C++ 接口。

我找不到太多关于此库的信息。

怎样才能得到一个BDD的二children？

例如：

Cudd mgr;
BDD x = mgr.bddVar();
BDD y = mgr.bddVar();
BDD f = x * y;

现在，对于 f，我想得到它的 then child 和 else child。文档说 DdNode 有这个 children 但我不知道如何访问它们。

谢谢。

Answer 1

您可以按如下方式访问 Cudd BDD 节点的 then 和 else 子节点：

DdNode *t = Cudd_T(f.getNode());
DdNode *e = Cudd_E(f.getNode());

这给出了 DdNode 指针，这是在使用纯 C 接口时用于引用 BDD 的数据结构。您可以通过以下方式再次获取 C++ 对象：

BDD tb = BDD(mgr,t);

请注意，以上仅适用于 f 不是补节点的情况。否则，您必须通过 Cudd_Regular 函数运行调用 "getNode" 函数的结果。请注意，这会颠倒 BDD 的含义。

您也可以像对待 CuDD 不使用反向节点一样对待 BDD。对于这种情况，您将获得 then- 和 else-successors，如下所示：

BDD t;
BDD e;
if (Cudd_IsComplement(f.getNode())) {
    t = !BDD(manager,Cudd_Regular(Cudd_T(f.getNode())));
    e = !BDD(manager,Cudd_Regular(Cudd_E(f.getNode())));
} else {
    t = BDD(manager,Cudd_T(f.getNode()));
    e = BDD(manager,Cudd_E(f.getNode()));
}

Answer 2

使用 Cython 绑定到 Python 包 dd.

的 CUDD 也可以访问 BDD 节点的后继节点

from dd import cudd as _bdd

bdd = _bdd.BDD()
bdd.declare('x', 'y')
u = bdd.add_expr(r'x /\ y')

# "else" successor of node `u`
v = u.low
# "then" successor of node `u`
w = u.high

u_ = bdd.add_expr(rf'(~ x /\ {v}) \/ (x /\ {w})')
assert u == u_, (u, u_)

描述了使用模块 dd.cudd 安装 dd here

隐藏：访问 BDD 子项

CUDD: Access BDD childs

c++

binary-decision-diagram

cudd