package smtml

  1. Overview
  2. Docs

Module Expr.SetSource

Sourcetype elt = t

The type of elements of the set

Sourcetype key = elt

Alias for the type of elements, for cross-compatibility with maps

Sourcetype t

The set type

Basic functions

Sourceval empty : t

The empty set

Sourceval is_empty : t -> bool

is_empty st is true if st contains no elements, false otherwise

Sourceval mem : elt -> t -> bool

mem elt set is true if elt is contained in set, O(log(n)) complexity.

Sourceval add : elt -> t -> t

add elt set adds element elt to the set. Preserves physical equality if elt was already present. O(log(n)) complexity.

Sourceval singleton : elt -> t

singleton elt returns a set containing a single element: elt

Sourceval cardinal : t -> int

cardinal set is the size of the set (number of elements), O(n) complexity.

Sourceval remove : elt -> t -> t

remove elt set returns a set containing all elements of set except elt. Returns a value physically equal to set if elt is not present.

Iterators

Sourceval iter : (elt -> unit) -> t -> unit

iter f set calls f on all elements of set.

Sourceval map : (elt -> elt) -> t -> t

map f set maps all elements of set to their image by f.

Sourceval filter : (elt -> bool) -> t -> t

filter f set is the subset of set that only contains the elements that satisfy f.

Sourceval for_all : (elt -> bool) -> t -> bool

for_all f set is true if f is true on all elements of set. Short-circuits on first false.

Sourceval fold : (elt -> 'acc -> 'acc) -> t -> 'acc -> 'acc

fold f set acc returns f elt_n (... (f elt_1 acc) ...), where elt_1, ..., elt_n are the elements of set.

Sourceval split : elt -> t -> t * bool * t

split elt set returns s_lt, present, s_gt where s_lt contains all elements of set smaller than elt, s_gt all those greater than elt, and present is true if elt is in set.

Sourceval pp : t Fmt.t

Pretty prints the set,

Functions on pairs of sets

Sourceval union : t -> t -> t

union a b is the set union of a and b, i.e. the set containing all elements that are either in a or b.

Sourceval inter : t -> t -> t

inter a b is the set intersection of a and b, i.e. the set containing all elements that are in both a or b.

Sourceval disjoint : t -> t -> bool

disjoint a b is true if a and b have no elements in common.

Sourceval subset : t -> t -> bool

subset a b is true if all elements of a are also in b.

Sourceval diff : t -> t -> t

diff s1 s2 is the set of all elements of s1 that aren't in s2.

  • since v0.11.0

Conversion functions

to_seq st iterates the whole set.

Sourceval to_rev_seq : t -> elt Smtml_prelude.Seq.t

to_rev_seq st iterates the whole set.

Sourceval add_seq : elt Smtml_prelude.Seq.t -> t -> t

add_seq s st adds all elements of the sequence s to st in order.

of_seq s creates a new set from the elements of s.

Sourceval of_list : elt list -> t

of_list l creates a new set from the elements of l.

Sourceval to_list : t -> elt list

to_list s returns the elements of s as a list.

Smtml Specific

Sourceval hash : t -> int

hash set computes the hash of a set.

Sourceval equal : t -> t -> bool

equal set1 set2 compares two sets for equality.

Sourceval compare : t -> t -> int

compare set1 set2 compares two sets lexicographically.

Sourceval get_symbols : t -> Symbol.t list

get_symbols exprs extracts all symbolic variables from a list of expressions.

Sourceval inline_symbol_values : elt Symbol.Map.t -> t -> t

inline_symbol_values symbol_map set replaces each symbol in all expressions of set by its image in symbol_map.