sig
  type metadata = ProblemMetadata.t
  type loc = Location.t
  type id = ID.t
  type 'a printer = Format.formatter -> 'a -> unit
  type 'a to_sexp = 'a -> Sexp_lib.t
  type 'a or_error = ('a, string) CCResult.t
  type ('t, 'ty) t = private {
    statements : ('t, 'ty) Statement.t CCVector.ro_vector;
    metadata : Problem.metadata;
  }
  val make :
    meta:Problem.metadata ->
    ('t, 'ty) Statement.t CCVector.ro_vector -> ('t, 'ty) Problem.t
  val of_list :
    meta:Problem.metadata ->
    ('t, 'ty) Statement.t list -> ('t, 'ty) Problem.t
  val statements :
    ('t, 'ty) Problem.t -> ('t, 'ty) Statement.t CCVector.ro_vector
  val metadata : ('a, 'b) Problem.t -> Problem.metadata
  val update_meta :
    ('t, 'ty) Problem.t ->
    (Problem.metadata -> Problem.metadata) -> ('t, 'ty) Problem.t
  val add_sat_means_unknown :
    bool -> ('t, 'ty) Problem.t -> ('t, 'ty) Problem.t
  val set_sat_means_unknown : ('t, 'ty) Problem.t -> ('t, 'ty) Problem.t
  val add_unsat_means_unknown :
    bool -> ('t, 'ty) Problem.t -> ('t, 'ty) Problem.t
  val set_unsat_means_unknown : ('t, 'ty) Problem.t -> ('t, 'ty) Problem.t
  val iter_statements :
    f:(('t, 'ty) Statement.t -> unit) -> ('t, 'ty) Problem.t -> unit
  val map_statements :
    f:(('t, 'ty) Statement.t -> ('t2, 'ty2) Statement.t) ->
    ('t, 'ty) Problem.t -> ('t2, 'ty2) Problem.t
  val fold_map_statements :
    f:('acc -> ('t, 'ty) Statement.t -> 'acc * ('t2, 'ty2) Statement.t) ->
    x:'acc -> ('t, 'ty) Problem.t -> 'acc * ('t2, 'ty2) Problem.t
  val flat_map_statements :
    f:(('t, 'ty) Statement.t -> ('t2, 'ty2) Statement.t list) ->
    ('t, 'ty) Problem.t -> ('t2, 'ty2) Problem.t
  val map :
    term:('a -> 'b) ->
    ty:('tya -> 'tyb) -> ('a, 'tya) Problem.t -> ('b, 'tyb) Problem.t
  val map_with :
    ?before:(unit -> ('b, 'tyb) Statement.t list) ->
    ?after:(unit -> ('b, 'tyb) Statement.t list) ->
    term:('a -> 'b) ->
    ty:('tya -> 'tyb) -> ('a, 'tya) Problem.t -> ('b, 'tyb) Problem.t
  module Print :
    functor (P1 : TermInner.PRINT) (P2 : TermInner.PRINT) ->
      sig val print : (P1.t, P2.t) Problem.t Problem.printer end
  module Convert :
    functor (T1 : TermInner.REPR) (T2 : TermInner.BUILD) ->
      sig
        type ('a, 'b, 'c) inv = < eqn : 'a; ind_preds : 'b; ty : 'c >
        val convert : (T1.t, T1.t) Problem.t -> (T2.t, T2.t) Problem.t
        val pipe :
          unit ->
          ((T1.t, T1.t) Problem.t, (T2.t, T2.t) Problem.t, 'ret, 'ret)
          Transform.t
      end
  exception IllFormed of string
  val goal : ('t, 'a) Problem.t -> 't
  val signature :
    ?init:'ty Signature.t -> ('a, 'ty) Problem.t -> 'ty Signature.t
  val env : ?init:('t, 'ty) Env.t -> ('t, 'ty) Problem.t -> ('t, 'ty) Env.t
  module Res :
    sig
      type info = {
        backend : string;
        time : float;
        message : string option;
      }
      type unknown_info =
          U_timeout of Problem.Res.info
        | U_out_of_scope of Problem.Res.info
        | U_incomplete of Problem.Res.info
        | U_other of Problem.Res.info * string
      type ('t, 'ty) t =
          Unsat of Problem.Res.info
        | Sat of ('t, 'ty) Model.t * Problem.Res.info
        | Unknown of Problem.Res.unknown_info list
        | Error of exn * Problem.Res.info
      val mk_info :
        ?message:string ->
        backend:string -> time:float -> unit -> Problem.Res.info
      val map :
        term:('t1 -> 't2) ->
        ty:('ty1 -> 'ty2) ->
        ('t1, 'ty1) Problem.Res.t -> ('t2, 'ty2) Problem.Res.t
      val map_m :
        f:(('t1, 'ty1) Model.t -> ('t2, 'ty2) Model.t) ->
        ('t1, 'ty1) Problem.Res.t -> ('t2, 'ty2) Problem.Res.t
      val print :
        (TermInner.prec -> 't Problem.printer) ->
        'ty Problem.printer -> ('t, 'ty) Problem.Res.t Problem.printer
      val print_info : Problem.Res.info Problem.printer
      val print_unknown_info : Problem.Res.unknown_info Problem.printer
      val print_head : ('a, 'b) Problem.Res.t Problem.printer
      val to_sexp :
        't Problem.to_sexp ->
        'ty Problem.to_sexp -> ('t, 'ty) Problem.Res.t Problem.to_sexp
    end
end