### ACL2-PC::BDD

(atomic macro)
` `

prove the current goal using bdds
Major Section: PROOF-CHECKER-COMMANDS

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

The general form is as shown in the latter example above, but with
any keyword-value pairs omitted and with values as described for the
`:`

`bdd`

hint; see hints.

This command simply calls the theorem prover with the indicated bdd
hint for the top-level goal. Note that if `:prove`

is `t`

(the
default), then the proof will succeed entirely using bdds or else
it will fail immediately. See bdd.