Trait BooleanFunctionQuant

Source
pub trait BooleanFunctionQuant: BooleanFunction {
Show 18 methods // 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 exists_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 exists(&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_exists( &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 exist_edge<'id>( manager: &Self::Manager<'id>, root: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, 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_exists_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>> { ... }
}
Expand description

Quantification extension for BooleanFunction

Required Methods§

Source

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.

Source

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.

Source

fn exists_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::exists() for more details.

Source

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§

Source

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.

Source

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.

Source

fn exists(&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.

Source

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

👎Deprecated

Deprecated alias for Self::exists()

Source

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.

Source

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.

Source

fn apply_exists( &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.

Source

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

👎Deprecated

Deprecated alias for Self::apply_exists()

Source

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.

Source

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

👎Deprecated

Deprecated alias for Self::exists_edge()

Source

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.

Source

fn apply_exists_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.

Source

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

👎Deprecated

Deprecated alias for Self::apply_exists_edge()

Source

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.

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§