sig
  type itysymbol = private {
    its_ts : Ty.tysymbol;
    its_nonfree : bool;
    its_private : bool;
    its_mutable : bool;
    its_fragile : bool;
    its_mfields : Ity.pvsymbol list;
    its_ofields : Ity.pvsymbol list;
    its_regions : Ity.region list;
    its_arg_flg : Ity.its_flag list;
    its_reg_flg : Ity.its_flag list;
    its_def : Ity.ity Ty.type_def;
  }
  and its_flag = private {
    its_frozen : bool;
    its_exposed : bool;
    its_liable : bool;
    its_fixed : bool;
    its_visible : bool;
  }
  and ity = private {
    ity_node : Ity.ity_node;
    ity_pure : bool;
    ity_tag : Weakhtbl.tag;
  }
  and ity_node = private
      Ityreg of Ity.region
    | Ityapp of Ity.itysymbol * Ity.ity list * Ity.ity list
    | Ityvar of Ty.tvsymbol
  and region = private {
    reg_name : Ident.ident;
    reg_its : Ity.itysymbol;
    reg_args : Ity.ity list;
    reg_regs : Ity.ity list;
  }
  and pvsymbol = private {
    pv_vs : Term.vsymbol;
    pv_ity : Ity.ity;
    pv_ghost : bool;
  }
  module Mits :
    sig
      type key = itysymbol
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val set_union : 'a t -> 'a t -> 'a t
      val set_inter : 'a t -> 'b t -> 'a t
      val set_diff : 'a t -> 'b t -> 'a t
      val set_submap : 'a t -> 'b t -> bool
      val set_disjoint : 'a t -> 'b t -> bool
      val set_compare : 'a t -> 'b t -> int
      val set_equal : 'a t -> 'b t -> bool
      val find_def : 'a -> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('a -> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> 'a -> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
      val fold2_inter :
        (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> 'c -> 'c) ->
        'a t -> 'b t -> 'c -> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> 'a -> 'a t -> 'a t
      val replace : exn -> key -> 'a -> 'a t -> 'a t
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val of_list : (key * 'a) list -> 'a t
      val contains : 'a t -> key -> bool
      val domain : 'a t -> unit t
      val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
      val is_num_elt : int -> 'a t -> bool
      type 'a enumeration
      val val_enum : 'a enumeration -> (key * 'a) option
      val start_enum : 'a t -> 'a enumeration
      val next_enum : 'a enumeration -> 'a enumeration
      val start_ge_enum : key -> 'a t -> 'a enumeration
      val next_ge_enum : key -> 'a enumeration -> 'a enumeration
    end
  module Sits :
    sig
      module M :
        sig
          type key = itysymbol
          type 'a t = 'a Mits.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> 'a -> 'a t -> 'a t
          val singleton : key -> 'a -> 'a t
          val remove : key -> 'a t -> 'a t
          val merge :
            (key -> 'a option -> 'b option -> 'c option) ->
            'a t -> 'b t -> 'c t
          val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
          val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
          val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val for_all : (key -> 'a -> bool) -> 'a t -> bool
          val exists : (key -> 'a -> bool) -> 'a t -> bool
          val filter : (key -> 'a -> bool) -> 'a t -> 'a t
          val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
          val cardinal : 'a t -> int
          val bindings : 'a t -> (key * 'a) list
          val min_binding : 'a t -> key * 'a
          val max_binding : 'a t -> key * 'a
          val choose : 'a t -> key * 'a
          val split : key -> 'a t -> 'a t * 'a option * 'a t
          val find : key -> 'a t -> 'a
          val map : ('a -> 'b) -> 'a t -> 'b t
          val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val set_union : 'a t -> 'a t -> 'a t
          val set_inter : 'a t -> 'b t -> 'a t
          val set_diff : 'a t -> 'b t -> 'a t
          val set_submap : 'a t -> 'b t -> bool
          val set_disjoint : 'a t -> 'b t -> bool
          val set_compare : 'a t -> 'b t -> int
          val set_equal : 'a t -> 'b t -> bool
          val find_def : 'a -> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('a -> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> 'a -> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
          val fold2_inter :
            (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> 'c -> 'c) ->
            'a t -> 'b t -> 'c -> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> 'a -> 'a t -> 'a t
          val replace : exn -> key -> 'a -> 'a t -> 'a t
          val keys : 'a t -> key list
          val values : 'a t -> 'a list
          val of_list : (key * 'a) list -> 'a t
          val contains : 'a t -> key -> bool
          val domain : 'a t -> unit t
          val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = 'a Mits.enumeration
          val val_enum : 'a enumeration -> (key * 'a) option
          val start_enum : 'a t -> 'a enumeration
          val next_enum : 'a enumeration -> 'a enumeration
          val start_ge_enum : key -> 'a t -> 'a enumeration
          val next_ge_enum : key -> 'a enumeration -> 'a enumeration
        end
      type elt = M.key
      type t = unit M.t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val merge : (elt -> bool -> bool -> bool) -> t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val disjoint : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
      val change : (bool -> bool) -> elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
      val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val translate : (elt -> elt) -> t -> t
      val add_new : exn -> elt -> t -> t
      val is_num_elt : int -> t -> bool
      val of_list : elt list -> t
      val contains : t -> elt -> bool
      val add_left : t -> elt -> t
      val remove_left : t -> elt -> t
      val print :
        (Format.formatter -> elt -> unit) -> Format.formatter -> t -> unit
    end
  module Hits :
    sig
      type key = itysymbol
      type !'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_keys : 'a t -> key Seq.t
      val to_seq_values : 'a t -> 'a Seq.t
      val add_seq : 'a t -> (key * 'a) Seq.t -> unit
      val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
      val of_seq : (key * 'a) Seq.t -> 'a t
      val find_def : 'a t -> 'a -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  module Wits :
    sig
      type key = itysymbol
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val find : 'a t -> key -> 'a
      val mem : 'a t -> key -> bool
      val set : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val length : 'a t -> int
      val memoize : int -> (key -> 'a) -> key -> 'a
      val memoize_rec : int -> ((key -> 'a) -> key -> 'a) -> key -> 'a
      val memoize_option : int -> (key option -> 'a) -> key option -> 'a
    end
  module Mity :
    sig
      type key = ity
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val set_union : 'a t -> 'a t -> 'a t
      val set_inter : 'a t -> 'b t -> 'a t
      val set_diff : 'a t -> 'b t -> 'a t
      val set_submap : 'a t -> 'b t -> bool
      val set_disjoint : 'a t -> 'b t -> bool
      val set_compare : 'a t -> 'b t -> int
      val set_equal : 'a t -> 'b t -> bool
      val find_def : 'a -> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('a -> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> 'a -> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
      val fold2_inter :
        (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> 'c -> 'c) ->
        'a t -> 'b t -> 'c -> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> 'a -> 'a t -> 'a t
      val replace : exn -> key -> 'a -> 'a t -> 'a t
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val of_list : (key * 'a) list -> 'a t
      val contains : 'a t -> key -> bool
      val domain : 'a t -> unit t
      val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
      val is_num_elt : int -> 'a t -> bool
      type 'a enumeration
      val val_enum : 'a enumeration -> (key * 'a) option
      val start_enum : 'a t -> 'a enumeration
      val next_enum : 'a enumeration -> 'a enumeration
      val start_ge_enum : key -> 'a t -> 'a enumeration
      val next_ge_enum : key -> 'a enumeration -> 'a enumeration
    end
  module Sity :
    sig
      module M :
        sig
          type key = ity
          type 'a t = 'a Mity.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> 'a -> 'a t -> 'a t
          val singleton : key -> 'a -> 'a t
          val remove : key -> 'a t -> 'a t
          val merge :
            (key -> 'a option -> 'b option -> 'c option) ->
            'a t -> 'b t -> 'c t
          val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
          val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
          val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val for_all : (key -> 'a -> bool) -> 'a t -> bool
          val exists : (key -> 'a -> bool) -> 'a t -> bool
          val filter : (key -> 'a -> bool) -> 'a t -> 'a t
          val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
          val cardinal : 'a t -> int
          val bindings : 'a t -> (key * 'a) list
          val min_binding : 'a t -> key * 'a
          val max_binding : 'a t -> key * 'a
          val choose : 'a t -> key * 'a
          val split : key -> 'a t -> 'a t * 'a option * 'a t
          val find : key -> 'a t -> 'a
          val map : ('a -> 'b) -> 'a t -> 'b t
          val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val set_union : 'a t -> 'a t -> 'a t
          val set_inter : 'a t -> 'b t -> 'a t
          val set_diff : 'a t -> 'b t -> 'a t
          val set_submap : 'a t -> 'b t -> bool
          val set_disjoint : 'a t -> 'b t -> bool
          val set_compare : 'a t -> 'b t -> int
          val set_equal : 'a t -> 'b t -> bool
          val find_def : 'a -> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('a -> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> 'a -> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
          val fold2_inter :
            (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> 'c -> 'c) ->
            'a t -> 'b t -> 'c -> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> 'a -> 'a t -> 'a t
          val replace : exn -> key -> 'a -> 'a t -> 'a t
          val keys : 'a t -> key list
          val values : 'a t -> 'a list
          val of_list : (key * 'a) list -> 'a t
          val contains : 'a t -> key -> bool
          val domain : 'a t -> unit t
          val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = 'a Mity.enumeration
          val val_enum : 'a enumeration -> (key * 'a) option
          val start_enum : 'a t -> 'a enumeration
          val next_enum : 'a enumeration -> 'a enumeration
          val start_ge_enum : key -> 'a t -> 'a enumeration
          val next_ge_enum : key -> 'a enumeration -> 'a enumeration
        end
      type elt = M.key
      type t = unit M.t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val merge : (elt -> bool -> bool -> bool) -> t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val disjoint : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
      val change : (bool -> bool) -> elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
      val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val translate : (elt -> elt) -> t -> t
      val add_new : exn -> elt -> t -> t
      val is_num_elt : int -> t -> bool
      val of_list : elt list -> t
      val contains : t -> elt -> bool
      val add_left : t -> elt -> t
      val remove_left : t -> elt -> t
      val print :
        (Format.formatter -> elt -> unit) -> Format.formatter -> t -> unit
    end
  module Hity :
    sig
      type key = ity
      type !'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_keys : 'a t -> key Seq.t
      val to_seq_values : 'a t -> 'a Seq.t
      val add_seq : 'a t -> (key * 'a) Seq.t -> unit
      val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
      val of_seq : (key * 'a) Seq.t -> 'a t
      val find_def : 'a t -> 'a -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  module Wity :
    sig
      type key = ity
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val find : 'a t -> key -> 'a
      val mem : 'a t -> key -> bool
      val set : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val length : 'a t -> int
      val memoize : int -> (key -> 'a) -> key -> 'a
      val memoize_rec : int -> ((key -> 'a) -> key -> 'a) -> key -> 'a
      val memoize_option : int -> (key option -> 'a) -> key option -> 'a
    end
  module Mreg :
    sig
      type key = region
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val set_union : 'a t -> 'a t -> 'a t
      val set_inter : 'a t -> 'b t -> 'a t
      val set_diff : 'a t -> 'b t -> 'a t
      val set_submap : 'a t -> 'b t -> bool
      val set_disjoint : 'a t -> 'b t -> bool
      val set_compare : 'a t -> 'b t -> int
      val set_equal : 'a t -> 'b t -> bool
      val find_def : 'a -> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('a -> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> 'a -> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
      val fold2_inter :
        (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> 'c -> 'c) ->
        'a t -> 'b t -> 'c -> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> 'a -> 'a t -> 'a t
      val replace : exn -> key -> 'a -> 'a t -> 'a t
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val of_list : (key * 'a) list -> 'a t
      val contains : 'a t -> key -> bool
      val domain : 'a t -> unit t
      val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
      val is_num_elt : int -> 'a t -> bool
      type 'a enumeration
      val val_enum : 'a enumeration -> (key * 'a) option
      val start_enum : 'a t -> 'a enumeration
      val next_enum : 'a enumeration -> 'a enumeration
      val start_ge_enum : key -> 'a t -> 'a enumeration
      val next_ge_enum : key -> 'a enumeration -> 'a enumeration
    end
  module Sreg :
    sig
      module M :
        sig
          type key = region
          type 'a t = 'a Mreg.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> 'a -> 'a t -> 'a t
          val singleton : key -> 'a -> 'a t
          val remove : key -> 'a t -> 'a t
          val merge :
            (key -> 'a option -> 'b option -> 'c option) ->
            'a t -> 'b t -> 'c t
          val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
          val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
          val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val for_all : (key -> 'a -> bool) -> 'a t -> bool
          val exists : (key -> 'a -> bool) -> 'a t -> bool
          val filter : (key -> 'a -> bool) -> 'a t -> 'a t
          val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
          val cardinal : 'a t -> int
          val bindings : 'a t -> (key * 'a) list
          val min_binding : 'a t -> key * 'a
          val max_binding : 'a t -> key * 'a
          val choose : 'a t -> key * 'a
          val split : key -> 'a t -> 'a t * 'a option * 'a t
          val find : key -> 'a t -> 'a
          val map : ('a -> 'b) -> 'a t -> 'b t
          val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val set_union : 'a t -> 'a t -> 'a t
          val set_inter : 'a t -> 'b t -> 'a t
          val set_diff : 'a t -> 'b t -> 'a t
          val set_submap : 'a t -> 'b t -> bool
          val set_disjoint : 'a t -> 'b t -> bool
          val set_compare : 'a t -> 'b t -> int
          val set_equal : 'a t -> 'b t -> bool
          val find_def : 'a -> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('a -> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> 'a -> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
          val fold2_inter :
            (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> 'c -> 'c) ->
            'a t -> 'b t -> 'c -> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> 'a -> 'a t -> 'a t
          val replace : exn -> key -> 'a -> 'a t -> 'a t
          val keys : 'a t -> key list
          val values : 'a t -> 'a list
          val of_list : (key * 'a) list -> 'a t
          val contains : 'a t -> key -> bool
          val domain : 'a t -> unit t
          val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = 'a Mreg.enumeration
          val val_enum : 'a enumeration -> (key * 'a) option
          val start_enum : 'a t -> 'a enumeration
          val next_enum : 'a enumeration -> 'a enumeration
          val start_ge_enum : key -> 'a t -> 'a enumeration
          val next_ge_enum : key -> 'a enumeration -> 'a enumeration
        end
      type elt = M.key
      type t = unit M.t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val merge : (elt -> bool -> bool -> bool) -> t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val disjoint : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
      val change : (bool -> bool) -> elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
      val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val translate : (elt -> elt) -> t -> t
      val add_new : exn -> elt -> t -> t
      val is_num_elt : int -> t -> bool
      val of_list : elt list -> t
      val contains : t -> elt -> bool
      val add_left : t -> elt -> t
      val remove_left : t -> elt -> t
      val print :
        (Format.formatter -> elt -> unit) -> Format.formatter -> t -> unit
    end
  module Hreg :
    sig
      type key = region
      type !'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_keys : 'a t -> key Seq.t
      val to_seq_values : 'a t -> 'a Seq.t
      val add_seq : 'a t -> (key * 'a) Seq.t -> unit
      val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
      val of_seq : (key * 'a) Seq.t -> 'a t
      val find_def : 'a t -> 'a -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  module Wreg :
    sig
      type key = region
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val find : 'a t -> key -> 'a
      val mem : 'a t -> key -> bool
      val set : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val length : 'a t -> int
      val memoize : int -> (key -> 'a) -> key -> 'a
      val memoize_rec : int -> ((key -> 'a) -> key -> 'a) -> key -> 'a
      val memoize_option : int -> (key option -> 'a) -> key option -> 'a
    end
  module Mpv :
    sig
      type key = pvsymbol
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val set_union : 'a t -> 'a t -> 'a t
      val set_inter : 'a t -> 'b t -> 'a t
      val set_diff : 'a t -> 'b t -> 'a t
      val set_submap : 'a t -> 'b t -> bool
      val set_disjoint : 'a t -> 'b t -> bool
      val set_compare : 'a t -> 'b t -> int
      val set_equal : 'a t -> 'b t -> bool
      val find_def : 'a -> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('a -> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> 'a -> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
      val fold2_inter :
        (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> 'c -> 'c) ->
        'a t -> 'b t -> 'c -> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> 'a -> 'a t -> 'a t
      val replace : exn -> key -> 'a -> 'a t -> 'a t
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val of_list : (key * 'a) list -> 'a t
      val contains : 'a t -> key -> bool
      val domain : 'a t -> unit t
      val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
      val is_num_elt : int -> 'a t -> bool
      type 'a enumeration
      val val_enum : 'a enumeration -> (key * 'a) option
      val start_enum : 'a t -> 'a enumeration
      val next_enum : 'a enumeration -> 'a enumeration
      val start_ge_enum : key -> 'a t -> 'a enumeration
      val next_ge_enum : key -> 'a enumeration -> 'a enumeration
    end
  module Spv :
    sig
      module M :
        sig
          type key = pvsymbol
          type 'a t = 'a Mpv.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> 'a -> 'a t -> 'a t
          val singleton : key -> 'a -> 'a t
          val remove : key -> 'a t -> 'a t
          val merge :
            (key -> 'a option -> 'b option -> 'c option) ->
            'a t -> 'b t -> 'c t
          val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
          val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
          val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val for_all : (key -> 'a -> bool) -> 'a t -> bool
          val exists : (key -> 'a -> bool) -> 'a t -> bool
          val filter : (key -> 'a -> bool) -> 'a t -> 'a t
          val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
          val cardinal : 'a t -> int
          val bindings : 'a t -> (key * 'a) list
          val min_binding : 'a t -> key * 'a
          val max_binding : 'a t -> key * 'a
          val choose : 'a t -> key * 'a
          val split : key -> 'a t -> 'a t * 'a option * 'a t
          val find : key -> 'a t -> 'a
          val map : ('a -> 'b) -> 'a t -> 'b t
          val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val set_union : 'a t -> 'a t -> 'a t
          val set_inter : 'a t -> 'b t -> 'a t
          val set_diff : 'a t -> 'b t -> 'a t
          val set_submap : 'a t -> 'b t -> bool
          val set_disjoint : 'a t -> 'b t -> bool
          val set_compare : 'a t -> 'b t -> int
          val set_equal : 'a t -> 'b t -> bool
          val find_def : 'a -> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('a -> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> 'a -> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
          val fold2_inter :
            (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> 'c -> 'c) ->
            'a t -> 'b t -> 'c -> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> 'a -> 'a t -> 'a t
          val replace : exn -> key -> 'a -> 'a t -> 'a t
          val keys : 'a t -> key list
          val values : 'a t -> 'a list
          val of_list : (key * 'a) list -> 'a t
          val contains : 'a t -> key -> bool
          val domain : 'a t -> unit t
          val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = 'a Mpv.enumeration
          val val_enum : 'a enumeration -> (key * 'a) option
          val start_enum : 'a t -> 'a enumeration
          val next_enum : 'a enumeration -> 'a enumeration
          val start_ge_enum : key -> 'a t -> 'a enumeration
          val next_ge_enum : key -> 'a enumeration -> 'a enumeration
        end
      type elt = M.key
      type t = unit M.t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val merge : (elt -> bool -> bool -> bool) -> t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val disjoint : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
      val change : (bool -> bool) -> elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
      val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val translate : (elt -> elt) -> t -> t
      val add_new : exn -> elt -> t -> t
      val is_num_elt : int -> t -> bool
      val of_list : elt list -> t
      val contains : t -> elt -> bool
      val add_left : t -> elt -> t
      val remove_left : t -> elt -> t
      val print :
        (Format.formatter -> elt -> unit) -> Format.formatter -> t -> unit
    end
  module Hpv :
    sig
      type key = pvsymbol
      type !'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val to_seq : 'a t -> (key * 'a) Seq.t
      val to_seq_keys : 'a t -> key Seq.t
      val to_seq_values : 'a t -> 'a Seq.t
      val add_seq : 'a t -> (key * 'a) Seq.t -> unit
      val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
      val of_seq : (key * 'a) Seq.t -> 'a t
      val find_def : 'a t -> 'a -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val memo : int -> (key -> 'a) -> key -> 'a
      val is_empty : 'a t -> bool
    end
  module Wpv :
    sig
      type key = pvsymbol
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val find : 'a t -> key -> 'a
      val mem : 'a t -> key -> bool
      val set : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val length : 'a t -> int
      val memoize : int -> (key -> 'a) -> key -> 'a
      val memoize_rec : int -> ((key -> 'a) -> key -> 'a) -> key -> 'a
      val memoize_option : int -> (key option -> 'a) -> key option -> 'a
    end
  val its_compare : Ity.itysymbol -> Ity.itysymbol -> int
  val ity_compare : Ity.ity -> Ity.ity -> int
  val reg_compare : Ity.region -> Ity.region -> int
  val pv_compare : Ity.pvsymbol -> Ity.pvsymbol -> int
  val its_equal : Ity.itysymbol -> Ity.itysymbol -> bool
  val ity_equal : Ity.ity -> Ity.ity -> bool
  val reg_equal : Ity.region -> Ity.region -> bool
  val pv_equal : Ity.pvsymbol -> Ity.pvsymbol -> bool
  val its_hash : Ity.itysymbol -> int
  val ity_hash : Ity.ity -> int
  val reg_hash : Ity.region -> int
  val pv_hash : Ity.pvsymbol -> int
  exception DuplicateRegion of Ity.region
  exception UnboundRegion of Ity.region
  val create_plain_record_itysymbol :
    priv:bool ->
    mut:bool ->
    Ident.preid ->
    Ty.tvsymbol list -> bool Ity.Mpv.t -> Term.term list -> Ity.itysymbol
  val create_plain_variant_itysymbol :
    Ident.preid -> Ty.tvsymbol list -> Ity.Spv.t list -> Ity.itysymbol
  val create_rec_itysymbol : Ident.preid -> Ty.tvsymbol list -> Ity.itysymbol
  val create_alias_itysymbol :
    Ident.preid -> Ty.tvsymbol list -> Ity.ity -> Ity.itysymbol
  val create_range_itysymbol :
    Ident.preid -> Number.int_range -> Ity.itysymbol
  val create_float_itysymbol :
    Ident.preid -> Number.float_format -> Ity.itysymbol
  val restore_its : Ty.tysymbol -> Ity.itysymbol
  val its_pure : Ity.itysymbol -> bool
  val ity_closed : Ity.ity -> bool
  val ity_fragile : Ity.ity -> bool
  exception BadItyArity of Ity.itysymbol * int
  exception BadRegArity of Ity.itysymbol * int
  val create_region :
    Ident.preid ->
    Ity.itysymbol -> Ity.ity list -> Ity.ity list -> Ity.region
  val ity_app : Ity.itysymbol -> Ity.ity list -> Ity.ity list -> Ity.ity
  val ity_app_pure : Ity.itysymbol -> Ity.ity list -> Ity.ity list -> Ity.ity
  val ity_reg : Ity.region -> Ity.ity
  val ity_var : Ty.tvsymbol -> Ity.ity
  val ity_purify : Ity.ity -> Ity.ity
  val ity_of_ty : Ty.ty -> Ity.ity
  val ity_of_ty_pure : Ty.ty -> Ity.ity
  val ty_of_ity : Ity.ity -> Ty.ty
  val ity_fold : ('a -> Ity.ity -> 'a) -> 'a -> Ity.ity -> 'a
  val reg_fold : ('a -> Ity.ity -> 'a) -> 'a -> Ity.region -> 'a
  val ity_s_fold : ('a -> Ity.itysymbol -> 'a) -> 'a -> Ity.ity -> 'a
  val reg_s_fold : ('a -> Ity.itysymbol -> 'a) -> 'a -> Ity.region -> 'a
  val ity_v_fold : ('a -> Ty.tvsymbol -> 'a) -> 'a -> Ity.ity -> 'a
  val reg_v_fold : ('a -> Ty.tvsymbol -> 'a) -> 'a -> Ity.region -> 'a
  val ity_freevars : Ty.Stv.t -> Ity.ity -> Ty.Stv.t
  val reg_freevars : Ty.Stv.t -> Ity.region -> Ty.Stv.t
  val ity_v_occurs : Ty.tvsymbol -> Ity.ity -> bool
  val reg_v_occurs : Ty.tvsymbol -> Ity.region -> bool
  val ity_r_fold : ('a -> Ity.region -> 'a) -> 'a -> Ity.ity -> 'a
  val reg_r_fold : ('a -> Ity.region -> 'a) -> 'a -> Ity.region -> 'a
  val ity_freeregs : Ity.Sreg.t -> Ity.ity -> Ity.Sreg.t
  val reg_freeregs : Ity.Sreg.t -> Ity.region -> Ity.Sreg.t
  val ity_r_occurs : Ity.region -> Ity.ity -> bool
  val reg_r_occurs : Ity.region -> Ity.region -> bool
  val ity_exp_fold : ('a -> Ity.region -> 'a) -> 'a -> Ity.ity -> 'a
  val reg_exp_fold : ('a -> Ity.region -> 'a) -> 'a -> Ity.region -> 'a
  val ity_rch_fold : ('a -> Ity.region -> 'a) -> 'a -> Ity.ity -> 'a
  val reg_rch_fold : ('a -> Ity.region -> 'a) -> 'a -> Ity.region -> 'a
  val ity_r_reachable : Ity.region -> Ity.ity -> bool
  val reg_r_reachable : Ity.region -> Ity.region -> bool
  val ity_r_stale : Ity.Sreg.t -> Ity.Sreg.t -> Ity.ity -> bool
  val reg_r_stale : Ity.Sreg.t -> Ity.Sreg.t -> Ity.region -> bool
  val ity_frz_regs : Ity.Sreg.t -> Ity.ity -> Ity.Sreg.t
  val ts_unit : Ty.tysymbol
  val ty_unit : Ty.ty
  val its_int : Ity.itysymbol
  val its_real : Ity.itysymbol
  val its_bool : Ity.itysymbol
  val its_str : Ity.itysymbol
  val its_unit : Ity.itysymbol
  val its_func : Ity.itysymbol
  val ity_int : Ity.ity
  val ity_real : Ity.ity
  val ity_bool : Ity.ity
  val ity_str : Ity.ity
  val ity_unit : Ity.ity
  val ity_func : Ity.ity -> Ity.ity -> Ity.ity
  val ity_pred : Ity.ity -> Ity.ity
  val its_tuple : int -> Ity.itysymbol
  val ity_tuple : Ity.ity list -> Ity.ity
  type ity_subst = private {
    isb_var : Ity.ity Ty.Mtv.t;
    isb_reg : Ity.ity Ity.Mreg.t;
  }
  exception TypeMismatch of Ity.ity * Ity.ity * Ity.ity_subst
  val isb_empty : Ity.ity_subst
  val ity_match : Ity.ity_subst -> Ity.ity -> Ity.ity -> Ity.ity_subst
  val reg_match : Ity.ity_subst -> Ity.region -> Ity.ity -> Ity.ity_subst
  val its_match_args : Ity.itysymbol -> Ity.ity list -> Ity.ity_subst
  val its_match_regs :
    Ity.itysymbol -> Ity.ity list -> Ity.ity list -> Ity.ity_subst
  val ity_freeze : Ity.ity_subst -> Ity.ity -> Ity.ity_subst
  val reg_freeze : Ity.ity_subst -> Ity.region -> Ity.ity_subst
  val ity_equal_check : Ity.ity -> Ity.ity -> unit
  val reg_equal_check : Ity.region -> Ity.region -> unit
  val ity_full_inst : Ity.ity_subst -> Ity.ity -> Ity.ity
  val reg_full_inst : Ity.ity_subst -> Ity.region -> Ity.ity
  val create_pvsymbol : Ident.preid -> ?ghost:bool -> Ity.ity -> Ity.pvsymbol
  val restore_pv : Term.vsymbol -> Ity.pvsymbol
  val t_freepvs : Ity.Spv.t -> Term.term -> Ity.Spv.t
  val pvs_of_vss : Ity.Spv.t -> 'a Term.Mvs.t -> Ity.Spv.t
  type mask = MaskVisible | MaskTuple of Ity.mask list | MaskGhost
  val mask_ghost : Ity.mask -> bool
  val mask_of_pv : Ity.pvsymbol -> Ity.mask
  val mask_union : Ity.mask -> Ity.mask -> Ity.mask
  val mask_equal : Ity.mask -> Ity.mask -> bool
  val mask_spill : Ity.mask -> Ity.mask -> bool
  type xsymbol = private {
    xs_name : Ident.ident;
    xs_ity : Ity.ity;
    xs_mask : Ity.mask;
  }
  module Mxs :
    sig
      type key = xsymbol
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val set_union : 'a t -> 'a t -> 'a t
      val set_inter : 'a t -> 'b t -> 'a t
      val set_diff : 'a t -> 'b t -> 'a t
      val set_submap : 'a t -> 'b t -> bool
      val set_disjoint : 'a t -> 'b t -> bool
      val set_compare : 'a t -> 'b t -> int
      val set_equal : 'a t -> 'b t -> bool
      val find_def : 'a -> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('a -> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> 'a -> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
      val fold2_inter :
        (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> 'c -> 'c) ->
        'a t -> 'b t -> 'c -> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> 'a -> 'a t -> 'a t
      val replace : exn -> key -> 'a -> 'a t -> 'a t
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val of_list : (key * 'a) list -> 'a t
      val contains : 'a t -> key -> bool
      val domain : 'a t -> unit t
      val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
      val is_num_elt : int -> 'a t -> bool
      type 'a enumeration
      val val_enum : 'a enumeration -> (key * 'a) option
      val start_enum : 'a t -> 'a enumeration
      val next_enum : 'a enumeration -> 'a enumeration
      val start_ge_enum : key -> 'a t -> 'a enumeration
      val next_ge_enum : key -> 'a enumeration -> 'a enumeration
    end
  module Sxs :
    sig
      module M :
        sig
          type key = xsymbol
          type 'a t = 'a Mxs.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> 'a -> 'a t -> 'a t
          val singleton : key -> 'a -> 'a t
          val remove : key -> 'a t -> 'a t
          val merge :
            (key -> 'a option -> 'b option -> 'c option) ->
            'a t -> 'b t -> 'c t
          val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
          val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
          val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val for_all : (key -> 'a -> bool) -> 'a t -> bool
          val exists : (key -> 'a -> bool) -> 'a t -> bool
          val filter : (key -> 'a -> bool) -> 'a t -> 'a t
          val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
          val cardinal : 'a t -> int
          val bindings : 'a t -> (key * 'a) list
          val min_binding : 'a t -> key * 'a
          val max_binding : 'a t -> key * 'a
          val choose : 'a t -> key * 'a
          val split : key -> 'a t -> 'a t * 'a option * 'a t
          val find : key -> 'a t -> 'a
          val map : ('a -> 'b) -> 'a t -> 'b t
          val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
          val set_union : 'a t -> 'a t -> 'a t
          val set_inter : 'a t -> 'b t -> 'a t
          val set_diff : 'a t -> 'b t -> 'a t
          val set_submap : 'a t -> 'b t -> bool
          val set_disjoint : 'a t -> 'b t -> bool
          val set_compare : 'a t -> 'b t -> int
          val set_equal : 'a t -> 'b t -> bool
          val find_def : 'a -> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('a -> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> 'a -> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
          val fold2_inter :
            (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> 'c -> 'c) ->
            'a t -> 'b t -> 'c -> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> 'a -> 'a t -> 'a t
          val replace : exn -> key -> 'a -> 'a t -> 'a t
          val keys : 'a t -> key list
          val values : 'a t -> 'a list
          val of_list : (key * 'a) list -> 'a t
          val contains : 'a t -> key -> bool
          val domain : 'a t -> unit t
          val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = 'a Mxs.enumeration
          val val_enum : 'a enumeration -> (key * 'a) option
          val start_enum : 'a t -> 'a enumeration
          val next_enum : 'a enumeration -> 'a enumeration
          val start_ge_enum : key -> 'a t -> 'a enumeration
          val next_ge_enum : key -> 'a enumeration -> 'a enumeration
        end
      type elt = M.key
      type t = unit M.t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val merge : (elt -> bool -> bool -> bool) -> t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val disjoint : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
      val change : (bool -> bool) -> elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
      val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
      val translate : (elt -> elt) -> t -> t
      val add_new : exn -> elt -> t -> t
      val is_num_elt : int -> t -> bool
      val of_list : elt list -> t
      val contains : t -> elt -> bool
      val add_left : t -> elt -> t
      val remove_left : t -> elt -> t
      val print :
        (Format.formatter -> elt -> unit) -> Format.formatter -> t -> unit
    end
  val xs_compare : Ity.xsymbol -> Ity.xsymbol -> int
  val xs_equal : Ity.xsymbol -> Ity.xsymbol -> bool
  val xs_hash : Ity.xsymbol -> int
  val create_xsymbol :
    Ident.preid -> ?mask:Ity.mask -> Ity.ity -> Ity.xsymbol
  exception IllegalSnapshot of Ity.ity
  exception IllegalAlias of Ity.region
  exception AssignPrivate of Ity.region
  exception AssignSnapshot of Ity.ity
  exception WriteImmutable of Ity.region * Ity.pvsymbol
  exception IllegalUpdate of Ity.pvsymbol * Ity.region
  exception StaleVariable of Ity.pvsymbol * Ity.region
  exception BadGhostWrite of Ity.pvsymbol * Ity.region
  exception DuplicateField of Ity.region * Ity.pvsymbol
  exception IllegalAssign of Ity.region * Ity.region * Ity.region
  exception ImpureVariable of Ty.tvsymbol * Ity.ity
  exception GhostDivergence
  type oneway = Total | Partial | Diverges
  val total : Ity.oneway -> bool
  val partial : Ity.oneway -> bool
  val diverges : Ity.oneway -> bool
  type effect = private {
    eff_reads : Ity.Spv.t;
    eff_writes : Ity.Spv.t Ity.Mreg.t;
    eff_taints : Ity.Sreg.t;
    eff_covers : Ity.Sreg.t;
    eff_resets : Ity.Sreg.t;
    eff_raises : Ity.Sxs.t;
    eff_spoils : Ty.Stv.t;
    eff_oneway : Ity.oneway;
    eff_ghost : bool;
  }
  val eff_empty : Ity.effect
  val eff_equal : Ity.effect -> Ity.effect -> bool
  val eff_pure : Ity.effect -> bool
  val eff_read : Ity.Spv.t -> Ity.effect
  val eff_write : Ity.Spv.t -> Ity.Spv.t Ity.Mreg.t -> Ity.effect
  val eff_assign :
    (Ity.pvsymbol * Ity.pvsymbol * Ity.pvsymbol) list -> Ity.effect
  val eff_read_pre : Ity.Spv.t -> Ity.effect -> Ity.effect
  val eff_read_post : Ity.effect -> Ity.Spv.t -> Ity.effect
  val eff_bind : Ity.Spv.t -> Ity.effect -> Ity.effect
  val eff_read_single : Ity.pvsymbol -> Ity.effect
  val eff_read_single_pre : Ity.pvsymbol -> Ity.effect -> Ity.effect
  val eff_read_single_post : Ity.effect -> Ity.pvsymbol -> Ity.effect
  val eff_bind_single : Ity.pvsymbol -> Ity.effect -> Ity.effect
  val eff_reset : Ity.effect -> Ity.Sreg.t -> Ity.effect
  val eff_reset_overwritten : Ity.effect -> Ity.effect
  val eff_raise : Ity.effect -> Ity.xsymbol -> Ity.effect
  val eff_catch : Ity.effect -> Ity.xsymbol -> Ity.effect
  val eff_spoil : Ity.effect -> Ity.ity -> Ity.effect
  val eff_partial : Ity.effect -> Ity.effect
  val eff_diverge : Ity.effect -> Ity.effect
  val eff_ghostify : bool -> Ity.effect -> Ity.effect
  val eff_ghostify_weak : bool -> Ity.effect -> Ity.effect
  val eff_union_seq : Ity.effect -> Ity.effect -> Ity.effect
  val eff_union_par : Ity.effect -> Ity.effect -> Ity.effect
  val eff_fusion : Ity.effect -> Ity.effect -> Ity.effect
  val mask_adjust : Ity.effect -> Ity.ity -> Ity.mask -> Ity.mask
  val eff_escape : Ity.effect -> Ity.ity -> Ity.Sity.t
  val ity_affected : 'a Ity.Mreg.t -> Ity.ity -> bool
  val pv_affected : 'a Ity.Mreg.t -> Ity.pvsymbol -> bool
  val pvs_affected : 'a Ity.Mreg.t -> Ity.Spv.t -> Ity.Spv.t
  type pre = Term.term
  type post = Term.term
  val open_post : Ity.post -> Term.vsymbol * Term.term
  val open_post_with : Term.term -> Ity.post -> Term.term
  val clone_post_result :
    ?loc:Loc.position -> ?attrs:Ident.Sattr.t -> Ity.post -> Ident.preid
  val result_id :
    ?loc:Loc.position ->
    ?attrs:Ident.Sattr.t -> ?ql:Ity.post list -> unit -> Ident.preid
  val create_post : Term.vsymbol -> Term.term -> Ity.post
  val annot_attr : Ident.attribute
  val break_attr : Ident.attribute
  type cty = private {
    cty_args : Ity.pvsymbol list;
    cty_pre : Ity.pre list;
    cty_post : Ity.post list;
    cty_xpost : Ity.post list Ity.Mxs.t;
    cty_oldies : Ity.pvsymbol Ity.Mpv.t;
    cty_effect : Ity.effect;
    cty_result : Ity.ity;
    cty_mask : Ity.mask;
    cty_freeze : Ity.ity_subst;
  }
  val create_cty :
    ?mask:Ity.mask ->
    Ity.pvsymbol list ->
    Ity.pre list ->
    Ity.post list ->
    Ity.post list Ity.Mxs.t ->
    Ity.pvsymbol Ity.Mpv.t -> Ity.effect -> Ity.ity -> Ity.cty
  val create_cty_defensive :
    ?mask:Ity.mask ->
    Ity.pvsymbol list ->
    Ity.pre list ->
    Ity.post list ->
    Ity.post list Ity.Mxs.t ->
    Ity.pvsymbol Ity.Mpv.t -> Ity.effect -> Ity.ity -> Ity.cty
  val cty_apply :
    Ity.cty -> Ity.pvsymbol list -> Ity.ity list -> Ity.ity -> Ity.cty
  val cty_tuple : Ity.pvsymbol list -> Ity.cty
  val cty_exec : Ity.cty -> Ity.cty
  val cty_exec_post : Ity.cty -> Ity.post list
  val cty_ghost : Ity.cty -> bool
  val cty_pure : Ity.cty -> bool
  val cty_ghostify : bool -> Ity.cty -> Ity.cty
  val cty_reads : Ity.cty -> Ity.Spv.t
  val cty_read_pre : Ity.Spv.t -> Ity.cty -> Ity.cty
  val cty_read_post : Ity.cty -> Ity.Spv.t -> Ity.cty
  val cty_add_pre : Ity.pre list -> Ity.cty -> Ity.cty
  val cty_add_post : Ity.cty -> Ity.post list -> Ity.cty
  val forget_reg : Ity.region -> unit
  val forget_pv : Ity.pvsymbol -> unit
  val forget_xs : Ity.xsymbol -> unit
  val forget_cty : Ity.cty -> unit
  val print_its : Stdlib.Format.formatter -> Ity.itysymbol -> unit
  val print_reg : Stdlib.Format.formatter -> Ity.region -> unit
  val print_reg_name : Stdlib.Format.formatter -> Ity.region -> unit
  val print_ity : Stdlib.Format.formatter -> Ity.ity -> unit
  val print_ity_full : Stdlib.Format.formatter -> Ity.ity -> unit
  val print_xs : Stdlib.Format.formatter -> Ity.xsymbol -> unit
  val print_pv : Stdlib.Format.formatter -> Ity.pvsymbol -> unit
  val print_pvty : Stdlib.Format.formatter -> Ity.pvsymbol -> unit
  val print_cty : Stdlib.Format.formatter -> Ity.cty -> unit
  val print_spec :
    Ity.pvsymbol list ->
    Ity.pre list ->
    Ity.post list ->
    Ity.post list Ity.Mxs.t ->
    Ity.pvsymbol Ity.Mpv.t ->
    Ity.effect -> Stdlib.Format.formatter -> Ity.ity option -> unit
end