Prover9 Manual

Version 2009-11A

Prover9 Options

There are three kinds of options:

Flags are Boolean-valued options which can be changed with the set and clear commands, e.g.,
set(clocks).
set(print_given).
Parms are integer-valued options which can be changed with the assign command, e.g.,
assign(max_weight, 30).
Stringparms are string-valued options which can be changed with the assign command, e.g.,
assign(order, kbo).

Option Dependencies

Several of the flags and parameters cause other flags and parameters to be changed. In some cases, that is the only direct effect they have. For example, if you clear(auto), you will see the following in the output.

clear(auto).
    % clear(auto) -> clear(auto_inference).
    % clear(auto_inference) -> clear(predicate_elim).
    % clear(auto_inference) -> assign(eq_defs, pass).
    % clear(auto) -> clear(auto_limits).
    % clear(auto_limits) -> assign(max_weight, 2147483647).
    % clear(auto_limits) -> assign(sos_limit, -1).

The lines starting with "%" are the dependent options that are changed in behalf of clear(auto). Note the sub-dependencies in this example.

The option dependencies can be undone by simply changing the dependent option afterward, as in the following example input.

clear(auto).
set(predicate_elim).

Option Listing

The option names below are links to the sections containing the descriptions.

From Page Clauses and Formulas

set(prolog_style_variables).
clear(prolog_style_variables).    % default clear

From Page Automatic Modes

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

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

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

set(auto_setup).    % default set
clear(auto_setup).

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

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]

set(raw).
clear(raw).    % default clear

From Page Term Ordering

assign(order, string).  % default string=lpo, range [lpo,rpo,kbo]

set(inverse_order).    % default set
clear(inverse_order).

assign(eq_defs, string).  % default string=unfold, range [unfold,fold,pass]

From Page More Search Prep

set(expand_relational_defs).
clear(expand_relational_defs).    % default clear

set(predicate_elim).    % default set
clear(predicate_elim).

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

set(sort_initial_sos).
clear(sort_initial_sos).    % default clear

set(process_initial_sos).    % default set
clear(process_initial_sos).

From Page Search Limits

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

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

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

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

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

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

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

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

From Page Selecting the Given Clause

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

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

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

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

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

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

set(default_parts).      % default set
clear(default_parts).

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

set(lightest_first).
clear(lightest_first).    % default clear

set(breadth_first).
clear(breadth_first).    % default clear

set(random_given).
clear(random_given).    % default clear

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

set(input_sos_first).    % default set
clear(input_sos_first).

From Page Inference Rules

set(binary_resolution).
clear(binary_resolution).    % default clear

set(neg_binary_resolution).
clear(neg_binary_resolution).    % default clear

set(ordered_res).    % default set
clear(ordered_res).

set(check_res_instances).
clear(check_res_instances).    % default clear

assign(literal_selection, string).  % default string=max_negative, range [max_negative, all_negative, none]

set(pos_hyper_resolution).
clear(pos_hyper_resolution).    % default clear

set(hyper_resolution).
clear(hyper_resolution).    % default clear

set(neg_hyper_resolution).
clear(neg_hyper_resolution).    % default clear

set(ur_resolution).
clear(ur_resolution).    % default clear

set(pos_ur_resolution).
clear(pos_ur_resolution).    % default clear

set(neg_ur_resolution).
clear(neg_ur_resolution).    % default clear

set(initial_nuclei).
clear(initial_nuclei).    % default clear

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

set(paramodulation).
clear(paramodulation).    % default clear

set(ordered_para).    % default set
clear(ordered_para).

set(check_para_instances).
clear(check_para_instances).    % default clear

set(para_from_vars).    % default set
clear(para_from_vars).

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

set(para_units_only).
clear(para_units_only).    % default clear

set(basic_paramodulation).
clear(basic_paramodulation).    % default clear

From Page Processing Inferred Clauses

set(lex_order_vars).
clear(lex_order_vars).    % default clear

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

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

set(back_demod).      % default set
clear(back_demod).

set(lex_dep_demod).    % default set
clear(lex_dep_demod).

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

set(lex_dep_demod_sane).    % default set
clear(lex_dep_demod_sane).

set(unit_deletion).
clear(unit_deletion).    % default clear

set(cac_redundancy).    % default set
clear(cac_redundancy).

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

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

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

assign(max_weight, n).  % default n=100, range [INT_MIN .. INT_MAX]

set(safe_unit_conflict).
clear(safe_unit_conflict).    % default clear

set(factor).
clear(factor).    % default clear

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

set(back_subsume).    % default set
clear(back_subsume).

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

From Page Output Files

set(echo_input).    % default set
clear(echo_input).

set(quiet).
clear(quiet).    % default clear

set(print_initial_clauses).    % default set
clear(print_initial_clauses).

set(print_given).    % default set
clear(print_given).

set(print_gen).
clear(print_gen).    % default clear

set(print_kept).
clear(print_kept).    % default clear

set(print_labeled).
clear(print_labeled).    % default clear

set(print_clause_properties).
clear(print_clause_properties).    % default clear

set(print_proofs).    % default set
clear(print_proofs).

set(default_output).    % default set
clear(default_output).

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

assign(stats, string).  % default string=lots, range [none,some,lots,all]

set(clocks).
clear(clocks).    % default clear

set(bell).    % default set
clear(bell).

From Page Weighting

assign(constant_weight, n).  % default n=1, range [INT_MIN .. INT_MAX]

assign(sk_constant_weight, n).  % default n=1, range [INT_MIN .. INT_MAX]

assign(variable_weight, n).  % default n=1, range [INT_MIN .. INT_MAX]

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

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

assign(prop_atom_weight, n).  % default n=1, range [INT_MIN .. INT_MAX]

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

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

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

assign(default_weight, n).  % default n=INT_MAX, range [INT_MIN .. INT_MAX]

From Page Goals and Denials

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

set(reuse_denials).
clear(reuse_denials).    % default clear

set(auto_denials).    % default set
clear(auto_denials).

set(restrict_denials).
clear(restrict_denials).    % default clear

From Page Hints

set(breadth_first_hints).
clear(breadth_first_hints).    % default clear

set(degrade_hints).    % default set
clear(degrade_hints).

set(limit_hint_matchers).
clear(limit_hint_matchers).    % default clear

set(back_demod_hints).    % default set
clear(back_demod_hints).

set(collect_hint_labels).
clear(collect_hint_labels).    % default clear

From Page Semantic Guidance

assign(multiple_interps, string).  % default string=false_in_all, range [false_in_all, false_in_some]

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

Next Section: Glossary