Ordered binary decision diagrams with rewriting
Note. The ACL2 bdd capability has been essentially superseded by GL; see gl.
Ordered binary decision diagrams (OBDDs, often simply called BDDs) are a technique, originally published by Randy Bryant, for the efficient simplification of Boolean expressions. In ACL2 we combine this technique with rewriting to handle arbitrary ACL2 terms that can represent not only Boolean values, but non-Boolean values as well. In particular, we provide a setting for deciding equality of bit vectors (lists of Boolean values).
An introduction to BDDs for the automated reasoning community may be found in ``Introduction to the OBDD Algorithm for the ATP Community'' by J Moore, Journal of Automated Reasoning (1994), pp. 33–45. (This paper also appears as Technical Report #84 from Computational Logic, Inc.)
See hints for a description of
(:vars nil :bdd-constructors (cons) :prove t :literal :all)
We suggest that you next visit the documentation topic bdd-introduction.