psmt2-frontend 0.4.0 · OCaml Package

module SMap : sig ... end

val init : int -> (int -> 'a) -> 'a list

type assoc =

| Right
| Left
| Chainable
| Pairwise

type fun_def = {

params : Smtlib_ty.ty;
assoc : assoc option;

}

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 add_funs : env -> (SMap.key * fun_def) list -> env

val add_par_funs : env -> (SMap.key * (string list -> fun_def)) list -> 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

package psmt2-frontend