BDD

Parent topic:  Home

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

• BDD-ALGORITHM -- summary of the BDD algorithm in ACL2

• BDD-INTRODUCTION -- examples illustrating the use of BDDs in ACL2

• IF* -- for conditional rewriting with BDDs

• SHOW-BDD -- inspect failed BDD proof attempts

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)