1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
<html>
<head><title>CASE-SPLIT-LIMITATIONS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>CASE-SPLIT-LIMITATIONS</h2>a list of two ``numbers'' limiting the number of cases produced at once
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
<pre>
Examples:
ACL2 !>(case-split-limitations (w state))
(500 100)
</pre>
With the setting above, <code>clausify</code> will not try subsumption/replacement
if more than 500 clauses are involved. Furthermore, the simplifier,
as it sweeps over a clause, will inhibit further case splits
when it has accumulated 100 subgoals. This inhibition is implemented by
continuing to rewrite subsequent literals but not splitting out their cases.
This can produce literals containing <code>IF</code>s.
<p>
See <a href="SET-CASE-SPLIT-LIMITATIONS.html">set-case-split-limitations</a> for a more general discussion.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
