A Binary Decision Diagram (BDD) represents a boolean function \( \{ 0,1 \}^n \rightarrow \{ 0,1 \} \) over a finite domain of \( n \) boolean input variables. More...

Classes
class	adiar::__bdd
	A (possibly) unreduced Binary Decision Diagram. More...

class	adiar::bdd
	A reduced Binary Decision Diagram. More...

Basic BDD Constructors
To construct a more complex but well-structured bdd by hand, please use the bdd_builder (see builder) instead.
bdd	adiar::bdd_const (bool value)
	The BDD representing the given constant value. More...

bdd	adiar::bdd_terminal (bool value)
	The BDD representing the given constant value. More...

bdd	adiar::bdd_false ()
	The BDD representing the constant `false`. More...

bdd	adiar::bdd_bot ()
	The bottom of the powerset lattice. More...

bdd	adiar::bdd_true ()
	The BDD representing the constant `true`. More...

bdd	adiar::bdd_top ()
	The top of the powerset lattice. More...

bdd	adiar::bdd_ithvar (bdd::label_type var)
	The BDD representing the i'th variable. More...

bdd	adiar::bdd_nithvar (bdd::label_type var)
	The BDD representing the negation of the i'th variable. More...

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

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

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

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

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

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

bdd	adiar::bdd_cube (const generator< int > &vars)
	The BDD representing the cube of all the given variables. More...

bdd	adiar::bdd_cube (const generator< pair< bdd::label_type, bool >> &vars)
	The BDD representing the cube of all the given variables. More...

template<typename ForwardIt >
bdd	adiar::bdd_cube (ForwardIt begin, ForwardIt end)
	The BDD representing the cube of all the given variables. More...

Basic BDD Manipulation
bdd	adiar::bdd_not (const bdd &f)
	Negation of a BDD. More...

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

__bdd	adiar::bdd_apply (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_and (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_nand (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'nand' operator.

__bdd	adiar::bdd_or (const bdd &f, const bdd &g)
	Logical 'or' operator. More...

__bdd	adiar::bdd_or (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_nor (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'nor' operator.

__bdd	adiar::bdd_xor (const bdd &f, const bdd &g)
	Logical 'xor' operator. More...

__bdd	adiar::bdd_xor (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_xnor (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'xnor' operator.

__bdd	adiar::bdd_imp (const bdd &f, const bdd &g)
	Logical 'implication' operator. More...

__bdd	adiar::bdd_imp (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'implication' operator.

__bdd	adiar::bdd_invimp (const bdd &f, const bdd &g)
	Logical 'inverse implication' operator. More...

__bdd	adiar::bdd_invimp (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'inverse implication' operator.

__bdd	adiar::bdd_equiv (const bdd &f, const bdd &g)
	Logical 'equivalence' operator. More...

__bdd	adiar::bdd_equiv (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'equivalence' operator.

__bdd	adiar::bdd_diff (const bdd &f, const bdd &g)
	Logical 'difference' operator. More...

__bdd	adiar::bdd_diff (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_less (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_ite (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_restrict (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_restrict (const exec_policy &ep, 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. More...

template<typename ForwardIt >
__bdd	adiar::bdd_restrict (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_low (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_high (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_exists (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_exists (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_exists (const exec_policy &ep, 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. More...

template<typename ForwardIt >
__bdd	adiar::bdd_exists (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_forall (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_forall (const exec_policy &ep, 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. More...

__bdd	adiar::bdd_forall (const exec_policy &ep, 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. More...

template<typename ForwardIt >
__bdd	adiar::bdd_forall (const exec_policy &ep, const bdd &f, ForwardIt begin, ForwardIt end)
	Forall quantification of multiple variables.

bdd	adiar::bdd_relprod (const bdd &states, const bdd &relation, const predicate< bdd::label_type > &pred)
	Relational Product of states and a relation. More...

bdd	adiar::bdd_relprod (const exec_policy &ep, const bdd &states, const bdd &relation, const predicate< bdd::label_type > &pred)
	Relational Product of states and a relation.

bdd	adiar::bdd_relnext (const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m)
	Forwards step with the Relational Product, including relabelling. More...

bdd	adiar::bdd_relnext (const exec_policy &ep, const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m)
	Forwards step with the Relational Product, including relabelling.

bdd	adiar::bdd_relnext (const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m, replace_type m_type)
	Forwards step with the Relational Product, including relabelling. More...

bdd	adiar::bdd_relnext (const exec_policy &ep, const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m, replace_type m_type)
	Forwards step with the Relational Product, including relabelling.

bdd	adiar::bdd_relnext (const bdd &states, const bdd &relation, const bdd::label_type varcount)
	Forwards step with the Relational Product for disjoint variable orderings, including relabelling. More...

bdd	adiar::bdd_relnext (const exec_policy &ep, const bdd &states, const bdd &relation, const bdd::label_type varcount)
	Forwards step with the Relational Product for disjoint variable orderings, including relabelling.

bdd	adiar::bdd_relnext (const bdd &states, const bdd &relation)
	Forwards step with the Relational Product for interleaved variable orderings, including relabelling. More...

bdd	adiar::bdd_relnext (const exec_policy &ep, const bdd &states, const bdd &relation)
	Forwards step with the Relational Product for interleaved variable orderings, including relabelling.

bdd	adiar::bdd_relprev (const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m)
	Backwards step with the Relational Product, including relabelling. More...

bdd	adiar::bdd_relprev (const exec_policy &ep, const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m)
	Backwards step with the Relational Product, including relabelling.

bdd	adiar::bdd_relprev (const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m, replace_type m_type)
	Backwards step with the Relational Product, including relabelling. More...

bdd	adiar::bdd_relprev (const exec_policy &ep, const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m, replace_type m_type)
	Backwards step with the Relational Product, including relabelling.

bdd	adiar::bdd_relprev (const bdd &states, const bdd &relation, const bdd::label_type varcount)
	Backwards step with the Relational Product for disjoint variable orderings, including relabelling. More...

bdd	adiar::bdd_relprev (const exec_policy &ep, const bdd &states, const bdd &relation, const bdd::label_type varcount)
	Backwards step with the Relational Product for disjoint variable orderings, including relabelling.

bdd	adiar::bdd_relprev (const bdd &states, const bdd &relation)
	Backwards step with the Relational Product for interleaved variable orderings, including relabelling. More...

bdd	adiar::bdd_relprev (const exec_policy &ep, const bdd &states, const bdd &relation)
	Backwards step with the Relational Product for interleaved variable orderings, including relabelling.

BDD Predicates
bool	adiar::bdd_iscanonical (const bdd &f)
	Check whether a BDD is canonical. More...

bool	adiar::bdd_isconst (const bdd &f)
	Whether a BDD is a constant. More...

bool	adiar::bdd_isterminal (const bdd &f)
	Whether a BDD is a constant (terminal). More...

bool	adiar::bdd_isfalse (const bdd &f)
	Whether a BDD is the constant `false`.

bool	adiar::bdd_istrue (const bdd &f)
	Whether a BDD is the constant `true`.

bool	adiar::bdd_isvar (const bdd &f)
	Whether a BDD is a function dependent on a single variable. More...

bool	adiar::bdd_isithvar (const bdd &f)
	Whether a BDD is the function of a single positive variable. More...

bool	adiar::bdd_isnithvar (const bdd &f)
	Whether a BDD is the function of a single negative variable. More...

bool	adiar::bdd_iscube (const bdd &f)
	Whether a BDD represents a cube. More...

bool	adiar::bdd_equal (const bdd &f, const bdd &g)
	Whether the two BDDs represent the same function.

bool	adiar::bdd_equal (const exec_policy &, const bdd &f, const bdd &g)
	Whether the two BDDs represent the same function.

bool	adiar::operator== (const bdd &f, const bdd &g)

bool	adiar::bdd_unequal (const bdd &f, const bdd &g)
	Whether the two BDDs represent different functions. More...

bool	adiar::bdd_unequal (const exec_policy &ep, const bdd &f, const bdd &g)
	Whether the two BDDs represent different functions.

bool	adiar::operator!= (const bdd &f, const bdd &g)

BDD Counting Operations
size_t	adiar::bdd_nodecount (const bdd &f)
	The number of (internal) nodes used to represent the function.

bdd::label_type	adiar::bdd_varcount (const bdd &f)
	The number of variables that influence the outcome of f, i.e. the number of levels in the BDD.

uint64_t	adiar::bdd_pathcount (const bdd &f)
	Count all unique (but not necessarily disjoint) paths to the true terminal. More...

uint64_t	adiar::bdd_pathcount (const exec_policy &ep, const bdd &f)
	Count all unique (but not necessarily disjoint) paths to the true terminal.

uint64_t	adiar::bdd_satcount (const bdd &f, bdd::label_type varcount)
	Count the number of assignments x that make f(x) true. More...

uint64_t	adiar::bdd_satcount (const exec_policy &ep, const bdd &f, bdd::label_type varcount)
	Count the number of assignments x that make f(x) true.

uint64_t	adiar::bdd_satcount (const bdd &f)
	Count the number of assignments x that make f(x) true. More...

uint64_t	adiar::bdd_satcount (const exec_policy &ep, const bdd &f)
	Count the number of assignments *x that make f(x) true.

Input Variables
bdd	adiar::bdd_replace (const bdd &f, const function< bdd::label_type(bdd::label_type)> &m)
	Replace variables in f according to the mapping in m. More...

bdd	adiar::bdd_replace (const exec_policy &ep, const bdd &f, const function< bdd::label_type(bdd::label_type)> &m)
	Replace variables in f according to the mapping in m.

bdd	adiar::bdd_replace (const bdd &f, const function< bdd::label_type(bdd::label_type)> &m, replace_type m_type)
	Replace variables in f according to the mapping in m. More...

bdd	adiar::bdd_replace (const exec_policy &ep, const bdd &f, const function< bdd::label_type(bdd::label_type)> &m, replace_type m_type)
	Replace variables in f according to the mapping in m.

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

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

bdd::label_type	adiar::bdd_topvar (const bdd &f)
	Get the root's variable label. More...

bdd::label_type	adiar::bdd_minvar (const bdd &f)
	Get the minimal occurring variable in the function's support. More...

bdd::label_type	adiar::bdd_maxvar (const bdd &f)
	Get the maximal occurring variable in the function's support. More...

bdd	adiar::bdd_satmin (const bdd &f)
	The lexicographically smallest cube x such that f(x) is true. More...

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

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

bdd	adiar::bdd_satmin (const bdd &f, const bdd &d)
	The lexicographically smallest x such that f(x) is true. More...

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

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

bdd	adiar::bdd_satmax (const bdd &f)
	The lexicographically largest cube x such that f(x) is true. More...

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

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

bdd	adiar::bdd_satmax (const bdd &f, const bdd &d)
	The lexicographically largest x such that f(x) is true. More...

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

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

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

pair< bdd, double >	adiar::bdd_optmin (const exec_policy &ep, 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. More...

double	adiar::bdd_optmin (const exec_policy &ep, 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. More...

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

template<typename ForwardIt >
bool	adiar::bdd_eval (const bdd &f, ForwardIt begin, ForwardIt end)
	Evaluate a BDD according to an assignment to its variables. More...

Conversion to BDDs
__bdd	adiar::bdd_from (const zdd &A, const generator< bdd::label_type > &dom)
	Obtains the BDD that represents the same function/set as the given ZDD within the given domain. More...

__bdd	adiar::bdd_from (const exec_policy &ep, const zdd &A, const generator< bdd::label_type > &dom)
	Obtains the BDD that represents the same function/set as the given ZDD within the given domain.

template<typename ForwardIt >
__bdd	adiar::bdd_from (const zdd &A, ForwardIt begin, ForwardIt end)
	Obtains the BDD that represents the same function/set as the given ZDD within the given domain. More...

template<typename ForwardIt >
__bdd	adiar::bdd_from (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Obtains the BDD that represents the same function/set as the given ZDD within the given domain.

__bdd	adiar::bdd_from (const zdd &A)
	Obtains the BDD that represents the same function/set as the given ZDD within the global domain. More...

__bdd	adiar::bdd_from (const exec_policy &ep, const zdd &A)
	Obtains the BDD that represents the same function/set as the given ZDD within the global domain.

DOT Files of BDDs
void	adiar::bdd_printdot (const bdd &f, std::ostream &out=std::cout, bool include_id=false)
	Output a DOT drawing of a BDD to the given output stream.

void	adiar::bdd_printdot (const bdd &f, const std::string &file_name, bool include_id=false)
	Output a DOT drawing of a BDD to the file with the given name.

Detailed Description

A Binary Decision Diagram (BDD) represents a boolean function \( \{ 0,1 \}^n \rightarrow \{ 0,1 \} \) over a finite domain of \( n \) boolean input variables.

The bdd class takes care of reference counting and optimal garbage collection of the underlying files. To ensure the most disk-space is available, try to garbage collect the bdd objects as quickly as possible and/or minimise the number of lvalues of said type.

Function Documentation

◆ bdd_and() [1/4]

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

Logical 'and' operator.

Returns: \( f \land g \)

See also: bdd_apply

◆ bdd_and() [2/4]

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() [3/4]

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() [4/4]

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_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_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_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_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_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_false()

bdd adiar::bdd_false ( )

The BDD representing the constant false.

Returns: \( \bot \)

◆ 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.
gen	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_from() [1/3]

__bdd adiar::bdd_from ( const zdd & A )

Obtains the BDD that represents the same function/set as the given ZDD within the global domain.

Parameters

A	Family of a set (within the given global Variable 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: BDD that is true for the exact same assignments to variables in the global domain.

See also: domain_set domain_isset

◆ bdd_from() [2/3]

__bdd adiar::bdd_from	(	const zdd &	A,
		const generator< bdd::label_type > &	dom
	)

Obtains the BDD that represents the same function/set as the given ZDD within the given domain.

Parameters

A	Family of a set (within the given domain)
dom	Generator function of domain variables in ascending order. These values may not exceed `bdd::max_label`.

Returns: BDD that is true for the exact same assignments to variables in the given domain.

◆ bdd_from() [3/3]

template<typename ForwardIt >

__bdd adiar::bdd_from	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Obtains the BDD that represents the same function/set as the given ZDD within the given domain.

Parameters

A	Family of a set (within the given domain)
begin	Single-pass forward iterator that provides the domain's variables in ascending order. These values may not exceed `bdd::max_label`.
end	Marks the end for `begin`.

Returns: BDD that is true for the exact same assignments to variables in the given domain.

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

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_iscanonical()

bool adiar::bdd_iscanonical ( const bdd & f )

Check whether a BDD is canonical.

◆ bdd_isconst()

bool adiar::bdd_isconst ( const bdd & f )

Whether a BDD is a constant.

See also: bdd_isfalse bdd_istrue

◆ bdd_iscube()

bool adiar::bdd_iscube ( const bdd & f )

Whether a BDD represents a cube.

See also: bdd_cube

◆ bdd_isithvar()

bool adiar::bdd_isithvar ( const bdd & f )

Whether a BDD is the function of a single positive variable.

See also: bdd_isvar bdd_ithvar

◆ bdd_isnithvar()

bool adiar::bdd_isnithvar ( const bdd & f )

Whether a BDD is the function of a single negative variable.

See also: bdd_isvar bdd_nithvar

◆ bdd_isterminal()

bool adiar::bdd_isterminal ( const bdd & f )

Whether a BDD is a constant (terminal).

See also: bdd_isfalse bdd_istrue

◆ bdd_isvar()

bool adiar::bdd_isvar ( const bdd & f )

Whether a BDD is a function dependent on a single variable.

See also: bdd_isithvar bdd_isnithvar

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

Exceptions

invalid_argument If f is a terminal.

See also: bdd_restrict

◆ 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_nand()

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

Logical 'nand' operator.

Returns: \( \neg (f \land g) \)

See also: bdd_apply

◆ 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_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 vica versa.

Returns: \( \neg f \)

◆ 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_or() [1/4]

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

Logical 'or' operator.

Returns: \( f \lor g \)

See also: bdd_apply

◆ bdd_or() [2/4]

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() [3/4]

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() [4/4]

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_pathcount()

uint64_t adiar::bdd_pathcount ( const bdd & f )

Count all unique (but not necessarily disjoint) paths to the true terminal.

Returns: The number of unique paths.

◆ bdd_relnext() [1/4]

bdd adiar::bdd_relnext	(	const bdd &	states,
		const bdd &	relation
	)

Forwards step with the Relational Product for interleaved variable orderings, including relabelling.

Parameters

states	A symbolic representation of the current set of states. These are all encoded with even variables.
relation	A relation between current (even) and next (odd) state variables.

◆ bdd_relnext() [2/4]

bdd adiar::bdd_relnext	(	const bdd &	states,
		const bdd &	relation,
		const bdd::label_type	varcount
	)

Forwards step with the Relational Product for disjoint variable orderings, including relabelling.

Parameters

states	A symbolic representation of the current set of states. These are all encoded with the variables `0`, `1`, ... `varcount - 1`.
relation	A relation between current and next state variables. The next state is encoded with variables `varcount`, `varcount+1`, ... `2*varcount - 1`.

◆ bdd_relnext() [3/4]

bdd adiar::bdd_relnext	(	const bdd &	states,
		const bdd &	relation,
		const function< optional< bdd::label_type >(bdd::label_type)> &	m
	)

Forwards step with the Relational Product, including relabelling.

Parameters

states	A symbolic representation of the current set of states.
relation	A relation between current and next states.
m	A (partial) variable relabelling from next to current. Variables for which `m` returns an empty value are existentially quantified, i.e. the previously current state variables.

◆ bdd_relnext() [4/4]

bdd adiar::bdd_relnext	(	const bdd &	states,
		const bdd &	relation,
		const function< optional< bdd::label_type >(bdd::label_type)> &	m,
		replace_type	m_type
	)

Forwards step with the Relational Product, including relabelling.

Parameters

states	A symbolic representation of the current set of states.
relation	A relation between current and next states.
m	A (partial) variable relabelling from next to current. Variables for which `m` returns an empty value are existentially quantified, i.e. the previously current state variables.
m_type	Guarantees on the class of variable relabelling, e.g. whether it is monotonic.

◆ bdd_relprev() [1/4]

bdd adiar::bdd_relprev	(	const bdd &	states,
		const bdd &	relation
	)

Backwards step with the Relational Product for interleaved variable orderings, including relabelling.

Parameters

states	A symbolic representation of the current set of states. These are all encoded with even variables.
relation	A relation between current (even) and next (odd) state variables.

◆ bdd_relprev() [2/4]

bdd adiar::bdd_relprev	(	const bdd &	states,
		const bdd &	relation,
		const bdd::label_type	varcount
	)

Backwards step with the Relational Product for disjoint variable orderings, including relabelling.

Parameters

states	A symbolic representation of the current set of states. These are all encoded with the variables `0`, `1`, ... `varcount - 1`.
relation	A relation between current and next state variables. The next state is encoded with variables `varcount`, `varcount+1`, ... `2*varcount - 1`.

◆ bdd_relprev() [3/4]

bdd adiar::bdd_relprev	(	const bdd &	states,
		const bdd &	relation,
		const function< optional< bdd::label_type >(bdd::label_type)> &	m
	)

Backwards step with the Relational Product, including relabelling.

Parameters

states	A symbolic representation of the current set of states.
relation	A relation between current and next states.
m	A (partial) variable relabelling from current to next. Variables for which `m` returns an empty value are existentially quantified, i.e. the next state variables (the previously current state variables).

◆ bdd_relprev() [4/4]

bdd adiar::bdd_relprev	(	const bdd &	states,
		const bdd &	relation,
		const function< optional< bdd::label_type >(bdd::label_type)> &	m,
		replace_type	m_type
	)

Backwards step with the Relational Product, including relabelling.

Parameters

states	A symbolic representation of the current set of states.
relation	A relation between current and next states.
m	A (partial) variable relabelling from current to next. Variables for which `m` returns an empty value are existentially quantified, i.e. the next state variables (the previously current state variables).
m_type	Guarantees on the class of variable relabelling, e.g. whether it is monotonic.

◆ bdd_relprod()

bdd adiar::bdd_relprod	(	const bdd &	states,
		const bdd &	relation,
		const predicate< bdd::label_type > &	pred
	)

Relational Product of states and a relation.

Parameters

states	A symbolic representation of the current (or next) set of states.
relation	A relation between current and next states.
m	Predicate whether a variable should be existentially quantified.

◆ bdd_replace() [1/2]

bdd adiar::bdd_replace	(	const bdd &	f,
		const function< bdd::label_type(bdd::label_type)> &	m
	)

Replace variables in f according to the mapping in m.

Parameters

f	BDD to replace variables within
m	Function from BDD label to another (or itself).

Exceptions

invalid_argument if m is not a monotonic relabelling.

◆ bdd_replace() [2/2]

bdd adiar::bdd_replace	(	const bdd &	f,
		const function< bdd::label_type(bdd::label_type)> &	m,
		replace_type	m_type
	)

Replace variables in f according to the mapping in m.

Parameters

f	BDD to replace variables within
m	Function from BDD label to another (or itself).
m_type	Guarantees on the class of variable relabelling, e.g. whether it is monotonic.

Exceptions

invalid_argument if m_type classifies m as not monotonic.

◆ 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 restructed 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_satcount() [1/2]

uint64_t adiar::bdd_satcount ( const bdd & f )

Count the number of assignments x that make f(x) true.

Same as bdd_satcount(f, varcount), with varcount set to be the size of the global domain or the number of variables within the given BDD.

See also: domain_set bdd_varcount

◆ bdd_satcount() [2/2]

uint64_t adiar::bdd_satcount	(	const bdd &	f,
		bdd::label_type	varcount
	)

Count the number of assignments x that make f(x) true.

Parameters

f	BDD to count within.
varcount	The number of variables in the domain of the function. This number should be larger than or equal to the number of levels in the BDD (

See also: bdd_varcount())

Returns: The number of unique assignments.

Exceptions

invalid_argument If varcount is not larger than the number of levels in the BDD.

◆ bdd_satmax() [1/6]

bdd adiar::bdd_satmax ( const bdd & f )

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

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

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

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.
begin	Single-pass forward iterator of immutable variables in ascending ordering.
end	Marks the end for `begin`.

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

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

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 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.
begin	Single-pass forward iterator of immutable variables in ascending ordering.
end	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.
begin	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_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_topvar()

bdd::label_type adiar::bdd_topvar ( const bdd & f )

Get the root's variable label.

Exceptions

invalid_argument If f is a terminal.

◆ bdd_true()

bdd adiar::bdd_true ( )

The BDD representing the constant true.

Returns: \( \top \)

◆ bdd_unequal()

bool adiar::bdd_unequal	(	const bdd &	f,
		const bdd &	g
	)

Whether the two BDDs represent different functions.

See also: bdd_equal

◆ 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!=()

bool adiar::operator!=	(	const bdd &	f,
		const bdd &	g
	)

See also: bdd_equal bdd_unequal

◆ 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 )

See also: bdd_diff, bdd_not

◆ operator-() [2/2]

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

See also: bdd_diff

◆ operator==()

bool adiar::operator==	(	const bdd &	f,
		const bdd &	g
	)

See also: bdd_equal

◆ 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

Classes

Basic BDD Constructors

Basic BDD Manipulation

BDD Predicates

BDD Counting Operations

Input Variables

Conversion to BDDs

DOT Files of BDDs

Detailed Description

Function Documentation

◆ bdd_and() [1/4]

◆ bdd_and() [2/4]

◆ bdd_and() [3/4]

◆ bdd_and() [4/4]

◆ bdd_apply()

◆ bdd_bot()

◆ bdd_const()

◆ bdd_cube() [1/3]

◆ bdd_cube() [2/3]

◆ bdd_cube() [3/3]

◆ bdd_diff()

◆ bdd_equiv()

◆ bdd_eval() [1/3]

◆ bdd_eval() [2/3]

◆ bdd_eval() [3/3]

◆ bdd_exists() [1/4]

◆ bdd_exists() [2/4]

◆ bdd_exists() [3/4]

◆ bdd_exists() [4/4]

◆ bdd_false()

◆ bdd_forall() [1/4]

◆ bdd_forall() [2/4]

◆ bdd_forall() [3/4]

◆ bdd_forall() [4/4]

◆ bdd_from() [1/3]

◆ bdd_from() [2/3]

◆ bdd_from() [3/3]

◆ bdd_high()

◆ bdd_imp()

◆ bdd_invimp()

◆ bdd_iscanonical()

◆ bdd_isconst()

◆ bdd_iscube()

◆ bdd_isithvar()

◆ bdd_isnithvar()

◆ bdd_isterminal()

◆ bdd_isvar()

◆ bdd_ite()

◆ bdd_ithvar()

◆ bdd_less()

◆ bdd_low()

◆ bdd_maxvar()

◆ bdd_minvar()

◆ bdd_nand()

◆ bdd_nithvar()

◆ bdd_nor()

◆ bdd_not()

◆ bdd_optmin() [1/2]

◆ bdd_optmin() [2/2]

◆ bdd_or() [1/4]

◆ bdd_or() [2/4]

◆ bdd_or() [3/4]

◆ bdd_or() [4/4]

◆ bdd_pathcount()

◆ bdd_relnext() [1/4]

◆ bdd_relnext() [2/4]

◆ bdd_relnext() [3/4]

◆ bdd_relnext() [4/4]

◆ bdd_relprev() [1/4]

◆ bdd_relprev() [2/4]

◆ bdd_relprev() [3/4]

◆ bdd_relprev() [4/4]

◆ bdd_relprod()

◆ bdd_replace() [1/2]

◆ bdd_replace() [2/2]

◆ bdd_restrict() [1/3]

◆ bdd_restrict() [2/3]

◆ bdd_restrict() [3/3]

◆ bdd_satcount() [1/2]

◆ bdd_satcount() [2/2]