Enum Sort 

pub enum Sort {
    Bits(u32),
    Memory,
}

What kind of thing a term computes.

Almost everything is a bitvector, and the exception is the whole point of this type: a rule with an effect relates one memory to another, and a memory is not a number however many bits one is willing to spend on it.

Variants

Bits(u32)

A bitvector this many bits wide.

Memory

The whole of memory, a map from an address to a byte.

Implementations

impl Sort

pub fn bits(self) -> Option<u32>

How many bits wide it is, or nothing when it is not a bitvector at all.

pub fn write(self, widths: &Widths) -> String

What SMT-LIB calls it, at the widths this question is being asked at.

Trait Implementations

impl Clone for Sort

fn clone(&self) -> Sort

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for Sort

impl Debug for Sort

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

Formats the value using the given formatter.

impl Eq for Sort

impl PartialEq for Sort

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for Sort