pub struct Const<'st, T>(/* private fields */);Expand description
This struct wraps specific instances of other terms to indicate that they
are constant. Constants are named terms whose value can be extracted from a
model using Model::eval.
To construct a Const<'st, T> call T::new_const where
T implements Sort.
Implementations§
Trait Implementations§
impl<'st, T: Copy> Copy for Const<'st, T>
Source§impl<'st, const EB: usize, const SB: usize> From<Const<'st, FloatingPoint<'st, EB, SB>>> for FloatingPoint<'st, EB, SB>
impl<'st, const EB: usize, const SB: usize> From<Const<'st, FloatingPoint<'st, EB, SB>>> for FloatingPoint<'st, EB, SB>
Source§fn from(c: Const<'st, FloatingPoint<'st, EB, SB>>) -> Self
fn from(c: Const<'st, FloatingPoint<'st, EB, SB>>) -> Self
Converts to this type from the input type.
Source§impl<'st> From<Const<'st, RoundingMode<'st>>> for RoundingMode<'st>
impl<'st> From<Const<'st, RoundingMode<'st>>> for RoundingMode<'st>
Source§fn from(c: Const<'st, RoundingMode<'st>>) -> Self
fn from(c: Const<'st, RoundingMode<'st>>) -> Self
Converts to this type from the input type.
Source§impl<'st, X: Sorted<'st>, Y: Sorted<'st>> IntoWithStorage<'st, Array<'st, X, Y>> for Const<'st, Array<'st, X, Y>>
impl<'st, X: Sorted<'st>, Y: Sorted<'st>> IntoWithStorage<'st, Array<'st, X, Y>> for Const<'st, Array<'st, X, Y>>
Source§fn into_with_storage(self, _st: &'st Storage) -> Array<'st, X, Y>
fn into_with_storage(self, _st: &'st Storage) -> Array<'st, X, Y>
Construct a
STerm with the presence of StorageSource§impl<'st> IntoWithStorage<'st, Bool<'st>> for Const<'st, Bool<'st>>
impl<'st> IntoWithStorage<'st, Bool<'st>> for Const<'st, Bool<'st>>
Source§fn into_with_storage(self, _st: &'st Storage) -> Bool<'st>
fn into_with_storage(self, _st: &'st Storage) -> Bool<'st>
Construct a
STerm with the presence of StorageSource§impl<'st> IntoWithStorage<'st, Int<'st>> for Const<'st, Int<'st>>
impl<'st> IntoWithStorage<'st, Int<'st>> for Const<'st, Int<'st>>
Source§fn into_with_storage(self, _st: &'st Storage) -> Int<'st>
fn into_with_storage(self, _st: &'st Storage) -> Int<'st>
Construct a
STerm with the presence of StorageSource§impl<'st> IntoWithStorage<'st, Real<'st>> for Const<'st, Real<'st>>
impl<'st> IntoWithStorage<'st, Real<'st>> for Const<'st, Real<'st>>
Source§fn into_with_storage(self, _st: &'st Storage) -> Real<'st>
fn into_with_storage(self, _st: &'st Storage) -> Real<'st>
Construct a
STerm with the presence of StorageSource§impl<'st, A> QuantifierVars<'st> for Const<'st, A>where
A: StaticSorted<'st>,
impl<'st, A> QuantifierVars<'st> for Const<'st, A>where
A: StaticSorted<'st>,
Source§impl<'st, T: Sorted<'st>> Sorted<'st> for Const<'st, T>
impl<'st, T: Sorted<'st>> Sorted<'st> for Const<'st, T>
Source§type Inner = T
type Inner = T
The inner type of the term. This is used for
Const<'st, T>
where the inner type is T.Source§fn sterm(self) -> STerm<'st>
fn sterm(self) -> STerm<'st>
Constructy the smtlib AST representation of the term with associated
storage.
Source§fn into_dynamic(self) -> Dynamic<'st>
fn into_dynamic(self) -> Dynamic<'st>
Casts the term into a dynamic term which looses static types and stores
the sort dynamically.
Source§fn _eq(self, other: impl IntoWithStorage<'st, Self::Inner>) -> Bool<'st>
fn _eq(self, other: impl IntoWithStorage<'st, Self::Inner>) -> Bool<'st>
Construct the term representing
(= self other)Auto Trait Implementations§
impl<'st, T> Freeze for Const<'st, T>where
T: Freeze,
impl<'st, T> RefUnwindSafe for Const<'st, T>where
T: RefUnwindSafe,
impl<'st, T> Send for Const<'st, T>where
T: Send,
impl<'st, T> Sync for Const<'st, T>where
T: Sync,
impl<'st, T> Unpin for Const<'st, T>where
T: Unpin,
impl<'st, T> UnsafeUnpin for Const<'st, T>where
T: UnsafeUnpin,
impl<'st, T> UnwindSafe for Const<'st, T>where
T: UnwindSafe,
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,
impl<T> ErasedDestructor for Twhere
T: 'static,
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 moreSource§impl<'st, T> IntoWithStorage<'st, T> for T
impl<'st, T> IntoWithStorage<'st, T> for T
Source§fn into_with_storage(self, _st: &'st Storage) -> T
fn into_with_storage(self, _st: &'st Storage) -> T
Construct a
STerm with the presence of StorageSource§impl<D> OwoColorize for D
impl<D> OwoColorize for D
Source§fn fg<C>(&self) -> FgColorDisplay<'_, C, Self>where
C: Color,
fn fg<C>(&self) -> FgColorDisplay<'_, C, Self>where
C: Color,
Set the foreground color generically Read more
Source§fn bg<C>(&self) -> BgColorDisplay<'_, C, Self>where
C: Color,
fn bg<C>(&self) -> BgColorDisplay<'_, C, Self>where
C: Color,
Set the background color generically. Read more
Source§fn black(&self) -> FgColorDisplay<'_, Black, Self>
fn black(&self) -> FgColorDisplay<'_, Black, Self>
Change the foreground color to black
Source§fn on_black(&self) -> BgColorDisplay<'_, Black, Self>
fn on_black(&self) -> BgColorDisplay<'_, Black, Self>
Change the background color to black
Source§fn red(&self) -> FgColorDisplay<'_, Red, Self>
fn red(&self) -> FgColorDisplay<'_, Red, Self>
Change the foreground color to red
Source§fn on_red(&self) -> BgColorDisplay<'_, Red, Self>
fn on_red(&self) -> BgColorDisplay<'_, Red, Self>
Change the background color to red
Source§fn green(&self) -> FgColorDisplay<'_, Green, Self>
fn green(&self) -> FgColorDisplay<'_, Green, Self>
Change the foreground color to green
Source§fn on_green(&self) -> BgColorDisplay<'_, Green, Self>
fn on_green(&self) -> BgColorDisplay<'_, Green, Self>
Change the background color to green
Source§fn yellow(&self) -> FgColorDisplay<'_, Yellow, Self>
fn yellow(&self) -> FgColorDisplay<'_, Yellow, Self>
Change the foreground color to yellow
Source§fn on_yellow(&self) -> BgColorDisplay<'_, Yellow, Self>
fn on_yellow(&self) -> BgColorDisplay<'_, Yellow, Self>
Change the background color to yellow
Source§fn blue(&self) -> FgColorDisplay<'_, Blue, Self>
fn blue(&self) -> FgColorDisplay<'_, Blue, Self>
Change the foreground color to blue
Source§fn on_blue(&self) -> BgColorDisplay<'_, Blue, Self>
fn on_blue(&self) -> BgColorDisplay<'_, Blue, Self>
Change the background color to blue
Source§fn magenta(&self) -> FgColorDisplay<'_, Magenta, Self>
fn magenta(&self) -> FgColorDisplay<'_, Magenta, Self>
Change the foreground color to magenta
Source§fn on_magenta(&self) -> BgColorDisplay<'_, Magenta, Self>
fn on_magenta(&self) -> BgColorDisplay<'_, Magenta, Self>
Change the background color to magenta
Source§fn purple(&self) -> FgColorDisplay<'_, Magenta, Self>
fn purple(&self) -> FgColorDisplay<'_, Magenta, Self>
Change the foreground color to purple
Source§fn on_purple(&self) -> BgColorDisplay<'_, Magenta, Self>
fn on_purple(&self) -> BgColorDisplay<'_, Magenta, Self>
Change the background color to purple
Source§fn cyan(&self) -> FgColorDisplay<'_, Cyan, Self>
fn cyan(&self) -> FgColorDisplay<'_, Cyan, Self>
Change the foreground color to cyan
Source§fn on_cyan(&self) -> BgColorDisplay<'_, Cyan, Self>
fn on_cyan(&self) -> BgColorDisplay<'_, Cyan, Self>
Change the background color to cyan
Source§fn white(&self) -> FgColorDisplay<'_, White, Self>
fn white(&self) -> FgColorDisplay<'_, White, Self>
Change the foreground color to white
Source§fn on_white(&self) -> BgColorDisplay<'_, White, Self>
fn on_white(&self) -> BgColorDisplay<'_, White, Self>
Change the background color to white
Source§fn default_color(&self) -> FgColorDisplay<'_, Default, Self>
fn default_color(&self) -> FgColorDisplay<'_, Default, Self>
Change the foreground color to the terminal default
Source§fn on_default_color(&self) -> BgColorDisplay<'_, Default, Self>
fn on_default_color(&self) -> BgColorDisplay<'_, Default, Self>
Change the background color to the terminal default
Source§fn bright_black(&self) -> FgColorDisplay<'_, BrightBlack, Self>
fn bright_black(&self) -> FgColorDisplay<'_, BrightBlack, Self>
Change the foreground color to bright black
Source§fn on_bright_black(&self) -> BgColorDisplay<'_, BrightBlack, Self>
fn on_bright_black(&self) -> BgColorDisplay<'_, BrightBlack, Self>
Change the background color to bright black
Source§fn bright_red(&self) -> FgColorDisplay<'_, BrightRed, Self>
fn bright_red(&self) -> FgColorDisplay<'_, BrightRed, Self>
Change the foreground color to bright red
Source§fn on_bright_red(&self) -> BgColorDisplay<'_, BrightRed, Self>
fn on_bright_red(&self) -> BgColorDisplay<'_, BrightRed, Self>
Change the background color to bright red
Source§fn bright_green(&self) -> FgColorDisplay<'_, BrightGreen, Self>
fn bright_green(&self) -> FgColorDisplay<'_, BrightGreen, Self>
Change the foreground color to bright green
Source§fn on_bright_green(&self) -> BgColorDisplay<'_, BrightGreen, Self>
fn on_bright_green(&self) -> BgColorDisplay<'_, BrightGreen, Self>
Change the background color to bright green
Source§fn bright_yellow(&self) -> FgColorDisplay<'_, BrightYellow, Self>
fn bright_yellow(&self) -> FgColorDisplay<'_, BrightYellow, Self>
Change the foreground color to bright yellow
Source§fn on_bright_yellow(&self) -> BgColorDisplay<'_, BrightYellow, Self>
fn on_bright_yellow(&self) -> BgColorDisplay<'_, BrightYellow, Self>
Change the background color to bright yellow
Source§fn bright_blue(&self) -> FgColorDisplay<'_, BrightBlue, Self>
fn bright_blue(&self) -> FgColorDisplay<'_, BrightBlue, Self>
Change the foreground color to bright blue
Source§fn on_bright_blue(&self) -> BgColorDisplay<'_, BrightBlue, Self>
fn on_bright_blue(&self) -> BgColorDisplay<'_, BrightBlue, Self>
Change the background color to bright blue
Source§fn bright_magenta(&self) -> FgColorDisplay<'_, BrightMagenta, Self>
fn bright_magenta(&self) -> FgColorDisplay<'_, BrightMagenta, Self>
Change the foreground color to bright magenta
Source§fn on_bright_magenta(&self) -> BgColorDisplay<'_, BrightMagenta, Self>
fn on_bright_magenta(&self) -> BgColorDisplay<'_, BrightMagenta, Self>
Change the background color to bright magenta
Source§fn bright_purple(&self) -> FgColorDisplay<'_, BrightMagenta, Self>
fn bright_purple(&self) -> FgColorDisplay<'_, BrightMagenta, Self>
Change the foreground color to bright purple
Source§fn on_bright_purple(&self) -> BgColorDisplay<'_, BrightMagenta, Self>
fn on_bright_purple(&self) -> BgColorDisplay<'_, BrightMagenta, Self>
Change the background color to bright purple
Source§fn bright_cyan(&self) -> FgColorDisplay<'_, BrightCyan, Self>
fn bright_cyan(&self) -> FgColorDisplay<'_, BrightCyan, Self>
Change the foreground color to bright cyan
Source§fn on_bright_cyan(&self) -> BgColorDisplay<'_, BrightCyan, Self>
fn on_bright_cyan(&self) -> BgColorDisplay<'_, BrightCyan, Self>
Change the background color to bright cyan
Source§fn bright_white(&self) -> FgColorDisplay<'_, BrightWhite, Self>
fn bright_white(&self) -> FgColorDisplay<'_, BrightWhite, Self>
Change the foreground color to bright white
Source§fn on_bright_white(&self) -> BgColorDisplay<'_, BrightWhite, Self>
fn on_bright_white(&self) -> BgColorDisplay<'_, BrightWhite, Self>
Change the background color to bright white
Source§fn bold(&self) -> BoldDisplay<'_, Self>
fn bold(&self) -> BoldDisplay<'_, Self>
Make the text bold
Source§fn dimmed(&self) -> DimDisplay<'_, Self>
fn dimmed(&self) -> DimDisplay<'_, Self>
Make the text dim
Source§fn italic(&self) -> ItalicDisplay<'_, Self>
fn italic(&self) -> ItalicDisplay<'_, Self>
Make the text italicized
Source§fn underline(&self) -> UnderlineDisplay<'_, Self>
fn underline(&self) -> UnderlineDisplay<'_, Self>
Make the text underlined
Source§fn blink(&self) -> BlinkDisplay<'_, Self>
fn blink(&self) -> BlinkDisplay<'_, Self>
Make the text blink
Source§fn blink_fast(&self) -> BlinkFastDisplay<'_, Self>
fn blink_fast(&self) -> BlinkFastDisplay<'_, Self>
Make the text blink (but fast!)
Source§fn reversed(&self) -> ReversedDisplay<'_, Self>
fn reversed(&self) -> ReversedDisplay<'_, Self>
Swap the foreground and background colors
Hide the text
Source§fn strikethrough(&self) -> StrikeThroughDisplay<'_, Self>
fn strikethrough(&self) -> StrikeThroughDisplay<'_, Self>
Cross out the text
Source§fn color<Color>(&self, color: Color) -> FgDynColorDisplay<'_, Color, Self>where
Color: DynColor,
fn color<Color>(&self, color: Color) -> FgDynColorDisplay<'_, Color, Self>where
Color: DynColor,
Set the foreground color at runtime. Only use if you do not know which color will be used at
compile-time. If the color is constant, use either
OwoColorize::fg or
a color-specific method, such as OwoColorize::green, Read moreSource§fn on_color<Color>(&self, color: Color) -> BgDynColorDisplay<'_, Color, Self>where
Color: DynColor,
fn on_color<Color>(&self, color: Color) -> BgDynColorDisplay<'_, Color, Self>where
Color: DynColor,
Set the background color at runtime. Only use if you do not know what color to use at
compile-time. If the color is constant, use either
OwoColorize::bg or
a color-specific method, such as OwoColorize::on_yellow, Read moreSource§fn fg_rgb<const R: u8, const G: u8, const B: u8>(
&self,
) -> FgColorDisplay<'_, CustomColor<R, G, B>, Self>
fn fg_rgb<const R: u8, const G: u8, const B: u8>( &self, ) -> FgColorDisplay<'_, CustomColor<R, G, B>, Self>
Set the foreground color to a specific RGB value.
Source§fn bg_rgb<const R: u8, const G: u8, const B: u8>(
&self,
) -> BgColorDisplay<'_, CustomColor<R, G, B>, Self>
fn bg_rgb<const R: u8, const G: u8, const B: u8>( &self, ) -> BgColorDisplay<'_, CustomColor<R, G, B>, Self>
Set the background color to a specific RGB value.
Source§fn truecolor(&self, r: u8, g: u8, b: u8) -> FgDynColorDisplay<'_, Rgb, Self>
fn truecolor(&self, r: u8, g: u8, b: u8) -> FgDynColorDisplay<'_, Rgb, Self>
Sets the foreground color to an RGB value.
Source§fn on_truecolor(&self, r: u8, g: u8, b: u8) -> BgDynColorDisplay<'_, Rgb, Self>
fn on_truecolor(&self, r: u8, g: u8, b: u8) -> BgDynColorDisplay<'_, Rgb, Self>
Sets the background color to an RGB value.
Source§impl<T> Source for T
impl<T> Source for T
Source§type Slice<'a> = <<T as Deref>::Target as Source>::Slice<'a>
where
T: 'a
type Slice<'a> = <<T as Deref>::Target as Source>::Slice<'a> where T: 'a
A type this
Source can be sliced into.Source§fn read<'a, Chunk>(&'a self, offset: usize) -> Option<Chunk>where
Chunk: Chunk<'a>,
fn read<'a, Chunk>(&'a self, offset: usize) -> Option<Chunk>where
Chunk: Chunk<'a>,
Read a chunk of bytes into an array. Returns
None when reading
out of bounds would occur. Read moreSource§fn slice(&self, range: Range<usize>) -> Option<<T as Source>::Slice<'_>>
fn slice(&self, range: Range<usize>) -> Option<<T as Source>::Slice<'_>>
Get a slice of the source at given range. This is analogous to
slice::get(range). Read moreSource§unsafe fn slice_unchecked(
&self,
range: Range<usize>,
) -> <T as Source>::Slice<'_>
unsafe fn slice_unchecked( &self, range: Range<usize>, ) -> <T as Source>::Slice<'_>
Get a slice of the source at given range. This is analogous to
slice::get_unchecked(range). Read more