Major Section: BDD
Attempts to use BDDs (see bdd), using :bdd hints,
can fail for various reasons. Sometimes it is useful to explore
such failures. To do so, one may simply execute the form
(show-bdd)inside the ACL2 loop. The system's response is generally self-explanatory. Perhaps you have already seen
show-bdd used in
some examples (see bdd-introduction and see if*). Here we
give some details about show-bdd.
(Show-bdd) prints the goal to which the BDD procedure was applied
and reports the number of nodes created during the BDD
computation, followed by additional information depending on whether
or not the computation ran to completion or aborted (for reasons
explained elsewhere; see bdd-algorithm). If the computation
did abort, a backtrace is printed that should be useful in
understanding where the problem lies. Otherwise, (show-bdd)
prints out ``falsifying constraints.'' This list of pairs
associates terms with values and suggests how to construct a
binding list for the variables in the conjecture that will falsify
the conjecture. It also prints out the term that is the result
of simplifying the input term. In each of these cases, parts
of the object may be hidden during printing, in order to avoid
creating reams of uninteresting output. If so, the user will be
queried about whether he wishes to see the entire object (alist or
term), which may be quite large. The following responses are
legal:
w-- Walk around the object with a structure editor
t-- Print the object in full
nil-- Do not print any more of the object
Show-bdd actually has four optional arguments, probably rarely
used. The general form is
(show-bdd goal-name goal-ans falsifying-ans term-ans)where
goal-name is the name of the goal on which the :bdd
hint was used (or, nil if the system should find such a goal),
goal-ans is the answer to be used in place of the query for
whether to print the input goal in full, falsifying-ans is the
answer to be used in place of the query for whether to print the
falsifying constraints in full, and term-ans is the answer to be
used in place of the query for whether to print the resulting
term in full.
