PSTACK

seeing what is the prover up to
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).

Entries in the pstack include the following (listed here alphabetically, except for the first).

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