		Search-engine friendly clone of the ACL2 documentation.

Memoize

Memoized-prover-fns

Memoize some theorem prover functions

In the community-books, the book tools/memoize-prover-fns.lisp arranges to memoize some functions in the theorem prover. Including this book MAY, in some cases, improve performance; perhaps more likely, including this book may degrade performance! So if you decide to include this book, it would serve you well to experiment by changing the list of prover functions to memoize. To do this you can proceed as follows.

(progn
  (unmemoize-lst (f-get-global 'memoized-prover-fns state))
  (make-event
   (pprogn (f-put-global 'memoized-prover-fns '(... <your_list> ...) state)
           (value '(value-triple nil))))
  (memoize-lst (f-get-global 'memoized-prover-fns state)))

Of course, you can run experiments that compare times for your proofs with different prover functions memoized (or, no prover functions memoized). In addition, as usual with memoization, you can evaluate (memsum) after trying some proofs to see if the functions you have memoized result in good ratios of hits to calls.

Note that this book automatically provides an attachment to finalize-event-user. So it might not work well with other books that provide such an attachment. For this book, the attachment clears the memoization tables after each book not under include-book. (That restriction could easily be lifted, but perhaps it's useful for performance. And perhaps not — feel free to experiment!)

If you find a good set of prover functions to memoize, please consider modifying the f-put-global call in the aforementioned book, tools/memoize-prover-fns.lisp, for your own set of prover functions.