Анализатор логических выражений для CUDD

Другая возможность — работать на Python, используя привязки Cython к CUDD:

from dd import cudd

bdd = cudd.BDD()
bdd.declare('a', 'b')
u = bdd.add_expr('a /\ ~ b')
s = bdd.to_expr(u)
print(s)

Начиная с dd == 0.5.3, файлы колес доступны в PyPI и содержат скомпилированную версию CUDD. Таким образом, pip install dd также установит CUDD в любой среде Linux с версией Python, соответствующей колесам (3.5 или 3.6).

Отказ от ответственности: я являюсь автором пакета dd.

Есть пара проектов, в которых уже содержится функциональность для разбора строки в BDD.

Например, на https://github.com/LTLMoP/slugs/blob/master/src/synchronousContextBasics.cpp, строки 22–64, вы можете найти простой синтаксический анализатор для шлифовки логических формул нормальной формы в C++. At предполагает, что переменные уже выделены, а ссылки BDD для узлов, представляющих переменные, хранятся в массивах «variables[..]», а их соответствующие имена хранятся в «variabeNames[...]». Адаптация общей идеи к C относительно прост. Класс «BF» в этом коде является оболочкой для ссылок «DdNode*».

Если вам нужна инфиксная нотация, вы всегда можете использовать yacc/lex для создания простого синтаксического анализатора, который сделает это за вас.