A Zero-suppressed Decision Diagram (ZDD) represents a family of a set of \( n \) numbers, i.e. an \( S \subseteq 2^{\{ 0, 1, \dots, n-1 \}} \). More...

Classes
class	adiar::__zdd
	A (possibly unreduced) Zero-suppressed Decision Diagram. More...

class	adiar::zdd
	Reduced Ordered Zero-suppressed Decision Diagram. More...

Basic ZDD Constructors
To construct a more complex but well-structured zdd by hand, please use the zdd_builder (see builder) instead.
zdd	adiar::zdd_terminal (bool value)
	The ZDD of only a single terminal.

zdd	adiar::zdd_empty ()
	The empty family, i.e. Ø .

zdd	adiar::zdd_null ()
	The family only with the empty set, i.e. { Ø } .

zdd	adiar::zdd_ithvar (zdd::label_type var, const generator< zdd::label_type > &dom)
	The set of bitvectors over a given domain where var is set to true.

template<typename ForwardIt >
zdd	adiar::zdd_ithvar (zdd::label_type var, ForwardIt begin, ForwardIt end)
	The set of bitvectors over a given domain where var is set to true.

zdd	adiar::zdd_ithvar (zdd::label_type var)
	The set of bitvectors over the globally set domain where var is set to true.

zdd	adiar::zdd_nithvar (zdd::label_type var, const generator< zdd::label_type > &dom)
	The set of bitvectors over a given domain where var is set to false.

template<typename ForwardIt >
zdd	adiar::zdd_nithvar (zdd::label_type var, ForwardIt begin, ForwardIt end)
	The set of bitvectors over a given domain where var is set to false.

zdd	adiar::zdd_nithvar (zdd::label_type var)
	The set of bitvectors over the globally set domain where var is set to false.

zdd	adiar::zdd_vars (const generator< zdd::label_type > &vars)
	The family { { 1, 2, ..., k } }.

template<typename ForwardIt >
zdd	adiar::zdd_vars (ForwardIt begin, ForwardIt end)
	The family { { 1, 2, ..., k } }.

zdd	adiar::zdd_point (const generator< zdd::label_type > &vars)
	The family { { 1, 2, ..., k } } with a single bit-vector.

template<typename ForwardIt >
zdd	adiar::zdd_point (ForwardIt begin, ForwardIt end)
	The family { { 1, 2, ..., k } } with a single bit-vector.

zdd	adiar::zdd_singleton (zdd::label_type var)
	The family { {i} } .

zdd	adiar::zdd_singletons (const generator< zdd::label_type > &vars)
	The family { {1}, {2}, ..., {k} }.

template<typename ForwardIt >
zdd	adiar::zdd_singletons (ForwardIt begin, ForwardIt end)
	The family { {1}, {2}, ..., {k} }.

zdd	adiar::zdd_powerset (const generator< zdd::label_type > &vars)
	The powerset of all given variables.

template<typename ForwardIt >
zdd	adiar::zdd_powerset (ForwardIt begin, ForwardIt end)
	The powerset of all given variables.

zdd	adiar::zdd_bot (const generator< zdd::label_type > &dom)
	Bottom of the powerset lattice.

template<typename ForwardIt >
zdd	adiar::zdd_bot (ForwardIt begin, ForwardIt end)
	Bottom of the powerset lattice.

zdd	adiar::zdd_bot ()
	Bottom of the powerset lattice.

zdd	adiar::zdd_top (const generator< zdd::label_type > &dom)
	Top of the powerset lattice.

template<typename ForwardIt >
zdd	adiar::zdd_top (ForwardIt begin, ForwardIt end)
	Top of the powerset lattice.

zdd	adiar::zdd_top ()
	Top of the powerset lattice.

Basic ZDD Manipulation
__zdd	adiar::zdd_binop (const zdd &A, const zdd &B, const predicate< bool, bool > &op)
	Apply a binary operator between the sets of two families.

__zdd	adiar::zdd_binop (const exec_policy &ep, const zdd &A, const zdd &B, const predicate< bool, bool > &op)
	Apply a binary operator between the sets of two families.

__zdd	adiar::zdd_union (const zdd &A, const zdd &B)
	The union of two families of sets.

__zdd	adiar::zdd_union (const exec_policy &ep, const zdd &A, const zdd &B)
	The union of two families of sets.

__zdd	adiar::operator\| (const zdd &lhs, const zdd &rhs)

zdd	adiar::operator+ (const zdd &A)

__zdd	adiar::operator+ (const zdd &lhs, const zdd &rhs)

__zdd	adiar::zdd_intsec (const zdd &A, const zdd &B)
	The intersection of two families of sets.

__zdd	adiar::zdd_intsec (const exec_policy &ep, const zdd &A, const zdd &B)
	The intersection of two families of sets.

__zdd	adiar::operator& (const zdd &lhs, const zdd &rhs)

__zdd	adiar::operator* (const zdd &lhs, const zdd &rhs)

__zdd	adiar::zdd_diff (const zdd &A, const zdd &B)
	The set difference of two families of sets.

__zdd	adiar::zdd_diff (const exec_policy &ep, const zdd &A, const zdd &B)
	The set difference of two families of sets.

__zdd	adiar::operator- (const zdd &A)

__zdd	adiar::operator- (const zdd &lhs, const zdd &rhs)

__zdd	adiar::zdd_change (const zdd &A, const generator< zdd::label_type > &vars)
	The symmetric difference between each set in the family and the given set of variables.

__zdd	adiar::zdd_change (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &vars)
	The symmetric difference between each set in the family and the given set of variables.

template<typename ForwardIt >
__zdd	adiar::zdd_change (const zdd &A, ForwardIt begin, ForwardIt end)
	The symmetric difference between each set in the family and the given set of variables.

template<typename ForwardIt >
__zdd	adiar::zdd_change (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	The symmetric difference between each set in the family and the given set of variables.

__zdd	adiar::zdd_complement (const zdd &A, const generator< zdd::label_type > &dom)
	Complement of A within the given domain.

__zdd	adiar::zdd_complement (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &dom)
	Complement of A within the given domain.

template<typename ForwardIt >
__zdd	adiar::zdd_complement (const zdd &A, ForwardIt begin, ForwardIt end)
	Complement of A within the given domain.

template<typename ForwardIt >
__zdd	adiar::zdd_complement (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Complement of A within the given domain.

__zdd	adiar::zdd_complement (const zdd &A)
	Complement of A within the global Variable Domain.

__zdd	adiar::zdd_complement (const exec_policy &ep, const zdd &A)
	Complement of A within the global Variable Domain.

__zdd	adiar::operator~ (const zdd &A)

__zdd	adiar::zdd_expand (const zdd &A, const generator< zdd::label_type > &vars)
	Expands the domain of the given ZDD to also include the given set of labels.

__zdd	adiar::zdd_expand (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &vars)
	Expands the domain of the given ZDD to also include the given set of labels.

template<typename ForwardIt >
__zdd	adiar::zdd_expand (const zdd &A, ForwardIt begin, ForwardIt end)
	Expands the domain of the given ZDD to also include the given set of labels.

template<typename ForwardIt >
__zdd	adiar::zdd_expand (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Expands the domain of the given ZDD to also include the given set of labels.

__zdd	adiar::zdd_offset (const zdd &A, zdd::label_type var)
	Subset that do not include the given element.

__zdd	adiar::zdd_offset (const exec_policy &ep, const zdd &A, zdd::label_type var)
	Subset that do not include the given element.

__zdd	adiar::zdd_offset (const zdd &A)
	Subset that do not include the top variable.

__zdd	adiar::zdd_offset (const exec_policy &ep, const zdd &A)
	Subset that do not include the top variable.

__zdd	adiar::zdd_offset (const zdd &A, const generator< zdd::label_type > &vars)
	Subset that do not include the given set of variables.

__zdd	adiar::zdd_offset (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &vars)
	Subset that do not include the given set of variables.

template<typename ForwardIt >
__zdd	adiar::zdd_offset (const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do not include the given set of variables.

template<typename ForwardIt >
__zdd	adiar::zdd_offset (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do not include the given set of variables.

__zdd	adiar::zdd_onset (const zdd &A, zdd::label_type var)
	Subset that do include the given element.

__zdd	adiar::zdd_onset (const exec_policy &ep, const zdd &A, zdd::label_type var)
	Subset that do include the given element.

__zdd	adiar::zdd_onset (const zdd &A)
	Subset that do include the top variable.

__zdd	adiar::zdd_onset (const exec_policy &ep, const zdd &A)
	Subset that do include the top variable.

__zdd	adiar::zdd_onset (const zdd &A, const generator< zdd::label_type > &vars)
	Subset that do include the given set of variables.

__zdd	adiar::zdd_onset (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &vars)
	Subset that do include the given set of variables.

template<typename ForwardIt >
__zdd	adiar::zdd_onset (const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do include the given set of variables.

template<typename ForwardIt >
__zdd	adiar::zdd_onset (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do include the given set of variables.

__zdd	adiar::zdd_project (const zdd &A, const predicate< zdd::label_type > &dom)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

__zdd	adiar::zdd_project (const exec_policy &ep, const zdd &A, const predicate< zdd::label_type > &dom)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

__zdd	adiar::zdd_project (const zdd &A, const generator< zdd::label_type > &dom)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

__zdd	adiar::zdd_project (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &dom)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

template<typename ForwardIt >
__zdd	adiar::zdd_project (const zdd &A, ForwardIt begin, ForwardIt end)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

template<typename ForwardIt >
__zdd	adiar::zdd_project (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

ZDD Predicates
bool	adiar::zdd_iscanonical (const zdd &A)
	Check whether a given ZDD is canonical.

bool	adiar::zdd_isterminal (const zdd &A)
	Whether this ZDD represents a terminal.

bool	adiar::zdd_isfalse (const zdd &A)
	Whether this ZDD represents false terminal.

bool	adiar::zdd_isempty (const zdd &A)
	Whether it is the empty family, i.e. Ø .

bool	adiar::zdd_istrue (const zdd &A)
	Whether this BDD represents true terminal.

bool	adiar::zdd_isnull (const zdd &A)
	Whether it is the null family, i.e. { Ø } .

bool	adiar::zdd_ispoint (const zdd &A)
	Whether it contains a single bit-vector `a`, i.e. A = { a }.

bool	adiar::zdd_equal (const zdd &A, const zdd &B)
	Whether they represent the same family.

bool	adiar::zdd_equal (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether they represent the same family.

bool	adiar::operator== (const zdd &lhs, const zdd &rhs)

bool	adiar::zdd_unequal (const zdd &A, const zdd &B)
	Whether they represent two different families.

bool	adiar::zdd_unequal (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether they represent two different families.

bool	adiar::operator!= (const zdd &lhs, const zdd &rhs)

bool	adiar::zdd_subseteq (const zdd &A, const zdd &B)
	Whether one family is a subset or equal to the other.

bool	adiar::zdd_subseteq (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether one family is a subset or equal to the other.

bool	adiar::operator<= (const zdd &lhs, const zdd &rhs)

bool	adiar::operator>= (const zdd &lhs, const zdd &rhs)

bool	adiar::zdd_subset (const zdd &A, const zdd &B)
	Whether one family is a strict subset of the other.

bool	adiar::zdd_subset (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether one family is a strict subset of the other.

bool	adiar::operator< (const zdd &lhs, const zdd &rhs)

bool	adiar::operator> (const zdd &lhs, const zdd &rhs)

bool	adiar::zdd_disjoint (const zdd &A, const zdd &B)
	Whether the two families are disjoint.

bool	adiar::zdd_disjoint (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether the two families are disjoint.

ZDD Counting Operations
size_t	adiar::zdd_nodecount (const zdd &A)
	The number of (internal) nodes used to represent the family of sets.

zdd::label_type	adiar::zdd_varcount (const zdd &A)
	The number of variables that exist in the family of sets, i.e. the number of levels in the ZDD.

uint64_t	adiar::zdd_size (const zdd &A)
	The number of sets in the family of sets.

uint64_t	adiar::zdd_size (const exec_policy &ep, const zdd &A)
	The number of sets in the family of sets.

Set Elements
void	adiar::zdd_support (const zdd &A, const consumer< zdd::label_type > &cb)
	Get (in ascending order) all of the variable labels that occur in the family.

template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
OutputIt	adiar::zdd_support (const zdd &A, OutputIt iter)
	Copy all of the variable labels (in ascending order) that occur in the family into the given container.

zdd::label_type	adiar::zdd_topvar (const zdd &f)
	Get the root's variable label.

zdd::label_type	adiar::zdd_minvar (const zdd &A)
	Get the minimal occurring variable in the family.

zdd::label_type	adiar::zdd_maxvar (const zdd &A)
	Get the maximal occurring variable in the family.

bool	adiar::zdd_contains (const zdd &A, const generator< zdd::label_type > &a)
	Whether the family includes the given set of labels.

template<typename ForwardIt >
bool	adiar::zdd_contains (const zdd &A, ForwardIt begin, ForwardIt end)
	Whether the family includes the given set of labels.

zdd	adiar::zdd_minelem (const zdd &A)
	Retrieves the lexicographically smallest set a in A.

void	adiar::zdd_minelem (const zdd &A, const consumer< zdd::label_type > &cb)
	Retrieves the lexicographically smallest set a in A.

template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
OutputIt	adiar::zdd_minelem (const zdd &A, OutputIt iter)
	Retrieves the lexicographically smallest set a in A.

zdd	adiar::zdd_maxelem (const zdd &A)
	Retrieves the lexicographically largest set a in A.

void	adiar::zdd_maxelem (const zdd &A, const consumer< zdd::label_type > &cb)
	Retrieves the lexicographically largest set a in A.

template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
OutputIt	adiar::zdd_maxelem (const zdd &A, OutputIt iter)
	Retrieves the lexicographically largest set a in A.

Conversion to ZDDs
__zdd	adiar::zdd_from (const bdd &f, const generator< zdd::label_type > &dom)
	Obtains the ZDD that represents the same function/set as the given BDD within the given domain.

__zdd	adiar::zdd_from (const exec_policy &ep, const bdd &f, const generator< zdd::label_type > &dom)
	Obtains the ZDD that represents the same function/set as the given BDD within the given domain.

template<typename ForwardIt >
__zdd	adiar::zdd_from (const bdd &f, ForwardIt begin, ForwardIt end)
	Obtains the ZDD that represents the same function/set as the given BDD within the given domain.

template<typename ForwardIt >
__zdd	adiar::zdd_from (const exec_policy &ep, const bdd &f, ForwardIt begin, ForwardIt end)
	Obtains the ZDD that represents the same function/set as the given BDD within the given domain.

__zdd	adiar::zdd_from (const bdd &f)
	Obtains the ZDD that represents the same function/set as the given BDD within the global Variable Domain.

__zdd	adiar::zdd_from (const exec_policy &ep, const bdd &f)
	Obtains the BDD that represents the same function/set as the given ZDD within the global domain.

Dot Files of ZDDs
void	adiar::zdd_printdot (const zdd &A, std::ostream &out=std::cout, bool include_id=false)
	Output a DOT drawing of a ZDD to the given output stream.

void	adiar::zdd_printdot (const zdd &A, const std::string &file_name, bool include_id=false)
	Output a DOT drawing of a ZDD to the file with the given name.

Detailed Description

A Zero-suppressed Decision Diagram (ZDD) represents a family of a set of \( n \) numbers, i.e. an \( S \subseteq 2^{\{ 0, 1, \dots, n-1 \}} \).

The zdd class takes care of reference counting and optimal garbage collection of the underlying files. To ensure the most disk-space is available, try to garbage collect the zdd objects as quickly as possible and/or minimise the number of lvalues of said type.

Function Documentation

◆ operator!=()

bool adiar::operator!=	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also: zdd_unequal

◆ operator&()

__zdd adiar::operator&	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also: zdd_intsec

◆ operator*()

__zdd adiar::operator*	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also: zdd_intsec

◆ operator+()

zdd adiar::operator+ ( const zdd & A )

See also: zdd_union

◆ operator-() [1/2]

__zdd adiar::operator- ( const zdd & A )

See also: zdd_diff, zdd_complement

◆ operator-() [2/2]

__zdd adiar::operator-	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also: zdd_diff

◆ operator<()

bool adiar::operator<	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also: zdd_subset

◆ operator<=()

bool adiar::operator<=	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also: zdd_subseteq

◆ operator==()

bool adiar::operator==	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also: zdd_equal

◆ operator>()

bool adiar::operator>	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also: zdd_subset

◆ operator>=()

bool adiar::operator>=	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also: zdd_subseteq

◆ operator|()

__zdd adiar::operator\|	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also: zdd_union

◆ operator~()

__zdd adiar::operator~ ( const zdd & A )

See also: zdd_complement

◆ zdd_binop()

__zdd adiar::zdd_binop	(	const zdd &	A,
		const zdd &	B,
		const predicate< bool, bool > &	op
	)

Apply a binary operator between the sets of two families.

Parameters

A	ZDD for the left-hand-side of the operator
B	ZDD for the right-hand-side of the operator
op	Binary predicate to combine the two families.

Returns: Product construction of the two that represents the boolean operator applied to the two family of sets.

◆ zdd_bot() [1/3]

zdd adiar::zdd_bot ( )

Bottom of the powerset lattice.

See also: zdd_empty

◆ zdd_bot() [2/3]

zdd adiar::zdd_bot ( const generator< zdd::label_type > & dom )

Bottom of the powerset lattice.

Parameters

dom	Generator function of the variables in descending order. These values may not exceed `zdd::max_label`.

See also: zdd_empty

◆ zdd_bot() [3/3]

template<typename ForwardIt >

zdd adiar::zdd_bot	(	ForwardIt	begin,
		ForwardIt	end
	)

inline

Bottom of the powerset lattice.

Parameters

begin	Single-pass forward iterator that provides the domain's variables in descending order. The variables may not exceed `zdd::max_label`.
end	Marks the end for `begin`.

See also: zdd_empty

◆ zdd_change() [1/2]

__zdd adiar::zdd_change	(	const zdd &	A,
		const generator< zdd::label_type > &	vars
	)

The symmetric difference between each set in the family and the given set of variables.

Parameters

A	ZDD to apply with the other.
vars	Generator function of labels to flip in ascending order. These values may not exceed `zdd::max_label`.

Returns: \( \{ \mathit{vars} \Delta a \mid a \in A \} \)

◆ zdd_change() [2/2]

template<typename ForwardIt >

__zdd adiar::zdd_change	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

The symmetric difference between each set in the family and the given set of variables.

Parameters

A	ZDD to apply with the other.
begin	Single-pass forward iterator that provides the to-be flipped variables in ascending order. These values may not exceed `zdd::max_label`.
end	Marks the end for `begin`.

Returns: \( \{ \mathit{vars} \Delta a \mid a \in A \} \)

◆ zdd_complement() [1/3]

__zdd adiar::zdd_complement ( const zdd & A )

Complement of A within the global Variable Domain.

Parameters

A	family of sets to complement

Precondition: The global Variable Domain is set to a set of variables that is equals to or a superset of the variables in A.

Returns: \( 2^{\mathit{dom}} \setminus A \)

See also: domain_set domain_isset

◆ zdd_complement() [2/3]

__zdd adiar::zdd_complement	(	const zdd &	A,
		const generator< zdd::label_type > &	dom
	)

Complement of A within the given domain.

Parameters

A	family of sets to complement
dom	Labels of the domain in ascending order

Returns: \( 2^{\mathit{dom}} \setminus A \)

◆ zdd_complement() [3/3]

template<typename ForwardIt >

__zdd adiar::zdd_complement	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Complement of A within the given domain.

Parameters

A	family of sets to complement
begin	Single-pass forward iterator that provides the domain's variables in ascending order. These values may not exceed `zdd::max_label`.
end	Marks the end for `begin`.

Returns: \( 2^{\mathit{dom}} \setminus A \)

◆ zdd_contains() [1/2]

bool adiar::zdd_contains	(	const zdd &	A,
		const generator< zdd::label_type > &	a
	)

Whether the family includes the given set of labels.

Parameters

A	Set of interest
a	Generator of a bit-vector in ascending order. All variables geneated should be smaller than or equal to `zdd::max_label`.

Returns: Whether \( a \in A \)

◆ zdd_contains() [2/2]

template<typename ForwardIt >

bool adiar::zdd_contains	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Whether the family includes the given set of labels.

Parameters

A	Set of interest
begin	Single-pass forward iterator of the set of labels in ascending order. All its values should be smaller than or equals to `zdd::max_label`.
end	Marks the end for `begin`.

Returns: Whether \( \{\mathit{begin}, \dots, \mathit{end}\} \in A \)

◆ zdd_diff()

__zdd adiar::zdd_diff	(	const zdd &	A,
		const zdd &	B
	)

The set difference of two families of sets.

Returns: \( A \setminus B \)

◆ zdd_expand() [1/2]

__zdd adiar::zdd_expand	(	const zdd &	A,
		const generator< zdd::label_type > &	vars
	)

Expands the domain of the given ZDD to also include the given set of labels.

Adds don't care nodes on each levels in vars. That is, this essentially is the inverse of the zdd_project and lifts the set of sets unprojects to a larger domain.

Parameters

A	Family of set to expand.
vars	Generator function of labels to unproject in ascending order. No variables it generates may already exist in `A` or exceed `zdd::max_label`.

Returns: \( \bigcup_{a \in A, i \in 2^{vars}} (a \cup i) \)

◆ zdd_expand() [2/2]

template<typename ForwardIt >

__zdd adiar::zdd_expand	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Expands the domain of the given ZDD to also include the given set of labels.

Parameters

A	Family of set to expand.
begin	Single-pass forward iterator that provides the to-be unprojected variables in ascending order. These may not be present in `A` or exceed `zdd::max_label`.
end	Marks the end for `begin`.

Returns: \( \bigcup_{a \in A, i \in 2^{vars}} (a \cup i) \)

See also: zdd_project

◆ zdd_from() [1/3]

__zdd adiar::zdd_from ( const bdd & f )

Obtains the ZDD that represents the same function/set as the given BDD within the global Variable Domain.

Parameters

f	Boolean function with the given domain

Precondition: The global Variable Domain is set to a set of variables that is equals to or a superset of the variables in A.

Returns: ZDD that is true for the exact same assignments to variables in the global domain.

◆ zdd_from() [2/3]

__zdd adiar::zdd_from	(	const bdd &	f,
		const generator< zdd::label_type > &	dom
	)

Obtains the ZDD that represents the same function/set as the given BDD within the given domain.

Parameters

f	Boolean function with the given domain
dom	Domain of all variables in ascending order. All generated values should be smaller than or equals to `zdd::max_label`.

Returns: ZDD that is true for the exact same assignments to variables in the given domain.

◆ zdd_from() [3/3]

template<typename ForwardIt >

__zdd adiar::zdd_from	(	const bdd &	f,
		ForwardIt	begin,
		ForwardIt	end
	)

Obtains the ZDD that represents the same function/set as the given BDD within the given domain.

Parameters

f	Boolean function with the given domain
begin	Single-pass forward iterator that provides the domain's variables in ascending order. None of its values may exceed `zdd::max_label`.
end	Marks the end for `begin`.

Returns: ZDD that is true for the exact same assignments to variables in the given domain.

◆ zdd_intsec()

__zdd adiar::zdd_intsec	(	const zdd &	A,
		const zdd &	B
	)

The intersection of two families of sets.

Returns: \( A \cap B \)

◆ zdd_iscanonical()

bool adiar::zdd_iscanonical ( const zdd & A )

Check whether a given ZDD is canonical.

◆ zdd_ithvar() [1/3]

zdd adiar::zdd_ithvar ( zdd::label_type var )

The set of bitvectors over the globally set domain where var is set to true.

Parameters

var	The variable to be forced to true.

Precondition: domain_isset() == true and the variable var should occur in the global domain.

◆ zdd_ithvar() [2/3]

zdd adiar::zdd_ithvar	(	zdd::label_type	var,
		const generator< zdd::label_type > &	dom
	)

The set of bitvectors over a given domain where var is set to true.

This function is (given the same domain of variables) semantically equivalent to bdd_ithvar even though the ZDD DAG does not at all look like the BDD DAG.

Parameters

var	The variable to be forced to true.
dom	Generator function of the domain in descending order. These variables should be smaller than or equals to `zdd::max_label`.

Precondition: The variable var should occur in dom.

Exceptions

invalid_argument If dom is not in descending order.

◆ zdd_ithvar() [3/3]

template<typename ForwardIt >

zdd adiar::zdd_ithvar	(	zdd::label_type	var,
		ForwardIt	begin,
		ForwardIt	end
	)

The set of bitvectors over a given domain where var is set to true.

Parameters

var	The variable to be forced to true.
begin	Single-pass forward iterator that provides the domain's variables in descending order. The variables may not exceed `zdd::max_label`.
end	Marks the end for `begin`.

Precondition: The variable var should occur in dom.

Exceptions

invalid_argument If the iterator does not provide values in descending order.

◆ zdd_maxelem() [1/3]

zdd adiar::zdd_maxelem ( const zdd & A )

Retrieves the lexicographically largest set a in A.

Outputs the trace of the high-most path to the true terminal. The resulting assignment is lexicographically largest, where every variable is treated as a digit and \( x_0 > x_1 > \dots \).

Parameters

A	Set of sets of interest.

◆ zdd_maxelem() [2/3]

void adiar::zdd_maxelem	(	const zdd &	A,
		const consumer< zdd::label_type > &	cb
	)

Retrieves the lexicographically largest set a in A.

Parameters

A	Set of sets of interest.
cb	Callback function that is called with the variables of the largest set in ascending order of the levels of `A`.

Precondition: A != zdd_empty()

◆ zdd_maxelem() [3/3]

template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>

OutputIt adiar::zdd_maxelem	(	const zdd &	A,
		OutputIt	iter
	)

Retrieves the lexicographically largest set a in A.

Parameters

A	Set of sets of interest.
begin	Single-pass output iterator for where to place the output.

Returns: The output iterator at its final state.

◆ zdd_maxvar()

zdd::label_type adiar::zdd_maxvar ( const zdd & A )

Get the maximal occurring variable in the family.

Exceptions

invalid_argument If A is a terminal.

◆ zdd_minelem() [1/3]

zdd adiar::zdd_minelem ( const zdd & A )

Retrieves the lexicographically smallest set a in A.

Outputs the trace of the low-most path to the true terminal. The resulting assignment is lexicographically smallest, where every variable is treated as a digit and \( x_0 > x_1 > \dots \).

Parameters

A	Set of sets of interest.

◆ zdd_minelem() [2/3]

void adiar::zdd_minelem	(	const zdd &	A,
		const consumer< zdd::label_type > &	cb
	)

Retrieves the lexicographically smallest set a in A.

Parameters

A	Set of sets of interest.
cb	Callback function that is called with the variables of the smallest set in ascending order of the levels of `A`.

Precondition: A != zdd_empty()

◆ zdd_minelem() [3/3]

template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>

OutputIt adiar::zdd_minelem	(	const zdd &	A,
		OutputIt	iter
	)

Retrieves the lexicographically smallest set a in A.

Parameters

A	Set of sets of interest.
begin	Single-pass forward iterator for where to place the output.

Returns: The output iterator at its final state.

◆ zdd_minvar()

zdd::label_type adiar::zdd_minvar ( const zdd & A )

Get the minimal occurring variable in the family.

Exceptions

invalid_argument If A is a terminal.

◆ zdd_nithvar() [1/3]

zdd adiar::zdd_nithvar ( zdd::label_type var )

The set of bitvectors over the globally set domain where var is set to false.

Parameters

var	The variable to be forced to false.

Precondition: domain_isset() == true and the variable var should occur in the global domain.

◆ zdd_nithvar() [2/3]

zdd adiar::zdd_nithvar	(	zdd::label_type	var,
		const generator< zdd::label_type > &	dom
	)

The set of bitvectors over a given domain where var is set to false.

Creates a ZDD with a don't care chain of nodes to the true child except for the node for var; this one instead is forced to be true.

Parameters

var	The variable to be forced to false.
dom	Generator function of the domain in descending order. The variables should be smaller than or equals to `zdd::max_label`.

Precondition: The variable var should occur in dom.

Exceptions

invalid_argument If dom is not in descending order.

◆ zdd_nithvar() [3/3]

template<typename ForwardIt >

zdd adiar::zdd_nithvar	(	zdd::label_type	var,
		ForwardIt	begin,
		ForwardIt	end
	)

The set of bitvectors over a given domain where var is set to false.

Parameters

var	The variable to be forced to false.
begin	Single-pass forward iterator that provides the domain's variables in descending order. The variables may not exceed `zdd::max_label`.
end	Marks the end for `begin`.

Precondition: The variable var should occur in dom.

Exceptions

invalid_argument If the iterator does not provide values in descending order.

◆ zdd_offset() [1/4]

__zdd adiar::zdd_offset ( const zdd & A )

Subset that do not include the top variable.

Parameters

A	Family of set

Remarks: In other BDD packages, this function is good for traversing a ZDD. But, here this is not a constant-time operation but constructs an entire new ZDD of up-to linear size.

Exceptions

invalid_argument If A is a terminal.

◆ zdd_offset() [2/4]

__zdd adiar::zdd_offset	(	const zdd &	A,
		const generator< zdd::label_type > &	vars
	)

Subset that do not include the given set of variables.

Parameters

A	Family of set
vars	Generator function of the variable labels to filter on in ascending order. The values generated should not exceed `zdd::max_label`.

Returns: \( \{ a \in A \mid \forall i \in \mathit{vars} : i \not\in a \} \)

◆ zdd_offset() [3/4]

template<typename ForwardIt >

__zdd adiar::zdd_offset	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Subset that do not include the given set of variables.

Parameters

A	Family of set
begin	Single-pass forward iterator that provides the variables to filter out in ascending order. These values may not exceed `zdd::max_label`.
end	Marks the end for `begin`.

Returns: \( \{ a \in A \mid \forall i \in \mathit{vars} : i \not\in a \} \)

◆ zdd_offset() [4/4]

__zdd adiar::zdd_offset	(	const zdd &	A,
		zdd::label_type	var
	)

Subset that do not include the given element.

Parameters

A	Family of set
var	Variable to include.

Returns: \( \{ a \in A \mid \mathit{var} \not\in a \} \)

◆ zdd_onset() [1/4]

__zdd adiar::zdd_onset ( const zdd & A )

Subset that do include the top variable.

Parameters

A	Family of set

Remarks: In other BDD packages, this function is good for traversing a ZDD. But, here this is not a constant-time operation but constructs an entire new ZDD of up-to linear size.

Exceptions

invalid_argument If A is a terminal.

◆ zdd_onset() [2/4]

__zdd adiar::zdd_onset	(	const zdd &	A,
		const generator< zdd::label_type > &	vars
	)

Subset that do include the given set of variables.

Parameters

A	Family of set
vars	Generator function of the variable labels to filter on in ascending order. The values generated may not exceed `zdd::max_label`

Returns: \( \{ a \in A \mid \forall i \in \mathit{vars} : i \in a \} \)

◆ zdd_onset() [3/4]

template<typename ForwardIt >

__zdd adiar::zdd_onset	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Subset that do include the given set of variables.

Parameters

A	Family of set
begin	Single-pass forward iterator that provides the variables to filter out in ascending order. These values may not exceed `zdd::max_label`
end	Marks the end for `begin`.

Returns: \( \{ a \in A \mid \forall i \in \mathit{vars} : i \in a \} \)

◆ zdd_onset() [4/4]

__zdd adiar::zdd_onset	(	const zdd &	A,
		zdd::label_type	var
	)

Subset that do include the given element.

Parameters

A	Family of set
var	Variable to include.

Returns: \( \{ a \in A \mid \mathit{var} \in a \} \)

◆ zdd_point() [1/2]

zdd adiar::zdd_point ( const generator< zdd::label_type > & vars )

The family { { 1, 2, ..., k } } with a single bit-vector.

Creates the ZDD for a set with a single bit-vector, i.e. a point.

Parameters

vars	Generator function of the variables in descending order. The variables may not exceed `zdd::max_label`.

Exceptions

invalid_argument If vars are not in descending order.

◆ zdd_point() [2/2]

template<typename ForwardIt >

zdd adiar::zdd_point	(	ForwardIt	begin,
		ForwardIt	end
	)

The family { { 1, 2, ..., k } } with a single bit-vector.

Parameters

begin	Single-pass forward iterator that provides the variables in descending order. The variables may not exceed `zdd::max_label`.
end	Marks the end for `begin`.

Exceptions

invalid_argument If the iterator does not provide values in descending order.

◆ zdd_powerset() [1/2]

zdd adiar::zdd_powerset ( const generator< zdd::label_type > & vars )

The powerset of all given variables.

Creates a ZDD with a don't care chain of nodes to the true child.

Parameters

vars	Generator function of the variables in descending order. These values may not exceed `zdd::max_label`.

Exceptions

invalid_argument If vars are not in ascending order.

◆ zdd_powerset() [2/2]

template<typename ForwardIt >

zdd adiar::zdd_powerset	(	ForwardIt	begin,
		ForwardIt	end
	)

The powerset of all given variables.

Parameters

begin	Single-pass forward iterator that provides the variables in descending order. The variables may not exceed `zdd::max_label`
end	Marks the end for `begin`.

Exceptions

invalid_argument If the iterator does not provide values in descending order.

◆ zdd_project() [1/3]

__zdd adiar::zdd_project	(	const zdd &	A,
		const generator< zdd::label_type > &	dom
	)

Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

Parameters

A	Family of sets to project
dom	Generator function, that produces the variables of the domain in descending order. They should not exceed `zdd::max_label`.

Returns: \( \prod_{\mathit{dom}}(A) = \{ a \setminus \mathit{dom}^c \mid a \in A \} \)

See also: zdd_expand

◆ zdd_project() [2/3]

__zdd adiar::zdd_project	(	const zdd &	A,
		const predicate< zdd::label_type > &	dom
	)

Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

Parameters

A	Family of sets to project
dom	Predicate function that defines the domain.

Returns: \( \prod_{\mathit{dom}}(A) = \{ a \setminus \mathit{dom}^c \mid a \in A \} \)

See also: zdd_expand

◆ zdd_project() [3/3]

template<typename ForwardIt >

__zdd adiar::zdd_project	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

Parameters

A	Family of sets to project
begin	Single-pass forward iterator that provides the domain in descending order. Its values should not exceed `zdd::max_label`
end	Marks the end for `begin`.

Returns: \( \prod_{\mathit{dom}}(A) = \{ a \setminus \mathit{dom}^c \mid a \in A \} \)

See also: zdd_expand

◆ zdd_singleton()

zdd adiar::zdd_singleton ( zdd::label_type var )

The family { {i} } .

Creates a ZDD of a single node with label var and the children false and true. The given label must be smaller than zdd::max_label.

Parameters

var	The label of the desired variable to include

Exceptions

invalid_argument If var is a too large value.

◆ zdd_singletons() [1/2]

zdd adiar::zdd_singletons ( const generator< zdd::label_type > & vars )

The family { {1}, {2}, ..., {k} }.

Creates a ZDD with a chain of nodes on the 'low' arc to the true child, and false otherwise.

Parameters

vars	Generator function of the variables in descending order. The variables may not exceed `zdd::max_label`.

Exceptions

invalid_argument If vars are not in descending order.

◆ zdd_singletons() [2/2]

template<typename ForwardIt >

zdd adiar::zdd_singletons	(	ForwardIt	begin,
		ForwardIt	end
	)

The family { {1}, {2}, ..., {k} }.

Parameters

begin	Single-pass forward iterator that provides the variables in descending order. The variables may not exceed `zdd::max_label`.
end	Marks the end for `begin`.

Exceptions

invalid_argument If the iterator does not provide values in descending order.

◆ zdd_support() [1/2]

void adiar::zdd_support	(	const zdd &	A,
		const consumer< zdd::label_type > &	cb
	)

Get (in ascending order) all of the variable labels that occur in the family.

Parameters

A	ZDD of interest.
cb	Callback function that consumes the variable labels.

◆ zdd_support() [2/2]

template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>

OutputIt adiar::zdd_support	(	const zdd &	A,
		OutputIt	iter
	)

Copy all of the variable labels (in ascending order) that occur in the family into the given container.

Parameters

A	ZDD of interest.
begin	Single-pass output iterator for where to place the output.

Returns: The output iterator at its final state.

◆ zdd_terminal()

zdd adiar::zdd_terminal ( bool value )

The ZDD of only a single terminal.

Parameters

value The constant terminal value.

See also: zdd_empty zdd_null

◆ zdd_top() [1/3]

zdd adiar::zdd_top ( )

Top of the powerset lattice.

Since no set of variables is given, the global Variable Domain is used (if available).

See also: zdd_powerset, zdd_null

◆ zdd_top() [2/3]

zdd adiar::zdd_top ( const generator< zdd::label_type > & dom )

Top of the powerset lattice.

Parameters

dom	Generator of the variables in descending order. These values may not exceed `zdd::max_label`.

See also: zdd_powerset, zdd_null

◆ zdd_top() [3/3]

template<typename ForwardIt >

zdd adiar::zdd_top	(	ForwardIt	begin,
		ForwardIt	end
	)

inline

Top of the powerset lattice.

Parameters

begin	Single-pass forward iterator that provides the domain's variables in descending order. These values may not exceed `zdd::max_label`.
end	Marks the end for `begin`.

See also: zdd_empty

◆ zdd_topvar()

zdd::label_type adiar::zdd_topvar ( const zdd & f )

Get the root's variable label.

Exceptions

invalid_argument If A is a terminal.

◆ zdd_union()

__zdd adiar::zdd_union	(	const zdd &	A,
		const zdd &	B
	)

The union of two families of sets.

Returns: \( A \cup B \)

◆ zdd_vars() [1/2]

zdd adiar::zdd_vars ( const generator< zdd::label_type > & vars )

The family { { 1, 2, ..., k } }.

Creates a ZDD with a chain of nodes on the 'high' arc to the true child, and false otherwise.

Parameters

vars	Generator function of the variables in descending order. The variables may not exceed `zdd::max_label`.

Exceptions

invalid_argument If vars are not in descending order.

◆ zdd_vars() [2/2]

template<typename ForwardIt >

zdd adiar::zdd_vars	(	ForwardIt	begin,
		ForwardIt	end
	)

The family { { 1, 2, ..., k } }.

Parameters

begin	Single-pass forward iterator that provides the variables in descending order. The variables may not exceed `zdd::max_label`.
end	Marks the end for `begin`.

Exceptions

invalid_argument If the iterator does not provide values in descending order.

Classes

Basic ZDD Constructors

Basic ZDD Manipulation

ZDD Predicates

ZDD Counting Operations

Set Elements

Conversion to ZDDs

Dot Files of ZDDs

Detailed Description

Function Documentation

◆ operator!=()

◆ operator&()

◆ operator*()

◆ operator+()

◆ operator-() [1/2]

◆ operator-() [2/2]

◆ operator<()

◆ operator<=()

◆ operator==()

◆ operator>()

◆ operator>=()

◆ operator|()

◆ operator~()

◆ zdd_binop()

◆ zdd_bot() [1/3]

◆ zdd_bot() [2/3]

◆ zdd_bot() [3/3]

◆ zdd_change() [1/2]

◆ zdd_change() [2/2]

◆ zdd_complement() [1/3]

◆ zdd_complement() [2/3]

◆ zdd_complement() [3/3]

◆ zdd_contains() [1/2]

◆ zdd_contains() [2/2]

◆ zdd_diff()

◆ zdd_expand() [1/2]

◆ zdd_expand() [2/2]

◆ zdd_from() [1/3]

◆ zdd_from() [2/3]

◆ zdd_from() [3/3]

◆ zdd_intsec()

◆ zdd_iscanonical()

◆ zdd_ithvar() [1/3]

◆ zdd_ithvar() [2/3]

◆ zdd_ithvar() [3/3]

◆ zdd_maxelem() [1/3]

◆ zdd_maxelem() [2/3]

◆ zdd_maxelem() [3/3]

◆ zdd_maxvar()

◆ zdd_minelem() [1/3]

◆ zdd_minelem() [2/3]

◆ zdd_minelem() [3/3]

◆ zdd_minvar()

◆ zdd_nithvar() [1/3]

◆ zdd_nithvar() [2/3]

◆ zdd_nithvar() [3/3]

◆ zdd_offset() [1/4]

◆ zdd_offset() [2/4]

◆ zdd_offset() [3/4]

◆ zdd_offset() [4/4]

◆ zdd_onset() [1/4]

◆ zdd_onset() [2/4]

◆ zdd_onset() [3/4]

◆ zdd_onset() [4/4]

◆ zdd_point() [1/2]

◆ zdd_point() [2/2]

◆ zdd_powerset() [1/2]

◆ zdd_powerset() [2/2]

◆ zdd_project() [1/3]

◆ zdd_project() [2/3]

◆ zdd_project() [3/3]

◆ zdd_singleton()

◆ zdd_singletons() [1/2]

◆ zdd_singletons() [2/2]

◆ zdd_support() [1/2]

◆ zdd_support() [2/2]

◆ zdd_terminal()

◆ zdd_top() [1/3]

◆ zdd_top() [2/3]

◆ zdd_top() [3/3]