sig
  module MIL :
    sig
      type key = int list
      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
    end
  type value =
      Term of Term.t
    | Lambda of Term.lambda
    | Map of Term.t Model.MIL.t
  type t = Model.value Var.VarHashtbl.t
  type path = Model.value list StateVar.StateVarHashtbl.t
  val equal_value : Model.value -> Model.value -> bool
  val path_offset : Numeral.t
  val pp_print_value :
    ?as_type:Type.t -> Format.formatter -> Model.value -> unit
  val pp_print_value_xml :
    ?as_type:Type.t -> Format.formatter -> Model.value -> unit
  val pp_print_model : Format.formatter -> Model.t -> unit
  val pp_print_path : Format.formatter -> Model.path -> unit
  val create : int -> Model.t
  val create_path : int -> Model.path
  val import_value : Model.value -> Model.value
  val of_list : (Var.t * Model.value) list -> Model.t
  val to_list : Model.t -> (Var.t * Model.value) list
  val path_to_list : Model.path -> (StateVar.t * Model.value list) list
  val path_of_list : (StateVar.t * Model.value list) list -> Model.path
  val path_of_term_list : (StateVar.t * Term.t list) list -> Model.path
  val path_from_model : StateVar.t list -> Model.t -> Numeral.t -> Model.path
  val path_length : Model.path -> int
  val model_at_k_of_path : Model.path -> Numeral.t -> Model.t
  val models_of_path : Model.path -> Model.t list
  val exists_on_path : (Model.t -> bool) -> Model.path -> bool
  val for_all_on_path : (Model.t -> bool) -> Model.path -> bool
  val bump_var : Numeral.t -> Model.t -> Model.t
  val set_var_offset : Numeral.t -> Model.t -> Model.t
  val merge : Model.t -> Model.t -> Model.t
  val bump_and_merge : Numeral.t -> Model.t -> Model.t -> Model.t
  val dimension_of_map : Term.t Model.MIL.t -> int list
end