Source file zdd_sigs.ml

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

(** Copyright Inria © 2025 *)

(** Signature of types for which set families can be created *)
module type T = sig
  type t

  val hash : t -> int
  (** Hash function *)

  val compare : t -> t -> int
  (** Total order *)

  val equal : t -> t -> bool
  (** Equality test *)

  val pp : Format.formatter -> t -> unit
  (** Pretty printer *)
end

(** The signature of set families *)
module type S = sig
  type elt

  type t
  (** Set families of finite sets over the type [elt], implemented as ZDDs *)

  val hash : t -> int
  (** Hash function *)

  val compare : t -> t -> int
  (** Total order *)

  val equal : t -> t -> bool
  (** Equality test *)

  val pp : Format.formatter -> t -> unit
  (** Pretty printer for ZDDs *)

  val empty : t
  (** The empty family: [∅] *)

  val is_empty : t -> bool
  (** Tests whether a ZDD is equal to [empty] *)

  val base : t
  (** The family that contains only the empty set: [{ ∅ }] *)

  val is_base : t -> bool
  (** Tests whether a ZDD is equal to [base] *)

  val wf : t -> bool
  (** Wellformedness test *)

  val singleton : elt list -> t
  (** [singleton [x1;... ; xn]] is the ZDD that represents the set family
      [{ { x1, ..., xn } }] *)

  val choose : t -> elt list
  (** Retrieves 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 *)

  val choose_opt : t -> elt list option
  (** Retrieves a set of the set family, if any. The choice of which set of the
      family is returned is not specified. *)

  val to_list : t -> elt list list
  (** Returns the sets that belong to a ZDD, as a list of lists of elements *)

  val to_seq : t -> elt list Seq.t
  (** Returns the sets that belong to a ZDD, as a sequence of lists of elements
  *)

  val cardinal_generic : ('a -> 'a -> 'a) -> 'a -> 'a -> t -> 'a
  (** [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]. *)

  val cardinal : t -> int
  (** [cardinal t] is the cardinal of the family represented by [t], i.e., how
      many sets it contains. *)

  val max_cardinal : t -> int
  (** [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. *)

  val min_cardinal : t -> int
  (** [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. *)

  val nb_nodes : t -> int
  (** Returns the number of nodes that are used to represent the ZDD *)

  val with_elt : elt -> t -> t
  (** [s ∈ with_elt y t] iff [s ∈ t] and [y ∈ s] *)

  val on_elt : elt -> t -> t
  (** [s ∈ on_elt y t] iff [{y} ∪ s ∈ t] and [y ∉ s] *)

  val without_elt : elt -> t -> t
  (** [s ∈ without_elt y t] iff [s ∈ t] and [y ∉ s] *)

  val off_elt : elt -> t -> t
  (** This is the same as [without_elt] *)

  val change_elt : elt -> t -> t
  (** [s ∈ change x t] iff either [x ∈ s] and [s ∖ {x} ∈ t], or [x ∉ s] and
      [{x} ∪ s ∈ t] *)

  val subset : t -> t -> bool
  (** [subset t1 t2] iff for every [s], [s ∈ t1] implies [s ∈ t2] *)

  val union : t -> t -> t
  (** [s ∈ inter t1 t2] iff [s ∈ t1] or [s ∈ t2] *)

  val inter : t -> t -> t
  (** [s ∈ inter t1 t2] iff [s ∈ t1] and [s ∈ t2] *)

  val diff : t -> t -> t
  (** [s ∈ diff t1 t2] iff [s ∈ t1] and [s ∉ t2] *)

  val sym_diff : t -> t -> t
  (** [s ∈ sym_diff t1 t2] iff either [s ∈ t1] and [s ∉ t2], or [s ∈ t2] and
      [s ∉ t1] *)

  val join : t -> t -> t
  (** [s ∈ join t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such that
      [s = s1 ∪ s2] *)

  val disjoint_join : t -> t -> t
  (** [s ∈ disjoint_join t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such
      that [s1 ∩ s2 = ∅] and [s = s1 ∪ s2] *)

  val joint_join : t -> t -> t
  (** [s ∈ joint_join t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such that
      [s1 ∩ s2 ≠ ∅] and [s = s1 ∪ s2] *)

  val meet : t -> t -> t
  (** [s ∈ meet t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such that
      [s = s1 ∩ s2] *)

  val delta : t -> t -> t
  (** [s ∈ delta t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such that
      [s = (s1 \ s2) ∪ (s2 \ s1)] *)

  val minus : t -> t -> t
  (** [s ∈ minus t1 t2] iff there exists [s1 ∈ t1] and [s2 ∈ t2] such that
      [s = s1 \ s2] *)

  val div : t -> t -> t
  (** When [t2 ≠ ∅]: [s ∈ div t1 t2] iff for any [s2 ∈ t2], [s ∪ s2 ∈ t1] and
      [s ∩ s2 = ∅]. When [t2 = ∅]: [div t1 t2 = t1]. *)

  val rem : t -> t -> t
  (** [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)]. **)

  val remove : elt -> t -> t
  (** [s ∈ remove y t] iff there exists [s' ∈ t] such that [s' = s \ { x }] *)

  val restrict : t -> t -> t
  (** [s ∈ restrict t1 t2] iff [s ∈ t1] and there exists [s' ∈ t2] such that
      [s' ⊆ s] *)

  val permit : t -> t -> t
  (** [s ∈ permit t1 t2] iff [s ∈ t1] and there exists [s' ∈ t2] such that
      [s ⊆ s'] *)

  val non_superset : t -> t -> t
  (** [s ∈ non_superset t1 t2] iff [s ∈ t1] and for every [s' ∈ t2], [s' ⊈ s] *)

  val non_subset : t -> t -> t
  (** [s ∈ non_subset t1 t2] iff [s ∈ t1] and for every [s' ∈ t2], [s ⊈ s'] *)

  val minima : t -> t
  (** [s ∈ maxima t] iff [s ∈ t] and for every [s' ∈ t], [s ⊆ s'] implies
      [s' ⊆ s] *)

  val maxima : t -> t
  (** [s ∈ minima t] iff [s ∈ t] and for every [s' ∈ t], [s' ⊆ s] implies
      [s ⊆ s'] *)

  val min_hitting_set : t -> t
  (** [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). *)

  val closure : t -> t
  (** [s ∈ closure t] iff there exists [t' ⊆ t] such that [s = ⋂ t'] *)

  val subset_closure : t -> t
  (** [s ∈ subset_closure t] iff there exists [s' ∈ t] such that [s ⊆ s'] *)

  val leq_FE_subset : t -> t -> bool
  (** [leq_FE_subset t1 t2] iff for every [S1 ∈ t1], there exists [S2 ∈ t2],
      such that [S1 ⊆ S2] *)

  val leq_FE_superset : t -> t -> bool
  (** [leq_FE_superset t1 t2] iff for every [S1 ∈ t1], there exists [S2 ∈ t2],
      such that [S1 ⊇ S2] *)

  val subst_gen : (t -> t -> t) -> (elt -> t option) -> t -> t
  (** [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] for
      disjunction. 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. *)

  val subst : (elt -> t option) -> t -> t
  (** [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. *)

  val iter_elt : (elt -> unit) -> t -> unit
  (** 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. *)

  val fold_elt : (elt -> 'a -> 'a) -> t -> 'a -> 'a
  (** 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. *)

  val iter : (elt list -> unit) -> t -> unit
  (** 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. *)

  val fold : (elt list -> 'a -> 'a) -> t -> 'a -> 'a
  (** 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. *)

  val pp_dot : Format.formatter -> t -> unit
  (** 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. *)
end

(** Signature of upward-closed sets, represented as the set of their minimal
    elements *)
module type UPSET = sig
  type elt
  type t

  val hash : t -> int
  (** Hash function *)

  val compare : t -> t -> int
  (** Total order *)

  val equal : t -> t -> bool
  (** Equality test *)

  val pp : Format.formatter -> t -> unit
  (** Pretty-printer *)

  val empty : t
  (** The empty family *)

  val full : t
  (** The full family *)

  val above : elt list -> t
  (** [above [x1;... ; xn]] is the family of the sets that include
      [{x1,..., xn}]. *)

  val subset : t -> t -> bool
  (** Inclusion test *)

  val union : t -> t -> t
  (** Union of set families *)

  val inter : t -> t -> t
  (** Intersection of set families *)

  val join : t -> t -> t
  (** [join t1 t2] is the upward closure of the family
      [{ s1 ∪ s2 | s1 ∈ t1, s2 ∈ t2 }]. This is the same as [inter s1 s2]. *)

  val meet : t -> t -> t
  (** [meet t1 t2] is the upward closure of the family
      [{ s1 ∩ s2 | s1 ∈ t1, s2 ∈ t2 }]. *)

  val minima : t -> elt list list
  (** The minimal elements of a family *)

  val subst : (elt -> t option) -> t -> t
  (** Substitution *)

  val iter_elt : (elt -> unit) -> t -> unit
  (** Iterator on the elements that occur in the minimal elements of the set
      family. The elements might be encountered more than once, and the order in
      which they are encountered is unspecified. *)

  val fold_elt : (elt -> 'a -> 'a) -> t -> 'a -> 'a
  (** Folder on the elements that occur in the minimal elements of the set
      family. The elements might be encountered more than once, and the order in
      which they are encountered is unspecified. *)

  val iter_minima : (elt list -> unit) -> t -> unit
  (** Iterator on the list of elements that represent the minimal sets in the
      families. The sets may occur in an unspecified order. The elements in the
      lists occur in increasing order. *)

  val fold_minima : (elt list -> 'a -> 'a) -> t -> 'a -> 'a
  (** Folder on the list of elements that represent the minimal sets in the
      families. The sets may occur in an unspecified order. The elements in the
      lists occur in increasing order. *)
end

(** Signature of downward-closed sets, represented as the set of their maximal
    elements *)
module type DOWNSET = sig
  type elt
  type t

  val hash : t -> int
  (** Hash function *)

  val compare : t -> t -> int
  (** Total order *)

  val equal : t -> t -> bool
  (** Equality test *)

  val pp : Format.formatter -> t -> unit
  (** Pretty-printer *)

  val empty : t
  (** The empty family *)

  val base : t
  (** The family [{ ∅ }] *)

  val below : elt list -> t
  (** [below [x1;... ; xn]] is the family of the sets that are included in
      [{x1,..., xn}]. *)

  val subset : t -> t -> bool
  (** Inclusion test *)

  val union : t -> t -> t
  (** Union of set families *)

  val inter : t -> t -> t
  (** Intersection of set families *)

  val join : t -> t -> t
  (** [join t1 t2] is the downward closure of the family
      [{ s1 ∪ s2 | s1 ∈ t1, s2 ∈ t2 }]. *)

  val meet : t -> t -> t
  (** [meet t1 t2] is the downward closure of the family
      [{ s1 ∩ s2 | s1 ∈ t1, s2 ∈ t2 }]. This is the same as [inter s1 s2]. *)

  val maxima : t -> elt list list
  (** The maximal elements of a family *)

  val subst : (elt -> t option) -> t -> t
  (** Substitution *)

  val iter_elt : (elt -> unit) -> t -> unit
  (** Iterator on the elements that occur in the maximal elements of the set
      family. The elements might be encountered more than once, and the order in
      which they are encountered is unspecified. *)

  val fold_elt : (elt -> 'a -> 'a) -> t -> 'a -> 'a
  (** Folder on the elements that occur in the maximal elements of the set
      family. The elements might be encountered more than once, and the order in
      which they are encountered is unspecified. *)

  val iter_maxima : (elt list -> unit) -> t -> unit
  (** Iterator on the list of elements that represent the maximal sets in the
      families. The sets may occur in an unspecified order. The elements in the
      lists occur in increasing order. *)

  val fold_maxima : (elt list -> 'a -> 'a) -> t -> 'a -> 'a
  (** Folder on the list of elements that represent the maximal sets in the
      families. The sets may occur in an unspecified order. The elements in the
      lists occur in increasing order. *)
end