Trait 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.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors