Basic Constructors

Construction of constants, variables, and cubes. More...

Functions
bdd	adiar::bdd_const (bool value)
	The BDD representing the given constant value.
bdd	adiar::bdd_terminal (bool value)
	The BDD representing the given constant value.
bdd	adiar::bdd_false ()
	The BDD representing the constant false.
bdd	adiar::bdd_bot ()
	The bottom of the powerset lattice.
bdd	adiar::bdd_true ()
	The BDD representing the constant true.
bdd	adiar::bdd_top ()
	The top of the powerset lattice.
bdd	adiar::bdd_ithvar (bdd::label_type var)
	The BDD representing the i'th variable.
bdd	adiar::bdd_nithvar (bdd::label_type var)
	The BDD representing the negation of the i'th variable.
bdd	adiar::bdd_and (const generator< int > &vars)
	The BDD representing the logical 'and' of all the given variables, i.e. a term of variables.
bdd	adiar::bdd_and (const generator< pair< bdd::label_type, bool > > &vars)
	The BDD representing the logical 'and' of all the given variables, i.e. a term of variables.
template<typename ForwardIt , typename = enable_if<!is_convertible<ForwardIt, bdd>>>
bdd	adiar::bdd_and (ForwardIt begin, ForwardIt end)
	The BDD representing the logical 'and' of all the given variables, i.e. a term of variables.
bdd	adiar::bdd_or (const generator< int > &vars)
	The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables.
bdd	adiar::bdd_or (const generator< pair< bdd::label_type, bool > > &vars)
	The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables.
template<typename ForwardIt , typename = enable_if<!is_convertible<ForwardIt, bdd>>>
bdd	adiar::bdd_or (ForwardIt begin, ForwardIt end)
	The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables.
bdd	adiar::bdd_cube (const generator< int > &vars)
	The BDD representing the cube of all the given variables.
bdd	adiar::bdd_cube (const generator< pair< bdd::label_type, bool > > &vars)
	The BDD representing the cube of all the given variables.
template<typename ForwardIt >
bdd	adiar::bdd_cube (ForwardIt begin, ForwardIt end)
	The BDD representing the cube of all the given variables.

Detailed Description

Construction of constants, variables, and cubes.

Remarks

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

Function Documentation

bdd_and() [1/3]

bdd adiar::bdd_and

(

const generator< int > &

vars

)

The BDD representing the logical 'and' of all the given variables, i.e. a term of variables.

Any negative labels provided by the generator are interpreted as the negation of said variable.

Parameters

vars	Generator of labels of variables in descending order. These values can at most be bdd::max_label.

Returns

\( \bigwedge_{x \in \mathit{vars}} x \)

Exceptions

invalid_argument

If vars are not in descending order.

bdd_and() [2/3]

bdd adiar::bdd_and

(

const generator< pair< bdd::label_type, bool > > &

vars

)

The BDD representing the logical 'and' of all the given variables, i.e. a term of variables.

Parameters

vars	Generator of pairs (label, negated) in descending order. These values can at most be bdd::max_label.

Returns

\( \bigwedge_{x \in \mathit{vars}} x \)

Exceptions

invalid_argument

If vars are not in descending order.

bdd_and() [3/3]

template<typename ForwardIt , typename = enable_if<!is_convertible<ForwardIt, bdd>>>

bdd adiar::bdd_and	(	ForwardIt	begin,
		ForwardIt	end
	)

The BDD representing the logical 'and' of all the given variables, i.e. a term of variables.

Any negative labels provided by the generator are interpreted as the negation of said variable.

Parameters

begin	Single-pass forward iterator that provides the variables in descending order. All its values should be smaller than or equals to bdd::max_label.
end	Marks the end for begin.

Returns

\( \bigwedge_{x \in \mathit{begin} \dots \mathit{end}} x \)

Exceptions

invalid_argument

If the iterator does not provide values in descending order.

bdd_bot()

bdd adiar::bdd_bot ( )

inline

The bottom of the powerset lattice.

Returns

\( \bot \)

See also

bdd_false

bdd_const()

bdd adiar::bdd_const

(

bool

value

)

The BDD representing the given constant value.

Parameters

value

The constant boolean value

See also

bdd_false bdd_true

bdd_cube() [1/3]

bdd adiar::bdd_cube

(

const generator< int > &

vars

)

The BDD representing the cube of all the given variables.

Any negative labels provided by the generator are interpreted as the negation of said variable.

Parameters

vars	Generator of labels of variables in descending order. These values can at most be bdd::max_label.

Returns

\( \bigwedge_{x \in \mathit{vars}} x \)

Exceptions

invalid_argument

If vars are not in descending order.

See also

bdd_and

bdd_cube() [2/3]

bdd adiar::bdd_cube

(

const generator< pair< bdd::label_type, bool > > &

vars

)

The BDD representing the cube of all the given variables.

Parameters

vars	Generator of pairs (label, negated) in descending order. These values can at most be bdd::max_label.

Returns

\( \bigwedge_{x \in \mathit{vars}} x \)

Exceptions

invalid_argument

If vars are not in descending order.

See also

bdd_and

bdd_cube() [3/3]

template<typename ForwardIt >

bdd adiar::bdd_cube	(	ForwardIt	begin,
		ForwardIt	end
	)

The BDD representing the cube of all the given variables.

Any negative labels provided by the generator are interpreted as the negation of said variable.

Parameters

begin	Single-pass forward iterator that provides the variables in descending order. All its values should be smaller than or equals to bdd::max_label.
end	Marks the end for begin.

Returns

\( \bigwedge_{x \in \mathit{begin} \dots \mathit{end}} x \)

Exceptions

invalid_argument

If the iterator does not provide values in descending order.

See also

bdd_and

bdd_false()

bdd adiar::bdd_false

(

)

The BDD representing the constant false.

Returns

\( \bot \)

See also

bdd_bot

bdd_ithvar()

bdd adiar::bdd_ithvar

(

bdd::label_type

var

)

The BDD representing the i'th variable.

Parameters

var	The label of the desired variable. This value must be smaller or equals to bdd::max_label.

Returns

\( x_{var} \)

Exceptions

invalid_argument

If var is a too large value.

bdd_nithvar()

bdd adiar::bdd_nithvar

(

bdd::label_type

var

)

The BDD representing the negation of the i'th variable.

Parameters

var	The label of the desired variable. This value must be smaller or equals to / bdd::max_label.

Returns

\( \neg x_{var} \)

Exceptions

invalid_argument

If var is a too large value.

bdd_or() [1/3]

bdd adiar::bdd_or

(

const generator< int > &

vars

)

The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables.

Any negative labels provided by the generator are interpreted as the negation of said variable.

Parameters

vars	Generator of labels of variables in descending order. When These values can at most be bdd::max_label.

Returns

\( \bigvee_{x \in \mathit{vars}} x \)

Exceptions

invalid_argument

If vars are not in descending order.

bdd_or() [2/3]

bdd adiar::bdd_or

(

const generator< pair< bdd::label_type, bool > > &

vars

)

The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables.

Parameters

vars	Generator of pairs (label, negated) in descending order. These values can at most be bdd::max_label.

Returns

\( \bigvee_{x \in \mathit{vars}} x \)

Exceptions

invalid_argument

If vars are not in descending order.

bdd_or() [3/3]

template<typename ForwardIt , typename = enable_if<!is_convertible<ForwardIt, bdd>>>

bdd adiar::bdd_or	(	ForwardIt	begin,
		ForwardIt	end
	)

The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables.

Any negative labels provided by the generator are interpreted as the negation of said variable.

Parameters

begin	Single-pass forward iterator that provides the variables in descending order. All its values should be smaller than or equals to bdd::max_label.
end	Marks the end for begin.

Returns

\( \bigwedge_{x \in \mathit{begin} \dots \mathit{end}} x \)

Exceptions

invalid_argument

If the iterator does not provide values in descending order.

bdd_terminal()

bdd adiar::bdd_terminal

(

bool

value

)

The BDD representing the given constant value.

Parameters

value

The constant boolean (terminal) value

See also

bdd_const bdd_false bdd_true

bdd_top()

bdd adiar::bdd_top ( )

inline

The top of the powerset lattice.

Returns

\( \top \)

See also

bdd_true

bdd_true()

bdd adiar::bdd_true

(

)

The BDD representing the constant true.

Returns

\( \top \)