Trait oxidd_core::function::BooleanFunction

pub trait BooleanFunction: Function {
    // Required methods
    fn new_var<'id>(manager: &mut Self::Manager<'id>) -> AllocResult<Self>;
    fn f_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
    fn t_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
    fn not_edge<'id>(
        manager: &Self::Manager<'id>,
        edge: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn and_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn or_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn nand_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn nor_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn xor_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn equiv_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn imp_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn imp_strict_edge<'id>(
        manager: &Self::Manager<'id>,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn sat_count_edge<'id, N: SatCountNumber, S: BuildHasher>(
        manager: &Self::Manager<'id>,
        edge: &EdgeOfFunc<'id, Self>,
        vars: LevelNo,
        cache: &mut SatCountCache<N, S>,
    ) -> N;
    fn pick_cube_edge<'id, 'a, I>(
        manager: &'a Self::Manager<'id>,
        edge: &'a EdgeOfFunc<'id, Self>,
        order: impl IntoIterator<IntoIter = I>,
        choice: impl FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>) -> bool,
    ) -> Option<Vec<OptBool>>
       where I: ExactSizeIterator<Item = &'a EdgeOfFunc<'id, Self>>;
    fn eval_edge<'id, 'a>(
        manager: &'a Self::Manager<'id>,
        edge: &'a EdgeOfFunc<'id, Self>,
        args: impl IntoIterator<Item = (Borrowed<'a, EdgeOfFunc<'id, Self>>, bool)>,
    ) -> bool;

    // Provided methods
    fn f<'id>(manager: &Self::Manager<'id>) -> Self { ... }
    fn t<'id>(manager: &Self::Manager<'id>) -> Self { ... }
    fn cofactors(&self) -> Option<(Self, Self)> { ... }
    fn cofactor_true(&self) -> Option<Self> { ... }
    fn cofactor_false(&self) -> Option<Self> { ... }
    fn not(&self) -> AllocResult<Self> { ... }
    fn not_owned(self) -> AllocResult<Self> { ... }
    fn and(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn or(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn nand(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn nor(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn xor(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn equiv(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn imp(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn imp_strict(&self, rhs: &Self) -> AllocResult<Self> { ... }
    fn cofactors_edge<'a, 'id>(
        manager: &'a Self::Manager<'id>,
        f: &'a EdgeOfFunc<'id, Self>,
    ) -> Option<(Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>)> { ... }
    fn cofactors_node<'a, 'id>(
        tag: ETagOfFunc<'id, Self>,
        node: &'a INodeOfFunc<'id, Self>,
    ) -> (Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>) { ... }
    fn not_edge_owned<'id>(
        manager: &Self::Manager<'id>,
        edge: EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>> { ... }
    fn satisfiable(&self) -> bool { ... }
    fn valid(&self) -> bool { ... }
    fn ite(&self, then_case: &Self, else_case: &Self) -> AllocResult<Self> { ... }
    fn ite_edge<'id>(
        manager: &Self::Manager<'id>,
        if_edge: &EdgeOfFunc<'id, Self>,
        then_edge: &EdgeOfFunc<'id, Self>,
        else_edge: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>> { ... }
    fn sat_count<N: SatCountNumber, S: BuildHasher>(
        &self,
        vars: LevelNo,
        cache: &mut SatCountCache<N, S>,
    ) -> N { ... }
    fn pick_cube<'a, I: ExactSizeIterator<Item = &'a Self>>(
        &'a self,
        order: impl IntoIterator<IntoIter = I>,
        choice: impl for<'id> FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>) -> bool,
    ) -> Option<Vec<OptBool>> { ... }
    fn pick_cube_uniform<'a, I: ExactSizeIterator<Item = &'a Self>, S: BuildHasher>(
        &'a self,
        order: impl IntoIterator<IntoIter = I>,
        cache: &mut SatCountCache<F64, S>,
        rng: &mut Rng,
    ) -> Option<Vec<OptBool>> { ... }
    fn pick_cube_uniform_edge<'id, 'a, I, S>(
        manager: &'a Self::Manager<'id>,
        edge: &'a EdgeOfFunc<'id, Self>,
        order: impl IntoIterator<IntoIter = I>,
        cache: &mut SatCountCache<F64, S>,
        rng: &mut Rng,
    ) -> Option<Vec<OptBool>>
       where I: ExactSizeIterator<Item = &'a EdgeOfFunc<'id, Self>>,
             S: BuildHasher { ... }
    fn eval<'a>(
        &'a self,
        args: impl IntoIterator<Item = (&'a Self, bool)>,
    ) -> bool { ... }
}

Boolean functions 𝔹ⁿ → 𝔹

As a user of this trait, you are probably most interested in methods like Self::not(), Self::and(), and Self::or(). As an implementor, it suffices to implement the functions operating on edges.

Required Methods

fn new_var<'id>(manager: &mut Self::Manager<'id>) -> AllocResult<Self>

Get a fresh variable, i.e., a function that is true if and only if the variable is true. This adds a new level to a decision diagram.

fn f_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>

Get the always false function ⊥ as edge

fn t_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>

Get the always true function ⊤ as edge

fn not_edge<'id>( manager: &Self::Manager<'id>, edge: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the negation ¬edge, edge version

fn and_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the conjunction lhs ∧ rhs, edge version

fn or_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the disjunction lhs ∨ rhs, edge version

fn nand_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the negated conjunction lhs ⊼ rhs, edge version

fn nor_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the negated disjunction lhs ⊽ rhs, edge version

fn xor_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the exclusive disjunction lhs ⊕ rhs, edge version

fn equiv_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the equivalence lhs ↔ rhs, edge version

fn imp_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the implication lhs → rhs, edge version

fn imp_strict_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the strict implication lhs < rhs, edge version

fn sat_count_edge<'id, N: SatCountNumber, S: BuildHasher>( manager: &Self::Manager<'id>, edge: &EdgeOfFunc<'id, Self>, vars: LevelNo, cache: &mut SatCountCache<N, S>, ) -> N

Edge version of Self::sat_count()

fn pick_cube_edge<'id, 'a, I>( manager: &'a Self::Manager<'id>, edge: &'a EdgeOfFunc<'id, Self>, order: impl IntoIterator<IntoIter = I>, choice: impl FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>) -> bool, ) -> Option<Vec<OptBool>>

where I: ExactSizeIterator<Item = &'a EdgeOfFunc<'id, Self>>,

Edge version of Self::pick_cube()

fn eval_edge<'id, 'a>( manager: &'a Self::Manager<'id>, edge: &'a EdgeOfFunc<'id, Self>, args: impl IntoIterator<Item = (Borrowed<'a, EdgeOfFunc<'id, Self>>, bool)>, ) -> bool

Edge version of Self::eval()

Provided Methods

fn f<'id>(manager: &Self::Manager<'id>) -> Self

Get the always false function ⊥

fn t<'id>(manager: &Self::Manager<'id>) -> Self

Get the always true function ⊤

fn cofactors(&self) -> Option<(Self, Self)>

Get the cofactors (f_true, f_false) of self

Let f(x₀, …, xₙ) be represented by self, where x₀ is (currently) the top-most variable. Then f_true(x₁, …, xₙ) = f(⊤, x₁, …, xₙ) and f_false(x₁, …, xₙ) = f(⊥, x₁, …, xₙ).

Note that the domain of f is 𝔹ⁿ⁺¹ while the domain of f_true and f_false is 𝔹ⁿ. This is irrelevant in case of BDDs and BCDDs, but not for ZBDDs: For instance, g(x₀) = x₀ and g’(x₀, x₁) = x₀ have the same representation as BDDs or BCDDs, but different representations as ZBDDs.

Structurally, the cofactors are simply the children in case of BDDs and ZBDDs. (For BCDDs, the edge tags are adjusted accordingly.) On these representations, runtime is thus in O(1).

Returns None iff self references a terminal node. If you only need f_true or f_false, Self::cofactor_true or Self::cofactor_false are slightly more efficient.

Locking behavior: acquires the manager’s lock for shared access.

fn cofactor_true(&self) -> Option<Self>

Get the cofactor f_true of self

This method is slightly more efficient than Self::cofactors in case f_false is not needed.

For a more detailed description, see Self::cofactors.

Returns None iff self references a terminal node.

Locking behavior: acquires the manager’s lock for shared access.

fn cofactor_false(&self) -> Option<Self>

Get the cofactor f_false of self

This method is slightly more efficient than Self::cofactors in case f_true is not needed.

For a more detailed description, see Self::cofactors.

Returns None iff self references a terminal node.

Locking behavior: acquires the manager’s lock for shared access.

fn not(&self) -> AllocResult<Self>

Compute the negation ¬self

Locking behavior: acquires the manager’s lock for shared access.

fn not_owned(self) -> AllocResult<Self>

Compute the negation ¬self, owned version

Compared to Self::not(), this method does not need to clone the function, so when the implementation is using (e.g.) complemented edges, this might be a little bit faster than Self::not().

Locking behavior: acquires the manager’s lock for shared access.

fn and(&self, rhs: &Self) -> AllocResult<Self>

Compute the conjunction self ∧ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

fn or(&self, rhs: &Self) -> AllocResult<Self>

Compute the disjunction self ∨ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

fn nand(&self, rhs: &Self) -> AllocResult<Self>

Compute the negated conjunction self ⊼ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

fn nor(&self, rhs: &Self) -> AllocResult<Self>

Compute the negated disjunction self ⊽ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

fn xor(&self, rhs: &Self) -> AllocResult<Self>

Compute the exclusive disjunction self ⊕ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

fn equiv(&self, rhs: &Self) -> AllocResult<Self>

Compute the equivalence self ↔ rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

fn imp(&self, rhs: &Self) -> AllocResult<Self>

Compute the implication self → rhs (or self ≤ rhs)

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

fn imp_strict(&self, rhs: &Self) -> AllocResult<Self>

Compute the strict implication self < rhs

Locking behavior: acquires the manager’s lock for shared access.

Panics if self and rhs don’t belong to the same manager.

fn cofactors_edge<'a, 'id>( manager: &'a Self::Manager<'id>, f: &'a EdgeOfFunc<'id, Self>, ) -> Option<(Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>)>

Get the cofactors (f_true, f_false) of f, edge version

Returns None iff f references a terminal node. For more details on the semantics of f_true and f_false, see Self::cofactors.

fn cofactors_node<'a, 'id>( tag: ETagOfFunc<'id, Self>, node: &'a INodeOfFunc<'id, Self>, ) -> (Borrowed<'a, EdgeOfFunc<'id, Self>>, Borrowed<'a, EdgeOfFunc<'id, Self>>)

Get the cofactors (f_true, f_false) of node, assuming an incoming edge with EdgeTag

Returns None iff f references a terminal node. For more details on the semantics of f_true and f_false, see Self::cofactors.

Implementation note: The default implementation assumes that cofactor 0 corresponds to f_true and cofactor 1 corresponds to f_false.

fn not_edge_owned<'id>( manager: &Self::Manager<'id>, edge: EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the negation ¬edge, owned edge version

Compared to Self::not_edge(), this method does not need to clone the edge, so when the implementation is using (e.g.) complemented edges, this might be a little bit faster than Self::not_edge().

fn satisfiable(&self) -> bool

Returns true iff self is satisfiable, i.e. is not ⊥

Locking behavior: acquires the manager’s lock for shared access.

fn valid(&self) -> bool

Returns true iff self is valid, i.e. is ⊤

Locking behavior: acquires the manager’s lock for shared access.

fn ite(&self, then_case: &Self, else_case: &Self) -> AllocResult<Self>

Compute if self { then_case } else { else_case }

This is equivalent to (self ∧ then_case) ∨ (¬self ∧ else_case) but possibly more efficient than computing all the conjunctions/disjunctions.

Locking behavior: acquires the manager’s lock for shared access.

Panics if self, then_case, and else_case don’t belong to the same manager.

fn ite_edge<'id>( manager: &Self::Manager<'id>, if_edge: &EdgeOfFunc<'id, Self>, then_edge: &EdgeOfFunc<'id, Self>, else_edge: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute if if_edge { then_edge } else { else_edge } (edge version)

This is equivalent to (self ∧ then_case) ∨ (¬self ∧ else_case) but possibly more efficient than computing all the conjunctions/disjunctions.

fn sat_count<N: SatCountNumber, S: BuildHasher>( &self, vars: LevelNo, cache: &mut SatCountCache<N, S>, ) -> N

Count the number of satisfying assignments, assuming vars input variables

The cache can be used to speed up multiple model counting operations for functions in the same decision diagram. If the model counts of just one function are of interest, one may simply pass an empty SatCountCache (using &mut SatCountCache::default()). The cache will automatically be invalidated in case there have been reordering operations or vars changed since the last query (see SatCountCache::clear_if_invalid()). Still, it is the caller’s responsibility to not use the cache for different managers.

Locking behavior: acquires the manager’s lock for shared access.

fn pick_cube<'a, I: ExactSizeIterator<Item = &'a Self>>( &'a self, order: impl IntoIterator<IntoIter = I>, choice: impl for<'id> FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>) -> bool, ) -> Option<Vec<OptBool>>

Pick a cube of this function

order is a list of variables. If it is non-empty, it must contain as many variables as there are levels.

Returns None if the function is false. Otherwise, this method returns a vector where the i-th entry indicates if the i-th variable of order (or the variable currently at the i-th level in case order is empty) is true, false, or “don’t care”.

Whenever there is a choice for a variable, choice is called to determine the valuation for this variable. The Edge argument is guaranteed to point to an inner node. (We pass an Edge and not an InnerNode reference since Edges provide more information, e.g., the NodeID.)

Locking behavior: acquires the manager’s lock for shared access.

fn pick_cube_uniform<'a, I: ExactSizeIterator<Item = &'a Self>, S: BuildHasher>( &'a self, order: impl IntoIterator<IntoIter = I>, cache: &mut SatCountCache<F64, S>, rng: &mut Rng, ) -> Option<Vec<OptBool>>

Pick a random cube of this function, where each cube has the same probability of being chosen

order is a list of variables. If it is non-empty, it must contain as many variables as there are levels.

Returns None if the function is false. Otherwise, this method returns a vector where the i-th entry indicates if the i-th variable of order (or the variable currently at the i-th level in case order is empty) is true, false, or “don’t care”. To obtain a total valuation from this partial valuation, it suffices to pick true or false with probability ½. (Note that this function returns a partial valuation with n “don’t cares” with a probability that is 2ⁿ as high as the probability of any total valuation.)

Locking behavior: acquires the manager’s lock for shared access.

fn pick_cube_uniform_edge<'id, 'a, I, S>( manager: &'a Self::Manager<'id>, edge: &'a EdgeOfFunc<'id, Self>, order: impl IntoIterator<IntoIter = I>, cache: &mut SatCountCache<F64, S>, rng: &mut Rng, ) -> Option<Vec<OptBool>>

where I: ExactSizeIterator<Item = &'a EdgeOfFunc<'id, Self>>, S: BuildHasher,

Edge version of Self::pick_cube_uniform()

fn eval<'a>(&'a self, args: impl IntoIterator<Item = (&'a Self, bool)>) -> bool

Evaluate this Boolean function

args determines the valuation for all variables. Missing values are assumed to be false. However, note that the arguments may also determine the domain, e.g., in case of ZBDDs. If values are specified multiple times, the last one counts. Panics if any function in args refers to a terminal node.

Locking behavior: acquires the manager’s lock for shared access.

Object Safety

This trait is not object safe.

Implementors