Major Section: OTHER
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
When the form (pstack) 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 (verbose-pstack t) before
starting a proof (see verbose-pstack) 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 set-inhibit-output-lst is irrelevant
for printing the pstack.
The use of (pstack t) or (pstack :all) should only be used
by those who are comfortable looking at functions in the ACL2 source code.
Otherwise, simply use (pstack).
preprocess-clause, simplify-clause, etc. (in general,xxx-clause):
top-level processes in the prover ``waterfall''
clausify: splitting a goal into subgoals
ev-fncall: evaluating a function on explicit arguments
ev-fncall-meta: evaluating a metafunction
forward-chain: building a context for the current goal using
forward-chaining rules
induct: finding an induction scheme
pop-clause: getting the next goal to prove by induction
process-assumptions: creating forcing rounds
remove-built-in-clauses: removing built-in clauses (see built-in-clauses)
process-equational-polys: deducing interesting equations
remove-trivial-equivalences: removing trivial equalities (and
equivalences) from the current goal
rewrite-atm: rewriting a top-level term in the current goal
setup-simplify-clause-pot-lst: building the linear arithmetic database
for the current goal
strip-branches, subsumption-replacement-loop: subroutines of
clausify
waterfall: top-level proof control