Enum ModelType 

pub enum ModelType {
    Unspecified,
    Auto,
    Int,
    Bool,
    Unit,
    BitVec(Option<usize>),
    Struct(Vec<ModelField>),
    Named(Ident),
}

A model of an SMT-LIB type.

Variants

Unspecified

Unspecified type.

Unlike an auto-derived type, unspecified is a concrete type. However, values of this type cannot be used for anything non-trivial. It is intended to be used as a placeholder for a type that is not yet known, but only appears in rules that are not yet covered by verification.

Auto

Automatically deduced primitive type, left to type-inference to determine.

Int

SMT-LIB Int

Bool

SMT-LIB Bool

Unit

Unit type.

BitVec(Option<usize>)

SMT-LIB bitvector, but with a potentially-polymorphic width

Struct(Vec<ModelField>)

Structured type.

Named(Ident)

Same model as the named type.

Trait Implementations

impl Clone for ModelType

fn clone(&self) -> ModelType

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ModelType

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

Formats the value using the given formatter.

impl Eq for ModelType

impl PartialEq for ModelType

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for ModelType

impl ToSExpr for ModelType

fn to_sexpr(&self) -> SExpr

Convert the given value to an S-expression.