Basic Constructors

Construction of constants, singletons, and points. More...

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

Detailed Description

Construction of constants, singletons, and points.

Remarks

To construct a more complex but well-structured zdd by hand, please use the zdd_builder (see builder) instead.

Function Documentation

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