Source file zdd_classic.ml

(** @author Benoît Montagu <benoit.montagu@inria.fr> *)

(** Copyright Inria © 2025 *)

include Zdd_sigs

(** Functor that creates a structure of set families *)
module Make (X : T) : S with type elt = X.t = struct
  type elt = X.t

  (** Set families of finite sets over the type [X.t], implemented as ZDDs *)
  type t = Empty | Base | Node of { id : int; elt : elt; zero : t; one : t }
  (* the subtree "one" cannot be [Empty] *)
  (* the deeper a tree node, the larger its element *)

  let get_cur_id, freshen_id =
    let r = ref 0 in
    let[@inline] get_cur_id () = !r and[@inline] freshen_id () = incr r in
    (get_cur_id, freshen_id)

  let empty_id = get_cur_id ()
  let () = freshen_id ()
  let base_id = get_cur_id ()
  let () = freshen_id ()

  let[@inline] get_id = function
    | Empty -> empty_id
    | Base -> base_id
    | Node { id; _ } -> id

  module M = struct
    type nonrec t = t

    (* this equality intentionally discards the "id" field *)
    let equal t1 t2 =
      match (t1, t2) with
      | Empty, Empty | Base, Base -> true
      | ( Node { id = _; elt = x1; zero = t10; one = t11 },
          Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
          t10 == t20 && t11 == t21 && X.equal x1 x2
      | _ -> false

    let hash seed = function
      | Empty -> Hashtbl.seeded_hash seed empty_id
      | Base -> Hashtbl.seeded_hash seed base_id
      | Node { id = _; elt; zero; one } ->
          let seed = Hashtbl.seeded_hash seed (get_id zero) in
          let seed = Hashtbl.seeded_hash seed (get_id one) in
          Hashtbl.seeded_hash seed (X.hash elt)

    let[@warning "-32"] seeded_hash = hash
    (* for OCaml >= 5.0 *)
  end

  module H = Ephemeron.K1.MakeSeeded (M)

  (** Pretty printer for ZDDs *)
  let rec pp fmt =
    let open Format in
    function
    | Empty -> pp_print_string fmt "∅"
    | Base -> pp_print_string fmt "{ ∅ }"
    | Node { id = _; elt = x; zero = Empty; one = Base } ->
        fprintf fmt "@[{{ @[%a@] }}@]" X.pp x
    | Node { id = _; elt = x; zero = Empty; one = t1 } ->
        fprintf fmt "@[{{ @[%a@] }}@ ⊔ (@[%a@])@]" X.pp x pp t1
    | Node { id = _; elt = x; zero = t0; one = Base } ->
        fprintf fmt "@[@[%a@]@ ∪ @[{{ @[%a@] }}@]@]" pp t0 X.pp x
    | Node { id = _; elt = x; zero = t0; one = t1 } ->
        fprintf fmt "@[@[%a@]@ ∪ (@[{{ @[%a@] }}@ ⊔ @[%a@]@])@]" pp t0 X.pp x pp
          t1

  (** The empty family: [∅] *)
  let empty = Empty

  (** The family that contains only the empty set: [{ ∅ }] *)
  let base = Base

  (** Tests whether a ZDD is equal to [empty] *)
  let is_empty = function Empty -> true | _ -> false

  (** Tests whether a ZDD is equal to [base] *)
  let is_base = function Base -> true | _ -> false

  (** Smart constructor for ZDD nodes *)
  let node =
    let h = H.create 128 in
    H.add h empty empty;
    H.add h base base;
    fun x t0 t1 ->
      if is_empty t1 then t0
      else
        let n = Node { id = get_cur_id (); elt = x; zero = t0; one = t1 } in
        match H.find_opt h n with
        | Some n' -> n'
        | None ->
            freshen_id ();
            H.add h n n;
            n

  let rec singleton_aux = function
    | [] -> base
    | x :: xs -> node x empty (singleton_aux xs)

  (** [singleton [x1;... ; xn]] is the ZDD that represents the set family
      [{ { x1, ..., xn } }] *)
  let singleton xs = singleton_aux (List.sort X.compare xs)

  let equal = ( == )
  let compare t1 t2 = Int.compare (get_id t1) (get_id t2)
  let hash t = Hashtbl.hash (get_id t)

  module N = struct
    type nonrec t = t

    let equal = equal
    let hash = hash
  end

  module H1 = Ephemeron.K1.Make (N)
  module H2 = Ephemeron.K2.Make (N) (N)

  let fix1 f =
    let h = H1.create 128 in
    let rec g x =
      match H1.find_opt h x with
      | Some v -> v
      | None ->
          let v = f g x in
          H1.add h x v;
          v
    in
    g

  let fix2 ~sym f =
    let h = H2.create 128 in
    let rec g x1 x2 =
      let x =
        if (not sym) || get_id x1 <= get_id x2 then (x1, x2) else (x2, x1)
      in
      match H2.find_opt h x with
      | Some v -> v
      | None ->
          let v = f g x1 x2 in
          H2.add h x v;
          v
    in
    g

  (** Wellformedness test *)
  let wf =
    fix1 @@ fun wf -> function
    | Empty | Base -> true
    | Node { id = _; elt = x; zero = t0; one = t1 } ->
        ((match t0 with
         | Empty | Base -> true
         | Node { elt; _ } -> X.compare x elt < 0)
        &&
        match t1 with
        | Empty -> false
        | Base -> true
        | Node { elt; _ } -> X.compare x elt < 0)
        && wf t0 && wf t1

  (** Retrieves the a set of the set family, if any. The choice of which set of
      the family is returned is not specified.

      @raise Not_found if the set family is empty *)
  let choose =
    fix1 @@ fun choose -> function
    | Empty -> raise Not_found
    | Base -> []
    | Node { id = _; elt; zero; one } -> (
        match choose zero with
        | r -> r
        | exception Not_found -> elt :: choose one)

  (** Retrieves the a set of the set family, if any. The choice of which set of
      the family is returned is not specified. *)
  let choose_opt =
    fix1 @@ fun choose_opt -> function
    | Empty -> None
    | Base -> Some []
    | Node { id = _; elt; zero; one } -> (
        match choose_opt zero with
        | Some _ as r -> r
        | None -> (
            match choose_opt one with
            | Some l -> Some (elt :: l)
            | None -> assert false))

  (** Returns the sets that belong to a ZDD, as a list of lists of elements *)
  let to_list =
    fix1 @@ fun to_list -> function
    | Empty -> []
    | Base -> [ [] ]
    | Node { id = _; elt = x; zero = t10; one = t20 } ->
        List.rev_append (to_list t10)
          (List.rev_map (fun l -> x :: l) (to_list t20))

  (** Returns the sets that belong to a ZDD, as a sequence of lists of elements
  *)
  let to_seq =
    fix1 @@ fun to_seq -> function
    | Empty -> Seq.empty
    | Base -> Seq.cons [] Seq.empty
    | Node { id = _; elt = x; zero = t10; one = t20 } ->
        Seq.append (to_seq t10) (Seq.map (fun l -> x :: l) (to_seq t20))

  (** [cardinal_generic plus zero one t] is the cardinal of the family
      represented by [t], i.e., how many sets it contains, where [plus] is used
      as (associative commutative) addition and [zero] as neutral element and
      [one] for [1]. *)
  let cardinal_generic plus zero one =
    fix1 @@ fun cardinal -> function
    | Empty -> zero
    | Base -> one
    | Node { id = _; elt = _; zero = t0; one = t1 } ->
        plus (cardinal t0) (cardinal t1)

  (** [cardinal t] is the cardinal of the family represented by [t], i.e., how
      many sets it contains. *)
  let cardinal =
    fix1 @@ fun cardinal -> function
    | Empty -> 0
    | Base -> 1
    | Node { id = _; elt = _; zero = t0; one = t1 } -> cardinal t0 + cardinal t1

  (** [max_cardinal t] returns the maximal cardinal of the sets contained in the
      family represented by [t]. Returns [min_int] if the family is empty. *)
  let max_cardinal =
    fix1 @@ fun max_cardinal -> function
    | Empty -> min_int
    | Base -> 0
    | Node { id = _; elt = _; zero = t0; one = t1 } ->
        max (max_cardinal t0) (1 + max_cardinal t1)

  (** [min_cardinal t] returns the minimal cardinal of the sets contained in the
      family represented by [t]. Returns [max_int] if the family is empty. *)
  let min_cardinal =
    fix1 @@ fun min_cardinal -> function
    | Empty -> max_int
    | Base -> 0
    | Node { id = _; elt = _; zero = t0; one = t1 } ->
        min (min_cardinal t0) (1 + min_cardinal t1)

  (** Returns the number of nodes that are used to represent the ZDD *)
  let nb_nodes =
    fix1 @@ fun nb_nodes -> function
    | Empty | Base -> 0
    | Node { id = _; elt = _; zero = t0; one = t1 } ->
        1 + nb_nodes t0 + nb_nodes t1

  (** [s ∈ with_elt y t] iff [s ∈ t] and [y ∈ s] *)
  let with_elt y =
    fix1 @@ fun with_elt -> function
    | Empty | Base -> empty
    | Node { id = _; elt = x; zero = t0; one = t1 } ->
        let n = X.compare x y in
        if n < 0 then node x (with_elt t0) (with_elt t1)
        else if n > 0 then empty
        else (* x = y *) node x empty t1

  (** [s ∈ on_elt y t] iff [{y} ∪ s ∈ t] and [y ∉ s] *)
  let on_elt y =
    fix1 @@ fun on_elt -> function
    | Empty | Base -> empty
    | Node { id = _; elt = x; zero = t0; one = t1 } ->
        let n = X.compare x y in
        if n < 0 then node x (on_elt t0) (on_elt t1)
        else if n > 0 then empty
        else (* x = y *) t1

  (** [s ∈ without_elt y t] iff [s ∈ t] and [y ∉ s] *)
  let without_elt y =
    fix1 @@ fun without_elt -> function
    | Empty -> empty
    | Base -> base
    | Node { id = _; elt = x; zero = t0; one = t1 } as t ->
        let n = X.compare x y in
        if n < 0 then node x (without_elt t0) (without_elt t1)
        else if n > 0 then t
        else (* x = y *) t0

  let off_elt = without_elt

  (** [s ∈ change x t] iff either [x ∈ s] and [s ∖ {x} ∈ t], or [x ∉ s] and
      [{x} ∪ s ∈ t] *)
  let change_elt y =
    fix1 @@ fun change_elt -> function
    | Empty -> empty
    | Base -> base
    | Node { id = _; elt = x; zero = t0; one = t1 } as t ->
        let n = X.compare x y in
        if n < 0 then node x (change_elt t0) (change_elt t1)
        else if n > 0 then node y empty t
        else (* x = y *) node x t1 t0

  (** [subset t1 t2] iff for every [s], [s ∈ t1] implies [s ∈ t2] *)
  let subset =
    fix2 ~sym:false @@ fun subset t1 t2 ->
    match (t1, t2) with
    | Empty, _ -> true
    | (Base | Node _), Empty -> false
    | Base, Base -> true
    | Node _, Base -> false
    | Base, Node { id = _; elt = _; zero = t20; one = _ } -> subset Base t20
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then subset t10 t2 && is_empty t11
        else if n > 0 then subset t1 t20
        else (* n = 0 *) subset t10 t20 && subset t11 t21

  (** [s ∈ inter t1 t2] iff [s ∈ t1] or [s ∈ t2] *)
  let union =
    fix2 ~sym:true @@ fun union t1 t2 ->
    match (t1, t2) with
    | Empty, t | t, Empty -> t
    | Base, Base -> base
    | Base, Node { id = _; elt = x; zero = t0; one = t1 }
    | Node { id = _; elt = x; zero = t0; one = t1 }, Base ->
        node x (union base t0) t1
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (union t10 t2) t11
        else if n > 0 then node x2 (union t1 t20) t21
        else (* n = 0 *)
          node x1 (union t10 t20) (union t11 t21)

  (** [s ∈ inter t1 t2] iff [s ∈ t1] and [s ∈ t2] *)
  let inter =
    fix2 ~sym:true @@ fun inter t1 t2 ->
    match (t1, t2) with
    | Empty, _ | _, Empty -> empty
    | Base, Base -> base
    | Base, Node { id = _; elt = _; zero = t0; one = _ }
    | Node { id = _; elt = _; zero = t0; one = _ }, Base ->
        inter base t0
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then inter t10 t2
        else if n > 0 then inter t1 t20
        else (* n = 0 *)
          node x1 (inter t10 t20) (inter t11 t21)

  (** [s ∈ diff t1 t2] iff [s ∈ t1] and [s ∉ t2] *)
  let diff =
    fix2 ~sym:false @@ fun diff t1 t2 ->
    match (t1, t2) with
    | Empty, _ -> empty
    | t, Empty -> t
    | Base, Base -> empty
    | Base, Node { id = _; elt = _; zero = t20; one = _ } -> diff base t20
    | Node { id = _; elt = x1; zero = t10; one = t11 }, Base ->
        node x1 (diff t10 base) t11
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (diff t10 t2) t11
        else if n > 0 then diff t1 t20
        else (* n = 0 *)
          node x1 (diff t10 t20) (diff t11 t21)

  (** [s ∈ sym_diff t1 t2] iff either [s ∈ t1] and [s ∉ t2], or [s ∈ t2] and
      [s ∉ t1] *)
  let sym_diff =
    fix2 ~sym:true @@ fun sym_diff t1 t2 ->
    match (t1, t2) with
    | Empty, t | t, Empty -> t
    | Base, Base -> empty
    | Base, Node { id = _; elt; zero; one }
    | Node { id = _; elt; zero; one }, Base ->
        node elt (sym_diff base zero) one
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (sym_diff t10 t2) t11
        else if n > 0 then node x2 (sym_diff t1 t20) t21
        else (* n = 0 *)
          node x1 (sym_diff t10 t20) (sym_diff t11 t21)

  (** [s ∈ join t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such that
      [s = s1 ∪ s2] *)
  let join =
    fix2 ~sym:true @@ fun join t1 t2 ->
    match (t1, t2) with
    | Empty, _ | _, Empty -> empty
    | Base, t | t, Base -> t
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (join t10 t2) (join t11 t2)
        else if n > 0 then node x2 (join t1 t20) (join t1 t21)
        else (* n = 0 *)
          node x1 (join t10 t20)
            (union (join t11 t21) (union (join t10 t21) (join t11 t20)))

  (** [s ∈ disjoint_join t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such
      that [s1 ∩ s2 = ∅] and [s = s1 ∪ s2] *)
  let disjoint_join =
    fix2 ~sym:true @@ fun disjoint_join t1 t2 ->
    match (t1, t2) with
    | Empty, _ | _, Empty -> empty
    | Base, t | t, Base -> t
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (disjoint_join t10 t2) (disjoint_join t11 t2)
        else if n > 0 then node x2 (disjoint_join t1 t20) (disjoint_join t1 t21)
        else (* n = 0 *)
          node x1 (disjoint_join t10 t20)
            (union (disjoint_join t10 t21) (disjoint_join t11 t20))

  (** [s ∈ joint_join t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such that
      [s1 ∩ s2 ≠ ∅] and [s = s1 ∪ s2] *)
  let joint_join =
    fix2 ~sym:true @@ fun joint_join t1 t2 ->
    match (t1, t2) with
    | Empty, _ | _, Empty | Base, _ | _, Base -> empty
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (joint_join t10 t2) (joint_join t11 t2)
        else if n > 0 then node x2 (joint_join t1 t20) (joint_join t1 t21)
        else (* n = 0 *)
          node x1 (joint_join t10 t20)
            (union (join t11 t21)
               (union (joint_join t10 t21) (joint_join t11 t20)))

  (** [s ∈ meet t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such that
      [s = s1 ∩ s2] *)
  let meet =
    fix2 ~sym:true @@ fun meet t1 t2 ->
    match (t1, t2) with
    | Empty, _ | _, Empty -> empty
    | Base, _ | _, Base -> base
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then union (meet t10 t2) (meet t11 t2)
        else if n > 0 then union (meet t1 t20) (meet t1 t21)
        else (* n = 0 *)
          union
            (node x1 (meet t10 t20) (meet t11 t21))
            (union (meet t10 t21) (meet t11 t20))

  (** [s ∈ delta t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such that
      [s = (s1 \ s2) ∪ (s2 \ s1)] *)
  let delta =
    fix2 ~sym:true @@ fun delta t1 t2 ->
    match (t1, t2) with
    | Empty, _ | _, Empty -> empty
    | Base, t | t, Base -> t
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (delta t10 t2) (delta t11 t2)
        else if n > 0 then node x2 (delta t1 t20) (delta t1 t21)
        else (* n = 0 *)
          node x1
            (union (delta t10 t20) (delta t11 t21))
            (union (delta t10 t21) (delta t11 t20))

  (** [s ∈ minus t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such that
      [s = s1 \ s2] *)
  let minus =
    fix2 ~sym:false @@ fun minus t1 t2 ->
    match (t1, t2) with
    | Empty, _ | _, Empty -> empty
    | Base, _ -> base
    | t, Base -> t
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (minus t10 t2) (minus t11 t2)
        else if n > 0 then union (minus t1 t20) (minus t1 t21)
        else (* n = 0 *)
          union
            (union (minus t10 t20) (minus t10 t21))
            (union (node x1 empty (minus t11 t20)) (minus t11 t21))

  (** [s ∈ div t1 t2] iff for any [s2 ∈ t2], [s ∪ s2 ∈ t1] and [s ∩ s2 = ∅] *)
  let div =
    fix2 ~sym:false @@ fun div t1 t2 ->
    match (t1, t2) with
    | Empty, _ | _, Empty -> t1
    | t, Base -> t
    | Base, _ -> empty
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (div t10 t2) (div t11 t2)
        else if n > 0 then empty
        else if
          (* n = 0 *)
          is_empty t20
        then div t11 t21
        else inter (node x1 (div t10 t20) (div t11 t20)) (div t11 t21)

  (** [rem t1 t2 = diff t1 (join (div t1 t2) t2)]. The following equation is
      always satisfied: [t1 = union (join (div t1 t2) t2) (rem t1 t2)]. **)
  let rem t1 t2 = diff t1 (join (div t1 t2) t2)

  (** [s ∈ remove y t] iff there exists [s' ∈ t] such that [s' = s \ { x }] *)
  let remove y =
    fix1 @@ fun remove -> function
    | Empty -> empty
    | Base -> base
    | Node { id = _; elt = x; zero = t0; one = t1 } as t ->
        let n = X.compare x y in
        if n < 0 then node x (remove t0) (remove t1)
        else if n > 0 then t
        else (* x = y *)
          union t0 t1

  (** [s ∈ restrict t1 t2] iff [s ∈ t1] and there exists [s' ∈ t2] such that
      [s' ⊆ s] *)
  let restrict =
    fix2 ~sym:false @@ fun restrict t1 t2 ->
    match (t1, t2) with
    | Empty, _ | _, Base -> t1
    | _, Empty -> t2
    | Base, Node { id = _; elt = _; zero = t20; one = _ } -> restrict base t20
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (restrict t10 t2) (restrict t11 t2)
        else if n > 0 then restrict t1 t20
        else
          node x1 (restrict t10 t20)
            (union (restrict t11 t20) (restrict t11 t21))

  (** [s ∈ permit t1 t2] iff [s ∈ t1] and there exists [s' ∈ t2] such that
      [s ⊆ s'] *)
  let permit =
    fix2 ~sym:false @@ fun permit t1 t2 ->
    match (t1, t2) with
    | Empty, _ | Base, Base -> t1
    | _, Empty -> t2
    | Node { id = _; elt = _; zero = t10; one = _ }, Base -> permit t10 base
    | Base, Node { id = _; elt = _; zero = t20; one = t21 } ->
        union (permit base t20) (permit base t21)
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then permit t10 t2
        else if n > 0 then union (permit t1 t20) (permit t1 t21)
        else node x1 (union (permit t10 t20) (permit t10 t21)) (permit t11 t21)

  (** [s ∈ non_superset t1 t2] iff [s ∈ t1] and for every [s' ∈ t2], [s' ⊈ s] *)
  let non_superset =
    fix2 ~sym:false @@ fun non_superset t1 t2 ->
    match (t1, t2) with
    | Empty, _ -> empty
    | _, Empty -> t1
    | _, Base -> empty
    | Base, Node { id = _; elt = _; zero = t20; one = _ } ->
        non_superset base t20
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (non_superset t10 t2) (non_superset t11 t2)
        else if n > 0 then non_superset t1 t20
        else
          node x1 (non_superset t10 t20)
            (inter (non_superset t11 t20) (non_superset t11 t21))

  (** [s ∈ non_subset t1 t2] iff [s ∈ t1] and for every [s' ∈ t2], [s ⊈ s'] *)
  let non_subset =
    fix2 ~sym:false @@ fun non_subset t1 t2 ->
    match (t1, t2) with
    | Empty, _ -> empty
    | _, Empty -> t1
    | Base, Base -> empty
    | Node { id = _; elt = x; zero = t10; one = t11 }, Base ->
        node x (non_subset t10 base) t11
    | Base, Node { id = _; elt = _; zero = t20; one = t21 } ->
        inter (non_subset base t20) (non_subset base t21)
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then node x1 (non_subset t10 t2) t11
        else if n > 0 then inter (non_subset t1 t20) (non_subset t1 t21)
        else
          node x1
            (inter (non_subset t10 t20) (non_subset t10 t21))
            (non_subset t11 t21)

  (** [s ∈ maxima t] iff [s ∈ t] and for every [s' ∈ t], [s ⊆ s'] implies
      [s' ⊆ s] *)
  let maxima =
    fix1 @@ fun maxima -> function
    | Empty -> empty
    | Base -> base
    | Node { id = _; elt = x; zero = t0; one = t1 } ->
        let m1 = maxima t1 in
        node x (non_subset (maxima t0) m1) m1

  (** [s ∈ minima t] iff [s ∈ t] and for every [s' ∈ t], [s' ⊆ s] implies
      [s ⊆ s'] *)
  let minima =
    fix1 @@ fun minima -> function
    | Empty -> empty
    | Base -> base
    | Node { id = _; elt = x; zero = t0; one = t1 } ->
        let m0 = minima t0 in
        node x m0 (non_superset (minima t1) m0)

  (** [s ∈ min_hitting_set t] iff for every [s' ∈ t], [s ∩ s' ≠ ∅], and such
      that no smaller set than [s] satisfies this property (i.e., [s] is
      minimal). *)
  let min_hitting_set =
    fix1 @@ fun min_hitting_set -> function
    | Empty | Base -> empty
    | Node { id = _; elt = x; zero = t0; one = t1 } ->
        let h1 = min_hitting_set t1 in
        if is_empty t0 then minima @@ node x h1 (union base h1)
        else
          let h0 = min_hitting_set t0 in
          minima @@ node x (join h0 h1) (join h0 (union base h1))

  (** [s ∈ closure t] iff there exists [t' ⊆ t] such that [s = ⋂ t'] *)
  let closure =
    fix1 @@ fun closure -> function
    | Empty -> empty
    | Base -> base
    | Node { id = _; elt = x; zero = t0; one = t1 } ->
        let c0 = closure t0 in
        let c1 = closure t1 in
        union (meet c0 c1) (node x c0 c1)

  (** [s ∈ subset_closure t] iff there exists [s' ∈ t] such that [s ⊆ s'] *)
  let subset_closure =
    fix1 @@ fun subset_closure -> function
    | Empty -> empty
    | Base -> base
    | Node { id = _; elt = x; zero = t0; one = t1 } ->
        let c0 = subset_closure t0 in
        let c1 = subset_closure t1 in
        node x (union base (union c0 c1)) c1

  (** [leq_FE_subset t1 t2] iff for every [S1 ∈ t1], there exists [S2 ∈ t2],
      such that [S1 ⊆ S2] *)
  let leq_FE_subset =
    fix2 ~sym:false @@ fun leq_FE_subset t1 t2 ->
    match (t1, t2) with
    | Empty, _ -> true
    | _, Empty -> false
    | Base, _ -> true
    | Node _, Base -> false
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then false
        else if n > 0 then leq_FE_subset t1 (union t20 t21)
        else (* n = 0 *)
          leq_FE_subset t10 (union t20 t21) && leq_FE_subset t11 t21

  (** [leq_FE_superset t1 t2] iff for every [S1 ∈ t1], there exists [S2 ∈ t2],
      such that [S1 ⊇ S2] *)
  let leq_FE_superset =
    fix2 ~sym:false @@ fun leq_FE_superset t1 t2 ->
    match (t1, t2) with
    | Empty, _ -> true
    | _, Empty -> false
    | _, Base -> true
    | Base, Node { id = _; elt = _; zero = t20; one = _ } ->
        leq_FE_superset base t20
    | ( Node { id = _; elt = x1; zero = t10; one = t11 },
        Node { id = _; elt = x2; zero = t20; one = t21 } ) ->
        let n = X.compare x1 x2 in
        if n < 0 then leq_FE_superset (union t10 t11) t2
        else if n > 0 then leq_FE_superset t1 t20
        else (* n = 0 *)
          leq_FE_superset t10 t20 && leq_FE_superset t11 (union t20 t21)

  (** [subst_gen union env t] substitutes in [t] the elements [x] such that
      [env x = Some sx] with [sx], with the interpretation of the set family [t]
      as a boolean expression in disjunctive normal form, using [union].
      Elements [x] such that [env x = None] are not modified, and are not
      removed. [subst_gen] performs memoization as soon as its two first
      arguments [union] and [env] are given. *)
  let subst_gen union env =
    fix1 @@ fun subst -> function
    | Empty -> empty
    | Base -> base
    | Node { id = _; elt = x; zero = t0; one = t1 } -> (
        let t0' = subst t0 and t1' = subst t1 in
        match env x with
        | None -> union t0' (join (node x empty base) t1')
        | Some sx -> union t0' (join sx t1'))

  (** [subst env t] substitutes in [t] the elements [x] such that
      [env x = Some sx] with [sx], with the interpretation of the set family [t]
      as a boolean expression in disjunctive normal form. Elements [x] such that
      [env x = None] are not modified, and are not removed. *)
  let subst env = subst_gen union env

  (** Iterator on the elements that occur in the set family. The elements might
      be encountered more than once, and the order in which they are encountered
      is unspecified. *)
  let iter_elt f =
    fix1 @@ fun iter -> function
    | Empty | Base -> ()
    | Node { id = _; elt; zero; one } ->
        f elt;
        iter zero;
        iter one

  (** Folder on the elements that occur in the set family. The elements might be
      encountered more than once, and the order in which they are encountered is
      unspecified. *)
  let fold_elt f =
    fix1 @@ fun fold -> function
    | Empty | Base -> fun acc -> acc
    | Node { id = _; elt; zero; one } ->
        let fold0 = fold zero in
        let fold1 = fold one in
        fun acc ->
          let acc = f elt acc in
          let acc = fold0 acc in
          fold1 acc

  (** Iterator on the list of elements that represent the sets in the families.
      The sets may occur in an unspecified order. The elements in the lists
      occur in increasing order. *)
  let iter =
    let g =
      fix1 @@ fun iter -> function
      | Empty -> fun _ -> ()
      | Base -> fun f -> f []
      | Node { id = _; elt; zero; one } ->
          let g0 = iter zero in
          let g1 = iter one in
          fun f ->
            g0 f;
            g1 (fun l -> f (elt :: l))
    in
    fun f t -> g t f

  (** Folder on the list of elements that represent the sets in the families.
      The sets may occur in an unspecified order. The elements in the lists
      occur in increasing order. *)
  let fold f t acc =
    let g =
      fix1 @@ fun fold -> function
      | Empty -> fun _f acc -> acc
      | Base -> fun f acc -> f [] acc
      | Node { id = _; elt; zero; one } ->
          let g0 = fold zero in
          let g1 = fold one in
          fun f acc -> g1 (fun l acc -> f (elt :: l) acc) (g0 f acc)
    in
    g t f acc

  module IntSet = Set.Make (Int)

  (** Pretty-printer of the representation of the ZDD as a graph in the DOT
      format. Dashed edges are 0 edges, solid edges are 1 edges. *)
  let pp_dot fmt t =
    let open Format in
    let seen = ref IntSet.empty in
    let register id = seen := IntSet.add id !seen in
    let rec browse t =
      let id = get_id t in
      if not @@ IntSet.mem id !seen then (
        register id;
        match t with
        | Empty -> fprintf fmt "@ %i [label=\"%s\"];" id "⊥"
        | Base -> fprintf fmt "@ %i [label=\"%s\"];" id "⊤"
        | Node { id = _; elt; zero; one } ->
            fprintf fmt "@ %i [label=\"%a\",ordering=out];" id X.pp elt;
            fprintf fmt "@ %i -> %i [style=dashed];" id (get_id zero);
            fprintf fmt "@ %i -> %i [style=solid];" id (get_id one);
            browse zero;
            browse one)
    in
    fprintf fmt "digraph@.@[<v>@[<v 2>{";
    browse t;
    fprintf fmt "@]@ @]}"
end