A Hons-based implementation of Boolean Expression Diagrams, described by Anderson and Hulgaard.
NOTE: this is a preliminary, work in progress. We do not recommend using this library for anything, yet.
In this library we represent BEDs using a Hons-based approach similar to ACL2::ubdds or ACL2::aigs. You would ordinarily expect a BED to be represented as a DAG. We instead use HONS to make the DAG explicit. This allows us to refer to particular nodes in the graph as if they were individual expressions, and makes it much easier to reason about BEDs. It is likely that an approach like ACL2::aignet could be used to develop a faster BED implementation, but we think this would be a lot more work.
BEDs are a non-canonical representation. The basic idea of our representation is:
Bed ::= Atom ; Terminal node | (VAR . (LEFT . RIGHT)) ; Variable ITE node | ((LEFT . RIGHT) . OP) ; Binary operator node
In the "well-formed" case:
But we don't have an explicit
This representation is a little goofy, but it has been carefully designed.
Allowing any ACL2 object as a BED means that we don't need a