		Search-engine friendly clone of the ACL2 documentation.

Cons-with-hint

Alternative to cons that tries to avoid consing when a suitable cons structure is provided as a hint.

This is a special purpose function that is intended to help with reducing the memory usage of functions that modify existing cons tree structures. Also see hons for a way to share cons structures; however, cons-with-hint is likely much cheaper than hons and hence can be useful for reducing consing without the overhead of hons.

Logically (cons-with-hint x y hint) is just (cons x y); hint is completely irrelevant and ignored. We generally expect that cons-with-hint will just be left enabled, so you should never have to reason about it.

But cons-with-hint has a special raw Common Lisp definition that tries to avoid consing by using your hint. Specifically: if hint is the cons (x . y), then hint is returned without creating a new cons. Equality checking against x and y is done using eql, which makes it a fast but incomplete check for equality.

What good is this? A fairly common operation in ACL2 is to ``change'' an existing data structure by consing together a new structure that is similar to it, but perhaps with some subtrees replaced. In many cases, some portion of the structure does not need to change.

For instance, consider a function like remove-equal, which updates a list by removing all copies of some element from it. The definition of remove-equal is as follows (in the logic; it has a slightly different definition in raw Lisp).

Function: remove-equal

(defun remove-equal (x l)
  (declare (xargs :guard (true-listp l)))
  (cond ((endp l) nil)
        ((equal x (car l))
         (remove-equal x (cdr l)))
        (t (cons (car l)
                 (remove-equal x (cdr l))))))

You can see that if l doesn't have any copies of x, this function will essentially make a fresh copy of the whole list x. That could waste a lot of memory when x is long. The choice was made to define remove-equal ``under the hood'' to call Common Lisp's function, remove; but it is easy to write a new version of remove-equal that uses cons-with-hint:

(defun remove-equal-with-hint (x l)
  (declare (xargs :guard (true-listp l)))
  (mbe :logic (remove-equal x l)
       :exec (cond ((endp l) nil)
                   ((equal x (car l))
                    (remove-equal-with-hint x (cdr l)))
                   (t
                    (cons-with-hint (car l)
                                    (remove-equal-with-hint x (cdr l))
                                    l)))))

This new version avoids consing in the case that we are not dropping an element. For example, at the time of this writing, we found the following memory usages on our copy of ACL2 built on CCL:

:q

;; 16 MB of memory allocated
(let ((list (make-list 1000 :initial-element 0)))
  (time (loop for i from 1 to 1000 do (remove-equal i list))))

;; 0 MB of memory allocated
(let ((list (make-list 1000 :initial-element 0)))
  (time (loop for i from 1 to 1000 do (remove-equal-with-hint i list))))

This memory usage is not very surprising when you consider that the list does not change when no removal takes place. For example (still in raw Lisp):

? (let ((x '(a b c d e))) (eq x (remove-equal-with-hint 3 x)))
T
?

Note that ACL2 asks Lisp to inline calls of cons-with-hint, so there will likely be no function call overhead for using cons-with-hint.