rustproof_libsmt::theories::bitvec

Enum OpCodes

pub enum OpCodes {
Show 40 variants    Concat,
    Extract(u64, u64),
    BvNot,
    BvAnd,
    BvOr,
    BvNeg,
    BvAdd,
    BvMul,
    BvSMulDoesNotOverflow,
    BvSMulDoesNotUnderflow,
    BvUMulDoesNotOverflow,
    BvUDiv,
    BvURem,
    BvShl,
    BvLShr,
    BvULt,
    BvNand,
    BvNor,
    BvXor,
    BvXnor,
    BvComp,
    BvSub,
    BvSDiv,
    BvSRem,
    BvSMod,
    BvAShr,
    Repeat(u64),
    ZeroExtend(u64),
    SignExtend(u64),
    RotateLeft(u64),
    RotateRight(u64),
    BvULe,
    BvUGt,
    BvUGe,
    BvSLt,
    BvSLe,
    BvSGt,
    BvSGe,
    Const(u64, usize),
    FreeVar(String),
}

Variants§

Concat

Extract(u64, u64)

BvNot

BvAnd

BvOr

BvNeg

BvAdd

BvMul

BvSMulDoesNotOverflow

BvSMulDoesNotUnderflow

BvUMulDoesNotOverflow

BvUDiv

BvURem

BvShl

BvLShr

BvULt

BvNand

BvNor

BvXor

BvXnor

BvComp

BvSub

BvSDiv

BvSRem

BvSMod

BvAShr

Repeat(u64)

ZeroExtend(u64)

SignExtend(u64)

RotateLeft(u64)

RotateRight(u64)

BvULe

BvUGt

BvUGe

BvSLt

BvSLe

BvSGt

BvSGe

Const(u64, usize)

FreeVar(String)

Trait Implementations§

impl Clone for OpCodes

fn clone(&self) -> OpCodes

Returns a copy of the value. Read more

1.0.0 · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more

impl Debug for OpCodes

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

Formats the value using the given formatter. Read more

impl Display for OpCodes

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

Formats the value using the given formatter. Read more

impl Into<QF_ABV_Fn> for OpCodes

fn into(self) -> QF_ABV_Fn

Converts this type into the (usually inferred) input type.

impl Into<QF_AUFBV_Fn> for OpCodes

fn into(self) -> QF_AUFBV_Fn

Converts this type into the (usually inferred) input type.

impl Into<QF_BV_Fn> for OpCodes

fn into(self) -> QF_BV_Fn

Converts this type into the (usually inferred) input type.

impl SMTNode for OpCodes

fn is_var(&self) -> bool

Returns true if the node is a symbolic variable

fn is_const(&self) -> bool

Returns true if the node is a constant value

fn is_fn(&self) -> bool

Returns true if the node is a function

Auto Trait Implementations§

impl Freeze for OpCodes

impl RefUnwindSafe for OpCodes

impl Send for OpCodes

impl Sync for OpCodes

impl Unpin for OpCodes

impl UnwindSafe for OpCodes

Blanket Implementations§

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

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

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

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

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

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

Mutably borrows from an owned value. Read more

impl<T> CloneToUninit for T
where T: Clone,

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)

Performs copy-assignment from self to dest. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

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

fn into(self) -> U

Calls U::from(self).

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

impl<T> ToOwned for T
where T: Clone,

type Owned = T

The resulting type after obtaining ownership.

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more

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

fn to_string(&self) -> String

Converts the given value to a String. Read more

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

type Error = Infallible

The type returned in the event of a conversion error.

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

Performs the conversion.

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

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

The type returned in the event of a conversion error.

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

Performs the conversion.