Ошибка передачи логического выражения в CUDD (работает в BuDDy)

Question

Я пытаюсь найти общее количество узлов в Shared- BDD с использованием CUDD. Я уже написал C код с использованием BuDDy-2.4, и он работает нормально, но когда Я использую CUDD вместо BuDDy, Моя программа показывает ошибку.

My BuDDY C Файл:

//BuDDY_C Code for Node Count:    

#define X1 (a&b&c&d)|(!c&d&f)|(g&!g)    //Define Function-1 here
#define X2 (a&b&d&!c)|(!c&!c&d)^(g) //Define Function-2 here


#include<bdd.h>
#include<stdio.h>
#include<stdlib.h>

int main(void)
{
bdd z[2],a,b,c,d,e,f,g,h;
int i,INPUT=8,node_count,order[8]={2,5,1,6,0,4,3,7};

printf("\nGiven Variable Order:\t ");
    for(i=0;i<INPUT;i++)
        printf("%d \t",order[i]); 

   bdd_init(1000,100);
   bdd_setvarnum(INPUT);

        a = bdd_ithvar(order[0]);  //Assign Variable order stored in order[0] to a
        b = bdd_ithvar(order[1]);  //Assign Variable order stored in order[1] to b
        c = bdd_ithvar(order[2]);  //Assign Variable order stored in order[2] to c
        d = bdd_ithvar(order[3]);  //Assign Variable order stored in order[3] to d
        e = bdd_ithvar(order[4]);  //Assign Variable order stored in order[4] to e
        f = bdd_ithvar(order[5]);  //Assign Variable order stored in order[5] to f
        g = bdd_ithvar(order[6]);  //Assign Variable order stored in order[6] to g
        h = bdd_ithvar(order[7]);  //Assign Variable order stored in order[7] to h


    z[0]=X1; 
    z[1]=X2;
   node_count=bdd_anodecount(z,2);
   bdd_done();
   printf("\n Total no of nodes are %d\n",node_count);
   return 0;

}

Мой CUDD C Программа:

//CUDD_C Code for Node Count
#define X1 (a&b&c&d)|(!c&d&f)|(g&!g)    //Define Function-1 here
#define X2 (a&b&d&!c)|(!c&!c&d)^(g) //Define Function-2 here

#include <stdio.h>
#include <stdlib.h>
#include "cudd.h"

int main(void) {
DdNode *z[2],*a,*b,*c,*d,*e,*f,*g,*h;
int i,INPUT=8,node_count,order[8]={2,5,1,6,0,4,3,7};

printf("\nGiven Variable Order:\t ");
    for(i=0;i<INPUT;i++)
        printf("%d \t",order[i]); 

DdManager * mgr = Cudd_Init(INPUT,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);


 a = Cudd_bddIthVar(mgr, order[0]);  //Assign Variable order stored in order[0] to a
 b = Cudd_bddIthVar(mgr, order[1]);  //Assign Variable order stored in order[0] to b
 c = Cudd_bddIthVar(mgr, order[2]);  //Assign Variable order stored in order[0] to c
 d = Cudd_bddIthVar(mgr, order[3]);  //Assign Variable order stored in order[0] to d
 e = Cudd_bddIthVar(mgr, order[4]);  //Assign Variable order stored in order[0] to e
 f = Cudd_bddIthVar(mgr, order[5]);  //Assign Variable order stored in order[0] to f
 g = Cudd_bddIthVar(mgr, order[6]);  //Assign Variable order stored in order[0] to g
 h = Cudd_bddIthVar(mgr, order[7]);  //Assign Variable order stored in order[0] to h


    z[0]=X1; 
    z[1]=X2;


  Cudd_Ref(z[0]);
  Cudd_Ref(z[1]);
/*-----Calculate no of nodes and number of shared nodes*/

        node_count= Cudd_SharingSize( z, 2);   
    printf("\n Total no of nodes are %d\n",node_count);

  int err = Cudd_CheckZeroRef(mgr);
  Cudd_Quit(mgr);
  return err;
}

Но эта программа CUDD C показывает ошибку

<b>balal@balal-HP-H710</b>:<b>~/Desktop/cudd-3.0.0</b>$ g++ -o test test2_cudd.c -lbdd
<b>test2_cudd.c:</b> In function ‘<b>int main()</b>’:
<b>test2_cudd.c:2:14:</b> <b>error: </b>invalid operands of types ‘<b>DdNode*</b>’ and ‘<b>DdNode*</b>’ to binary ‘<b>operator&</b>’
 #define X1 (<b>a&b</b>&c&d)|(!c&d&f)|(g&!g) //Define Function-1 here
             <b>~^~</b>
<b>test2_cudd.c:30:7:</b> <b>note: </b>in expansion of macro ‘<b>X1</b>’
  z[0]=<b>X1</b>;
       <b>^~</b>
<b>test2_cudd.c:2:25:</b> <b>error: </b>invalid operands of types ‘<b>bool</b>’ and ‘<b>DdNode*</b>’ to binary ‘<b>operator&</b>’
 #define X1 (a&b&c&d)|(<b>!c&d</b>&f)|(g&!g) //Define Function-1 here
                       <b>~~^~</b>
<b>test2_cudd.c:30:7:</b> <b>note: </b>in expansion of macro ‘<b>X1</b>’
  z[0]=<b>X1</b>;
       <b>^~</b>
<b>test2_cudd.c:2:33:</b> <b>error: </b>invalid operands of types ‘<b>DdNode*</b>’ and ‘<b>bool</b>’ to binary ‘<b>operator&</b>’
 #define X1 (a&b&c&d)|(!c&d&f)|(<b>g&!g</b>) //Define Function-1 here
                                <b>~^~~</b>
<b>test2_cudd.c:30:7:</b> <b>note: </b>in expansion of macro ‘<b>X1</b>’
  z[0]=<b>X1</b>;
       <b>^~</b>
<b>test2_cudd.c:3:14:</b> <b>error: </b>invalid operands of types ‘<b>DdNode*</b>’ and ‘<b>DdNode*</b>’ to binary ‘<b>operator&</b>’
 #define X2 (<b>a&b</b>&d&!c)|(!c&!c&d)^(g) //Define Function-2 here
             <b>~^~</b>
<b>test2_cudd.c:31:7:</b> <b>note: </b>in expansion of macro ‘<b>X2</b>’
  z[1]=<b>X2</b>;
       <b>^~</b>
<b>test2_cudd.c:3:29:</b> <b>error: </b>invalid operands of types ‘<b>int</b>’ and ‘<b>DdNode*</b>’ to binary ‘<b>operator&</b>’
 #define X2 (a&b&d&!c)|(<b>!c&!c&d</b>)^(g) //Define Function-2 here
                        <b>~~~~~^~</b>
<b>test2_cudd.c:31:7:</b> <b>note: </b>in expansion of macro ‘<b>X2</b>’
  z[1]=<b>X2</b>;
       <b>^~</b>
<b>balal@balal-HP-H710</b>:<b>~/Desktop/cudd-3.0.0</b>$ 

Answer 1

Другая возможность - использовать интерфейс Cython для CUDD, который входит в пакет Python dd. Установка dd с модулем dd.cudd описана здесь и может быть обобщена как

pip download dd --no-deps
tar -xzf dd-*.tar.gz
cd dd-*/
python setup.py install --fetch --cudd

Это будет загружать и создавать CUDD, а также создавать и устанавливать привязки Cython для dd до CUDD. dd имеет привязки Cython также к BuDDy, и они могут быть построены аналогичным образом, когда пользователь загружает и создает BuDDy и передает --buddy в сценарий setup.py.

Пример кода может быть переведен в следующий код Python.

from dd import cudd as _bdd

bdd = _bdd.BDD()
bdd.declare('a', 'b', 'c', 'd', 'e', 'f', 'g', 'h')
# /\ is conjunction in TLA+, \/ disjunction, ~ negation
X1 = bdd.add_expr('(a /\ b /\ c /\ d) \/ (~ c /\ d /\ f) \/ (g /\ ~ g)')
    # note that g /\ ~ g is FALSE
X2 = bdd.add_expr('(a /\ b /\ d /\ ~ c) \/ ((~ c /\ ~ c /\ d) ^ g)')
    # note that ~ c /\ ~ c is ~ c


# using the operators &, |, ! for conjunction, disjunction, and negation
X1_ = bdd.add_expr('(a & b & c & d) \/ (!c & d & f) \/ (g & !g)')
X2_ = bdd.add_expr('(a & b & d & !c) \/ ((!c & !c & d) ^ g)')
assert X1 == X1_, (X1, X1_)
assert X2 == X2_, (X2, X2_)


def descendants(roots):
    """Return nodes reachable from `roots`.

    Nodes in `roots` are included.
    """
    if not roots:
        return set()
    visited = set()
    for u in roots:
        _descendants(u, visited)
    assert set(roots).issubset(visited), (roots, visited)
    return visited

def _descendants(u, visited):
    v, w = u.low, u.high
    # terminal node or visited ?
    if u.low is None or u in visited:
        return
    _descendants(v, visited)
    _descendants(w, visited)
    visited.add(u)


r = descendants([X1, X2])
print(len(r))

# plot diagrams of the results using GraphViz
bdd.dump('X1.pdf', [X1])
bdd.dump('X2.pdf', [X2])

Функция descendants вычисляет набор узлов, доступных из заданных узлов (узлы, на которые ссылаются X1 и X2) , включая заданные узлы. Ответ для переменной порядка в моем прогоне составляет 16 узлов. Диаграммы для BDD булевых функций X1 и X2 следующие.

BDD булевой функции X1

X1">

BDD логической функции X2

X2">

Answer 2

Вы пытаетесь использовать оператор «&» на узлах BDD при написании вашей программы на C. Поскольку C не поддерживает перегрузку операторов, это не сработает, потому что оператор "&" может в большинстве случаев означать получение побитового И адресов, что вам не нужно.

Для того, чтобы вычислить AND двух BDD, вы должны использовать функцию Cudd_bddAnd. См., Например, здесь для примера. Обратите внимание, что таким образом ваши макросы станут намного длиннее и должны включать локальные переменные помимо областей действия.

Альтернативой является использование интерфейса C ++ для CUDD, где BDD могут быть инкапсулированы в объекты, поддерживающие перегрузку операторов. .

Обратите внимание, что

z[0]=X1; 
z[1]=X2;
Cudd_Ref(z[0]);
Cudd_Ref(z[1]);

также может вызвать проблемы. В CUDD на узлы необходимо ссылаться с помощью Cudd_Ref (...) перед вызовом любой другой функции CUDD, которая может создавать новые узлы. Так как ваш макрос X2 включает в себя операции над BDD, это может произойти. Так что лучше сразу использовать Cudd_Ref (...) BDD. Лучше выглядит следующее:

z[0]=X1; 
Cudd_Ref(z[0]);
z[1]=X2;
Cudd_Ref(z[1]);

Обратите внимание, что код вашего друга также неверен по той же причине. Однако, поскольку тип BDD определен как "typedef int BDD;" вместо этого компилятор использовал побитовые AND и OR для номеров узлов BDD, поэтому он скомпилирован в код, который дает неправильные результаты.