sig
  type model_element_kind =
      Result
    | Call_result of Loc.position
    | Old
    | At of string
    | Loop_before
    | Loop_previous_iteration
    | Loop_current_iteration
    | Error_message
    | Other
  val print_model_kind :
    Stdlib.Format.formatter -> Model_parser.model_element_kind -> unit
  type concrete_syntax_int = {
    int_value : Number.int_constant;
    int_verbatim : string;
  }
  type concrete_syntax_bv = {
    bv_value : BigInt.t;
    bv_length : int;
    bv_verbatim : string;
  }
  type concrete_syntax_real = {
    real_value : Number.real_constant;
    real_verbatim : string;
  }
  type concrete_syntax_frac = {
    frac_num : Model_parser.concrete_syntax_real;
    frac_den : Model_parser.concrete_syntax_real;
    frac_verbatim : string;
  }
  type concrete_syntax_float_value =
      Plus_infinity
    | Minus_infinity
    | Plus_zero
    | Minus_zero
    | NaN
    | Float_number of { float_sign : Model_parser.concrete_syntax_bv;
        float_exp : Model_parser.concrete_syntax_bv;
        float_mant : Model_parser.concrete_syntax_bv; float_hex : string;
      }
  type concrete_syntax_float = {
    float_exp_size : int;
    float_significand_size : int;
    float_val : Model_parser.concrete_syntax_float_value;
  }
  type concrete_syntax_constant =
      Boolean of bool
    | String of string
    | Integer of Model_parser.concrete_syntax_int
    | Real of Model_parser.concrete_syntax_real
    | Float of Model_parser.concrete_syntax_float
    | BitVector of Model_parser.concrete_syntax_bv
    | Fraction of Model_parser.concrete_syntax_frac
  type concrete_syntax_quant = Forall | Exists
  type concrete_syntax_binop = And | Or | Implies | Iff
  type concrete_syntax_funlit_elts = {
    elts_index : Model_parser.concrete_syntax_term;
    elts_value : Model_parser.concrete_syntax_term;
  }
  and concrete_syntax_funlit = {
    elts : Model_parser.concrete_syntax_funlit_elts list;
    others : Model_parser.concrete_syntax_term;
  }
  and concrete_syntax_fun = {
    args : string list;
    body : Model_parser.concrete_syntax_term;
  }
  and concrete_syntax_term =
      Var of string
    | Const of Model_parser.concrete_syntax_constant
    | Apply of string * Model_parser.concrete_syntax_term list
    | If of Model_parser.concrete_syntax_term *
        Model_parser.concrete_syntax_term * Model_parser.concrete_syntax_term
    | Epsilon of string * Model_parser.concrete_syntax_term
    | Quant of Model_parser.concrete_syntax_quant * string list *
        Model_parser.concrete_syntax_term
    | Binop of Model_parser.concrete_syntax_binop *
        Model_parser.concrete_syntax_term * Model_parser.concrete_syntax_term
    | Not of Model_parser.concrete_syntax_term
    | Function of Model_parser.concrete_syntax_fun
    | FunctionLiteral of Model_parser.concrete_syntax_funlit
    | Record of (string * Model_parser.concrete_syntax_term) list
    | Proj of (string * Model_parser.concrete_syntax_term)
    | Let of (string * Model_parser.concrete_syntax_term) list *
        Model_parser.concrete_syntax_term
  val print_concrete_term :
    Stdlib.Format.formatter -> Model_parser.concrete_syntax_term -> unit
  val concrete_var_from_vs :
    Term.vsymbol -> Model_parser.concrete_syntax_term
  val concrete_const_bool : bool -> Model_parser.concrete_syntax_term
  val concrete_apply_from_ls :
    Term.lsymbol ->
    Model_parser.concrete_syntax_term list ->
    Model_parser.concrete_syntax_term
  val concrete_apply_equ :
    Model_parser.concrete_syntax_term ->
    Model_parser.concrete_syntax_term -> Model_parser.concrete_syntax_term
  val subst_concrete_term :
    Model_parser.concrete_syntax_term Wstdlib.Mstr.t ->
    Model_parser.concrete_syntax_term -> Model_parser.concrete_syntax_term
  val t_and_l_concrete :
    Model_parser.concrete_syntax_term list ->
    Model_parser.concrete_syntax_term
  type model_element = {
    me_kind : Model_parser.model_element_kind;
    me_value : Term.term;
    me_concrete_value : Model_parser.concrete_syntax_term;
    me_location : Loc.position option;
    me_attrs : Ident.Sattr.t;
    me_lsymbol : Term.lsymbol;
  }
  val create_model_element :
    value:Term.term ->
    concrete_value:Model_parser.concrete_syntax_term ->
    oloc:Loc.position option ->
    attrs:Ident.Sattr.t -> lsymbol:Term.lsymbol -> Model_parser.model_element
  val get_lsymbol_or_model_trace_name : Model_parser.model_element -> string
  type model
  val is_model_empty : Model_parser.model -> bool
  val empty_model : Model_parser.model
  val set_model_files :
    Model_parser.model ->
    Model_parser.model_element list Wstdlib.Mint.t Wstdlib.Mstr.t ->
    Model_parser.model
  val get_model_elements :
    Model_parser.model -> Model_parser.model_element list
  val get_model_term_loc : Model_parser.model -> Loc.position option
  val get_model_term_attrs : Model_parser.model -> Ident.Sattr.t
  val search_model_element_for_id :
    Model_parser.model ->
    ?loc:Loc.position -> Ident.ident -> Model_parser.model_element option
  val search_model_element_call_result :
    Model_parser.model ->
    Expr.expr_id option -> Model_parser.model_element option
  val json_model : Model_parser.model -> Json_base.json
  val print_model :
    print_attrs:bool -> Stdlib.Format.formatter -> Model_parser.model -> unit
  val interleave_with_source :
    print_attrs:bool ->
    ?start_comment:string ->
    ?end_comment:string ->
    Model_parser.model ->
    rel_filename:string ->
    source_code:string ->
    locations:(Loc.position * 'a) list -> string * (Loc.position * 'a) list
  val model_for_positions_and_decls :
    Model_parser.model -> positions:Loc.position list -> Model_parser.model
  class clean :
    object
      method apply :
        string ->
        Model_parser.concrete_syntax_term list ->
        Model_parser.concrete_syntax_term option
      method binop :
        Model_parser.concrete_syntax_binop ->
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term option
      method bitvector :
        Model_parser.concrete_syntax_bv ->
        Model_parser.concrete_syntax_term option
      method boolean : bool -> Model_parser.concrete_syntax_term option
      method cond :
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term option
      method const :
        Model_parser.concrete_syntax_constant ->
        Model_parser.concrete_syntax_term option
      method element :
        Model_parser.model_element -> Model_parser.model_element option
      method epsilon :
        string ->
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term option
      method float :
        Model_parser.concrete_syntax_float ->
        Model_parser.concrete_syntax_term option
      method fraction :
        Model_parser.concrete_syntax_frac ->
        Model_parser.concrete_syntax_term option
      method func :
        string list ->
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term option
      method funliteral :
        Model_parser.concrete_syntax_funlit_elts list ->
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term option
      method integer :
        Model_parser.concrete_syntax_int ->
        Model_parser.concrete_syntax_term option
      method lett :
        (string * Model_parser.concrete_syntax_term) list ->
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term option
      method model : Model_parser.model -> Model_parser.model
      method neg :
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term option
      method proj :
        string ->
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term option
      method quant :
        Model_parser.concrete_syntax_quant ->
        string list ->
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term option
      method real :
        Model_parser.concrete_syntax_real ->
        Model_parser.concrete_syntax_term option
      method record :
        (string * Model_parser.concrete_syntax_term) list ->
        Model_parser.concrete_syntax_term option
      method string : string -> Model_parser.concrete_syntax_term option
      method value :
        Model_parser.concrete_syntax_term ->
        Model_parser.concrete_syntax_term option
      method var : string -> Model_parser.concrete_syntax_term option
    end
  val clean_model :
    #Model_parser.clean -> Model_parser.model -> Model_parser.model
  type model_parser = Printer.printing_info -> string -> Model_parser.model
  type raw_model_parser =
      Printer.printing_info -> string -> Model_parser.model_element list
  val register_remove_field :
    (Ident.Sattr.t * Term.term * Model_parser.concrete_syntax_term ->
     Ident.Sattr.t * Term.term * Model_parser.concrete_syntax_term) ->
    unit
  val register_model_parser :
    desc:Pp.formatted -> string -> Model_parser.raw_model_parser -> unit
  val lookup_model_parser : string -> Model_parser.model_parser
  val list_model_parsers : unit -> (string * Pp.formatted) list
end