Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Api/naming scheme #545

Merged
merged 26 commits into from
Sep 28, 2023
Merged
Changes from all commits
Commits
Show all changes
26 commits
Select commit Hold shift + click to select a range
8003771
Elaborate on naming scheme
SSoelvsten Sep 26, 2023
9d507c0
Fix naming scheme of dd_predicates
SSoelvsten Sep 26, 2023
fae727b
Hide implementation of dd_predicates
SSoelvsten Sep 26, 2023
8e12ba0
Move 'zdd_subset' implementation into implementation file
SSoelvsten Sep 26, 2023
1be61a5
Move <adiar/functional.h> into its own Documentation Module
SSoelvsten Sep 26, 2023
6ff513d
Enforce Snake_Case for enum values
SSoelvsten Sep 26, 2023
319168e
Make all static constexpr variables snake_case
SSoelvsten Sep 26, 2023
c3beb94
Fix template parameter names for levelized priority queue
SSoelvsten Sep 26, 2023
1ddf340
Elaborate on naming scheme for types
SSoelvsten Sep 26, 2023
a5aa41c
Clean up of '__level_of<>' template function
SSoelvsten Sep 26, 2023
296357d
Move templated inference of level stream into utilities
SSoelvsten Sep 26, 2023
c8d818e
Add missing documentation to level_merger
SSoelvsten Sep 26, 2023
6644c23
Move zdd_top and zdd_bot into compilation unit for consistency
SSoelvsten Sep 26, 2023
5abfa3a
Improve consistency of simple one-liners in public API
SSoelvsten Sep 26, 2023
bc9e35c
Add 'end' marker to documentation
SSoelvsten Sep 26, 2023
06de2e0
Code cleanup on 'cardinality' variable in tuple
SSoelvsten Sep 26, 2023
afae8d7
Align Domain module with naming scheme
SSoelvsten Sep 26, 2023
03e36a7
Fix adiar/functional uses std::exceptions directly
SSoelvsten Sep 26, 2023
512936b
Rename Statistics module to match with naming scheme
SSoelvsten Sep 26, 2023
c5eacd2
Delete <adiar/data.h>
SSoelvsten Sep 26, 2023
78eb35a
Further clean up of public API (WIP)
SSoelvsten Sep 26, 2023
52483b2
Refactor 'cut_type' into class with member functions
SSoelvsten Sep 27, 2023
503d690
Move 'bool_op' predicates and manipulation into adiar::internal
SSoelvsten Sep 27, 2023
422ba7c
Proof read and update CHANGELOG
SSoelvsten Sep 27, 2023
bc0d5e2
Update CONTRIBUTING about state of naming scheme
SSoelvsten Sep 27, 2023
5fcdcd6
Fix compilation of example/queens due to breaking changes
SSoelvsten Sep 27, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
364 changes: 287 additions & 77 deletions CHANGELOG.md

Large diffs are not rendered by default.

60 changes: 48 additions & 12 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
@@ -161,12 +161,48 @@ CPP source file.

### §3 Naming Scheme

All functions and classes and their member functions should follow the rules
below.
The codebase uses [snake case](https://en.wikipedia.org/wiki/Snake_case) as much
as possible. This nicely aligns Adiar's codebase with the *std* (and the
*tpie*) namespace that the developers are used to anyway. Furthermore, this way
of writing might be easier to read.

- Use [snake case](https://en.wikipedia.org/wiki/Snake_case).
- All Decision Diagram functions in the public API are prefixed with the type of
the decision diagram, e.g. the Apply function for a `bdd` is called `bdd_apply`.
- For *namespaces*, *classes*, *variables*, and *functions* use `snake_case`.
The only other exceptions are *enum* values and the public API (see below).

- Preprocessing variables use *SNAKE_CASE*.

- We cannot use *snake_case* or *SNAKE_CASE* for enum values since that may
clash with keywords or preprocessing variables. Hence, we have settled on
`Snake_Case`.

- Yet, in the public *BDD* API we run into some problems. What we really want
is to have the `bdd` and `zdd` "class" prefix all functions as a namespace,
e.g. we would write `adiar::bdd h = adiar::bdd::and(f,g)`. Yet we cannot do
so since `and`, `or`, and `xor` are keywords in C++.

So we need some alternative. Yet, each is a compromise in some way.
Currently, we have chosen to stick with a naming scheme that aligns with the
C API of *BuDDy* and *Sylvan* and does not clash too much with the use of
*snake_case*:

All functions of the public API are of the form `{prefix}_{functionname}`,
e.g. `bdd_and(f,g)` by prepending `bdd_` onto the `and(f,g)` function name.
Functions names that consist of multiple words, e.g. *is true*, is written
in *nocase*, e.g. `bdd_istrue(f)`.

- Type variables exposed from a class have their names suffixed with `_type`.
Template type parameters are suffixed with `_t`. Global types are *not*
suffixed with anything (except if there is a good reason to do it).

This aligns with *std* and prevents shadowing between the two.

- Private class member variables are prefixed with a single `_`; non-static
public ones may also be prefixed as such.

The entire public API, i.e. everything in the *adiar* namespace, should adhere
to the above. Yet, the internal logic in *adiar::internal* may still . Please
fix these when you see them. But, do those changes in an independent commit of
one changing/adding logic.

### §4 No Almost Always Auto!

@@ -179,17 +215,17 @@ reader and (3) to provide all the information necessary to debug the code.

As Adiar grows larger and more complex, one submodule is the foundation on which
others are built. Hence, **all** functions, data structures, classes, and
variables - even the ones in *src/adiar/internal/* that are not part of the
public API - should be well documented for both the *end users* and also the
variables - even the ones in *adiar::internal* that are not part of the public
API - should be well documented for both the *end users* and especially also the
*developers*.

### §6 Test Everything Thoroughly

Adiar's Decision Diagrams are to be used in the context of verification of
critical software. At the same time, the Adiar's algorithms are much more
complex than other BDD implementations and have multiple layers from which an
error could originate.
critical software. At the same time, Adiar's algorithms are much more complex
than other BDD implementations and have multiple layers from which an error
could originate.

Hence, it is vital we can ensure correctness of Adiar by having as thorough unit
testing as possible. This also applies to everything within
*src/adiar/internal/* that is not part of the public API.
testing as possible. This also applies to everything within *adiar::internal*
that is not part of the public API.
2 changes: 1 addition & 1 deletion docs/Doxyfile.in
Original file line number Diff line number Diff line change
@@ -872,10 +872,10 @@ INPUT = @CMAKE_SOURCE_DIR@/docs/index.md \
@CMAKE_SOURCE_DIR@/docs/cite.md \
@CMAKE_SOURCE_DIR@/docs/ \
@CMAKE_SOURCE_DIR@/src/adiar/adiar.h \
@CMAKE_SOURCE_DIR@/src/adiar/functional.h \
@CMAKE_SOURCE_DIR@/src/adiar/access_mode.h \
@CMAKE_SOURCE_DIR@/src/adiar/memory_mode.h \
@CMAKE_SOURCE_DIR@/src/adiar/quantify_mode.h \
@CMAKE_SOURCE_DIR@/src/adiar/functional.h \
@CMAKE_SOURCE_DIR@/src/adiar/bdd.h \
@CMAKE_SOURCE_DIR@/src/adiar/bdd/bdd.h \
@CMAKE_SOURCE_DIR@/src/adiar/zdd.h \
4 changes: 2 additions & 2 deletions example/knights_tour.cpp
Original file line number Diff line number Diff line change
@@ -25,7 +25,7 @@ size_t largest_nodes = 1;
* finally by time. Most importantly, this means that any "snapshot" of the
* board at a specific time-step are grouped together.
*/
inline typename adiar::zdd::label_t int_of_position(int N, int r, int c, int t = 0)
inline typename adiar::zdd::label_type int_of_position(int N, int r, int c, int t = 0)
{
return (N * N * t) + (N * r) + c;
}
@@ -425,7 +425,7 @@ int main(int argc, char* argv[])

// ===== ADIAR =====
// Print statistics, if compiled with those flags.
adiar::adiar_printstat();
adiar::statistics_print();

// Close all of Adiar down again
adiar::adiar_deinit();
22 changes: 11 additions & 11 deletions example/queens.cpp
Original file line number Diff line number Diff line change
@@ -20,7 +20,7 @@ size_t largest_nodes = 0;
*
* N*i + j.
*/
inline typename adiar::bdd::label_t label_of_position(uint64_t N, uint64_t i, uint64_t j)
inline typename adiar::bdd::label_type label_of_position(uint64_t N, uint64_t i, uint64_t j)
{
return (N * i) + j;
}
@@ -83,7 +83,7 @@ adiar::bdd n_queens_S(int i, int j)
// On row of the queen in question
int column = N - 1;
do {
typename adiar::bdd::label_t label = label_of_position(N, row, column);
typename adiar::bdd::label_type label = label_of_position(N, row, column);

// If (row, column) == (i,j), then the chain goes through high because
// then we need to check the queen actually is placed here.
@@ -220,12 +220,12 @@ void n_queens_print_solution(std::vector<uint64_t>& assignment)

/* At this point, we now also need to convert an assignment back into a position
* on the board. So, we'll also need the following two small functions. */
inline uint64_t i_of_label(uint64_t N, typename adiar::bdd::label_t label)
inline uint64_t i_of_label(uint64_t N, typename adiar::bdd::label_type label)
{
return label / N;
}

inline uint64_t j_of_label(uint64_t N, typename adiar::bdd::label_t label)
inline uint64_t j_of_label(uint64_t N, typename adiar::bdd::label_type label)
{
return label % N;
}
@@ -237,7 +237,7 @@ uint64_t n_queens_list(uint64_t N, uint64_t column,
std::vector<uint64_t>& partial_assignment,
const adiar::bdd& constraints)
{
if (adiar::is_false(constraints)) {
if (adiar::bdd_isfalse(constraints)) {
return 0;
}
deepest_column = std::max(deepest_column, column);
@@ -248,15 +248,15 @@ uint64_t n_queens_list(uint64_t N, uint64_t column,
partial_assignment.push_back(row_q);

// Construct the assignment for this entire column
adiar::shared_file<adiar::map_pair<adiar::bdd::label_t, adiar::assignment>> column_assignment;
adiar::shared_file<adiar::map_pair<adiar::bdd::label_type, adiar::assignment>> column_assignment;

{ // The assignment_writer has to be detached, before we call any bdd
// functions. It is automatically detached upon destruction, hence we have
// it in this little scope.
adiar::file_writer<adiar::map_pair<adiar::bdd::label_t, adiar::assignment>> aw(column_assignment);
adiar::file_writer<adiar::map_pair<adiar::bdd::label_type, adiar::assignment>> aw(column_assignment);

for (uint64_t row = 0; row < N; row++) {
aw << adiar::map_pair<adiar::bdd::label_t, adiar::assignment>(label_of_position(N, row, column), row == row_q);
aw << adiar::map_pair<adiar::bdd::label_type, adiar::assignment>(label_of_position(N, row, column), row == row_q);
}
}

@@ -272,7 +272,7 @@ uint64_t n_queens_list(uint64_t N, uint64_t column,

// Obtain the lexicographically minimal true assignment. Well, only one
// exists, so we get the only one left.
adiar::bdd_satmin(restricted_constraints, [&N, &partial_assignment](adiar::bdd::label_t x, bool v) {
adiar::bdd_satmin(restricted_constraints, [&N, &partial_assignment](adiar::bdd::label_type x, bool v) {
// Skip all empty (false) locations
if (!v) { return; }

@@ -284,7 +284,7 @@ uint64_t n_queens_list(uint64_t N, uint64_t column,
for (uint64_t c = N-1; c > column; c--) {
partial_assignment.pop_back();
}
} else if (adiar::is_true(restricted_constraints)) {
} else if (adiar::bdd_istrue(restricted_constraints)) {
n_queens_print_solution(partial_assignment);
solutions += 1;
} else {
@@ -412,7 +412,7 @@ int main(int argc, char* argv[])

// ===== ADIAR =====
// Print statistics, if compiled with those flags.
adiar::adiar_printstat();
adiar::statistics_print();

// Close all of Adiar down again
adiar::adiar_deinit();
2 changes: 1 addition & 1 deletion src/adiar/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -10,7 +10,6 @@ set(HEADERS
assignment.h
bool_op.h
builder.h
data.h
deprecated.h
domain.h
exception.h
@@ -34,6 +33,7 @@ set(HEADERS

# adiar/internal
internal/assert.h
internal/bool_op.h
internal/block_size.h
internal/cnl.h
internal/cut.h
2 changes: 1 addition & 1 deletion src/adiar/access_mode.cpp
Original file line number Diff line number Diff line change
@@ -2,5 +2,5 @@

namespace adiar
{
access_mode_t access_mode = access_mode_t::AUTO;
access_mode_t access_mode = access_mode_t::Auto;
}
26 changes: 13 additions & 13 deletions src/adiar/access_mode.h
Original file line number Diff line number Diff line change
@@ -19,33 +19,33 @@ namespace adiar
/// \{

//////////////////////////////////////////////////////////////////////////////
/// \brief Whether Adiar should exclusively use random access (RA) or
/// priority queues (PQ) or automatically pick either way based on
/// size of input.
/// \brief Whether Adiar should exclusively use random access
/// (`Random_Access`) or priority queues (`Priority_Queue`) or
/// automatically pick either way based on the width of inputs.
///
/// \details
/// | Enum Value | Effect |
/// |------------|------------------------------------------------|
/// | `AUTO` | Automatically decide on type of access to use. |
/// | `RA` | Always use *random access*. |
/// | `PQ` | Always use *priority queues*. |
/// | Enum Value | Effect |
/// |------------------|------------------------------------------------|
/// | `Auto` | Automatically decide on type of access to use. |
/// | `Random_Access` | Always use *random access*. |
/// | `Priority_Queue` | Always use *priority queues*. |
//////////////////////////////////////////////////////////////////////////////
enum class access_mode_t { AUTO, RA, PQ };
enum class access_mode_t { Auto, Random_Access, Priority_Queue };

//////////////////////////////////////////////////////////////////////////////
/// \brief The current access mode (default: `AUTO`).
/// \brief The current access mode (default: `Auto`).
///
/// \details
/// If you want to force *Adiar* to a specific access mode then you should
/// set the global variable `adiar::access_mode` to one of the above three
/// values. For example, one can force *Adiar* always use random access with
/// the following piece of code.
/// ```cpp
/// adiar::access_mode = adiar::access_mode_t::RA
/// adiar::access_mode = adiar::access_mode_t::Random_Access
/// ```
///
/// \warning Using `RA` may lead to crashes if all inputs are too wide or
/// input to random access is not canonical!
/// \warning Using `Random_Access` may lead to crashes if all inputs are too
/// wide or input to random access is not canonical!
//////////////////////////////////////////////////////////////////////////////
extern access_mode_t access_mode;

17 changes: 9 additions & 8 deletions src/adiar/adiar.cpp
Original file line number Diff line number Diff line change
@@ -6,7 +6,6 @@
#include <tpie/memory.h>
#include <tpie/tempname.h>

#include <adiar/domain.h>
#include <adiar/internal/assert.h>
#include <adiar/internal/block_size.h>
#include <adiar/internal/memory.h>
@@ -27,9 +26,9 @@ namespace adiar
if (!_adiar_initialized && _tpie_initialized) {
throw runtime_error("Adiar cannot be initialized after call to 'adiar_deinit()'");
}
if (memory_limit_bytes < MINIMUM_MEMORY) {
if (memory_limit_bytes < minimum_memory) {
throw invalid_argument("Adiar requires at least "
+ std::to_string(MINIMUM_MEMORY / 1024 / 1024)
+ std::to_string(minimum_memory / 1024 / 1024)
+ " MiB of memory");
}

@@ -54,12 +53,14 @@ namespace adiar

// Initialise Adiar state
// - reset statistics
adiar_statsreset();
statistics_reset();

// - reset memory moyde
memory_mode = memory_mode_t::AUTO;
// - reset enum settings
access_mode = access_mode_t::Auto;
memory_mode = memory_mode_t::Auto;
quantify_mode = quantify_mode_t::Auto;

// - all done, mark iniitialized
// - all done, mark initialized
_adiar_initialized = true;
} catch (const std::exception &e) {
// LCOV_EXCL_START
@@ -85,7 +86,7 @@ namespace adiar
{
if (!_adiar_initialized) return;

adiar_unset_domain();
domain_unset();

tpie::tpie_finish(tpie::ALL);
_adiar_initialized = false;
23 changes: 14 additions & 9 deletions src/adiar/adiar.h
Original file line number Diff line number Diff line change
@@ -10,21 +10,26 @@
#include <string>

////////////////////////////////////////////////////////////////////////////////
/// Core
#include <adiar/access_mode.h>
#include <adiar/assignment.h>
#include <adiar/builder.h>
#include <adiar/domain.h>
/// Core types
#include <adiar/exception.h>
#include <adiar/file.h>
#include <adiar/functional.h>
#include <adiar/file.h> // <-- TODO: Remove!

////////////////////////////////////////////////////////////////////////////////
/// Core Settings
#include <adiar/access_mode.h>
#include <adiar/memory_mode.h>
#include <adiar/quantify_mode.h>

////////////////////////////////////////////////////////////////////////////////
/// Global Domain
#include <adiar/domain.h>

////////////////////////////////////////////////////////////////////////////////
/// Decision Diagrams
#include <adiar/bdd.h>
#include <adiar/zdd.h>
#include <adiar/builder.h>

////////////////////////////////////////////////////////////////////////////////
/// Statistics
@@ -54,21 +59,21 @@ namespace adiar
//////////////////////////////////////////////////////////////////////////////
/// \brief Minimum value of 128 MiB for the memory limit.
//////////////////////////////////////////////////////////////////////////////
constexpr size_t MINIMUM_MEMORY = 128 * 1024 * 1024;
constexpr size_t minimum_memory = 128 * 1024 * 1024;

//////////////////////////////////////////////////////////////////////////////
/// \brief Initiates Adiar with the given amount of memory (given in bytes)
///
/// \param memory_limit_bytes
/// The amount of internal memory (in bytes) that Adiar is allowed to use.
/// This has to be at least MINIMUM_BYTES.
/// This has to be at least minimum_memory.
///
/// \param temp_dir
/// The directory in which to place all temporary files. Default on Linux is
/// the */tmp* library.
///
/// \throws invalid_argument If `memory_limit_bytes` is set to a value less
/// than the `MINIMUM_MEMORY` required.
/// than the `minimum_memory` required.
///
/// \throws runtime_error If `adiar_init()` and then `adiar_deinit()` have
/// been called previously.
Loading