DdManagerには、x, y, x', y'という変数があり、BDDはxとyで作成されています。 は、今私は、すなわち、x'とy'によって構築された、同一のBDDを取得し、y'にx'からx、yを変更したいです。BDDの変数をCUDDパッケージで置き換えるにはどうすればよいですか？
CUDDパッケージを使用してこれを取得するにはどうすればよいですか？私はモデル検査アルゴリズムを実装したいときにこの問題に遭遇しました。私はこの操作を実装する方法を知りたいか、シンボリックモデル検査アルゴリズムを誤解しているかどうかを知りたいですか？ ありがとうございます！
これは、機能Cudd_bddSwapVariablesで行います。
Cudd_bddNewVarを返すBDDノードによって表される）の変数の第1のアレイ自分で配列を割り当てて解放する必要があります。 package ddに含まれているCUDDにCythonバインディングを使用して変数置換の
例：
from dd import cudd
bdd = cudd.BDD() # instantiate a shared BDD manager
bdd.declare("x", "y", "x'", "y'")
u = bdd.add_expr("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)
>>> s
"ite(x', TRUE, y')"
# another way to confirm the result is as expected
v_ = bdd.add_expr("x' \/ y'")
assert v == v_
はご回答いただきありがとうございます！私は文書を読んで、この機能を試してみましたが失敗しました。あなたの応答を読んだ後、私はもう一度やり直します。おそらく私は前に間違ったパラメータを設定しています。ありがとう〜 – HelloWorld