1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
(** @author Benoît Montagu <benoit.montagu@inria.fr> *)
(** Copyright Inria © 2025 *)
include Zdd_sigs
module Make_ZddZE = ZddZE.Make
(** Functor that creates a structure of set families using an implementation of
ZDDs using zero-attributed edges *)
module Make_Zdd = Zdd_classic.Make
(** Functor that creates a structure of set families using a classic
implementation of ZDDs *)
module Make = Make_Zdd
(** Functor that creates a structure of set families *)
(** Functor that creates a structure of upward closed sets *)
module UpSet (X : T) : UPSET with type elt = X.t = struct
module F = Make (X)
type elt = X.t
type t = F.t
let hash = F.hash
let compare = F.compare
let equal = F.equal
let pp fmt t =
if F.is_empty t then F.pp fmt t
else if F.is_base t then Format.fprintf fmt "↑%a" F.pp t
else Format.fprintf fmt "↑(@[%a@])" F.pp t
let empty = F.empty
let full = F.base
let above = F.singleton
let subset = F.leq_FE_superset
let union s1 s2 = F.union (F.non_superset s1 s2) (F.non_superset s2 s1)
let inter s1 s2 = F.minima (F.join s1 s2)
let join = inter
let meet s1 s2 = F.minima (F.join s1 s2)
let minima = F.to_list
let subst env =
let subst = F.subst_gen F.union env in
fun t -> F.minima (subst t)
let iter_elt = F.iter_elt
let fold_elt = F.fold_elt
let iter_minima = F.iter
let fold_minima = F.fold
end
(** Functor that creates a structure of downward closed sets *)
module DownSet (X : T) : DOWNSET with type elt = X.t = struct
module F = Make (X)
type elt = X.t
type t = F.t
let hash = F.hash
let compare = F.compare
let equal = F.equal
let pp fmt t =
if F.is_empty t then F.pp fmt t
else if F.is_base t then Format.fprintf fmt "↓%a" F.pp t
else Format.fprintf fmt "↓(@[%a@])" F.pp t
let empty = F.empty
let base = F.base
let below = F.singleton
let subset = F.leq_FE_subset
let union s1 s2 = F.union (F.non_subset s1 s2) (F.non_subset s2 s1)
let inter s1 s2 = F.maxima (F.meet s1 s2)
let join s1 s2 = F.maxima (F.join s1 s2)
let meet = inter
let maxima = F.to_list
let subst env =
let subst = F.subst_gen F.union env in
fun t -> F.maxima (subst t)
let iter_elt = F.iter_elt
let fold_elt = F.fold_elt
let iter_maxima = F.iter
let fold_maxima = F.fold
end