Module Const (.ml)

module Const: sig .. end

exception FOF of bool

FOF theorem is raised if the input is in fof format. theorem is true iff the input contains a conjecture.

exception CLAUSIFIER_RESOURCE_OUT

clausfier ran out of resources.

exception NO_SOLUTION of string

the derivation is aborted because of a limitation of the implementation.

exception PARSE_ERROR

error in the input file.

val debug : bool

compile the (slow) debug version which performs additional consistency checks, i.e. each module may perform additional consistency checks.

val stable_derivation : bool

ensures that independently of all flags the same derivation is produced. disables some optimizations.

val version : string

the current system version, e.g. "Darwin 1.0"

val resolvent_max_size : int

the maximum length of a resolvent computed by Preprocessing_resolution.compute_resolvents.

val resolvents_max_number : int

the maximum number of resolvents computed by Preprocessing_resolution.compute_resolvents.

val max_cached_partial_context_unifiers : int

how many partial context unifiers are explicitely cached in Context_unifier.context_partner.cp_partial_context_unifier?

val max_unprocessed_assert_candidates : int

how many assert candidates (context unifiers) may be stored after being computed before being evaluated? might save on computation if a closing context unifier is found before the candidates need to be evaluated.

val max_assert_candidates : int

how many evaluated assert candidates (context unifiers) may be stored? this is the size of a cache of best candidates, worse candidates are forgotten until needed, then recomputed.

this trades off potential recomputation time for a fixed upper limit on candidate memory usage.

val max_assert_lookahead : int

how many assert candidates (within the current bound) should be stored in the lookahead?

val max_assert_lookahead_exceeding : int

how many assert candidates exceeding the current bound should be stored in the lookahead?

val max_unprocessed_split_candidates : int

like Const.max_unprocessed_assert_candidates for split candidates.

val decay_clause_utility_interval : int

decrease the utility value of clauses and lemmas after each decay_clause_utility backtrack operations.

val decay_clause_utility_ratio : int

divide the clause utility by decay_clause_utility_ratio on decay.

val lemma_max_constraints : int

for lifted lemmas stop the computation of a lemma if more then lemma_max_constraints constraints are generated. just too expensive in general.

val jumping_min_distance : int

a jump must at least skip over this many choice points.

val jumping_check_every_splits : int

Check after each jump_check_every_splits if a jump should be done (also based on the used time and the time limit).

val jumping_time_delta : float

for purposes of determining if a jump should be done the remaining time ration is assumed to be this fraction higher than it actually is (based on the given timeout and the used time).

val fd_static_symmetry_reduction : bool

use static symmetry reduction

for each sort do some static symmetry reduction for constants.

E.g., if the constants are a, b, c, d, and the domain size is 3, then the axioms are:

• a = 1
• b = 1 \/ b = 2
• c = 1 \/ c = 2 \/ c = 3
• d = 1 \/ d = 2 \/ d = 3 \/ more

val fd_use_canonicity : bool

use canonicity axioms in conjunction with static symmetry reduction.

E.g., if the constants are a, b, c, d, and the domain size is 3, then the axioms are: c = 3 -> b = 2 d = 3 -> b = 2 \/ c = 2

val fd_use_term_definitions : bool

use term definitions for flattening of deep terms.

for example,

p(f(g(x), y))

will be transformed into the two clauses

p(s0(x))

and

s0(x, y) = f(g(x), y), where s0 is a fresh skolem symbol.

These are then flattened as usual. The definition term s0(x, y) is reused whenever an instance of f(g(x), y) has to be flattened.

val fd_use_definitions : bool

add definitions for equalities.

for example, after f(a, x) is flattened to x = y <- r_f(z, x), r_a(z) it produces the definition f(z, y) <- a(z).

val fd_use_diff : bool

replace Symbol.equality by -Symbol.diff. as except for the equality axioms all clauses contain only positive equalities, this has the effect that -v unifies less often, and there are less context unifiers in most cases.

val fd_instantiate_totality_axiom : bool

instantiate the total axioms for arities for which only 1 symbol exist.

For example, if f is the only symbol of arity 1, then add the totality axiom r_2(f, x, 1) \/ ... \/ r_2(f, x, n) instead of the more general r_2(z, x, 1) \/ ... \/ r_2(z, x, n)