module Dummy : sig ... endmodule SmtSolver : sig ... endmodule Proof = SmtSolver.Proofmodule Dot : sig ... endtype atom = Fsmt.ttype clause = SmtSolver.St.clausetype proof = SmtSolver.Proof.proofval solve : unit -> resval assume : Fsmt.Formula.t list list -> unitval get_proof : unit -> SmtSolver.Proof.proofval eval : Fsmt.Formula.t -> boolval unsat_core : SmtSolver.Proof.proof -> SmtSolver.Proof.clause listval print_atom : Format.formatter -> Fsmt.t -> unitval print_clause : Format.formatter -> SmtSolver.St.clause -> unitval print_proof : Format.formatter -> SmtSolver.Proof.proof -> unit