1

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

我没有找到关于这个图书馆的太多信息。

如何获得 BDD 的两个孩子？

例如：

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

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

谢谢你。

4

2 回答 2

3

您可以访问 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 的含义。

您还可以将 BDD 视为好像 CuDD 没有使用倒置节点。对于这种情况，您将获得 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()));
}
于 2017-12-08T13:51:30.953 回答
0

使用 Cython 绑定到 Python 包的 CUDD 也可以访问 BDD 节点的后继节点dd。

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了使用模块的安装dd.cudd

于 2020-02-23T15:00:11.517 回答