		Search-engine friendly clone of the ACL2 documentation.

System-attachments

System-level algorithms that users can modify with attachments

This topic concerns advanced methods for modifying the behavior of ACL2. See defattach for some relevant background.

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. At the end of this topic is a list that associates each such f with brief documentation (often, just a link). Users are permitted to modify these attachments using defattach-system, even without a trust tag (see defttag), because they do not affect soundness.

Here are two functions that are useful for attaching to many attachable 0-ary system functions.

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 the following example of a pair (f . g) as described above, i.e., a system function f that comes with attachment g.

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

Here is how we can make the so-called ``assume-true-false'' algorithm more aggressive; see assume-true-false-aggressive-p.

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

The following brief explanations are intentionally brief. We expect that those who want to use such system attachments are comfortable as “system programmers”, so that the brief documentation below is sufficient for getting started. Perusal of the ACL2 source code and its comments can fill in details as needed.

Also see efficiency for further discussion on making system attachments that modify ACL2's default behavior.

Summary of attachable system functions

ACL2X-EXPANSION-ALIST
Built-in attachment: IDENTITY-WITH-STATE
[Undocumented: low-level system utility]

ALWAYS-DO-PROOFS-DURING-MAKE-EVENT-EXPANSION
Built-in attachment: CONSTANT-NIL-FUNCTION-ARITY-0
Documentation: See make-event.

ANCESTORS-CHECK
Built-in attachment: ANCESTORS-CHECK-BUILTIN
Documentation: Backchaining control; see use-trivial-ancestors-check. Source function strip-ancestor-literals might also be useful.

APPLY$-USERFN
Built-in attachment: DOPPELGANGER-APPLY$-USERFN
[Undocumented: low-level system utility]

ASSUME-TRUE-FALSE-AGGRESSIVE-P
Built-in attachment: CONSTANT-NIL-FUNCTION-ARITY-0
Documentation: See assume-true-false-aggressive-p.

BADGE-USERFN
Built-in attachment: DOPPELGANGER-BADGE-USERFN
[Undocumented: low-level system utility]

BEING-OPENEDP-LIMITED-FOR-NONREC
Built-in attachment: CONSTANT-T-FUNCTION-ARITY-0
Documentation: Attach to constant-nil-function-arity-0 to extend to non-recursively defined functions the stack-based limitation on opening recursively-defined functions.

BRKPT1-BRR-DATA-ENTRY
Built-in attachment: BRKPT1-BRR-DATA-ENTRY-BUILTIN
Documentation: See with-brr-data.

BRKPT2-BRR-DATA-ENTRY
Built-in attachment: BRKPT2-BRR-DATA-ENTRY-BUILTIN
Documentation: See with-brr-data.

CONJOIN-CLAUSE-SETS-BOUND
Built-in attachment: CONJOIN-CLAUSE-SETS-BOUND-BUILTIN
Documentation: Attach to a constant function that returns a natural number (default 50) bounding how large a clause-set can be to do smart merging into another clause-set; see comments in the definition of conjoin-clause-sets in the ACL2 sources for more explanation.

HEAVY-LINEAR-P
Built-in attachment: CONSTANT-NIL-FUNCTION-ARITY-0
Documentation: See heavy-linear-p.

HIDE-WITH-COMMENT-P
Built-in attachment: CONSTANT-T-FUNCTION-ARITY-0
Documentation: See hide.

ONCEP-TP
Built-in attachment: ONCEP-TP-BUILTIN
Documentation: See free-variables-type-prescription.

PRINT-CLAUSE-ID-OKP
Built-in attachment: PRINT-CLAUSE-ID-OKP-BUILTIN
Documentation: See set-print-clause-ids.

QUICK-AND-DIRTY-SRS
Built-in attachment: QUICK-AND-DIRTY-SRS-BUILTIN
Documentation: See quick-and-dirty-subsumption-replacement-step.

RELIEVE-HYP-FAILURE-ENTRY-SKIP-P
Built-in attachment: RELIEVE-HYP-FAILURE-ENTRY-SKIP-P-BUILTIN
[Undocumented: low-level system utility]

REMOVE-GUARD-HOLDERS-BLOCKED-BY-HIDE-P
Built-in attachment: CONSTANT-T-FUNCTION-ARITY-0
Documentation: See guard-holders.

REMOVE-GUARD-HOLDERS-LAMP
Built-in attachment: CONSTANT-T-FUNCTION-ARITY-0
Documentation: See guard-holders.

REMOVE-TRIVIAL-EQUIVALENCES-ENABLED-P
Built-in attachment: CONSTANT-T-FUNCTION-ARITY-0
Documentation: See remove-trivial-equivalences-enabled-p.

REWRITE-IF-AVOID-SWAP
Built-in attachment: CONSTANT-NIL-FUNCTION-ARITY-0
Documentation: See rewrite-if-avoid-swap.

RW-CACHE-DEBUG
Built-in attachment: RW-CACHE-DEBUG-BUILTIN
[Undocumented: low-level system utility]

RW-CACHE-DEBUG-ACTION
Built-in attachment: RW-CACHE-DEBUG-ACTION-BUILTIN
[Undocumented: low-level system utility]

RW-CACHEABLE-FAILURE-REASON
Built-in attachment: RW-CACHEABLE-FAILURE-REASON-BUILTIN
[Undocumented: low-level system utility]

SET-LD-HISTORY-ENTRY-USER-DATA
Built-in attachment: SET-LD-HISTORY-ENTRY-USER-DATA-DEFAULT
Documentation: See ld-history.

SIMPLIFIABLE-MV-NTH-P
Built-in attachment: CONSTANT-T-FUNCTION-ARITY-0
Documentation: See theories-and-primitives.

TOO-MANY-IFS-POST-REWRITE
Built-in attachment: TOO-MANY-IFS-POST-REWRITE-BUILTIN
Documentation: Heuristic for discarding rewriter result with “too many IFs”. Defeat by attaching constant-nil-function-arity-2.

TOO-MANY-IFS-PRE-REWRITE
Built-in attachment: TOO-MANY-IFS-PRE-REWRITE-BUILTIN
Documentation: Heuristic for skipping rewrite when unrewritten result has “too many IFs”. Defeat by attaching constant-nil-function-arity-2.

UNTRANSLATE-LAMBDA-OBJECT-P
Built-in attachment: CONSTANT-T-FUNCTION-ARITY-0
Documentation: See lambda$.

UPDATE-BRR-DATA-1
Built-in attachment: UPDATE-BRR-DATA-1-BUILTIN
Documentation: See with-brr-data.

UPDATE-BRR-DATA-2
Built-in attachment: UPDATE-BRR-DATA-2-BUILTIN
Documentation: See with-brr-data.

USE-ENHANCED-RECOGNIZER
Built-in attachment: CONSTANT-T-FUNCTION-ARITY-0
Documentation: Heuristic for treating (equal TERM nil) and (equal nil TERM) as providing a type for TERM during forward-chaining and other operations that assume such a term to be true.

WORSE-THAN
Built-in attachment: WORSE-THAN-BUILTIN
[Undocumented: low-level system utility]

WORSE-THAN-OR-EQUAL
Built-in attachment: WORSE-THAN-OR-EQUAL-BUILTIN
[Undocumented: low-level system utility]

Subtopics

Assume-true-false-aggressive-p: Control rewriter's use of the type-alist with IF calls
Remove-trivial-equivalences-enabled-p: Avoid removal of trivial equivalences during rewriting
Heavy-linear-p: Extend the use of linear-arithmetic during rewriting
Rewrite-if-avoid-swap: Control rewriter's swapping of branches of IF calls