Module 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;
}
type theory =
| Core
| Ints
| Reals
| Reals_Ints
| FloatingPoint
| Arrays
| BitVectors
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 contains : string -> string -> bool