Hi, can you please tell me how can I copy one bdd to another?

[johnyf]

BDDs can be copied between different BDD managers. Within a single BDD manager, each BDD is uniquely represented, so there is no notion of copying a BDD within the same BDD manager. An example of copying/transferring a BDD from a BDD manager to another BDD manager is at https://github.com/tulip-control/dd/blob/f9aa4d1a09c286de769bde17dd92ece63cf4c3d9/examples/transfer_bdd.py. Please see also https://github.com/tulip-control/dd/issues/57#issuecomment-650327509 for copying between BDD managers and ZDD managers.

An example that copies the nodes of a BDD from an instance of the class dd.cudd.BDD (a BDD manager implemented using the C library CUDD) to an instance of the class dd.autoref.BDD is

from dd import cudd
from dd import autoref

bdd_manager_1 = cudd.BDD()  # instantiate a BDD manager implemented in Cython using the C library CUDD
bdd_manager_1.declare('x', 'y')  # register some variable names
u = bdd_manager_1.add_expr('x \/ y')  # create the BDD of the disjunction of x and y

bdd_manager_2 = autoref.BDD()  # instantiate another BDD manager, this one implemented in Python
bdd_manager_2.declare(*bdd_manager_1.vars)  # declare the variables x, y also in `bdd_manager_2`
v = bdd_manager_1.copy(u, bdd_manager_2)  # copy the nodes used to represent BDD `u` from the `bdd_manager_1` to `bdd_manager_2`

v_ = bdd_manager_2.add_expr('x \/ y')  # directly create the BDD of the disjunction of x and y in `bdd_manager_2`
assert v == v_, (v, v_)  # confirm that copying yields the correct result

It may also be useful to consult the module dd._copy.

BDDs can also be dumped to a file and loaded from a file (pickle files when using the class dd.autoref.BDD and DDDMP files when using the class dd.cudd.BDD), and dumped to PDF files in the form of diagrams.