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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
<html>
<head><title>PSTACK.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>PSTACK</h2>seeing what is the prover up to
<pre>Major Section: <a href="OTHER.html">OTHER</a>
</pre><p>
<pre>
General Forms:
(pstack) ; inspect break
(pstack t) ; inspect break, printing all calls in abbreviated form
(pstack :all) ; as above, but only abbreviating the ACL2 world
</pre>
<p>
When the form <code>(pstack)</code> is executed during a break from a proof, or at the
end of a proof that the user has aborted, a ``process stack'' (or ``prover
stack'') will be printed that gives some idea of what the theorem prover has
been doing. Moreover, by evaluating <code>(verbose-pstack t)</code> before
starting a proof (see <a href="VERBOSE-PSTACK.html">verbose-pstack</a>) one can get trace-like information
about prover functions, including time summaries, printed to the screen
during a proof. This feature is currently quite raw and may be refined
considerably as time goes on, based on user suggestions. For example, the
usual control of printing given by <a href="SET-INHIBIT-OUTPUT-LST.html">set-inhibit-output-lst</a> is irrelevant
for printing the pstack.<p>
The use of <code>(pstack t)</code> or <code>(pstack :all)</code> should only be used
by those who are comfortable looking at functions in the ACL2 source code.
Otherwise, simply use <code>(pstack)</code>.
<p>
<ul>
<li><h3><a href="VERBOSE-PSTACK.html">VERBOSE-PSTACK</a> -- seeing what is the prover up to (for advanced users)
</h3>
</li>
</ul>
Entries in the pstack include the following (listed here alphabetically,
except for the first).<p>
<code>preprocess-clause</code>, <code>simplify-clause</code>, etc. (in general,<code>xxx-clause</code>):
top-level processes in the prover ``waterfall''<p>
<code>clausify</code>: splitting a goal into subgoals<p>
<code>ev-fncall</code>: evaluating a function on explicit arguments<p>
<code>ev-fncall-meta</code>: evaluating a metafunction<p>
<code>forward-chain</code>: building a context for the current goal using
<code><a href="FORWARD-CHAINING.html">forward-chaining</a></code> rules<p>
<code>induct</code>: finding an induction scheme<p>
<code>pop-clause</code>: getting the next goal to prove by induction<p>
<code>process-assumptions</code>: creating forcing rounds<p>
<code>remove-built-in-clauses</code>: removing built-in clauses (see <a href="BUILT-IN-CLAUSES.html">built-in-clauses</a>)<p>
<code>process-equational-polys</code>: deducing interesting equations<p>
<code>remove-trivial-equivalences</code>: removing trivial equalities (and
equivalences) from the current goal<p>
<code>rewrite-atm</code>: rewriting a top-level term in the current goal<p>
<code>setup-simplify-clause-pot-lst</code>: building the linear arithmetic database
for the current goal<p>
<code>strip-branches</code>, <code>subsumption-replacement-loop</code>: subroutines of
<code>clausify</code><p>
<code>waterfall</code>: top-level proof control<p>
<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>
|
