memoize-raw

(defun mf-multiprocessing
  (flg &optional quiet)
  (cond ((iff *enable-multithreaded-memoization* flg) (when (not quiet)
        (format *standard-output*
          "~%; Note: Multiprocessing is already ~a.~%"
          (if *enable-multithreaded-memoization*
            "on"
            "off"))))
    (t (unwind-protect (setq *enable-multithreaded-memoization* flg)
        (rememoize-all t))))
  flg)

(defun initial-memoize-info-ht
  nil
  (if *enable-multithreaded-memoization*
    (mf-mht :shared :default)
    (mf-mht)))

(defun initial-memoize-call-array
  (n)
  (make-array n :element-type 'mfixnum :initial-element 0))

(defun mf-note-arity
  (fn nargs nvals)
  (mf-sethash fn
    (cons nargs nvals)
    *number-of-arguments-and-values-ht*))

(defun memoize-look-up-def-raw
  (sym quiet-p)
  (let ((temp (get sym 'acl2-saved-def)))
    (cond (temp (cdr temp))
      (t (let* ((fn (symbol-function sym)) (lam (and fn (function-lambda-expression fn))))
          (cond (lam (assert (or (eq (car lam) 'lambda)
                  (eq (car lam) 'named-lambda)))
              lam)
            (quiet-p nil)
            (t (error "Lisp cannot find a definition for ~
                                ~s.~%Consider using ~s or supplying to ~
                                ~%memoize(-fn) an explicit :CL-DEFUN ~
                                argument.~a"
                sym
                'save-def
                ""))))))))

(defun 10-days
  nil
  (let ((n (* *10-days-in-seconds* (ceiling *float-ticks/second*))))
    n))

(defun pons
  (x y ht)
  (declare (hash-table ht))
  (incf-pons-calls)
  (let* ((flex-alist (mf-gethash y ht)) (entry (hl-flex-assoc x flex-alist)))
    (cond (entry)
      (t (incf-pons-misses)
        (let* ((was-alistp (listp flex-alist)) (new-cons (cons x y))
            (new-flex-alist (mf-flex-acons new-cons flex-alist)))
          (when was-alistp (mf-sethash y new-flex-alist ht))
          new-cons)))))

(defun initialize-never-memoize-ht
  nil
  (let ((ht (mf-mht :test 'eq :shared :default)))
    (note-fns-in-file "hons-raw.lisp" ht)
    (note-fns-in-file "memoize-raw.lisp" ht)
    (flet ((update-nmht (fn)
         (when (and (fboundp fn) (not (macro-function fn)))
           (never-memoize-fn fn))))
      (mf-maphash (lambda (key val) (declare (ignore val)) (update-nmht key))
        ht)
      (loop for
        fn
        in
        *common-lisp-symbols-from-main-lisp-package*
        do
        (update-nmht fn))))
  nil)

(defun never-memoize-fn
  (fn)
  (mf-sethash fn t *never-memoize-ht*)
  nil)

(defun never-memoize-p
  (fn)
  (mf-gethash fn *never-memoize-ht*))

(defun outside-caller-col-base
  nil
  (ma-index *initial-max-symbol-to-fixnum*))

(defun memoize-table-desired-size
  (fn min-size)
  (let* ((max-sizes (mf-gethash fn *memo-max-sizes*)))
    (if (not max-sizes)
      min-size
      (let* ((nclears (access memo-max-sizes-entry max-sizes :num-clears)) (avg-mt-size (access memo-max-sizes-entry max-sizes :avg-mt-size))
          (our-guess (ceiling (* 1.2 avg-mt-size)))
          (capped-guess (min our-guess (* nclears 44000)))
          (final-guess (max *mht-default-size* min-size capped-guess)))
        (when (and (< (integer-length (- nclears 1)) (integer-length nclears))
            *memoize-verbose*)
          (format t
            "; ~s memo table: ~s clears, avg size ~s, guess ~s, final ~
                     ~s~%"
            fn
            nclears
            avg-mt-size
            our-guess
            final-guess))
        final-guess))))

(defun pons-table-desired-size
  (fn min-size)
  (let* ((max-sizes (mf-gethash fn *memo-max-sizes*)))
    (if (not max-sizes)
      *mht-default-size*
      (let* ((nclears (access memo-max-sizes-entry max-sizes :num-clears)) (avg-pt-size (access memo-max-sizes-entry max-sizes :avg-pt-size))
          (our-guess (ceiling (* 1.2 avg-pt-size)))
          (capped-guess (min our-guess (* nclears 44000)))
          (final-guess (max *mht-default-size* min-size capped-guess)))
        (when (and (< (integer-length (- nclears 1)) (integer-length nclears))
            *memoize-verbose*)
          (format t
            "; ~s pons table: ~s clears, avg size ~s, guess ~s, final ~
                     ~s~%"
            fn
            nclears
            avg-pt-size
            our-guess
            final-guess))
        final-guess))))

(defun make-initial-memoize-hash-table
  (fn init-size)
  (with-global-memoize-lock (mf-mht :size (memoize-table-desired-size fn init-size))))

(defun make-initial-memoize-pons-table
  (fn init-size)
  (with-global-memoize-lock (mf-mht :size (pons-table-desired-size fn init-size))))

(defun update-memo-max-sizes
  (fn pt-size mt-size)
  (when (or (< 0 mt-size) (< 0 pt-size))
    (with-global-memoize-lock (let ((old (mf-gethash fn *memo-max-sizes*)))
        (if (not old)
          (mf-sethash fn
            (make memo-max-sizes-entry
              :num-clears 1
              :max-pt-size pt-size
              :max-mt-size mt-size
              :avg-pt-size (coerce pt-size 'float)
              :avg-mt-size (coerce mt-size 'float))
            *memo-max-sizes*)
          (let* ((old.num-clears (access memo-max-sizes-entry old :num-clears)) (old.max-pt-size (access memo-max-sizes-entry old :max-pt-size))
              (old.max-mt-size (access memo-max-sizes-entry old :max-mt-size))
              (old.avg-pt-size (access memo-max-sizes-entry old :avg-pt-size))
              (old.avg-mt-size (access memo-max-sizes-entry old :avg-mt-size))
              (new.num-clears (+ 1 old.num-clears)))
            (mf-sethash fn
              (make memo-max-sizes-entry
                :num-clears new.num-clears
                :max-pt-size (max pt-size old.max-pt-size)
                :max-mt-size (max mt-size old.max-mt-size)
                :avg-pt-size (/ (+ pt-size (* old.avg-pt-size old.num-clears))
                  new.num-clears)
                :avg-mt-size (/ (+ mt-size (* old.avg-mt-size old.num-clears))
                  new.num-clears))
              *memo-max-sizes*))))))
  nil)

(defun print-memo-max-sizes
  nil
  (with-global-memoize-lock (when (equal (mf-hash-table-count *memo-max-sizes*) 0)
      (return-from print-memo-max-sizes nil))
    (format t
      "Memo table statistics gathered at each from when they were ~
             cleared:~%~%")
    (let ((indent 8) indent-str)
      (mf-maphash (lambda (fn entry)
          (declare (ignore entry))
          (setq indent (max indent (length (symbol-name fn)))))
        *memo-max-sizes*)
      (setq indent-str (format nil "~a" (+ 2 indent)))
      (format t
        (concatenate 'string "~" indent-str ":@a")
        "Function")
      (format t
        " ~10:@a | ~15:@a ~15:@a | ~15:@a ~15:@a~%"
        "Clears"
        "PT Max"
        "PT Avg"
        "MT Max"
        "MT Avg")
      (mf-maphash (lambda (fn entry)
          (let* ((num-clears (access memo-max-sizes-entry entry :num-clears)) (max-pt-size (access memo-max-sizes-entry entry :max-pt-size))
              (max-mt-size (access memo-max-sizes-entry entry :max-mt-size))
              (avg-pt-size (access memo-max-sizes-entry entry :avg-pt-size))
              (avg-mt-size (access memo-max-sizes-entry entry :avg-mt-size)))
            (format t
              (concatenate 'string
                "~"
                indent-str
                ":@a ~10:D | ~15:D ~15:D | ~15:D ~15:D~%")
              fn
              num-clears
              max-pt-size
              (floor avg-pt-size)
              max-mt-size
              (floor avg-mt-size))))
        *memo-max-sizes*)
      (format t "~%")))
  nil)

(defun memoize-flush1
  (lst)
  (with-global-memoize-lock (loop for
      sym
      in
      lst
      do
      (when (boundp (the symbol sym))
        (let ((old (symbol-value (the symbol sym))))
          (unless (or (null old) (eql 0 (mf-hash-table-count old)))
            (setf (symbol-value (the symbol sym)) nil)))))))

(defun sync-memoize-call-array
  nil
  (with-global-memoize-lock (let ((n1 (ma-index *2max-memoize-fns*)) (n2 (1+ *max-symbol-to-fixnum*)))
      (declare (type (and fixnum mfixnum) n1 n2))
      (setq *memoize-call-array* (initial-memoize-call-array 1))
      (setq *callers-array* (make-array 0))
      (gc$)
      (setq *memoize-call-array* (initial-memoize-call-array n1))
      (setq *callers-array* (make-array n2 :initial-element nil))
      (setq *caller* (outside-caller-col-base)))))

(defun memoize-call-array-grow
  (&optional (2nmax (* 2 (ceiling (* 3/2 (/ *2max-memoize-fns* 2))))))
  (with-global-memoize-lock (unless (integerp 2nmax)
      (error "(memoize-call-array-grow ~s).  Arg must be an integer."
        2nmax))
    (unless (evenp 2nmax)
      (error "(memoize-call-array-grow ~s).  Arg must be even."
        2nmax))
    (unless (> 2nmax 100)
      (error "(memoize-call-array-grow ~s).  Arg must be > 100."
        2nmax))
    (when (<= 2nmax *2max-memoize-fns*)
      (cw "; memoize-call-array-grow: *memoize-call-array* already big enough.~%")
      (return-from memoize-call-array-grow))
    (unless (<= (* 2nmax 2nmax) most-positive-mfixnum)
      (error "memoize-call-array-grow:  most-positive-mfixnum exceeded.  Too ~
             many memoized functions."))
    (unless (<= (* 2nmax 2nmax) most-positive-fixnum)
      (error "memoize-call-array-grow:  most-positive-fixnum exceeded.  Too ~
             many memoized functions."))
    (unless (< (* 2nmax 2nmax) array-total-size-limit)
      (error "memoize-call-array-grow: ARRAY-TOTAL-SIZE-LIMIT exceeded.  Too ~
             many memoized functions."))
    (unless (< (* 2nmax 2nmax) array-dimension-limit)
      (error "memoize-call-array-grow: ARRAY-DIMENSION-LIMIT exceeded.  Too ~
             many memoized functions."))
    (unless (eql *caller* (outside-caller-col-base))
      (cerror "Continue at your own risk."
        "MEMOIZE-CALL-ARRAY-GROW was called while a memoized function~%~
              was executing, so all bets are off.  Continue only at your own~%~
              risk.  That risk may be low, but at the least, memoization~%~
              reports (in particular, from memsum) will probably be~%~
              inaccurate."))
    (setq *2max-memoize-fns* 2nmax)
    (let ((state *the-live-state*))
      (observation 'memoize-call-array-grow
        "Now reinitializing memoization structures.  This will ~
                   erase saved values and statistics."))
    (sync-memoize-call-array)
    (rememoize-all))
  nil)

(defun memoize-use-attachment-warning
  (fn at-fn)
  (when *memoize-use-attachment-warning-p*
    (let ((state *the-live-state*))
      (warning$ 'top-level
        "Attachment"
        "Although the function ~x0 is memoized, a result is not being ~
                 stored because ~@1.  Warnings such as this one, about not ~
                 storing results, will remain off for all functions for the ~
                 remainder of the session unless the variable ~x2 is set to a ~
                 non-nil value in raw Lisp."
        fn
        (mv-let (lookup-p at-fn)
          (if (consp at-fn)
            (assert$ (eq (car at-fn) :lookup) (mv t (cdr at-fn)))
            (mv nil at-fn))
          (cond (lookup-p (msg "a stored result was used from a call of ~
                                     memoized function ~x0, which may have ~
                                     been computed using attachments"
                at-fn))
            ((eq at-fn :|{APPLY$-OR-BADGE}-USERFN|) (msg "one of the functions ~v0, which depend ~
                                     on warrants for the result, was called ~
                                     during evaluation of a call of ~x1"
                '(apply$-userfn badge-userfn)
                fn))
            (t (msg "an attachment to function ~x0 was used ~
                                     during evaluation of one of its calls"
                at-fn))))
        '*memoize-use-attachment-warning-p*))
    (setq *memoize-use-attachment-warning-p* nil)))

(defun memoize-look-up-def
  (fn cl-defun inline wrld &key quiet-p)
  (cond ((eq cl-defun :default) (cond ((null inline) nil)
        ((not (fboundp fn)) (error "MEMOIZE-LOOK-UP-DEF: ** ~a is undefined." fn))
        ((let ((def (cltl-def-from-name fn wrld)))
           (cond (def (assert (eq (car def) 'defun)) (cdr def)))))
        (t (memoize-look-up-def-raw fn quiet-p))))
    ((eq (car cl-defun) 'defun) (cdr cl-defun))
    (t cl-defun)))

(defun memoize-fn-init
  (fn inline wrld &aux (state *the-live-state*))
  (with-global-memoize-lock (unless (symbolp fn)
      (error "Memoize-fn: ~s is not a symbol." fn))
    (maybe-untrace! fn)
    (unless *memoize-init-done*
      (error "Memoize-fn:  *MEMOIZE-INIT-DONE* is still nil."))
    (unless (fboundp fn)
      (error "Memoize-fn: ~s is not fboundp." fn))
    (when (or (macro-function fn)
        (special-operator-p fn)
        (and (fboundp 'compiler-macro-function)
          (compiler-macro-function fn)))
      (error "Memoize-fn: ~s is a macro or a special operator or has a ~
             compiler macro."
        fn))
    (when (never-memoize-p fn)
      (error "Memoize-fn: ~s must never be memoized" fn))
    (when (and inline
        (or (member-eq fn (f-get-global 'logic-fns-with-raw-code state))
          (member-eq fn
            (f-get-global 'program-fns-with-raw-code state))))
      (error "Memoize-fn: ~s must never be memoized with :inline t,~%~
             because it belongs to the list stored in state global~%~
             variable ~s and thus runs code different~%~
             than that stored in the ACL2 logical world, as is typically~%~
             used when inserting inlined code for memoization."
        fn
        (if (member-eq fn (f-get-global 'logic-fns-with-raw-code state))
          'logic-fns-with-raw-code
          'program-fns-with-raw-code)))
    (when (memoizedp-raw fn)
      (observation 'memoize
        "~s0 is currently memoized. We will first unmemoize it, ~
                   then memoize it again."
        fn)
      (unmemoize-fn fn))
    (when (member fn (eval '(trace)))
      (observation 'memoize
        "Untracing ~s before memoizing it."
        fn)
      (eval `(untrace ,FN)))
    (when (and (fboundp 'old-trace) (member fn (eval '(old-trace))))
      (observation 'memoize
        "Old-untracing ~s before memoizing it."
        fn)
      (eval `(old-untrace ,FN)))
    (when (getpropc fn 'constrainedp nil wrld)
      (error "Memoize-fn: ~s is constrained; you may instead wish to memoize a ~
             caller or to memoize its attachment (see :DOC defattach)."
        fn))))

(defun memoize-fn-init-2
  (fn formals condition stobjs-in stobjs-out)
  (unless (and (symbol-listp formals)
      (no-duplicatesp formals)
      (loop for
        x
        in
        formals
        never
        (constantp x)))
    (error "Memoize-fn: FORMALS, ~a, must be a true list of distinct, ~
            nonconstant symbols."
      formals))
  (when (intersection lambda-list-keywords formals)
    (error "Memoize-fn: FORMALS, ~a, may not intersect LAMBDA-LIST-KEYWORDS."
      formals))
  (when (and condition
      (or (member 'state stobjs-in) (member 'state stobjs-out)))
    (error "Memoize-fn:  ~s uses STATE." fn)))

(defun memoize-fn-inner-body
  (fn condition
    body
    fn-col-base
    tablename
    localtablename
    ponstablename
    localponstablename
    memo-table-init-size
    formals
    specials
    stobjs-out
    number-of-args
    commutative
    aokp
    prog1-fn)
  (let ((mf-record-mht (and *record-mht-calls*
         `((safe-incf (aref ,*MF-MA*
              ,(MA-INDEX-FROM-COL-BASE FN-COL-BASE *MA-MHT-INDEX*))
            1)))) (mf-record-hit (and *record-hits*
          condition
          `((safe-incf (aref ,*MF-MA*
               ,(MA-INDEX-FROM-COL-BASE FN-COL-BASE *MA-HITS-INDEX*))
             1)))))
    `(cond ,@(AND (NOT (MEMBER-EQUAL CONDITION '('T T)))
       `(((NOT ,CONDITION) ,@(AND *CONDITION-NIL-AS-HIT* MF-RECORD-HIT) ,BODY)))
      ,@(AND CONDITION
       `((T
          (LET (,*MF-ANS* ,*MF-ARGS* ,*MF-ANS-P*)
            (DECLARE (IGNORABLE ,*MF-ANS* ,*MF-ARGS* ,*MF-ANS-P*))
            (WHEN (NULL ,TABLENAME)
              ,@MF-RECORD-MHT
              (SETQ ,TABLENAME
                      (MAKE-INITIAL-MEMOIZE-HASH-TABLE ',FN
                                                       ,MEMO-TABLE-INIT-SIZE)))
            (SETQ ,LOCALTABLENAME ,TABLENAME)
            ,@(AND (> NUMBER-OF-ARGS 1)
                   `((WHEN (NULL ,PONSTABLENAME)
                       (SETQ ,PONSTABLENAME
                               (MAKE-INITIAL-MEMOIZE-PONS-TABLE ',FN
                                                                ,MEMO-TABLE-INIT-SIZE)))
                     (SETQ ,LOCALPONSTABLENAME ,PONSTABLENAME)))
            (SETQ ,*MF-ARGS*
                    ,(COND
                      (COMMUTATIVE
                       `(COND
                         ((MIS-ORDERED-COMMUTATIVE-ARGS ,(CAR FORMALS)
                                                        ,(CADR FORMALS))
                          (PIST* ,LOCALPONSTABLENAME ,(CADR FORMALS)
                                 ,(CAR FORMALS) ,@SPECIALS))
                         (T
                          (PIST* ,LOCALPONSTABLENAME ,(CAR FORMALS)
                                 ,(CADR FORMALS) ,@SPECIALS))))
                      (T `(PIST* ,LOCALPONSTABLENAME ,@FORMALS ,@SPECIALS))))
            (MULTIPLE-VALUE-SETQ (,*MF-ANS* ,*MF-ANS-P*)
              ,(LET ((GETHASH-FORM `(MF-GETHASH ,*MF-ARGS* ,LOCALTABLENAME)))
                 (COND
                  (AOKP `(COND (*AOKP* ,GETHASH-FORM) (T (VALUES NIL NIL))))
                  (T GETHASH-FORM))))
            (COND
             (,*MF-ANS-P*
              ,@(AND AOKP `((UPDATE-ATTACHED-FN-CALLED ',(CONS :LOOKUP FN))))
              ,@MF-RECORD-HIT
              ,@(COND ((NULL (CDR STOBJS-OUT)) `(,*MF-ANS*))
                      (T
                       (LET ((LEN-1 (1- (LENGTH STOBJS-OUT))))
                         `(,(CONS 'MV
                                  (NCONC
                                   (LOOP FOR I FIXNUM BELOW LEN-1
                                         COLLECT `(POP ,*MF-ANS*))
                                   (LIST *MF-ANS*))))))))
             (T
              ,(LET* ((VARS
                       (LOOP FOR I FIXNUM BELOW (IF (CDR STOBJS-OUT)
                                                    (LENGTH STOBJS-OUT)
                                                    1)
                             COLLECT (MF-MAKE-SYMBOL "O~a" I))))
                 (COND
                  (AOKP
                   `(MV?-LET ,VARS ,BODY
                             (PROGN
                              (MF-SETHASH ,*MF-ARGS* (LIST* ,@VARS)
                                          ,LOCALTABLENAME)
                              (MV? ,@VARS))))
                  (T
                   `(LET (,*ATTACHED-FN-TEMP*)
                      (MV?-LET ,VARS
                               (LET ((*AOKP* (AND *AOKP* T))
                                     (SAVED-WARRANT-REQS *WARRANT-REQS*))
                                 (WHEN (CONSP SAVED-WARRANT-REQS)
                                   (SETQ *WARRANT-REQS*
                                           (AND SAVED-WARRANT-REQS T)))
                                 (,PROG1-FN ,BODY
                                  (COND
                                   ((NOT (MEMBER *AOKP* '(T NIL) :TEST #'EQ))
                                    (SETQ ,*ATTACHED-FN-TEMP* *AOKP*))
                                   ((CONSP *WARRANT-REQS*)
                                    (SETQ ,*ATTACHED-FN-TEMP*
                                            :{APPLY$-OR-BADGE}-USERFN)
                                    (WHEN (CONSP SAVED-WARRANT-REQS)
                                      (SETQ *WARRANT-REQS*
                                              (UNION-EQ *WARRANT-REQS*
                                                        SAVED-WARRANT-REQS))))
                                   ((EQ SAVED-WARRANT-REQS T)
                                    (SETQ *WARRANT-REQS* T)))))
                               (PROGN
                                (COND
                                 (,*ATTACHED-FN-TEMP*
                                  (MEMOIZE-USE-ATTACHMENT-WARNING ',FN
                                                                  ,*ATTACHED-FN-TEMP*))
                                 (T
                                  (MF-SETHASH ,*MF-ARGS* (LIST* ,@VARS)
                                              ,LOCALTABLENAME)))
                                (WHEN ,*ATTACHED-FN-TEMP*
                                  (ASSERT
                                   (OR *AOKP*
                                       (EQ ,*ATTACHED-FN-TEMP*
                                           :{APPLY$-OR-BADGE}-USERFN)))
                                  (UPDATE-ATTACHED-FN-CALLED
                                   ,*ATTACHED-FN-TEMP*))
                                (MV? ,@VARS))))))))))))))))

(defun memoize-fn-outer-body
  (inner-body fn fn-col-base start-ticks forget prog1-fn)
  `(let (,@(AND *RECORD-BYTES* `((,*MF-START-BYTES* (HEAP-BYTES-ALLOCATED)))) ,@(AND *RECORD-PONS-CALLS* `((,*MF-START-PONS* *PONS-CALL-COUNTER*)))
      (,START-TICKS ,(IF *RECORD-TIME*
     '(INTERNAL-REAL-TICKS)
     '0)))
    (declare (ignorable ,@(AND *RECORD-BYTES* `(,*MF-START-BYTES*))
        ,@(AND *RECORD-PONS-CALLS* `(,*MF-START-PONS*)))
      (type mfixnum
        ,START-TICKS
        ,@(AND *RECORD-PONS-CALLS* `(,*MF-START-PONS*))
        ,@(AND *RECORD-BYTES* `(,*MF-START-BYTES*))))
    (,(COND
  ((OR *RECORD-PONS-CALLS* *RECORD-BYTES* *RECORD-TIME* FORGET)
   (IF (F-GET-GLOBAL 'PROTECT-MEMOIZE-STATISTICS *THE-LIVE-STATE*)
       'UNWIND-PROTECT-DISABLE-INTERRUPTS-DURING-CLEANUP
       PROG1-FN))
  (T 'PROGN)) ,(COND
  ((OR *RECORD-BYTES* *RECORD-CALLS* *RECORD-HITS* *RECORD-MHT-CALLS*
       *RECORD-PONS-CALLS* *RECORD-TIME*)
   `(LET ((*CALLER* ,FN-COL-BASE))
      ,INNER-BODY))
  (T INNER-BODY))
      ,@(AND *RECORD-PONS-CALLS*
       `((SAFE-INCF
          (AREF ,*MF-MA* ,(MA-INDEX-FROM-COL-BASE FN-COL-BASE *MA-PONS-INDEX*))
          (THE-MFIXNUM (- *PONS-CALL-COUNTER* ,*MF-START-PONS*)))))
      ,@(AND *RECORD-BYTES*
       `((SAFE-INCF
          (AREF ,*MF-MA*
                ,(MA-INDEX-FROM-COL-BASE FN-COL-BASE *MA-BYTES-INDEX*))
          (THE-MFIXNUM (- (HEAP-BYTES-ALLOCATED) ,*MF-START-BYTES*)))))
      ,@(AND *RECORD-TIME*
       `((SAFE-INCF
          (THE MFIXNUM (AREF ,*MF-MA* (THE-MFIXNUM (1+ ,*MF-COUNT-LOC*))))
          (THE-MFIXNUM
           (FIX-TICKS (THE-MFIXNUM (- (INTERNAL-REAL-TICKS) ,START-TICKS))
                      ',FN)))))
      ,@(AND FORGET `((CLEAR-MEMOIZE-TABLE ',FN))))))

(defun memoize-fn-def
  (inner-body outer-body
    fn
    formals
    specials
    dcls
    fnn
    start-ticks
    localtablename
    localponstablename)
  `(defun ,FN
    ,FORMALS
    ,@DCLS
    (declare (ignorable ,@FORMALS ,@SPECIALS))
    (with-global-memoize-lock-static (let* ((,*MF-COUNT-LOC* ,(IF (OR *RECORD-CALLS* *RECORD-TIME*)
     `(THE-MFIXNUM (+ *CALLER* ,(* 2 FNN)))
     0)) (,*MF-MA* *memoize-call-array*)
          ,LOCALTABLENAME
          ,LOCALPONSTABLENAME)
        (declare (type mfixnum ,*MF-COUNT-LOC*)
          (ignorable ,*MF-COUNT-LOC*
            ,*MF-MA*
            ,LOCALPONSTABLENAME
            ,LOCALTABLENAME)
          (type (simple-array mfixnum (*)) ,*MF-MA*))
        ,@(AND *RECORD-CALLS* `((SAFE-INCF (AREF ,*MF-MA* ,*MF-COUNT-LOC*) 1)))
        (if (eql -1 ,START-TICKS)
          ,OUTER-BODY
          ,INNER-BODY)))))

(defun memoize-fn-formals
  (fn wrld inline &key (cl-defun :default cl-defun-p))
  (let ((formals (getpropc fn 'formals t wrld)))
    (if (eq formals t)
      (let ((cl-defun (if cl-defun-p
             cl-defun
             (memoize-look-up-def fn cl-defun inline wrld :quiet-p t))))
        (if (consp cl-defun)
          (cadr cl-defun)
          (let ((n (mf-len-inputs fn)))
            (if n
              (loop for
                i
                fixnum
                below
                n
                collect
                (mf-make-symbol "X~a" i))
              t))))
      formals)))

(defun cltl-def-memoize-invoke
  (fn-def old-fn invoke)
  (let ((gsym (gensym)) (fn (car fn-def))
      (formals (cadr fn-def))
      (decls (butlast (cddr fn-def) 1)))
    (eval `(defvar ,GSYM nil))
    `(,FN ,FORMALS
      ,@DECLS
      (if ,GSYM
        (funcall ,OLD-FN ,@FORMALS)
        (let ((,GSYM t))
          (,INVOKE ,@FORMALS))))))

(defun memoize-fn
  (fn &key
    (condition t)
    (inline t)
    (cl-defun :default)
    (formals :default)
    (stobjs-in :default)
    (specials nil)
    (commutative nil)
    (stobjs-out :default)
    (forget nil)
    (memo-table-init-size *mht-default-size*)
    (aokp nil)
    (invoke nil)
    &aux
    (wrld (w *the-live-state*))
    (memoize-fn-signature-error "Memoize-fn: could not determine a signature for ~a.~%~
  To assert the signature of ~:*~a, use (mf-note-arity '~:*~a nargs nvals),~%~
  for example, (mf-note-arity '~:*~a 3 1).)  If there are stobjs arguments~%~
  then do not use that mechanism; instead, pass suitable arguments to~%~
  memoize-fn."))
  "The documentation for MEMOIZE-FN is very incomplete.  One may invoke
  (MEMOIZE-FN fn) on the name of a Common Lisp function FN from outside the
  ACL2 loop to get results of possible interest in terms of memoization
  activity and profiling information.  MEMOIZE-FN already has a dozen
  parameters.

  MEMOIZE-FN replaces the SYMBOL-FUNCTION for the symbol FN with 'enhanced'
  raw Common Lisp code that, supposedly, does not affect the value returned by
  FN but may make some notes and may even obtain some return values by
  remembering them from a previous call.

  If the CONDITION parameter is not NIL or 'NIL, then whenever FN is called,
  and there is not as yet any value remembered for a call of FN on the given
  arguments, then if the evaluation of the CONDITION parameter (where the
  formals of FN are bound to its actuals) is not NIL or 'NIL, the values that
  are computed for FN on the given arguments will be saved under the given
  arguments.

  If the INLINE parameter is T, then when MEMOIZE-FN creates a new body for FN,
  we place the old body of FN within the new body, i.e., 'in line'.  However,
  if the INLINE parameter is NIL, then we place code that calls the existing
  SYMBOL-FUNCTION for FN within the new body.  One might well argue that our
  parity for the INLINE parameter to MEMOIZE-fn is backwards, but we don't
  think so.

  One may lie to MEMOIZE-FN to force the memoization of a function that has
  ACL2's state as an explicit parameter by using fraudulent FORMALS, STOBJS-IN,
  and STOBJS-OUT parameters to MEMOIZE-FN.

  If the COMMUTATIVE parameter is not NIL, then the two arguments may be
  swapped before further processing.  We hope/presume that ACL2 will have been
  used first to prove that commutativity.

  If the CL-DEFUN parameter is not NIL, we pretend that the current body of FN
  is that parameter, and similarly for FORMALS, STOBJS-IN, and STOBJS-OUT.

  If FN is a raw Common Lisp function and not an ACL2-approved function, it may
  make reference to a variable, say S, that has a SPECIAL binding, in which
  case one needs to consider what in the world the meaning is for memoizing
  such a function at all.  If S is a member of the SPECIALS parameter, then it
  is assumed that FN does not alter but only refers to S.  MEMOIZE-FN acts as
  though FN had S as an extra argument for purposes of memoization.

  If the FORGET parameter is not NIL, the pons and memo tables of FN are
  discarded at the end of every outermost call of FN."
  (when (equal condition *nil*) (setq condition nil))
  (with-global-memoize-lock (with-warnings-suppressed (memoize-fn-init fn inline wrld)
      (let* ((cl-defun0 (memoize-look-up-def fn cl-defun inline wrld)) (old-fn (symbol-function fn))
          (cl-defun (if invoke
              (cltl-def-memoize-invoke cl-defun0 old-fn invoke)
              cl-defun0))
          (formals (cond ((eq formals :default) (let ((formals (memoize-fn-formals fn wrld inline :cl-defun cl-defun)))
                  (if (eq formals t)
                    (error memoize-fn-signature-error fn)
                    formals)))
              (t formals)))
          (stobjs-in (if (eq stobjs-in :default)
              (let ((s (getpropc fn 'stobjs-in t wrld)))
                (if (eq s t)
                  (make-list (len formals))
                  s))
              stobjs-in))
          (stobjs-out (if (eq stobjs-out :default)
              (let ((s (getpropc fn 'stobjs-out t wrld)))
                (if (eq s t)
                  (let ((n (mf-len-outputs fn)))
                    (cond (n (make-list n))
                      ((null condition) (list nil))
                      (t (error memoize-fn-signature-error fn))))
                  s))
              stobjs-out)))
        (memoize-fn-init-2 fn
          formals
          condition
          stobjs-in
          stobjs-out)
        (mf-sethash fn
          (cons (length stobjs-in) (length stobjs-out))
          *number-of-arguments-and-values-ht*)
        (let* ((fnn (symbol-to-fixnum-create fn)) (fn-col-base (ma-index fnn))
            (body (progn (assert old-fn)
                (cond (invoke (car (last cl-defun)))
                  (inline (assert (consp cl-defun)) (car (last cl-defun)))
                  (t `(funcall ,OLD-FN ,@FORMALS)))))
            (dcls (mf-dcls (cddr (butlast cl-defun))))
            (start-ticks (let ((v (hons-gentemp (memoize-fn-suffix "START-TICKS-" fn))))
                (eval `(prog1 (defparameter ,V -1) (declaim (type mfixnum ,V))))))
            (tablename (eval `(defg ,(HONS-GENTEMP (MEMOIZE-FN-SUFFIX "MEMOIZE-HT-FOR-" FN))
                  nil)))
            (ponstablename (eval `(defg ,(HONS-GENTEMP (MEMOIZE-FN-SUFFIX "PONS-HT-FOR-" FN))
                  nil)))
            (localtablename (make-symbol "TABLENAME"))
            (localponstablename (make-symbol "PONSTABLENAME"))
            (sts (and condition
                (remove-duplicates-eq (loop for
                    st
                    in
                    (union stobjs-in stobjs-out)
                    when
                    (and st (not (eq st :df)))
                    collect
                    (assert$ (not (eq st 'state))
                      (st-lst (congruent-stobj-rep (or (concrete-stobj st wrld) st) wrld)))))))
            (number-of-args (+ (len formals) (len specials)))
            (prog1-fn (if (cdr stobjs-out)
                'multiple-value-prog1
                'prog1))
            (inner-body (memoize-fn-inner-body fn
                condition
                body
                fn-col-base
                tablename
                localtablename
                ponstablename
                localponstablename
                memo-table-init-size
                formals
                specials
                stobjs-out
                number-of-args
                commutative
                aokp
                prog1-fn))
            (outer-body (memoize-fn-outer-body inner-body
                fn
                fn-col-base
                start-ticks
                forget
                prog1-fn))
            (def (memoize-fn-def inner-body
                outer-body
                fn
                formals
                specials
                dcls
                fnn
                start-ticks
                localtablename
                localponstablename))
            (success nil))
          (unwind-protect (progn (let ((ma *memoize-call-array*))
                (declare (type (simple-array mfixnum (*)) ma))
                (loop for
                  i
                  of-type
                  mfixnum
                  from
                  fn-col-base
                  below
                  (ma-index-from-col-base fn-col-base *2max-memoize-fns*)
                  unless
                  (eql (aref ma i) 0)
                  do
                  (setf (aref ma i) 0)))
              (memoize-eval-compile def old-fn)
              (mf-sethash fn
                (make memoize-info-ht-entry
                  :ext-anc-attachments (and aokp (ext-ancestors-attachments fn wrld))
                  :start-ticks start-ticks
                  :num fnn
                  :tablename tablename
                  :ponstablename ponstablename
                  :condition condition
                  :inline inline
                  :memoized-fn (symbol-function fn)
                  :old-fn old-fn
                  :fn fn
                  :sts sts
                  :cl-defun cl-defun
                  :formals formals
                  :commutative commutative
                  :specials specials
                  :stobjs-in stobjs-in
                  :stobjs-out stobjs-out
                  :record-bytes *record-bytes*
                  :record-calls *record-calls*
                  :record-hits *record-hits*
                  :record-mht-calls *record-mht-calls*
                  :record-pons-calls *record-pons-calls*
                  :record-time *record-time*
                  :forget forget
                  :memo-table-init-size memo-table-init-size
                  :aokp aokp
                  :invoke invoke)
                *memoize-info-ht*)
              (mf-sethash fnn fn *memoize-info-ht*)
              (and condition
                (loop for
                  s
                  in
                  sts
                  do
                  (push tablename (symbol-value (the symbol s)))))
              (setq success t))
            (unless success
              (without-interrupts (setf (symbol-function fn) old-fn)
                (remhash fn *memoize-info-ht*)
                (remhash fnn *memoize-info-ht*)
                (and condition
                  (loop for
                    s
                    in
                    sts
                    when
                    (eq tablename (car (symbol-value (the symbol s))))
                    do
                    (pop (symbol-value (the symbol s)))))
                (setq fn nil)
                (error "Memoize-fn:  Failed to memoize ~s." fn))))))))
  fn)

(defun profile-fn
  (fn &rest
    r
    &key
    (condition nil)
    (inline nil)
    &allow-other-keys)
  (apply (function memoize-fn)
    fn
    :condition condition
    :inline inline
    r))

(defun mf-shorten
  (x n)
  (cond ((and (stringp x) (<= (length x) n)) x)
    (t (let ((x (if (stringp x)
             (hons-copy x)
             x)))
        (cond ((mf-gethash x *mf-shorten-ht*))
          (t (let ((*print-pretty* nil) (*print-length* 10)
                (*print-level* 5)
                (*print-lines* 2))
              (let ((str (with-output-to-string (s)
                     (cond ((stringp x) (princ x s)) (t (prin1 x s))))))
                (mf-sethash x
                  (cond ((<= (length str) n) str)
                    (t (concatenate 'string (subseq str 0 (max 0 n)) "///")))
                  *mf-shorten-ht*)))))))))

(defun memoized-values
  (&optional (fn (memoized-functions)))
  (with-global-memoize-lock (cond ((listp fn) (mapc (function memoized-values) fn))
      ((not (memoizedp-raw fn)) (format t "~%; Memoized-values:  ~s is not memoized." fn))
      (t (let ((tb (symbol-value (access memoize-info-ht-entry
                 (mf-gethash fn *memoize-info-ht*)
                 :tablename))))
          (cond ((and tb (not (eql 0 (mf-hash-table-count tb)))) (format t "~%; Memoized values for ~s." fn)
              (mf-maphash (lambda (key v) (format t "~%~s~%=>~%~s" key v))
                tb)))))))
  (force-output *standard-output*)
  nil)

(defun print-call-stack
  nil
  (float-ticks/second-init)
  (our-syntax (let (lst (ticks (internal-real-ticks)) (*print-case* :downcase))
      (with-global-memoize-lock (mf-maphash (lambda (k v)
            (when (symbolp k)
              (let ((x (symbol-value (the symbol (access memoize-info-ht-entry v :start-ticks)))))
                (declare (type mfixnum x))
                (when (> x 0) (push (cons k x) lst)))))
          *memoize-info-ht*))
      (setq lst (sort lst (function <) :key (function cdr)))
      (setq lst
        (loop for
          pair
          in
          lst
          collect
          (list (car pair)
            (mf-num-to-string (/ (the-mfixnum (- ticks (cdr pair))) *float-ticks/second*)))))
      (when lst
        (terpri *standard-output*)
        (mf-print-alist (cons '("Stack of monitored function calls." "Time since outermost call.")
            lst)
          5))))
  (force-output *standard-output*)
  nil)

(defun char-list-fraction
  (l)
  (if (atom l)
    0
    (+ (char-code (car l)) (/ (char-list-fraction (cdr l)) 256))))

(defun symbol-name-order
  (s)
  (unless (symbolp s) (setq s (fixnum-to-symbol s)))
  (- (char-list-fraction (coerce (symbol-name s) 'list))))

(defun compute-calls-and-times
  nil
  (with-global-memoize-lock (let ((ma *memoize-call-array*) (2m *2max-memoize-fns*)
        (ca *callers-array*)
        (n (the fixnum (1+ *max-symbol-to-fixnum*))))
      (declare (type (simple-array mfixnum (*)) ma)
        (type (simple-array t (*)) ca)
        (type fixnum 2m n))
      (cond ((eql (length ca) n) (loop for
            i
            fixnum
            below
            n
            do
            (setf (aref ca i) nil)))
        (t (setq *callers-array* (make-array n :initial-element nil))
          (setq ca *callers-array*)))
      (loop for
        i
        fixnum
        below
        (ma-index-calls n 0 2m)
        do
        (setf (aref ma i) 0))
      (loop for
        i
        fixnum
        from
        *initial-max-symbol-to-fixnum*
        to
        *max-symbol-to-fixnum*
        do
        (let ((col-base (ma-index i 0 2m)))
          (declare (type mfixnum col-base))
          (loop for
            j
            fixnum
            from
            *initial-max-symbol-to-fixnum*
            to
            *max-symbol-to-fixnum*
            do
            (let* ((calls-row (ma-index-calls j)) (index (ma-index-from-col-base col-base calls-row))
                (calls (the-mfixnum (aref ma index))))
              (declare (type mfixnum calls-row index calls))
              (when (> calls 0)
                (let* ((ticks-index (the-mfixnum (1+ index))) (ticks (aref ma ticks-index))
                    (ticks-row (the-mfixnum (1+ calls-row))))
                  (declare (type mfixnum ticks-index ticks ticks-row))
                  (safe-incf (aref ma calls-row)
                    calls
                    compute-calls-and-times)
                  (safe-incf (aref ma ticks-row)
                    ticks
                    compute-calls-and-times)
                  (push i (aref ca j)))))))))))

(defun clear-one-memo-and-pons-hash
  (l strategy)
  (with-global-memoize-lock (let* ((fn (access memoize-info-ht-entry l :fn)) (mt (symbol-value (access memoize-info-ht-entry l :tablename)))
        (pt (symbol-value (access memoize-info-ht-entry l :ponstablename)))
        (mt-count (and mt (mf-hash-table-count mt)))
        (pt-count (and pt (mf-hash-table-count pt))))
      (when mt
        (let* ((mt-target-size (memoize-table-desired-size fn 0)))
          (if (or (eq strategy :clear)
              (and (eq strategy :auto) (< mt-count mt-target-size)))
            (unless (eql 0 mt-count) (clrhash mt))
            (setf (symbol-value (access memoize-info-ht-entry l :tablename))
              nil))))
      (when pt
        (let* ((pt-target-size (pons-table-desired-size fn 0)))
          (if (or (eq strategy :clear)
              (and (eq strategy :auto) (< pt-count pt-target-size)))
            (unless (eql 0 pt-count) (clrhash pt))
            (setf (symbol-value (access memoize-info-ht-entry l :ponstablename))
              nil))))
      (when (or mt-count pt-count)
        (update-memo-max-sizes fn (or pt-count 1) (or mt-count 1)))))
  nil)

(defun clear-memoize-call-array
  nil
  (with-global-memoize-lock (let ((ma *memoize-call-array*))
      (declare (type (simple-array mfixnum (*)) ma))
      (let ((len (length ma)))
        (cond ((typep len 'fixnum) (loop for
              i
              fixnum
              below
              len
              do
              (setf (aref ma i) 0)))
          (t (loop for
              i
              of-type
              integer
              below
              len
              do
              (setf (aref ma i) 0))))))))

(defun clear-memoize-statistics
  nil
  (with-global-memoize-lock (setq *pons-call-counter* 0)
    (setq *pons-misses-counter* 0)
    (clear-memoize-call-array))
  nil)

(defun acl2h-init-memoizations
  nil
  (loop for
    entry
    in
    *thread-unsafe-builtin-memoizations*
    when
    (not (memoizedp-raw (car entry)))
    do
    (with-lower-overhead (apply 'memoize-fn entry))))

(defun set-bad-lisp-consp-memoize
  (arg)
  (cond (arg (when (not (memoizedp-raw 'bad-lisp-consp))
        (with-lower-overhead (apply 'memoize-fn *bad-lisp-consp-memoization*))))
    (t (when (memoizedp-raw 'bad-lisp-consp)
        (unmemoize-fn 'bad-lisp-consp)))))

(defun memstat (&rest r) (apply (function memoized-values) r))

(defun clear-memo-tables nil (clear-memoize-tables))

(defun lower-overhead
  nil
  (setq *record-bytes* nil)
  (setq *record-calls* nil)
  (setq *record-hits* nil)
  (setq *record-mht-calls* nil)
  (setq *record-pons-calls* nil)
  (setq *record-time* nil))

(defun update-memo-entry-for-attachments
  (fns entry special-name wrld)
  (let* ((ext-anc-attachments (access memoize-info-ht-entry entry :ext-anc-attachments)) (valid-p (if (eq fns :clear)
          :clear (or (null ext-anc-attachments)
            (ext-anc-attachments-valid-p fns
              ext-anc-attachments
              special-name
              wrld
              t)))))
    (cond ((eq valid-p t) (mv nil entry))
      (t (mv (if (eq valid-p nil)
            t
            valid-p)
          (change memoize-info-ht-entry
            entry
            :ext-anc-attachments (ext-ancestors-attachments (access memoize-info-ht-entry entry :fn)
              wrld)))))))

(defun update-memo-entries-for-attachments
  (fns wrld state)
  (let ((ctx 'top-level) (fns (if (eq fns :clear)
          :clear (strict-merge-sort-symbol< (loop for
              fn
              in
              fns
              collect
              (canonical-sibling fn wrld)))))
      (special-name *special-cltl-cmd-attachment-mark-name*))
    (when (eq fns :clear)
      (observation ctx
        "Memoization tables for functions memoized with :AOKP T ~
                    are being cleared."))
    (when fns
      (with-global-memoize-lock (mf-maphash (lambda (k entry)
            (when (symbolp k)
              (mv-let (changedp new-entry)
                (update-memo-entry-for-attachments fns
                  entry
                  special-name
                  wrld)
                (when changedp
                  (when (not (or (eq changedp t) (eq fns :clear)))
                    (observation ctx
                      "Memoization table for function ~x0 is ~
                                      being cleared because ~@1."
                      k
                      (if (eq changedp special-name)
                        "it depends on apply$-userfn or ~
                                          badge-userfn and at least one badge ~
                                          has changed"
                        (msg "the attachment to function ~x0 ~
                                             has changed"
                          changedp)))
                    (clear-one-memo-and-pons-hash entry :auto))
                  (mf-sethash k new-entry *memoize-info-ht*)))))
          *memoize-info-ht*))))
  (clear-memoize-table 'canonical-ancestors-rec)
  (clear-memoize-table 'immediate-canonical-ancestors)
  (clear-memoize-table 'canonical-ancestors-tr-rec)
  (clear-memoize-table 'immediate-canonical-ancestors-tr)
  (clear-memoize-table 'canonical-ancestors-path)
  (clear-memoize-table 'canonical-ancestors-tr-path))