假设DdManager
有四个变量:x, y, x', y'
并且我有一个由x
and构建的 BDD y
。现在我想更改x
为x'
, y
,y'
即获得由x'
and构建的相同 BDD y'
。
我怎样才能使用 CUDD 包得到这个?当我想实现模型检查算法时遇到了这个问题。我想知道如何实现这个操作或者我是否误解了符号模型检查算法?非常感谢!
假设DdManager
有四个变量:x, y, x', y'
并且我有一个由x
and构建的 BDD y
。现在我想更改x
为x'
, y
,y'
即获得由x'
and构建的相同 BDD y'
。
我怎样才能使用 CUDD 包得到这个?当我想实现模型检查算法时遇到了这个问题。我想知道如何实现这个操作或者我是否误解了符号模型检查算法?非常感谢!
您可以使用函数来执行此操作Cudd_bddSwapVariables
。它获取以下参数:
Cudd_bddNewVar
将返回的 BDD 节点表示)您将需要自己分配和释放数组。
使用 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_