Module `Msat__.Solver`

module type S = Msat.Solver_intf.S: Safe external interface of solvers.

module Make_cdcl_t : functor (Th : Msat.Solver_intf.PLUGIN_CDCL_T) -> S with type Term.t = Msat.Solver_intf.void and module Formula = Th.Formula and type lemma = Th.proof and type theory = Th.t

module Make_mcsat : functor (Th : Msat.Solver_intf.PLUGIN_MCSAT) -> S with module Term = Th.Term and module Formula = Th.Formula and type lemma = Th.proof and type theory = Th.t

module Make_pure_sat : functor (Th : Msat.Solver_intf.PLUGIN_SAT) -> S with type Term.t = Msat.Solver_intf.void and module Formula = Th.Formula and type lemma = Th.proof and type theory = unit