		Search-engine friendly clone of the ACL2 documentation.

Table

Using-tables-efficiently

Notes on how to use tables efficiently

(Thanks to Jared Davis for contributing this documentation topic, to which we have made only minor modifications.)

Suppose your book contains table events, or macros that expand into table events, of the following form:

(table my-table 'my-field <computation>)

Then <computation> will be evaluated twice during certify-book and again every time you include the book with include-book. In some cases this overhead can be avoided using make-event.

See also defconsts for an analogous trick involving defconst.

As an example, suppose we want to store numbers in a table only if they satisfy some computationally expensive predicate. We'll introduce a new book, number-table.lisp, and create a table to store these numbers:

(table number-table 'data nil)

Instead of implementing a ``computationally expensive predicate,'' we'll write a function that just prints a message when it is called and accepts even numbers:

(defun expensive-computation (n)
  (prog2$ (cw "Expensive computation on ~x0.~%" n)
          (evenp n)))

Now we'll implement a macro, add-number, which will add its argument to the table only if it satisfies the expensive predicate:

(defmacro add-number (n)
  `(table number-table 'data
          (let ((current-data
                 (cdr (assoc-eq 'data (table-alist 'number-table world)))))
            (if (expensive-computation ,n)
                (cons ,n current-data)
              current-data))))

Finally, we'll call add-number a few times to finish the book.

(add-number 1)
(add-number 2)
(add-number 3)

When we now invoke (certify-book "number-table"), we see the expensive predicate being called twice for each number: once in Step 2, the main pass, then again in Step 3, the admissibility check. Worse, the computation is performed again for each number when we use include-book to load number-table, e.g.,

ACL2 !>(include-book "number-table")
Expensive computation on 1.
Expensive computation on 2.
Expensive computation on 3.

To avoid these repeated executions, we can pull the test out of the table event using make-event. Here's an alternate implementation of add-number that won't repeat the computation:

(defmacro add-number (n)
  `(make-event
    (if (expensive-computation ,n)
        '(table number-table 'data
                (cons ,n (cdr (assoc 'data
                                     (table-alist 'number-table world)))))
      '(value-triple :expensive-computation-failed))))

When we recertify number-table.lisp, we'll see the expensive computation is still called once for each number in Step 2, but is no longer called during Step 3. Similarly, the include-book no longer shows any calls of the expensive computation.