Index of types

active_simplify_rule [Env_intf.S]
any_phase [Phases]

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]

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.

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

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

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

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

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)

lit_rewrite_rule [Env_intf.S]
Rewrite rule on literals

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

or_error [Phases]
or_error [Extensions]

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]

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]

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 [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

unary_inf_rule [Env_intf.S]

valuation [Trail]
A boolean valuation
value [Cut_form.FV_tbl]
var [Cut_form]