2

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!

0 _
  • 10,524
  • 11
  • 77
  • 109
HelloWorld
  • 47
  • 4

2 Answers2

2

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.

0 _
  • 10,524
  • 11
  • 77
  • 109
DCTLib
  • 1,016
  • 8
  • 22
  • Thank you for your response! I have read the document and tried this function before but failed. After reading your response, I try again and succeed. Maybe I set wrong parameters before. Thank you~ – HelloWorld Feb 25 '17 at 08:08
0

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_
0 _
  • 10,524
  • 11
  • 77
  • 109