CODEWITHSUNDEEP
model-checkingbinary-decision-diagramcudd
HelloWorld
HelloWorld

Reputation: 47

How can I replace some variables in a BDD by CUDD package？

Suppose DdManager has four variables: x, y, x', y' and I have a BDD built by x and y. Now I want to change x to x', y to y', namely, get an identical BDD built by x' and y'.

How can I get this using the CUDD package? I encountered this problem when I wanted to implement a model checking algorithm. I want to know how to implement this operation or whether I misunderstand the symbolic model checking algorithm? Thank you very much!

Upvotes: 2

Views: 598

Answers (2)

0 _
0 _

Reputation: 11464

Example of variable substitution using the Cython bindings to CUDD that are included in the package dd:

from dd import cudd

bdd = cudd.BDD()  # instantiate a shared BDD manager
bdd.declare("x", "y", "x'", "y'")
u = bdd.add_expr(r"x \/ y")  # create the BDD for the disjunction of x and y
rename = dict(x="x'", y="y'")
v = bdd.let(rename, u)  # substitution of x' for x and y' for y
s = bdd.to_expr(v)
print(s)  # outputs:  "ite(x', TRUE, y')"

# another way to confirm that the result is as expected
v_ = bdd.add_expr(r"x' \/ y'")
assert v == v_

Upvotes: 0

DCTLib
DCTLib

Reputation: 1056

You do this with the function Cudd_bddSwapVariables. It gets the following parameters:

  1. A BDD Manager
  2. The BDD where you want to replace variables by others.
  3. The first array of variables (represented by the BDD nodes that also Cudd_bddNewVar would return)
  4. The second array of variables
  5. The number of variables being swapped.

You will need to allocate and free the arrays yourself.

Upvotes: 3

Related Questions