Index of modules

Backend interface

Deduki backend for proofs

Dot backend for proofs

Simple case where the theory is empty and the proof type is the one given in the formula interface

The module defining formulas

Mcsat expressions

mSAT safe interface

SMT formulas

mSAT core

Logging function, for debugging

A functor that can generate as many solvers as needed.

Functor to generate a backend to output proofs for the dedukti type checker.

Functor for making a module to export proofs to the DOT format.

This functor provides an implementation of Tseitin's CNF conversion.

Functor to create a solver parametrised by the atomic formulas and a theory.

Functor to create a SMT Solver parametrised by the atomic formulas and a theory.

Functor to make a safe external interface.

Functor to create a module building proofs from a sat-solver unsat trace.

Functor to instantiate the types of clauses for a solver.

Create McSat solver

McSat Theory

A module to manipulate proofs.

Resolution proofs

Interface for proofs

Sat solver

Functor to instantiate the types of clauses for a solver.

Create SAT/SMT Solvers

Interface for Solvers

Internal types (implementation)

Internal types (interface)

WARNING: Very dangerous module that expose the internal representation used by the solver.

Module defining atom and clauses

SMT Theory

Tseitin CNF conversion

Interfaces for Tseitin's CNF conversion