Prover9 Manual Version 2009-02A

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).

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

Symbol Ordering

Like Prover9, Mace4 accepts function_order and relation_order commands that specify an order on the symbols in the problem. The syntax of the commands is the same as in Prover9, for example, 
predicate_order([=, <=, P, Q]).          % = < P < Q
function_order([a, b, c, +, *, h, g]).   % a < b < c < + < * < h < g
Mace4's the default symbol order is the same as Prover9's. As in Prover9, function symbols are always less than predicate symbols.

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.

Option Listing

Basic Options

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

assign(end_size, n).  % default n=-1, range [-1 .. INT_MAX]  % 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 start_size; if that search fails, the size is incremented, and another search starts. This continues up through the value end_size (or until some other limit terminates the process). If end_size is -1, there is no limit. (Also see the iterate parameter below.)

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

assign(domain_size, n).  % default n=0, range [0 .. INT_MAX]  % command-line -n n
This parameter says to search only the given size. This (meta-) parameter works simply by making the following changes. 
  assign(domain_size, n) -> assign(start_size, n).
  assign(domain_size, n) -> assign(end_size, n).

assign(iterate, string).  % default string=all, range [all,evens,odds,primes,nonprimes]
The iterate parameter can be used to add an additional constraint to the domain sizes. It can be used together with the increment parameter. The iterate parameter cannot be specified on the command line. 
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. A value of -1 means there is no limit. 
assign(max_seconds, n).  % default n=-1, range [-1 .. INT_MAX]  % command-line -t n
The parameter max_seconds says to stop searching after n seconds. A value of -1 means there is no limit. 
assign(max_seconds_per, n).  % default n=-1, range [-1 .. 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. A value of -1 means there is no limit. 
assign(max_megs, n).  % default n=200, range [-1 .. INT_MAX]  % command-line -b n
The parameter max_megs says to stop searching when (about) n megabytes of memory have been used. A value of -1 means there is no limit. 
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).      % default set    % command-line -P 1
clear(print_models).                     % 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_tabular).                       % command-line -p 1
clear(print_models_tabular).    % default clear  % command-line -p 0
If this flag is set, and if is clear, all structures that are found are printed in a tabular form. If both print_models and print_models_standard are set, the last one in the input takes effect. 
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(order_domain).
clear(order_domain).        % default clear
If this flag is set, the relations < and <= are fixed as order relations on the domain in the obvious way. 
set(arithmetic).
clear(arithmetic).        % default clear
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 Arithmetic for Mace4. 
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 most 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(skolems_last).                       % command-line -S 1
clear(skolems_last).    % default clear  % command-line -S 0
Next Section: Interpformat