package psmt2-frontend

  1. Overview
  2. Docs
type th_def = {
  1. sorts : (string * ((int * int) * (string -> (Smtlib_ty.ty list * int list) -> Smtlib_ty.desc))) list;
  2. funs : (string * Smtlib_typed_env.fun_def) list;
  3. par_funs : (string * (string list -> Smtlib_typed_env.fun_def)) list;
}
type theory =
  1. | Core
  2. | Ints
  3. | Reals
  4. | Reals_Ints
  5. | FloatingPoint
  6. | Arrays
  7. | 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