pub enum RefinementStrategy {
None,
BlockCounterexamples,
ConflictLearning,
Generalization,
}Expand description
Refinement strategy for narrowing the search space
Variants§
None
No refinement
BlockCounterexamples
Block found counterexamples
ConflictLearning
Learn from conflicts
Generalization
Generalize from counterexamples
Trait Implementations§
Source§impl Clone for RefinementStrategy
impl Clone for RefinementStrategy
Source§fn clone(&self) -> RefinementStrategy
fn clone(&self) -> RefinementStrategy
Returns a duplicate of the value. Read more
1.0.0 · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source. Read moreSource§impl Debug for RefinementStrategy
impl Debug for RefinementStrategy
Source§impl PartialEq for RefinementStrategy
impl PartialEq for RefinementStrategy
impl Copy for RefinementStrategy
impl Eq for RefinementStrategy
impl StructuralPartialEq for RefinementStrategy
Auto Trait Implementations§
impl Freeze for RefinementStrategy
impl RefUnwindSafe for RefinementStrategy
impl Send for RefinementStrategy
impl Sync for RefinementStrategy
impl Unpin for RefinementStrategy
impl UnwindSafe for RefinementStrategy
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
Source§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
Source§impl<T> Instrument for T
impl<T> Instrument for T
Source§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
Source§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more