package psmt2-frontend

  1. Overview
  2. Docs

Module Psmt2Frontend.Smtlib_typed_envSource

Sourcemodule SMap : sig ... end
Sourceval init : int -> (int -> 'a) -> 'a list
Sourcetype assoc =
  1. | Right
  2. | Left
  3. | Chainable
  4. | Pairwise
Sourcetype fun_def = {
  1. params : Smtlib_ty.ty;
  2. assoc : assoc option;
}
Sourcetype env = {
  1. sorts : ((int * int) * (string -> (Smtlib_ty.ty list * int list) -> Smtlib_ty.desc)) SMap.t;
  2. funs : fun_def list SMap.t;
  3. par_funs : (string list -> fun_def) list SMap.t;
  4. constructors : int SMap.t SMap.t;
}
Sourceval empty : unit -> env
Sourceval get_arit : 'a Smtlib_syntax.data -> string -> int
Sourceval check_identifier : Smtlib_syntax.identifier_aux Smtlib_syntax.data -> int -> unit
Sourceval check_sort_already_exist : (env * 'a SMap.t) -> SMap.key Smtlib_syntax.data -> unit
Sourceval check_sort_exist : (env * 'a SMap.t) -> SMap.key Smtlib_syntax.data -> unit
Sourceval mk_sort_definition : int -> 'a -> bool -> (int * 'a) * (string -> (Smtlib_ty.ty list * 'b) -> Smtlib_ty.desc)
Sourceval mk_sort : (env * 'a SMap.t) -> SMap.key Smtlib_syntax.data -> ((int * int) * (string -> (Smtlib_ty.ty list * int list) -> Smtlib_ty.desc)) -> env
Sourceval mk_sort_decl : (env * 'a SMap.t) -> SMap.key Smtlib_syntax.data -> string -> bool -> env
Sourceval find_sort_def : env -> SMap.key Smtlib_syntax.data -> (int * int) * (string -> (Smtlib_ty.ty list * int list) -> Smtlib_ty.desc)
Sourceval add_sorts : env -> (SMap.key * ((int * int) * (string -> (Smtlib_ty.ty list * int list) -> Smtlib_ty.desc))) list -> env
Sourceval find_sort_symb : (env * Smtlib_ty.ty SMap.t) -> SMap.key Smtlib_syntax.data -> Smtlib_ty.ty list -> int list -> Smtlib_ty.ty
Sourceval extract_arit_ty_assoc : Smtlib_ty.ty -> int * Smtlib_ty.ty
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval check_fun_exists : (env * Smtlib_ty.ty Smtlib_ty.SMap.t) -> SMap.key Smtlib_syntax.data -> Smtlib_ty.ty list -> bool -> unit
Sourceval mk_fun_ty : Smtlib_ty.ty list -> Smtlib_ty.ty -> assoc option -> fun_def
Sourceval mk_fun_ty_arg : Smtlib_ty.ty list -> Smtlib_ty.ty -> assoc option -> 'a -> 'b -> fun_def
Sourceval add_funs : env -> (SMap.key * fun_def) list -> env
Sourceval add_par_funs : env -> (SMap.key * (string list -> fun_def)) list -> env
Sourceval find_simpl_sort_symb : (env * 'a) -> SMap.key Smtlib_syntax.data -> Smtlib_ty.ty list -> Smtlib_ty.ty