(advanced topic) controlling a heuristic in the prover's clausifier

This topic is probably only of interest to those who are undertaking particularly complex proof developments.

The ACL2 prover's handling of propositional logic uses a heuristic that we believe might cause the prover to slow down significantly or even to trigger a stack overflow. However, we believe these negative effects are only felt on very large formulas — formulas that are likely to cause similar degradation of many other parts of ACL2.

The following two events turn off that heuristic (by eliminating calls to
source function

(defun quick-and-dirty-srs-off (cl1 ac) (declare (ignore cl1 ac) (xargs :mode :logic :guard t)) nil) (defattach-system quick-and-dirty-srs quick-and-dirty-srs-off)

However, if you feel the need to try this out, please remember that the
proof is likely to fail anyway since other parts of ACL2 will probably be
stressed. A more basic problem with your proof strategy may exist: the
formulas are getting extraordinarily large. A common approach for avoiding
such problem include disabling functions (see in-theory). Other less
common approaches might help if you are sufficiently desperate, such as
defining your own

For an example of where this capability has proven useful, see
without-subsumption. That tool uses `set-case-split-limitations`
as well, since that is another way to control the prover's handling of
propositional logic.

To turn the heuristic back on:

(defattach-system quick-and-dirty-srs quick-and-dirty-srs-builtin)