Adiar  2.1.0
An External Memory Decision Diagram Library
adiar Namespace Reference

Core types. More...

Classes

class  exec_policy
 Settings to dictate the execution of Adiar's algorithms. More...
 
class  __bdd
 A (possibly) unreduced Binary Decision Diagram. More...
 
class  bdd
 A reduced Binary Decision Diagram. More...
 
class  __zdd
 A (possibly unreduced) Zero-suppressed Decision Diagram. More...
 
class  zdd
 Reduced Ordered Zero-suppressed 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...
 
struct  statistics
 Available statistics from algorithm's and data structures. More...
 

Typedefs

using bdd_ptr = builder_ptr< bdd_policy >
 Pointer for a BDD node created by a BDD builder. More...
 
using zdd_ptr = builder_ptr< zdd_policy >
 Pointer for a ZDD node created by a ZDD builder. More...
 
using bdd_builder = builder< bdd_policy >
 Builder for BDDs. More...
 
using zdd_builder = builder< zdd_policy >
 Builder for ZDDs. More...
 
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. More...
 
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::accessexec_policy::get< exec_policy::access > () const
 Chosen access mode.
 
template<>
const exec_policy::memoryexec_policy::get< exec_policy::memory > () const
 Chosen memory type.
 
template<>
const exec_policy::quantify::algorithmexec_policy::get< exec_policy::quantify::algorithm > () const
 Chosen quantification strategy.
 
template<>
const exec_policy::quantify::transposition_growthexec_policy::get< exec_policy::quantify::transposition_growth > () const
 Chosen quantification strategy.
 
template<>
const exec_policy::quantify::transposition_maxexec_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. More...
 
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. More...
 
void domain_set (const internal::shared_file< domain_var > &dom)
 Set the domain globally for all of Adiar. More...
 
void domain_unset ()
 Removes any globally shared domain variables (if any). More...
 
bool domain_isset ()
 Whether Adiar has a global domain.
 
internal::shared_file< domain_vardomain_get ()
 Returns the global domain. More...
 
domain_var domain_size ()
 The size of the domain. More...
 
statistics statistics_get ()
 Obtain a copy of all statistics gathered. More...
 
void statistics_print (std::ostream &o=std::cout)
 Print statistics to an output stream (default std::cout). More...
 
void statistics_reset ()
 Resets all statistics to default value. More...
 
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 BDD Constructors

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

bdd bdd_const (bool value)
 The BDD representing the given constant value. More...
 
bdd bdd_terminal (bool value)
 The BDD representing the given constant value. More...
 
bdd bdd_false ()
 The BDD representing the constant false. More...
 
bdd bdd_bot ()
 The bottom of the powerset lattice. More...
 
bdd bdd_true ()
 The BDD representing the constant true. More...
 
bdd bdd_top ()
 The top of the powerset lattice. More...
 
bdd bdd_ithvar (bdd::label_type var)
 The BDD representing the i'th variable. More...
 
bdd bdd_nithvar (bdd::label_type var)
 The BDD representing the negation of the i'th variable. More...
 
bdd bdd_and (const generator< int > &vars)
 The BDD representing the logical 'and' of all the given variables, i.e. a term of variables. More...
 
bdd bdd_and (const generator< pair< bdd::label_type, bool >> &vars)
 The BDD representing the logical 'and' of all the given variables, i.e. a term of variables. More...
 
template<typename ForwardIt , typename = enable_if<!is_convertible<ForwardIt, bdd>>>
bdd bdd_and (ForwardIt begin, ForwardIt end)
 The BDD representing the logical 'and' of all the given variables, i.e. a term of variables. More...
 
bdd bdd_or (const generator< int > &vars)
 The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables. More...
 
bdd bdd_or (const generator< pair< bdd::label_type, bool >> &vars)
 The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables. More...
 
template<typename ForwardIt , typename = enable_if<!is_convertible<ForwardIt, bdd>>>
bdd bdd_or (ForwardIt begin, ForwardIt end)
 The BDD representing the logical 'or' of all the given variables, i.e. a clause of variables. More...
 
bdd bdd_cube (const generator< int > &vars)
 The BDD representing the cube of all the given variables. More...
 
bdd bdd_cube (const generator< pair< bdd::label_type, bool >> &vars)
 The BDD representing the cube of all the given variables. More...
 
template<typename ForwardIt >
bdd bdd_cube (ForwardIt begin, ForwardIt end)
 The BDD representing the cube of all the given variables. More...
 
Basic BDD Manipulation
bdd bdd_not (const bdd &f)
 Negation of a BDD. More...
 
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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
template<typename ForwardIt >
__bdd bdd_forall (const exec_policy &ep, const bdd &f, ForwardIt begin, ForwardIt end)
 Forall quantification of multiple variables.
 
bdd bdd_relprod (const bdd &states, const bdd &relation, const predicate< bdd::label_type > &pred)
 Relational Product of states and a relation. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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.
 
BDD Predicates
bool bdd_iscanonical (const bdd &f)
 Check whether a BDD is canonical. More...
 
bool bdd_isconst (const bdd &f)
 Whether a BDD is a constant. More...
 
bool bdd_isterminal (const bdd &f)
 Whether a BDD is a constant (terminal). More...
 
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. More...
 
bool bdd_isithvar (const bdd &f)
 Whether a BDD is the function of a single positive variable. More...
 
bool bdd_isnithvar (const bdd &f)
 Whether a BDD is the function of a single negative variable. More...
 
bool bdd_iscube (const bdd &f)
 Whether a BDD represents a cube. More...
 
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. More...
 
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)
 
BDD 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 f, i.e. the number of levels in the BDD.
 
uint64_t bdd_pathcount (const bdd &f)
 Count all unique (but not necessarily disjoint) paths to the true terminal. More...
 
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. More...
 
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. More...
 
uint64_t bdd_satcount (const exec_policy &ep, const bdd &f)
 Count the number of assignments *x that make f(x) true.
 
Input Variables
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. More...
 
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. More...
 
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.
 
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. More...
 
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. More...
 
bdd::label_type bdd_topvar (const bdd &f)
 Get the root's variable label. More...
 
bdd::label_type bdd_minvar (const bdd &f)
 Get the minimal occurring variable in the function's support. More...
 
bdd::label_type bdd_maxvar (const bdd &f)
 Get the maximal occurring variable in the function's support. More...
 
bdd bdd_satmin (const bdd &f)
 The lexicographically smallest cube x such that f(x) is true. More...
 
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. More...
 
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. More...
 
bdd bdd_satmin (const bdd &f, const bdd &d)
 The lexicographically smallest x such that f(x) is true. More...
 
void bdd_satmin (const bdd &f, const consumer< pair< bdd::label_type, bool >> &c)
 The lexicographically smallest x such that f(x) is true. More...
 
template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>> && !is_convertible<OutputIt, bdd>>>
OutputIt bdd_satmin (const bdd &f, OutputIt iter)
 The lexicographically smallest x such that f(x) is true. More...
 
bdd bdd_satmax (const bdd &f)
 The lexicographically largest cube x such that f(x) is true. More...
 
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. More...
 
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. More...
 
bdd bdd_satmax (const bdd &f, const bdd &d)
 The lexicographically largest x such that f(x) is true. More...
 
void bdd_satmax (const bdd &f, const consumer< pair< bdd::label_type, bool >> &c)
 The lexicographically largest x such that f(x) is true. More...
 
template<typename OutputIt , typename = enable_if<!is_convertible<OutputIt, consumer<pair<bdd::label_type, bool>>> && !is_convertible<OutputIt, bdd>>>
OutputIt bdd_satmax (const bdd &f, OutputIt iter)
 The lexicographically largest x such that f(x) is true. More...
 
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. More...
 
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. More...
 
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. More...
 
bool bdd_eval (const bdd &f, const generator< pair< bdd::label_type, bool >> &xs)
 Evaluate a BDD according to an assignment to its variables. More...
 
template<typename ForwardIt >
bool bdd_eval (const bdd &f, ForwardIt begin, ForwardIt end)
 Evaluate a BDD according to an assignment to its variables. More...
 
Conversion to BDDs
__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. More...
 
__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. More...
 
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. More...
 
__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.
 
DOT Files of BDDs
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.
 
Basic ZDD Constructors

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

zdd zdd_terminal (bool value)
 The ZDD of only a single terminal. More...
 
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. More...
 
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. More...
 
zdd zdd_ithvar (zdd::label_type var)
 The set of bitvectors over the globally set domain where var is set to true. More...
 
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. More...
 
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. More...
 
zdd zdd_nithvar (zdd::label_type var)
 The set of bitvectors over the globally set domain where var is set to false. More...
 
zdd zdd_vars (const generator< zdd::label_type > &vars)
 The family { { 1, 2, ..., k } }. More...
 
template<typename ForwardIt >
zdd zdd_vars (ForwardIt begin, ForwardIt end)
 The family { { 1, 2, ..., k } }. More...
 
zdd zdd_point (const generator< zdd::label_type > &vars)
 The family { { 1, 2, ..., k } } with a single bit-vector. More...
 
template<typename ForwardIt >
zdd zdd_point (ForwardIt begin, ForwardIt end)
 The family { { 1, 2, ..., k } } with a single bit-vector. More...
 
zdd zdd_singleton (zdd::label_type var)
 The family { {i} } . More...
 
zdd zdd_singletons (const generator< zdd::label_type > &vars)
 The family { {1}, {2}, ..., {k} }. More...
 
template<typename ForwardIt >
zdd zdd_singletons (ForwardIt begin, ForwardIt end)
 The family { {1}, {2}, ..., {k} }. More...
 
zdd zdd_powerset (const generator< zdd::label_type > &vars)
 The powerset of all given variables. More...
 
template<typename ForwardIt >
zdd zdd_powerset (ForwardIt begin, ForwardIt end)
 The powerset of all given variables. More...
 
zdd zdd_bot (const generator< zdd::label_type > &dom)
 Bottom of the powerset lattice. More...
 
template<typename ForwardIt >
zdd zdd_bot (ForwardIt begin, ForwardIt end)
 Bottom of the powerset lattice. More...
 
zdd zdd_bot ()
 Bottom of the powerset lattice. More...
 
zdd zdd_top (const generator< zdd::label_type > &dom)
 Top of the powerset lattice. More...
 
template<typename ForwardIt >
zdd zdd_top (ForwardIt begin, ForwardIt end)
 Top of the powerset lattice. More...
 
zdd zdd_top ()
 Top of the powerset lattice. More...
 
Basic ZDD Manipulation
__zdd zdd_binop (const zdd &A, const zdd &B, const predicate< bool, bool > &op)
 Apply a binary operator between the sets of two families. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
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. More...
 
__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. More...
 
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. More...
 
__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. More...
 
__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. More...
 
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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
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. More...
 
__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. More...
 
__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. More...
 
__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. More...
 
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. More...
 
__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. More...
 
__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. More...
 
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.
 
ZDD Predicates
bool zdd_iscanonical (const zdd &A)
 Check whether a given ZDD is canonical. More...
 
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.
 
ZDD Counting Operations
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 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.
 
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. More...
 
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. More...
 
zdd::label_type zdd_topvar (const zdd &f)
 Get the root's variable label. More...
 
zdd::label_type zdd_minvar (const zdd &A)
 Get the minimal occurring variable in the family. More...
 
zdd::label_type zdd_maxvar (const zdd &A)
 Get the maximal occurring variable in the family. More...
 
bool zdd_contains (const zdd &A, const generator< zdd::label_type > &a)
 Whether the family includes the given set of labels. More...
 
template<typename ForwardIt >
bool zdd_contains (const zdd &A, ForwardIt begin, ForwardIt end)
 Whether the family includes the given set of labels. More...
 
zdd zdd_minelem (const zdd &A)
 Retrieves the lexicographically smallest set a in A. More...
 
void zdd_minelem (const zdd &A, const consumer< zdd::label_type > &cb)
 Retrieves the lexicographically smallest set a in A. More...
 
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. More...
 
zdd zdd_maxelem (const zdd &A)
 Retrieves the lexicographically largest set a in A. More...
 
void zdd_maxelem (const zdd &A, const consumer< zdd::label_type > &cb)
 Retrieves the lexicographically largest set a in A. More...
 
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. More...
 
Conversion to ZDDs
__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. More...
 
__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. More...
 
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. More...
 
__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 of ZDDs
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.
 

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]. More...
 
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
 
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. More...
 
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. More...
 
template<typename... Args>
using predicate = function< bool(Args...)>
 Predicate function given value(s) of type(s) Args. More...
 
template<typename Arg >
using consumer = function< void(Arg)>
 Consumer function of value(s) of type(s) Args. More...
 
template<typename VarType >
using cost = function< double(VarType)>
 Cost function that assigns a cost to each variable. More...
 
template<typename RetType >
using generator = function< optional< RetType >()>
 Generator function that produces a new value of RetType for each call. More...
 
template<typename ValueType , typename OutputIt >
consumer< ValueType > make_consumer (OutputIt &iter)
 Wrap an iterator into a consumer function.
 
template<typename ValueType , typename OutputIt >
consumer< ValueType > make_consumer (OutputIt &&iter)
 Wrap an iterator into a consumer function.
 
template<typename OutputIt >
consumer< typename OutputIt::container_type::value_type > make_consumer (OutputIt &iter)
 Wrap an iterator into a consumer function.
 
template<typename OutputIt >
consumer< typename OutputIt::container_type::value_type > make_consumer (OutputIt &&iter)
 Wrap an 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. More...
 
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. More...
 
template<typename ForwardIt >
generator< typename ForwardIt::value_type > make_generator (ForwardIt &begin, ForwardIt &end)
 Wrap a begin and end iterator pair into a generator function.
 
template<typename ForwardIt >
generator< typename 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::file_stream 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) More...
 
bool adiar_initialized () noexcept
 Whether Adiar is initialized.
 
void adiar_deinit ()
 Closes and cleans up everything by Adiar. More...
 

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