Index of types


A
active_simplify_rule [Env_intf.S]
any_phase [Phases]

B
backward_redundant_rule [Env_intf.S]
find redundant clauses in ProofState.ActiveSet w.r.t the clause.
backward_simplify_rule [Env_intf.S]
backward simplification by a unit clause.
binary_inf_rule [Env_intf.S]
bool_lit [Trail]
bool_lit [Proof]

C
case [Cover_set]
check [Proof]
How do we check a step?
clause [Cut_form]
clause [Sat_solver_intf.S]
clause [Clause_intf.S]
clause_conversion_rule [Env_intf.S]
A hook to convert a particular statement into a list of clauses
conversion_result [Env_intf.S]
cst [Cover_set]
cut_res [Avatar_intf.S]
This represents a cut on a formula, where we obtain a list of clauses cut_pos representing the formula itself with the trail lemma, and a boolean literal cut_lit that is true iff the trail is true.

D
decl [EnumTypes.S]
declare_result [EnumTypes.S]

E
env_action [Extensions]
An extension is allowed to modify an environment
env_with_clauses [Phases]
env_with_result [Phases]
errcode [Phases]

F
filename [Phases]
flag [SClause]
flag [Clause_intf.S]
form [Cut_form]
form [Proof]

G
generate_rule [Env_intf.S]
Generation of clauses regardless of current clause.

I
ind_skolem [Ind_cst]
inductive_case [BBox]
inf_rule [Env_intf.S]
An inference returns a list of conclusions
is_trivial_rule [Env_intf.S]
Rule that checks whether the clause is trivial (a tautology)
is_trivial_trail_rule [Env_intf.S]
Rule that checks whether the trail is trivial (a tautology)

K
kind [Proof]
Classification of proof steps

L
lit_rewrite_rule [Env_intf.S]
Rewrite rule on literals

M
multi_simpl_rule [Env_intf.S]
(maybe) rewrite a clause to a set of clauses.

O
or_error [Phases]
or_error [Extensions]

P
packed [Env]
parent [Proof]
payload [Bool_lit_intf.S]
Additional data carried in the literal
payload [BBox]
phase [Phases]
prec_action [Extensions]
Actions that modify the set of rules Compute_prec
printer [Avatar]
profile [ClauseQueue_intf]
profile [ClauseQueue]
proof [Sat_solver_intf]
proof [Clause_intf]
proof [Proof]
Proof Step with its conclusion
proof_step [Sat_solver_intf]
proof_step [Clause_intf]

R
redundant_rule [Env_intf.S]
check whether the clause is redundant w.r.t the set
res [Classify_cst]
result [Sat_solver_intf]
result [Proof]
rule [Proof]
rw_simplify_rule [Env_intf.S]

S
sequence [Proof]
simplify_rule [Env_intf.S]
Simplify the clause structurally (basic simplifications), in the simplification monad.
spec [AC_intf]
spec [AC]
state [Extensions]
state_actions [Extensions]
statement_src [Proof]
stats [Env_intf.S]
statistics on clauses : num active, num passive, num simplification
stats [ProofState_intf.S]
statistics on the state (num active, num passive, num simplification)
step [Proof]
A proof step, without the conclusion
subst [ClauseContext]
szs_status [Saturate]
The SZS status of a state

T
t [Phases]
Monad type, representing an action starting at phase 'p1 and stopping at phase 'p2
t [Cut_form]
A formula of the form forall vars. \bigand_i C_i.
t [Cover_set.Case]
t [Cover_set]
t [Ind_cst]
A ground term of an inductive type.
t [Trail]
t [Bool_lit.PAYLOAD]
t [ClauseContext]
A context is represented as a regular array of literals, containing at least one specific variable x, paired with this variable x.
t [Bool_lit_intf.S]
t [BBox]
t [Params]
t [SimplM]
t [Selection]
t [Proof.S]
t [Proof.Parent]
t [Proof.Step]
t [Proof.Result]
t [Proof.Kind]
t [Proof.Rule]
t [Proof]
t [Extensions]
An extension contains a number of actions that can modify the Flex_state.t during preprocessing, or modify the Env_intf.S once it is built.
t [SClause]
t [ClauseQueue_intf.S.WeightFun]
attribute a weight to a clause.
t [Clause_intf.S.WithPos]
t [Clause_intf.S.Eligible]
Eligibility criterion for a literal
t [Clause_intf.S]
t [ClauseQueue_intf.S]
A priority queue.
term [Fool]
term [EnumTypes]
term [Cut_form]
term [Cover_set]
term [ClauseContext]
term_rewrite_rule [Env_intf.S]
Rewrite rule on terms

U
unary_inf_rule [Env_intf.S]

V
valuation [Trail]
A boolean valuation
var [Cut_form]