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

Question

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

Спасибо!

Answer 1

Другая возможность - работать в 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 доступны файлы wheel, включающие скомпилированную версию CUDD. Так pip install dd также установит CUDD в любой среде Linux с версией Python, соответствующей колесам (3.5 или 3.6).

Отказ от ответственности: я автор пакета dd,

Answer 2

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

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

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