Skip to main content

Logic

smtlib

Enum Logic 

Source 
pub enum Logic {

Show 26 variants    AUFLIA,
    AUFLIRA,
    AUFNIRA,
    LIA,
    LRA,
    QF_ABV,
    QF_AUFBV,
    QF_AUFLIA,
    QF_AX,
    QF_BV,
    QF_BVFP,
    QF_IDL,
    QF_LIA,
    QF_LRA,
    QF_NIA,
    QF_NRA,
    QF_RDL,
    QF_UF,
    QF_UFBV,
    QF_UFIDL,
    QF_UFLIA,
    QF_UFLRA,
    QF_UFNRA,
    UFLRA,
    UFNIA,
    Custom(String),

}
Expand description

Logics allow specifictation of which (sub-)logic should be used by a solver.

A more detailed description of logics can be found on the SMT-LIB website.

This is a graph :)

Variants§

§

AUFLIA

Closed formulas built over arbitrary expansions of the Ints and ArraysEx signatures with free sort and function symbols, but with the following restrictions:

  • all terms of sort Int are linear, that is, have no occurrences of the function symbols *, /, div, mod, and abs, except as specified in the :extensions attributes;
  • all array terms have sort (Array Int Int).
§

AUFLIRA

Closed formulas built over arbitrary expansions of the Reals_Ints and ArraysEx signatures with free sort and function symbols, but with the following restrictions:

  • all terms of sort Int are linear, that is, have no occurrences of the function symbols *, /, div, mod, and abs, except as specified in the :extensions attributes;
  • all terms of sort Real are linear, that is, have no occurrences of the function symbols * and /, except as specified in the :extensions attribute;
  • all array terms have sort (Array Int Real) or (Array Int (Array Int Real)).
§

AUFNIRA

Closed formulas built over arbitrary expansions of the Reals_Ints and ArraysEx signatures with free sort and function symbols.

§

LIA

Closed formulas built over an arbitrary expansion of the Ints signature with free constant symbols, but whose terms of sort Int are all linear, that is, have no occurrences of the function symbols *, /, div, mod, and abs, except as specified the :extensions attribute.

§

LRA

Closed formulas built over arbitrary expansions of the Reals signature with free constant symbols, but containing only linear atoms, that is, atoms with no occurrences of the function symbols * and /, except as specified the :extensions attribute.

§

QF_ABV

Closed quantifier-free formulas built over the FixedSizeBitVectors and ArraysEx signatures, with the restriction that all array terms have sort of the form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0.

§

QF_AUFBV

Closed quantifier-free formulas built over an arbitrary expansion of the FixedSizeBitVectors and ArraysEx signatures with free sort and function symbols, but with the restriction that all array terms have sort of the form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0.

§

QF_AUFLIA

Closed quantifier-free formulas built over arbitrary expansions of the Ints and ArraysEx signatures with free sort and function symbols, but with the following restrictions:

  • all terms of sort Int are linear, that is, have no occurrences of the function symbols *, /, div, mod, and abs, except as specified in the :extensions attributes;
  • all array terms have sort (Array Int Int).
§

QF_AX

Closed quantifier-free formulas built over an arbitrary expansion of the ArraysEx signature with free sort and constant symbols.

§

QF_BV

Closed quantifier-free formulas built over an arbitrary expansion of the FixedSizeBitVectors signature with free constant symbols over the sorts (_ BitVec m) for 0 < m. Formulas in ite terms must satisfy the same restriction as well, with the exception that they need not be closed (because they may be in the scope of a let binder).

§

QF_BVFP

Closed quantifier-free formulas over the FixedSizeBitVectors and FloatingPoint theories.

§

QF_IDL

Closed quantifier-free formulas with atoms of the form:

  • q
  • (op (- x y) n),
  • (op (- x y) (- n)), or
  • (op x y) where
    • q is a variable or free constant symbol of sort Bool,
    • op is <, <=, >, >=, =, or distinct,
    • x, y are free constant symbols of sort Int,
    • n is a numeral.
§

QF_LIA

Closed quantifier-free formulas built over an arbitrary expansion of the Ints signature with free constant symbols, but whose terms of sort Int are all linear, that is, have no occurrences of the function symbols /, div, mod, and abs, and no occurrences of the function symbol *, except as specified in the :extensions attribute.

§

QF_LRA

Closed quantifier-free formulas built over arbitrary expansions of the Reals signature with free constant symbols, but containing only linear atoms, that is, atoms with no occurrences of the function symbols * and /, except as specified the :extensions attribute.

§

QF_NIA

Closed quantifier-free formulas built over an arbitrary expansion of the Ints signature with free constant symbols.

§

QF_NRA

Closed quantifier-free formulas built over arbitrary expansions of the Reals signature with free constant symbols.

§

QF_RDL

Closed quantifier-free formulas with atoms of the form:

  • p
  • (op (- x y) c),
  • (op x y),
  • (op (- (+ x … x) (+ y … y)) c) with n > 1 occurrences of x and of y, where
    • p is a variable or free constant symbol of sort Bool,
    • c is an expression of the form m or (- m) for some numeral m,
    • op is <, <=, >, >=, =, or distinct,
    • x, y are free constant symbols of sort Real.
§

QF_UF

Closed quantifier-free formulas built over an arbitrary expansion of the Core signature with free sort and function symbols.

§

QF_UFBV

Closed quantifier-free formulas built over arbitrary expansions of the FixedSizeBitVectors signature with free sort and function symbols.

§

QF_UFIDL

Closed quantifier-free formulas built over an arbitrary expansion with free sort and function symbols of the signature consisting of

  • all the sort and function symbols of Core and

  • the following symbols of Int:

    :sorts ((Int 0)) :funs ((NUMERAL Int) (- Int Int Int) (+ Int Int Int) (<= Int Int Bool) (< Int Int Bool) (>= Int Int Bool) (> Int Int Bool) )

Additionally, for every term of the form (op t1 t2) with op in {+, -}, at least one of t1 and t2 is a numeral.

§

QF_UFLIA

Closed quantifier-free formulas built over arbitrary expansions of the Ints signatures with free sort and function symbols, but with the following restrictions:

  • all terms of sort Int are linear, that is, have no occurrences of the function symbols *, /, div, mod, and abs, except as specified in the :extensions attributes;
§

QF_UFLRA

Closed quantifier-free formulas built over arbitrary expansions of the Reals signature with free sort and function symbols, but containing only linear atoms, that is, atoms with no occurrences of the function symbols * and /, except as specified the :extensions attribute.

§

QF_UFNRA

Closed quantifier-free formulas built over arbitrary expansions of the Reals signature with free sort and function symbols.

§

UFLRA

Closed formulas built over arbitrary expansions of the Reals signature with free sort and function symbols, but containing only linear atoms, that is, atoms with no occurrences of the function symbols * and /, except as specified the :extensions attribute.

§

UFNIA

Closed formulas built over an arbitrary expansion of the Ints signature with free sort and function symbols.

§

Custom(String)

A fallback variant in case the user wants to specify some logic which is not part of the predefined collection.

Implementations§

Source§

impl Logic

Source

pub fn name(&self) -> Cow<'static, str>

Returns the name of the logic.

Trait Implementations§

Source§

impl Display for Logic

Source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

impl Freeze for Logic

§

impl RefUnwindSafe for Logic

§

impl Send for Logic

§

impl Sync for Logic

§

impl Unpin for Logic

§

impl UnsafeUnpin for Logic

§

impl UnwindSafe for Logic

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> ErasedDestructor for T
where T: 'static,

Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T> IntoEither for T

Source§

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 more
Source§

fn into_either_with<F>(self, into_left: F) -> Either<Self, Self> ⓘ
where F: FnOnce(&Self) -> bool,

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

impl<'st, T> IntoWithStorage<'st, T> for T

Source§

fn into_with_storage(self, _st: &'st Storage) -> T

Construct a STerm with the presence of Storage
Source§

impl<D> OwoColorize for D

Source§

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,

Set the background color generically. Read more
Source§

fn black(&self) -> FgColorDisplay<'_, Black, Self>

Change the foreground color to black
Source§

fn on_black(&self) -> BgColorDisplay<'_, Black, Self>

Change the background color to black
Source§

fn red(&self) -> FgColorDisplay<'_, Red, Self>

Change the foreground color to red
Source§

fn on_red(&self) -> BgColorDisplay<'_, Red, Self>

Change the background color to red
Source§

fn green(&self) -> FgColorDisplay<'_, Green, Self>

Change the foreground color to green
Source§

fn on_green(&self) -> BgColorDisplay<'_, Green, Self>

Change the background color to green
Source§

fn yellow(&self) -> FgColorDisplay<'_, Yellow, Self>

Change the foreground color to yellow
Source§

fn on_yellow(&self) -> BgColorDisplay<'_, Yellow, Self>

Change the background color to yellow
Source§

fn blue(&self) -> FgColorDisplay<'_, Blue, Self>

Change the foreground color to blue
Source§

fn on_blue(&self) -> BgColorDisplay<'_, Blue, Self>

Change the background color to blue
Source§

fn magenta(&self) -> FgColorDisplay<'_, Magenta, Self>

Change the foreground color to magenta
Source§

fn on_magenta(&self) -> BgColorDisplay<'_, Magenta, Self>

Change the background color to magenta
Source§

fn purple(&self) -> FgColorDisplay<'_, Magenta, Self>

Change the foreground color to purple
Source§

fn on_purple(&self) -> BgColorDisplay<'_, Magenta, Self>

Change the background color to purple
Source§

fn cyan(&self) -> FgColorDisplay<'_, Cyan, Self>

Change the foreground color to cyan
Source§

fn on_cyan(&self) -> BgColorDisplay<'_, Cyan, Self>

Change the background color to cyan
Source§

fn white(&self) -> FgColorDisplay<'_, White, Self>

Change the foreground color to white
Source§

fn on_white(&self) -> BgColorDisplay<'_, White, Self>

Change the background color to white
Source§

fn default_color(&self) -> FgColorDisplay<'_, Default, Self>

Change the foreground color to the terminal default
Source§

fn on_default_color(&self) -> BgColorDisplay<'_, Default, Self>

Change the background color to the terminal default
Source§

fn bright_black(&self) -> FgColorDisplay<'_, BrightBlack, Self>

Change the foreground color to bright black
Source§

fn on_bright_black(&self) -> BgColorDisplay<'_, BrightBlack, Self>

Change the background color to bright black
Source§

fn bright_red(&self) -> FgColorDisplay<'_, BrightRed, Self>

Change the foreground color to bright red
Source§

fn on_bright_red(&self) -> BgColorDisplay<'_, BrightRed, Self>

Change the background color to bright red
Source§

fn bright_green(&self) -> FgColorDisplay<'_, BrightGreen, Self>

Change the foreground color to bright green
Source§

fn on_bright_green(&self) -> BgColorDisplay<'_, BrightGreen, Self>

Change the background color to bright green
Source§

fn bright_yellow(&self) -> FgColorDisplay<'_, BrightYellow, Self>

Change the foreground color to bright yellow
Source§

fn on_bright_yellow(&self) -> BgColorDisplay<'_, BrightYellow, Self>

Change the background color to bright yellow
Source§

fn bright_blue(&self) -> FgColorDisplay<'_, BrightBlue, Self>

Change the foreground color to bright blue
Source§

fn on_bright_blue(&self) -> BgColorDisplay<'_, BrightBlue, Self>

Change the background color to bright blue
Source§

fn bright_magenta(&self) -> FgColorDisplay<'_, BrightMagenta, Self>

Change the foreground color to bright magenta
Source§

fn on_bright_magenta(&self) -> BgColorDisplay<'_, BrightMagenta, Self>

Change the background color to bright magenta
Source§

fn bright_purple(&self) -> FgColorDisplay<'_, BrightMagenta, Self>

Change the foreground color to bright purple
Source§

fn on_bright_purple(&self) -> BgColorDisplay<'_, BrightMagenta, Self>

Change the background color to bright purple
Source§

fn bright_cyan(&self) -> FgColorDisplay<'_, BrightCyan, Self>

Change the foreground color to bright cyan
Source§

fn on_bright_cyan(&self) -> BgColorDisplay<'_, BrightCyan, Self>

Change the background color to bright cyan
Source§

fn bright_white(&self) -> FgColorDisplay<'_, BrightWhite, Self>

Change the foreground color to bright white
Source§

fn on_bright_white(&self) -> BgColorDisplay<'_, BrightWhite, Self>

Change the background color to bright white
Source§

fn bold(&self) -> BoldDisplay<'_, Self>

Make the text bold
Source§

fn dimmed(&self) -> DimDisplay<'_, Self>

Make the text dim
Source§

fn italic(&self) -> ItalicDisplay<'_, Self>

Make the text italicized
Source§

fn underline(&self) -> UnderlineDisplay<'_, Self>

Make the text underlined
Make the text blink
Make the text blink (but fast!)
Source§

fn reversed(&self) -> ReversedDisplay<'_, Self>

Swap the foreground and background colors
Source§

fn hidden(&self) -> HiddenDisplay<'_, Self>

Hide the text
Source§

fn strikethrough(&self) -> StrikeThroughDisplay<'_, Self>

Cross out the text
Source§

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 more
Source§

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 more
Source§

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>

Set the background color to a specific RGB value.
Source§

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>

Sets the background color to an RGB value.
Source§

fn style(&self, style: Style) -> Styled<&Self>

Apply a runtime-determined style
Source§

impl<T> ToString for T
where T: Display + ?Sized,

Source§

fn to_string(&self) -> String

Converts the given value to a String. Read more
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = !

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, !>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.