adiar Namespace Reference

Core types. More...

Classes
class	__bdd
	A (possibly) unreduced Binary Decision Diagram. More...
class	__zdd
	A (possibly unreduced) Zero-suppressed Decision Diagram. More...
class	bdd
	A reduced Binary Decision Diagram. More...
class	builder
	A builder for decision diagrams. More...
class	builder_ptr
	The pointer type that builders use to identify the nodes they have constructed in a decision diagram. More...
class	exec_policy
	Settings to dictate the execution of Adiar's algorithms. More...
struct	statistics
	Available statistics from algorithm's and data structures. More...
class	zdd
	Reduced Ordered Zero-suppressed Decision Diagram. More...

Typedefs
using	bdd_ptr = builder_ptr< bdd_policy >
	Pointer for a BDD node created by a BDD builder.
using	zdd_ptr = builder_ptr< zdd_policy >
	Pointer for a ZDD node created by a ZDD builder.
using	bdd_builder = builder< bdd_policy >
	Builder for BDDs.
using	zdd_builder = builder< zdd_policy >
	Builder for ZDDs.
using	domain_var = internal::node::label_type
	The variable type of a domain variable.
using	invalid_argument = std::invalid_argument
	Inputs that are invalid.
using	domain_error = std::domain_error
	Inputs for which an operation is undefined.
using	out_of_range = std::out_of_range
	Attempt to access elements outside of the given range.
using	runtime_error = std::runtime_error
	Errors beyond the scope of the program.
using	system_error = std::system_error
	System runtime errors with an associated error code.
template<bool Condition, typename Type = void>
using	enable_if = typename std::enable_if< Condition, Type >::type
template<typename T1 , typename T2 >
using	pair = std::pair< T1, T2 >
	A pair of values.
template<typename T >
using	optional = std::optional< T >
	An optional value, i.e. a possibly existent value.
template<typename T >
using	shared_ptr = std::shared_ptr< T >
	Shared ownership of an object on the heap. This smart pointer essentially provides a (thread-safe) reference count and automatic garbage collection.
template<typename T >
using	unique_ptr = std::unique_ptr< T >
	Sole ownership of an object on the heap. Unlike the shared_ptr, this smart pointer has the semantics of a single owner (and hence no need to do reference counting).

Enumerations
enum class	assignment : signed char { False = 0 , True = 1 , None = -1 }
	Possible values to assign a variable. More...
enum class	replace_type : signed char { Non_Monotone = 3 , Monotone = 2 , Shift = 0 , Identity = -1 }
	Possible guarantees of a variable permutation/remapping m of type int -> int. More...

Functions
template<>
const exec_policy::access &	exec_policy::get< exec_policy::access > () const
	Chosen access mode.
template<>
const exec_policy::memory &	exec_policy::get< exec_policy::memory > () const
	Chosen memory type.
template<>
const exec_policy::quantify::algorithm &	exec_policy::get< exec_policy::quantify::algorithm > () const
	Chosen quantification strategy.
template<>
const exec_policy::quantify::transposition_growth &	exec_policy::get< exec_policy::quantify::transposition_growth > () const
	Chosen quantification strategy.
template<>
const exec_policy::quantify::transposition_max &	exec_policy::get< exec_policy::quantify::transposition_max > () const
	Chosen quantification strategy.
void	domain_set (const domain_var varcount)
	Set the domain globally for all of Adiar to be [0, varcount).
void	domain_set (const generator< domain_var > &dom)
	Set the domain globally for all of Adiar to be the variables produced by the given generator function.
template<typename ForwardIt >
void	domain_set (ForwardIt begin, ForwardIt end)
	Set the domain globally for all of Adiar to be the variables in the given range of iterators.
void	domain_set (const internal::shared_file< domain_var > &dom)
	Set the domain globally for all of Adiar.
void	domain_unset ()
	Removes any globally shared domain variables (if any).
bool	domain_isset ()
	Whether Adiar has a global domain.
internal::shared_file< domain_var >	domain_get ()
	Returns the global domain.
domain_var	domain_size ()
	The size of the domain.
statistics	statistics_get ()
	Obtain a copy of all statistics gathered.
void	statistics_print (std::ostream &o=std::cout)
	Print statistics to an output stream (default std::cout).
void	statistics_reset ()
	Resets all statistics to default value.
template<typename T1 , typename T2 >
constexpr pair< T1, T2 >	make_pair (const T1 &t1, const T2 &t2)
	Create an adiar::pair, deducing the target type based on the types of the arguments.
template<typename T >
constexpr optional< T >	make_optional ()
	Create an empty adiar::optional, i.e. None.
template<typename T >
constexpr optional< T >	make_optional (const T &t)
	Create an adiar::optional with Some value.
template<typename T , typename... TT>
shared_ptr< T >	make_shared (TT &&... tt)
	Creates a new object on the heap with shared ownership.
template<typename T , typename... TT>
unique_ptr< T >	make_unique (TT &&... tt)
	Creates a new object on the heap with unique ownership.
Basic Constructors
To construct a more complex but well-structured zdd by hand, please use the zdd_builder (see builder) instead.
bdd	bdd_const (bool value)
	The BDD representing the given constant value.
bdd	bdd_terminal (bool value)
	The BDD representing the given constant value.
bdd	bdd_false ()
	The BDD representing the constant false.
bdd	bdd_bot ()
	The bottom of the powerset lattice.
bdd	bdd_true ()
	The BDD representing the constant true.
bdd	bdd_top ()
	The top of the powerset lattice.
bdd	bdd_ithvar (bdd::label_type var)
	The BDD representing the i'th variable.
bdd	bdd_nithvar (bdd::label_type var)
	The BDD representing the negation of the i'th variable.
bdd	bdd_and (const generator< int > &vars)
	The BDD representing the logical 'and' of all the given variables, i.e. a term of variables.
bdd	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	bdd_and (ForwardIt begin, ForwardIt end)
	The BDD representing the logical 'and' of all the given variables, i.e. a term of variables.
bdd	bdd_or (const generator< int > &vars)
	The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables.
bdd	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	bdd_or (ForwardIt begin, ForwardIt end)
	The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables.
bdd	bdd_cube (const generator< int > &vars)
	The BDD representing the cube of all the given variables.
bdd	bdd_cube (const generator< pair< bdd::label_type, bool > > &vars)
	The BDD representing the cube of all the given variables.
template<typename ForwardIt >
bdd	bdd_cube (ForwardIt begin, ForwardIt end)
	The BDD representing the cube of all the given variables.
zdd	zdd_terminal (bool value)
	The ZDD of only a single terminal.
zdd	zdd_empty ()
	The empty family, i.e. Ø .
zdd	zdd_null ()
	The family only with the empty set, i.e. { Ø } .
zdd	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	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	zdd_ithvar (zdd::label_type var)
	The set of bitvectors over the globally set domain where var is set to true.
zdd	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	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	zdd_nithvar (zdd::label_type var)
	The set of bitvectors over the globally set domain where var is set to false.
zdd	zdd_vars (const generator< zdd::label_type > &vars)
	The family { { 1, 2, ..., k } }.
template<typename ForwardIt >
zdd	zdd_vars (ForwardIt begin, ForwardIt end)
	The family { { 1, 2, ..., k } }.
zdd	zdd_point (const generator< zdd::label_type > &vars)
	The family { { 1, 2, ..., k } } with a single bit-vector.
template<typename ForwardIt >
zdd	zdd_point (ForwardIt begin, ForwardIt end)
	The family { { 1, 2, ..., k } } with a single bit-vector.
zdd	zdd_singleton (zdd::label_type var)
	The family { {i} } .
zdd	zdd_singletons (const generator< zdd::label_type > &vars)
	The family { {1}, {2}, ..., {k} }.
template<typename ForwardIt >
zdd	zdd_singletons (ForwardIt begin, ForwardIt end)
	The family { {1}, {2}, ..., {k} }.
zdd	zdd_powerset (const generator< zdd::label_type > &vars)
	The powerset of all given variables.
template<typename ForwardIt >
zdd	zdd_powerset (ForwardIt begin, ForwardIt end)
	The powerset of all given variables.
zdd	zdd_bot (const generator< zdd::label_type > &dom)
	Bottom of the powerset lattice.
template<typename ForwardIt >
zdd	zdd_bot (ForwardIt begin, ForwardIt end)
	Bottom of the powerset lattice.
zdd	zdd_bot ()
	Bottom of the powerset lattice.
zdd	zdd_top (const generator< zdd::label_type > &dom)
	Top of the powerset lattice.
template<typename ForwardIt >
zdd	zdd_top (ForwardIt begin, ForwardIt end)
	Top of the powerset lattice.
zdd	zdd_top ()
	Top of the powerset lattice.
Basic Operations
bdd	bdd_not (const bdd &f)
	Negation of a BDD.
bdd	operator~ (const bdd &f)
__bdd	bdd_apply (const bdd &f, const bdd &g, const predicate< bool, bool > &op)
	Apply a binary operator between two BDDs.
__bdd	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	bdd_and (const bdd &f, const bdd &g)
	Logical 'and' operator.
__bdd	bdd_and (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'and' operator.
__bdd	operator& (const bdd &lhs, const bdd &rhs)
__bdd	operator* (const bdd &lhs, const bdd &rhs)
__bdd	bdd_nand (const bdd &f, const bdd &g)
	Logical 'nand' operator.
__bdd	bdd_nand (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'nand' operator.
__bdd	bdd_or (const bdd &f, const bdd &g)
	Logical 'or' operator.
__bdd	bdd_or (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'or' operator.
__bdd	operator| (const bdd &lhs, const bdd &rhs)
bdd	operator+ (const bdd &f)
__bdd	operator+ (const bdd &lhs, const bdd &rhs)
__bdd	bdd_nor (const bdd &f, const bdd &g)
	Logical 'nor' operator.
__bdd	bdd_nor (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'nor' operator.
__bdd	bdd_xor (const bdd &f, const bdd &g)
	Logical 'xor' operator.
__bdd	bdd_xor (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'xor' operator.
__bdd	operator^ (const bdd &lhs, const bdd &rhs)
__bdd	bdd_xnor (const bdd &f, const bdd &g)
	Logical 'xnor' operator.
__bdd	bdd_xnor (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'xnor' operator.
__bdd	bdd_imp (const bdd &f, const bdd &g)
	Logical 'implication' operator.
__bdd	bdd_imp (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'implication' operator.
__bdd	bdd_invimp (const bdd &f, const bdd &g)
	Logical 'inverse implication' operator.
__bdd	bdd_invimp (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'inverse implication' operator.
__bdd	bdd_equiv (const bdd &f, const bdd &g)
	Logical 'equivalence' operator.
__bdd	bdd_equiv (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'equivalence' operator.
__bdd	bdd_diff (const bdd &f, const bdd &g)
	Logical 'difference' operator.
__bdd	bdd_diff (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'difference' operator.
bdd	operator- (const bdd &f)
__bdd	operator- (const bdd &lhs, const bdd &rhs)
__bdd	bdd_less (const bdd &f, const bdd &g)
	Logical 'less than' operator.
__bdd	bdd_less (const exec_policy &ep, const bdd &f, const bdd &g)
	Logical 'less than' operator.
__bdd	bdd_ite (const bdd &f, const bdd &g, const bdd &h)
	If-Then-Else operator.
__bdd	bdd_ite (const exec_policy &ep, const bdd &f, const bdd &g, const bdd &h)
	If-Then-Else operator.
__bdd	bdd_restrict (const bdd &f, bdd::label_type var, bool val)
	Restrict a single variable to a constant value.
__bdd	bdd_restrict (const exec_policy &ep, const bdd &f, bdd::label_type var, bool val)
	Restrict a single variable to a constant value.
__bdd	bdd_restrict (const bdd &f, const generator< pair< bdd::label_type, bool > > &xs)
	Restrict a subset of variables to constant values.
__bdd	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	bdd_restrict (const bdd &f, ForwardIt begin, ForwardIt end)
	Restrict a subset of variables to constant values.
template<typename ForwardIt >
__bdd	bdd_restrict (const exec_policy &ep, const bdd &f, ForwardIt begin, ForwardIt end)
	Restrict a subset of variables to constant values.
__bdd	bdd_low (const bdd &f)
	Restrict the root to false, i.e. follow its low edge.
__bdd	bdd_low (const exec_policy &ep, const bdd &f)
	Restrict the root to false, i.e. follow its low edge.
__bdd	bdd_high (const bdd &f)
	Restrict the root to true, i.e. follow its high edge.
__bdd	bdd_high (const exec_policy &ep, const bdd &f)
	Restrict the root to true, i.e. follow its high edge.
__bdd	bdd_exists (const bdd &f, bdd::label_type var)
	Existential quantification of a single variable.
__bdd	bdd_exists (const exec_policy &ep, const bdd &f, bdd::label_type var)
	Existential quantification of a single variable.
__bdd	bdd_exists (const bdd &f, const predicate< bdd::label_type > &vars)
	Existential quantification of multiple variables.
__bdd	bdd_exists (const exec_policy &ep, const bdd &f, const predicate< bdd::label_type > &vars)
	Existential quantification of multiple variables.
__bdd	bdd_exists (const bdd &f, const generator< bdd::label_type > &vars)
	Existential quantification of multiple variables.
__bdd	bdd_exists (const exec_policy &ep, const bdd &f, const generator< bdd::label_type > &vars)
	Existential quantification of multiple variables.
template<typename ForwardIt >
__bdd	bdd_exists (const bdd &f, ForwardIt begin, ForwardIt end)
	Existential quantification of multiple variables.
template<typename ForwardIt >
__bdd	bdd_exists (const exec_policy &ep, const bdd &f, ForwardIt begin, ForwardIt end)
	Existential quantification of multiple variables.
__bdd	bdd_forall (const bdd &f, bdd::label_type var)
	Forall quantification of a single variable.
__bdd	bdd_forall (const exec_policy &ep, const bdd &f, bdd::label_type var)
	Forall quantification of a single variable.
__bdd	bdd_forall (const bdd &f, const predicate< bdd::label_type > &vars)
	Forall quantification of multiple variables.
__bdd	bdd_forall (const exec_policy &ep, const bdd &f, const predicate< bdd::label_type > &vars)
	Forall quantification of multiple variables.
__bdd	bdd_forall (const bdd &f, const generator< bdd::label_type > &vars)
	Forall quantification of multiple variables.
__bdd	bdd_forall (const exec_policy &ep, const bdd &f, const generator< bdd::label_type > &vars)
	Forall quantification of multiple variables.
template<typename ForwardIt >
__bdd	bdd_forall (const bdd &f, ForwardIt begin, ForwardIt end)
	Forall quantification of multiple variables.
template<typename ForwardIt >
__bdd	bdd_forall (const exec_policy &ep, const bdd &f, ForwardIt begin, ForwardIt end)
	Forall quantification of multiple variables.
__zdd	zdd_binop (const zdd &A, const zdd &B, const predicate< bool, bool > &op)
	Apply a binary operator between the sets of two families.
__zdd	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	zdd_union (const zdd &A, const zdd &B)
	The union of two families of sets.
__zdd	zdd_union (const exec_policy &ep, const zdd &A, const zdd &B)
	The union of two families of sets.
__zdd	operator| (const zdd &lhs, const zdd &rhs)
zdd	operator+ (const zdd &A)
__zdd	operator+ (const zdd &lhs, const zdd &rhs)
__zdd	zdd_intsec (const zdd &A, const zdd &B)
	The intersection of two families of sets.
__zdd	zdd_intsec (const exec_policy &ep, const zdd &A, const zdd &B)
	The intersection of two families of sets.
__zdd	operator& (const zdd &lhs, const zdd &rhs)
__zdd	operator* (const zdd &lhs, const zdd &rhs)
__zdd	zdd_diff (const zdd &A, const zdd &B)
	The set difference of two families of sets.
__zdd	zdd_diff (const exec_policy &ep, const zdd &A, const zdd &B)
	The set difference of two families of sets.
__zdd	operator- (const zdd &A)
__zdd	operator- (const zdd &lhs, const zdd &rhs)
__zdd	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	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	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	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	zdd_complement (const zdd &A, const generator< zdd::label_type > &dom)
	Complement of A within the given domain.
__zdd	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	zdd_complement (const zdd &A, ForwardIt begin, ForwardIt end)
	Complement of A within the given domain.
template<typename ForwardIt >
__zdd	zdd_complement (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Complement of A within the given domain.
__zdd	zdd_complement (const zdd &A)
	Complement of A within the global Variable Domain.
__zdd	zdd_complement (const exec_policy &ep, const zdd &A)
	Complement of A within the global Variable Domain.
__zdd	operator~ (const zdd &A)
__zdd	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	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	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	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	zdd_offset (const zdd &A, zdd::label_type var)
	Subset that do not include the given element.
__zdd	zdd_offset (const exec_policy &ep, const zdd &A, zdd::label_type var)
	Subset that do not include the given element.
__zdd	zdd_offset (const zdd &A)
	Subset that do not include the top variable.
__zdd	zdd_offset (const exec_policy &ep, const zdd &A)
	Subset that do not include the top variable.
__zdd	zdd_offset (const zdd &A, const generator< zdd::label_type > &vars)
	Subset that do not include the given set of variables.
__zdd	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	zdd_offset (const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do not include the given set of variables.
template<typename ForwardIt >
__zdd	zdd_offset (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do not include the given set of variables.
__zdd	zdd_onset (const zdd &A, zdd::label_type var)
	Subset that do include the given element.
__zdd	zdd_onset (const exec_policy &ep, const zdd &A, zdd::label_type var)
	Subset that do include the given element.
__zdd	zdd_onset (const zdd &A)
	Subset that do include the top variable.
__zdd	zdd_onset (const exec_policy &ep, const zdd &A)
	Subset that do include the top variable.
__zdd	zdd_onset (const zdd &A, const generator< zdd::label_type > &vars)
	Subset that do include the given set of variables.
__zdd	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	zdd_onset (const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do include the given set of variables.
template<typename ForwardIt >
__zdd	zdd_onset (const exec_policy &ep, const zdd &A, ForwardIt begin, ForwardIt end)
	Subset that do include the given set of variables.
__zdd	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	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	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	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	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	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	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	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	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	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	bdd_relprod (const bdd &states, const bdd &relation, const predicate< bdd::label_type > &pred)
	Relational Product of states and a relation.
bdd	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	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	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	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	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	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	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	bdd_relnext (const bdd &states, const bdd &relation)
	Forwards step with the Relational Product for interleaved variable orderings, including relabelling.
bdd	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	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	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	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	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	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	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	bdd_relprev (const bdd &states, const bdd &relation)
	Backwards step with the Relational Product for interleaved variable orderings, including relabelling.
bdd	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	bdd_iscanonical (const bdd &f)
	Check whether a BDD is canonical.
bool	bdd_isconst (const bdd &f)
	Whether a BDD is a constant.
bool	bdd_isterminal (const bdd &f)
	Whether a BDD is a constant (terminal).
bool	bdd_isfalse (const bdd &f)
	Whether a BDD is the constant false.
bool	bdd_istrue (const bdd &f)
	Whether a BDD is the constant true.
bool	bdd_isvar (const bdd &f)
	Whether a BDD is a function dependent on a single variable, i.e. is a literal.
bool	bdd_isithvar (const bdd &f)
	Whether a BDD is the function of a single positive variable.
bool	bdd_isnithvar (const bdd &f)
	Whether a BDD is the function of a single negative variable.
bool	bdd_iscube (const bdd &f)
	Whether a BDD represents a cube.
bool	bdd_equal (const bdd &f, const bdd &g)
	Whether the two BDDs represent the same function.
bool	bdd_equal (const exec_policy &, const bdd &f, const bdd &g)
	Whether the two BDDs represent the same function.
bool	operator== (const bdd &f, const bdd &g)
bool	bdd_unequal (const bdd &f, const bdd &g)
	Whether the two BDDs represent different functions.
bool	bdd_unequal (const exec_policy &ep, const bdd &f, const bdd &g)
	Whether the two BDDs represent different functions.
bool	operator!= (const bdd &f, const bdd &g)
bool	zdd_iscanonical (const zdd &A)
	Check whether a given ZDD is canonical.
bool	zdd_isterminal (const zdd &A)
	Whether this ZDD represents a terminal.
bool	zdd_isfalse (const zdd &A)
	Whether this ZDD represents false terminal.
bool	zdd_isempty (const zdd &A)
	Whether it is the empty family, i.e. Ø .
bool	zdd_istrue (const zdd &A)
	Whether this BDD represents true terminal.
bool	zdd_isnull (const zdd &A)
	Whether it is the null family, i.e. { Ø } .
bool	zdd_ispoint (const zdd &A)
	Whether it contains a single bit-vector a, i.e. A = { a }.
bool	zdd_equal (const zdd &A, const zdd &B)
	Whether they represent the same family.
bool	zdd_equal (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether they represent the same family.
bool	operator== (const zdd &lhs, const zdd &rhs)
bool	zdd_unequal (const zdd &A, const zdd &B)
	Whether they represent two different families.
bool	zdd_unequal (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether they represent two different families.
bool	operator!= (const zdd &lhs, const zdd &rhs)
bool	zdd_subseteq (const zdd &A, const zdd &B)
	Whether one family is a subset or equal to the other.
bool	zdd_subseteq (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether one family is a subset or equal to the other.
bool	operator<= (const zdd &lhs, const zdd &rhs)
bool	operator>= (const zdd &lhs, const zdd &rhs)
bool	zdd_subset (const zdd &A, const zdd &B)
	Whether one family is a strict subset of the other.
bool	zdd_subset (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether one family is a strict subset of the other.
bool	operator< (const zdd &lhs, const zdd &rhs)
bool	operator> (const zdd &lhs, const zdd &rhs)
bool	zdd_disjoint (const zdd &A, const zdd &B)
	Whether the two families are disjoint.
bool	zdd_disjoint (const exec_policy &ep, const zdd &A, const zdd &B)
	Whether the two families are disjoint.
Counting Operations
size_t	bdd_nodecount (const bdd &f)
	The number of (internal) nodes used to represent the function.
bdd::label_type	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	bdd_pathcount (const bdd &f)
	Count all unique (but not necessarily disjoint) paths to the true terminal.
uint64_t	bdd_pathcount (const exec_policy &ep, const bdd &f)
	Count all unique (but not necessarily disjoint) paths to the true terminal.
uint64_t	bdd_satcount (const bdd &f, bdd::label_type varcount)
	Count the number of assignments x that make f(x) true.
uint64_t	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	bdd_satcount (const bdd &f)
	Count the number of assignments x that make f(x) true.
uint64_t	bdd_satcount (const exec_policy &ep, const bdd &f)
	Count the number of assignments *x that make f(x) true.
size_t	zdd_nodecount (const zdd &A)
	The number of (internal) nodes used to represent the family of sets.
zdd::label_type	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	zdd_size (const zdd &A)
	The number of sets in the family of sets.
uint64_t	zdd_size (const exec_policy &ep, const zdd &A)
	The number of sets in the family of sets.
Input Variables
void	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	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	bdd_topvar (const bdd &f)
	Get the root's variable label.
bdd::label_type	bdd_minvar (const bdd &f)
	Get the minimal occurring variable in the function's support.
bdd::label_type	bdd_maxvar (const bdd &f)
	Get the maximal occurring variable in the function's support.
bdd	bdd_satmin (const bdd &f)
	The lexicographically smallest cube x such that f(x) is true.
bdd	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	bdd_satmin (const bdd &f, ForwardIt cbegin, ForwardIt cend)
	The lexicographically smallest x such that f(x) is true.
bdd	bdd_satmin (const bdd &f, const bdd &d)
	The lexicographically smallest x such that f(x) is true.
void	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	bdd_satmin (const bdd &f, OutputIt iter)
	The lexicographically smallest x such that f(x) is true.
bdd	bdd_satmax (const bdd &f)
	The lexicographically largest cube x such that f(x) is true.
bdd	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	bdd_satmax (const bdd &f, ForwardIt cbegin, ForwardIt cend)
	The lexicographically largest x such that f(x) is true.
bdd	bdd_satmax (const bdd &f, const bdd &d)
	The lexicographically largest x such that f(x) is true.
void	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	bdd_satmax (const bdd &f, OutputIt iter)
	The lexicographically largest x such that f(x) is true.
pair< bdd, double >	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 >	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	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	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	bdd_eval (const bdd &f, const predicate< bdd::label_type > &xs)
	Evaluate a BDD according to an assignment to its variables.
bool	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	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	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	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	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	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	bdd_from (const zdd &A)
	Obtains the BDD that represents the same function/set as the given ZDD within the global domain.
__bdd	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	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	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	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	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	zdd_from (const bdd &f)
	Obtains the ZDD that represents the same function/set as the given BDD within the global Variable Domain.
__zdd	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	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	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	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	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.
Set Elements
void	zdd_support (const zdd &A, const consumer< zdd::label_type > &cb)
	Get (in ascending order) all of the variable labels that occur in the family.
template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
OutputIt	zdd_support (const zdd &A, OutputIt iter)
	Copy all of the variable labels (in ascending order) that occur in the family into the given container.
zdd::label_type	zdd_topvar (const zdd &f)
	Get the root's variable label.
zdd::label_type	zdd_minvar (const zdd &A)
	Get the minimal occurring variable in the family.
zdd::label_type	zdd_maxvar (const zdd &A)
	Get the maximal occurring variable in the family.
bool	zdd_contains (const zdd &A, const generator< zdd::label_type > &a)
	Whether the family includes the given set of labels.
template<typename ForwardIt >
bool	zdd_contains (const zdd &A, ForwardIt begin, ForwardIt end)
	Whether the family includes the given set of labels.
zdd	zdd_minelem (const zdd &A)
	Retrieves the lexicographically smallest set a in A.
void	zdd_minelem (const zdd &A, const consumer< zdd::label_type > &cb)
	Retrieves the lexicographically smallest set a in A.
template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
OutputIt	zdd_minelem (const zdd &A, OutputIt iter)
	Retrieves the lexicographically smallest set a in A.
zdd	zdd_maxelem (const zdd &A)
	Retrieves the lexicographically largest set a in A.
void	zdd_maxelem (const zdd &A, const consumer< zdd::label_type > &cb)
	Retrieves the lexicographically largest set a in A.
template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<zdd::label_type>>>>
OutputIt	zdd_maxelem (const zdd &A, OutputIt iter)
	Retrieves the lexicographically largest set a in A.

Variables
const predicate< bool, bool >	and_op = [](const bool a, const bool b) -> bool { return a & b; }
	Logical 'and' operator, i.e. the truth table: [1,0,0,0].
const predicate< bool, bool >	nand_op = [](const bool a, const bool b) -> bool { return !(a & b); }
	Logical 'not and' operator, i.e. the truth table: [0,1,1,1].
const predicate< bool, bool >	or_op = [](const bool a, const bool b) -> bool { return a | b; }
	Logical 'or' operator, i.e. the truth table: [1,1,1,0].
const predicate< bool, bool >	nor_op = [](const bool a, const bool b) -> bool { return !(a | b); }
	Logical 'not or' operator, i.e. the truth table: [0,0,0,1].
const predicate< bool, bool >	xor_op = [](const bool a, const bool b) -> bool { return a ^ b; }
	Logical 'xor' operator, i.e. the truth table: [0,1,1,0].
const predicate< bool, bool >	xnor_op = [](const bool a, const bool b) -> bool { return a == b; }
	Logical 'xor' operator, i.e. the truth table: [1,0,0,1].
const predicate< bool, bool >	imp_op = [](const bool a, const bool b) -> bool { return a <= b; }
	Logical 'implication' operator, i.e. the truth table: [1,0,1,1].
const predicate< bool, bool >	invimp_op = [](const bool a, const bool b) -> bool { return b <= a; }
	Logical 'implication' operator, i.e. the truth table: [1,1,0,1].
const predicate< bool, bool >	equiv_op = xnor_op
	Logical 'equivalence' operator, i.e. the 'xnor' operator.
const predicate< bool, bool >	diff_op
	Logical 'set difference' operator, i.e. the truth table [0,1,0,0].
const predicate< bool, bool >	less_op = [](const bool a, const bool b) -> bool { return a < b; }
	Logical 'less' operator, i.e. the truth table [0,0,1,0].
constexpr domain_var	domain_max = internal::node::max_label
	The maximum supported domain variable.
template<typename A , typename B >
constexpr bool	is_convertible = std::is_convertible<A, B>::value
template<typename A , typename B >
constexpr bool	is_same = std::is_same<A, B>::value
template<typename A , typename B >
constexpr bool	needs_conversion = !is_same<A, B> && is_convertible<A, B>
template<typename A >
constexpr bool	is_const = std::is_const<std::remove_reference_t<A>>::value
template<typename A >
constexpr bool	is_mutable = !is_const<A>
template<typename A >
constexpr bool	is_integral = std::is_integral<A>::value
template<typename A >
constexpr bool	is_void = std::is_void<A>::value
Version Number
constexpr unsigned short	version_major = 2
	Major version of Adiar.
constexpr unsigned short	version_minor = 1
	Minor version of Adiar.
constexpr unsigned short	version_patch = 0
	Patch version of Adiar.
constexpr unsigned short	version = (version_major * 10'000) + (version_minor*100) + version_patch
	Combined version number of Adiar into a single integer.
constexpr std::string_view	version_string = "2.1.0"
	A pre-formatted string for version of the Adiar version.

Function Objects
To bridge the gap between your algorithms and their data structures and the algorithms of Adiar, we use the abstract notion of predicate, consumer, and generator functions.
template<typename TypeSignature >
using	function = std::function< TypeSignature >
	General-purpose polymorphic function wrapper.
template<typename... Args>
using	predicate = function< bool(Args...)>
	Predicate function given value(s) of type(s) Args.
template<typename Arg >
using	consumer = function< void(Arg)>
	Consumer function of value of type Arg.
template<typename VarType >
using	cost = function< double(VarType)>
	Cost function that assigns a cost to each variable.
template<typename RetType >
using	generator = function< optional< RetType >()>
	Generator function that produces a new value of RetType for each call.
template<typename ValueType , typename OutputIt >
consumer< ValueType >	make_consumer (OutputIt &&iter)
	Wrap an iterator into a consumer function.
template<typename OutputIt , typename = enable_if<!is_void< typename std::iterator_traits<std::remove_reference_t<OutputIt>>::value_type>>>
consumer< typename std::iterator_traits< std::remove_reference_t< OutputIt > >::value_type >	make_consumer (OutputIt &&iter)
	Wrap an iterator into a consumer function.
template<typename OutputIt , typename = enable_if<is_void< typename std::iterator_traits<std::remove_reference_t<OutputIt>>::value_type>>>
consumer< typename std::remove_reference_t< OutputIt >::container_type::value_type >	make_consumer (OutputIt &&iter)
	Wrap an insertion iterator into a consumer function.
template<typename ForwardIt >
consumer< typename ForwardIt::value_type >	make_consumer (ForwardIt &begin, ForwardIt &end)
	Wrap a begin and end iterator pair into a consumer function.
template<typename ForwardIt >
consumer< typename std::iterator_traits< std::remove_reference_t< ForwardIt > >::value_type >	make_consumer (ForwardIt &&begin, ForwardIt &&end)
	Wrap a begin and end iterator pair into a consumer function.
template<typename ForwardIt >
generator< typename std::remove_reference_t< ForwardIt >::value_type >	make_generator (ForwardIt &&begin, ForwardIt &&end)
	Wrap a begin and end iterator pair into a generator function.
template<typename Stream >
generator< typename Stream::value_type >	make_generator (Stream &s)
	Wrap an adiar::internal::ifstream into a generator function.
template<typename RetType >
generator< RetType >	make_generator (const RetType &r)
	Wrap a single value into a generator.

Package Initialisation
After having linked the C++ source file with Adiar, one needs to include the <adiar/adiar.h> header, initialise the library before using any of its data structures, and finally remember to deinitialise the library again before the program terminates.
constexpr size_t	minimum_memory = 128 * 1024 * 1024
	Minimum value of 128 MiB for the memory limit.
void	adiar_init (size_t memory_limit_bytes, std::string temp_dir="")
	Initiates Adiar with the given amount of memory (given in bytes)
bool	adiar_initialized () noexcept
	Whether Adiar is initialized.
void	adiar_deinit ()
	Closes and cleans up everything by Adiar.

Detailed Description

Core types.

Global Domain Decision Diagrams Statistics Deprecated Functions

Typedef Documentation

optional

template<typename T >

using adiar::optional = typedef std::optional<T>

An optional value, i.e. a possibly existent value.

Not having a value is for example used to indicate the end of streams and generators.

Enumeration Type Documentation

assignment

enum class adiar::assignment : signed char

strong

Possible values to assign a variable.

Enumerator
False	Assigning to false.
True	Assigning to true.
None	Assigning to no value (i.e. both true and false are valid).

replace_type

enum class adiar::replace_type : signed char

strong

Possible guarantees of a variable permutation/remapping m of type int -> int.

The ordering on the values of replace_type reflect the strength of the guarantee. For example, replace_type::Affine < replace_type::Monotone since any affine function is also monotone.

See also

bdd_replace

Enumerator
Non_Monotone	Any variable remapping without any guarantees on m.
Monotone	For any x < y then the mapped values preserve that order, i.e. m(x) < m(y).
Shift	(faster version of 'Monotone'): m(x) = x + b for an integer b.
Identity	Nothing needs to be done, as m(x) = x.

Variable Documentation

diff_op

const predicate<bool, bool> adiar::diff_op

Initial value:

= [](const bool a, const bool b) -> bool {
    
    return a & !b;
  }

Logical 'set difference' operator, i.e. the truth table [0,1,0,0].