Module Logtk__Multiset.Make
Parameters
X : Stdlib.Map.OrderedType
Signature
type elt
= X.t
Elements of the multiset
val size : t -> int
Number of distinct elements.
val cardinal : t -> Z.t
Number of unique occurrences of elements (the multiplicity of each element is considered)
val empty : t
Empty multiset
val is_empty : t -> bool
Is the multiset empty?
val find : t -> elt -> Z.t
Return the multiplicity of the element within the multiset. Will return
Z.zero
if the element is not part of the multiset
val singleton : elt -> t
val doubleton : elt -> elt -> t
val add : t -> elt -> t
Add one occurrence of the element
val difference : t -> t -> t
Difference of multisets. If
x
has a bigger multiplicity in the second argument it won't appear in the result
module Seq : sig ... end
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val choose : t -> elt
Chose one element, or
- raises Not_found
if the multiset is empty
val of_coeffs : (elt * Z.t) list -> t
From list of elements with multiplicities. Multiplicities lower than 0 will not count.
val of_iarray : elt Logtk.IArray.t -> t
From immutable array
val of_array : elt array -> t
val to_list : t -> (elt * Z.t) list
List of elements with their coefficients
val cancel : t -> t -> t * t
Remove common elements from the multisets. For instance, on
{1,1,2}
and{1,2,2,3}
,cancel
will return({1}, {2,3})
Comparisons
In the following, the comparison function must be equality-compatible with E.compare
. In other words, if E.compare x y = 0
then f x y = Comparison.Eq
must hold.
val compare_partial : (elt -> elt -> Logtk.Comparison.t) -> t -> t -> Logtk.Comparison.t
Compare two multisets with the multiset extension of the given ordering. This ordering is total iff the element ordering is.
val is_max : (elt -> elt -> Logtk.Comparison.t) -> elt -> t -> bool
Is the given element maximal (ie not dominated by any other element) within the multiset?
val max : (elt -> elt -> Logtk.Comparison.t) -> t -> t
Maximal elements of the multiset, w.r.t the given ordering.
val max_seq : (elt -> elt -> Logtk.Comparison.t) -> t -> (elt * Z.t) Iter.t
Fold on maximal elements
val max_l : (elt -> elt -> Logtk.Comparison.t) -> elt list -> elt list
Maximal elements of a list
val compare_partial_l : (elt -> elt -> Logtk.Comparison.t) -> elt list -> elt list -> Logtk.Comparison.t
Compare two multisets represented as list of elements