CODEWITHSUNDEEP
cboolean-expressioncudd
ashishbaghudana
ashishbaghudana

Reputation: 429

Boolean Expression Parser for CUDD

I am using the CUDD library on C for making Binary Decision Diagrams. I was wondering if there is some way to convert a Boolean expression given as a string to a Binary Decision Diagram.

Thank you!

Upvotes: 1

Views: 442

Answers (2)

0 _
0 _

Reputation: 11484

Another possibility is to work in Python, using Cython bindings to CUDD:

from dd import cudd

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

As of dd == 0.5.6, wheel files are available from PyPI that include a compiled version of CUDD. So in any Linux environment with Python version that matches that of the wheels, pip install dd will also install dd.cudd, linked to CUDD.

Note: I am an author of the package dd.

Upvotes: 1

DCTLib
DCTLib

Reputation: 1056

There are a couple of projects around in which the functionality to parse a string to a BDD is already contained.

For an example, at https://github.com/LTLMoP/slugs/blob/master/src/synthesisContextBasics.cpp, lines 22-64, you can find a simple parser for polish normal form boolean formulas in C++. At assumes that the variables have already been allocated and BDD references for nodes representing the variables are stored in the arrays "variables[..]" and their respective names are stored in "variabeNames[...]" Adapting the general idea to C is relatively simple. The class "BF" in that code is a wrapper for "DdNode*" references.

If you want infix notation, you can always use yacc/lex to build a simple parser that will do that for you.

Upvotes: 1

Related Questions