Binary Decision Diagrams

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 Constructors
To construct a more complex but well-structured zdd by hand, please use the zdd_builder (see builder) instead.
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.
zdd	adiar::zdd_terminal (bool value)
	The ZDD of only a single terminal.
zdd	adiar::zdd_empty ()
	The empty family, i.e. Ø .
zdd	adiar::zdd_null ()
	The family only with the empty set, i.e. { Ø } .
zdd	adiar::zdd_ithvar (zdd::label_type var, const generator< zdd::label_type > &dom)
	The set of bitvectors over a given domain where var is set to true.
template<typename ForwardIt >
zdd	adiar::zdd_ithvar (zdd::label_type var, ForwardIt begin, ForwardIt end)
	The set of bitvectors over a given domain where var is set to true.
zdd	adiar::zdd_ithvar (zdd::label_type var)
	The set of bitvectors over the globally set domain where var is set to true.
zdd	adiar::zdd_nithvar (zdd::label_type var, const generator< zdd::label_type > &dom)
	The set of bitvectors over a given domain where var is set to false.
template<typename ForwardIt >
zdd	adiar::zdd_nithvar (zdd::label_type var, ForwardIt begin, ForwardIt end)
	The set of bitvectors over a given domain where var is set to false.
zdd	adiar::zdd_nithvar (zdd::label_type var)
	The set of bitvectors over the globally set domain where var is set to false.
zdd	adiar::zdd_vars (const generator< zdd::label_type > &vars)
	The family { { 1, 2, ..., k } }.
template<typename ForwardIt >
zdd	adiar::zdd_vars (ForwardIt begin, ForwardIt end)
	The family { { 1, 2, ..., k } }.
zdd	adiar::zdd_point (const generator< zdd::label_type > &vars)
	The family { { 1, 2, ..., k } } with a single bit-vector.
template<typename ForwardIt >
zdd	adiar::zdd_point (ForwardIt begin, ForwardIt end)
	The family { { 1, 2, ..., k } } with a single bit-vector.
zdd	adiar::zdd_singleton (zdd::label_type var)
	The family { {i} } .
zdd	adiar::zdd_singletons (const generator< zdd::label_type > &vars)
	The family { {1}, {2}, ..., {k} }.
template<typename ForwardIt >
zdd	adiar::zdd_singletons (ForwardIt begin, ForwardIt end)
	The family { {1}, {2}, ..., {k} }.
zdd	adiar::zdd_powerset (const generator< zdd::label_type > &vars)
	The powerset of all given variables.
template<typename ForwardIt >
zdd	adiar::zdd_powerset (ForwardIt begin, ForwardIt end)
	The powerset of all given variables.
zdd	adiar::zdd_bot (const generator< zdd::label_type > &dom)
	Bottom of the powerset lattice.
template<typename ForwardIt >
zdd	adiar::zdd_bot (ForwardIt begin, ForwardIt end)
	Bottom of the powerset lattice.
zdd	adiar::zdd_bot ()
	Bottom of the powerset lattice.
zdd	adiar::zdd_top (const generator< zdd::label_type > &dom)
	Top of the powerset lattice.
template<typename ForwardIt >
zdd	adiar::zdd_top (ForwardIt begin, ForwardIt end)
	Top of the powerset lattice.
zdd	adiar::zdd_top ()
	Top of the powerset lattice.

Basic Operations
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_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.
__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.
__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.
__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.
__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.
__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.
__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.
__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.
__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.
__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.
__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.
__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.
__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.
__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.
__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.
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.
__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.
__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.
__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.
__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.
__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.
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.
__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.
__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.
__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.
template<typename ForwardIt >
__bdd	adiar::bdd_forall (const exec_policy &ep, const bdd &f, ForwardIt begin, ForwardIt end)
	Forall quantification of multiple variables.
__zdd	adiar::zdd_binop (const zdd &A, const zdd &B, const predicate< bool, bool > &op)
	Apply a binary operator between the sets of two families.
__zdd	adiar::zdd_binop (const exec_policy &ep, const zdd &A, const zdd &B, const predicate< bool, bool > &op)
	Apply a binary operator between the sets of two families.
__zdd	adiar::zdd_union (const zdd &A, const zdd &B)
	The union of two families of sets.
__zdd	adiar::zdd_union (const exec_policy &ep, const zdd &A, const zdd &B)
	The union of two families of sets.
__zdd	adiar::operator| (const zdd &lhs, const zdd &rhs)
zdd	adiar::operator+ (const zdd &A)
__zdd	adiar::operator+ (const zdd &lhs, const zdd &rhs)
__zdd	adiar::zdd_intsec (const zdd &A, const zdd &B)
	The intersection of two families of sets.
__zdd	adiar::zdd_intsec (const exec_policy &ep, const zdd &A, const zdd &B)
	The intersection of two families of sets.
__zdd	adiar::operator& (const zdd &lhs, const zdd &rhs)
__zdd	adiar::operator* (const zdd &lhs, const zdd &rhs)
__zdd	adiar::zdd_diff (const zdd &A, const zdd &B)
	The set difference of two families of sets.
__zdd	adiar::zdd_diff (const exec_policy &ep, const zdd &A, const zdd &B)
	The set difference of two families of sets.
__zdd	adiar::operator- (const zdd &A)
__zdd	adiar::operator- (const zdd &lhs, const zdd &rhs)
__zdd	adiar::zdd_change (const zdd &A, const generator< zdd::label_type > &vars)
	The symmetric difference between each set in the family and the given set of variables.
__zdd	adiar::zdd_change (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &vars)
	The symmetric difference between each set in the family and the given set of variables.
template<typename ForwardIt >
__zdd	adiar::zdd_change (const zdd &A, ForwardIt begin, ForwardIt end)
	The symmetric difference between each set in the family and the given set of variables.
template<typename ForwardIt >
__zdd	adiar::zdd_change (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	The symmetric difference between each set in the family and the given set of variables.
__zdd	adiar::zdd_complement (const zdd &A, const generator< zdd::label_type > &dom)
	Complement of A within the given domain.
__zdd	adiar::zdd_complement (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &dom)
	Complement of A within the given domain.
template<typename ForwardIt >
__zdd	adiar::zdd_complement (const zdd &A, ForwardIt begin, ForwardIt end)
	Complement of A within the given domain.
template<typename ForwardIt >
__zdd	adiar::zdd_complement (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Complement of A within the given domain.
__zdd	adiar::zdd_complement (const zdd &A)
	Complement of A within the global Variable Domain.
__zdd	adiar::zdd_complement (const exec_policy &ep, const zdd &A)
	Complement of A within the global Variable Domain.
__zdd	adiar::operator~ (const zdd &A)
__zdd	adiar::zdd_expand (const zdd &A, const generator< zdd::label_type > &vars)
	Expands the domain of the given ZDD to also include the given set of labels.
__zdd	adiar::zdd_expand (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &vars)
	Expands the domain of the given ZDD to also include the given set of labels.
template<typename ForwardIt >
__zdd	adiar::zdd_expand (const zdd &A, ForwardIt begin, ForwardIt end)
	Expands the domain of the given ZDD to also include the given set of labels.
template<typename ForwardIt >
__zdd	adiar::zdd_expand (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Expands the domain of the given ZDD to also include the given set of labels.
__zdd	adiar::zdd_offset (const zdd &A, zdd::label_type var)
	Subset that do not include the given element.
__zdd	adiar::zdd_offset (const exec_policy &ep, const zdd &A, zdd::label_type var)
	Subset that do not include the given element.
__zdd	adiar::zdd_offset (const zdd &A)
	Subset that do not include the top variable.
__zdd	adiar::zdd_offset (const exec_policy &ep, const zdd &A)
	Subset that do not include the top variable.
__zdd	adiar::zdd_offset (const zdd &A, const generator< zdd::label_type > &vars)
	Subset that do not include the given set of variables.
__zdd	adiar::zdd_offset (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &vars)
	Subset that do not include the given set of variables.
template<typename ForwardIt >
__zdd	adiar::zdd_offset (const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do not include the given set of variables.
template<typename ForwardIt >
__zdd	adiar::zdd_offset (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do not include the given set of variables.
__zdd	adiar::zdd_onset (const zdd &A, zdd::label_type var)
	Subset that do include the given element.
__zdd	adiar::zdd_onset (const exec_policy &ep, const zdd &A, zdd::label_type var)
	Subset that do include the given element.
__zdd	adiar::zdd_onset (const zdd &A)
	Subset that do include the top variable.
__zdd	adiar::zdd_onset (const exec_policy &ep, const zdd &A)
	Subset that do include the top variable.
__zdd	adiar::zdd_onset (const zdd &A, const generator< zdd::label_type > &vars)
	Subset that do include the given set of variables.
__zdd	adiar::zdd_onset (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &vars)
	Subset that do include the given set of variables.
template<typename ForwardIt >
__zdd	adiar::zdd_onset (const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do include the given set of variables.
template<typename ForwardIt >
__zdd	adiar::zdd_onset (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do include the given set of variables.
__zdd	adiar::zdd_project (const zdd &A, const predicate< zdd::label_type > &dom)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.
__zdd	adiar::zdd_project (const exec_policy &ep, const zdd &A, const predicate< zdd::label_type > &dom)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.
__zdd	adiar::zdd_project (const zdd &A, const generator< zdd::label_type > &dom)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.
__zdd	adiar::zdd_project (const exec_policy &ep, const zdd &A, const generator< zdd::label_type > &dom)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.
template<typename ForwardIt >
__zdd	adiar::zdd_project (const zdd &A, ForwardIt begin, ForwardIt end)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.
template<typename ForwardIt >
__zdd	adiar::zdd_project (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

Variable Reordering / Substitution
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.
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.
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.

Transition System Operations
bdd	adiar::bdd_relprod (const bdd &states, const bdd &relation, const predicate< bdd::label_type > &pred)
	Relational Product of states and a relation.
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.
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.
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.
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.
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.
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.
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.
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.
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.

Predicates
bool	adiar::bdd_iscanonical (const bdd &f)
	Check whether a BDD is canonical.
bool	adiar::bdd_isconst (const bdd &f)
	Whether a BDD is a constant.
bool	adiar::bdd_isterminal (const bdd &f)
	Whether a BDD is a constant (terminal).
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, i.e. is a literal.
bool	adiar::bdd_isithvar (const bdd &f)
	Whether a BDD is the function of a single positive variable.
bool	adiar::bdd_isnithvar (const bdd &f)
	Whether a BDD is the function of a single negative variable.
bool	adiar::bdd_iscube (const bdd &f)
	Whether a BDD represents a cube.
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.
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)
bool	adiar::zdd_iscanonical (const zdd &A)
	Check whether a given ZDD is canonical.
bool	adiar::zdd_isterminal (const zdd &A)
	Whether this ZDD represents a terminal.
bool	adiar::zdd_isfalse (const zdd &A)
	Whether this ZDD represents false terminal.
bool	adiar::zdd_isempty (const zdd &A)
	Whether it is the empty family, i.e. Ø .
bool	adiar::zdd_istrue (const zdd &A)
	Whether this BDD represents true terminal.
bool	adiar::zdd_isnull (const zdd &A)
	Whether it is the null family, i.e. { Ø } .
bool	adiar::zdd_ispoint (const zdd &A)
	Whether it contains a single bit-vector a, i.e. A = { a }.
bool	adiar::zdd_equal (const zdd &A, const zdd &B)
	Whether they represent the same family.
bool	adiar::zdd_equal (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether they represent the same family.
bool	adiar::operator== (const zdd &lhs, const zdd &rhs)
bool	adiar::zdd_unequal (const zdd &A, const zdd &B)
	Whether they represent two different families.
bool	adiar::zdd_unequal (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether they represent two different families.
bool	adiar::operator!= (const zdd &lhs, const zdd &rhs)
bool	adiar::zdd_subseteq (const zdd &A, const zdd &B)
	Whether one family is a subset or equal to the other.
bool	adiar::zdd_subseteq (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether one family is a subset or equal to the other.
bool	adiar::operator<= (const zdd &lhs, const zdd &rhs)
bool	adiar::operator>= (const zdd &lhs, const zdd &rhs)
bool	adiar::zdd_subset (const zdd &A, const zdd &B)
	Whether one family is a strict subset of the other.
bool	adiar::zdd_subset (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether one family is a strict subset of the other.
bool	adiar::operator< (const zdd &lhs, const zdd &rhs)
bool	adiar::operator> (const zdd &lhs, const zdd &rhs)
bool	adiar::zdd_disjoint (const zdd &A, const zdd &B)
	Whether the two families are disjoint.
bool	adiar::zdd_disjoint (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether the two families are disjoint.

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 the Boolean function, i.e. the number of levels present in the BDD.
uint64_t	adiar::bdd_pathcount (const bdd &f)
	Count all unique (but not necessarily disjoint) paths to the true terminal.
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.
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.
uint64_t	adiar::bdd_satcount (const exec_policy &ep, const bdd &f)
	Count the number of assignments *x that make f(x) true.
size_t	adiar::zdd_nodecount (const zdd &A)
	The number of (internal) nodes used to represent the family of sets.
zdd::label_type	adiar::zdd_varcount (const zdd &A)
	The number of variables that exist in the family of sets, i.e. the number of levels present in the ZDD.
uint64_t	adiar::zdd_size (const zdd &A)
	The number of sets in the family of sets.
uint64_t	adiar::zdd_size (const exec_policy &ep, const zdd &A)
	The number of sets in the family of sets.

Input Variables
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.
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.
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.
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.

Conversion from other Decision Diagrams
__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.
__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.
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.
__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.
__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.
__zdd	adiar::zdd_from (const exec_policy &ep, 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.
template<typename ForwardIt >
__zdd	adiar::zdd_from (const exec_policy &ep, 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.
__zdd	adiar::zdd_from (const exec_policy &ep, const bdd &f)
	Obtains the BDD that represents the same function/set as the given ZDD within the global domain.

DOT Files
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.
void	adiar::zdd_printdot (const zdd &A, std::ostream &out=std::cout, bool include_id=false)
	Output a DOT drawing of a ZDD to the given output stream.
void	adiar::zdd_printdot (const zdd &A, const std::string &file_name, bool include_id=false)
	Output a DOT drawing of a ZDD 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 release your 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_equal()

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

Whether the two BDDs represent the same function.

Remarks

If either f or g is an unreduced result of an immediate computation as part of evaluating bdd_equal's' parameters, one will have to pay the cost of reducing it. If you need the result later, please store it in an intermediate variable.

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

See also

bdd_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 (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_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.

Whether f is equivalent to \( x \).

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.

Whether f is equivalent to \( \neg x \).

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, i.e. is a literal.

Whether f is equivalent to \( x \) or \( \neg x \).

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 (requires a full traversal).

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

Returns

\( (\exists x \in \{ x \mid x \equiv 0 \mod 2 \} : (\mathit{states} \land \mathit{relation})) [x' \mapsto x' - 1] \)

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.

Returns

\( (\exists x \in \{ x \mid x < \mathit{varcount} \} : (\mathit{states} \land \mathit{relation})) [x' \mapsto x' - \mathit{varcount}] \)

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. For all intends an purposes, this relabelling happens after quantification.

Returns

\( (\exists x \in \{ x \mid \mathit{m}(x) = \text{None} \} : (\mathit{states} \land \mathit{relation}))[x' \mapsto m(x')] \)

Exceptions

invalid_argument

if m is not a monotonic relabelling.

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. For all intends an purposes, this relabelling happens after quantification.
m_type	Guarantees on the class of variable relabelling, e.g. whether it is monotonic.

Returns

\( (\exists x \in \{ x \mid \mathit{m}(x) = \text{None} \} : (\mathit{states} \land \mathit{relation}))[x' \mapsto m(x')] \)

Exceptions

invalid_argument

if m is not a monotonic relabelling.

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.

Returns

\( (\exists x' \{ x' \mid x' \equiv 1 \mod 2 \} : (\mathit{states}[x \mapsto x + 1] \land \mathit{relation})) \)

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.

Returns

\( (\exists x' \in \{ x' \mid \geq \mathit{varcount} \} : (\mathit{states}[x \mapsto x + \mathit{varcount}] \land \mathit{relation})) \)

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). For all intends an purposes, this relabelling happens prior to conjunction.

Returns

\( (\exists x' \in \{ x' \mid \mathit{m}(x') = \text{None} \} : (\mathit{states}[x \mapsto m(x)] \land \mathit{relation})) \)

Exceptions

invalid_argument

if m is not a monotonic relabelling.

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). For all intends and purposes, this relabelling happens prior to conjunction.
m_type	Guarantees on the class of variable relabelling, e.g. whether it is monotonic.

Returns

\( (\exists x' \in \{ x' \mid \mathit{m}(x') = \text{None} \} : (\mathit{states}[x \mapsto m(x)] \land \mathit{relation})) \)

Exceptions

invalid_argument

if m is not a monotonic relabelling.

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.

Returns

\( \exists x \in \mathit{pred}(x) : (\mathit{states} \land \mathit{relation}) \)

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

Remarks

If either f or g is an unreduced result of an immediate computation as part of evaluating bdd_unequal's' parameters, one will have to pay the cost of reducing it. If you need the result later, please store it in an intermediate variable.

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!=() [1/2]

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

See also

bdd_equal bdd_unequal

operator!=() [2/2]

bool adiar::operator!=	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also

zdd_unequal

operator&() [1/2]

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

See also

bdd_and

operator&() [2/2]

__zdd adiar::operator&	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also

zdd_intsec

operator*() [1/2]

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

See also

bdd_and

operator*() [2/2]

__zdd adiar::operator*	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also

zdd_intsec

operator+() [1/3]

bdd adiar::operator+

(

const bdd &

f

)

See also

bdd_or

operator+() [2/3]

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

See also

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

bdd_or

operator+() [3/3]

zdd adiar::operator+

(

const zdd &

A

)

See also

zdd_union

operator-() [1/4]

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/4]

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

See also

bdd_diff

operator-() [3/4]

__zdd adiar::operator-

(

const zdd &

A

)

Remarks

Unary difference subtracts from universe over all variables in th global Variable Domain , making its equivalent to its complement.

See also

zdd_diff, zdd_complement

operator-() [4/4]

__zdd adiar::operator-	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also

zdd_diff

operator<()

bool adiar::operator<	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also

zdd_subset

operator<=()

bool adiar::operator<=	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also

zdd_subseteq

operator==() [1/2]

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

See also

bdd_equal

operator==() [2/2]

bool adiar::operator==	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also

zdd_equal

operator>()

bool adiar::operator>	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also

zdd_subset

operator>=()

bool adiar::operator>=	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also

zdd_subseteq

operator^()

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

See also

bdd_xor

operator|() [1/2]

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

See also

bdd_or

operator|() [2/2]

__zdd adiar::operator|	(	const zdd &	lhs,
		const zdd &	rhs
	)

See also

zdd_union

operator~() [1/2]

bdd adiar::operator~

(

const bdd &

f

)

See also

bdd_not

operator~() [2/2]

__zdd adiar::operator~

(

const zdd &

A

)

See also

zdd_complement

zdd_binop()

__zdd adiar::zdd_binop	(	const zdd &	A,
		const zdd &	B,
		const predicate< bool, bool > &	op
	)

Apply a binary operator between the sets of two families.

Parameters

A	ZDD for the left-hand-side of the operator
B	ZDD for the right-hand-side of the operator
op	Binary predicate to combine the two families.

Returns

Product construction of the two that represents the boolean operator applied to the two family of sets.

zdd_bot() [1/3]

zdd adiar::zdd_bot

(

)

Bottom of the powerset lattice.

See also

zdd_empty

zdd_bot() [2/3]

zdd adiar::zdd_bot

(

const generator< zdd::label_type > &

dom

)

Bottom of the powerset lattice.

Parameters

dom	Generator function of the variables in descending order. These values may not exceed zdd::max_label.

See also

zdd_empty

zdd_bot() [3/3]

template<typename ForwardIt >

zdd adiar::zdd_bot ( ForwardIt  begin, ForwardIt  end  )

inline

Bottom of the powerset lattice.

Parameters

begin	Single-pass forward iterator that provides the domain's variables in descending order. The variables may not exceed zdd::max_label.
end	Marks the end for begin.

See also

zdd_empty

zdd_change() [1/2]

__zdd adiar::zdd_change	(	const zdd &	A,
		const generator< zdd::label_type > &	vars
	)

The symmetric difference between each set in the family and the given set of variables.

Parameters

A	ZDD to apply with the other.
vars	Generator function of labels to flip in ascending order. These values may not exceed zdd::max_label.

Returns

\( \{ \mathit{vars} \Delta a \mid a \in A \} \)

zdd_change() [2/2]

template<typename ForwardIt >

__zdd adiar::zdd_change	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

The symmetric difference between each set in the family and the given set of variables.

Parameters

A	ZDD to apply with the other.
begin	Single-pass forward iterator that provides the to-be flipped variables in ascending order. These values may not exceed zdd::max_label.
end	Marks the end for begin.

Returns

\( \{ \mathit{vars} \Delta a \mid a \in A \} \)

zdd_complement() [1/3]

__zdd adiar::zdd_complement

(

const zdd &

A

)

Complement of A within the global Variable Domain.

Parameters

A	family of sets to complement

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

\( 2^{\mathit{dom}} \setminus A \)

See also

domain_set domain_isset

zdd_complement() [2/3]

__zdd adiar::zdd_complement	(	const zdd &	A,
		const generator< zdd::label_type > &	dom
	)

Complement of A within the given domain.

Parameters

A	family of sets to complement
dom	Labels of the domain in ascending order

Returns

\( 2^{\mathit{dom}} \setminus A \)

zdd_complement() [3/3]

template<typename ForwardIt >

__zdd adiar::zdd_complement	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Complement of A within the given domain.

Parameters

A	family of sets to complement
begin	Single-pass forward iterator that provides the domain's variables in ascending order. These values may not exceed zdd::max_label.
end	Marks the end for begin.

Returns

\( 2^{\mathit{dom}} \setminus A \)

zdd_diff()

__zdd adiar::zdd_diff	(	const zdd &	A,
		const zdd &	B
	)

The set difference of two families of sets.

Returns

\( A \setminus B \)

zdd_expand() [1/2]

__zdd adiar::zdd_expand	(	const zdd &	A,
		const generator< zdd::label_type > &	vars
	)

Expands the domain of the given ZDD to also include the given set of labels.

Adds don't care nodes on each levels in vars. That is, this essentially is the inverse of the zdd_project and lifts the set of sets unprojects to a larger domain.

Parameters

A	Family of set to expand.
vars	Generator function of labels to unproject in ascending order. No variables it generates may already exist in A or exceed zdd::max_label.

Returns

\( \bigcup_{a \in A, i \in 2^{vars}} (a \cup i) \)

zdd_expand() [2/2]

template<typename ForwardIt >

__zdd adiar::zdd_expand	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Expands the domain of the given ZDD to also include the given set of labels.

Parameters

A	Family of set to expand.
begin	Single-pass forward iterator that provides the to-be unprojected variables in ascending order. These may not be present in A or exceed zdd::max_label.
end	Marks the end for begin.

Returns

\( \bigcup_{a \in A, i \in 2^{vars}} (a \cup i) \)

See also

zdd_project

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.

zdd_intsec()

__zdd adiar::zdd_intsec	(	const zdd &	A,
		const zdd &	B
	)

The intersection of two families of sets.

Returns

\( A \cap B \)

zdd_iscanonical()

bool adiar::zdd_iscanonical

(

const zdd &

A

)

Check whether a given ZDD is canonical.

zdd_ithvar() [1/3]

zdd adiar::zdd_ithvar

(

zdd::label_type

var

)

The set of bitvectors over the globally set domain where var is set to true.

Parameters

var	The variable to be forced to true.

Precondition

domain_isset() == true and the variable var should occur in the global domain.

zdd_ithvar() [2/3]

zdd adiar::zdd_ithvar	(	zdd::label_type	var,
		const generator< zdd::label_type > &	dom
	)

The set of bitvectors over a given domain where var is set to true.

This function is (given the same domain of variables) semantically equivalent to bdd_ithvar even though the ZDD DAG does not at all look like the BDD DAG.

Parameters

var	The variable to be forced to true.
dom	Generator function of the domain in descending order. These variables should be smaller than or equals to zdd::max_label.

Precondition

The variable var should occur in dom.

Exceptions

invalid_argument

If dom is not in descending order.

zdd_ithvar() [3/3]

template<typename ForwardIt >

zdd adiar::zdd_ithvar	(	zdd::label_type	var,
		ForwardIt	begin,
		ForwardIt	end
	)

The set of bitvectors over a given domain where var is set to true.

Parameters

var	The variable to be forced to true.
begin	Single-pass forward iterator that provides the domain's variables in descending order. The variables may not exceed zdd::max_label.
end	Marks the end for begin.

Precondition

The variable var should occur in dom.

Exceptions

invalid_argument

If the iterator does not provide values in descending order.

zdd_nithvar() [1/3]

zdd adiar::zdd_nithvar

(

zdd::label_type

var

)

The set of bitvectors over the globally set domain where var is set to false.

Parameters

var	The variable to be forced to false.

Precondition

domain_isset() == true and the variable var should occur in the global domain.

zdd_nithvar() [2/3]

zdd adiar::zdd_nithvar	(	zdd::label_type	var,
		const generator< zdd::label_type > &	dom
	)

The set of bitvectors over a given domain where var is set to false.

Creates a ZDD with a don't care chain of nodes to the true child except for the node for var; this one instead is forced to be true.

Parameters

var	The variable to be forced to false.
dom	Generator function of the domain in descending order. The variables should be smaller than or equals to zdd::max_label.

Precondition

The variable var should occur in dom.

Exceptions

invalid_argument

If dom is not in descending order.

zdd_nithvar() [3/3]

template<typename ForwardIt >

zdd adiar::zdd_nithvar	(	zdd::label_type	var,
		ForwardIt	begin,
		ForwardIt	end
	)

The set of bitvectors over a given domain where var is set to false.

Parameters

var	The variable to be forced to false.
begin	Single-pass forward iterator that provides the domain's variables in descending order. The variables may not exceed zdd::max_label.
end	Marks the end for begin.

Precondition

The variable var should occur in dom.

Exceptions

invalid_argument

If the iterator does not provide values in descending order.

zdd_offset() [1/4]

__zdd adiar::zdd_offset

(

const zdd &

A

)

Subset that do not include the top variable.

Parameters

A	Family of set

Remarks

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

Exceptions

invalid_argument

If A is a terminal.

zdd_offset() [2/4]

__zdd adiar::zdd_offset	(	const zdd &	A,
		const generator< zdd::label_type > &	vars
	)

Subset that do not include the given set of variables.

Parameters

A	Family of set
vars	Generator function of the variable labels to filter on in ascending order. The values generated should not exceed zdd::max_label.

Returns

\( \{ a \in A \mid \forall i \in \mathit{vars} : i \not\in a \} \)

zdd_offset() [3/4]

template<typename ForwardIt >

__zdd adiar::zdd_offset	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Subset that do not include the given set of variables.

Parameters

A	Family of set
begin	Single-pass forward iterator that provides the variables to filter out in ascending order. These values may not exceed zdd::max_label.
end	Marks the end for begin.

Returns

\( \{ a \in A \mid \forall i \in \mathit{vars} : i \not\in a \} \)

zdd_offset() [4/4]

__zdd adiar::zdd_offset	(	const zdd &	A,
		zdd::label_type	var
	)

Subset that do not include the given element.

Parameters

A	Family of set
var	Variable to include.

Returns

\( \{ a \in A \mid \mathit{var} \not\in a \} \)

zdd_onset() [1/4]

__zdd adiar::zdd_onset

(

const zdd &

A

)

Subset that do include the top variable.

Parameters

A	Family of set

Remarks

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

Exceptions

invalid_argument

If A is a terminal.

zdd_onset() [2/4]

__zdd adiar::zdd_onset	(	const zdd &	A,
		const generator< zdd::label_type > &	vars
	)

Subset that do include the given set of variables.

Parameters

A	Family of set
vars	Generator function of the variable labels to filter on in ascending order. The values generated may not exceed zdd::max_label

Returns

\( \{ a \in A \mid \forall i \in \mathit{vars} : i \in a \} \)

zdd_onset() [3/4]

template<typename ForwardIt >

__zdd adiar::zdd_onset	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Subset that do include the given set of variables.

Parameters

A	Family of set
begin	Single-pass forward iterator that provides the variables to filter out in ascending order. These values may not exceed zdd::max_label
end	Marks the end for begin.

Returns

\( \{ a \in A \mid \forall i \in \mathit{vars} : i \in a \} \)

zdd_onset() [4/4]

__zdd adiar::zdd_onset	(	const zdd &	A,
		zdd::label_type	var
	)

Subset that do include the given element.

Parameters

A	Family of set
var	Variable to include.

Returns

\( \{ a \in A \mid \mathit{var} \in a \} \)

zdd_point() [1/2]

zdd adiar::zdd_point

(

const generator< zdd::label_type > &

vars

)

The family { { 1, 2, ..., k } } with a single bit-vector.

Creates the ZDD for a set with a single bit-vector, i.e. a point.

Parameters

vars	Generator function of the variables in descending order. The variables may not exceed zdd::max_label.

Exceptions

invalid_argument

If vars are not in descending order.

zdd_point() [2/2]

template<typename ForwardIt >

zdd adiar::zdd_point	(	ForwardIt	begin,
		ForwardIt	end
	)

The family { { 1, 2, ..., k } } with a single bit-vector.

Parameters

begin	Single-pass forward iterator that provides the variables in descending order. The variables may not exceed zdd::max_label.
end	Marks the end for begin.

Exceptions

invalid_argument

If the iterator does not provide values in descending order.

zdd_powerset() [1/2]

zdd adiar::zdd_powerset

(

const generator< zdd::label_type > &

vars

)

The powerset of all given variables.

Creates a ZDD with a don't care chain of nodes to the true child.

Parameters

vars	Generator function of the variables in descending order. These values may not exceed zdd::max_label.

Exceptions

invalid_argument

If vars are not in ascending order.

zdd_powerset() [2/2]

template<typename ForwardIt >

zdd adiar::zdd_powerset	(	ForwardIt	begin,
		ForwardIt	end
	)

The powerset of all given variables.

Parameters

begin	Single-pass forward iterator that provides the variables in descending order. The variables may not exceed zdd::max_label
end	Marks the end for begin.

Exceptions

invalid_argument

If the iterator does not provide values in descending order.

zdd_project() [1/3]

__zdd adiar::zdd_project	(	const zdd &	A,
		const generator< zdd::label_type > &	dom
	)

Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

Parameters

A	Family of sets to project
dom	Generator function, that produces the variables of the domain in descending order. They should not exceed zdd::max_label.

Returns

\( \prod_{\mathit{dom}}(A) = \{ a \setminus \mathit{dom}^c \mid a \in A \} \)

See also

zdd_expand

zdd_project() [2/3]

__zdd adiar::zdd_project	(	const zdd &	A,
		const predicate< zdd::label_type > &	dom
	)

Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

Parameters

A	Family of sets to project
dom	Predicate function that defines the domain.

Returns

\( \prod_{\mathit{dom}}(A) = \{ a \setminus \mathit{dom}^c \mid a \in A \} \)

See also

zdd_expand

zdd_project() [3/3]

template<typename ForwardIt >

__zdd adiar::zdd_project	(	const zdd &	A,
		ForwardIt	begin,
		ForwardIt	end
	)

Project family of sets onto a domain, i.e. remove from every set all variables not within the domain.

Parameters

A	Family of sets to project
begin	Single-pass forward iterator that provides the domain in descending order. Its values should not exceed zdd::max_label
end	Marks the end for begin.

Returns

\( \prod_{\mathit{dom}}(A) = \{ a \setminus \mathit{dom}^c \mid a \in A \} \)

See also

zdd_expand

zdd_singleton()

zdd adiar::zdd_singleton

(

zdd::label_type

var

)

The family { {i} } .

Creates a ZDD of a single node with label var and the children false and true. The given label must be smaller than zdd::max_label.

Parameters

var	The label of the desired variable to include

Exceptions

invalid_argument

If var is a too large value.

zdd_singletons() [1/2]

zdd adiar::zdd_singletons

(

const generator< zdd::label_type > &

vars

)

The family { {1}, {2}, ..., {k} }.

Creates a ZDD with a chain of nodes on the 'low' arc to the true child, and false otherwise.

Parameters

vars	Generator function of the variables in descending order. The variables may not exceed zdd::max_label.

Exceptions

invalid_argument

If vars are not in descending order.

zdd_singletons() [2/2]

template<typename ForwardIt >

zdd adiar::zdd_singletons	(	ForwardIt	begin,
		ForwardIt	end
	)

The family { {1}, {2}, ..., {k} }.

Parameters

begin	Single-pass forward iterator that provides the variables in descending order. The variables may not exceed zdd::max_label.
end	Marks the end for begin.

Exceptions

invalid_argument

If the iterator does not provide values in descending order.

zdd_terminal()

zdd adiar::zdd_terminal

(

bool

value

)

The ZDD of only a single terminal.

Parameters

value

The constant terminal value.

See also

zdd_empty zdd_null

zdd_top() [1/3]

zdd adiar::zdd_top

(

)

Top of the powerset lattice.

Since no set of variables is given, the global Variable Domain is used (if available).

See also

zdd_powerset, zdd_null

zdd_top() [2/3]

zdd adiar::zdd_top

(

const generator< zdd::label_type > &

dom

)

Top of the powerset lattice.

Parameters

dom	Generator of the variables in descending order. These values may not exceed zdd::max_label.

See also

zdd_powerset, zdd_null

zdd_top() [3/3]

template<typename ForwardIt >

zdd adiar::zdd_top ( ForwardIt  begin, ForwardIt  end  )

inline

Top of the powerset lattice.

Parameters

begin	Single-pass forward iterator that provides the domain's variables in descending order. These values may not exceed zdd::max_label.
end	Marks the end for begin.

See also

zdd_empty

zdd_union()

__zdd adiar::zdd_union	(	const zdd &	A,
		const zdd &	B
	)

The union of two families of sets.

Returns

\( A \cup B \)

zdd_vars() [1/2]

zdd adiar::zdd_vars

(

const generator< zdd::label_type > &

vars

)

The family { { 1, 2, ..., k } }.

Creates a ZDD with a chain of nodes on the 'high' arc to the true child, and false otherwise.

Parameters

vars	Generator function of the variables in descending order. The variables may not exceed zdd::max_label.

Exceptions

invalid_argument

If vars are not in descending order.

zdd_vars() [2/2]

template<typename ForwardIt >

zdd adiar::zdd_vars	(	ForwardIt	begin,
		ForwardIt	end
	)

The family { { 1, 2, ..., k } }.

Parameters

begin	Single-pass forward iterator that provides the variables in descending order. The variables may not exceed zdd::max_label.
end	Marks the end for begin.

Exceptions

invalid_argument

If the iterator does not provide values in descending order.