pub enum CaseSplitStrategy {
Exhaustive,
ModelBased,
Heuristic,
Lazy,
}Expand description
Case split strategy for non-convex theories.
Variants§
Exhaustive
Enumerate all cases.
ModelBased
Use model to guide splitting.
Heuristic
Use heuristics.
Lazy
Lazy splitting (defer as long as possible).
Trait Implementations§
Source§impl Clone for CaseSplitStrategy
impl Clone for CaseSplitStrategy
Source§fn clone(&self) -> CaseSplitStrategy
fn clone(&self) -> CaseSplitStrategy
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 CaseSplitStrategy
impl Debug for CaseSplitStrategy
Source§impl PartialEq for CaseSplitStrategy
impl PartialEq for CaseSplitStrategy
impl Copy for CaseSplitStrategy
impl Eq for CaseSplitStrategy
impl StructuralPartialEq for CaseSplitStrategy
Auto Trait Implementations§
impl Freeze for CaseSplitStrategy
impl RefUnwindSafe for CaseSplitStrategy
impl Send for CaseSplitStrategy
impl Sync for CaseSplitStrategy
impl Unpin for CaseSplitStrategy
impl UnwindSafe for CaseSplitStrategy
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