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.