Think there's a typo in master/doc.md#design-principles

[glarange]

Where it says {r} should be {u}, right?

u = bdd.add_expr('y \/ z') 
s = 'x /\ {r}'.format(u=u)
v = bdd.add_expr(s)
v_ = bdd.add_expr('x /\ (y \/ z)')
assert v == v_

This perhaps begs the question. How do I obtain a list of all the nodes in the bdd? (It's already described how to obtain a dictionary with all the variables in the bdd.)

[johnyf]

Yes, {r} should be {u}. Thank you for noting this. Introduced in https://github.com/tulip-control/dd/commit/a5c2725a5a17147bcd33eefa688c9512701177a5#diff-0e8d44201e6f72496813ac550141c407R169. Addressed in 8a34797f4dd5c91455294fccc2ade2b44d740a11.

To list all nodes reachable in a BDD, the following function enumerate_nodes can be used for BDD managers that are instances of the classes dd.autoref.BDD or dd.cudd.BDD:

def enumerate_nodes(u, mem=None):
    """Return `set` of all node references reachable from `u`."""
    if mem is None:
        mem = set()
    _enumerate_nodes(u, mem)
    return mem

def _enumerate_nodes(u, mem):
    if u in mem:
        return
    mem.add(u)
    if u.var is None:
        return
    enumerate_nodes(u.low, mem)
    enumerate_nodes(u.high, mem)

For example:

from dd import autoref

bdd = autoref.BDD()
bdd.declare('x', 'y')
u = bdd.add_expr('x \/ y')
nodes = enumerate_nodes(u)
print(nodes)

The same function (numerate_nodes) works with the class dd.cudd.BDD, for example:

from dd import cudd

bdd = cudd.BDD()
bdd.declare('x', 'y')
u = bdd.add_expr('x \/ y')
nodes = enumerate_nodes(u, set())
print(nodes)

Please note that the function enumerate_nodes lists all node references that are reachable from a node. So some nodes may be listed only negated, or both rectified and negated. To obtain a "canonical" list of nodes (all rectified, no negated references), the above list can be mapped as follows:

def rectify_nodes(nodes):
    return {rectify(u) for u in nodes}

def rectify(u):
    """Return negated reference, if node is negated."""
    if u.negated:
        return ~ u
    else:
        return u

positive_nodes = rectify_nodes(nodes)

To list all the nodes in a BDD manager, the following function can be used with a list of all external references to nodes in the manager:

def enumerate_manager_nodes(all_external_refs):
    nodes = set()
    for u in all_external_refs:
        enumerate_nodes(u, nodes)
    return rectify_nodes(nodes)

For example:

from dd import cudd

bdd = cudd.BDD()
bdd.declare('x', 'y', 'z')
u = bdd.add_expr('x \/ ~ y')
v = bdd.add_expr('y /\ z')

all_external_refs = [u, v]
nodes = enumerate_manager_nodes(all_external_refs)
print(nodes)

For the low-level Python implementation in the module dd.bdd, the entire set of nodes in the BDD manager is stored in the attribute BDD._succ. Based on this, the nodes in an instance of dd.autoref.BDD can be listed with

from dd import autoref

def iter_manager_nodes(bdd):
    for u in bdd._bdd._succ:
        yield bdd._wrap(u)

bdd = autoref.BDD()
bdd.declare('x', 'y')
u = bdd.add_expr('x \/ y')
nodes = list(iter_manager_nodes(bdd))
print(nodes)

[glarange]

Sweet. First recursive BDD external function I run. (I realize it's all recursive inside. ) This runs well and supersedes something similar that was shown in the design principles with I think the deprecated _succ. I pointed this out in another issue posted today. Thanks once more.

[johnyf]

As commented in https://github.com/tulip-control/dd/issues/61#issuecomment-682202023, _succ is an attribute of the class dd.bdd.BDD, not of the class dd.autoref.BDD. The example function print_descendants in the documentation is designed to be used with the class dd.bdd.BDD.