		Search-engine friendly clone of the ACL2 documentation.

System-attachments

System-level algorithms that users can modify with attachments

For background on attachments, see defattach.

If you evaluate the form (global-val 'attachments-at-ground-zero (w state)), you will see a list of pairs of the form (f . g), where f is a built-in constrained utility and g is its attachment. Here is one such pair.

(ASSUME-TRUE-FALSE-AGGRESSIVE-P . CONSTANT-NIL-FUNCTION-ARITY-0)

Users are permitted to modify these attachments, even without a trust tag (see defttag), because they do not affect soundness. See defattach-system.

We do not attempt to explain how to define functions to attach to system functions. We do however point out these two useful functions, for attaching to some constant functions (functions with arity 0).

Function: constant-t-function-arity-0

(defun constant-t-function-arity-0
       nil (declare (xargs :guard t))
       t)

Function: constant-nil-function-arity-0

(defun constant-nil-function-arity-0
       nil (declare (xargs :guard t))
       nil)

To see how to use one of these functions, consider again the example above, where constrained system function assume-true-false-aggressive-p has the attachment, constant-nil-function-arity-0. Here we make the so-called ``assume-true-false'' algorithm more aggressive.

(defattach-system assume-true-false-aggressive-p constant-t-function-arity-0)

Note that we are not explaining here what it means to make that algorithm more aggressive! We expect those who want to use these attachments to be comfortable as ``system programmers'', as they peruse the ACL2 source code and its comments in order to see how to modify system behavior with attachments. Perhaps more user-level documentation will be written to help with that process.

Also see efficiency for more about using attachments to modify the prover's behavior.