Module Config (.ml)

module Config: sig .. end

configuration for a derivation

Types

type literal = Term.literal

type flags = Flags.flags

type problem = Problem.problem

type config

Functions

Creation

val create : flags:flags ->
       problem:problem ->
       is_horn:bool -> start_time:float -> fof:bool -> theorem:bool -> config

create ~flags ~horn ~equality ~start_time ~fof ~theorem creates a new configuration initialized with flags. The problem is considered to be Horn, if is-horn is true, to contain equality predicates, if contains_equality is true. The time (wall clock) when the derivation was started is given with start_time fof states that the problem is formulated with first-order formulas, theorem that it also contains a conjecture.

val start_time : config -> float

returns the (wall clock) time when the derivation was started.

val is_horn : config -> bool

is the problem (after transformations) horn?

val is_fof : config -> bool

is the original problem fof or cnf?

val is_theorem : config -> bool

for a fof problems, does it contain a conjecture?

val problem : config -> problem

returns the problem clause set to solve.

Options

For an explanation of most of these settings see also module Flags.

val resolve : config -> bool

apply resolve.

val subsume : config -> bool

apply subsume.

val compact : config -> bool

apply compact.

val productivity : config -> bool

only consider productive remainders.

val mixed_literals : config -> bool

allow context literals containing universal and parametric variables.

val finite_domain : config -> bool

search for finite domain models.

val finite_domain_functionality : config -> bool

add functionality axioms for each function symbol in finite domain mode.

e.g, for domain size 3 and the binary function symbol f add:

f(x, y) != 1 \/ f(x, y) != 2

f(x, y) != 2 \/ f(x, y) != 1

f(x, y) != 1 \/ f(x, y) != 3

f(x, y) != 3 \/ f(x, y) != 1

f(x, y) != 2 \/ f(x, y) != 3

f(x, y) != 3 \/ f(x, y) != 2

which in essence is for all domain different elements d, d':

f(x, y) = d => f(x, y) != d'

val lemma : config -> Flags.opt_lemma

compute and store lemmas.

val lemma_min : config -> int

when forgetting lemmas keep at least lemma_min lemmas.

val lemma_max : config -> int

forget lemmas when there are more than lemma_max lemmas.

val lemma_uip : config -> bool

use the UIP in lemma generation as described in Lemma.

val lemma_parametric_assert : config -> int

apply parametric propagation on lemmas/clauses learnt at least n times.

val equality : config -> Flags.opt_equality

how should equality be handled?

val plus_v : config -> bool

should +v be used instead of -v as the initial context literal?

val default_v : config -> literal

returns +v or -v, depending on Config.plus_v.

val backtracking : config -> Flags.opt_backtracking

the chosen backtracking method.

val iterative_deepening : config -> Flags.opt_iterative_deepening

the chosen iterative deepening method.

val deepening_bound : config -> int

the initial bound for the iterative deepening. The current bound is maintained in Bound.bound.

val lookahead_exceeding : config -> bool

apply the close look-ahaed also to Assert candidates exceeding the current deepening bound.

val restart : config -> Flags.opt_restart

the chosen restarting strategy.

val jumping : config -> bool

do jumps in the search space Jumping.

val neg_assert_candidates : config -> Flags.opt_neg_assert_candidates

how to handle negative Assert candidate literals in the Horn case.

val term_indexing : config -> bool

should term indexing be applied for context checks?

val problem_file_name : config -> string

the file name of the problem.

val time_out_CPU : config -> float

system cpu timeout in seconds.

val time_out_WC : config -> float

system cpu timeout in seconds.

Verboseness

val print_level : config -> int

print level.

val print_configuration : config -> bool

print the configuration settings.

val print_equality_axioms : config -> bool

print the added equality axioms, if any.

val print_lemmas : config -> bool

print the lemmas generated and kept over restarts.

val print_finite_domain_axioms : config -> bool

print the axiomation in finite domain mode (Finite_domain).

val print_finite_domain_problem : config -> Flags.opt_print_fd_problem

print the generated problem in finite domain mode (Finite_domain).

val print_statistics : config -> bool

print a statistics after the derivation.

val print_model_context : config -> bool

print a found model as a context.

val print_model_context_file : config -> string

like Config.print_model_context, but to the file with the given name.

val print_model_DIG : config -> bool

print a found model as a DIG.

val print_model_DIG_file : config -> string

like Config.print_model_DIG, but to the file with the given name.

val print_model_finite : config -> bool

print the multiplication tables of a found finite domain model.

val print_model_tptp : config -> bool

print a model in TPTP format

val print_model_tptp_file : config -> string

like Config.print_model_tptp, but to the file with the given name.

val print_derivation_online : config -> bool

print Assert, Split, and Close applications when they are applied during the derivation, plus stuff like the depth bound, backtracking, and restarts.

val print_derivation_context_unifier : config -> bool

print the corresponding context unifier when an application of Assert, Split, or Close is printed.

val print_assert_candidates : config -> bool

print each computed applicable assert candidate.

val print_split_candidates : config -> bool

print each computed applicable split candidate.

Representation

val print : config -> unit

string representation of the configuration (ala Print.print_label).