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