|
|
|---|
|
|
|
|---|
(atomic macro) prove the current goal using bdds
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
This command simply calls the theorem prover with the indicated bdd hint
for the top-level goal. Note that if