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