Enum Sort 

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

What kind of thing a term computes.

Most things are a bitvector, and the two exceptions are 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. A rule about a float relates two floats, and a float is not the number its bits spell either, however much it looks like one.

Variants

Bits(u32)

A bitvector this many bits wide.

Float(u32)

A float in the interchange format of this many bits, which is a different kind of thing from the bitvector of the same size: adding two of them is not adding their bits.

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.

A float is not one. Everything that asks this is about to take an extract of it or put it end to end with something, and neither is a thing to do to a float without saying so.

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