sig
  type ctx
  val create :
    ?ty_prop:LogtkType.t ->
    ?prefix:string ->
    ?prop_prefix:string -> LogtkSignature.t -> LogtkSkolem.ctx
  val to_signature : LogtkSkolem.ctx -> LogtkSignature.t
  val fresh_sym : ctx:LogtkSkolem.ctx -> ty:LogtkType.t -> LogtkSymbol.t
  val fresh_sym_with :
    ctx:LogtkSkolem.ctx -> ty:LogtkType.t -> string -> LogtkSymbol.t
  val fresh_ty_const :
    ?prefix:string -> ctx:LogtkSkolem.ctx -> unit -> LogtkSymbol.t
  val instantiate_ty : LogtkFormula.FO.t -> LogtkType.t -> LogtkFormula.FO.t
  val instantiate : LogtkFormula.FO.t -> LogtkFOTerm.t -> LogtkFormula.FO.t
  val clear_var : ctx:LogtkSkolem.ctx -> unit
  val fresh_var : ctx:LogtkSkolem.ctx -> int
  val update_var : ctx:LogtkSkolem.ctx -> LogtkFOTerm.t -> unit
  val skolem_form :
    ctx:LogtkSkolem.ctx ->
    ty:LogtkType.t -> LogtkFormula.FO.t -> LogtkFormula.FO.t
  type polarity = [ `Both | `Neg | `Pos ]
  type definition = {
    form : LogtkFormula.FO.t;
    proxy : LogtkFormula.FO.t;
    polarity : LogtkSkolem.polarity Pervasives.ref;
  }
  val has_definition : ctx:LogtkSkolem.ctx -> LogtkFormula.FO.t -> bool
  val get_definition :
    ctx:LogtkSkolem.ctx ->
    polarity:LogtkSkolem.polarity -> LogtkFormula.FO.t -> LogtkFormula.FO.t
  val all_definitions :
    ctx:LogtkSkolem.ctx -> LogtkSkolem.definition Sequence.t
  val remove_def : ctx:LogtkSkolem.ctx -> LogtkSkolem.definition -> unit
  val pop_new_definitions :
    ctx:LogtkSkolem.ctx -> LogtkSkolem.definition list
  val has_new_definitions : ctx:LogtkSkolem.ctx -> bool
  val skolem_ho :
    ctx:LogtkSkolem.ctx -> ty:LogtkType.t -> LogtkHOTerm.t -> LogtkHOTerm.t
end