CUDD: Access BDD childs

Question

我正在使用CUDD C 接口。

我没有找到有关此库的太多信息。

我如何找到一个BDD的两个孩子？

例如：

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

现在，使用F，我想让它的孩子和其他孩子。文档说ddnode有这个孩子，但我不知道如何访问他们。

谢谢。

Answer 1

您可以访问cudd bdd节点的孩子，如下所示：

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

这给出了DDNode指针，该指针是用于使用普通C接口时使用的数据结构。您可以通过：

再次获得C 对象

BDD tb = BDD(mgr,t);

请注意，以上仅在F是互补的节点时起作用。否则，您必须通过cudd_regular函数来调用" getNode"函数的结果。请注意，这会倒转BDD的含义。

您也可以像对待cudd一样对待BDD，就像没有使用倒出节点一样。对于这种情况，您将获得以下内容的否则 - 和核对员工：

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

使用与Python软件包dd的cudd的Cython绑定也可以访问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安装在此处