Trait 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> { ... }
    fn apply_forall(
        &self,
        op: BooleanOperator,
        rhs: &Self,
        vars: &Self,
    ) -> AllocResult<Self> { ... }
    fn apply_exist(
        &self,
        op: BooleanOperator,
        rhs: &Self,
        vars: &Self,
    ) -> AllocResult<Self> { ... }
    fn apply_unique(
        &self,
        op: BooleanOperator,
        rhs: &Self,
        vars: &Self,
    ) -> AllocResult<Self> { ... }
    fn apply_forall_edge<'id>(
        manager: &Self::Manager<'id>,
        op: BooleanOperator,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
        vars: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>> { ... }
    fn apply_exist_edge<'id>(
        manager: &Self::Manager<'id>,
        op: BooleanOperator,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
        vars: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, Self>> { ... }
    fn apply_unique_edge<'id>(
        manager: &Self::Manager<'id>,
        op: BooleanOperator,
        lhs: &EdgeOfFunc<'id, Self>,
        rhs: &EdgeOfFunc<'id, Self>,
        vars: &EdgeOfFunc<'id, Self>,
    ) -> AllocResult<EdgeOfFunc<'id, 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.

fn apply_forall( &self, op: BooleanOperator, rhs: &Self, vars: &Self, ) -> AllocResult<Self>

Combined application of op and quantification ∀x. self <op> rhs, where <op> is any of the operations from BooleanOperator

See also Self::forall() and the trait BooleanFunction for more details.

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

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

fn apply_exist( &self, op: BooleanOperator, rhs: &Self, vars: &Self, ) -> AllocResult<Self>

Combined application of op and quantification ∃x. self <op> rhs, where <op> is any of the operations from BooleanOperator

See also Self::exist() and the trait BooleanFunction for more details.

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

fn apply_unique( &self, op: BooleanOperator, rhs: &Self, vars: &Self, ) -> AllocResult<Self>

Combined application of op and quantification ∃!x. self <op> rhs, where <op> is any of the operations from BooleanOperator

See also Self::unique() and the trait BooleanFunction for more details.

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

fn apply_forall_edge<'id>( manager: &Self::Manager<'id>, op: BooleanOperator, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Combined application of op and forall quantification, edge version

See Self::apply_forall() for more details.

fn apply_exist_edge<'id>( manager: &Self::Manager<'id>, op: BooleanOperator, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Combined application of op and existential quantification, edge version

See Self::apply_exist() for more details.

fn apply_unique_edge<'id>( manager: &Self::Manager<'id>, op: BooleanOperator, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Combined application of op and unique quantification, edge version

See Self::apply_unique() for more details.

Object Safety

This trait is not object safe.

Implementors