		Search-engine friendly clone of the ACL2 documentation.

Optimization

Preferred-definitions

To instruct GL to symbolically execute filter2 in place of filter1, we can do the following:

(defthm filter1-for-gl
  (equal (filter1 x) (filter2 x))
  :rule-classes nil)

(gl::set-preferred-def filter1 filter1-for-gl)

The set-preferred-def form extends a table that GL consults when expanding a function's definition. Each entry in the table pairs a function name with the name of a theorem. The theorem must state that a call of the function is unconditionally equal to some other term.

When GL encounters a call of a function in this table, it replaces the call with the right-hand side of the theorem, which is justified by the theorem. So after the above event, GL will replace calls of filter1 with filter2.

As another example of a preferred definition, GL automatically optimizes the definition of evenp, which ACL2 defines as follows:

(evenp x) = (integerp (* x (/ 2)))

This definition is basically unworkable since GL provides little support for rational numbers. However, GL has an efficient, built-in implementation of logbitp. So to permit the efficient execution of evenp, GL proves the following identity and uses it as evenp's preferred definition.

(defthm evenp-is-logbitp
  (equal (evenp x)
         (or (not (acl2-numberp x))
             (and (integerp x)
                  (equal (logbitp 0 x) nil)))))