Module `Libzipperposition.Sat_solver`

Interface to MSat

include module type of Sat_solver_intf

type proof_step = Logtk.Proof.Step.t
type proof = Logtk.Proof.t
type result = | Sat | Unsat of proof

exception WrongState of string

module type S = sig ... end

module Make : functor () S

val set_compact : bool -> unit: Toggle compact proofs. if true, collapse internal resolution nodes in proofs