mace4 - searches for finite countermodels of first-order
statements
mace4 [options] < input-file >
output-file
This manual page documents briefly the mace4 command.
The program mace4 searches for finite structures satisfying
first-order and equational statements, the same kind of statement that
prover9(1) accepts. If the statement is the denial of some
conjecture, any structures found by mace4 are counterexamples to the
conjecture. mace4 can be a valuable complement to prover9(1),
looking for counterexamples before (or at the same time as) using
prover9(1) to search for a proof. It can also be used to help debug
input clauses and formulas for prover9(1).
A summary of options is included below. Options override the
equivalent settings given in the input file. To set or clear a flag, you
must give 1 or 0 as the value.
- -help
- This tells mace4 to print a summary of these command-line
options.
- -n n
- This gives the starting domain size for the search. The default value is
2. If you also give an -N option, mace4 will iterate domain
sizes up through the -N value, using an increment given by the
-I value. Otherwise, mace4 will search only for the
-n value.
- -N n
- This gives the ending domain size for the search. The default is 10.
- -i n
- This gives the domain size increment for the search. The default is
1.
- -q n
- This flag overrides the parameter iterate. It says to try the sizes that
are prime numbers, from -n up through -N.
- -m n
- Stop searching when the nth structure has been found. The default
is 1.
- -t n
- Stop searching after n seconds.
- -s n
- Allow at most n seconds for each domain size. The parameter can be
used (together with -t) to give an overall time limit.
- -b n
- Stop searching when (about) n megabytes of memory have been
used.
- -V n
- 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 `_'.
- -P n
- 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 isofilter(1) and interpformat(1).
- -p n
- If this flag is set, and if -P is clear, all structures that are
found are printed in a tabular form.
- -R n
- 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.
- -v n
- If this 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.)
- -T n
- If the trace flag is set, detailed information about the search, including
a trace of all assignments and backtracking, is printed to the standard
output. This flag causes a lot of output, so it should be used only on
small searches.
There also exist a number of advanced options, which are used for
experimentation with search methods. They can be ignored by nearly all
users. For descriptions of these options, see the original mace4
manual.
prover9(1).
Full documentation for mace4 is found in the prover9 manual,
available on Debian systems in the prover9-doc package at
/usr/share/doc/prover9-doc/manual/index.html.
The original mace4 manual, which can be downloaded at
http://www.cs.unm.edu/~mccune/prover9/mace4.pdf
mace4 was written by William McCune
<mccune@cs.unm.edu>
This manual page was written by Peter Collingbourne
<peter@pcc.me.uk>, for the Debian project (but may be used by
others).