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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
|
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>Prover9 Manual: Mace4 Options</title>
<link rel="stylesheet" href="manual.css">
</head>
<body>
<hr>
<table width="100%">
<tr>
<colgroup>
<col width="33%">
<col width="34%">
<col width="33%">
</colgroup>
<td align="left"><i>Prover9 Manual</i>
<td align="center"><img src="prover9-5a-256t.gif">
<td align="right"><i>Version 2009-02A</i>
</table>
<hr>
<!-- Main content -->
<h1>Mace4 Options</h1>
Mace4 accepts <tt>set</tt>, <tt>clear</tt>, and <tt>assign</tt>
commands in the input file. Several of these are in common with
Prover9 (e.g., <tt>assign(max_seconds, 30)</tt>), but most
are specifically for Mace4.
<p>
If Mace4 is called with the command-line option <tt>-c</tt>
(compatability mode), it will ignore any <tt>set</tt>, <tt>clear</tt>,
and <tt>assign</tt> that it does not recognize, assuming they
are meant for some other program (Prover9).
<p>
Most Mace4 options can be specified on the command line instead
of in the input file.
When Mace4 options are specified on the command line, single-character
codes are used. For example, the command-line option
<tt>-t 30</tt> means the same as <tt>assign(max_second, 30)</tt>
in the input file. If an option is given in <i>both</i> places,
the one on the command line takes precedence.
Command-line options for Boolean-valued options (flags)
always take an argument: 1 means "set", and 0 means "clear".
For example, <tt>-V 1</tt> means <tt>set(prolog_style_vaiables</tt>,
and <tt>-V 0</tt> means <tt>clear(prolog_style_variables)</tt>.
<p>
The command "<tt>mace4 -help</tt>" shows the correspondence between
the command-line codes and the option names, and it shows the default
values.
<h2>Symbol Ordering</h2>
Like Prover9, Mace4 accepts <tt>function_order</tt> and
<tt>relation_order</tt> commands that specify an order on the
symbols in the problem. The syntax of the commands is the
<a href="term-order.html#lex_command">same as in Prover9</a>, for example,
<pre class="my_file">
predicate_order([=, <=, P, Q]). % = < P < Q
function_order([a, b, c, +, *, h, g]). % a < b < c < + < * < h < g
</pre>
Mace4's the default symbol order is the
<a href="term-order.html#default_lex">same as Prover9's</a>.
As in Prover9, function symbols are always less than predicate symbols.
<p>
The symbol order can have a big effect on the time it takes to find
a model or exhaust a domain size, because it determines the order in which
Mace4 tries to fill in the function and relation tables. Unfortunately,
we do not know of any general-purpose heuristics for selecting a
good symbol order. If Mace4 takes too long to go through a particular
domain size, we suggest trying a different symbol order.
<h2>Option Listing</h2>
<h3>Basic Options</h3>
<pre class="my_file">
assign(start_size, <i>n</i>). % default <i>n</i>=2, range [2 .. <tt>INT_MAX</tt>] % command-line -n <i>n</i>
</pre>
<pre class="my_file">
assign(end_size, <i>n</i>). % default <i>n</i>=-1, range [-1 .. <tt>INT_MAX</tt>] % command-line -N <i>n</i>
</pre>
<pre class="my_file">
assign(increment, <i>n</i>). % default <i>n</i>=1, range [1 .. <tt>INT_MAX</tt>] % command-line -i <i>n</i>
</pre>
These three parameter work together to determine the domain sizes
to be searched. The search starts for structures of size
<tt>start_size</tt>; if that search fails,
the size is incremented, and another search starts. This continues
up through the value <tt>end_size</tt> (or until some other limit
terminates the process). If <tt>end_size</tt> is -1, there is no limit.
(Also see the <tt>iterate</tt> parameter below.)
<p>
For example, the command-line options "<tt>-n 5 -N 11 -i 2</tt>"
say to try domain sizes 5,7,9,11.
<pre class="my_file">
assign(domain_size, <i>n</i>). % default <i>n</i>=0, range [0 .. <tt>INT_MAX</tt>] % command-line -n <i>n</i>
</pre>
This parameter says to search <i>only</i> the given size.
This (meta-) parameter works simply by making the following changes.
<pre>
assign(domain_size, <i>n</i>) -> assign(start_size, <i>n</i>).
assign(domain_size, <i>n</i>) -> assign(end_size, <i>n</i>).
</pre>
<pre class="my_file">
assign(iterate, <i>string</i>). % default <i>string</i>=all, range [all,evens,odds,primes,nonprimes]
</pre>
The <tt>iterate</tt> parameter can be used to add an additional constraint
to the domain sizes. It can be used together with the <tt>increment</tt>
parameter. The <tt>iterate</tt> parameter cannot be specified on the
command line.
<pre class="my_file">
assign(max_models, <i>n</i>). % default <i>n</i>=1, range [-1 .. <tt>INT_MAX</tt>] % command-line -m <i>n</i>
</pre>
The parameter <tt>max_models</tt> says to stop searching when the <i>n</i>-th structure has been found.
A value of -1 means there is no limit.
<pre class="my_file">
assign(max_seconds, <i>n</i>). % default <i>n</i>=-1, range [-1 .. <tt>INT_MAX</tt>] % command-line -t <i>n</i>
</pre>
The parameter
<a href="limits.html#max_seconds"><tt><b>max_seconds</b></tt></a>
says to stop searching after <i>n</i> seconds.
A value of -1 means there is no limit.
<pre class="my_file">
assign(max_seconds_per, <i>n</i>). % default <i>n</i>=-1, range [-1 .. <tt>INT_MAX</tt>] % command-line -s <i>n</i>
</pre>
The parameter allows at most <i>n</i> seconds for each domain size.
The parameter <a href="limits.html#max_seconds"><tt><b>max_seconds</b></tt></a> can be used (together with <tt>max_seconds_per</tt>)
to given an overall time limit.
A value of -1 means there is no limit.
<pre class="my_file">
assign(max_megs, <i>n</i>). % default <i>n</i>=200, range [-1 .. <tt>INT_MAX</tt>] % command-line -b <i>n</i>
</pre>
The parameter <a href="limits.html#max_megs"><tt><b>max_megs</b></tt></a>
says to stop searching when (about) <i>n</i> megabytes of memory have been used.
A value of -1 means there is no limit.
<pre class="my_file">
set(prolog_style_variables). % command-line -V 1
clear(prolog_style_variables). % default clear % command-line -V 0
</pre>
A rule is needed for distinguishing variables from constants in
clauses and formulas with free variables.
If this flag is clear, variables start with
(lower case) 'u' through 'z'.
If this flag is set, variables in clauses start with
(upper case) 'A' through 'Z' or '_'.
<pre class="my_file">
set(print_models). % default set % command-line -P 1
clear(print_models). % command-line -P 0
</pre>
If this flag is set, all structures that are found are printed
in "standard" form, which means they are suitable as
input to other LADR programs such as
<a href="m4-isofilter.html">isofilter</a> and
<a href="m4-interpforma.html">interpformat</a>.
<pre class="my_file">
set(print_models_tabular). % command-line -p 1
clear(print_models_tabular). % default clear % command-line -p 0
</pre>
If this flag is set, and if is clear,
all structures that are found are printed in a tabular form.
If both <tt>print_models</tt> and <tt>print_models_standard</tt>
are set, the last one in the input takes effect.
<pre class="my_file">
set(integer_ring). % command-line -R 1
clear(integer_ring). % default clear % command-line -R 0
</pre>
If this flag is set, a ring structure is is applied to the search.
The operations {+,-,*} are assumed to be the ring of integers
(mod domain_size). This method puts a tight constraint on
the search, allowing much larger structures to be investigated.
Here is an example.
<pre class="my_job">
mace4 -f <a href="ring41.in">ring41.in</a> > <a href="ring41.out">ring41.out</a>
</pre>
For further information on the <tt>integer_ring</tt> flag, see
<a href="http://www.cs.unm.edu/~mccune/slides/award-2004.pdf">
slides from a workshop presentation</a>.
<pre class="my_file">
set(order_domain).
clear(order_domain). % default clear
</pre>
If this flag is set, the relations <tt><</tt> and <tt><=</tt>
are fixed as order relations on the domain in the obvious way.
<pre class="my_file">
set(arithmetic).
clear(arithmetic). % default clear
</pre>
If this flag is set, several function and relation symbols understood
by Mace4 as operations and relations on the integers, and evaluation
of terms involving those symbols occurs during the search for models.
See the page <a href="m4-arithmetic.html">Arithmetic for Mace4</a>.
<pre class="my_file">
set(verbose). % command-line -v 1
clear(verbose). % default clear % command-line -v 0
</pre>
If the <tt>verbose</tt> flag is set, the output file receives
information about the search, including the initial partial model (the
part of the model that can be determined before backtracking starts)
and timing and other statistics for each domain size. (It does not
give a trace of the backtracking, so it does not consume a lot of file
space.)
<pre class="my_file">
set(trace). % command-line -T 1
clear(trace). % default clear % command-line -T 0
</pre>
If the <tt>trace</tt> flag is set, detailed information about the
search, including a trace of all assignments and backtracking, is
printed to the standard output. <i>This flag causes a lot of output, so
it should be used only on small searches</i>.
<h3>Advanced Options</h3>
These options are used for experimentation with search methods.
They can be ignored by nearly all users. For descriptions of
most of these options, see the original Mace4 manual
[<a href="references.html#McCune-Mace4">McCune-Mace4</a>]
(<a href="http://www.cs.unm.edu/~mccune/prover9/mace4.pdf">PDF)</a>.
<pre class="my_file">
set(lnh). % default set % command-line -L 1
clear(lnh). % command-line -L 0
</pre>
<pre class="my_file">
assign(selection_order, <i>n</i>). % default <i>n</i>=2, range [0 .. 2] % command-line -O <i>n</i>
</pre>
<pre class="my_file">
assign(selection_measure, <i>n</i>). % default <i>n</i>=4, range [0 .. 4] % command-line -M <i>n</i>
</pre>
<pre class="my_file">
set(negprop). % default set % command-line -G 1
clear(negprop). % command-line -G 0
</pre>
<pre class="my_file">
set(neg_assign). % default set % command-line -H 1
clear(neg_assign). % command-line -H 0
</pre>
<pre class="my_file">
set(neg_assign_near). % default set % command-line -I 1
clear(neg_assign_near). % command-line -I 0
</pre>
<pre class="my_file">
set(neg_elim). % default set % command-line -J 1
clear(neg_elim). % command-line -J 0
</pre>
<pre class="my_file">
set(neg_elim_near). % default set % command-line -K 1
clear(neg_elim_near). % command-line -K 0
</pre>
<pre class="my_file">
set(skolems_last). % command-line -S 1
clear(skolems_last). % default clear % command-line -S 0
</pre>
<hr>
Next Section:
<a href="m4-arithmetic.html">Interpformat</a>
</body>
</html>
|
