Source file zddZE.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
    | WithEmpty of { id : int; node : t }
    | 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 *)
  (* no two WithEmpty in a row *)
  (* no WithEmpty of a node whose zero node is WithEmpty *)

  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
    | WithEmpty { 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 -> true
      | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 } ->
          t1 == t2
      | ( 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
      | WithEmpty { id = _; node } -> Hashtbl.seeded_hash seed (get_id node)
      | 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 "∅"
    | WithEmpty { id = _; node } -> fprintf fmt "@[{ ∅ } ∪ @[%a@]@]" pp node
    | Node
        {
          id = _;
          elt = x;
          zero = Empty;
          one = WithEmpty { id = _; node = Empty };
        } ->
        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 = WithEmpty { id = _; node = Empty } }
      ->
        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 = WithEmpty { id = base_id; node = Empty }

  (** 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
    | WithEmpty { id = _; node = Empty } -> true
    | _ -> false

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

  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 | WithEmpty { id = _; node = Empty } -> true
    | WithEmpty { id = _; node = WithEmpty _ }
    | WithEmpty
        { id = _; node = Node { id = _; elt = _; zero = WithEmpty _; one = _ } }
      ->
        false
    | WithEmpty { id = _; node } -> wf node
    | Node { id = _; elt = x; zero = t0; one = t1 } ->
        ((match t0 with
         | Empty | WithEmpty { id = _; node = Empty } -> true
         | WithEmpty { id = _; node = WithEmpty _ } -> false
         | WithEmpty { id = _; node = Node { elt; _ } } | Node { elt; _ } ->
             X.compare x elt < 0)
        &&
        match t1 with
        | Empty | WithEmpty { id = _; node = WithEmpty _ } -> false
        | WithEmpty { id = _; node = Empty } -> true
        | WithEmpty { id = _; node = Node { elt; _ } } | 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
    | WithEmpty _ -> []
    | 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
    | WithEmpty _ -> 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 -> []
    | WithEmpty { id = _; node } -> [] :: to_list node
    | 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
    | WithEmpty { id = _; node } -> Seq.cons [] (to_seq node)
    | 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
    | WithEmpty { id = _; node } -> plus one (cardinal node)
    | 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
    | WithEmpty { id = _; node } -> 1 + cardinal node
    | 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
    | WithEmpty { id = _; node } -> max 0 (max_cardinal node)
    | 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
    | WithEmpty _ -> 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 -> 0
    | WithEmpty { id = _; node } -> 1 + nb_nodes node
    | 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 -> empty
    | WithEmpty { id = _; node } -> with_elt node
    | 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 -> empty
    | WithEmpty { id = _; node } -> on_elt node
    | 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
    | WithEmpty { id = _; node } -> with_empty (without_elt node)
    | 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
    | WithEmpty { id = _; node } -> with_empty (change_elt node)
    | 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
    | (WithEmpty _ | Node _), Empty | WithEmpty _, Node _ -> false
    | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 }
    | (Node _ as t1), WithEmpty { id = _; node = t2 } ->
        subset t1 t2
    | ( 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
    | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 }
    | WithEmpty { id = _; node = t1 }, (Node _ as t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } ->
        with_empty (union t1 t2)
    | ( 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
    | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 } ->
        with_empty (inter t1 t2)
    | WithEmpty { id = _; node = t1 }, (Node _ as t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } ->
        inter t1 t2
    | ( 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
    | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 } ->
        diff t1 t2
    | WithEmpty { id = _; node = t1 }, (Node _ as t2) -> with_empty (diff t1 t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } -> diff t1 t2
    | ( 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
    | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 } ->
        sym_diff t1 t2
    | WithEmpty { id = _; node = t1 }, (Node _ as t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } ->
        with_empty (sym_diff t1 t2)
    | ( 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
    | WithEmpty { id = _; node = t1' }, WithEmpty { id = _; node = t2' } ->
        with_empty (union (union t1 t2) (join t1' t2'))
    | WithEmpty { id = _; node = t1 }, (Node _ as t2) -> union (join t1 t2) t2
    | (Node _ as t1), WithEmpty { id = _; node = t2 } -> union t1 (join t1 t2)
    | ( 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
    | WithEmpty { id = _; node = t1' }, WithEmpty { id = _; node = t2' } ->
        with_empty (union (union t1' t2') (disjoint_join t1' t2'))
    | WithEmpty { id = _; node = t1 }, (Node _ as t2) ->
        union t2 (disjoint_join t1 t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } ->
        union t1 (disjoint_join t1 t2)
    | ( 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 -> empty
    | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 }
    | WithEmpty { id = _; node = t1 }, (Node _ as t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } ->
        joint_join t1 t2
    | ( 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
    | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 }
    | WithEmpty { id = _; node = t1 }, (Node _ as t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } ->
        with_empty (meet t1 t2)
    | ( 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
    | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 } ->
        with_empty (union (union t1 t2) (delta t1 t2))
    | WithEmpty { id = _; node = t1 }, (Node _ as t2) -> union t2 (delta t1 t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } -> union t1 (delta t1 t2)
    | ( 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
    | WithEmpty { id = _; node = t1' }, WithEmpty { id = _; node = t2' } ->
        with_empty (union t1 (minus t1' t2'))
    | WithEmpty { id = _; node = t1 }, (Node _ as t2) ->
        with_empty (minus t1 t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } -> union t1 (minus t1 t2)
    | ( 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, WithEmpty { id = _; node = Empty } -> t
    | WithEmpty { id = _; node = Empty }, _ -> empty
    | WithEmpty { id = _; node = t1' }, WithEmpty { id = _; node = t2' } ->
        inter t1 (div t1' t2')
    | (Node _ as t1), WithEmpty { id = _; node = t2 } -> inter t1 (div t1 t2)
    | WithEmpty { id = _; node = t1 }, (Node _ as t2) -> div t1 t2
    | ( 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
    | WithEmpty { id = _; node } -> with_empty (remove node)
    | 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, _ | _, WithEmpty _ -> t1
    | _, Empty -> empty
    | WithEmpty { id = _; node = t1 }, (Node _ as t2) -> restrict t1 t2
    | ( 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, _ | _, Empty -> empty
    | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 } ->
        with_empty (permit t1 t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } -> permit t1 t2
    | WithEmpty { id = _; node = t1 }, (Node _ as t2) ->
        with_empty (permit t1 t2)
    | ( 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
    | t, Empty -> t
    | _, WithEmpty _ -> empty
    | WithEmpty { id = _; node = t1 }, (Node _ as t2) ->
        with_empty (non_superset t1 t2)
    | ( 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
    | t, Empty -> t
    | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 }
    | WithEmpty { id = _; node = t1 }, (Node _ as t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } ->
        non_subset t1 t2
    | ( 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
    | WithEmpty { id = _; node = Empty } -> base
    | WithEmpty { id = _; node } -> maxima node
    | 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
    | WithEmpty _ -> 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 | WithEmpty _ -> 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
    | WithEmpty { id = _; node } -> with_empty (closure node)
    | 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
    | WithEmpty { id = _; node = Empty } -> base
    | WithEmpty { id = _; node } -> subset_closure node
    | Node { id = _; elt = x; zero = t0; one = t1 } ->
        let c0 = subset_closure t0 in
        let c1 = subset_closure t1 in
        with_empty (node x (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
    | WithEmpty { id = _; node = t1 }, WithEmpty { id = _; node = t2 }
    | WithEmpty { id = _; node = t1 }, (Node _ as t2)
    | (Node _ as t1), WithEmpty { id = _; node = t2 } ->
        leq_FE_subset t1 t2
    | ( 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, _ | _, WithEmpty _ -> true
    | _, Empty | WithEmpty _, Node _ -> 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 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
    | WithEmpty { id = _; node } -> with_empty (subst node)
    | 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 -> ()
    | WithEmpty { id = _; node } -> iter node
    | 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 -> fun acc -> acc
    | WithEmpty { id = _; node } -> fold node
    | 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 _ -> ()
      | WithEmpty { id = _; node } ->
          let g = iter node in
          fun f ->
            f [];
            g 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
      | WithEmpty { id = _; node } ->
          let g = fold node in
          fun f acc -> g f (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. Edges that
      start with a dot are 0-attributed 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 "⊥"
        | WithEmpty { id = _; node } ->
            fprintf fmt "@ %i -> %i [dir=both,arrowtail=dot];" id (get_id node);
            browse node
        | Node { id = _; elt; zero; one = WithEmpty { id = _; node = 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 [dir=both,arrowtail=dot,style=solid];" id
              (get_id one);
            browse zero;
            browse one
        | 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