sig
  type term = Nunchaku_core.TermInner.Default.t
  val name : string
  type mode = [ `Sk_all | `Sk_ho | `Sk_types ]
  type state
  val create : ?prefix:string -> mode:Skolem.mode -> unit -> Skolem.state
  val skolemize :
    state:Skolem.state ->
    ?in_goal:bool ->
    Nunchaku_core.Polarity.t ->
    Skolem.term -> Skolem.term * (Nunchaku_core.ID.t * Skolem.term) list
  val print_state : Format.formatter -> Skolem.state -> unit
  val skolemize_pb :
    state:Skolem.state ->
    (Skolem.term, Skolem.term) Nunchaku_core.Problem.t ->
    (Skolem.term, Skolem.term) Nunchaku_core.Problem.t
  val decode_model :
    skolems_in_model:bool ->
    state:Skolem.state ->
    (Skolem.term, Skolem.term) Nunchaku_core.Model.t ->
    (Skolem.term, Skolem.term) Nunchaku_core.Model.t
  val pipe :
    skolems_in_model:bool ->
    mode:Skolem.mode ->
    print:bool ->
    check:bool ->
    ((Skolem.term, Skolem.term) Nunchaku_core.Problem.t,
     (Skolem.term, Skolem.term) Nunchaku_core.Problem.t,
     (Skolem.term, Skolem.term) Nunchaku_core.Problem.Res.t,
     (Skolem.term, Skolem.term) Nunchaku_core.Problem.Res.t)
    Nunchaku_core.Transform.t
  val pipe_with :
    mode:Skolem.mode ->
    decode:(Skolem.state -> 'c -> 'd) ->
    print:bool ->
    check:bool ->
    ((Skolem.term, Skolem.term) Nunchaku_core.Problem.t,
     (Skolem.term, Skolem.term) Nunchaku_core.Problem.t, 'c, 'd)
    Nunchaku_core.Transform.t
end