hello. i made a dd wrapper for bex.

[tangentstorm]

Hello, I'm the author of bex, a rust crate for working with Boolean expressions as BDDs, ANF polynomials, or just plain ASTs.

I have an experimental python wrapper here:

https://github.com/tangentstorm/bex/tree/main/py

It includes both a bare-bones python wrapper and from bex.dd import BDD, which passes all your tests from common.py and common_bdd.py (with a few tests slightly modified because bex breaks from convention and numbers variables from the bottom up).

Bex does BDD operations in parallel, like sylvan, and it also has support for collecting complicated expressions into an AST structure and then converting them to BDDs from the "top down", which allows it to work backwards and avoid work that would later be cancelled out (for example, by an AND 0 at the end). (This feature is not yet exposed to the python bindings...)

Anyway, I don't know if any of this would be interesting to you. I mostly work on bex for fun and (AFAIK) don't currently have any users. I made the dd wrapper so I can start benchmarking what I've done against other packages, but if you think this might be useful to your user base, I'm happy to collaborate.

Sorry for writing this as an issue. I didn't know where else to post it. :)

[johnyf]

Thanks for noting this. One possibility would be to add bex to the list of BDD packages at: https://github.com/johnyf/tool_lists/blob/main/bdd.md, where there are sections for Rust and for Python packages. The optimization when converting an AST to a BDD is interesting. It seems to integrate the leaf cases of BDD construction into the converter.

The current parser implementation in dd._parser converts strings directly to BDDs. Specifically dd._parser.Parser is the parser grammar and a conversion from strings to ASTs, and dd._parser.Translator is the conversion from strings to BDDs.

The motivation for the direct conversion was to parse long expressions without changing the recursion limit with sys.setrecursionlimit() or reaching the underlying C stack limit. Recursion is still present in the BDD operations, but the recursion depth there is bounded by the number of declared BDD variables. An earlier implementation used syntax trees (AST) as intermediate representation, and converted the ASTs recursively to BDDs.

Parsing long expressions via ASTs is possible also using an iterative converter from AST to BDD. There are iterative and recursive converters from AST to BDD in dd/tests/iterative_recursive_flattener.py. These are used in the tests of dd/tests/parser_test.py, together with dd._parser.Translator and dd._parser.Parser. For example, parser_test.test_linear_syntax_tree_to_bdd() constructs a syntax tree for which the recursive implementation raises RecursionError. The direct conversion of dd._parser.Translator is simpler than the iterative implementation in iterative_recursive_flattener._reduce_syntax_tree(), which is why it is used in dd._parser.add_expr().

[tangentstorm]

The optimization when converting an AST to a BDD is interesting. It seems to integrate the leaf cases of BDD construction into the converter.

Well, basic simplifications are done everywhere (x & 0 is always 0) unless you turn them off. But the basic way the converters work is that they assign a virtual variable to each node in the AST. So if the top node is node 500, we start with the bdd ite(v500,1,0)... And then recursively replace the top variable with its definition. So maybe that node is the AND of v200 and v499. We replace the v500 with ite(v499,ite(v200,1,0),0), and then v499 is the new top variable so we replace that. So now anywhere we can show that either of those two nodes are 0, we get to short circuit a bit.

(Then there's another version of that same algorithm that first reorders the levels so that at each step, the nodes you're using in the "replacement" of the highest numbered variable get moved up to the top so the rewrite is less impactful on the dag).

As for leaf nodes, the node references are 64-bit numbers (NIDs) that encode things like the branch variable, so the 0/1 constants and variables don't actually have any nodes allocated for them. There's just a constant NID for 0, 1, and in fact for each variable.

But the neat trick is the one I haven't implemented yet, and it's the reason for numbering things from the bottom: there's plenty of room in the NID to hold an entire 32-bit truth table, so in theory, there's no reason to ever allocate anything for a graph of the bottom 5 variables. (And in fact, with the other bits of the nid, you can get this up to "any combination of 5 or fewer of the bottom 85 variables")... All of the BDD ops on these can just be replaced with functions that operates entirely in the ALU on those 64 bits.

Aside from this (and being multi-threaded) there's really not anything special about what bex is doing... So if I'm to get my benchmarks right, I'll want to compare building an AST and converting from the top down to the normal bottom-up way of doing things... So, I'll probably expose the AST representation to python before too long.

I've only had a little time to look over the AST->BDD translations in dd. It seems like you're making a different distinction than me. AFAICT, they're both still composing BDDs from the bottom up, right?

Maybe it would be interesting to port my substitution algorithms over to python and see how the top down approach works for the other BDD packages.

Meanwhile, I'll submit a PR to get bex on your BDD list. Thanks!