Psmt2Frontend.Smtlib_typed_env
module SMap : sig ... end
type env = {
sorts : ((int * int) * (string -> (Smtlib_ty.ty list * int list) -> Smtlib_ty.desc)) SMap.t; |
funs : fun_def list SMap.t; |
par_funs : (string list -> fun_def) list SMap.t; |
constructors : int SMap.t SMap.t; |
}
val empty : unit -> env
val get_arit : 'a Smtlib_syntax.data -> string -> int
val get_index : Smtlib_syntax.index_aux Smtlib_syntax.data -> string
val get_identifier : Smtlib_syntax.identifier_aux Smtlib_syntax.data -> Smtlib_syntax.symbol * string list
val check_identifier : Smtlib_syntax.identifier_aux Smtlib_syntax.data -> int -> unit
val check_sort_already_exist : (env * 'a SMap.t) -> SMap.key Smtlib_syntax.data -> unit
val check_sort_exist : (env * 'a SMap.t) -> SMap.key Smtlib_syntax.data -> unit
val mk_sort_definition : int -> 'a -> bool -> (int * 'a) * (string -> (Smtlib_ty.ty list * 'b) -> Smtlib_ty.desc)
val mk_sort : (env * 'a SMap.t) -> SMap.key Smtlib_syntax.data -> ((int * int) * (string -> (Smtlib_ty.ty list * int list) -> Smtlib_ty.desc)) -> env
val mk_sort_decl : (env * 'a SMap.t) -> SMap.key Smtlib_syntax.data -> string -> bool -> env
val find_sort_def : env -> SMap.key Smtlib_syntax.data -> (int * int) * (string -> (Smtlib_ty.ty list * int list) -> Smtlib_ty.desc)
val add_sorts : env -> (SMap.key * ((int * int) * (string -> (Smtlib_ty.ty list * int list) -> Smtlib_ty.desc))) list -> env
val find_sort_symb : (env * Smtlib_ty.ty SMap.t) -> SMap.key Smtlib_syntax.data -> Smtlib_ty.ty list -> int list -> Smtlib_ty.ty
val find_sort : (env * Smtlib_ty.ty SMap.t) -> Smtlib_syntax.sort_aux Smtlib_syntax.data -> Smtlib_ty.ty
val extract_arit_ty_assoc : Smtlib_ty.ty -> int * Smtlib_ty.ty
val compare_fun_assoc : ('a * Smtlib_ty.ty Smtlib_ty.SMap.t) -> 'b Smtlib_syntax.data -> Smtlib_ty.ty -> Smtlib_ty.ty -> assoc -> Smtlib_ty.ty option
val compare_fun_def : ('a * Smtlib_ty.ty Smtlib_ty.SMap.t) -> 'b Smtlib_syntax.data -> Smtlib_ty.ty -> fun_def list -> bool -> Smtlib_ty.ty option
val find_fun : (env * Smtlib_ty.ty Smtlib_ty.SMap.t) -> SMap.key Smtlib_syntax.data -> Smtlib_ty.ty list -> string list -> bool -> Smtlib_ty.ty
val check_fun_exists : (env * Smtlib_ty.ty Smtlib_ty.SMap.t) -> SMap.key Smtlib_syntax.data -> Smtlib_ty.ty list -> bool -> unit
val mk_fun_ty : Smtlib_ty.ty list -> Smtlib_ty.ty -> assoc option -> fun_def
val mk_fun_ty_arg : Smtlib_ty.ty list -> Smtlib_ty.ty -> assoc option -> 'a -> 'b -> fun_def
val add_fun_def : (env * Smtlib_ty.ty Smtlib_ty.SMap.t) -> SMap.key Smtlib_syntax.data -> Smtlib_ty.ty list -> Smtlib_ty.ty -> assoc option -> env
val find_simpl_sort_symb : (env * 'a) -> SMap.key Smtlib_syntax.data -> Smtlib_ty.ty list -> Smtlib_ty.ty
val extract_pars : Smtlib_ty.ty SMap.t -> SMap.key Smtlib_syntax.data list -> Smtlib_ty.ty SMap.t
val mk_const : (env * Smtlib_ty.ty SMap.t) -> (SMap.key Smtlib_syntax.data * SMap.key Smtlib_syntax.data list * Smtlib_syntax.sort_aux Smtlib_syntax.data) -> env
val mk_fun_def : (env * Smtlib_ty.ty SMap.t) -> (SMap.key Smtlib_syntax.data * Smtlib_syntax.sort_aux Smtlib_syntax.data list * Smtlib_syntax.sort_aux Smtlib_syntax.data) -> env
val mk_fun_dec : (env * Smtlib_ty.ty SMap.t) -> (SMap.key Smtlib_syntax.data * (SMap.key Smtlib_syntax.data list * Smtlib_syntax.sort_aux Smtlib_syntax.data list * Smtlib_syntax.sort_aux Smtlib_syntax.data)) -> env
val find_sort_name : Smtlib_syntax.sort_aux Smtlib_syntax.data -> Smtlib_syntax.symbol * string list
val mk_sort_def : (env * Smtlib_ty.ty SMap.t) -> SMap.key Smtlib_syntax.data -> SMap.key Smtlib_syntax.data list -> Smtlib_syntax.sort_aux Smtlib_syntax.data -> env
val find_constr : env -> SMap.key Smtlib_syntax.data -> Smtlib_ty.ty
val mk_constr_decs : (env * Smtlib_ty.ty SMap.t) -> SMap.key Smtlib_syntax.data -> Smtlib_ty.ty -> (SMap.key Smtlib_syntax.data * (SMap.key Smtlib_syntax.data * Smtlib_syntax.sort_aux Smtlib_syntax.data) list) list -> env
val mk_dt_dec : (env * Smtlib_ty.ty SMap.t) -> SMap.key Smtlib_syntax.data -> (SMap.key Smtlib_syntax.data list * (SMap.key Smtlib_syntax.data * (SMap.key Smtlib_syntax.data * Smtlib_syntax.sort_aux Smtlib_syntax.data) list) list) -> env
val mk_datatype : (env * Smtlib_ty.ty SMap.t) -> SMap.key Smtlib_syntax.data -> SMap.key Smtlib_syntax.data list -> (SMap.key Smtlib_syntax.data * (SMap.key Smtlib_syntax.data * Smtlib_syntax.sort_aux Smtlib_syntax.data) list) list -> env
val mk_datatypes : (env * Smtlib_ty.ty SMap.t) -> (SMap.key Smtlib_syntax.data * string) list -> (SMap.key Smtlib_syntax.data list * (SMap.key Smtlib_syntax.data * (SMap.key Smtlib_syntax.data * Smtlib_syntax.sort_aux Smtlib_syntax.data) list) list) list -> env