easy_smt

Struct KnownAtoms

Source 
#[non_exhaustive]
pub struct KnownAtoms {
Show 83 fields
    pub check_sat: SExpr,
    pub check_sat_assuming: SExpr,
    pub unsat: SExpr,
    pub sat: SExpr,
    pub unknown: SExpr,
    pub declare_const: SExpr,
    pub declare_datatype: SExpr,
    pub declare_datatypes: SExpr,
    pub par: SExpr,
    pub declare_sort: SExpr,
    pub declare_fun: SExpr,
    pub define_fun: SExpr,
    pub assert: SExpr,
    pub get_model: SExpr,
    pub get_value: SExpr,
    pub get_unsat_core: SExpr,
    pub set_logic: SExpr,
    pub set_option: SExpr,
    pub exit: SExpr,
    pub push: SExpr,
    pub pop: SExpr,
    pub bool: SExpr,
    pub bang: SExpr,
    pub success: SExpr,
    pub t: SExpr,
    pub f: SExpr,
    pub not: SExpr,
    pub imp: SExpr,
    pub and: SExpr,
    pub or: SExpr,
    pub xor: SExpr,
    pub eq: SExpr,
    pub distinct: SExpr,
    pub ite: SExpr,
    pub int: SExpr,
    pub minus: SExpr,
    pub plus: SExpr,
    pub times: SExpr,
    pub div: SExpr,
    pub modulo: SExpr,
    pub rem: SExpr,
    pub lte: SExpr,
    pub lt: SExpr,
    pub gte: SExpr,
    pub gt: SExpr,
    pub array: SExpr,
    pub select: SExpr,
    pub store: SExpr,
    pub let_: SExpr,
    pub forall: SExpr,
    pub exists: SExpr,
    pub match_: SExpr,
    pub und: SExpr,
    pub bit_vec: SExpr,
    pub concat: SExpr,
    pub extract: SExpr,
    pub bvnot: SExpr,
    pub bvor: SExpr,
    pub bvand: SExpr,
    pub bvnand: SExpr,
    pub bvxor: SExpr,
    pub bvxnor: SExpr,
    pub bvneg: SExpr,
    pub bvadd: SExpr,
    pub bvsub: SExpr,
    pub bvmul: SExpr,
    pub bvudiv: SExpr,
    pub bvurem: SExpr,
    pub bvsdiv: SExpr,
    pub bvsmod: SExpr,
    pub bvsrem: SExpr,
    pub bvshl: SExpr,
    pub bvlshr: SExpr,
    pub bvashr: SExpr,
    pub bvule: SExpr,
    pub bvult: SExpr,
    pub bvuge: SExpr,
    pub bvugt: SExpr,
    pub bvsle: SExpr,
    pub bvslt: SExpr,
    pub bvsge: SExpr,
    pub bvsgt: SExpr,
    pub bvcomp: SExpr,

}

Fields (Non-exhaustive)§

This struct is marked as non-exhaustive
Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.
§check_sat: SExpr

The atom: check-sat

§check_sat_assuming: SExpr

The atom: check-sat-assuming

§unsat: SExpr

The atom: unsat

§sat: SExpr

The atom: sat

§unknown: SExpr

The atom: unknown

§declare_const: SExpr

The atom: declare-const

§declare_datatype: SExpr

The atom: declare-datatype

§declare_datatypes: SExpr

The atom: declare-datatypes

§par: SExpr

The atom: par

§declare_sort: SExpr

The atom: declare-sort

§declare_fun: SExpr

The atom: declare-fun

§define_fun: SExpr

The atom: define-fun

§assert: SExpr

The atom: assert

§get_model: SExpr

The atom: get-model

§get_value: SExpr

The atom: get-value

§get_unsat_core: SExpr

The atom: get-unsat-core

§set_logic: SExpr

The atom: set-logic

§set_option: SExpr

The atom: set-option

§exit: SExpr

The atom: exit

§push: SExpr

The atom: push

§pop: SExpr

The atom: pop

§bool: SExpr

The atom: Bool

§bang: SExpr

The atom: !

§success: SExpr

The atom: success

§t: SExpr

The atom: true

§f: SExpr

The atom: false

§not: SExpr

The atom: not

§imp: SExpr

The atom: =>

§and: SExpr

The atom: and

§or: SExpr

The atom: or

§xor: SExpr

The atom: xor

§eq: SExpr

§The atom: `

`

§distinct: SExpr

The atom: distinct

§ite: SExpr

The atom: ite

§int: SExpr

The atom: Int

§minus: SExpr

§The atom: `

`

§plus: SExpr

The atom: +

§times: SExpr

The atom: *

§div: SExpr

The atom: div

§modulo: SExpr

The atom: mod

§rem: SExpr

The atom: rem

§lte: SExpr

The atom: <=

§lt: SExpr

The atom: <

§gte: SExpr

The atom: `

= `

§gt: SExpr

The atom: `

`

§array: SExpr

The atom: Array

§select: SExpr

The atom: select

§store: SExpr

The atom: store

§let_: SExpr

The atom: let

§forall: SExpr

The atom: forall

§exists: SExpr

The atom: exists

§match_: SExpr

The atom: match

§und: SExpr

The atom: _

§bit_vec: SExpr

The atom: BitVec

§concat: SExpr

The atom: concat

§extract: SExpr

The atom: extract

§bvnot: SExpr

The atom: bvnot

§bvor: SExpr

The atom: bvor

§bvand: SExpr

The atom: bvand

§bvnand: SExpr

The atom: bvnand

§bvxor: SExpr

The atom: bvxor

§bvxnor: SExpr

The atom: bvxnor

§bvneg: SExpr

The atom: bvneg

§bvadd: SExpr

The atom: bvadd

§bvsub: SExpr

The atom: bvsub

§bvmul: SExpr

The atom: bvmul

§bvudiv: SExpr

The atom: bvudiv

§bvurem: SExpr

The atom: bvurem

§bvsdiv: SExpr

The atom: bvsdiv

§bvsmod: SExpr

The atom: bvsmod

§bvsrem: SExpr

The atom: bvsrem

§bvshl: SExpr

The atom: bvshl

§bvlshr: SExpr

The atom: bvlshr

§bvashr: SExpr

The atom: bvashr

§bvule: SExpr

The atom: bvule

§bvult: SExpr

The atom: bvult

§bvuge: SExpr

The atom: bvuge

§bvugt: SExpr

The atom: bvugt

§bvsle: SExpr

The atom: bvsle

§bvslt: SExpr

The atom: bvslt

§bvsge: SExpr

The atom: bvsge

§bvsgt: SExpr

The atom: bvsgt

§bvcomp: SExpr

The atom: bvcomp

Auto Trait Implementations§

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> 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, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

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

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

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.