1

Cudd_bddIteシンプルなBDDを実装するために使用しようとしています。次のコードは期待どおりに機能し、図の図 ( node を表しますbdd)を示します。

DdNode *v1 = Cudd_bddNewVar(gbm);
Cudd_Ref(v1);

DdNode *v2 = Cudd_bddNewVar(gbm);
Cudd_Ref(v2);

DdNode *v3 = Cudd_bddNewVar(gbm);
Cudd_Ref(v3);

DdNode *tmp1 = Cudd_bddIte(gbm, v1, Cudd_ReadLogicZero(gbm), Cudd_ReadOne(gbm));
Cudd_Ref(tmp1);

DdNode *tmp2 = Cudd_bddIte(gbm, v2, tmp1, Cudd_ReadOne(gbm));
Cudd_Ref(tmp2);
Cudd_RecursiveDeref(gbm,tmp1);

DdNode *bdd = Cudd_bddIte(gbm, v3, tmp2, Cudd_ReadOne(gbm));
Cudd_Ref(bdd);
Cudd_RecursiveDeref(gbm,tmp2);

ここに画像の説明を入力

ただし、ITEステートメントをtmp2次のように変更すると

DdNode *tmp2 = Cudd_bddIte(gbm, v2, tmp1, Cudd_ReadLogicZero(gbm));

この予期しないグラフが表示されます。

ここに画像の説明を入力

最初の図のように、false の場合、最上位の変数がすぐに 1 を返すと予想されるため、これは間違っています。私は何を間違っていますか？

4

1 に答える 1