Module Solver

module Solver: sig .. end

Create SAT/SMT Solvers

This module provides a functor to create an SMT solver. Additionally, it also gives a functor that produce an adequate empty theory that can be given to the Make functor in order to create a pure SAT solver.

module type S = Solver_intf.S

The interface of instantiated solvers.

module DummyTheory: functor (F : Formula_intf.S) -> Theory_intf.S  with type formula = F.t
                 and type proof = F.proof

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

module Make: functor (F : Formula_intf.S) -> functor (Th : Theory_intf.S  with type formula = F.t
                         and type proof = F.proof) -> functor (Dummy : sig
end) -> S  with type St.formula = F.t
     and type St.proof = F.proof

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