如何通过CUDD软件包?替换BDD中的某些变量

Question

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

如何使用CUDD软件包获得此功能？当我想实现模型检查算法时，我遇到了这个问题。我想知道如何实施此操作，还是误解了符号模型检查算法？非常感谢！

Answer 1

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

1. BDD Manager
2. 您想替换其他变量的BDD。
3. 第一个变量数组（由Cudd_bddNewVar也将返回的BDD节点表示）
4. 变量的第二个数组
5. 交换变量的数量。

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

Answer 2

使用与cudd的Cython绑定的可变替代示例，该bogdage 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_