|
|
|---|
|
|
|
|---|
(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)