Conversion to ZDDs

Conversion from Binary Decision Diagrams . More...

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

Detailed Description

Conversion from Binary Decision Diagrams .

Function Documentation

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.