sig
  type term = Logic.T.t
  type lit = Logic.Lit.t
  type clause = Logic.C.t
  type name_ctx = (string, term) Hashtbl.t
  val create_ctx : unit -> name_ctx
  val term_of_ast : ctx:name_ctx -> TopDownAst.term -> term
  val lit_of_ast : ctx:name_ctx -> TopDownAst.literal -> lit
  val clause_of_ast : ?ctx:name_ctx -> TopDownAst.clause -> clause
  val clauses_of_ast : ?ctx:name_ctx -> TopDownAst.clause list -> clause list
  val parse_chan : in_channel -> [ `Error of string | `Ok of clause list ]
  val parse_file : string -> [ `Error of string | `Ok of clause list ]
  val parse_string : string -> [ `Error of string | `Ok of clause list ]
  val clause_of_string : string -> clause
  val load_chan : CamlInterface.Logic.DB.t -> Pervasives.in_channel -> bool
  val load_file : CamlInterface.Logic.DB.t -> string -> bool
  val load_string : CamlInterface.Logic.DB.t -> string -> bool
end