Enum rustproof_libsmt::theories::bitvec::OpCodes

pub enum OpCodes {
    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

ConcatExtract(u64, u64)BvNotBvAndBvOrBvNegBvAddBvMulBvSMulDoesNotOverflowBvSMulDoesNotUnderflowBvUMulDoesNotOverflowBvUDivBvURemBvShlBvLShrBvULtBvNandBvNorBvXorBvXnorBvCompBvSubBvSDivBvSRemBvSModBvAShrRepeat(u64)ZeroExtend(u64)SignExtend(u64)RotateLeft(u64)RotateRight(u64)BvULeBvUGtBvUGeBvSLtBvSLeBvSGtBvSGeConst(u64, usize)FreeVar(String)

Trait Implementations

impl Clone for OpCodes

fn clone(&self) -> OpCodes

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for OpCodes

fn fmt(&self, __arg_0: &mut Formatter) -> Result

Formats the value using the given formatter.

impl Display for OpCodes

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

Formats the value using the given formatter.

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

impl Into<QF_BV_Fn> for OpCodes

fn into(self) -> QF_BV_Fn

Performs the conversion.

impl Into<QF_AUFBV_Fn> for OpCodes

fn into(self) -> QF_AUFBV_Fn

Performs the conversion.

impl Into<QF_ABV_Fn> for OpCodes

fn into(self) -> QF_ABV_Fn

Performs the conversion.