Enum BoundedExpr 

pub enum BoundedExpr {
    Var(String),
    Bool(bool),
    Int(i64),
    And(Box<BoundedExpr>, Box<BoundedExpr>),
    Or(Box<BoundedExpr>, Box<BoundedExpr>),
    Not(Box<BoundedExpr>),
    Implies(Box<BoundedExpr>, Box<BoundedExpr>),
    Eq(Box<BoundedExpr>, Box<BoundedExpr>),
    Lt(Box<BoundedExpr>, Box<BoundedExpr>),
    Gt(Box<BoundedExpr>, Box<BoundedExpr>),
    Lte(Box<BoundedExpr>, Box<BoundedExpr>),
    Gte(Box<BoundedExpr>, Box<BoundedExpr>),
    Unsupported(String),
    BitVecConst {
        width: u32,
        value: u64,
    },
    BitVecVar(String, u32),
    BitVecBinary {
        op: BitVecBoundedOp,
        left: Box<BoundedExpr>,
        right: Box<BoundedExpr>,
    },
    BitVecExtract {
        high: u32,
        low: u32,
        operand: Box<BoundedExpr>,
    },
    BitVecConcat(Box<BoundedExpr>, Box<BoundedExpr>),
    ArraySelect {
        array: Box<BoundedExpr>,
        index: Box<BoundedExpr>,
    },
    ArrayStore {
        array: Box<BoundedExpr>,
        index: Box<BoundedExpr>,
        value: Box<BoundedExpr>,
    },
    IntBinary {
        op: ArithBoundedOp,
        left: Box<BoundedExpr>,
        right: Box<BoundedExpr>,
    },
    Comparison {
        op: CmpBoundedOp,
        left: Box<BoundedExpr>,
        right: Box<BoundedExpr>,
    },
    ForAll {
        var: String,
        sort: BoundedSort,
        body: Box<BoundedExpr>,
    },
    Exists {
        var: String,
        sort: BoundedSort,
        body: Box<BoundedExpr>,
    },
    Apply {
        name: String,
        args: Vec<BoundedExpr>,
    },
}

A verification expression in the bounded timestep model. This is a Z3-ready IR — each node maps directly to a Z3 AST construct.

Variants

Var(String)

Boolean variable: “signal@timestep”

Bool(bool)

Boolean literal

Int(i64)

Integer literal

And(Box<BoundedExpr>, Box<BoundedExpr>)

Conjunction

Or(Box<BoundedExpr>, Box<BoundedExpr>)

Disjunction

Not(Box<BoundedExpr>)

Negation

Implies(Box<BoundedExpr>, Box<BoundedExpr>)

Implication: a → b

Eq(Box<BoundedExpr>, Box<BoundedExpr>)

Equality: a == b

Lt(Box<BoundedExpr>, Box<BoundedExpr>)

Less than: a < b

Gt(Box<BoundedExpr>, Box<BoundedExpr>)

Greater than: a > b

Lte(Box<BoundedExpr>, Box<BoundedExpr>)

Less than or equal: a <= b

Gte(Box<BoundedExpr>, Box<BoundedExpr>)

Greater than or equal: a >= b

Unsupported(String)

Unsupported construct (fail closed, not silently true)

BitVecConst

Bitvector constant with explicit width

Fields

width: u32

value: u64

BitVecVar(String, u32)

Bitvector variable with known width

BitVecBinary

Bitvector binary operation

Fields

op: BitVecBoundedOp

left: Box<BoundedExpr>

right: Box<BoundedExpr>

BitVecExtract

Bitvector extraction: operand[high:low]

Fields

high: u32

low: u32

operand: Box<BoundedExpr>

BitVecConcat(Box<BoundedExpr>, Box<BoundedExpr>)

Bitvector concatenation

ArraySelect

Array select: array[index]

Fields

array: Box<BoundedExpr>

index: Box<BoundedExpr>

ArrayStore

Array store: array[index] := value

Fields

array: Box<BoundedExpr>

index: Box<BoundedExpr>

value: Box<BoundedExpr>

IntBinary

Integer arithmetic binary operation

Fields

op: ArithBoundedOp

left: Box<BoundedExpr>

right: Box<BoundedExpr>

Comparison

Comparison returning Bool from Int/BV operands

Fields

op: CmpBoundedOp

left: Box<BoundedExpr>

right: Box<BoundedExpr>

ForAll

Universal quantifier

Fields

var: String

sort: BoundedSort

body: Box<BoundedExpr>

Exists

Existential quantifier

Fields

var: String

sort: BoundedSort

body: Box<BoundedExpr>

Apply

Uninterpreted function application (system functions like $onehot0, $bits, $clog2)

Fields

name: String

args: Vec<BoundedExpr>

Trait Implementations

impl Clone for BoundedExpr

fn clone(&self) -> BoundedExpr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BoundedExpr

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

Formats the value using the given formatter.

impl PartialEq for BoundedExpr

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