Alternative decision diagram library

[grencez]

The glu 2.4 multi-value decision diagram library seems to cause problems on Mac, and Windows cannot build it.

One path forward to implement an MDD structure ourselves. Pham and Emerson (https://www.researchgate.net/publication/236149939_Implementing_Binary_Decision_Diagram) show the algorithm for BDDs.

• We can save memory by serializing the DD nodes in a bit vector, using only as many bits as necessary to represent variable and node indices.
• Node storage is aligned to byte boundary.
  • size_t is guaranteed to hold node id.
  • hash table can point to key easily.
• Represent False and True as 00 and 01 bits to save space. Others have a preceding 1 bit.

The necessary functions are just:

• make(ctx, sign): 1 is true, -1 is false
• restrict(&x, var, val): x &= (var=val)
• smooth(&x, signz, z): x without vars set in z, or x with only the vars in z
• transition(x, y): f such that f(x)=y
• ite(x, signy, y, signz, z):
• image(f, x): f(x)
• preimage(f, y): minimal x where f(x) = y

Supporting data structures:

• Hash map for (xnode, y_or_z) -> node idx
• Hash map for node content -> node idx
• Function to extract bits from bytes