Gc-strategy
The garbage collection strategy
The form (gc-strategy state) provides the value the current
garbage collection strategy if that notion is supported by the underlying host
lisp (currently, CCL only). The logical story is that gc-strategy reads
its value from the oracle field of the ACL2 state. The return
value is thus a triple of the form (mv erp val state), where erp
will always be nil in practice, and logically, val is the top of the
acl2-oracle field of the state (see read-ACL2-oracle) and the returned
state has the updated (popped) acl2-oracle.
For more information, see set-gc-strategy.
