Show-bdd
Inspect failed BDD proof attempts
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
y — Print the object in full
n — 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 nil if there is to be a query and otherwise is the
answer to be used (without a query) for whether to print the input goal in
full (t for 'y', nil for 'n', and :w for 'w'),
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.
