diff --git a/.gitignore b/.gitignore index 0245ec3d6..d12991953 100644 --- a/.gitignore +++ b/.gitignore @@ -21,6 +21,11 @@ build/ *.dot *.png +# --------------------- +# Documentation Exceptions +!docs/*.png +!docs/**/*.png + ################################################################################ # LCOV reports *.info diff --git a/docs/cite.md b/docs/cite.md index c30d2ada3..5f5cd5032 100644 --- a/docs/cite.md +++ b/docs/cite.md @@ -1,7 +1,7 @@ --- layout: default title: Citing this project -nav_order: 7 +nav_order: 8 description: "Citations" permalink: /cite --- @@ -19,6 +19,7 @@ some of your academic work. 1. TOC {:toc} +--- ## Lars Arge diff --git a/docs/core.md b/docs/core.md deleted file mode 100644 index 36c79d293..000000000 --- a/docs/core.md +++ /dev/null @@ -1,18 +0,0 @@ ---- -layout: default -title: Core -nav_order: 5 -description: "The underlying data types and files" -permalink: /core -has_children: true ---- - -# Core -{: .no_toc } - -Most of the features of *Adiar* can be used without knowing anything about how -the underlying algorithms work. Yet, a quite a few operations involve a -*label_file* or *assignment_file*. Furthermore, an efficient manual construction -of a well structured Decision Diagrams will require direct interaction with the -underlying data types and files. -{: .fs-6 .fw-300 } diff --git a/docs/core/data_types.md b/docs/core/data_types.md deleted file mode 100644 index d99549d02..000000000 --- a/docs/core/data_types.md +++ /dev/null @@ -1,160 +0,0 @@ ---- -layout: default -title: Data types -nav_order: 1 -parent: Core -description: "The data types placed in streams" -permalink: core/data_types ---- - -# Data types -{: .no_toc } - -## Table of Contents -{: .no_toc .text-delta } - -1. TOC -{:toc} - ---- - -## Nodes - -### Identifiers and Ordering -A non-terminal node is uniquely identified by two values: its _label_ and its _id_. -The prior is the variable it represents, whereas _id_ is a unique number -specific to the number's _label_. Together they create a unique identifier _uid_ -of a node. This identifier is supposed to reflect the following total ordering. - -

- n < m ≡ n.label < m.label || (n.label = m.label && n.id < m.id) -

- -These uids can be stored within a single unsigned 64-bit integer, which then -acts as a "pointer" to the node and can be constructed as follows. - -- `uid_t create_node_uid(label_t l, id_t id)` - - Create the unique identifier for the node with label _l_ and identifier _id_. - We provide `ptr_t create_node_ptr(l, id)` as an alternative. - -One then must use the following two functions to again retrieve the label or id -from a uid. - -- `label_t label_of(uid_t u)` - -- `id_t id_of(uid_t u)` - -Here `id_t`, `uid_t`, and `ptr_t` are aliases for an unsigned 64-bit integer and -`label_t` for an unsigned 32-bit integer. The uid constructed (and the -algorithms by extension) only works as intended, if the label, resp. id, is less -or equal to `MAX_LABEL`, resp. `MAX_ID`. - -A unique identifier for a terminal is recognised by a single bit-flag within the -64-bit number of the identifer. One can create, read from, and manipulate -terminal-identifiers by using the following functions. - -- `uid_t create_terminal_uid(bool v)` - - Create the unique identifier to a terminal with a given boolean value. We also - provide `ptr_t create_terminal_ptr(v)` as an alternative. - -- `bool value_of(ptr_t p)` - - Extract the boolean value of the given terminal identifier. - -- `uid_t negate(ptr_t p)` - - Negate the value of the terminal - -One can identify whether a given `ptr_t` or `uid_t` is to a node or a terminal with -the following two predicates. - -- `bool is_node(uid_t p)` - -- `bool is_terminal(uid_t p)` - - - `bool is_false(uid_t p)` - - Shorthand for `is_terminal(p) && !value_of(p)`. - - - `bool is_true(uid_t p)` - - Shorthand for `is_terminal(p) && value_of(p)`. - -### The Node Struct - -With the above a node in _Adiar_ is the following combination of 3 unsigned -64-bit numbers - -```cpp -struct node { uid_t uid; ptr_t low; ptr_t high; }; -``` - -For which the operators `<` , `>`, `==`, and `!=` have been defined to reflect -the ordering based on the uid discussed above. For convenience, one can create a -node with the following function. - -- `node_t create_node(label_t label, id_t id, uid_t low, uid_t high)` - - Create a node, given a label and an id for the specific node, together with - the identifier for its low and high child. We also provide variants of this - function, where `low` and `high` are themselves nodes. - - The functions on uids above are also lifted to nodes - -- `label_t label_of(node_t n)` - - Extract the label from within the uid of a non-terminal node. - -- `id_t id_of(node_t n)` - - Extract the id from within the uid of a non-terminal node. - -- `node_t create_terminal(bool value)` - - Create a terminal node with a specific boolean value. - -- `bool is_terminal(node_t n)` - - Assert whether the node is a terminal node. - -- `bool value_of(node_t n)` - - Extract the value of the given terminal node. - - To evaluate whether a node *n* is specifically the *v* terminal then you may use - the `is_false(n)` and `is_true(n)` functions which are shorthand for - `is_terminal(n) && value_of(n) == v`. - -- `node_t negate(node_t n)` (operator `!`) - - Negates the content of a node. If the node is a terminal, then its value is - negated, otherwise if it has a pointer to a terminal, then that pointer is - negated. - - -## Assignments - -An assignment to a variable depends on the _label_ of the variable together with -the boolean _value_ it is assigned to. - -```cpp -struct assignment { label_t label; bool value; }; -``` - -For which the operators `<` , `>`, `==`, and `!=` have been defined to reflect -an increasiing ordering on the label. The `!` operator negates the value in the -assignment. - -- `assignment_t create_assignment(label_t label, bool value)` - - Create an assignment given a label and value. - -- `label_t label_of(assignment_t assignment)` - - Obtain the label of the variable to-be assigned a value. - -- `assignment_t create_assignment(label_t label, bool value)` - - Obtain the value to-be assigned to the variable with the label. diff --git a/docs/core/files.md b/docs/core/files.md deleted file mode 100644 index 482f922a3..000000000 --- a/docs/core/files.md +++ /dev/null @@ -1,140 +0,0 @@ ---- -layout: default -title: Files -nav_order: 2 -parent: Core -description: "Files, file streams, and file writers" -permalink: core/files ---- - -# Files -{: .no_toc } - -## Table of Contents -{: .no_toc .text-delta } - -1. TOC -{:toc} - ---- - -## Nodes - -BDDs are stored on disk with the specific ordering mentioned in Section -[Core/Data types](data_types.md#identifiers-and-ordering). If you want to -construct a BDD by hand then you have to explicitly follow this ordering; -otherwise the algorithms will have _undefined behaviour_. Yet, that is not the -whole story: In _Adiar_ a set of nodes are stored in a `node_file` in which all -these nodes are stored in _reverse_ of the ordering. - - -### Node Stream - -One can then read from a `node_file` by use of the `node_stream` class, -where the boolean template argument specifies whether the content should be -reversed (default is an in-order traversal of the nodes). This class attaches to -the `node_file` (and the [BDD](../bdd.md) wrapping class) on construction and -detaches again on deconstruction. The class provides the following member -functions - -- `void reset()` - - Reset the node_stream back to its beginning. - -- `bool can_pull()` - - Return whether there is a next element to pull. - -- `const node pull()` - - Get the next node from the stream and move to the next. - -- `const node peek()` - - Get the next node from the stream without moving to the next. - -### Node Writer - -To follow the ordering in a `node_file` one has to write nodes bottom-up and in -reverse for each level with respect to the _id_. One can write nodes to the file -by use of the `node_writer` object, that can be constructed in two ways. - -- `node_writer()` - - Construct a `node_writer` attached to nothing. - -- `node_writer(const node_file)` - - Construct a `node_writer` attached to the given `node_file`. - -The `node_writer` class provides the following member functions - -- `void push(node_t n)` (operator `<<`) - - Push a single node to the `node_file`. This also applies a few sanity checks - on the provided input, such as checks on the ordering. This does not check - whether the children named by _n_ do indeed exist in the file. If you provide - an _n_ with spurious children, then algorithms with this as their input will - have _undefined behaviour_. - -- `void attach(node_file f)` - - Attach the `node_writer` to a given `node_file`. - -- `bool attached() const` - - Whether the current `node_writer` currently is attached to a `node_file`. - -- `void detach()` - - Detach the `node_writer` from its current `node_file`, if any. - -It is important to note, that one cannot have multiple `node_writers` attached -to the same `node_file`. Furthermore, one also has to detach the `node_writer` -before anything can be read from the `node_file` or that the algorithms of -_Adiar_ can process on them. So, remember to either detach it explicitly or have -the `node_writer` destructed before calling any such functions. - -#### A Note on Equality Checking - -The _equality checking_ algorithm (`==`) of _Adiar_ exploits multiple -characteristics of decision diagrams to speed up its computation. If you want to -use your self-made decision diagrams in equality checking, then you have to be -sure to adhere to write it in its reduced form. - -1. Do not write nodes that are suppressed in the decision diagram, e.g. for BDDs - do not write nodes with _low_ == _high_. - -2. Do not write duplicate nodes to the same file, i.e. nodes where both their - _low_ children are the same and their _high_ children are the same. - -Equality checking also is much faster if the constructed decision diagram is on -_canonical_ form. The decision diagram being canonical means that it also -satisfies the following two constraints. - -1. The first node pushed to each level has _id_ `MAX_ID`, the next has _id_ - `MAX_ID - 1`, and so on. - -2. The nodes within each level are lexicographically ordered by their children - (_high_ first then _low_). That is, a node _n_ written to the file after - already having written node _m_ on the same level must not only satisfy _n < - m_ from Section [Core/Data types](data_types.md#identifiers-and-ordering) - but also the following extended constraint - -

- n.id < m.id ≡ n.high < m.high || (n.high = m.high && n.low < m.low) -

- -## Assignments and Labels - -Some functions take a list of assignments (cf. [Core/Data types](data_types.md#assignments))) -as input or return them as an output. To create such input, resp. traverse such -output, one can use the `assignment_writer`, resp. `assignment_stream`. Other -functions work on lists of labels (cf. [Core/Data types](data_types.md#identifiers-and-ordering)) -for which we provide the `label_writer` and `label_stream`. - -These writers provide the same interface as the `node_writer`. They also have -sanity checks on the ordering of their elements when pushing elements. The -streams also provide the same member functions as above with the addition of the -`attach(x_file)`, `attached()`, and `detach()` member functions. - diff --git a/docs/data_structures.md b/docs/data_structures.md new file mode 100644 index 000000000..014fdc760 --- /dev/null +++ b/docs/data_structures.md @@ -0,0 +1,16 @@ +--- +layout: default +title: Data Structures +nav_order: 3 +description: "Data Structures of Adiar" +permalink: /data_structures +has_children: true +--- + +# Data Structures +{: .no_toc } + +*Adiar* supports manipulation of two types of decision diagrams: *binary* (BDD) +and *zero-suppressed* (ZDD). Some of the operations on these decision diagrams +relate to a list of *labels* of or *assignments* of input variables. +{: .fs-6 .fw-300 } diff --git a/docs/bdd.md b/docs/data_structures/bdd.md similarity index 70% rename from docs/bdd.md rename to docs/data_structures/bdd.md index fb1723ec8..14652b823 100644 --- a/docs/bdd.md +++ b/docs/data_structures/bdd.md @@ -1,9 +1,10 @@ --- layout: default title: BDD -nav_order: 3 +nav_order: 1 +parent: Data Structures description: "Binary Decision Diagrams" -permalink: /bdd +permalink: data_structures/bdd --- # BDD @@ -17,9 +18,9 @@ A Binary Decision Diagram (BDD) represents a boolean function

The `bdd` class takes care of reference counting and optimal garbage collection -of the underlying files (cf. [Core/Files](core/files#nodes)). To ensure the -most disk-space is available, try to garbage collect the `bdd` objects as -quickly as possible and/or minimise the number of lvalues of said type. +of the underlying files. To ensure the most disk-space is available, try to +garbage collect the `bdd` objects as quickly as possible and/or minimise the +number of lvalues of said type. ## Table of Contents {: .no_toc .text-delta } @@ -31,10 +32,8 @@ quickly as possible and/or minimise the number of lvalues of said type. ## Basic Constructors -To construct a more complex but well-structured `bdd` than what follows below, -create a [`node_file`](core/files.md#nodes) and write the nodes bottom-up with -the [`node_writer`](core/files.md#node-writer). The `bdd` object can then be -copy-constructed from the `node_file`. +To construct a more complex but well-structured `bdd` by hand see the section on +[Manual Construction](../manual_construction). ### `bdd bdd_terminal(bool v)` {: .no_toc } @@ -57,13 +56,15 @@ Create a BDD representing the negation of the literal with the given label {: .no_toc } Construct a BDD representing the *and* of all the literals with the provided -labels. The *vars* must be sorted in increasing order. +[labels](./labels_and_assignments.md#labels). The *vars* must be sorted in +increasing order. ### `bdd bdd_or(label_file vars)` {: .no_toc } Construct a BDD representing the *or* of all the literals with the provided -labels. The *vars* must be sorted in increasing order. +[labels](./labels_and_assignments.md#labels). The *vars* must be sorted in +increasing order. ### `bdd bdd_counter(label_t min_var, label_t max_var, label_t threshold)` {: .no_toc } @@ -134,7 +135,8 @@ i.e. *∃v : f[xvar / v]*. {: .no_toc } Existentially quantify *f* for variables in *vars* in the very order these -variables are provided. +variables are provided in the +[`label_file`](./labels_and_assignments.md#labels). ### `bdd bdd_forall(bdd f, label_t l)` {: .no_toc } @@ -146,7 +148,7 @@ Forall quantification of the variable with label *var* in the BDD for _f_, i.e. {: .no_toc } Forall quantify *f* for variables in *vars* in the very order these variables -are provided. +are provided in the [`label_file`](./labels_and_assignments.md#labels). ### `bdd bdd_ite(bdd f, bdd g, bdd h)` {: .no_toc } @@ -154,7 +156,7 @@ are provided. Return the BDD representing the if-then-else of *f*, *g*, and *h*, i.e. *f ? g : h*. In other BDD packages such a function is good for manually constructing a BDD bottom-up, but for those purposes one should here instead use the -[`node_writer`](core/files.md#node-writer) class. +[`bdd_builder`](../manual_construction/builder.md#builderdd_policy-class) class. ### `bdd bdd_not(bdd f)` (operator: `~`) {: .no_toc } @@ -164,31 +166,32 @@ Return the BDD representing the negation of *f*, i.e. *¬f*. ### `bdd bdd_restrict(bdd f, assignment_file as)` {: .no_toc } -Return the BDD representing *f[xss, ..., xt +Return the BDD representing *f[xs / vs, ..., xt / vt]* for *(s ; vs), ..., (t, vt)* in *as*. That is, the BDD for *f* where the variable xs is restricted to the -fixed value vs, and so on. The assignments in *as* must be in +fixed value vs, and so on. The +[assignments](./labels_and_assignments.md#assignments) in *as* must be in increasing order wrt. the label. ## Counting Operations -### `uint64_t bdd_nodecount(bdd f)` +### `size_t bdd_nodecount(bdd f)` {: .no_toc } Return the number of nodes (not counting terminal nodes) in the BDD for *f*. -### `uint64_t bdd_varcount(bdd f)` +### `size_t bdd_varcount(bdd f)` {: .no_toc } Return the number of variables present in the BDD for *f*. -### `uint64_t bdd_pathcount(bdd f)` +### `size_t bdd_pathcount(bdd f)` {: .no_toc } Return the number of unique (but not necessarily disjoint) paths in the BDD for *f* that lead to a *true* terminal. -### `uint64_t bdd_satcount(bdd f, size_t varcount)` +### `size_t bdd_satcount(bdd f, size_t varcount)` {: .no_toc } Count the number of satisfying assignments (i.e. the number of *x* such that @@ -234,50 +237,60 @@ Whether *f* is the always true constant function. This is merely shorthand for ## Input variables -### `bool bdd_eval(bdd f, T x)` +### `bool bdd_eval(bdd f, assignment_func x)` {: .no_toc } Return *f(x)*, i.e. the evaluation of the given BDD for *f* according to the -assignment *x*. The type *T* of *x* can either be any function *label_t → bool* -(e.g. a lambda function) or an *assignment_file*. +total function, [`assignment_func`](./labels_and_assignments.md#assignments) *x*. + +### `bool bdd_eval(bdd f, assignment_file x)` +{: .no_toc } + +Return *f(x)*, i.e. the evaluation of the given BDD for *f* according to the +[`assignment_file`](./labels_and_assignments.md#assignments) *x*. ### `assignment_file bdd_satmin(bdd f)` {: .no_toc } -Return the lexicographically smallest *x* such that *f(x) = 1*. The variables -mentioned in *x* are for all levels in the given BDD. +Return the lexicographically smallest +[assignment](./labels_and_assignments.md#files) *x* such that *f(x) = +1*. The variables mentioned in *x* are for all levels in the given BDD. ### `assignment_file bdd_satmax(bdd f)` {: .no_toc } -Return the lexicographically largest *x* such that *f(x) = 1*. The variables -mentioned in *x* are for all levels in the given BDD. +Return the lexicographically largest +[assignment](./labels_and_assignments.md#files) *x* such that *f(x) = 1*. The +variables mentioned in *x* are for all levels in the given BDD. ### `label_t min_label(bdd f)` {: .no_toc } -Return the smallest label in the BDD for *f*, i.e. the label of the root. This -is the smallest input variable that has an effect on the output of *f*. +Return the smallest [label](./labels_and_assignments.md#labels) in the BDD for +*f*, i.e. the label of the root. This is the smallest input variable that has an +effect on the output of *f*. ### `label_t max_label(bdd f)` {: .no_toc } -Return the largest label in the BDD for *f*, i.e. the label of the deepest node. -This is the largest input variable that has an effect on the output of *f*. +Return the largest [label](./labels_and_assignments.md#labels) in the BDD for +*f*, i.e. the label of the deepest node. This is the largest input variable that +has an effect on the output of *f*. ### `label_file bdd_varprofile(bdd f)` {: .no_toc } -Return a file with the labels of the existing levels in *f*. +Obtain a [file of labels](./labels_and_assignments.md#files) of the existing +levels in *f*. ## Other Functions ### `bdd bdd_from(zdd A, label_file dom)` {: .no_toc } -Converts a [ZDD](zdd.md) into a BDD interpreted within the variable domain -*dom*. The domain should be a superset of the variables in the given ZDD. By -default, `dom` is the globally set domain. +Converts a [`zdd`](zdd.md) into a `bdd` interpreted within the variable domain +*dom*. The domain should be a superset of the variables in the given ZDD. If not +provided, then *dom* is set to the [globally set domain](../settings/domain.md). ## DOT Output diff --git a/docs/data_structures/labels_and_assignments.md b/docs/data_structures/labels_and_assignments.md new file mode 100644 index 000000000..544ee2e80 --- /dev/null +++ b/docs/data_structures/labels_and_assignments.md @@ -0,0 +1,271 @@ +--- +layout: default +title: Labels and Assignments +nav_order: 3 +parent: Data Structures +description: "Labels and Assignments" +permalink: data_structures/labels_and_assignments +--- + +## Table of Contents +{: .no_toc .text-delta } + +1. TOC +{:toc} + +--- + +## Labels + +An input variable *xi* is identified by its label *i* which in +*Adiar* is defined as the following type. + +```cpp +typedef uint32_t label_t; +``` + +Please note, that while `label_t` is an unsigned 32-bit integer, not all bits +are used. Specifically, *Adiar* does not support any labels larger than the +`MAX_LABEL` value (*224-1*). + +### Example + +The set of all even labels between *0* and *42* (inclusive) is constructed with +the following piece of code. +```cpp +label_file labels; + +{ // Garbage collect writer to free write-lock + label_writer lw(labels); + + for (label_t l = 0; l <= 42; l = l+2) { + lw << l; + } +} +``` +and it can then be read again as follows +```cpp +label_stream ls(labels); + +while (ls.can_pull()) { + std::cout << " " << ls.pull() << std::endl; +} +``` +For more details on the `label_file`, `label_stream`, and +`label_writer` see the section on [Files](#files) below. + +## Assignments + +An assignment maps a *label* to a boolean *value* and so they can be represented +as a pairing of the two. + +```cpp +struct assignment { label_t label; bool value; }; + +typedef assignment assignment_t +``` + +The operators `<` and `>` are defined such that they enforce labels are ordered +ascendingly. The `==`, and `!=` operators check both values. Finally, the `!` +operator negates the *value* and leaves the *label* unchanged. + +### `assignment_t create_assignment(label_t label, bool value)` + +Create an assignment given a label and value. + +### `label_t label_of(assignment_t assignment)` +{: .no_toc } + +Obtain the label of the variable to-be assigned a value. + +### `bool value_of(assignment_t assignment)` +{: .no_toc } + +Obtain the value to-be assigned to the variable with the label. + +### Example 1: Encoding a Total Assignment into a Function + +Consider the following truth assignment + +| Variable | Value | +|:-------------:|:-----:| +| x0 | ⊤ | +| x1 | ⊥ | +| x2 | ⊥ | +| x3 | ⊤ | + +Assuming the domain is only [0; 3] then we can encode it with the following +lambda function. + +```cpp +assignment_func assignment = [](label_t i) { return i == 0 || i == 3 }; +``` + +### Example 2: Encoding a Partial Assignment into a File + +One can encode the very same truth table above in `assignment_file` by use of +the `assignment_writer` shown below. +```cpp +assignment_file assignment; + +{ // Garbage collect writer to free write-lock + assignment_writer aw(assignment); + + aw << create_assignment(0, true ) + << create_assignment(1, false) + << create_assignment(2, false) + << create_assignment(3, true ) + ; +} +``` +Notice, the scope around the `assignment_writer` to detach it early. One can +then read this assignment and print out the above table as follows +```cpp +assignment_stream<> as(assignment); + +std::cout << "| var | value |" << std::endl; +std::cout << "|-----|-------|" << std::endl; + +while (as.can_pull()) { + assignment_t a = as.pull(); + std::cout << "| x" << a.label << " | " << a.value << " |" << std::endl; +} +``` +For more details on the `assignment_file`, `assignment_stream`, and +`assignment_writer` see the section on [Files](#files) below. + +## Files + +Both a `label_file` and an `assignment_file` are instances of a `simple_file` +which one can write to the end of and can read in either direction using their +respective *writer* and *stream* classes. + +--- + +### `file_stream` class + +This templated class provides a read-only access to a file with a single +*reading direction*. If the boolean `REVERSE` is set to *true* (default +*false*), then one reads the file in the reverse direction. + +--- + +### Constructors +{: .no_toc } + +### `file_stream::file_stream<>()` +{: .no_toc } + +Construct the stream class, attached to nothing. + +### `file_stream::file_stream<>(const simple_file)` +{: .no_toc } + +Construct the stream and have it attach to the given `simple_file`. + +--- + +### Member Functions +{: .no_toc } + +and it has the following member functions. + +### `bool file_stream::can_pull()` +{: .no_toc } + +Whether there is an element to pull in the desired direction. + +### `T file_stream::pull()` +{: .no_toc } + +Get the element from the stream in the desired direction and move to the next. + +### `T file_stream::peek()` +{: .no_toc } + +Get the element from the stream in the desired direction without moving to the +next. + +### `void file_stream::reset()` +{: .no_toc } + +Reset the stream back to its beginning of the current file. If `reverse` is +true, then it resets back to the end. + +### `void file_stream::attach(simple_file f)` +{: .no_toc } + +Attach the stream to the given file. + +### `bool file_stream::attached()` +{: .no_toc } + +Whether the stream is attached to a file. + +### `void file_stream::detach()` +{: .no_toc } + +Detach the stream from its current file, if any. + +--- + +### `simple_file_writer` class + +This allows one to push elements to the end of a file. The `Comp` template +argument is a comparator to enforce some desired structure of the file. This is +not important for the `label_writer` (`no_ordering`), but for the +`assignment_writer` this enforces an ascending order +(`std::less`). + +--- + +### Constructors +{: .no_toc } + +### `simple_file_writer::simple_file_writer<>()` +{: .no_toc } + +Construct it attached to nothing. + +### `simple_file_writer::simple_file_writer<>(const simple_file)` +{: .no_toc } + +Construct it attached to the given *simple_file*. + +--- + +### Member Functions +{: .no_toc } + +### `void simple_file_writer::push(T t)` (operator `<<`) +{: .no_toc } + +Push an *element* to the end of the file and check it is provided in-order. + +### `void simple_file_writer::unsafe_push(T t)` +{: .no_toc } + +Push an *element* to the end of the file. + +### `void simple_file_writer::sort()` +{: .no_toc } + +Sort the content of the attached file to be in the correct order based on +`Comp`. This is not useful in a `label_writer` but in the `assignment_writer` +this can be used to repair . + +### `void simple_file_writer::attach(simple_file f)` +{: .no_toc } + +Attach the writer to the given file. + +### `bool simple_file_writer::attached()` +{: .no_toc } + +Whether the writer is attached to a file. + +### `void simple_file_writer::detach()` +{: .no_toc } + +Detach the writer from its current file, if any. + diff --git a/docs/zdd.md b/docs/data_structures/zdd.md similarity index 68% rename from docs/zdd.md rename to docs/data_structures/zdd.md index 2f74db1bc..2ea3152d3 100644 --- a/docs/zdd.md +++ b/docs/data_structures/zdd.md @@ -1,9 +1,10 @@ --- layout: default title: ZDD -nav_order: 3 +nav_order: 2 +parent: Data Structures description: "Zero-suppressed Decision Diagrams" -permalink: /zdd +permalink: data_structures/zdd --- # ZDD @@ -17,9 +18,9 @@ A Zero-suppressed Decision Diagram (ZDD) represents a family of set of numbers

The `zdd` class takes care of reference counting and optimal garbage collection -of the underlying files (cf. [Core/Files](core/files.md#nodes)). To ensure the -most disk-space is available, try to garbage collect the `zdd` objects as -quickly as possible and/or minimise the number of lvalues of said type. +of the underlying files. To ensure the most disk-space is available, try to +garbage collect the `zdd` objects as quickly as possible and/or minimise the +number of lvalues of said type. ## Table of Contents {: .no_toc .text-delta } @@ -31,10 +32,8 @@ quickly as possible and/or minimise the number of lvalues of said type. ## Basic Constructors -To construct a more complex but well-structured `zdd` than what follows below, -create a [`node_file`](core/files.md#nodes) and write the nodes bottom-up with -the [`node_writer`](core/files.md#node-writer). The `zdd` object can then be -copy-constructed from the `node_file`. +To construct a more complex but well-structured `zdd` by hand see the section on +[Manual Construction](../manual_construction). ### `zdd zdd_terminal(bool v)` {: .no_toc } @@ -58,21 +57,23 @@ The labels in *vars* must be sorted in increasing order. ### `zdd zdd_singletons(label_file vars)` {: .no_toc } -Create a ZDD representing the family *{ {vars1}, {vars2}, ..., {varsk} }*. -The labels in *vars* must be sorted in increasing order. +Create a ZDD representing the family *{ {vars1}, {vars2}, +..., {varsk} }*. The [labels](./labels_and_assignments.md#labels) in +*vars* must be sorted in increasing order. ### `zdd zdd_powerset(label_file vars)` {: .no_toc } -Create a ZDD representing the family *pow(vars) = 2vars*. The labels -in *vars* must be sorted in increasing order. +Create a ZDD representing the family *pow(vars) = 2vars*. The +[labels](./labels_and_assignments.md#labels) in *vars* must be sorted in +increasing order. ### `zdd zdd_sized_set(label_file vars, k, pred)` {: .no_toc } -Create a ZDD representing the family *{ s ∈ pow(vars) | pred(|s|, k) }*, where pred -is a comparison predicate such as `std::less`, `std::greater`, and -`std::equal_to`. +Create a ZDD representing the family *{ s ∈ pow(vars) | pred(|s|, k) }* of +[labels](./labels_and_assignments.md#labels), where pred is a comparison +predicate such as `std::less`, `std::greater`, and `std::equal_to`. ## Basic Manipulation @@ -99,56 +100,61 @@ and/or *B*. Some operators are also provided with an alias function: {: .no_toc } Constructs the ZDD for *{ vars Δ a | a ∈ A }*, where Δ is the symmetric -difference between the two sets of variables *a* and *vars*. In other words, for -each set in *A* the value of each variable *i* from *vars* is flipped. +difference between the two [sets of variables](./labels_and_assignments.md#labels) +*a* and *vars*. In other words, for each set in *A* the value of each variable +*i* from *vars* is flipped. ### `zdd zdd_complement(zdd A, label_file dom)` (operator `~`) {: .no_toc } Constructs the ZDD for *pow(dom)* \ *A*, i.e. the complement of *A* with respect -to the variable domain, *dom*. The variables in *A* have to exist in *dom* too. -By default, `dom` is the globally set domain. +to the [set of variable domain](./labels_and_assignments.md#labels), *dom*. The +variables in *A* have to exist in *dom* too. If not provided, then `dom` is set +to the [globally set domain](../settings/domain.md). ### `zdd zdd_expand(zdd A, label_file vars)` {: .no_toc } Expands the domain of A to also include the variables in *vars*, i.e. it -computes the set *Ua ∈ A, i ∈ pow(vars) (a ∪ i)*. The variables in -*vars* are not allowed to be present in *A*. +computes the set *Ua ∈ A, i ∈ pow(vars) (a ∪ i)*. The +[variables](./labels_and_assignments.md#labels) in *vars* are not allowed to be +present in *A*. ### `zdd zdd_offset(zdd A, label_file vars)` {: .no_toc } Computes the ZDD for the subset *{ a ∈ A | ∀i ∈ vars : i ∉ a }*, i.e. where the -variables *i* in *vars* are set to 0. +[variables](./labels_and_assignments.md#labels) *i* in *vars* are set to 0. ### `zdd zdd_onset(zdd A, label_file vars)` {: .no_toc } Computes the ZDD for the subset *{ a ∈ A | ∀i ∈ vars : i ∈ a }*, i.e. where the -variables *i* in *vars* are set to 1. +[variables](./labels_and_assignments.md#labels) *i* in *vars* are set to 1. ### `zdd zdd_project(zdd A, label_file dom)` {: .no_toc } Construct the ZDD for πi1, ..., ik(A) = { s \ { i1, ..., ik }c | s ∈ A }, where i1, -..., ik are the elements in *vars*. That is, this constructs a ZDD of -the same sets, but where only the elements in the new domain *dom* are kept. +..., ik are the elements in the [set of variable +domain](./labels_and_assignments.md#labels), *dom*. That is, this constructs a +ZDD of the same sets, but where only the elements in the new domain *dom* are +kept. ## Counting Operations -### `uint64_t zdd_nodecount(zdd A)` +### `size_t zdd_nodecount(zdd A)` {: .no_toc } Return the number of nodes (not counting terminal nodes) in the ZDD for *A*. -### `uint64_t zdd_varcount(zdd A)` +### `size_t zdd_varcount(zdd A)` {: .no_toc } Return the number of variables present in the ZDD for *A*. -### `uint64_t zdd_size(zdd A)` +### `size_t zdd_size(zdd A)` {: .no_toc } Return \|*A*\|, i.e. the number of sets of elements in the family of sets *A*. @@ -214,14 +220,16 @@ Return whether *a ∈ A*. ### `std::optional zdd_minelem(zdd A)` {: .no_toc } -Finds the *a ∈ A* (if any) that is lexicographically smallest when interpreting -*a* as a binary number with 0 being the most significant bit. +Finds the [set of variables](./labels_and_assignments.md#labels) *a ∈ A* (if +any) that is lexicographically smallest when interpreting *a* as a binary number +with 0 being the most significant bit. ### `std::optional zdd_maxelem(zdd A)` {: .no_toc } -Finds the *a ∈ A* (if any) that is lexicographically largest when interpreting -*a as a binary number with 0 being the most significant bit. +Finds the [set of variables](./labels_and_assignments.md#labels) *a ∈ A* (if +any) that is lexicographically largest when interpreting *a as a binary number +with 0 being the most significant bit. ### `label_t min_label(zdd A)` {: .no_toc } @@ -238,16 +246,17 @@ the deepest node of the DAG in the ZDD. ### `label_file zdd_varprofile(zdd A)` {: .no_toc } -Return a file with the labels of the existing levels in *A*. +Obtain a [file of labels](./labels_and_assignments.md#labels) with the existing +levels in *A*. ## Other Functions ### `zdd zdd_from(bdd f, label_file dom)` {: .no_toc } -Converts a [BDD](bdd.md) into a ZDD interpreted within the variable domain -*dom*. The domain should be a superset of the variables in the given BDD. By -default, `dom` is the globally set domain. +Converts a [`bdd`](bdd.md) into a `zdd` interpreted within the variable domain +*dom*. The domain should be a superset of the variables in the given BDD. If not +provided, then `dom` is set to the [globally set domain](../settings/domain.md). ## DOT Output diff --git a/docs/examples.md b/docs/examples.md index 41308fefd..c097b92de 100644 --- a/docs/examples.md +++ b/docs/examples.md @@ -1,7 +1,7 @@ --- layout: default title: Examples -nav_order: 6 +nav_order: 7 description: "Complete examples that cover how to use Adiar" has_children: true --- @@ -9,5 +9,5 @@ has_children: true # Examples {: .no_toc } -The following examples provide an introduction to using all aspects of _Adiar_. +The following examples provide an introduction to using all aspects of *Adiar*. {: .fs-6 .fw-300 } diff --git a/docs/examples/knights_tour.md b/docs/examples/knights_tour.md index 430e625cb..66352fa2e 100644 --- a/docs/examples/knights_tour.md +++ b/docs/examples/knights_tour.md @@ -79,6 +79,10 @@ All remaining time steps remains one long "don't care" chain in between. Yet, inside of this chain we can encode the hamiltonian constraint for these three cells on the board by skipping them within the chain. +Hence, we can create the ZDD by hand using the +[`zdd_builder`](../manual_construction/builder.md#builderdd_policy-class) as +follows. + ```cpp adiar::zdd constraint_closed(int N) { diff --git a/docs/examples/queens.md b/docs/examples/queens.md index 8e03c2cfc..475672186 100644 --- a/docs/examples/queens.md +++ b/docs/examples/queens.md @@ -46,7 +46,7 @@ inline label_t label_of_position(uint64_t N, uint64_t i, uint64_t j) } ``` -### Explicitly constructing base cases +### Explicitly Constructing Base Cases Let us first restrict our attention to the base case of expressing the state of a single field (_i_,_j_). We need to express that a single queen is placed here, @@ -60,15 +60,17 @@ conflicting positions. We could construct the BDD with the builders and algorithms of _Adiar_. But, we can do even better than that, because the resulting BDD is well structured. So, -we can explicitly construct in one go with a `bdd_builder`! Remember that nodes -are to be written bottom-up. By the ordering of variables in `label_of_position` -we have to deal with (1) queens on the row _i_ and (2) queens on other rows. For -(1) we have to check all variables, whereas for (2) we only need to check on -column _j_ and the diagonals. All nodes but the one for xij are -connected to by their _low_ edge to the node generated before them (or to the -_true_ terminal if said node is first one generated). The xij -variable is, on the other hand, connected to the prior generated node by its -high edge. All other edges go the to _false_ terminal. +we can explicitly construct in one go with a +[`bdd_builder`](../manual_construction/builder.md#builderdd_policy-class)! +Remember that nodes are to be constructed bottom-up. By the ordering of +variables in `label_of_position` we have to deal with (1) queens on the row _i_ +and (2) queens on other rows. For (1) we have to check all variables, whereas +for (2) we only need to check on column _j_ and the diagonals. All nodes but the +one for xij are connected to by their _low_ edge to the node +generated before them (or to the _true_ terminal if said node is first one +generated). The xij variable is, on the other hand, connected to the +prior generated node by its high edge. All other edges go the to _false_ +terminal. ```cpp adiar::bdd n_queens_S(int i, int j) @@ -121,7 +123,7 @@ adiar::bdd n_queens_S(int i, int j) } ``` -### Constructing the entire board +### Constructing the Entire Board From the formula in `n_queens_S` we can construct the formula for the entire row by combining them with an OR. Since the formula is _true_ only when the queen is @@ -159,7 +161,7 @@ bdd n_queens_B(int N) } ``` -## Counting the number of solutions +## Counting the Number of Solutions When the entire board is constructed as described above, then we merely need to count the number of satisfying solutions to the generated BDD. @@ -174,9 +176,10 @@ int main(int argc, char* argv[]) } ``` -## Printing each solution +## Printing each Solution -The following is based on a [report by Martin Faartoft](github.com/MartinFaartoft/n-queens-bdd/blob/master/report.tex). +The following is based on a [report by Martin +Faartoft](github.com/MartinFaartoft/n-queens-bdd/blob/master/report.tex). If we want to list all the assignments then we have to do something more than merely count the number of satisfying assignments. But, given the BDD we just diff --git a/docs/getting_started.md b/docs/getting_started.md index 4fad551e0..2304a59bb 100644 --- a/docs/getting_started.md +++ b/docs/getting_started.md @@ -78,7 +78,10 @@ int main() } ``` -The `adiar_init` function initialises the BDD library given the following arguments +### `void adiar_init(size_t memory_limit_bytes, std::string temp_dir)` +{: .no_toc } + +Initialises the BDD library given the following arguments - `memory_limit_bytes` @@ -89,13 +92,14 @@ The `adiar_init` function initialises the BDD library given the following argume The directory in which to place all temporary files. Default on Linux is the `/tmp` library. -If you create any [bdd](bdd.md) or [zdd](zdd.md) objects then remember to have -them garbage collected (for example, by letting a local variable go out of scope -as shown above) before calling `adiar::adiar_deinit()`. +### `bool adiar_initialized()` +{: .no_toc } + +Whether *Adiar* is initialized. + +### `void adiar_deinit()` +{: .no_toc } -By default *Adiar* decides whether to use internal or external memory for each -algorithm based on the size of the inputs. However, if you want to force using -always internal or external memory set the global variable `adiar::memory::mode` -to `adiar::memory::INTERNAL` or `adiar::memory::EXTERNAL` (default is -`adiar::memory::AUTO`). Setting `adiar::memory::mode` to `adiar::memory::INTERNAL` -is at your own risk and may crash if the input is too large. +Deinitialises the library. Notice, that all [bdd](bdd.md) and [zdd](zdd.md) +objects have to be destructed before calling this function, e.g. by letting a +local variable go out of scope as shown above. diff --git a/docs/index.md b/docs/index.md index aebd47d24..7cff2be11 100644 --- a/docs/index.md +++ b/docs/index.md @@ -26,22 +26,22 @@ nodes on disk to delay recursion. Dependencies and installation of *Adiar* and how to initialise it in your C++ application. -2. [BDD](bdd.md) +2. [Data Structures](data_structures.md) + 1. [Binary Decision Diagrams (BDD)](data_structures/bdd.md) + 2. [Zero-suppressed Decision Diagrams (ZDD)](data_structures/zdd.md) + 3. [Labels and Assignments](data_structures/labels_and_assignments.md) - Binary Decision Diagrams and its supported functions. +3. [Manual Construction](manual_construction.md) -3. [ZDD](zdd.md) - - Zero-suppressed Decision Diagrams and its supported functions. + How to construct BDDs and ZDDs bottom-up by hand. 4. [Statistics](statistics.md) Statistics on the internal algorithms and data structures. -5. [Core](core.md) +5. [Settings](settings.md) - The underlying *data types* and *files* that you can use to construct larger - decision diagrams programmatically. + Global settings of *Adiar* that can be set at run or at compile-time. 6. [Examples](examples.md) diff --git a/docs/manual_construction.md b/docs/manual_construction.md new file mode 100644 index 000000000..3e39925b3 --- /dev/null +++ b/docs/manual_construction.md @@ -0,0 +1,24 @@ +--- +layout: default +title: Manual Construction +nav_order: 4 +description: "Manual Construction of BDDs and ZDDs" +permalink: /manual_construction +has_children: true +--- + +# Manual Construction +{: .no_toc } + +In some cases, one may already know the shape of the +[BDDs](data_structures/bdd.md) and/or as [ZDDs](data_structures/zdd.md) for a +more complex function. In those cases, it is much cheaper to construct them by +hand than to manipulate logic formulas +{: .fs-6 .fw-300 } + +To this end, one can construct these decision diagrams bottom-up in *Adiar* by +use of the provided [builders](manual_construction/builder.md). Expert users +that need a few more ounces of performance out of such a manual construction +constructions, on the other hand, may want to +[write](manual_construction/node_writer.md) directly to the raw files +underneath. diff --git a/docs/manual_construction/builder.md b/docs/manual_construction/builder.md new file mode 100644 index 000000000..e273b3e64 --- /dev/null +++ b/docs/manual_construction/builder.md @@ -0,0 +1,146 @@ +--- +layout: default +title: Builder +nav_order: 1 +parent: Manual Construction +description: "Builder Class" +permalink: manual_construction/builder +--- + +# Builder +{: .no_toc } + +The builder classes provide easy-to-use interfaces for a manual bottom-up +construction of a BDD and a ZDD that is similar to manual construction in any +other BDD package. +{: .fs-6 .fw-300 } + +## Table of Contents +{: .no_toc .text-delta } + +1. TOC +{:toc} + +--- + +## `builder` class + +The builder classes are implemented as a single templated class +`builder` where the template argument carries the logic related to +the specific type of decision diagram. These builders provide the user with +"pointers" to the nodes created within for use them during construction. In what +follows we will write `dd` as a placeholder for both +[`bdd`](../data_structures/bdd.md) and [`zdd`](../data_structures/zdd.md). + +We provide the following aliases for both the builder and their pointers so one +does not need to take the templated argument into account. + +### `bdd_builder` +{: .no_toc } + +Builder for Binary Decision Diagram ([`bdd`](../data_structures/bdd.md)). + +### `zdd_builder` +{: .no_toc } + +Builder for Zero-suppressed Decision Diagram ([`zdd`](../data_structures/zdd.md)). + +--- + +### Constructors +{: .no_toc } + +### `dd_builder::dd_builder()` +{: .no_toc } + +Default constructor. After construction it is ready to add nodes with any of the +*add_node* member functions below. + +--- + +### Member Functions +{: .no_toc } + +### `dd_ptr dd_builder::add_node(bool v)` +{: .no_toc } + +Adds a terminal node with a given value *v*. This may be called at any time, +regardless of whether any other nodes have been created. + +### `dd_ptr dd_builder::add_node(label_t label, dd_ptr low, dd_ptr high)` +{: .no_toc } + +Adds a decision diagram node with a given *label* and the given *low* and *high* +child. + +This will apply the first reduction rule associated with the specific type of +decision diagram `dd`, e.g. not construct a *don't care* node for BDDs but +instead just return its child. The builder cannot apply the second reduction +rule, i.e. merging of duplicate nodes, so that is still left up to you to do. + +This will throw a `std::invalid_argument` exception in the following cases: +- The provided *low* or *high* pointers originate from another builder object. +- Nodes are not added bottom-up, i.e. the *label* provided is strictly larger + than the label of the previously added non-terminal node. +- The provided *label* is larger than what is supported by *Adiar*. +- It violates the variable ordering, i.e. the label of one or both its children + is smaller than or equals to the provided *label*. + +### `dd_ptr dd_builder::add_node(label_t label, bool low, dd_ptr high)` +{: .no_toc } + +Similar to `add_node(label, add_node(low), high)`. + +### `dd_ptr dd_builder::add_node(label_t label, dd_ptr low, bool high)` +{: .no_toc } + +Similar to `add_node(label, low, add_node(high))`. + +### `dd_ptr dd_builder::add_node(label_t label, bool low, bool high)` +{: .no_toc } + +Similar to `add_node(label, add_node(low), add_node(high))`. + +### `dd dd_builder::build()` +{: .no_toc } + +Build the final decision diagram `dd` object with the nodes that were added +prior to this call. This will also immediately [*clear()*](#void-builderclear) +it to create a new one. + +This will throw a `std::domain_error` if +- *add_node(...)* has not been called, i.e. no nodes have been added before this. +- The resulting decision diagram has more than one root. + +### `void dd_builder::clear()` +{: .no_toc } + +Clear the builder of all its current content, discarding all nodes and +invalidating any pointers to them. This is similar to constructing a new +builder. + +## Example + +Consider the following BDD, equivalent to the formula (x0 ∧ +x1) ∨ x2. + + +![Example (a) of a BDD](./example_a.png){: style="max-width: 10rem; margin: 0 auto; display: block" } + + +This can be constructed as follows + +```cpp +bdd_builder b; + +const bdd_ptr p2 = b.add_node(2, false, true); +const bdd_ptr p1 = b.add_node(1, false, true); +const bdd_ptr p0 = b.add_node(0, p2, p1); + +bdd example_a = b.build(); +``` + +Notice, construction has to be done bottom up! So, one has to create the node +for *x2* first even though the subtrees stored in *p1* and *p2* are +disjoint. + diff --git a/docs/manual_construction/example_a.png b/docs/manual_construction/example_a.png new file mode 100644 index 000000000..5253a7014 Binary files /dev/null and b/docs/manual_construction/example_a.png differ diff --git a/docs/manual_construction/example_dags.png b/docs/manual_construction/example_dags.png new file mode 100644 index 000000000..ef4887f19 Binary files /dev/null and b/docs/manual_construction/example_dags.png differ diff --git a/docs/manual_construction/node_writer.md b/docs/manual_construction/node_writer.md new file mode 100644 index 000000000..4e19a928f --- /dev/null +++ b/docs/manual_construction/node_writer.md @@ -0,0 +1,463 @@ +--- +layout: default +title: Nodes and Writers +nav_order: 2 +parent: Manual Construction +description: "Nodes, their Files and Writers" +permalink: manual_construction/node_writer +--- + +# Nodes, their Files, and their Writers +{: .no_toc } + +The [builder](./builder.md) provides an abstraction of the representation of +decision diagrams in *Adiar* at a minor cost to the performance of manually +constructing. An expert user may desire to get closer to the raw files for the +sake of performance. +{: .fs-6 .fw-300 } + +## Table of Contents +{: .no_toc .text-delta } + +1. TOC +{:toc} + +--- + +## Unique Identifiers + +A non-terminal node is uniquely identified by a tuple (*i*, *id*). The first +entry, *i*, is the label of the variabel whereas *id* is an identifier of that +specific node. This identifier only needs to be unique on each level, i.e. for +each *i*, since nodes are still uniquely identifiable by the combination of +their label and identifier. This tuple create a unique identifier *uid* of a +node which substitute as a "pointer" to it. + +| C++ Type | Type | Semantics | +|------------|-----------|---------------------------------------------------------------------| +| `uint32_t` | `label_t` | The label, i.e. input variable, of a BDD node. | +| `uint64_t` | `id_t` | The level-identifier of a node, i.e. the index on said level. | +| `uint64_t` | `uid_t` | Unique identifier of a node consisting of a label and an identifier | + +For sake of performance, these uids are encoded as an unsigned 64-bit integer. +Hence, the label and the id cannot make use of all their bits available and so +their values are upper bounded by the constants `MAX_LABEL` and `MAX_ID`. + +### `uid_t create_node_uid(label_t l, id_t id)` +{: .no_toc } + +Create the unique identifier for the node with label *l* and identifier *id*. + +### `label_t label_of(uid_t u)` +{: .no_toc } + +Obtain the label from a unique identifier. + +### `id_t id_of(uid_t u)` +{: .no_toc } + +Obtain the label from a unique identifier. + +### `uid_t create_terminal_uid(bool v)` +{: .no_toc } + +Create the unique identifier to a terminal with a given boolean value. + +### `bool value_of(ptr_t p)` +{: .no_toc } + +Extract the boolean value of the given terminal identifier. + +### `uid_t negate(ptr_t p)` +{: .no_toc } + +Negate the value of the terminal + +### `bool is_node(uid_t p)` +{: .no_toc } + +Whether a unique identifier is for a non-terminal decision diagram node. + +### `bool is_terminal(uid_t p)` +{: .no_toc } + +Whether a unique identifier is for a terminal node. + +### `bool is_false(uid_t p)` +{: .no_toc } + +Shorthand for `is_terminal(p) && !value_of(p)`. + +### `bool is_true(uid_t p)` +{: .no_toc } + +Shorthand for `is_terminal(p) && value_of(p)`. + +## Nodes + +With the above a node in _Adiar_ is the following combination of 3 unsigned +64-bit numbers + +```cpp +struct node { uid_t uid; uid_t low; uid_t high; }; + +typedef node node_t; +``` + +### `node_t create_node(label_t label, id_t id, uid_t low, uid_t high)` +{: .no_toc } + +Create a node, given a label and an id for the specific node, together with the +identifier for its low and high child. We also provide variants of this +function, where `low` and `high` are of type `node_t`. + +### `label_t label_of(node_t n)` +{: .no_toc } + +Extract the label of a non-terminal node, i.e. `label_of(n.uid)`. + +### `id_t id_of(node_t n)` +{: .no_toc } + +Extract the id of a non-terminal node, i.e. `id_of(n.uid)`. + +### `node_t create_terminal(bool value)` +{: .no_toc } + +Create a terminal node with a specific boolean value. + +### `bool is_terminal(node_t n)` +{: .no_toc } + +Assert whether the node represents a terminal node. + +### `bool value_of(node_t n)` +{: .no_toc } + +Extract the value of the given terminal node. + +### `bool is_false(node_t)` +{: .no_toc } + +Whether *n* represents the false terminal, i.e. similar to `is_terminal(n) && !value_of(n)`. + +### `bool is_true(node_t)` +{: .no_toc } + +Whether *n* represents the false terminal, i.e. similar to `is_terminal(n) && value_of(n)`. + +### `node_t negate(node_t n)` (operator `!`) +{: .no_toc } + +Negates a node +- If it is a terminal, then its value is negated +- If it is a non-terminal node with a pointer to a terminal, then said pointer is negated. + +## `node_file` class + +A decision diagram is represented in *Adiar* as a list of nodes that are in +reverse of the following total ordering of their [unique +identifiers](#unique-identifiers). + +

+ (i1, id1) < (i2, id2) ≡ + i1 < i2 || (labe1 = i2 && id1 < id2) +

+ +That is, decision diagrams in *Adiar* are list of nodes in *descending* order +with respect to the nodes' unique identifiers. + +For example, consider the following four BDDs. + +![Examples BDDs](./example_dags.png) + +These are represented in *Adiar* as a `node_file` with the following list of +nodes. + +- (a) : [ { (2,0) , ⊥ , ⊤ } ] +- (b) : [ { (1,0) , ⊥ , ⊤ }, { (0,0) , ⊥ , (1,0) } ] +- (c) : [ { (1,1) , ⊤ , ⊥ }, { (1,0) , ⊥ , ⊤ }, { (0,0) , (1,0) , (1,1) } ] +- (d) : [ { (2,0) , ⊥ , ⊤ }, { (1,0) , (2,0) , ⊤ } ] + +### Equality Checking and Canonicity + +Since *Adiar* represents each BDD in a separate file, then it cannot merely +check for equality by merely comparing pointers in constant time. Instead, +multiple features of reduced decision diagrams are exploited to speed up its +computation. + +If your manually constructed decision diagrams is supposed to be used in the +context of equality checking then you have to be sure to adhere to write it in +its reduced form. + +1. Do not write nodes that are suppressed in the decision diagram, e.g. for BDDs + do not push nodes where *low* == *high*. + +2. Do not write duplicate nodes to the same file, i.e. nodes where both their + *low* children are the same and their *high* children are the same. + +Equality checking also is much faster if the constructed decision diagram is on +*canonical* form. The decision diagram being canonical means that it also +satisfies the following two constraints. + +1. The first node pushed to each level has *id* `MAX_ID`, the next has *id* + `MAX_ID - 1`, and so on. + +2. The nodes within each level are lexicographically ordered by their children + (*high* first then *low*). That is, a node *n* written to the file after + already having written node *m* on the same level must not only satisfy *n.uid + < m.uid* but also the following extended constraint + +

+ n.id < m.id ≡ n.high < m.high || (n.high = m.high && n.low < m.low) +

+ +Note that the above examples are **not** canonical. Their identifiers are not +starting at `MAX_ID` and in (b) are the two nodes on level *1* in the wrong +order. + +### Meta variables + +A `node_file` also contains several pieces of meta information, but you can skip +this section since the [`node_writer`](node_writer) class provides the +`.push(node_t n)` function takes care of computing these very values. Yet, to +further improve performance you can skip the logic and use the `.unsafe_push` +function instead and then provide these values yourself. + +Below is a list of all pieces of meta information stored in a `node_file`. +Points that are checkmarked are updated by the `.unsafe_push(node_t)` function +and require no updates from the user. + +#### Level Information +{: .no_toc } + +Next to the file containing nodes, there is another file with `level_information` + +```cpp +struct level_info { label_t label; size_t width; }; +``` + +The examples above would have the following level information stored. + +- (a) : [ { 2, 1 } ] +- (b) : [ { 1, 1 } , { 0, 1 } ] +- (c) : [ { 1, 2 } , { 0, 1 } ] +- (d) : [ { 2, 1 } , { 1, 1 } ] + +#### Canonicity +{: .no_toc } + +A single boolean value `canonical` (default `false`) marks whether the nodes +are on a [*canonical form*](#equality-checking-and-canonicity). + +#### Number of Terminals +{: .no_toc } + +The 2-length array `number_of_terminals` includes the number of arcs (directed +edges) from an internal node to a terminal. The *0* index includes the number of +arcs to *false* whereas *1* the number of arcs to *true*. + +In the four examples above these ought to be set to. + +- (a) : [ 1, 1 ] +- (b) : [ 2, 1 ] +- (c) : [ 2, 2 ] +- (d) : [ 1, 2 ] + +#### Maximum Levelized Cut +{: .no_toc } + +The 4-length array `max_1level_cut` and `max_2level_cut` provide an upper bound +on the maximum *1*-level and *2*-level cuts in the directed acyclic graph (DAG). +A *1-level* cut divides the DAG in two right in-between two levels. A *2-level* +cut has a bit more wiggle-room in its shape: nodes on one specific level may +choose to be on either side of the cut depending on whether they have more +in-going or out-going arcs. + +The four entries in the array correspond to the size of the cut of a specific +subgraph with or withour arcs to one or both terminals. The following enum in +` f)` +{: .no_toc } + +Attach the writer to the given file. + +### `bool node_writer::attached()` +{: .no_toc } + +Whether the writer is attached to a file. + +### `void node_writer::detach()` +{: .no_toc } + +Detach the writer from its current file, if any. This will also update the meta +information with sound upper bounds for the *1-level* and the *2-level* cuts. + +## Examples + +We will construct the following BDD in two ways with the `node_writer`. + +![Example (a) of a BDD](./example_a.png){: style="max-width: 10rem; margin: 0 auto; display: block" } + +### Using `node_writer::push(...)` + +When using the `node_writer::push(node_t)` function one only needs to construct +the nodes and push them in the correct order. + +```cpp +node_file nf; + +{ // Scope to get node_writer to deconstruct and detach early + node_writer nw(nf); + + const uid_t terminal_F = create_terminal_uid(false); + const uid_t terminal_T = create_terminal_uid(true); + const node_t n2 = create_node(2, MAX_ID, terminal_F, terminal_T); + const node_t n1 = create_node(1, MAX_ID, terminal_F, terminal_T); + const node_t n0 = create_node(0, MAX_ID, n2, n1); + + nw << n2 << n1 << n0; +} + +bdd result(nf); +``` + +### Using `node_writer::unsafe_push(...)` + +If one wants to skip the cost of the logic inside of the *push* function then +one also needs to add the necessary meta information. + +```cpp +node_file nf; + +{ // Scope to get node_writer to deconstruct and detach early + node_writer nw(nf); + + // Nodes + const uid_t terminal_F = create_terminal_uid(false); + const uid_t terminal_T = create_terminal_uid(true); + + const node_t n2 = create_node(2, MAX_ID, terminal_F, terminal_T); + nw.unsafe_push(n2); + + const node_t n1 = create_node(1, MAX_ID, terminal_F, terminal_T); + nw.unsafe_push(n1); + + const node_t n0 = create_node(0, MAX_ID, n2, n1); + nw.unsafe_push(n0); + + // Level information + nw.unsafe_push(create_level_info(2,1)); + nw.unsafe_push(create_level_info(1,1)); + nw.unsafe_push(create_level_info(0,1)); + + // Canonicity + nf->canonical = true; + + // Number of Terminals + // Is already taken care of by '.unsafe_push(node_t n)', so it should not + // be updated. + + // 1-level cut + nf->max_1level_cut[cut_type::INTERNAL] = 2; + nf->max_1level_cut[cut_type::INTERNAL_FALSE] = 3; + nf->max_1level_cut[cut_type::INTERNAL_TRUE] = 3; + nf->max_1level_cut[cut_type::ALL] = 4; + + // 2-level cut + // Technically, the destructor of the 'node_writer' already notices during + // the '.detach()' that each level is a single node wide and so the 1-level + // and 2-level cut must be the same. + // + // Yet, for the sake of completeness. + nf->max_2level_cut[cut_type::INTERNAL] = 2; + nf->max_2level_cut[cut_type::INTERNAL_FALSE] = 3; + nf->max_2level_cut[cut_type::INTERNAL_TRUE] = 3; + nf->max_2level_cut[cut_type::ALL] = 4; +} + +bdd result(nf); +``` diff --git a/docs/settings.md b/docs/settings.md new file mode 100644 index 000000000..c7ddad258 --- /dev/null +++ b/docs/settings.md @@ -0,0 +1,15 @@ +--- +layout: default +title: Settings +nav_order: 5 +description: "Advanced Settings for Adiar" +permalink: /settings +has_children: true +--- + +# Settings +{: .no_toc } + +Some features of *Adiar* are only available if some settings of Adiar are set. +Other behaviours can be tweaked at run or at compilation time. +{: .fs-6 .fw-300 } diff --git a/docs/settings/domain.md b/docs/settings/domain.md new file mode 100644 index 000000000..54de48929 --- /dev/null +++ b/docs/settings/domain.md @@ -0,0 +1,35 @@ +--- +layout: default +title: Domain +nav_order: 1 +parent: Settings +description: "Domain of All Variables" +permalink: settings/domain +--- + +# Domain +{: .no_toc } + +Some operations depend on a domain of all variables for the problem being +modelled. For simplicity, this can be set once. + {: .fs-6 .fw-300 } + +--- + +### `void adiar_set_domain(label_file dom)` +{: .no_toc } + +Sets the global domain of variables to the +[labels](../data_structures/labels_and_assignments#labels) in the given +[`label_file`](../data_structures/labels_and_assignments.md#files). + +### `bool adiar_has_domain()` +{: .no_toc } + +Whether a global domain already is set. + +### `label_file adiar_get_domain()` +{: .no_toc } + +Retrieve the [`label_file`](../data_structures/labels_and_assignments.md#files) +that represents the current domain. diff --git a/docs/settings/memory_mode.md b/docs/settings/memory_mode.md new file mode 100644 index 000000000..e26dc05f7 --- /dev/null +++ b/docs/settings/memory_mode.md @@ -0,0 +1,45 @@ +--- +layout: default +title: Memory Mode +nav_order: 2 +parent: Settings +description: "Memory Mode of Auxiliary Data Structures" +permalink: settings/memory_mode +--- + +# Memory Mode +{: .no_toc } + +*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. +{: .fs-6 .fw-300 } + +What type of auxiliary data structure is used is encapsulated in the following +`memory_mode` enum in the `adiar::memory` namespace which can have one of the +following three values + +| Enum Value | Effect | +|------------|------------------------------------------------| +| `AUTO` | Automatically decide on type of memory to use. | +| `INTERNAL` | Always use *internal* memory. | +| `EXTERNAL` | Always use *external* memory. | + +If you want to force *Adiar* to a specific memory mode then you should set the +global variable `adiar::memory::mode` to one of the above three values. For +example, one can force *Adiar* always use internal memory with the +following piece of code. +```cpp +adiar::memory::mode = adiar::memory::INTERNAL +``` + +| ! WARNING ! | +|:----------------------------------------------------------------------------:| +| **Using `INTERNAL` may lead to crashes if an input or output is too large!** | + +By default `adiar::memory::mode` is set to `AUTO`. That is, *Adiar* decides +whether to use internal or external memory for each algorithm based on meta +information about the inputs. + diff --git a/docs/statistics.md b/docs/statistics.md index c4f3a4011..844c82eb3 100644 --- a/docs/statistics.md +++ b/docs/statistics.md @@ -1,7 +1,7 @@ --- layout: default title: Statistics -nav_order: 4 +nav_order: 6 description: "Gathering statistics" permalink: /statistics --- @@ -15,6 +15,8 @@ permalink: /statistics 1. TOC {:toc} +--- + ## Activate Gathering of Statistics Statistics are by default **not** gathered due to a concern of the performance of *Adiar*. That is, the logic related to updating the statistics is only run diff --git a/external/tpie b/external/tpie index d15dad532..06a8a35bf 160000 --- a/external/tpie +++ b/external/tpie @@ -1 +1 @@ -Subproject commit d15dad532662a23f3c6d328dabad4122a1fa44b3 +Subproject commit 06a8a35bf65d01ff39cd84871d974bd9133d0be5