		Search-engine friendly clone of the ACL2 documentation.

Efficiency

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.

Proof efficiency

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, and you prove the rewrite rules (equal (op x y) (op y x)) and (equal (op x (op y z)) (op y (op x z))), then ACL2 will use an n^2 algorithm to put arguments in order, essentially with bubblesort, in a sequence like this:

(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 n*log(n) algorithm. You may consider creating calls of hide to avoid exploring terms that are in the expected form. Calls of hide may be removed when ready either with a suitable :expand hint or by enabling a rewrite rule (equal (hide x) x).

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 (all-attachments (w state)) and all built-in such attachments by evaluating (global-val 'attachments-at-ground-zero (w state)), except for a few exceptions (see defattach). For most of these, however, you will need to consult the ACL2 source files for relevant information. Here are some key examples of how to modify system behavior.

(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 books/projects/stateman/stateman22.lisp.

(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 books/tools/memoize-prover-fns.lisp note a reduction in proof time from 4200 seconds to 49 seconds for one example by memoizing some system functions. Those comments also have some discussion about which system functions to consider memoizing. Perhaps ACL2 users will contribute further documentation on which system functions to memoize for efficiency.

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))

Programming efficiency

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 (signed-byte 64), or any stronger declaration (e.g., (unsigned-byte 63), (signed-byte 12), or (integer 0 100)), can provide dramatic performance improvements in compiled code. You can peruse that code using disassemble$.

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.

Miscellaneous efficiency ideas

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.