Trait oxidd_core::function::BooleanFunctionQuant

pub trait BooleanFunctionQuant: BooleanFunction {
    // Required methods
    fn restrict_edge<'id>(
        manager: &Self::Manager<'id>,
        root: &EdgeOfFunc<'id, Self>,
        vars: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn forall_edge<'id>(
        manager: &Self::Manager<'id>,
        root: &EdgeOfFunc<'id, Self>,
        vars: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn exist_edge<'id>(
        manager: &Self::Manager<'id>,
        root: &EdgeOfFunc<'id, Self>,
        vars: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
    fn unique_edge<'id>(
        manager: &Self::Manager<'id>,
        root: &EdgeOfFunc<'id, Self>,
        vars: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>>;

    // Provided methods
    fn restrict(&self, vars: &Self) -> AllocResult<Self> { ... }
    fn forall(&self, vars: &Self) -> AllocResult<Self> { ... }
    fn exist(&self, vars: &Self) -> AllocResult<Self> { ... }
    fn unique(&self, vars: &Self) -> AllocResult<Self> { ... }
}

Quantification extension for BooleanFunction

Required Methods

fn restrict_edge<'id>( manager: &Self::Manager<'id>, root: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Restrict a set of vars to constant values, edge version

See Self::restrict() for more details.

fn forall_edge<'id>( manager: &Self::Manager<'id>, root: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the universal quantification of root over vars, edge version

See Self::forall() for more details.

fn exist_edge<'id>( manager: &Self::Manager<'id>, root: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the existential quantification of root over vars, edge version

See Self::exist() for more details.

fn unique_edge<'id>( manager: &Self::Manager<'id>, root: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the unique quantification of root over vars, edge version

See Self::unique() for more details.

Provided Methods

fn restrict(&self, vars: &Self) -> AllocResult<Self>

Restrict a set of vars to constant values

vars conceptually is a partial assignment, represented as the conjunction of positive or negative literals, depending on whether the variable should be mapped to true or false.

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

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

fn forall(&self, vars: &Self) -> AllocResult<Self>

Compute the universal quantification over vars

vars is a set of variables, which in turn is just the conjunction of the variables. This operation removes all occurrences of the variables by universal quantification. Universal quantification ∀x. f(…, x, …) of a boolean function f(…, x, …) over a single variable x is f(…, 0, …) ∧ f(…, 1, …).

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

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

fn exist(&self, vars: &Self) -> AllocResult<Self>

Compute the existential quantification over vars

vars is a set of variables, which in turn is just the conjunction of the variables. This operation removes all occurrences of the variables by existential quantification. Existential quantification ∃x. f(…, x, …) of a boolean function f(…, x, …) over a single variable x is f(…, 0, …) ∨ f(…, 1, …).

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

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

fn unique(&self, vars: &Self) -> AllocResult<Self>

Compute the unique quantification over vars

vars is a set of variables, which in turn is just the conjunction of the variables. This operation removes all occurrences of the variables by unique quantification. Unique quantification ∃!x. f(…, x, …) of a boolean function f(…, x, …) over a single variable x is f(…, 0, …) ⊕ f(…, 1, …).

Unique quantification is also known as the Boolean difference or Boolean derivative.

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

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

Object Safety

This trait is not object safe.

Implementors