Psmt2Frontend.Smtlib_typed_logic
type th_def = {
sorts : (string * ((int * int) * (string -> (Smtlib_ty.ty list * int list) -> Smtlib_ty.desc))) list; |
funs : (string * Smtlib_typed_env.fun_def) list; |
par_funs : (string * (string list -> Smtlib_typed_env.fun_def)) list; |
}
val new_fun : Smtlib_ty.ty list -> Smtlib_ty.ty -> Smtlib_typed_env.assoc option -> Smtlib_typed_env.fun_def
val core : th_def
val ints : th_def
val reals : th_def
val reals_ints : th_def
val arrays : th_def
val floating_point : th_def
val bit_vectors : th_def
val add_theories : Smtlib_typed_env.env -> theory list -> Smtlib_typed_env.env
val set_logic : Smtlib_typed_env.env -> string Smtlib_syntax.data -> Smtlib_typed_env.env