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
|