Source file zdd.ml

(** @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