Level-Agnostic Unique Node Table

[ssoelvsten]

Assuming #444 and #697 use the ptr_uint64 directly instead of computing it, we don't need to include that information inside of the node itself: the parents already have "assigned" it a level! This also opens up for some node reuse, e.g. bdd_ithvar(...) and bdd_nithvar(...) requires merely 2 nodes in the table (which could be placed at indices 3 and 4 upon table construction).

We can further increase node reusage, if we think of the level as a (relative) offset. That is, a node at level i will only note down level j for its children but rather i-j. This way, the same set of three nodes can represent the xor of all adjacent variables.

[ssoelvsten]

Alfons Laarman mentioned, this idea is somewhat akin to variable shifting for SDDs. That might indicate this is a promising idea!