adiar::exec_policy Class Reference

Settings to dictate the execution of Adiar's algorithms. More...

#include <adiar/exec_policy.h>

Classes
class	quantify
	Strategies and settings for Adiar to use in quantify/project algorithms. More...

Public Types
enum class	access : char { Auto , Random_Access , Priority_Queue }
	Whether Adiar should exclusively use random access or priority queues or automatically pick either way based on the width of inputs. More...
enum class	memory : char { Auto , Internal , External }
	Whether Adiar should exclusively use internal or external memory or automatically pick either type based on size of input. More...

Public Member Functions
	exec_policy ()=default
	Default constructor with all options set to their default value.
	exec_policy (const exec_policy &)=default
	Copy constructor.
	exec_policy (exec_policy &&)=default
	Move constructor.
	exec_policy (const access &am)
	Conversion construction from access enum.
	exec_policy (const memory &mm)
	Conversion construction from memory enum.
	exec_policy (const quantify::algorithm &qa)
	Conversion construction from quantify enum.
	exec_policy (const quantify::transposition_growth &tg)
	Conversion construction from quantify transposition growth value.
	exec_policy (const quantify::transposition_max &tm)
	Conversion construction from quantify transposition max runs value.
exec_policy &	operator= (const exec_policy &)=default
	Copy assignment.
exec_policy &	operator= (exec_policy &&)=default
	Move assignment.
template<typename T >
const T &	get () const
	Obtain a value.
bool	operator== (const exec_policy &ep) const
	Check for equality of settings.
bool	operator!= (const exec_policy &ep) const
	Check for at least one mismatch in the settings.
exec_policy &	set (const access &am)
	Set the access mode.
exec_policy	operator& (const access &am) const
	Create a copy with the access mode changed.
exec_policy &	set (const memory &mm)
	Set the memory mode.
exec_policy	operator& (const memory &mm) const
	Create a copy with the memory mode changed.
exec_policy &	set (const quantify::algorithm &qa)
	Set the quantify algorithm.
exec_policy	operator& (const quantify::algorithm &qa) const
	Create a copy with the quantify algorithm changed.
exec_policy &	set (const quantify::transposition_growth &tg)
	Set the quantify strategy.
exec_policy	operator& (const quantify::transposition_growth &tg) const
	Create a copy with the quantify algorithm changed.
exec_policy &	set (const quantify::transposition_max &tm)
	Set the quantify strategy.
exec_policy	operator& (const quantify::transposition_max &tm) const
	Create a copy with the quantify algorithm changed.

Detailed Description

Settings to dictate the execution of Adiar's algorithms.

Adiar's algorithms work very differently from other BDD implementations. Hence, it makes use of multiple novel techniques to make it competitive across the entire spectrum of BDD shapes and sizes. These can be turned on/off or tweaked by changing these settings.

Most likely, you would want to apply all techniques (in a safe way) and so you do not need to think about changing any of these.

For example, you can fix the bdd_exists to only use internal memory and the Nested Sweeping framework as follows:

bdd_exists(exec_policy::memory::Internal & exec_policy::quantify::Nested,
           f,
           vars.rbegin(), vars.rend());

Member Enumeration Documentation

access

enum adiar::exec_policy::access : char

strong

Whether Adiar should exclusively use random access or priority queues or automatically pick either way based on the width of inputs.

Adiar’s Algorithms delay recursion through use of auxiliary data structures. These auxiliary data structures are redundant when the width of one or more inputs fits in the internal memory. In these cases it is much faster to load in the entire level of a diagram and then use random access.

Note

For more details, please read "Random Access on Narrow Decision Diagrams in External Memory" SPIN 2024.

Warning

Using Random_Access may lead to crashes if all inputs are too wide or input to random access is not canonical!

See also

bdd_apply zdd_binop

Enumerator
Auto	Pick Random Access when an input is narrow enough.
Random_Access	Always use Random Access
Priority_Queue	Always use Priority Queues

memory

enum adiar::exec_policy::memory : char

strong

Whether Adiar should exclusively use internal or external memory or automatically pick either type based on size of input.

Adiar’s Algorithms delay recursion through use of auxiliary data structures. These auxiliary data structures can be optimised for internal memory, and so have a high performance on very small instances, or they can be designed for external memory such that they can handle decision diagrams much larger than the available memory.

Note

For more details, please read "Predicting Memory Demands of BDD Operations using Maximum Graph Cuts" ATVA 2023.

Warning

Using Internal may lead to crashes if an input or output is too large!

Enumerator
Auto	Pick internal memory as long as it is safe to do so.
Internal	Always use internal memory
External	Always use external memory

---

The documentation for this class was generated from the following file:

• /home/runner/work/adiar/adiar/src/adiar/exec_policy.h