logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . TypedSTerm . Var_tbl
include Hashtbl.S with type key = t Var.t
type key = t Var.t
type !'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
  • since 4.00.0
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
  • since 4.05.0
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : ( key -> 'a -> unit ) -> 'a t -> unit
val filter_map_inplace : ( key -> 'a -> 'a option ) -> 'a t -> unit
  • since 4.03.0
val fold : ( key -> 'a -> 'b -> 'b ) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
  • since 4.00.0
val to_seq_keys : _ t -> key Seq.t
  • since 4.07
val to_seq_values : 'a t -> 'a Seq.t
  • since 4.07
val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
  • since 4.07
val get : 'a t -> key -> 'a option

Safe version of Hashtbl.find.

val get_or : 'a t -> key -> default:'a -> 'a

get_or tbl k ~default returns the value associated to k if present, and returns default otherwise (if k doesn't belong in tbl).

  • since 0.16
val add_list : 'a list t -> key -> 'a -> unit

add_list tbl x y adds y to the list x is bound to. If x is not bound, it becomes bound to y.

  • since 0.16
val incr : ?by:int -> int t -> key -> unit

incr ?by tbl x increments or initializes the counter associated with x. If get tbl x = None, then after update, get tbl x = Some 1; otherwise, if get tbl x = Some n, now get tbl x = Some (n+1).

  • parameter by

    if specified, the int value is incremented by by rather than 1.

  • since 0.16
val decr : ?by:int -> int t -> key -> unit

Like incr but subtract 1 (or the value of by). If the value reaches 0, the key is removed from the table. This does nothing if the key is not already present in the table.

  • since 0.16
val keys : 'a t -> key CCHashtbl.iter

Iterate on keys (similar order as Hashtbl.iter).

val values : 'a t -> 'a CCHashtbl.iter

Iterate on values in the table.

val keys_list : _ t -> key list

keys_list t is the list of keys in t. If the key is in the Hashtable multiple times, all occurrences will be returned.

  • since 0.8
val values_list : 'a t -> 'a list

values_list t is the list of values in t.

  • since 0.8
val map_list : ( key -> 'a -> 'b ) -> 'a t -> 'b list

Map on a hashtable's items, collect into a list.

val to_iter : 'a t -> (key * 'a) CCHashtbl.iter

Iterate on bindings in the table.

  • since 2.8
val to_seq : 'a t -> (key * 'a) CCHashtbl.sequence
val add_iter : 'a t -> (key * 'a) CCHashtbl.iter -> unit

Add the corresponding pairs to the table, using Hashtbl.add.

  • since 2.8
val add_std_seq : 'a t -> (key * 'a) Seq.t -> unit

Add the corresponding pairs to the table, using Hashtbl.add.

  • since 2.8
val add_seq : 'a t -> (key * 'a) CCHashtbl.sequence -> unit
val of_iter : (key * 'a) CCHashtbl.iter -> 'a t

From the given bindings, added in order.

  • since 2.8
val of_std_seq : (key * 'a) Seq.t -> 'a t

From the given bindings, added in order.

  • since 2.8
val of_seq : (key * 'a) CCHashtbl.sequence -> 'a t
val add_iter_count : int t -> key CCHashtbl.iter -> unit

add_iter_count tbl i increments the count of each element of i by calling incr. This is useful for counting how many times each element of i occurs.

  • since 2.8
val add_std_seq_count : int t -> key Seq.t -> unit

add_seq_count tbl seq increments the count of each element of seq by calling incr. This is useful for counting how many times each element of seq occurs.

  • since 2.8
val add_seq_count : int t -> key CCHashtbl.sequence -> unit
val of_iter_count : key CCHashtbl.iter -> int t

Like add_seq_count, but allocates a new table and returns it.

  • since 2.8
val of_std_seq_count : key Seq.t -> int t

Like add_seq_count, but allocates a new table and returns it.

  • since 2.8
val of_seq_count : key CCHashtbl.sequence -> int t
val to_list : 'a t -> (key * 'a) list

List of bindings (order unspecified).

val of_list : (key * 'a) list -> 'a t

Build a table from the given list of bindings k_i -> v_i, added in order using add. If a key occurs several times, it will be added several times, and the visible binding will be the last one.

val update : 'a t -> f:( key -> 'a option -> 'a option ) -> k:key -> unit

update tbl ~f ~k updates key k by calling f k (Some v) if k was mapped to v, or f k None otherwise; if the call returns None then k is removed/stays removed, if the call returns Some v' then the binding k -> v' is inserted using Hashtbl.replace.

  • since 0.14
val get_or_add : 'a t -> f:( key -> 'a ) -> k:key -> 'a

get_or_add tbl ~k ~f finds and returns the binding of k in tbl, if it exists. If it does not exist, then f k is called to obtain a new binding v; k -> v is added to tbl and v is returned.

  • since 1.0

Printer for tables. Renamed from print since 2.0.

  • since 0.13