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§
Sourcefn restrict_edge<'id>(
manager: &Self::Manager<'id>,
root: &EdgeOfFunc<'id, Self>,
vars: &EdgeOfFunc<'id, Self>,
) -> AllocResult<EdgeOfFunc<'id, Self>>
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.
Sourcefn forall_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>>
Compute the universal quantification of root
over vars
, edge
version
See Self::forall()
for more details.
Sourcefn exists_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>>
Compute the existential quantification of root
over vars
, edge
version
See Self::exists()
for more details.
Sourcefn unique_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>>
Compute the unique quantification of root
over vars
, edge version
See Self::unique()
for more details.
Provided Methods§
Sourcefn restrict(&self, vars: &Self) -> AllocResult<Self>
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.
Sourcefn forall(&self, vars: &Self) -> AllocResult<Self>
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.
Sourcefn exists(&self, vars: &Self) -> AllocResult<Self>
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.
Sourcefn exist(&self, vars: &Self) -> AllocResult<Self>
👎Deprecated
fn exist(&self, vars: &Self) -> AllocResult<Self>
Deprecated alias for Self::exists()
Sourcefn unique(&self, vars: &Self) -> AllocResult<Self>
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.
Sourcefn apply_forall(
&self,
op: BooleanOperator,
rhs: &Self,
vars: &Self,
) -> AllocResult<Self>
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.
Sourcefn apply_exists(
&self,
op: BooleanOperator,
rhs: &Self,
vars: &Self,
) -> AllocResult<Self>
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.
Sourcefn apply_exist(
&self,
op: BooleanOperator,
rhs: &Self,
vars: &Self,
) -> AllocResult<Self>
👎Deprecated
fn apply_exist( &self, op: BooleanOperator, rhs: &Self, vars: &Self, ) -> AllocResult<Self>
Deprecated alias for Self::apply_exists()
Sourcefn apply_unique(
&self,
op: BooleanOperator,
rhs: &Self,
vars: &Self,
) -> AllocResult<Self>
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.
Sourcefn exist_edge<'id>(
manager: &Self::Manager<'id>,
root: &EdgeOfFunc<'id, Self>,
vars: &EdgeOfFunc<'id, Self>,
) -> AllocResult<EdgeOfFunc<'id, Self>>
👎Deprecated
fn exist_edge<'id>( manager: &Self::Manager<'id>, root: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>
Deprecated alias for Self::exists_edge()
Sourcefn 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_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.
Sourcefn 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_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.
Sourcefn 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
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 alias for Self::apply_exists_edge()
Sourcefn 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>>
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.