sig
  type term = TypedSTerm.t
  type form = TypedSTerm.t
  type type_ = TypedSTerm.t
  type lit = Cnf.term SLiteral.t
  exception Error of string
  exception NotCNF of Cnf.form
  val miniscope : ?distribute_exists:bool -> Cnf.form -> Cnf.form
  type options =
      DistributeExists
    | DisableRenaming
    | InitialProcessing of (Cnf.form -> Cnf.form)
    | PostNNF of (Cnf.form -> Cnf.form)
    | PostSkolem of (Cnf.form -> Cnf.form)
  type clause = Cnf.lit list
  val clause_to_fo :
    ?ctx:FOTerm.Conv.ctx -> Cnf.clause -> FOTerm.t SLiteral.t list
  type 'a f_statement = (Cnf.term, Cnf.term, Cnf.type_, 'a) Statement.t
  type 'a c_statement = (Cnf.clause, Cnf.term, Cnf.type_, 'a) Statement.t
  val pp_f_statement : 'a Cnf.f_statement CCFormat.printer
  val pp_c_statement : 'a Cnf.c_statement CCFormat.printer
  val is_clause : Cnf.form -> bool
  val is_cnf : Cnf.form -> bool
  val cnf_of :
    ?opts:Cnf.options list ->
    ?ctx:Skolem.ctx ->
    ?neg_src:('a -> 'a) ->
    ?cnf_src:('a -> 'a) ->
    'a Cnf.f_statement -> 'a Cnf.c_statement CCVector.ro_vector
  val cnf_of_seq :
    ?opts:Cnf.options list ->
    ?ctx:Skolem.ctx ->
    ?neg_src:('a -> 'a) ->
    ?cnf_src:('a -> 'a) ->
    'a Cnf.f_statement Sequence.t -> 'a Cnf.c_statement CCVector.ro_vector
  val type_declarations : 'a Cnf.c_statement Sequence.t -> Cnf.type_ ID.Map.t
  val convert :
    StatementSrc.t Cnf.c_statement Sequence.t ->
    Statement.clause_t CCVector.ro_vector
end