Enum BitVecOp 

pub enum BitVecOp {
    And,
    Or,
    Xor,
    Not,
    Shl,
    Shr,
    AShr,
    Add,
    Sub,
    Mul,
    SDiv,
    SRem,
    ULt,
    SLt,
    ULe,
    SLe,
    Eq,
}

Bitvector operations for hardware verification.

These map directly to Z3’s bitvector theory operations.

Variants

And

Or

Xor

Not

Shl

Shr

AShr

Arithmetic shift right (sign-extending).

Add

Sub

Mul

SDiv

Signed division, truncating toward zero (matches Rust i64 /).

SRem

Signed remainder, sign following the dividend (matches Rust i64 %).

ULt

Unsigned less than.

SLt

Signed less than.

ULe

Unsigned less than or equal.

SLe

Signed less than or equal.

Eq

Bitvector equality.

Trait Implementations

impl Clone for BitVecOp

fn clone(&self) -> BitVecOp

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BitVecOp

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for BitVecOp

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for BitVecOp

fn eq(&self, other: &BitVecOp) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for BitVecOp

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Copy for BitVecOp

impl Eq for BitVecOp

impl StructuralPartialEq for BitVecOp