module Log : sig ... endmodule Formula_intf : sig ... endmodule Plugin_intf : sig ... endmodule Theory_intf : sig ... endmodule Expr_intf : sig ... endmodule Tseitin_intf : sig ... endmodule Solver_types_intf : sig ... endmodule Solver_types : sig ... endmodule Res_intf : sig ... endmodule Res : sig ... endmodule Solver_intf : sig ... endmodule Internal : sig ... endmodule External : sig ... endmodule Solver : sig ... endmodule Mcsolver : sig ... endmodule Dot : sig ... endmodule Dedukti : sig ... endmodule Tseitin : sig ... endmodule Expr : sig ... endmodule Cnf : sig ... endmodule Sat : sig ... endmodule Sig : sig ... endmodule Unionfind : sig ... endmodule Cc : sig ... endmodule Mcsat : sig ... endmodule Smt : sig ... end