如何用CUDD包替换BDD中的一些变量？

Question

假设 DdManager 有四个变量：x, y, x', y' 并且我有一个由 x 和 y 构建的 BDD。现在我想将 x 更改为 x'，将 y 更改为 y'，即获得由 x' 和 y' 构建的相同 BDD。

我如何使用 CUDD 包获得它？我在想实现一个模型检查算法时遇到了这个问题。我想知道如何实现这个操作或者我是否误解了符号模型检查算法？非常感谢！

Answer 1

您可以使用函数 Cudd_bddSwapVariables 执行此操作。它获取以下参数：

BDD 经理
您想用其他变量替换变量的 BDD。
第一个变量数组（由同样 Cudd_bddNewVar 将 return 表示的 BDD 节点表示）
第二个变量数组
交换的变量数。

您需要自己分配和释放数组。

Answer 2

使用 Cython 绑定到 package dd 中包含的 CUDD 的变量替换示例：

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_

如何用CUDD包替换BDD中的一些变量？

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

model-checking

binary-decision-diagram

cudd