Efficiency considerations

This topic is a grab-bag of ideas for the efficient use of ACL2, including proofs and programming. It is far from complete, and tips for using ACL2 effectively may be found throughout the documentation. The present topic will, ideally, improve over time, both in its content and in its organization. Please contribute!

Here we discuss primarily time efficiency rather than space efficiency.
You can time forms using `time$`. That may show you that your tweaks
to proof scripts or function definitions don't make a noticeable difference!
We focus below on some techniques that have a reasonable chance of making a
difference.

Perhaps the most basic idea for carrying out proofs efficiently is to use rewriting effectively; see introduction-to-the-theorem-prover and, in particular, the sections on rewriting. Here we mention just a few common ways to improve the efficiency of rewriting in ACL2.

- Consider minimizing the number of hypotheses of a rule. See remove-hyps for a tool that can help with that.
- Manage theories effectively. See accumulated-persistence
for a way to identify rules that might best be disabled. In
particular, it can be useful to disable functions whose expansions generate
large case splits (see splitter); otherwise, sometimes it can be useful
to limit case-splits with
`set-case-split-limitations`. - When many similar proofs are being performed (for example, for families of similar theorems generated by macros), the tool removable-runes may be helpful.

Sometimes rewriting is slow for inherent algorithmic reasons. For example,
if you have a binary function,

(op d (op c (op b a))) (op d (op c (op a b))) (op d (op a (op c b))) (op d (op a (op b c))) (op a (op d (op b c))) (op a (op b (op d c))) (op a (op b (op c d)))

In such a case, you may find it very helpful to create a suitable meta rule or a clause-processor rule, to implement an `hide` to avoid exploring
terms that are in the expected form. Calls of

We conclude this section with ways to tweak the ACL2 system to speed up slow proofs. These can be especially useful if very large terms are involved. One simple thing to try is to turn off the rewrite cache.

(set-rw-cache-state nil)

Some system behaviors can be modified using `defattach-system`
— also see system-attachments — typically by modifying
heuristics. You can find all attachments by evaluating

(defun constant-nil-function-arity-2 (x y) (declare (xargs :mode :logic :guard t) (ignore x y)) nil) (defattach-system too-many-ifs-post-rewrite constant-nil-function-arity-2) (defattach-system too-many-ifs-pre-rewrite constant-nil-function-arity-2) (defattach-system quick-and-dirty-srs constant-nil-function-arity-2)

In some cases books may provide more sophisticated uses of `defattach-system` (or `defattach`). For a key example, see `use-trivial-ancestors-check`.

Another way to speed up system functions can be by using memoization. Here is an example from

(memoize 'acl2::sublis-var1 :condition '(and (null acl2::alist) (consp acl2::form) (eq (car acl2::form) 'HIDE)))

See memoized-prover-fns for a convenient way to do such memoization
that automatically clears memoization tables after each event. (Also see
clear-memoize-table and clear-memoize-tables, and see hons-wash for another way to clean up after memoization.) Comments in the
book

The following may be helpful at the level of book certification, and are discussed in :doc certify-book-debug.

(set-serialize-character-system nil) (set-bad-lisp-consp-memoize nil) (set-inhibit-output-lst '(proof-tree event))

Ideas for efficient programming include the use of compilation for host
Lisps (other than CCL and SBCL, which compile automatically); see comp
and set-compile-fns. For logic-mode functions, verify guards if feasible; otherwise consider using program-mode wrappers
(see program-wrapper). Consider writing recursive definitions using
tail recursion when possible. In some cases the use of hash cons,
memoization, or fast alists may reduce computation time dramatically; see
hons-and-memoization. Single-threaded objects (see stobj),
arrays, multiple-value return, and `mbe` are helpful
programming constructs provided by ACL2 for efficient execution. Some
built-in functions are constructed for efficiency; see for example `cons-with-hint` to reduce consing and read-file-into-string for
obtaining the contents of a file quickly.

You might find `type` declarations to be useful. In
particular, if your host Lisp is GCL then the use of the declaration

Of course, if a programming technique or construct is useful for efficient
execution in Common Lisp and it is supported by ACL2, then it is useful for
efficient execution in ACL2. In particular, consider using `type` declarations for numbers in place of `xargs` `guard`.

The use of `make-event` can sometimes reduce computation time; see
for example using-tables-efficiently and defconsts.

You can profile functions to see where time is being spent during proofs or when computing with user-defined functions. Sometimes it is even useful to profile virtually all ACL2 source functions, or even virtually all user-defined functions. That can be done as follows — also see profile-ACL2 and profile-all — but note that when the problem is slow proofs, then since the results will display time spent in various ACL2 prover routines, those results might not be helpful to most users.

(include-book "centaur/memoize/old/profile" :dir :system) (profile-acl2) ; or, (profile-all) to include user-defined functions [[Then run a slow form.]] (memsum) ; shows where time is spent

For computations and proofs that may benefit from parallel computation, you could build the variant ACL2(p) of ACL2. See parallelism.