Module Mcsolver

module Mcsolver: sig .. end

Create McSat solver

This module provides a functor to create an McSAt solver.

module type S = Solver_intf.S

The interface exposed by the solver.

module Make: functor (E : Expr_intf.S) -> functor (Th : Plugin_intf.S  with type term = E.Term.t
                         and type formula = E.Formula.t
                         and type proof = E.proof) -> functor (Dummy : sig
end) -> S  with type St.term = E.Term.t
     and type St.formula = E.Formula.t
     and type St.proof = E.proof

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