# Bdd

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.)

Further information about BDDs in ACL2 can be found in the subtopics of
this documentation section. In particular, see bdd-introduction
for a good starting place that provides a number of examples.

See hints for a description of :bdd hints. For quick
reference, here is an example; but only the :vars part of the hint is
required, as explained in the documentation for hints. The values
shown are the defaults.

(:vars nil :bdd-constructors (cons) :prove t :literal :all)

We suggest that you next visit the documentation topic bdd-introduction.

### Subtopics

- If*
- For conditional rewriting with BDDs
- Bdd-algorithm
- Summary of the BDD algorithm in ACL2
- Bdd-introduction
- Examples illustrating the use of BDDs in ACL2
- Show-bdd
- Inspect failed BDD proof attempts
- Obdd
- Ordered binary decision diagrams with rewriting