SHOW-BDD

inspect failed BDD proof attempts
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.