Index of modules

Backend interface

Coq Backend

Deduki backend for proofs

Provides a reasonnable default to instantiate the Make functor, assuming the original printing functions are compatible with DOT html labels.

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

Hashtable over proofs.

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.

Base functor to output Coq proofs

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.

Simple functo to output Coq proofs

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

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