Index of values

( ** ) [Clause_intf.S.Eligible]
Logical "and"
(++) [Clause_intf.S.Eligible]
Logical "or"
(>>=) [Phases.Infix]
(>>=) [SimplM.Infix]
(>>=) [SimplM]
Monadic bind
(>>?=) [Phases.Infix]
(>|=) [Phases.Infix]
(>|=) [SimplM.Infix]
(~~) [Clause_intf.S.Eligible]
Logical "not"

abs [Bool_lit_intf.S]
Literal without its sign
adapt [SClause]
add [Cut_form.FV_tbl]
add [Trail]
add [AC_intf.S]
Declare that the given symbol is AC, and update the Env subsequently by adding clauses, etc.
add [ProofState_intf.S.CLAUSE_SET]
Add clauses to the set
add [ClauseQueue_intf.S]
Add a clause to the Queue
add_active [Env_intf.S]
Add active clauses
add_active_simplify [Env_intf.S]
Add simplification w.r.t active set
add_backward_redundant [Env_intf.S]
Add rule that finds redundant clauses within active set
add_backward_simplify [Env_intf.S]
Add simplification of the active set
add_basic_simplify [Env_intf.S]
Add basic simplification rule
add_binary_inf [Env_intf.S]
Add a binary inference rule
add_clause [Sat_solver_intf.S]
add_clause ~tag ~proof c adds the constraint c to the SAT solver, annotated with proof.
add_clause_conversion [Env_intf.S]
add_clause_seq [Sat_solver_intf.S]
add_clauses [Sat_solver_intf.S]
add_from_hook [Ctx_intf.S.Lit]
add_generate [Env_intf.S]
add_imply [Avatar_intf.S]
add_imply l res means that the conjunction of lemmas in l implies that the lemma res is proven
add_is_trivial [Env_intf.S]
Add tautology detection rule
add_is_trivial_trail [Env_intf.S]
Add tautology detection rule
add_lemma [Avatar_intf.S]
Add the given cut to the list of lemmas.
add_list [Trail]
add_lit_rule [Env_intf.S]
Add a literal rewrite rule
add_multi_simpl_rule [Env_intf.S]
Add a multi-clause simplification rule
add_opt [Params]
add_opts [Params]
add_passive [Env_intf.S]
Add passive clauses
add_prove_lemma [Avatar_intf.S]
Add a mean of proving lemmas
add_redundant [Env_intf.S]
Add redundancy criterion w.r.t.
add_rewrite_rule [Env_intf.S]
Add a term rewrite rule
add_rw_simplify [Env_intf.S]
Add forward rewriting rule
add_seq [ClauseQueue_intf.S]
Add clauses to the queue
add_signature [Ctx_intf.S]
Merge the given signature with the context's one
add_simpl [Env_intf.S]
Add simplification clauses
add_step_init [Env_intf.S]
add a function to call before each saturation step
add_to_hook [Ctx_intf.S.Lit]
add_unary_inf [Env_intf.S]
Add a unary inference rule
add_unary_simplify [Env_intf.S]
Add unary simplification rule (not dependent on proof state)
after_check_sat [Avatar_intf.S]
all [Selection]
available names for selection functions
all_proved [Sat_solver_intf.S]
Set of (signed) proved literals
all_simplify [Env_intf.S]
Use all simplification rules to convert a clause into a set of maximally simplified clause (or [] if they are all trivial).
almost_bfs [ClauseQueue_intf.S]
Half FIFO, half default
always [Clause_intf.S.Eligible]
All literals
app_list [SimplM]
apply [ClauseContext]
apply c t fills the hole of c with the given term t.
apply_same_scope [ClauseContext]
Same as ClauseContext.apply, but now variables from the context and variables from the term live in the same scope
apply_sign [Bool_lit_intf.S]
apply_sign s lit is lit if s, neg lit otherwise
apply_subst [Cut_form]
are_variant [Cut_form]
Are these two cut formulas alpha-equivalent?
arith [Clause_intf.S.Eligible]
as_case [BBox]
If payload t = Case p, then return Some p, else return None
as_lemma [BBox]
at [Cut_form.Pos]
Return the subterm at the given position, or
at [Clause_intf.S.Pos]

backward_simplify [Env_intf.S]
Perform backward simplification with the given clause.
basic_simplify [Superposition_intf.S]
basic simplifications (remove duplicate literals, trivial literals, destructive equality resolution...)
basic_simplify [Env_intf.S]
Basic (and fast) simplifications
before_check_sat [Avatar_intf.S]
bfs [ClauseQueue_intf.S]
bind [Phases]
bind state f calls f to go one step further from state
by_name [Extensions]
Get an extension by its name, if any

canc_div_case_switch [Arith_int.S]
Eliminate negative divisibility literals within a power-of-prime quotient of Z: not (d^i | m) ----->
canc_div_chaining [Arith_int.S]
Chain together two divisibility literals, assuming they share the same prime
canc_div_prime_decomposition [Arith_int.S]
Eliminate divisibility literals with a non-power-of-prime quotient of Z (for instance 6 | a ---> { 2 | a, 3 | a })
canc_divisibility [Arith_int.S]
Infer divisibility constraints from integer equations, for instace C or 2a=b ----> C or 2 | b if a is maximal
canc_equality_factoring [Arith_int.S]
cancellative equality factoring
canc_ineq_chaining [Arith_int.S]
cancellative inequality chaining.
canc_ineq_factoring [Arith_int.S]
Factoring between two inequation literals
canc_less_to_lesseq [Arith_int.S]
Simplification: a < b ----> a+1 ≤ b
canc_sup_active [Arith_int.S]
cancellative superposition where given clause is active
canc_sup_passive [Arith_int.S]
cancellative superposition where given clause is passive
cancellation [Arith_int.S]
cancellation (unifies some terms on both sides of a comparison operator)
case_switch_limit [Arith_int]
Positive integer: maximum width of an inequality case switch.
cases [Cover_set]
Cases of the cover set
check [Phases_impl]
check [Sat_solver_intf.S]
Is the current problem satisfiable?
check [Params]
check_empty [Avatar_intf.S]
Forbid empty clauses with trails, i.e.
check_satisfiability [Avatar_intf.S]
Checks that the SAT context is still valid
check_timeout [Saturate]
check whether we still have some time w.r.t timeout
classify [Classify_cst]
classify id returns the role id plays in inductive reasoning
clause_at [Cut_form.Pos]
Lookup which clause the position is about, return it and the rest of the position.
clauses [ProofState_intf.S.PassiveSet]
Current set of clauses
clauses [ProofState_intf.S.ActiveSet]
Current set of clauses
combine [ClauseQueue_intf.S.WeightFun]
Combine a list of pairs w, coeff where w is a weight function, and coeff a strictly positive number.
combine [Clause_intf.S.Eligible]
Logical "and" of the given eligibility criteria.
comes_from_goal [Clause_intf.S]
true iff the clause is (indirectly) deduced from a goal or lemma
compare [Cover_set.Case]
compare [Ind_cst]
compare [Trail]
compare [ClauseContext]
compare [Bool_lit_intf.S]
compare [SClause]
compare [Clause_intf.S.WithPos]
compare [Ctx_intf.S]
Compare two terms
compare [Clause_intf.S]
condensation [Superposition_intf.S]
contextual_literal_cutting [Superposition_intf.S]
contexual Literal.t cutting of the given clause by the active set
convert_input_statements [Env_intf.S]
Convert raw input statements into clauses, triggering Env_intf.S.on_input_statement
convert_lemma [Avatar_intf.S]
Intercepts input lemmas and converts them into clauses.
cr_add [Env_intf.S]
cr_return [Env_intf.S]
cr_skip [Env_intf.S]
create [Cut_form.FV_tbl]
create [Clause_intf.S]
Build a new clause from the given literals.
create_a [Clause_intf.S]
Build a new clause from the given literals.
cs [Cut_form]
cur_phase [Phases.Key]
The current phase is stored in the state using this key
current_phase [Phases]
Get the current phase
cut_depth [Avatar_intf.S]
cut_form [Avatar_intf.S]
cut_lit [Avatar_intf.S]
cut_pos [Avatar_intf.S]
cut_proof [Avatar_intf.S]
cut_proof_parent [Avatar_intf.S]
cut_res_clauses [Avatar_intf.S]

debug [ProofState_intf.S]
debug functions: much more detailed printing
declarations [Cover_set]
declarations set returns a list of type declarations that should be made if set is new (declare the top cst and its subcases)
declare [Ctx_intf.S]
Declare the type of a symbol (updates signature)
declare_ty [EnumTypes.S]
Declare that the domain of the type ty_id is restricted to given list of cases, in the form forall var. Or_{c in cases} var = c.
def_as_rewrite [Params]
default [Selection]
Default selection function
default [Extensions]
Default extension.
default [ClauseQueue_intf.S.WeightFun]
Use Literal.heuristic_weight
default [ClauseQueue_intf.S]
Obtain the default queue
depth [Ind_cst]
distance_to_goal [Clause_intf.S]
See Proof.distance_to_goal, applied to the clause's proof
div_case_switch_limit [Arith_int]
Positive integer: maximum prime number suitable for div_case_switch (ie maximum n for enumeration of cases in n^k | x)
do_binary_inferences [Env_intf.S]
do binary inferences that involve the given clause
do_generate [Env_intf.S]
do generating inferences
do_unary_inferences [Env_intf.S]
do unary inferences for the given clause
dominates [Ind_cst]
dominates c1 c2 if depth c1 < depth c2.
dot_all_roots [Params]
dot_file [Params]
dot_llproof [Params]
dot_sat [Params]
dummy [Bool_lit.PAYLOAD]
dummy [Bool_lit_intf.S]
Value that should not be used
dummy [BBox]

eligible_param [Clause_intf.S]
Bitvector that indicates which of the literals of subst(clause) are eligible for paramodulation.
eligible_res [Clause_intf.S]
Bitvector that indicates which of the literals of subst(clause) are eligible for resolution.
eligible_res_no_subst [Clause_intf.S]
More efficient version of Clause_intf.S.eligible_res with Subst.empty
eliminate_unshielded [Arith_int.S]
Eliminate unshielded variables using an adaptation of Cooper's algorithm
empty [Trail]
empty_state [Phases]
enable_depth_limit [Heuristics]
Set a maximal depth for terms.
eq [Clause_intf.S.Eligible]
eq_subsumes [Superposition_intf.S]
equality subsumption
equal [Cover_set.Case]
equal [Ind_cst]
equal [Trail]
equal [ClauseContext]
equal [Bool_lit_intf.S]
equal [SClause]
except_RR_horn [Selection]
except_RR_horn p behaves like p, except if the clause is a range-restricted Horn clause.
exists [Trail]
exists_ac [AC_intf.S]
Is there any AC symbol?
exit [Phases]
expand_def [Params]
explore [ClauseQueue_intf.S]
Use heuristics for selecting "small" clauses
extension [Higher_order]
extension [Fool]
extension [Ind_types]
extension [Heuristics]
extension [Arith_rat]
extension [Arith_int]
extension [EnumTypes]
extension [Rewriting]
extension [Superposition]
extension [Induction]
extension [Avatar]
Extension that enables Avatar splitting and create a new SAT-solver.
extension [AC]
extensions [Extensions]
All currently available extensions
extract [ClauseContext]
extract lits t returns None if t doesn't occur in lits.
extract_exn [ClauseContext]
Unsafe version of ClauseContext.extract.

fail [Phases]
Fail with the given error message
favor_all_neg [ClauseQueue_intf.S.WeightFun]
Favor clauses with only negative ground lits
favor_goal [ClauseQueue_intf.S.WeightFun]
The closest a clause is from the initial goal, the lowest its weight.
favor_ground [ClauseQueue_intf.S.WeightFun]
favor_horn [ClauseQueue_intf.S.WeightFun]
favor_non_all_neg [ClauseQueue_intf.S.WeightFun]
Favor clauses that have at least one non-(ground negative) lit
files [Params]
filter [Trail]
Only keep a subset of boolean literals
filter [Clause_intf.S.Eligible]
filter_absurd_trails [Avatar_intf.S]
filter_trails f calls f on every trail associated with the empty clause.
find_ind_skolems [Ind_cst]
find_ind_skolem term searches subterms of term for constants that are of an inductive type and that are skolems or (already) inductive constants.
find_proof [AC_intf.S]
Recover the proof for the AC-property of this symbol.
find_signature [Ctx_intf.S]
Find the type of the given symbol
find_signature_exn [Ctx_intf.S]
Unsafe version of Ctx_intf.S.find_signature.
flag_backward_simplified [SClause]
clause has been backward simplified
flag_cut_introduced [Avatar]
flag_lemma [SClause]
clause is a lemma
flag_persistent [SClause]
clause cannot be redundant
flag_redundant [SClause]
clause has been shown to be redundant
flex_add [Env_intf.S]
add k -> v to the flex state
flex_get [Env_intf.S]
flex_get k is the same as Flex_state.get_exn k (flex_state ()).
flex_state [Env_intf.S]
State inherited from configuration
fold [Trail]
fold_l [Phases]
fold_l [SimplM]
for_all [Trail]
forward_simplify [Env_intf.S]
Simplify the clause w.r.t to the active set and experts
fresh_id [Bool_lit_intf.S]
Make a fresh ID.
from_hooks [Ctx_intf.S.Lit]
from_string [Selection]
selection function from string (may fail)

generate [Env_intf.S]
Perform all generating inferences
get [Phases]
get [Cut_form.FV_tbl]
get [SimplM]
get_active [Env_intf.S]
Active clauses
get_empty_clauses [Env_intf.S]
Set of known empty clauses
get_env [Avatar]
get_flag [SClause]
get value of boolean flag
get_flag [Clause_intf.S]
get value of boolean flag
get_key [Phases]
get_key k returns the value associated with k in the state
get_passive [Env_intf.S]
Passive clauses
get_profile [ClauseQueue]
get_proof [Sat_solver_intf.S]
Return a proof of false, assuming Sat_solver_intf.S.check returned Unsat.
get_proof_of_lit [Sat_solver_intf.S]
get_proof_of_lit lit returns the proof of lit, assuming it has been proved true at level 0 (see Sat_solver_intf.S.valuation_level)
get_proof_opt [Sat_solver_intf.S]
Obtain the proof, if any
get_some_empty_clause [Env_intf.S]
Some empty clause, if present, otherwise None
given_clause [Saturate.S]
run the given clause until a timeout occurs or a result is found.
given_clause_step [Saturate.S]
Perform one step of the given clause algorithm.
goal_oriented [ClauseQueue_intf.S]
custom weight function that favors clauses that are "close" to initial conjectures.
ground [ClauseQueue_intf.S]
Favor positive unit clauses and ground clauses

handle_distinct_constants [Superposition_intf.S]
Decide on "quoted" "symbols" (which are all distinct)
has_empty_clause [Env_intf.S]
Is there an empty clause?
has_selected_lits [Clause_intf.S]
does the clause have some selected literals?
has_trail [Clause_intf.S]
Has a non-empty trail?
hash [Cover_set.Case]
hash [Ind_cst]
hash [Trail]
hash [ClauseContext]
hash [Bool_lit_intf.S]
hash [SClause]
home [Const]

id [Ind_cst]
id [SClause]
id [Clause_intf.S]
id_as_cst [Ind_cst]
id_as_cst_exn [Ind_cst]
Unsafe version of as_cst
id_is_cst [Ind_cst]
Check whether the given constant is an inductive constant
id_is_cstor [Classify_cst]
id_is_defined [Classify_cst]
id_is_ind_skolem [Ind_cst]
id_is_potential_cst id ty returns true if id:ty is a skolem constant of an inductive type, or if it is already an inductive constant.
id_is_projector [Classify_cst]
id_is_sub [Ind_cst]
idx_fv [Superposition_intf.S]
index for subsumption
idx_sup_from [Superposition_intf.S]
index for superposition from the set
idx_sup_into [Superposition_intf.S]
index for superposition into the set
ind_skolem_compare [Ind_cst]
ind_skolem_depth [Ind_cst]
depth of the skolem (0 if not an inductive constant)
ind_skolem_equal [Ind_cst]
ind_vars [Cut_form]
subset of Cut_form.vars that have an inductive type
infer_active [Superposition_intf.S]
superposition where given clause is active
infer_equality_factoring [Superposition_intf.S]
infer_equality_resolution [Superposition_intf.S]
infer_passive [Superposition_intf.S]
superposition where given clause is passive
inject_case [BBox]
Inject cst = case
inject_lemma [BBox]
Make a new literal from this formula that we are going to cut on.
inject_lits [BBox]
Inject a clause into a boolean literal.
instantiate_vars [EnumTypes.S]
Instantiate variables whose type is a known enumerated type, with all cases of this type.
introduce_cut [Avatar_intf.S]
Introduce a cut on the given clause(s).
is_ac [AC_intf.S]
is_active [Trail]
Trail.is_active t ~v is true iff all boolean literals in t are satisfied in the boolean valuation v.
is_active [Env_intf.S]
Is the clause in the active set
is_active [Clause_intf.S]
True if the clause's trail is active in this valuation
is_backward_simplified [SClause]
is_backward_simplified [Clause_intf.S]
is_base [Cover_set.Case]
is_case [BBox]
is_completeness_preserved [Ctx_intf.S]
Check whether completeness was preserved so far
is_eligible_param [Clause_intf.S]
Check whether the idx-th literal is eligible for paramodulation
is_empty [Trail]
Empty trail?
is_empty [SClause]
is_empty [Clause_intf.S]
Is the clause an empty clause?
is_empty [ClauseQueue_intf.S]
check whether the queue is empty
is_goal [Clause_intf.S]
Looking at the clause's proof, return true iff the clause is an initial (negated) goal from the problem
is_ground [Clause_intf.S]
is_lemma [BBox]
returns true if the bool literal represents a lemma
is_maxlit [Clause_intf.S]
Is the i-th literal maximal in subst(clause)? Equivalent to Bitvector.get (maxlits ~ord c subst) i
is_new [SimplM]
is_oriented_rule [Clause_intf.S]
Is the clause a positive oriented clause?
is_passive [Env_intf.S]
Is the clause a passive clause?
is_rec [Cover_set.Case]
is_redundant [Env_intf.S]
Is the given clause redundant w.r.t the active set?
is_redundant [SClause]
is_redundant [Clause_intf.S]
is_same [SimplM]
is_selected [Clause_intf.S]
check whether a literal is selected
is_semantic_tautology [Superposition_intf.S]
semantic tautology deletion, using a congruence closure algorithm to see if negative literals imply some positive Literal.t
is_sub [Ind_cst]
Is the constant a sub-constant (i.e.
is_tautology [Arith_int.S]
is the clause a tautology w.r.t linear expressions?
is_tautology [Superposition_intf.S]
Check whether the clause is a (syntactic) tautology, ie whether it contains true or "A" and "not A"
is_trivial [Trail]
returns true iff the trail contains both i and -i.
is_trivial [AC_intf.S]
Check whether the clause is AC-trivial
is_trivial [Env_intf.S]
Check whether the clause is trivial
is_trivial_lit [AC_intf.S]
Is the literal AC-trivial?
is_trivial_trail [Env_intf.S]
Check whether the trail is trivial
is_unit_clause [Clause_intf.S]
is the clause a unit clause?

k_avatar [Avatar]
k_simplify_trail [Avatar]
key [Superposition]
key to access the Env.flex_state.
key [Params]
key_ac [AC]

labels [Trail]
last_result [Sat_solver_intf.S]
Last computed result.
length [Trail]
length [SClause]
length [Clause_intf.S]
Number of literals
length [ClauseQueue_intf.S]
Number of elements
lit_at [Cut_form.Pos]
Lookup which literal the position is about, return it and the rest of the position.
lits [SClause]
lits [Clause_intf.S.Seq]
lits [Clause_intf.S]
load_extensions [Phases_impl]
lost_completeness [Ctx.Key]
lost_completeness [Ctx_intf.S]
To be called when completeness is not preserved

make [Cut_form]
make [Cover_set]
Build a cover set for the given type.
make [Ind_cst]
Make a new constant of the given type
make [ClauseContext]
Make a context from a var and literals containing this var.
make [Bool_lit_intf.S]
Make a fresh literal with the given payload
make [SClause]
make [ClauseQueue_intf.S]
Bring your own implementation of queue.
make_skolem [Ind_cst]
map [Phases]
Map the current value
map [Trail]
map [SimplM]
map_l [SimplM]
mark_backward_simplified [SClause]
mark_backward_simplified [Clause_intf.S]
mark_redundant [SClause]
mark_redundant [Clause_intf.S]
max [Clause_intf.S.Eligible]
Maximal literals of the clause
max_goal [Selection]
Select a maximal negative literal, if any, or nothing
maxlits [Clause_intf.S]
List of maximal literals
mem [Cut_form.FV_tbl]
mem [Trail]
merge [Trail]
Merge several trails (e.g.
merge_l [Trail]
Merge several trails (e.g.
mk_proof_res [Bool_clause]
mk_proof_res [SClause]
multi_simplify [Env_intf.S]
Can we simplify the clause into a List of simplified clauses?
must_be_kept [BBox]
must_be_kept lit means that lit should survive in boolean splitting, that is, that if C <- lit, Gamma then any clause derived from C recursively will have lit in its trail.

name [ClauseQueue_intf.S]
Name of the implementation/role of the queue
names [Extensions]
Names of loaded extensions
neg [Bool_lit_intf.S]
Negate the boolean literal
neg [Clause_intf.S.Eligible]
Only negative literals
new_flag [SClause]
new flag that can be used on clauses
next [ProofState_intf.S.PassiveSet]
Get-and-remove the next passive clause to process
next_passive [Env_intf.S]
Extract next passive clause
no_select [Selection]
Never select literals.
norm [Bool_lit_intf.S]
norm l = abs l, not (sign l)
normalize [Cut_form]
Use rewriting to normalize the formula
num_clauses [ProofState_intf.S.PassiveSet]
num_clauses [ProofState_intf.S.ActiveSet]

of_form [Ctx_intf.S.Lit]
of_forms [Clause_intf.S]
Directly from list of formulas
of_forms_axiom [Clause_intf.S]
Construction from formulas as axiom (initial clause)
of_list [Trail]
of_profile [ClauseQueue_intf.S]
Select the queue corresponding to the given profile
of_sclause [Clause_intf.S]
of_statement [Clause_intf.S]
Extract a clause from a statement, if any
on_add [AC_intf.S]
on_add_clause [ProofState_intf.S.CLAUSE_SET]
signal triggered when a clause is added to the set
on_empty_clause [Env_intf.S]
Signal triggered when an empty clause is found
on_input_lemma [Avatar_intf.S]
Triggered every time a cut is introduced for an input lemma (i.e.
on_input_statement [Env_intf.S]
Triggered on every input statement
on_lemma [Avatar_intf.S]
Triggered every time a cut is introduced, by any means.
on_new_cst [Ind_cst]
Triggered with new inductive constants
on_new_symbol [Ctx_intf.S]
on_remove_clause [ProofState_intf.S.CLAUSE_SET]
signal triggered when a clause is removed from the set
on_signature_update [Ctx_intf.S]
on_start [Env_intf.S]
Triggered before starting saturation
ord [Params]
ord [Env_intf.S]
ord [Ctx_intf.S]
current ordering on terms

param [Clause_intf.S.Eligible]
Only literals that are eligible for paramodulation
params [Env_intf.S]
parse_args [Params]
parse_args returns parameters
parse_cli [Phases_impl]
Parses the file list and parameters, also puts the parameters in the state
payload [Bool_lit_intf.S]
Obtain the payload
payload [BBox]
Obtain the payload of this boolean literal, that is, what the literal represents
penalty [ClauseQueue_intf.S.WeightFun]
Returns the penalty of the clause
penalty [Clause_intf.S]
pos [Clause_intf.S.Eligible]
Only positive literals
pp [Cover_set.Case]
pp [Cover_set]
pp [Ind_cst]
pp [ClauseContext]
pp [Bool_lit_intf.S]
pp [BBox]
pp [Env_intf.S]
pp [ProofState_intf.S]
pretty print the content of the state
pp [SClause]
pp [Clause_intf.S.WithPos]
pp [Clause_intf.S]
pp [ClauseQueue_intf.S]
pp_bclause [BBox]
pp_cut_res [Avatar_intf.S]
pp_decl [EnumTypes.S]
pp_full [Env_intf.S]
pp_in [SClause]
pp_payload [BBox]
pp_res [Classify_cst]
pp_set [Clause_intf.S]
pp_set_tstp [Clause_intf.S]
pp_signature [Classify_cst]
Print classification of signature
pp_trail [SClause]
pp_trail [Clause_intf.S]
Printer for boolean trails, that uses Clause_intf.S.Ctx to display boxes
pp_trail_tstp [SClause]
pp_tstp [Cut_form]
pp_tstp [BBox]
pp_tstp [SClause]
pp_tstp [Clause_intf.S]
pp_tstp_full [SClause]
Print in a toplevel TPTP statement
pp_tstp_full [Clause_intf.S]
Print in a cnf() statement
pp_vars [SClause]
pp_zf [Cut_form]
pp_zf [BBox]
pp_zf [SClause]
prec_constr [Classify_cst]
Partial order on ID.t, with: regular > constant > sub_constant > cstor
precedence [Env_intf.S]
prelude [Params]
presaturate [Params]
presaturate [Saturate.S]
Interreduction of the given state, without generating inferences.
print [Phases_impl]
Printing of results
print_lemmas [Avatar_intf.S]
print the current list of lemmas, and their status
print_stats [Phases_impl]
process_file [Phases_impl]
process_file f parses f, does the preprocessing phases, including type inference, choice of precedence, ordering, etc.
process_files_and_print [Phases_impl]
Process each file in the list successively, printing the results.
profile_of_string [ClauseQueue]
proof [Clause_intf.S]
Obtain the pair conclusion, step
proof_parent [Clause_intf.S]
proof_parent_subst [Clause_intf.S]
proof_res_as_bc [Bool_clause]
proof_step [Clause_intf.S]
Extract its proof from the clause
proof_tc [Bool_clause]
proof_tc [SClause]
proved_at_0 [Sat_solver_intf.S]
If the literal has been propagated at decision level 0, return its value (which does not depend on the model).

queue [ProofState_intf.S.PassiveSet]
Current state of the clause queue

raw_lits [ClauseContext]
give access to the underlying literals.
register [Heuristics.S]
register [Arith_rat.S]
register [Arith_int.S]
register [Superposition_intf.S]
Register rules in the environment
register [Superposition]
Register the superposition module to its Environment's mixtbl.
register [Induction_intf.S]
Register the inference rules for inductive reasoning
register [Avatar_intf.S]
Register inference rules to the environment
register [Extensions]
Register an extension to the (current) prover.
remove [Trail]
remove [ProofState_intf.S.CLAUSE_SET]
Remove clauses from the set
remove_active [Env_intf.S]
Remove active clauses
remove_passive [Env_intf.S]
Remove passive clauses
remove_simpl [Env_intf.S]
Remove simplification clauses
renaming [Ctx_intf.S]
replace [Cut_form.Pos]
In-place modification of the array, in which the subterm at given position is replaced by the by term.
replace_many [Cut_form.Pos]
In-place modification of the array, in which the subterm at given position is replaced by the by term.
res [Clause_intf.S.Eligible]
Only literals that are eligible for resolution
return [Phases]
Return a value into the monad
return [SimplM]
return_err [Phases]
return_new [SimplM]
return_opt [SimplM]
return_opt ~old t returns return_new u if t=Some u, else returns same old.
return_phase [Phases]
Finish the given phase
return_phase_err [Phases]
return_same [SimplM]
run [Phases]
run m is run_with empty_state m
run_parallel [Phases]
run_sequentiel l runs each action of the list in succession, restarting every time with the initial state (once an action has finished, its state is discarded).
run_with [Phases]
run_with state m executes the actions in m starting with state, returning some value (or error) and the final state.

same_cst [Cover_set.Case]
true iff the two cases are on the same constant
same_type [Ind_cst]
Do these two inductive constants have the same type?
scan_statement [AC_intf.S]
Check whether the statement contains an "AC" attribute, do the proper declaration in this case
section [Superposition]
section [BBox]
section [Const]
seed [Params]
select [Params]
select [Ctx.PARAMETERS]
select [Ctx_intf.S]
selected_lits [Clause_intf.S]
get the list of selected literals
selection_fun [Ctx_intf.S]
selection function for clauses
set [Phases]
set_compact [Sat_solver]
Toggle compact proofs.
set_flag [SClause]
set boolean flag
set_flag [Clause_intf.S]
set boolean flag
set_key [Phases]
set_ord [Ctx_intf.S]
set_printer [Sat_solver_intf.S]
How to print literals?
set_profile [ClauseQueue]
set_selection_fun [Ctx_intf.S]
set_sign [Bool_lit_intf.S]
Set the sign of the literal to the given boolean
setup [Higher_order.S]
Register rules in the environment
setup [Fool.S]
Register rules in the environment
setup [Ind_types.Make]
setup [EnumTypes.S]
Register rules in the environment
setup [Rewriting.Make]
setup [Sat_solver_intf.S]
setup [AC_intf.S]
Register on Env
setup_gc [Phases_impl]
setup_signal [Phases_impl]
sign [Bool_lit_intf.S]
Current sign of the literal (positive or negative)
signature [Env_intf.S]
signature [Ctx.PARAMETERS]
signature [Ctx_intf.S]
Current signature
simplify [AC_intf.S]
Simplify the clause modulo AC
simplify_active_with [Env_intf.S]
Can be called when a simplification relation becomes stronger, with the strengthened relation.
singleton [Trail]
skolems [Cover_set.Case]
split [Avatar_intf.S]
Split a clause into components
start_phase [Phases]
Start the given phase
stat_clause_create [Clause]
stats [Env_intf.S]
Compute stats
stats [ProofState_intf.S]
Compute statistics
step_init [Env_intf.S]
call all functions registered with Env_intf.S.add_step_init
steps [Params]
string_of_any_phase [Phases]
string_of_phase [Phases]
sub_constants [Cover_set.Case]
All sub-constants that are subterms of a specific case
sub_constants [Cover_set]
All sub-constants of a given inductive constant
subst1 [Cut_form]
Substitution of one variable
subsumed_by [Env_intf.S]
List of active clauses subsumed by the given clause
subsumed_by_active_set [Superposition_intf.S]
check whether the clause is subsumed by any clause in the set
subsumed_in_active_set [Superposition_intf.S]
list of clauses in the active set that are subsumed by the clause
subsumes [Superposition_intf.S]
subsumes c1 c2 iff c1 subsumes c2
subsumes [Trail]
subsumes a b is true iff a is a subset of b
subsumes_with [Superposition_intf.S]
returns subsuming subst if the first clause subsumes the second one
symbols [AC_intf.S]
set of AC symbols
symbols [Clause_intf.S]
symbols that occur in the clause
symbols_of_terms [AC_intf.S]
set of AC symbols occurring in the given term

take_first [ClauseQueue_intf.S]
Take first element of the queue, or raise Not_found
terms [Cut_form.Seq]
terms [Clause_intf.S.Seq]
terms_with_pos [Cut_form.Seq]
timeout [Params]
to_form [Ctx_intf.S.Lit]
to_forms [Clause_intf.S]
Easy iteration on an abstract view of literals
to_hooks [Ctx_intf.S.Lit]
to_int [Bool_lit_intf.S]
to_list [Trail]
to_lit [Cover_set.Case]
to_s_form [Cut_form]
Convert to input formula
to_s_form [Trail]
to_s_form [BBox]
to_s_form [SClause]
to_s_form [Clause_intf.S]
to_sclause [Clause_intf.S]
to_seq [Cut_form.FV_tbl]
to_seq [Trail]
to_string [Clause_intf.S]
Debug printing to a string
to_string [ClauseQueue_intf.S]
to_term [Cover_set.Case]
to_term [Ind_cst]
top [Cover_set]
top constant of the coverset
trail [SClause]
trail [Clause_intf.S]
Get the clause's trail
trail_l [Clause_intf.S]
Merge the trails of several clauses
trail_subsumes [Clause_intf.S]
trail_subsumes c1 c2 = Trail.subsumes (get_trail c1) (get_trail c2)
trivial [Cut_form]
trivial [ClauseContext]
Trivial context, that contains 0 holes.
ty [Cover_set]
ty [Ind_cst]

unary_depth [Params]
unary_simplify [Env_intf.S]
Simplify the clause.
update [Phases]
update ~f changes the state using f
update_flex_state [Env_intf.S]
update_flex_state f changes flex_state () using f
update_proof [Clause_intf.S]
update_proof c f creates a new clause that is similar to c in all aspects, but with the proof f (proof_step c)
update_trail [SClause]
update_trail [Clause_intf.S]
Change the trail.

valuation [Sat_solver_intf.S]
Assuming the last call to Sat_solver_intf.S.check returned Sat, get the boolean valuation for this (positive) literal in the current model.
valuation_level [Sat_solver_intf.S]
Gives the value of a literal in the model, as well as its decision level.
vars [Cut_form]
vars [Clause_intf.S.Seq]
version [Params]
version [Const]

weight [Clause_intf.S]
weight_fun [Classify_cst]
with_phase [Phases]
Start phase, call f () to get the result, return its result using Phases.return_phase
with_phase1 [Phases]
with_phase2 [Phases]