Trait oxidd_core::function::FunctionSubst

pub trait FunctionSubst: Function {
    // Required method
    fn substitute_edge<'id, 'a>(
        manager: &'a Self::Manager<'id>,
        edge: &'a EdgeOfFunc<'id, Self>,
        substitution: impl Substitution<Var = Borrowed<'a, EdgeOfFunc<'id, Self>>, Replacement = Borrowed<'a, EdgeOfFunc<'id, Self>>>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;

    // Provided method
    fn substitute<'a>(
        &'a self,
        substitution: impl Substitution<Var = &'a Self, Replacement = &'a Self>,
    ) -> AllocResult<Self> { ... }
}

Substitution extension for Function

Required Methods

fn substitute_edge<'id, 'a>( manager: &'a Self::Manager<'id>, edge: &'a EdgeOfFunc<'id, Self>, substitution: impl Substitution<Var = Borrowed<'a, EdgeOfFunc<'id, Self>>, Replacement = Borrowed<'a, EdgeOfFunc<'id, Self>>>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Edge version of Self::substitute()

Provided Methods

fn substitute<'a>( &'a self, substitution: impl Substitution<Var = &'a Self, Replacement = &'a Self>, ) -> AllocResult<Self>

Substitute variables in self according to substitution

The substitution is performed in a parallel fashion, e.g.: (¬x ∧ ¬y)[x ↦ ¬x ∧ ¬y, y ↦ ⊥] = ¬(¬x ∧ ¬y) ∧ ¬⊥ = x ∨ y

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

Panics if self and the function in substitution don’t belong to the same manager.

Object Safety

This trait is not object safe.

Implementors