Automatic Modes

Prover9's automatic mode is set by default. Otter's automatic mode must be explicitly set.

If you simply give Prover9 a set of clauses and/or formulas, Prover9 will look at the clauses and decide which inference rules and clause-processing operations to use. If you don't like the automatic decisions that Prover9 makes, you can clear the flag auto or any of the secondary auto flags that depend on it. Prover9 output files show in detail the effects of changing these flags.

set(auto).    % default set
clear(auto).

This is the basic automatic mode of Prover9. The only direct effect of this flag is that it changes four secondary auto flags as follows.

  set(auto) -> set(auto_inference).
  set(auto) -> set(auto_process).
  set(auto) -> set(auto_limits).
  set(auto) -> set(auto_denials).

  clear(auto) -> clear(auto_inference).
  clear(auto) -> clear(auto_process).
  clear(auto) -> clear(auto_limits).
  clear(auto) -> clear(auto_denials).

Any of the secondary flags, as well as the entire automatic mode can be cleared by the user.

set(auto_inference).    % default set
clear(auto_inference).

If this flag is set, the input clauses are checked for several syntactic properties such as the presence of equality and non-Horn clauses. Based on the results of the checks, Prover9 decides which inference rules to use. In addition, changing this flag causes the following changes.

  set(auto_inference) -> set(predicate_elim).
  set(auto_inference) -> assign(eq_defs, unfold).

  clear(auto_inference) -> clear(predicate_elim).
  clear(auto_inference) -> assign(eq_defs, pass).

set(auto_process).    % default set
clear(auto_process).

This flag causes several other flags that affect clause processing to be altered based syntactic properties of the initial clauses.

If all clauses are Horn and there are negative nonunits, the flag back_unit_deletion is automatically set. If there are non-Horn clauses, the flags back_unit_deletion and factor are automatically set.

Unlike ordinary option dependencies, the options that are changed by auto_process cannot be undone by placing commands in the input file, because they depend on the structure of the clauses.

set(auto_limits).    % default set
clear(auto_limits).

The only effect of changing this flag is that two parameters are changed in the following ways.

  set(auto_limits) -> assign(max_weight, 100).
  set(auto_limits) -> assign(sos_limit, 10000).

  clear(auto_limits) -> assign(max_weight, INT_MAX).
  clear(auto_limits) -> assign(sos_limit, -1).

An Experimental Automatic Mode

set(auto2).
clear(auto2).    % default clear

assign(lrs_ticks, n).  % default n=-1, range [-1 .. INT_MAX]

assign(lrs_interval, n).  % default n=50, range [1 .. INT_MAX]

assign(min_sos_limit, n).  % default n=0, range [0 .. INT_MAX]

These three parameters work together and are used to automatically adjust the parameter sos_limit by means of a "limited resource strategy" [RV-lrs]. If lrs_ticks ≥ 0, the method is applied.

This is an experimental feature and is not recommended for general use.