		Search-engine friendly clone of the ACL2 documentation.

Boolean-reasoning

Bed

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:

All terminals are Booleans, i.e., t or nil
The variable names are any ACL2 atoms
The operators are valid bed-op-ps.

But we don't have an explicit bed-p recognizer and we can interpret any ACL2 object as a BED:

Any atom is coerced into a well-formed terminal using, e.g., (if x t nil).
Any improper operator is coerced into a bed-op-p using bed-op-fix.
In any (var . atom) pair, the atom is interpreted as (nil . nil).

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 bed-p recognizer and can avoid memoized checks of beds for well-formedness. Our goofy interpretation of the cons cases keeps each node to only two conses, without any ambiguity between variables and operators. Finally, checking atom is fast, so we can quickly distinguish variable from operator nodes.

Subtopics

Bed-op-p: Recognizer for BED operators.
Bed-from-aig: Translate an AIG into a BED.
Bed-mk1: Low-level functions for constructing BEDs.
Bed-eval: Semantics of BEDs.
Up: Preliminary implementation of UP operations described in the paper.
Aig-translation: Translators to convert Hons ACL2::aigs into BEDs, and vice-versa.