2

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

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

4

2 回答 2

2

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

  1. BDD 经理
  2. 您希望将变量替换为其他变量的 BDD。
  3. 第一个变量数组（由也Cudd_bddNewVar将返回的 BDD 节点表示）
  4. 第二个变量数组
  5. 正在交换的变量数。

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

于 2017-02-24T16:56:00.860 回答
0

使用 Cython 绑定到包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_
于 2017-10-15T21:49:29.400 回答