ClauseQueue
Priority Queue of clauses
Clause
Clauses
SClause
Simple Clause
Const
Configuration and Globals
Extensions
Dynamic extensions
Literal
Equational literals
Literals
Array of literals
Ctx
Basic context for literals, clauses...
ProofStep
Manipulate proofs
ProofPrint
Manipulate proofs
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.
Saturate
Main saturation algorithm.
Selection
Selection functions
AC
AC redundancy
AC_intf
Declare that the given symbol is AC, and update the Env subsequently by adding clauses, etc.
SimplM
Simplification Monad
Compute_prec
Compute Precedence
Params
Parameters for the prover, etc.
Env
Global environment for an instance of the prover
Monome
Polynomes of order 1, over several variables.
ArithLit
Arithmetic Literal
Signals
Useful signals
Multisets
Several Multisets
Ctx_intf
current ordering on terms
Clause_intf
Flags
Env_intf
An inference returns a list of conclusions
ProofState_intf
Set of active clauses
BBox
BBox (Boolean Box)
ClauseContext
Clause context
ClauseQueue_intf
A priority queue of clauses, purely functional
Bool_lit
Boolean Literal
Bool_lit_intf
Additional data carried in the literal
Sat_solver
Interface to MSat
Sat_solver_intf
add_clause ~tag ~proof c adds the constraint c to the SAT solver, annotated with proof.
Trail
Boolean Trail
Ind_cst
Inductive Constants and Cases
Phases
Phases of the Prover
Phases_impl
Implementation of Phases
Flex_state
Extensible Map for State
Classify_cst
Classification of Constants
Rewrite_rule
Rewrite Rules
Avatar
Basic Splitting à la Avatar
Avatar_intf
Split a clause into components
Induction
Induction through Cut
Induction_intf
Induction
Superposition
Inference and simplification rules for the superposition calculus
Rewriting
Rewriting
EnumTypes
Inference and simplification rules for "Enum Types"
ArithInt
Cancellative Inferences on Integer Arithmetic
Heuristics
Heuristics
Ind_types
Deal with Inductive Types
MetaProverState
Meta Prover for zipperposition
MetaProverState_intf
Rewrite system