Major Section: ACL2-TUTORIAL
Maybe you've been using ACL2 for awhile, and you wonder if there are lesser-known features that you might find useful. Then this topic is for you. We present below a ``laundry list'' of some such features, with brief descriptions and links to documentation topics.
Although the list below is long, it is not intended to be complete, and
indeed some topics have been deliberately excluded. Some have fallen out of
use, perhaps for good reason, such as NU-REWRITER and OBDD. Others
are already likely to be discovered when needed, such as GETENV$ and
perhaps DOUBLE-REWRITE. Some topics are referenced by documentation
for others in the list, such as MBT, which is referenced by MBE.
Some utilities such as PSTACK and VERBOSE-PSTACK seem too
low-level to be worthy of inclusion below.
For an extensive introduction to using the prover, which may include some aspects new to you, see INTRODUCTION-TO-THE-THEOREM-PROVER. A shorter topic contains highlights for efficient prover usage: see TIPS. Also see ACL2-SEDAN for an extension of ACL2 (written by others), ACL2s, that includes an Eclipse-based interface, more powerful and automatic termination reasoning, and other features.
We now move on to the list.
======================================== Top-level commands and utilities: ========================================
o See A! and see P! to abort or pop.
o See ACL2-CUSTOMIZATION for initial commands to run at startup.
o See KEYWORD-COMMANDS for how keyword commands are processed.
o See LD for many ways to control the top-level loop.
o See COMPILATION for a discussion of
set-compiler-enabledand other compiler-related utilities.o For useful reader macros `
#!', `#.', and `#u', see SHARP-BANG-READER, see SHARP-DOT-READER, and see SHARP-U-READER.o To save and use an ACL2 executable, see ACL2-AS-STANDALONE-PROGRAM and see SAVE-EXEC.
o For utilities related to timing, see TIME$, see WITH-PROVER-TIME-LIMIT, see WITH-PROVER-STEP-LIMIT, and see SET-PROVER-STEP-LIMIT.
o To query and manage the database, see HISTORY (which discusses many useful utilities, such as
:PBTand:PL), and see DEAD-EVENTS.o See ADD-INCLUDE-BOOK-DIR for linking keyword for
:dirargument ofLDandINCLUDE-BOOK.o See REBUILD for a fast way to load a file without waiting for proofs.
o For parallel certification, see BOOK-MAKEFILES (
-joption of `make') and see PROVISIONAL-CERTIFICATION.
======================================== Some relatively less common events: ========================================
o See RESET-PREHISTORY to reset the prehistory.
o See ASSERT-EVENT to assert that a given form returns a non-nil value.
o See DEFATTACH to execute constrained functions using corresponding attached functions.
o See DEFUN-SK to define a function whose body has an outermost quantifier.
o See DEFCHOOSE to define a Skolem (witnessing) function.
o For efficiency consider using
defconst-fast; see DEFCONST.o See SET-VERIFY-GUARDS-EAGERNESS to specify when guard verification is tried by default.
======================================== Output and its control (see IO for additional information): ========================================
o See WITH-OUTPUT to suppress or turn on specified output for an event.
o See EVISC-TABLE for support for abbreviated output.
o See NTH-ALIASES-TABLE for a table used to associate names for
NTH/UPDATE-NTHprinting.o See OUTPUT-TO-FILE to redirect output to a file.
o See PRINT-CONTROL to control ACL2 printing.
o See SET-EVISC-TUPLE to control suppression of details when printing.
o See SET-INHIBIT-OUTPUT-LST to control output by type.
o See SET-IPRINT to allow abbreviated output to be read back in.
o See SET-PRINT-BASE to control the radix in which numbers are printed.
o See SET-PRINT-RADIX to control whether the radix of a number is printed.
o See SET-PRINT-CASE to control whether symbols are printed in upper case or in lower case.
======================================== On proving termination for definitions: ========================================
o See ORDINALS for a discussion of ordinals in ACL2.
o See RULER-EXTENDERS for a control on ACL2's termination and induction analyses.
o See SET-WELL-FOUNDED-RELATION to set the default well-founded relation for termination analysis.
o See ACL2-SEDAN for a related tool that provides extra automation for termination proofs.
======================================== Proof debugging and output control: ========================================
o See ACCUMULATED-PERSISTENCE to get statistics on which runes are being tried.
o See ADD-MACRO-FN and see ADD-MACRO-ALIAS to associate a function name with a macro name.
o See BREAK-REWRITE for how to monitor rewrite rules.
o See DMR for dynamic monitoring of rewriting and other prover activity.
o See FORWARD-CHAINING-REPORTS to see reports about the forward chaining process.
o See GUARD-DEBUG to generate markers to indicate sources of guard proof obligations.
o See PROOF-CHECKER for support for low-level interaction.
o See REDO-FLAT for redo on failure of a
PROGN,ENCAPSULATE, orCERTIFY-BOOK.o See SET-GAG-MODE and see PSO to abbreviate or restore proof output.
o See SET-INHIBIT-OUTPUT-LST, see SET-INHIBIT-WARNINGS, and see SET-INHIBITED-SUMMARY-TYPES to inhibit various types of output.
o See SET-RAW-PROOF-FORMAT to make proof output display lists of runes.
o See SKIP-PROOFS to skip proofs for a given form.
======================================== Program debugging: ========================================
o See BREAK$ to cause an immediate Lisp break.
o See BREAK-ON-ERROR to break when encountering a hard or soft error caused by ACL2.
o See DISASSEMBLE$ to disassemble a function.
o See PRINT-GV to print a form whose evaluation caused a guard violation.
o See PROFILE to turn on profiling for one function.
o See TRACE$ and see OPEN-TRACE-FILE to trace function evaluations, possibly sending trace output to a file.
o See WET to evaluate a form and print a subsequent error trace.
========================================
Programming and evaluation idioms, support, utilities (also see PROGRAMMING
for more utilities, e.g., RANDOM$)
========================================
o See ARRAYS and See DEFSTOBJ for introductions to ACL2 arrays and single-threaded objects (stobjs), respectively, each of which provides efficient destructive operations in an applicative setting. Also see WITH-LOCAL-STOBJ for a way to create local stobjs.
o See ASSERT$ to cause a hard error if the given test is false.
o See CANONICAL-PATHNAME to obtain the true absolute filename, with soft links resolved.
o See CASE-MATCH for a utility providing pattern matching and destructuring.
o See DEFPUN to define a tail-recursive function symbol.
o See EC-CALL to execute a call in the ACL2 logic instead of raw Lisp.
o See ER to print an error message and ``cause an error''.
o See FLET to provide local binding of function symbols.
o See GC$ to invoke the garbage collector.
o See MBE to attach code for execution.
o See MV-LIST to convert a multiple-valued result to a single-valued list.
o See MV? to return one or more values.
o For non-executable code, see DEFUN-NX and see NON-EXEC.
o See PROG2$ and see PROGN$ to execute two or more forms and return the value of the last one.
o See PROGRAMMING-WITH-STATE for how to program using the von Neumannesque ACL2 state object.
o See TOP-LEVEL to evaluate a top-level form as a function body.
o See WITH-GUARD-CHECKING to suppress or enable guard-checking for a form.
o For ways to fake access to the state see WORMHOLE, see WITH-LOCAL-STATE, see CW, see CW!, see PRINTING-TO-STRINGS, see OBSERVATION-CW, and (dangerous!) see WITH-LIVE-STATE.
======================================== Connecting with the underlying host Lisp, and doing other evil: ========================================
o See DEFTTAG to introduce a trust tag (ttag).
o See DEFMACRO-LAST to define a macro that returns its last argument, but with side effects.
o See PROGN! to evaluate forms that are not necessarily events.
o See RETURN-LAST to return the last argument, perhaps with side effects.
o See SET-RAW-MODE to enter or exit ``raw mode,'' a raw Lisp environment.
o See SYS-CALL to make a system call to the host operating system.
======================================== Macros and related utilities: ========================================
o See DEFABBREV for a convenient form of macro definition for simple expansions.
o See MACRO-ARGS for the formals list of a macro definition (see DEFMACRO).
o See MAKE-EVENT for a sort of extension of
DEFMACROthat allows access to the state, by evaluating (expanding) a given form and then evaluate the result of that expansion.o See TRANS, see TRANS!, and see TRANS1 to print the macroexpansion of a form.
======================================== Experimental extensions: ========================================
o See HONS-AND-MEMOIZATION for ACL2(h); in particular, see MEMOIZE for efficient function memoization and see PROFILE for profiling.
o See REAL for ACL2(r), which supports the real numbers.
o See PARALLELISM for ACL2(p), which supports parallel evaluation and proof.
======================================== Database control and query: ========================================
o See DISABLEDP to determine whether a given name or rune is disabled.
o For redefinition support see REDEF, see REDEF!, see REDEF+, see REDEF-, and see REDEFINED-NAMES.
o See TABLE for user-managed tables.
o See VERIFY-GUARDS-FORMULA to view a guard proof obligation without doing the proof.
======================================== Prover control ========================================
o For congruence-based reasoning see DEFCONG, see CONGRUENCE, see EQUIVALENCE, see DEFEQUIV, and see DEFREFINEMENT.
o For meta rules and clause processors see META, see DEFEVALUATOR, see CLAUSE-PROCESSOR, see DEFINE-TRUSTED-CLAUSE-PROCESSOR (for connecting with external tools, such as SAT solvers), and See EXTENDED-METAFUNCTIONS (for state and context-sensitive metafunctions).
o For theory control, see THEORIES for detailed information, but in particular see DEFTHEORY, see THEORY-FUNCTIONS, see IN-ARITHMETIC-THEORY (and see NON-LINEAR-ARITHMETIC), and see THEORY-INVARIANT.
o See HINTS for a complete list of prover hints, including some of the more obscure ones such as
:restrict,:clause-processor,:nonlinearp,:backchain-limit-rw,:reorder, and:backtrack. Also see HINTS-AND-THE-WATERFALL for an explanation of how hints interact with the ACL2 proof process. For other topics related to hints, see OVERRIDE-HINTS, see ADD-CUSTOM-KEYWORD-HINT, see DEFAULT-HINTS, and see COMPUTED-HINTS (also see USING-COMPUTED-HINTS and for other topicsUSING-COMPUTED-HINTS-xxxsee MISCELLANEOUS. o See BIND-FREE to bind free-variables of a rewrite or linear rule.o See CASE-SPLIT for a utility like
FORCEthat immediately splits the top-level goal on the indicated hypothesis.o See CASE-SPLIT-LIMITATIONS for a way to the number of cases produced at once
o See DEFAULT-BACKCHAIN-LIMIT to specify the backchain limit for a rule.
o See FORCE for an identity function used to force a hypothesis.
o See OTF-FLG for a way to push more than one initial subgoal for induction.
o See RULE-CLASSES to add various kinds of rules to the database, including more unusual sorts such as
:built-in-clauserules and:inductionrules.o See SET-BACKCHAIN-LIMIT to set the backchain-limit used by the type-set and rewriting mechanisms.
o See SET-BODY to set an alternate definition body for
:expandhints.o See SET-REWRITE-STACK-LIMIT to set the rewrite stack depth used by the rewriter.
o See SYNTAXP to attach a heuristic filter on a
:rewrite,:meta, or:linearrule.
