`DisjointDomain`

Abstract domains for collections of elements from disjoint unions of domains. Formally, the elements form a cofibered domain from a discrete category.

Elements are grouped into disjoint buckets by a congruence or/and a projection. All operations on elements are performed bucket-wise and must be bucket-closed.

Examples of such domains are path-sensitivity and address sets.

`module type Representative = sig ... end`

Buckets defined by projection. The module is the image (representative) of the projection function `of_elt`

.

```
module ProjectiveSet
(E : Printable.S)
(B : SetDomain.S with type elt = E.t)
(R : Representative with type elt = E.t) :
sig ... end
```

Set of elements `E.t`

grouped into buckets by `R`

, where each bucket is described by the set `B`

.

`module type MayEqualSetDomain = sig ... end`

```
module ProjectiveSetPairwiseMeet
(E : Printable.S)
(B : MayEqualSetDomain with type elt = E.t)
(R : Representative with type elt = E.t) :
SetDomain.S with type elt = E.t
```

`module type Congruence = sig ... end`

Buckets defined by congruence.

```
module PairwiseSet
(E : Printable.S)
(B : SetDomain.S with type elt = E.t)
(C : Congruence with type elt = E.t) :
SetDomain.S with type elt = E.t
```

Set of elements `E.t`

grouped into buckets by `C`

, where each bucket is described by the set `B`

.

`module type RepresentativeCongruence = sig ... end`

Buckets defined by a coarse projection and a fine congruence. Congruent elements must have the same representative, but not vice versa (`Representative`

would then suffice).

```
module CombinedSet
(E : Printable.S)
(B : SetDomain.S with type elt = E.t)
(RC : RepresentativeCongruence with type elt = E.t) :
sig ... end
```

Set of elements `E.t`

grouped into buckets by `RC`

, where each bucket is described by the set `B`

.

Generalization of above sets into maps, whose key set behaves like above sets, but each element can also be associated with a value.

```
module ProjectiveMap
(E : Printable.S)
(V : Printable.S)
(B : MapDomain.S with type key = E.t and type value = V.t)
(R : Representative with type elt = E.t) :
MapDomain.S with type key = E.t and type value = B.value
```

Map of keys `E.t`

grouped into buckets by `R`

, where each bucket is described by the map `B`

with values `V.t`

.

```
module PairwiseMap
(E : Printable.S)
(R : Printable.S)
(B : MapDomain.S with type key = E.t and type value = R.t)
(C : Congruence with type elt = E.t) :
MapDomain.S with type key = E.t and type value = B.value
```

Map of keys `E.t`

grouped into buckets by `C`

, where each bucket is described by the map `B`

with values `R.t`

.