Basic Operations

Basic Boolean operations. More...

Functions
bdd	adiar::bdd_not (const bdd &f)
	Negation of a BDD.
bdd	adiar::operator~ (const bdd &f)
__bdd	adiar::bdd_apply (const bdd &f, const bdd &g, const predicate< bool, bool > &op)
	Apply a binary operator between two BDDs.
__bdd	adiar::bdd_and (const bdd &f, const bdd &g)
	Logical 'and' operator.
__bdd	adiar::operator& (const bdd &lhs, const bdd &rhs)
__bdd	adiar::operator* (const bdd &lhs, const bdd &rhs)
__bdd	adiar::bdd_nand (const bdd &f, const bdd &g)
	Logical 'nand' operator.
__bdd	adiar::bdd_or (const bdd &f, const bdd &g)
	Logical 'or' operator.
__bdd	adiar::operator| (const bdd &lhs, const bdd &rhs)
bdd	adiar::operator+ (const bdd &f)
__bdd	adiar::operator+ (const bdd &lhs, const bdd &rhs)
__bdd	adiar::bdd_nor (const bdd &f, const bdd &g)
	Logical 'nor' operator.
__bdd	adiar::bdd_xor (const bdd &f, const bdd &g)
	Logical 'xor' operator.
__bdd	adiar::operator^ (const bdd &lhs, const bdd &rhs)
__bdd	adiar::bdd_xnor (const bdd &f, const bdd &g)
	Logical 'xnor' operator.
__bdd	adiar::bdd_imp (const bdd &f, const bdd &g)
	Logical 'implication' operator.
__bdd	adiar::bdd_invimp (const bdd &f, const bdd &g)
	Logical 'inverse implication' operator.
__bdd	adiar::bdd_equiv (const bdd &f, const bdd &g)
	Logical 'equivalence' operator.
__bdd	adiar::bdd_diff (const bdd &f, const bdd &g)
	Logical 'difference' operator.
bdd	adiar::operator- (const bdd &f)
__bdd	adiar::operator- (const bdd &lhs, const bdd &rhs)
__bdd	adiar::bdd_less (const bdd &f, const bdd &g)
	Logical 'less than' operator.
__bdd	adiar::bdd_ite (const bdd &f, const bdd &g, const bdd &h)
	If-Then-Else operator.
__bdd	adiar::bdd_restrict (const bdd &f, bdd::label_type var, bool val)
	Restrict a single variable to a constant value.
__bdd	adiar::bdd_restrict (const bdd &f, const generator< pair< bdd::label_type, bool > > &xs)
	Restrict a subset of variables to constant values.
template<typename ForwardIt >
__bdd	adiar::bdd_restrict (const bdd &f, ForwardIt begin, ForwardIt end)
	Restrict a subset of variables to constant values.
__bdd	adiar::bdd_low (const bdd &f)
	Restrict the root to false, i.e. follow its low edge.
__bdd	adiar::bdd_high (const bdd &f)
	Restrict the root to true, i.e. follow its high edge.
__bdd	adiar::bdd_exists (const bdd &f, bdd::label_type var)
	Existential quantification of a single variable.
__bdd	adiar::bdd_exists (const bdd &f, const predicate< bdd::label_type > &vars)
	Existential quantification of multiple variables.
__bdd	adiar::bdd_exists (const bdd &f, const generator< bdd::label_type > &vars)
	Existential quantification of multiple variables.
template<typename ForwardIt >
__bdd	adiar::bdd_exists (const bdd &f, ForwardIt begin, ForwardIt end)
	Existential quantification of multiple variables.
__bdd	adiar::bdd_forall (const bdd &f, bdd::label_type var)
	Forall quantification of a single variable.
__bdd	adiar::bdd_forall (const bdd &f, const predicate< bdd::label_type > &vars)
	Forall quantification of multiple variables.
__bdd	adiar::bdd_forall (const bdd &f, const generator< bdd::label_type > &vars)
	Forall quantification of multiple variables.
template<typename ForwardIt >
__bdd	adiar::bdd_forall (const bdd &f, ForwardIt begin, ForwardIt end)
	Forall quantification of multiple variables.

Detailed Description

Basic Boolean operations.

Function Documentation

bdd_and()

__bdd adiar::bdd_and	(	const bdd &	f,
		const bdd &	g
	)

Logical 'and' operator.

Returns

\( f \land g \)

See also

bdd_apply

bdd_apply()

__bdd adiar::bdd_apply	(	const bdd &	f,
		const bdd &	g,
		const predicate< bool, bool > &	op
	)

Apply a binary operator between two BDDs.

Parameters

f	BDD for the left-hand-side of the operator
g	BDD for the right-hand-side of the operator
op	Binary predicate on bool to-be applied.

Returns

\( f \mathbin{\mathit{op}} g\)

See also

bool_op

bdd_diff()

__bdd adiar::bdd_diff	(	const bdd &	f,
		const bdd &	g
	)

Logical 'difference' operator.

Returns

\( f \setminus g \)

See also

bdd_apply

bdd_equiv()

__bdd adiar::bdd_equiv	(	const bdd &	f,
		const bdd &	g
	)

Logical 'equivalence' operator.

Returns

\( f = g \)

See also

bdd_apply

bdd_exists() [1/4]

__bdd adiar::bdd_exists	(	const bdd &	f,
		bdd::label_type	var
	)

Existential quantification of a single variable.

Computes the BDD for \( \exists x_{i} : f \) faster than computing \( f|_{x_i = \bot} \lor f|_{x_i = \top} \) using bdd_apply and bdd_restrict.

Parameters

f	BDD to be quantified
var	Variable to quantify in f

Returns

\( \exists x_{var} : f \)

bdd_exists() [2/4]

__bdd adiar::bdd_exists	(	const bdd &	f,
		const generator< bdd::label_type > &	vars
	)

Existential quantification of multiple variables.

Parameters

f	BDD to be quantified.
vars	Generator function, that produces variables to be quantified in descending order. These values have to be smaller than or equals to bdd::max_label.

Returns

\( \exists x_i \in \texttt{gen()} : f \)

bdd_exists() [3/4]

__bdd adiar::bdd_exists	(	const bdd &	f,
		const predicate< bdd::label_type > &	vars
	)

Existential quantification of multiple variables.

Parameters

f	BDD to be quantified.
vars	Predicate to identify the variables to quantify in f. You may abuse the fact, that this predicate will only be invoked in ascending/descending order of the levels in f (but, with retraversals).

Returns

\( \exists x_i \in \texttt{vars} : f \)

bdd_exists() [4/4]

template<typename ForwardIt >

__bdd adiar::bdd_exists	(	const bdd &	f,
		ForwardIt	begin,
		ForwardIt	end
	)

Existential quantification of multiple variables.

Parameters

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

Returns

\( \exists x_i \in \texttt{begin} ... \texttt{end} : f \)

bdd_forall() [1/4]

__bdd adiar::bdd_forall	(	const bdd &	f,
		bdd::label_type	var
	)

Forall quantification of a single variable.

Computes the BDD for \( \forall x_{i} : f \) faster than computing \( f|_{x_i = \bot} \land f|_{x_i = \top} \) using bdd_apply and bdd_restrict.

Parameters

f	BDD to be quantified.
var	Variable to quantify in f

Returns

\( \forall x_{var} : f \)

bdd_forall() [2/4]

__bdd adiar::bdd_forall	(	const bdd &	f,
		const generator< bdd::label_type > &	vars
	)

Forall quantification of multiple variables.

Parameters

f	BDD to be quantified.
vars	Generator function, that produces variables to be quantified in descending order. These values have to be smaller than or equals to bdd::max_label.

Returns

\( \forall x_i \in \texttt{gen()} : f \)

bdd_forall() [3/4]

__bdd adiar::bdd_forall	(	const bdd &	f,
		const predicate< bdd::label_type > &	vars
	)

Forall quantification of multiple variables.

Parameters

f	BDD to be quantified.
vars	Predicate to identify the variables to quantify in f. You may abuse the fact, that this predicate will only be invoked in ascending/descending order of the levels in f (but, with retraversals).

Returns

\( \forall x_i \in \texttt{vars} : f \)

bdd_forall() [4/4]

template<typename ForwardIt >

__bdd adiar::bdd_forall	(	const bdd &	f,
		ForwardIt	begin,
		ForwardIt	end
	)

Forall quantification of multiple variables.

Parameters

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

Returns

\( \forall x_i \in \texttt{begin} ... \texttt{end} : f \)

bdd_high()

__bdd adiar::bdd_high

(

const bdd &

f

)

Restrict the root to true, i.e. follow its high edge.

Remarks

In other BDD packages, this function is good for traversing a BDD. But, here this is not a constant-time operation but constructs an entire new BDD of up-to linear size (requires a full traversal).

Exceptions

invalid_argument

If f is a terminal.

See also

bdd_restrict

bdd_imp()

__bdd adiar::bdd_imp	(	const bdd &	f,
		const bdd &	g
	)

Logical 'implication' operator.

Returns

\( f \rightarrow g \)

See also

bdd_apply

bdd_invimp()

__bdd adiar::bdd_invimp	(	const bdd &	f,
		const bdd &	g
	)

Logical 'inverse implication' operator.

Returns

\( f \leftarrow g \)

See also

bdd_apply

bdd_ite()

__bdd adiar::bdd_ite	(	const bdd &	f,
		const bdd &	g,
		const bdd &	h
	)

If-Then-Else operator.

Computes the BDD expressing \( f ? g : h \) more efficient than computing \( (f \land g) \lor (\neg f \land h) \) with bdd_apply.

Parameters

f	BDD for the if conditional
g	BDD for the then case
h	BDD for the else case

Returns

\( f ? g : h \)

Remarks

In other BDD packages, this function is good for manually constructing a BDD bottom-up. But, here you should use the bdd_builder class (see builder) instead

See also

bdd_apply builder bdd_builder

bdd_less()

__bdd adiar::bdd_less	(	const bdd &	f,
		const bdd &	g
	)

Logical 'less than' operator.

Returns

\( f < g \)

See also

bdd_apply

bdd_low()

__bdd adiar::bdd_low

(

const bdd &

f

)

Restrict the root to false, i.e. follow its low edge.

Remarks

In other BDD packages, this function is good for traversing a BDD. But, here this is not a constant-time operation but constructs an entire new BDD of up-to linear size (requires a full traversal).

Exceptions

invalid_argument

If f is a terminal.

See also

bdd_restrict

bdd_nand()

__bdd adiar::bdd_nand	(	const bdd &	f,
		const bdd &	g
	)

Logical 'nand' operator.

Returns

\( \neg (f \land g) \)

See also

bdd_apply

bdd_nor()

__bdd adiar::bdd_nor	(	const bdd &	f,
		const bdd &	g
	)

Logical 'nor' operator.

Returns

\( \neg (f \lor g) \)

See also

bdd_apply

bdd_not()

bdd adiar::bdd_not

(

const bdd &

f

)

Negation of a BDD.

Flips the negation flag such that reading nodes with a node_stream within Adiar's algorithms will on-the-fly change the false terminals into the true terminals and vice versa.

Returns

\( \neg f \)

bdd_or()

__bdd adiar::bdd_or	(	const bdd &	f,
		const bdd &	g
	)

Logical 'or' operator.

Returns

\( f \lor g \)

See also

bdd_apply

bdd_restrict() [1/3]

__bdd adiar::bdd_restrict	(	const bdd &	f,
		bdd::label_type	var,
		bool	val
	)

Restrict a single variable to a constant value.

The variable i is restricted to the value v.

Parameters

f	BDD to restrict.
var	Variable to assign
val	Value assigned

Returns

\( f|_{x_i = v} \)

bdd_restrict() [2/3]

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

Restrict a subset of variables to constant values.

For each tuple (i,v) in the assignment xs, the variable with label i is set to the constant value v. This binds the scope of the variables in xs, i.e. any later mention of a variable i is not the same as variable i in xs.

Parameters

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

Returns

\( f|_{(i,v) \in xs : x_i = v} \)

bdd_restrict() [3/3]

template<typename ForwardIt >

__bdd adiar::bdd_restrict	(	const bdd &	f,
		ForwardIt	begin,
		ForwardIt	end
	)

Restrict a subset of variables to constant values.

For each tuple (i,v) provided by the iterator, the variable with label i is set to the constant value v.

Parameters

f	BDD to restrict
begin	Single-pass forward iterator that provides the to-be restricted variables in ascending order. All variables should be smaller than or equals to bdd::max_label.
end	Marks the end for begin.

Returns

\( f|_{(i,v) \in xs : x_i = v} \)

bdd_xnor()

__bdd adiar::bdd_xnor	(	const bdd &	f,
		const bdd &	g
	)

Logical 'xnor' operator.

Returns

\( \neg (f \oplus g) \)

See also

bdd_apply

bdd_xor()

__bdd adiar::bdd_xor	(	const bdd &	f,
		const bdd &	g
	)

Logical 'xor' operator.

Returns

\( f \oplus g \)

See also

bdd_apply

operator&()

__bdd adiar::operator&	(	const bdd &	lhs,
		const bdd &	rhs
	)

See also

bdd_and

operator*()

__bdd adiar::operator*	(	const bdd &	lhs,
		const bdd &	rhs
	)

See also

bdd_and

operator+() [1/2]

bdd adiar::operator+

(

const bdd &

f

)

See also

bdd_or

operator+() [2/2]

__bdd adiar::operator+	(	const bdd &	lhs,
		const bdd &	rhs
	)

See also

bdd_or ///////////////////////////////////////////////////////////////////////////////////////////////

bdd_or

operator-() [1/2]

bdd adiar::operator-

(

const bdd &

f

)

Remarks

Unary difference subtracts from \( \top \) value, making its equivalent to negation.

See also

bdd_diff, bdd_not

operator-() [2/2]

__bdd adiar::operator-	(	const bdd &	lhs,
		const bdd &	rhs
	)

See also

bdd_diff

operator^()

__bdd adiar::operator^	(	const bdd &	lhs,
		const bdd &	rhs
	)

See also

bdd_xor

operator|()

__bdd adiar::operator|	(	const bdd &	lhs,
		const bdd &	rhs
	)

See also

bdd_or

operator~()

bdd adiar::operator~

(

const bdd &

f

)

See also

bdd_not