Skip to content

Commit

Permalink
Rephrase locking behavior docs
Browse files Browse the repository at this point in the history
  • Loading branch information
@nhusung
nhusung committed Apr 30, 2024
1 parent 8c5507f commit 67f8838
Show file tree
Hide file tree
Showing 9 changed files with 218 additions and 218 deletions.
52 changes: 26 additions & 26 deletions bindings/cpp/include/oxidd/bcdd.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ class bcdd_manager {
///
/// `this` must not be invalid (check via is_invalid()).
///
/// Locking behavior: acquires an exclusive manager lock.
/// Locking behavior: acquires the manager's lock for exclusive access.
///
/// @returns The BCDD function representing the variable
[[nodiscard]] bcdd_function new_var() noexcept;
Expand All @@ -126,7 +126,7 @@ class bcdd_manager {
///
/// `this` must not be invalid (check via is_invalid()).
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(1)
///
Expand All @@ -136,7 +136,7 @@ class bcdd_manager {
///
/// `this` must not be invalid (check via is_invalid()).
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(1)
///
Expand All @@ -151,7 +151,7 @@ class bcdd_manager {
///
/// `this` must not be invalid (check via is_invalid()).
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// @returns The number of inner nodes
[[nodiscard]] size_t num_inner_nodes() const noexcept {
Expand Down Expand Up @@ -302,7 +302,7 @@ class bcdd_function {
/// cofactor_true() or cofactor_false(). These functions are slightly more
/// efficient then.
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(1)
///
Expand All @@ -318,7 +318,7 @@ class bcdd_function {
/// This function is slightly more efficient than cofactors() in case
/// `f_false` is not needed.
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(1)
///
Expand All @@ -332,7 +332,7 @@ class bcdd_function {
/// This function is slightly more efficient than cofactors() in case `f_true`
/// is not needed.
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(1)
///
Expand All @@ -344,7 +344,7 @@ class bcdd_function {

/// Compute the BCDD for the negation `¬this`
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(1)
///
Expand All @@ -354,7 +354,7 @@ class bcdd_function {
}
/// Compute the BCDD for the conjunction `lhs ∧ rhs`
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(|lhs| · |rhs|)
///
Expand All @@ -370,7 +370,7 @@ class bcdd_function {
}
/// Compute the BCDD for the disjunction `lhs ∨ rhs`
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(|lhs| · |rhs|)
///
Expand All @@ -386,7 +386,7 @@ class bcdd_function {
}
/// Compute the BCDD for the exclusive disjunction `lhs ⊕ rhs`
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(|lhs| · |rhs|)
///
Expand All @@ -402,7 +402,7 @@ class bcdd_function {
}
/// Compute the BCDD for the negated conjunction `this ⊼ rhs`
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(|this| · |rhs|)
///
Expand All @@ -413,7 +413,7 @@ class bcdd_function {
}
/// Compute the BCDD for the negated disjunction `this ⊽ rhs`
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(|this| · |rhs|)
///
Expand All @@ -424,7 +424,7 @@ class bcdd_function {
}
/// Compute the BCDD for the equivalence `this ↔ rhs`
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(|this| · |rhs|)
///
Expand All @@ -435,7 +435,7 @@ class bcdd_function {
}
/// Compute the BCDD for the implication `this → rhs` (or `this ≤ rhs`)
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(|this| · |rhs|)
///
Expand All @@ -446,7 +446,7 @@ class bcdd_function {
}
/// Compute the BCDD for the strict implication `this < rhs`
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(|this| · |rhs|)
///
Expand All @@ -458,7 +458,7 @@ class bcdd_function {
}
/// Compute the BCDD for the conditional `this ? t : e`
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// Runtime complexity: O(|this| · |t| · |e|)
///
Expand All @@ -476,7 +476,7 @@ class bcdd_function {
/// universal quantification. Universal quantification of a Boolean function
/// `f(…, x, …)` over a single variable `x` is `f(…, 0, …) ∧ f(…, 1, …)`.
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// @returns The BCDD function (may be invalid if the operation runs out of
/// memory)
Expand All @@ -491,7 +491,7 @@ class bcdd_function {
/// function `f(…, x, …)` over a single variable `x` is
/// `f(…, 0, …) ∨ f(…, 1, …)`.
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// @returns The BCDD function (may be invalid if the operation runs out of
/// memory)
Expand All @@ -505,7 +505,7 @@ class bcdd_function {
/// unique quantification. Unique quantification of a Boolean function
/// `f(…, x, …)` over a single variable `x` is `f(…, 0, …) ⊕ f(…, 1, …)`.
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// @returns The BCDD function (may be invalid if the operation runs out of
/// memory)
Expand All @@ -521,7 +521,7 @@ class bcdd_function {
///
/// `this` must not be invalid (check via is_invalid()).
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// @returns Node count including the terminal node
[[nodiscard]] std::size_t node_count() const noexcept {
Expand All @@ -533,7 +533,7 @@ class bcdd_function {
///
/// `this` must not be invalid (check via is_invalid()).
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// @returns `true` iff there is a satisfying assignment
[[nodiscard]] bool satisfiable() const noexcept {
Expand All @@ -546,7 +546,7 @@ class bcdd_function {
/// `this` must not be invalid (in the technical, not the mathematical sense).
/// Check via is_invalid().
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// @returns `true` iff there is are only satisfying assignment
[[nodiscard]] bool valid() const noexcept {
Expand All @@ -558,7 +558,7 @@ class bcdd_function {
///
/// `this` must not be invalid (check via is_invalid()).
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// @returns Count of satisfying assignments
[[nodiscard]] double sat_count_double(level_no_t vars) const noexcept {
Expand All @@ -570,7 +570,7 @@ class bcdd_function {
///
/// `this` must not be invalid (check via is_invalid()).
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// @returns A satisfying assignment if there exists one. If this function is
/// unsatisfiable, the assignment is empty.
Expand All @@ -585,7 +585,7 @@ class bcdd_function {
/// assumed to be false. The order is irrelevant. All elements must point to
/// inner nodes.
///
/// Locking behavior: acquires a shared manager lock.
/// Locking behavior: acquires the manager's lock for shared access.
///
/// @param args Slice of pairs `(variable, value)`, where all variables are
/// not invalid
Expand Down
Loading

0 comments on commit 67f8838

Please sign in to comment.