Input Variables

Information on variables in BDDs. More...

Functions
void	adiar::bdd_support (const bdd &f, const consumer< bdd::label_type > &cb)
	Get (in ascending order) all of the variable labels that occur in the BDD.
template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<bdd::label_type>>>>
OutputIt	adiar::bdd_support (const bdd &f, OutputIt iter)
	Copy all of the variable labels (in ascending order) that occur in the BDD into the given container.
bdd::label_type	adiar::bdd_topvar (const bdd &f)
	Get the root's variable label.
bdd::label_type	adiar::bdd_minvar (const bdd &f)
	Get the minimal occurring variable in the function's support.
bdd::label_type	adiar::bdd_maxvar (const bdd &f)
	Get the maximal occurring variable in the function's support.
bdd	adiar::bdd_satmin (const bdd &f)
	The lexicographically smallest cube x such that f(x) is true.
bdd	adiar::bdd_satmin (const bdd &f, const generator< bdd::label_type > &d, const size_t d_size=bdd::max_label+1)
	The lexicographically smallest x such that f(x) is true within the given domain.
template<typename ForwardIt , typename = enable_if<is_const<typename ForwardIt::reference>>>
bdd	adiar::bdd_satmin (const bdd &f, ForwardIt cbegin, ForwardIt cend)
	The lexicographically smallest x such that f(x) is true.
bdd	adiar::bdd_satmin (const bdd &f, const bdd &d)
	The lexicographically smallest x such that f(x) is true.
void	adiar::bdd_satmin (const bdd &f, const consumer< pair< bdd::label_type, bool > > &c)
	The lexicographically smallest x such that f(x) is true.
template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>> && !is_convertible<OutputIt, bdd>>>
OutputIt	adiar::bdd_satmin (const bdd &f, OutputIt iter)
	The lexicographically smallest x such that f(x) is true.
bdd	adiar::bdd_satmax (const bdd &f)
	The lexicographically largest cube x such that f(x) is true.
bdd	adiar::bdd_satmax (const bdd &f, const generator< bdd::label_type > &d, const size_t d_size=bdd::max_label+1)
	The lexicographically largest x such that f(x) is true within the given domain.
template<typename ForwardIt , typename = enable_if<is_const<typename ForwardIt::reference>>>
bdd	adiar::bdd_satmax (const bdd &f, ForwardIt cbegin, ForwardIt cend)
	The lexicographically largest x such that f(x) is true.
bdd	adiar::bdd_satmax (const bdd &f, const bdd &d)
	The lexicographically largest x such that f(x) is true.
void	adiar::bdd_satmax (const bdd &f, const consumer< pair< bdd::label_type, bool > > &c)
	The lexicographically largest x such that f(x) is true.
template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>> && !is_convertible<OutputIt, bdd>>>
OutputIt	adiar::bdd_satmax (const bdd &f, OutputIt iter)
	The lexicographically largest x such that f(x) is true.
pair< bdd, double >	adiar::bdd_optmin (const bdd &f, const cost< bdd::label_type > &c)
	Obtain the satisfying assignment that is minimal for the given linear cost function over the global domain.
double	adiar::bdd_optmin (const bdd &f, const cost< bdd::label_type > &c, const consumer< pair< bdd::label_type, bool > > &cb)
	Obtain the satisfying assignment that is minimal for the given linear cost function over the global domain.
bool	adiar::bdd_eval (const bdd &f, const predicate< bdd::label_type > &xs)
	Evaluate a BDD according to an assignment to its variables.
bool	adiar::bdd_eval (const bdd &f, const generator< pair< bdd::label_type, bool > > &xs)
	Evaluate a BDD according to an assignment to its variables.
template<typename ForwardIt >
bool	adiar::bdd_eval (const bdd &f, ForwardIt begin, ForwardIt end)
	Evaluate a BDD according to an assignment to its variables.

Detailed Description

Information on variables in BDDs.

Function Documentation

bdd_eval() [1/3]

bool adiar::bdd_eval	(	const bdd &	f,
		const generator< pair< bdd::label_type, bool > > &	xs
	)

Evaluate a BDD according to an assignment to its variables.

Parameters

f	The BDD to evaluate.
xs	Assignments (i,v) to variables in (in ascending order).

Exceptions

out_of_range	If traversal of the BDD leads to going beyond the end of the content of xs.
invalid_argument	If a level in the BDD does not exist in xs.

bdd_eval() [2/3]

bool adiar::bdd_eval	(	const bdd &	f,
		const predicate< bdd::label_type > &	xs
	)

Evaluate a BDD according to an assignment to its variables.

The given assignment function may assume/abuse that it is only called with the labels in a strictly increasing order.

Parameters

f	The BDD to evaluate
xs	An assignment function of the type \( \texttt{label\_t} \rightarrow \texttt{bool} \).

bdd_eval() [3/3]

template<typename ForwardIt >

bool adiar::bdd_eval	(	const bdd &	f,
		ForwardIt	begin,
		ForwardIt	end
	)

Evaluate a BDD according to an assignment to its variables.

Parameters

f	The BDD to evaluate.
begin	Single-pass forward iterator that provides the assignment in ascending order.
end	Marks the end for begin.

Exceptions

out_of_range	If traversal of the BDD leads to going beyond the end of the content of xs.
invalid_argument	If a level in the BDD does not exist in xs.

bdd_maxvar()

bdd::label_type adiar::bdd_maxvar

(

const bdd &

f

)

Get the maximal occurring variable in the function's support.

Exceptions

invalid_argument

If f is a terminal.

bdd_minvar()

bdd::label_type adiar::bdd_minvar

(

const bdd &

f

)

Get the minimal occurring variable in the function's support.

Exceptions

invalid_argument

If f is a terminal.

bdd_optmin() [1/2]

pair< bdd, double > adiar::bdd_optmin	(	const bdd &	f,
		const cost< bdd::label_type > &	c
	)

Obtain the satisfying assignment that is minimal for the given linear cost function over the global domain.

Parameters

f	The BDD of feasible solutions
c	A (pure) function that provides the cost function's coefficient.

Returns

A pair of a BDD cube with the best satisfying assignment and its cost. If no solution was found, returns the false constant and NaN

bdd_optmin() [2/2]

double adiar::bdd_optmin	(	const bdd &	f,
		const cost< bdd::label_type > &	c,
		const consumer< pair< bdd::label_type, bool > > &	cb
	)

Obtain the satisfying assignment that is minimal for the given linear cost function over the global domain.

Parameters

f	The BDD of feasible solutions
c	A (pure) function that provides the cost function's coefficient.
cb	A callback function that is called in descending order.

Returns

The cost of the satisfying solution if any, otherwise NaN.

Remarks

If f is a terminal, cb will never be called

bdd_satmax() [1/6]

bdd adiar::bdd_satmax

(

const bdd &

f

)

The lexicographically largest cube x such that f(x) is true.

Parameters

f	BDD of interest.

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

Returns

A bdd whos only path to the true terminal reflects the maximal assignment.

bdd_satmax() [2/6]

bdd adiar::bdd_satmax	(	const bdd &	f,
		const bdd &	d
	)

The lexicographically largest x such that f(x) is true.

Parameters

f	BDD of interest.
d	BDD cube of variables that ought to be included.

Returns

A bdd whos only path to the true terminal reflects the maximal assignment.

Exceptions

domain_error

If bdd_iscube(d) is not satisfied.

bdd_satmax() [3/6]

void adiar::bdd_satmax	(	const bdd &	f,
		const consumer< pair< bdd::label_type, bool > > &	c
	)

The lexicographically largest x such that f(x) is true.

Parameters

f	BDD of interest.
c	Consumer that is called in ascending order of the bdd's levels with the (var, value) pairs of the assignment.

bdd_satmax() [4/6]

bdd adiar::bdd_satmax	(	const bdd &	f,
		const generator< bdd::label_type > &	d,
		const size_t	d_size = bdd::max_label+1
	)

The lexicographically largest x such that f(x) is true within the given domain.

Parameters

f	BDD of interest.
d	Generator of domain in ascending order.
d_size	Upper bound on the number of elements generated by d.

Returns

A bdd whos only path to the true terminal reflects the maximal assignment.

bdd_satmax() [5/6]

template<typename ForwardIt , typename = enable_if<is_const<typename ForwardIt::reference>>>

bdd adiar::bdd_satmax	(	const bdd &	f,
		ForwardIt	cbegin,
		ForwardIt	cend
	)

The lexicographically largest x such that f(x) is true.

Parameters

f	BDD of interest.
cbegin	Single-pass forward iterator of immutable variables in ascending ordering.
cend	Marks the end for cbegin.

Returns

A bdd whos only path to the true terminal reflects the maximal assignment and (at least) includes the variables in [begin, end).

bdd_satmax() [6/6]

template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>> && !is_convertible<OutputIt, bdd>>>

OutputIt adiar::bdd_satmax	(	const bdd &	f,
		OutputIt	iter
	)

The lexicographically largest x such that f(x) is true.

Parameters

f	BDD of interest.
iter	Single-pass output iterator for where to place the output.

Returns

The output iterator at its final state.

bdd_satmin() [1/6]

bdd adiar::bdd_satmin

(

const bdd &

f

)

The lexicographically smallest cube x such that f(x) is true.

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

Returns

A bdd whos only path to the true terminal reflects the minimal assignment.

bdd_satmin() [2/6]

bdd adiar::bdd_satmin	(	const bdd &	f,
		const bdd &	d
	)

The lexicographically smallest x such that f(x) is true.

Parameters

f	BDD of interest.
d	BDD cube of variables that ought to be included.

Returns

A bdd whos only path to the true terminal reflects the minimal assignment.

Exceptions

domain_error

If bdd_iscube(d) is not satisfied.

bdd_satmin() [3/6]

void adiar::bdd_satmin	(	const bdd &	f,
		const consumer< pair< bdd::label_type, bool > > &	c
	)

The lexicographically smallest x such that f(x) is true.

Parameters

f	BDD of interest.
c	Consumer that is called in ascending order of the bdd's levels with the (var, value) pairs of the assignment.

bdd_satmin() [4/6]

bdd adiar::bdd_satmin	(	const bdd &	f,
		const generator< bdd::label_type > &	d,
		const size_t	d_size = bdd::max_label+1
	)

The lexicographically smallest x such that f(x) is true within the given domain.

Parameters

f	BDD of interest.
d	Generator of domain in ascending order.
d_size	Upper bound on the number of elements generated by d. This value is merely an allocation hint for the sake of optimisation.

Returns

A bdd whos only path to the true terminal reflects the minimal assignment.

bdd_satmin() [5/6]

template<typename ForwardIt , typename = enable_if<is_const<typename ForwardIt::reference>>>

bdd adiar::bdd_satmin	(	const bdd &	f,
		ForwardIt	cbegin,
		ForwardIt	cend
	)

The lexicographically smallest x such that f(x) is true.

Parameters

f	BDD of interest.
cbegin	Single-pass forward iterator of immutable variables in ascending ordering.
cend	Marks the end for begin.

Returns

A bdd whos only path to the true terminal reflects the minimal assignment and (at least) includes the variables in [begin, end).

bdd_satmin() [6/6]

template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>> && !is_convertible<OutputIt, bdd>>>

OutputIt adiar::bdd_satmin	(	const bdd &	f,
		OutputIt	iter
	)

The lexicographically smallest x such that f(x) is true.

Parameters

f	BDD of interest.
iter	Single-pass output iterator for where to place the output.

Returns

The output iterator at its final state.

bdd_support() [1/2]

void adiar::bdd_support	(	const bdd &	f,
		const consumer< bdd::label_type > &	cb
	)

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

Parameters

f	BDD of interest.
cb	Callback function that consumes the variable labels.

bdd_support() [2/2]

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

OutputIt adiar::bdd_support	(	const bdd &	f,
		OutputIt	iter
	)

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

Parameters

f	BDD of interest.
iter	Single-pass output iterator for where to place the output.

Returns

The output iterator at its final state.

bdd_topvar()

bdd::label_type adiar::bdd_topvar

(

const bdd &

f

)

Get the root's variable label.

Exceptions

invalid_argument

If f is a terminal.