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
|