module St : Solver_types.Smodule Th : sig ... endmodule Dummy : sig ... endmodule St : sig ... endmodule Proof : sig ... endtype atom = St.formulatype res = | Sat of (St.term, St.formula) Solver_intf.sat_state| Unsat of (St.clause, Proof.proof) Solver_intf.unsat_stateval assume : ?tag:int -> atom list list -> unitval new_lit : St.term -> unitval new_atom : atom -> unitval unsat_core : Proof.proof -> St.clause listval true_at_level0 : atom -> boolval get_tag : St.clause -> int optionval export_dimacs : Format.formatter -> unit -> unitval export_icnf : Format.formatter -> unit -> unit