Priority Queue of clauses

Clauses

Simple Clause

Configuration and Globals

Dynamic extensions

Equational literals

Array of literals

Basic context for literals, clauses...

Manipulate proofs

Manipulate proofs

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.

Main saturation algorithm.

Selection functions

AC redundancy

Declare that the given symbol is AC, and update the Env subsequently by adding clauses, etc.

Simplification Monad

Compute Precedence

Parameters for the prover, etc.

Global environment for an instance of the prover

Polynomes of order 1, over several variables.

Arithmetic Literal

Useful signals

Several Multisets

current ordering on terms

Flags

An inference returns a list of conclusions

Set of active clauses

BBox (Boolean Box)

Clause context

A priority queue of clauses, purely functional

Boolean Literal

Additional data carried in the literal

Interface to MSat

add_clause ~tag ~proof c adds the constraint c to the SAT solver, annotated with proof.

Boolean Trail

Inductive Constants and Cases

Phases of the Prover

Implementation of Phases

Extensible Map for State

Classification of Constants

Rewrite Rules

Basic Splitting à la Avatar

Split a clause into components

Induction through Cut

Induction

Inference and simplification rules for the superposition calculus

Rewriting

Inference and simplification rules for "Enum Types"

Cancellative Inferences on Integer Arithmetic

Heuristics

Deal with Inductive Types

Meta Prover for zipperposition

Rewrite system