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] | |
| ArithInt |
Cancellative Inferences on Integer Arithmetic
|
| ArithLit |
Arithmetic Literal
|
| 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 [MetaProverState_intf.S] | |
| C [Heuristics.S] | |
| C [ArithInt.S] | |
| C [EnumTypes.S] | |
| C [Superposition.S] | |
| C [AC_intf.S] | |
| C [Env_intf.S] | |
| C [ProofState_intf.S] | |
| C [ClauseQueue_intf.S] | |
| CHashtbl [Clause_intf.S] | |
| CQueue [ProofState_intf.S] |
Priority queues on clauses
|
| 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
|
| Comp [Literal] |
Comparisons
|
| Compute_prec |
Compute Precedence
|
| Const |
Configuration and Globals
|
| Conv [Literals] | |
| Conv [Literal] |
Conversions
|
| Ctx [Env_intf.S] | |
| Ctx [ProofState_intf.S] | |
| Ctx |
Basic context for literals, clauses...
|
| Ctx [Clause_intf.S] | |
| Ctx_intf |
current ordering on terms
|
E | |
| E [MetaProverState_intf.S] | |
| E [Avatar_intf.S] | |
| Eligible [Clause_intf.S] | |
| EnumTypes |
Inference and simplification rules for "Enum Types"
|
| Env [Heuristics.S] | |
| Env [ArithInt.S] | |
| Env [EnumTypes.S] | |
| Env [Superposition.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 | |
| Flex_state |
Extensible Map for State
|
| Focus [ArithLit] | |
| Focus [Monome] |
Focus on a specific term
|
H | |
| Heuristics |
Heuristics
|
I | |
| Ind_cst |
Inductive Constants and Cases
|
| Ind_types |
Deal with Inductive Types
|
| Induction |
Induction through Cut
|
| Induction_intf |
Induction
|
| Infix [Phases] | |
| Infix [SimplM] | |
| Int [Monome] | |
K | |
| Key [Rewriting] | |
| Key [Phases] | |
| Key [Ctx] | |
L | |
| Lit [Trail] | |
| Lit [Sat_solver_intf.S] | |
| Lit [BBox] | |
| Lit [Ctx_intf.S] | |
| Literal |
Equational literals
|
| Literals |
Array of literals
|
| Loc [ProofStep] | |
M | |
| MMT [Multisets] | |
| MT [Multisets] | |
| Make [MetaProverState] | |
| Make [Ind_types] | |
| Make [Heuristics] | |
| Make [ArithInt] | |
| 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] | |
| Meta [Induction_intf.S] | |
| MetaProverState |
Meta Prover for zipperposition
|
| MetaProverState_intf |
Rewrite system
|
| Modulo [Monome.Int] | |
| Monome |
Polynomes of order 1, over several variables.
|
| Multisets |
Several Multisets
|
P | |
| PS [Heuristics.S] | |
| PS [ArithInt.S] | |
| PS [Superposition.S] | |
| PTbl [ProofStep] | |
| Params |
Parameters for the prover, etc.
|
| PassiveSet [ProofState_intf.S] | |
| Phases |
Phases of the Prover
|
| Phases_impl |
Implementation of Phases
|
| Pos [Literals] | |
| Pos [Literal] |
Positions
|
| Pos [Clause_intf.S] | |
| ProofPrint |
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
|
| ProofStep |
Manipulate proofs
|
R | |
| Result [MetaProverState_intf.S] | |
| Rewrite_rule |
Rewrite Rules
|
| Rewriting |
Rewriting
|
S | |
| 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 [ArithLit] | |
| Seq [Monome] | |
| Seq [Literals] | |
| Seq [Literal] | |
| Seq [Clause_intf.S] | |
| Set [Rewrite_rule] |
Set of Rewrite Rules
|
| Set [ClauseContext] | |
| Set [Bool_lit_intf.S] | |
| Signals |
Useful signals
|
| SimplM |
Simplification Monad
|
| SimplSet [ProofState_intf.S] | |
| Solve [Monome.Int] | |
| Solver [Avatar_intf.S] | |
| SubsumptionIndex [ProofState_intf.S] | |
| Superposition |
Inference and simplification rules for the superposition calculus
|
T | |
| Tbl [ProofPrint] | |
| TermIndex [ProofState_intf.S] | |
| Trail |
Boolean Trail
|
U | |
| UnitIndex [ProofState_intf.S] | |
| Util [ArithLit] |
Some Utils for arith
|
V | |
| View [Literals] | |
| View [Literal] |
Specific views
|
W | |
| WeightFun [ClauseQueue_intf.S] |
Weight functions
|
| WithPos [Clause_intf.S] |
Clause within which a subterm (and its position) are hilighted
|