memoize-prover-fns

Included Books

top

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

memoize-lst-fnfunction

(defun memoize-lst-fn
  (lst options acc)
  (declare (xargs :guard (and (true-listp lst) (true-listp acc))))
  (cond ((endp lst) (reverse acc))
    (t (memoize-lst-fn (cdr lst)
        options
        (cons `(memoize ',(CAR LST) ,@OPTIONS) acc)))))

memoize-lstmacro

(defmacro memoize-lst
  (lst &rest options &key (verbose 'nil))
  (declare (ignorable verbose))
  `(make-event (cons 'progn
      (memoize-lst-fn ,LST
        ',(LIST* :VERBOSE VERBOSE (REMOVE-KEYWORD :VERBOSE OPTIONS))
        nil))))

unmemoize-lst-fnfunction

(defun unmemoize-lst-fn
  (lst acc)
  (declare (xargs :guard (and (true-listp lst) (true-listp acc))))
  (cond ((endp lst) (reverse acc))
    (t (unmemoize-lst-fn (cdr lst)
        (cons `(unmemoize ',(CAR LST)) acc)))))

unmemoize-lstmacro

(defmacro unmemoize-lst
  (lst)
  `(make-event (list 'with-output
      :off :all (cons 'progn (unmemoize-lst-fn ,LST nil)))))

clear-memoize-table-lstfunction

(defun clear-memoize-table-lst
  (lst)
  (declare (xargs :guard (true-listp lst)))
  (cond ((endp lst) nil)
    (t (prog2$ (clear-memoize-table (car lst))
        (clear-memoize-table-lst (cdr lst))))))

other

(make-event (pprogn (f-put-global 'memoized-prover-fns
      '(macroexpand1-cmp translate11-lst
        translate11-call
        translate11
        all-fnnames1
        all-vars1
        all-vars1-lst
        ffnnamep-mod-mbe-lst
        remove-guard-holders
        remove-guard-holders-weak
        remove-guard-holders1
        remove-guard-holders1-lst
        normalize
        normalize-lst)
      state)
    (value '(value-triple :memoized-prover-fns-assigned)))
  :check-expansion t)

other

(memoize-lst (f-get-global 'memoized-prover-fns state))

finalize-event-user-memoizefunction

(defun finalize-event-user-memoize
  (ctx body state)
  (declare (xargs :stobjs state)
    (ignore ctx body))
  (cond ((or (global-val 'include-book-path (w state))
       (not (and (f-boundp-global 'memoized-prover-fns state)
           (true-listp (f-get-global 'memoized-prover-fns state))))) state)
    (t (progn$ (clear-memoize-table-lst (f-get-global 'memoized-prover-fns state))
        state))))

other

(defattach (finalize-event-user finalize-event-user-memoize)
  :system-ok t)

other

(defxdoc memoized-prover-fns
  :parents (memoize)
  :short "Memoize some theorem prover functions"
  :long "<p>In the @(see community-books), the book
 @('tools/memoize-prover-fns.lisp') arranges to @(see 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.</p>

 @({
 (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)))
 })

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

 <p>Note that this book automatically provides an attachment to @(tsee
 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 @(tsee include-book).  (That restriction
 could easily be lifted, but perhaps it's useful for performance.  And perhaps
 not &mdash; feel free to experiment!)</p>

 <p>If you find a good set of prover functions to memoize, please consider
 modifying the @(tsee f-put-global) call in the aforementioned book,
 @('tools/memoize-prover-fns.lisp'), for your own set of prover
 functions.</p>")

other

(defpointer memoize-prover-fns memoized-prover-fns)