1MACE4(1) General Commands Manual MACE4(1)
2
6 mace4 - searches for finite countermodels of first-order statements
7
9 mace4 [options] < input-file > output-file
10
12 This manual page documents briefly the mace4 command.
13 The program mace4 searches for finite structures satisfying first-order
15 and equational statements, the same kind of statement that prover9(1)
16 accepts. If the statement is the denial of some conjecture, any struc‐
17 tures found by mace4 are counterexamples to the conjecture. mace4 can
18 be a valuable complement to prover9(1), looking for counterexamples
19 before (or at the same time as) using prover9(1) to search for a proof.
20 It can also be used to help debug input clauses and formulas for
21 prover9(1).
22
24 A summary of options is included below. Options override the equiva‐
25 lent settings given in the input file. To set or clear a flag, you
26 must give 1 or 0 as the value.
27 -help This tells mace4 to print a summary of these command-line
29 options.
30 -n n This gives the starting domain size for the search. The default
32 value is 2. If you also give an -N option, mace4 will iterate
33 domain sizes up through the -N value, using an increment given
34 by the -I value. Otherwise, mace4 will search only for the -n
35 value.
36 -N n This gives the ending domain size for the search. The default is
38 10.
39 -i n This gives the domain size increment for the search. The default
41 is 1.
42 -q n This flag overrides the parameter iterate. It says to try the
44 sizes that are prime numbers, from -n up through -N.
45 -m n Stop searching when the nth structure has been found. The
47 default is 1.
48 -t n Stop searching after n seconds.
50 -s n Allow at most n seconds for each domain size. The parameter can
52 be used (together with -t) to give an overall time limit.
53 -b n Stop searching when (about) n megabytes of memory have been
55 used.
56 -V n A rule is needed for distinguishing variables from constants in
58 clauses and formulas with free variables. If this flag is clear,
59 variables start with (lower case) `u' through `z'. If this flag
60 is set, variables in clauses start with (upper case) `A' through
61 `Z' or `_'.
62 -P n If this flag is set, all structures that are found are printed
64 in `standard' form, which means they are suitable as input to
65 other LADR programs such as isofilter(1) and interpformat(1).
66 -p n If this flag is set, and if -P is clear, all structures that are
68 found are printed in a tabular form.
69 -R n If this flag is set, a ring structure is is applied to the
71 search. The operations {+,-,*} are assumed to be the ring of
72 integers (mod domain_size). This method puts a tight constraint
73 on the search, allowing much larger structures to be investi‐
74 gated.
75 -v n If this flag is set, the output file receives information about
77 the search, including the initial partial model (the part of the
78 model that can be determined before backtracking starts) and
79 timing and other statistics for each domain size. (It does not
80 give a trace of the backtracking, so it does not consume a lot
81 of file space.)
82 -T n If the trace flag is set, detailed information about the search,
84 including a trace of all assignments and backtracking, is
85 printed to the standard output. This flag causes a lot of out‐
86 put, so it should be used only on small searches.
87 There also exist a number of advanced options, which are used for
89 experimentation with search methods. They can be ignored by nearly all
90 users. For descriptions of these options, see the original mace4 man‐
91 ual.
92
94 prover9(1).
95 Full documentation for mace4 is found in the prover9 manual, available
96 on Debian systems in the prover9-doc package at
97 /usr/share/doc/prover9-doc/manual/index.html.
98 The original mace4 manual, which can be downloaded at
99 http://www.cs.unm.edu/~mccune/prover9/mace4.pdf
100
102 mace4 was written by William McCune <mccune@cs.unm.edu>
103 This manual page was written by Peter Collingbourne
105 <pcc03@doc.ic.ac.uk>, for the Debian project (but may be used by oth‐
106 ers).
107 August 12, 2007 MACE4(1)