Mace4 Options

Mace4 accepts set, clear, and assign commands in the input file. Several of these are in common with Prover9 (e.g., assign(max_seconds, 30)), but most are specifically for Mace4.

If Mace4 is called with the command-line option -c (compatability mode), it will ignore any set, clear, and assign that it does not recognize, assuming they are meant for some other program (Prover9).

Each Mace4 option can be specified on the command line instead of in the input file. In practice, Mace4 options are usually specified on the command line, so that the input files can be used also for Prover9.

When Mace4 options are specified on the command line, single-character codes are used. For example, the command-line option -t 30 means the same as assign(max_second, 30) in the input file. If an option is given in both 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, -V 1 means set(prolog_style_vaiables, and -V 0 means clear(prolog_style_variables).

The command "mace4 -help" shows the correspondence between the command-line codes and the option names, and it shows the default values.

Option Listing

Basic Options

assign(domain_size, n).  % default n=2, range [2 .. 200]  % command-line -n n

assign(iterate_up_to, n).  % default n=10, range [-1 .. 200]  % command-line -N n

assign(increment, n).  % default n=1, range [1 .. INT_MAX]  % command-line -i n

These three parameter work together to determine the domain sizes to be searched. The search starts for structures of size domain_size; if that search fails, the size is incremented, and another search starts. This continues up through the value iterate_up_to (or until some other limit terminates the process).

For example, the command-line options "-n 5 -N 11 -i 2" say to try domain sizes 5,7,9,11.

set(iterate_primes).                       % command-line -q 1
clear(iterate_primes).    % default clear  % command-line -q 0

This flag overrides the parameter iterate. It says to try the sizes that are prime numbers, from domain_size up through iterate_up_to.

For example, the command-line options "-n 10 -N 30 -q 1" say to try domain sizes 11, 13, 17, 19, 23, 29.

assign(max_models, n).  % default n=1, range [-1 .. INT_MAX]  % command-line -m n

The parameter max_models says to stop searching when the n-th structure has been found.

assign(max_seconds, n).  % default n=INT_MAX, range [0 .. INT_MAX]  % command-line -t n

The parameter max_seconds says to stop searching after n seconds.

assign(max_seconds_per, n).  % default n=INT_MAX, range [0 .. INT_MAX]  % command-line -s n

The parameter allows at most n seconds for each domain size. The parameter max_seconds can be used (together with max_seconds_per) to given an overall time limit.

assign(max_megs, n).  % default n=200, range [0 .. INT_MAX]  % command-line -b n

The parameter max_megs says to stop searching when (about) n megabytes of memory have been used.

set(prolog_style_variables).                       % command-line -V 1
clear(prolog_style_variables).    % default clear  % command-line -V 0

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 '_'.

set(print_models_standard).      % default set    % command-line -P 1
clear(print_models_standard).                     % command-line -P 0

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 and interpformat.

set(print_models).                       % command-line -p 1
clear(print_models).    % default clear  % command-line -p 0

If this flag is set, and if print_models_standard is clear, all structures that are found are printed in a tabular form.

set(integer_ring).                       % command-line -R 1
clear(integer_ring).    % default clear  % command-line -R 0

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.

mace4 -f ring41.in > ring41.out

For further information on the integer_ring flag, see slides from a workshop presentation.

set(verbose).                       % command-line -v 1
clear(verbose).    % default clear  % command-line -v 0

If the verbose 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.)

set(trace).                       % command-line -T 1
clear(trace).    % default clear  % command-line -T 0

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.

Advanced Options

These options 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 [McCune-Mace4] (PDF).

set(lnh).      % default set    % command-line -L 1
clear(lnh).                     % command-line -L 0

assign(selection_order, n).  % default n=2, range [0 .. 2]  % command-line -O n

assign(selection_measure, n).  % default n=4, range [0 .. 4]  % command-line -M n

set(negprop).      % default set    % command-line -G 1
clear(negprop).                     % command-line -G 0

set(neg_assign).      % default set    % command-line -H 1
clear(neg_assign).                     % command-line -H 0

set(neg_assign_near).      % default set    % command-line -I 1
clear(neg_assign_near).                     % command-line -I 0

set(neg_elim).      % default set    % command-line -J 1
clear(neg_elim).                     % command-line -J 0

set(neg_elim_near).      % default set    % command-line -K 1
clear(neg_elim_near).                     % command-line -K 0

set(skolem_last).                       % command-line -S 1
clear(skolem_last).    % default clear  % command-line -S 0

Next Section: Interpformat