Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
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 * 'b) * (string -> (Smtlib_ty.ty list * 'c) -> 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