1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
<html>
<head><title>SHOW-BDD.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>SHOW-BDD</h2>inspect failed BDD proof attempts
<pre>Major Section: <a href="BDD.html">BDD</a>
</pre><p>
Attempts to use BDDs (see <a href="BDD.html">bdd</a>), using <code>:</code><code><a href="BDD.html">bdd</a></code> <a href="HINTS.html">hints</a>,
can fail for various reasons. Sometimes it is useful to explore
such failures. To do so, one may simply execute the form
<pre>
(show-bdd)
</pre>
inside the ACL2 loop. The system's response is generally
self-explanatory. Perhaps you have already seen <code>show-bdd</code> used in
some examples (see <a href="BDD-INTRODUCTION.html">bdd-introduction</a> and see <a href="IF_star_.html">if*</a>). Here we
give some details about <code>show-bdd</code>.
<p>
<code>(Show-bdd)</code> prints the goal to which the BDD procedure was applied
and reports the number of nodes created during the <a href="BDD.html">BDD</a>
computation, followed by additional information depending on whether
or not the computation ran to completion or aborted (for reasons
explained elsewhere; see <a href="BDD-ALGORITHM.html">bdd-algorithm</a>). If the computation
did abort, a backtrace is printed that should be useful in
understanding where the problem lies. Otherwise, <code>(show-bdd)</code>
prints out ``falsifying constraints.'' This list of pairs
associates <a href="TERM.html">term</a>s 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 <a href="TERM.html">term</a> that is the result
of simplifying the input <a href="TERM.html">term</a>. 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
<a href="TERM.html">term</a>), which may be quite large. The following responses are
legal:
<blockquote>
<code> w</code> -- Walk around the object with a structure editor<p>
<code> t</code> -- Print the object in full<p>
<code>nil</code> -- Do not print any more of the object
</blockquote>
<p>
<code>Show-bdd</code> actually has four optional arguments, probably rarely
used. The general form is
<pre>
(show-bdd goal-name goal-ans falsifying-ans term-ans)
</pre>
where <code>goal-name</code> is the name of the goal on which the <code>:</code><code><a href="BDD.html">bdd</a></code>
hint was used (or, <code>nil</code> if the system should find such a goal),
<code>goal-ans</code> is the answer to be used in place of the query for
whether to print the input goal in full, <code>falsifying-ans</code> is the
answer to be used in place of the query for whether to print the
falsifying constraints in full, and <code>term-ans</code> is the answer to be
used in place of the query for whether to print the resulting
<a href="TERM.html">term</a> in full.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
