Enum VerifyType 

pub enum VerifyType {
    Int,
    Bool,
    Object,
    BitVector(u32),
    Array(Box<VerifyType>, Box<VerifyType>),
    Real,
}

Type declarations for verification variables.

Each type maps to a Z3 sort:

VerifyType	Z3 Sort	Usage
Int	IntSort	Numeric constraints, bounds checking
Bool	BoolSort	Logical propositions
Object	Uninterpreted	Entities (people, objects, propositions)

Variants

Int

Integer type, maps to Z3 IntSort.

Bool

Boolean type, maps to Z3 BoolSort.

Object

Opaque object type for entities, maps to an uninterpreted sort.

BitVector(u32)

Fixed-width bitvector, maps to Z3 BitVecSort(n).

Array(Box<VerifyType>, Box<VerifyType>)

Array type (index → element), maps to Z3 ArraySort.

Real

Real number type, maps to Z3 RealSort (IEEE 1800-2023).

Trait Implementations

impl Clone for VerifyType

fn clone(&self) -> VerifyType

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for VerifyType

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for VerifyType

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for VerifyType

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

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

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for VerifyType

impl StructuralPartialEq for VerifyType