package zdd

  1. Overview
  2. Docs

Module Zdd.Make_ZddZESource

Functor that creates a structure of set families using an implementation of ZDDs using zero-attributed edges

Parameters

module X : sig ... end

Signature

Sourcetype elt = X.t
Sourcetype t

Set families of finite sets over the type elt, implemented as ZDDs

Sourceval hash : t -> int

Hash function

Sourceval compare : t -> t -> int

Total order

Sourceval equal : t -> t -> bool

Equality test

Sourceval pp : Format.formatter -> t -> unit

Pretty printer for ZDDs

Sourceval empty : t

The empty family: ∅

Sourceval is_empty : t -> bool

Tests whether a ZDD is equal to empty

Sourceval base : t

The family that contains only the empty set: { ∅ }

Sourceval is_base : t -> bool

Tests whether a ZDD is equal to base

Sourceval wf : t -> bool

Wellformedness test

Sourceval singleton : elt list -> t

singleton [x1;... ; xn] is the ZDD that represents the set family { { x1, ..., xn } }

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

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

Sourceval to_list : t -> elt list list

Returns the sets that belong to a ZDD, as a list of lists of elements

Sourceval to_seq : t -> elt list Seq.t

Returns the sets that belong to a ZDD, as a sequence of lists of elements

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

Sourceval cardinal : t -> int

cardinal t is the cardinal of the family represented by t, i.e., how many sets it contains.

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

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

Sourceval nb_nodes : t -> int

Returns the number of nodes that are used to represent the ZDD

Sourceval with_elt : elt -> t -> t

s ∈ with_elt y t iff s ∈ t and y ∈ s

Sourceval on_elt : elt -> t -> t

s ∈ on_elt y t iff {y} ∪ s ∈ t and y ∉ s

Sourceval without_elt : elt -> t -> t

s ∈ without_elt y t iff s ∈ t and y ∉ s

Sourceval off_elt : elt -> t -> t

This is the same as without_elt

Sourceval change_elt : elt -> t -> t

s ∈ change x t iff either x ∈ s and s ∖ {x} ∈ t, or x ∉ s and {x} ∪ s ∈ t

Sourceval subset : t -> t -> bool

subset t1 t2 iff for every s, s ∈ t1 implies s ∈ t2

Sourceval union : t -> t -> t

s ∈ inter t1 t2 iff s ∈ t1 or s ∈ t2

Sourceval inter : t -> t -> t

s ∈ inter t1 t2 iff s ∈ t1 and s ∈ t2

Sourceval diff : t -> t -> t

s ∈ diff t1 t2 iff s ∈ t1 and s ∉ t2

Sourceval sym_diff : t -> t -> t

s ∈ sym_diff t1 t2 iff either s ∈ t1 and s ∉ t2, or s ∈ t2 and s ∉ t1

Sourceval join : t -> t -> t

s ∈ join t1 t2 iff there exists s1 ∈ t1 and s2 ∈ t2 such that s = s1 ∪ s2

Sourceval 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

Sourceval 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

Sourceval meet : t -> t -> t

s ∈ meet t1 t2 iff there exists s1 ∈ t1 and s2 ∈ t2 such that s = s1 ∩ s2

Sourceval delta : t -> t -> t

s ∈ delta t1 t2 iff there exists s1 ∈ t1 and s2 ∈ t2 such that s = (s1 \ s2) ∪ (s2 \ s1)

Sourceval minus : t -> t -> t

s ∈ minus t1 t2 iff there exists s1 ∈ t1 and s2 ∈ t2 such that s = s1 \ s2

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

Sourceval 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). *

Sourceval remove : elt -> t -> t

s ∈ remove y t iff there exists s' ∈ t such that s' = s \ { x }

Sourceval restrict : t -> t -> t

s ∈ restrict t1 t2 iff s ∈ t1 and there exists s' ∈ t2 such that s' ⊆ s

Sourceval permit : t -> t -> t

s ∈ permit t1 t2 iff s ∈ t1 and there exists s' ∈ t2 such that s ⊆ s'

Sourceval non_superset : t -> t -> t

s ∈ non_superset t1 t2 iff s ∈ t1 and for every s' ∈ t2, s' ⊈ s

Sourceval non_subset : t -> t -> t

s ∈ non_subset t1 t2 iff s ∈ t1 and for every s' ∈ t2, s ⊈ s'

Sourceval minima : t -> t

s ∈ maxima t iff s ∈ t and for every s' ∈ t, s ⊆ s' implies s' ⊆ s

Sourceval maxima : t -> t

s ∈ minima t iff s ∈ t and for every s' ∈ t, s' ⊆ s implies s ⊆ s'

Sourceval 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).

Sourceval closure : t -> t

s ∈ closure t iff there exists t' ⊆ t such that s = ⋂ t'

Sourceval subset_closure : t -> t

s ∈ subset_closure t iff there exists s' ∈ t such that s ⊆ s'

Sourceval leq_FE_subset : t -> t -> bool

leq_FE_subset t1 t2 iff for every S1 ∈ t1, there exists S2 ∈ t2, such that S1 ⊆ S2

Sourceval leq_FE_superset : t -> t -> bool

leq_FE_superset t1 t2 iff for every S1 ∈ t1, there exists S2 ∈ t2, such that S1 ⊇ S2

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

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

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

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

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

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

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