Module `Sidekick_smt_solver`

Core of the SMT solver using Sidekick_sat

Sidekick_sat (in src/sat/) is a modular SAT solver in pure OCaml.

This builds a Sidekick_core.SOLVER on top of it.

module type ARG = sig ... end: Argument to pass to the functor Make in order to create a new Msat-based SMT solver.

module type S = Sidekick_core.SOLVER

module Make : functor (A : ARG) -> S with module T = A.T and type proof = A.proof and module Lit = A.Lit and module P = A.P: Main functor to get a solver.