Module Libzipperposition.Sat_solverSource

Interface to MSat

include module type of Sat_solver_intf
Sourcetype proof_step = Logtk.Proof.Step.t
Sourcetype proof = Logtk.Proof.t
Sourcetype result =
  1. | Sat
  2. | Unsat of proof
Sourceexception WrongState of string
Sourcemodule type S = sig ... end
Sourcemodule Make () : S
Sourceval set_compact : bool -> unit

Toggle compact proofs. if true, collapse internal resolution nodes in proofs