Enum VerifyOp 

pub enum VerifyOp {
    Add,
    Sub,
    Mul,
    Div,
    FloorDiv,
    Eq,
    Neq,
    Gt,
    Lt,
    Gte,
    Lte,
    And,
    Or,
    Implies,
}

Binary operations in the verification IR.

Operations are grouped by category:

• Arithmetic: Add, Sub, Mul, Div (Int × Int → Int)
• Comparison: Eq, Neq, Gt, Lt, Gte, Lte (Int × Int → Bool)
• Logic: And, Or, Implies (Bool × Bool → Bool)

Variants

Add

Addition.

Sub

Subtraction.

Mul

Multiplication.

Div

Integer division (Euclidean, matching Z3’s div).

FloorDiv

Floor division (a // b) — the quotient rounded toward negative infinity, exactly. Encoded as to_int(to_real(a) / to_real(b)) (Z3’s to_int is the floor function), which is precise across every sign combination — unlike VerifyOp::Div, whose Euclidean rounding only coincides with floor when the divisor is positive.

Eq

Equality.

Neq

Inequality.

Gt

Greater than.

Lt

Less than.

Gte

Greater than or equal.

Lte

Less than or equal.

And

Conjunction.

Or

Disjunction.

Implies

Material implication.

Trait Implementations

impl Clone for VerifyOp

fn clone(&self) -> VerifyOp

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for VerifyOp

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for VerifyOp

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for VerifyOp

fn eq(&self, other: &VerifyOp) -> 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 VerifyOp

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 VerifyOp

impl Eq for VerifyOp

impl StructuralPartialEq for VerifyOp