sig
  module Constructor :
    sig
      type constructor
      val get_num_fields : Z3.Datatype.Constructor.constructor -> int
      val get_constructor_decl :
        Z3.Datatype.Constructor.constructor -> Z3.FuncDecl.func_decl
      val get_tester_decl :
        Z3.Datatype.Constructor.constructor -> Z3.FuncDecl.func_decl
      val get_accessor_decls :
        Z3.Datatype.Constructor.constructor -> Z3.FuncDecl.func_decl list
    end
  val mk_constructor :
    Z3.context ->
    Z3.Symbol.symbol ->
    Z3.Symbol.symbol ->
    Z3.Symbol.symbol list ->
    Z3.Sort.sort option list ->
    int list -> Z3.Datatype.Constructor.constructor
  val mk_constructor_s :
    Z3.context ->
    string ->
    Z3.Symbol.symbol ->
    Z3.Symbol.symbol list ->
    Z3.Sort.sort option list ->
    int list -> Z3.Datatype.Constructor.constructor
  val mk_sort_ref : Z3.context -> Z3.Symbol.symbol -> Z3.Sort.sort
  val mk_sort_ref_s : Z3.context -> string -> Z3.Sort.sort
  val mk_sort :
    Z3.context ->
    Z3.Symbol.symbol ->
    Z3.Datatype.Constructor.constructor list -> Z3.Sort.sort
  val mk_sort_s :
    Z3.context ->
    string -> Z3.Datatype.Constructor.constructor list -> Z3.Sort.sort
  val mk_sorts :
    Z3.context ->
    Z3.Symbol.symbol list ->
    Z3.Datatype.Constructor.constructor list list -> Z3.Sort.sort list
  val mk_sorts_s :
    Z3.context ->
    string list ->
    Z3.Datatype.Constructor.constructor list list -> Z3.Sort.sort list
  val get_num_constructors : Z3.Sort.sort -> int
  val get_constructors : Z3.Sort.sort -> Z3.FuncDecl.func_decl list
  val get_recognizers : Z3.Sort.sort -> Z3.FuncDecl.func_decl list
  val get_accessors : Z3.Sort.sort -> Z3.FuncDecl.func_decl list list
end