Неожиданный вывод Cudd_bddIte - PullRequest
Новая
       28

Неожиданный вывод Cudd_bddIte

0 голосов
/ 14 сентября 2018

Я пытаюсь использовать Cudd_bddIte для реализации простых BDD. Следующий код работает должным образом, давая диаграмму на рисунке (которая представляет узел 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);

enter image description here

Однако, если я изменю оператор ITE для tmp2 на следующий 

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

Я получаю этот неожиданный график:

enter image description here

Для меня это неправильно, так как я ожидаю, что самая верхняя переменная все равно сразу же выдаст 1, если ложь, как на первом рисунке. Что я делаю не так?

1 Ответ

0 голосов
/ 16 сентября 2018

В (RO) BDD все переменные отображаются в определенном порядке.В вашем случае порядок выглядит как «v1, v2, v3», так как вы разместили его в таком порядке и , похоже, переупорядочение переменных не произошло.

Функция Cudd_bddIte не требуетчто вы уважаете порядок, когда вы строите BDD.Когда вы используете функцию bddIte в своем коде, вы используете эту функциональность: для построения «bdd» вы применяете функцию bddIte к переменной v3, используя два поддеревья над v1 и v2.Однако v3 находится в конце порядка переменных, поэтому все дерево реструктурируется.

И фактически второе отображаемое дерево обладает ожидаемым свойством: всякий раз, когда v3 имеетзначение TRUE, BDD отображает оценку переменной в TRUE.Это видно из того факта, что единственный способ достичь приемника «0» - через узел 0x2e, который предназначен для переменной v3, а приемник «0» может быть достигнут только тогда, когда выбран преемник узла.

...