zdd 0.5 · OCaml Package

Functor that creates a structure of set families

Parameters

module X : T

Signature

type elt = X.t

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.

raises 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.

package zdd

Parameters

Signature