Priority Queue of clauses

Clauses

Simple Clause

Configuration and Globals

Dynamic extensions

Basic context for literals, clauses...

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

Parameters for the prover, etc.

Global environment for an instance of the prover

Useful signals

Classification of Constants

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

Cover Set

Universally Quantified Conjunction of Clauses

Phases of the Prover

Implementation of Phases

Basic Splitting à la Avatar

Split a clause into components

Induction through Cut

Induction

Inference and simplification rules for the superposition calculus

Term Indices

Rewriting

Inference and simplification rules for "Enum Types"

Cancellative Inferences on Integer Arithmetic

Cancellative Inferences on Rational Arithmetic

Heuristics

Deal with Inductive Types

boolean subterms