Module Dpll_literal.Literal_map


module Literal_map: Index.Map  with type key = Literal.t
Maps keyed off literals.

type key 
Type of indexed objects.
type 'a t 
Map from indices 0, ... ,n - 1 (where n is the number of keys in the map) to 'a.
val size : 'a t -> int
size m is the number of indices mapped by m.


val create : 'a -> 'a t
create x is a new, empty map. x can be any element of type 'a and is used only for initializing the underlying representation.
val is_empty : 'a t -> bool
is_empty m holds if the map is empty.


val mem : 'a t -> key -> bool
mem m k is true iff there is a mapping for index k in m, i.e. index k < Index.Map.size m.
val find : 'a t -> key -> 'a
find m k is the mapping for the index of k in m.


val add : 'a t -> key -> 'a -> unit
add m k x modifies m by mapping the index of k to x. Any previously unmapped indices in 0, ..., index k will also be mapped to x.


val replace : 'a t -> key -> 'a -> unit
replace m k x updates m by mapping the index of k to x.


val copy : 'a t -> 'a t
A copy of the map.
val iter : (key -> 'a -> unit) -> 'a t -> unit
iter f m applies f to all mappings in m.
val iter_const : ('a -> key -> 'b -> unit) -> 'a -> 'b t -> unit
iter_const f x m is Index.Map.iter (f x) m, only faster since applying closures is slow.
val fold : ('a -> key -> 'b -> 'a) -> 'a -> 'b t -> 'a
fold f a m applies f to an accumulated value and each key-value pair in the mapping m.
val fold_const : ('a -> 'b -> key -> 'c -> 'b) -> 'a -> 'b -> 'c t -> 'b
fold_const f x a m is Index.Map.fold (f x) a m, only faster since applying closures is slow.
val modify : ('a -> 'a) -> 'a t -> unit
modify f m modifies a map so that each index maps to f of its prior value.
val modify_const : ('a -> 'b -> 'b) -> 'a -> 'b t -> unit
modify_const f x v is modify (f x) v, only faster since applying closures is slow.
val set_all : 'a t -> 'a -> unit
set_all m x updates m by mapping every key to x.

Hosted by the SourceForge.net Logo* web site.
*Other names and brands may be claimed as the property of others.