Enum SpecExpr

pub enum SpecExpr {
    ConstInt {
        val: i128,
        pos: Pos,
    },
    ConstBitVec {
        val: i128,
        width: i8,
        pos: Pos,
    },
    ConstBool {
        val: i8,
        pos: Pos,
    },
    ConstUnit {
        pos: Pos,
    },
    Var {
        var: Ident,
        pos: Pos,
    },
    Op {
        op: SpecOp,
        args: Vec<SpecExpr>,
        pos: Pos,
    },
    Pair {
        l: Box<SpecExpr>,
        r: Box<SpecExpr>,
    },
    Enum {
        name: Ident,
    },
}

An expression used to specify term semantics, similar to SMT-LIB syntax.

Variants

ConstInt

An operator that matches a constant integer value.

Fields

val: i128

pos: Pos

ConstBitVec

An operator that matches a constant bitvector value.

Fields

val: i128

width: i8

pos: Pos

ConstBool

An operator that matches a constant boolean value.

Fields

val: i8

pos: Pos

ConstUnit

The Unit constant value.

Fields

pos: Pos

Var

Fields

var: Ident

pos: Pos

Op

An application of a type variant or term.

Fields

op: SpecOp

args: Vec<SpecExpr>

pos: Pos

Pair

Pairs, currently used for switch statements.

Fields

l: Box<SpecExpr>

r: Box<SpecExpr>

Enum

Enums variant values (enums defined by model)

Fields

name: Ident

Trait Implementations

impl Clone for SpecExpr

fn clone(&self) -> SpecExpr

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for SpecExpr

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

Formats the value using the given formatter.

impl PartialEq for SpecExpr

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

impl StructuralPartialEq for SpecExpr