## QUICK-AND-DIRTY-SUBSUMPTION-REPLACEMENT-STEP

(advanced topic) controlling a heuristic in the prover's clausifier
Major Section: OTHER

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 `quick-and-dirty-subsumption-replacement-step`

, after which
this documentation topic is named).

(defun quick-and-dirty-srs-off (cl1 ac)
(declare (ignore cl1 ac)
(xargs :mode :logic :guard t))
nil)
(defattach 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
`IF`

function to use in place of the built-in `IF`

.

If you do find an example for which the above two events provide significant
benefit, we (the ACL2 implementors) would be interested in hearing about
it.

To turn the heuristic back on:

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