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 [Bool_clause]  
C  
case [Cover_set]  
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_form [Cut_form]  
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]  
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)

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]  
parametrized [Selection]  
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

prelude [Phases]  
printer [Avatar]  
profile [ClauseQueue_intf]  
profile [ClauseQueue]  
proof [Sat_solver_intf]  
proof [Clause_intf]  
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]  
rw_simplify_rule [Env_intf.S]  
S  
sets [Clause] 
Bundle of clause sets

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]  
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)

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.FV_tbl]  
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 [Bool_clause]  
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

value [Cut_form.FV_tbl]  
var [Cut_form] 