CUDD: Access BDD childs

Question

I'm working with CUDD C++ interface.

I'm finding not much information about this library.

How can I get the two children of a BDD?

For example:

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

Now, with f, I want to get its then child and else child. The documentation says that DdNode has this children but I don't know how to access them.

Thank you.

Answer 1

You can access the then and else children of a Cudd BDD node as follows:

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

This gives DdNode pointer, which is the data structure used to refer to BDDs when using the plain C interface. You can get C++ objects again by:

BDD tb = BDD(mgr,t);

Note that the above only works if f is not a complemented node. Otherwise, you have to run the result of calling "getNode" function through the Cudd_Regular function. Note that this inverts the meaning of the BDD.

You could also treat the BDDs like as if CuDD did not use inverted nodes. For this case, you would get then- and else-successors as follows:

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

Accessing the successors of a BDD node is also possible using the Cython bindings to CUDD of the Python package 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_)

Installation of dd with the module dd.cudd is described here