Index of modules


A
AC
AC redundancy
AC_intf
Declare that the given symbol is AC, and update the Env subsequently by adding clauses, etc.
ActiveSet [ProofState_intf.S]
Arith_int
Cancellative Inferences on Integer Arithmetic
Arith_rat
Cancellative Inferences on Rational Arithmetic
Avatar
Basic Splitting à la Avatar
Avatar_intf
Split a clause into components

B
BBox
BBox (Boolean Box)
BLit [Avatar_intf.S]
Bool_lit
Boolean Literal
Bool_lit_intf
Additional data carried in the literal

C
C [Higher_order.S]
C [Fool.S]
C [Heuristics.S]
C [Arith_rat.S]
C [Arith_int.S]
C [EnumTypes.S]
C [Superposition_intf.S]
C [AC_intf.S]
C [Env_intf.S]
C [ProofState_intf.S]
C [ClauseQueue_intf.S]
CQueue [ProofState_intf.S]
Priority queues on clauses
Case [Cover_set]
Inductive Case
Classify_cst
Classification of Constants
Clause
Clauses
ClauseContext
Clause context
ClauseQueue
Priority Queue of clauses
ClauseQueue_intf
A priority queue of clauses, purely functional
ClauseSet [Clause_intf.S]
Simple set
Clause_intf
Flags
Const
Configuration and Globals
Cover_set
Cover Set
Cst_set [Ind_cst]
Set of constants
Ctx [Env_intf.S]
Ctx [ProofState_intf.S]
Ctx
Basic context for literals, clauses...
Ctx [Clause_intf.S]
Ctx_intf
current ordering on terms
Cut_form
Universally Quantified Conjunction of Clauses

E
E [Avatar_intf.S]
Eligible [Clause_intf.S]
EnumTypes
Inference and simplification rules for "Enum Types"
Env [Higher_order.S]
Env [Fool.S]
Env [Heuristics.S]
Env [Arith_rat.S]
Env [Arith_int.S]
Env [EnumTypes.S]
Env [Superposition_intf.S]
Env [Induction_intf.S]
Env
Global environment for an instance of the prover
Env [AC_intf.S]
Env [Saturate.S]
Env_intf
An inference returns a list of conclusions
Extensions
Dynamic extensions

F
FV_tbl [Cut_form]
Structure for Sets of cut forms, indexed modulo α-eq
Fool
boolean subterms

H
Heuristics
Heuristics
Higher_order
HO

I
Ind_cst
Inductive Constants and Cases
Ind_types
Deal with Inductive Types
Induction
Induction through Cut
Induction_intf
Induction
Infix [Phases]
Infix [SimplM]

K
Key [Phases]
Key [Ctx]
Kind [Proof]

L
Lit [Trail]
Lit [Sat_solver_intf.S]
Lit [BBox]
Lit [Ctx_intf.S]
Loc [Proof]

M
Make [Higher_order]
Make [Fool]
Make [Ind_types]
Make [Heuristics]
Make [Arith_rat]
Make [Arith_int]
Make [EnumTypes]
Make [Rewriting]
Make [Superposition]
Make [Induction]
Make [Avatar]
Make [Sat_solver]
Make [Bool_lit]
Make [Env]
Build a new Environment
Make [AC]
Make [Saturate]
Make [ProofState]
Make [Ctx]
Create a new context
Make [Clause]
Make [ClauseQueue]

P
PS [Heuristics.S]
PS [Arith_rat.S]
PS [Arith_int.S]
PS [Superposition_intf.S]
Params
Parameters for the prover, etc.
Parent [Proof]
PassiveSet [ProofState_intf.S]
Phases
Phases of the Prover
Phases_impl
Implementation of Phases
Pos [Cut_form]
Pos [Clause_intf.S]
Proof
Manipulate proofs
ProofState [Env_intf.S]
ProofState
The state of a proof, contains a set of active clauses (processed), a set of passive clauses (to be processed), and an ordering that is used for redundancy elimination.
ProofState_intf
Set of active clauses

R
Result [Proof]
Rewriting
Rewriting
Rule [Proof]
A rule is a name for some specific inference or transformation rule that is used to deduce formulas from other formulas.

S
S [Proof]
SClause
Simple Clause
Sat_solver
Interface to MSat
Sat_solver_intf
add_clause ~tag ~proof c adds the constraint c to the SAT solver, annotated with proof.
Saturate
Main saturation algorithm.
Selection
Selection functions
Seq [Cut_form]
Seq [Clause_intf.S]
Set [ClauseContext]
Set [Bool_lit_intf.S]
Signals
Useful signals
SimplM
Simplification Monad
SimplSet [ProofState_intf.S]
Solver [Avatar_intf.S]
Step [Proof]
An inference step is composed of a set of premises, a rule, a status (theorem/trivial/equisatisfiable…), and is used to deduce new Proof.result using these premises and metadata.
SubsumptionIndex [ProofState_intf.S]
Superposition
Inference and simplification rules for the superposition calculus
Superposition_intf
Term Indices

T
Tbl [Bool_lit_intf.S]
Tbl [Proof.S]
Tbl [Clause_intf.S]
TermIndex [ProofState_intf.S]
Trail
Boolean Trail

U
UnitIndex [ProofState_intf.S]

W
WeightFun [ClauseQueue_intf.S]
Weight functions
WithPos [Clause_intf.S]
Clause within which a subterm (and its position) are hilighted