Enum SmtTerm 

pub enum SmtTerm {
    Place(PlaceKey),
    Value(String),
    Const(u64),
    ConstParam(String),
    Add(Box<SmtTerm>, Box<SmtTerm>),
    Sub(Box<SmtTerm>, Box<SmtTerm>),
    Mul(Box<SmtTerm>, Box<SmtTerm>),
    Div(Box<SmtTerm>, Box<SmtTerm>),
    Rem(Box<SmtTerm>, Box<SmtTerm>),
}

Common SMT term used by diagnostics and property-independent query building.

Variants

Place(PlaceKey)

Value(String)

Const(u64)

ConstParam(String)

Const-generic parameter value (produces the same SMT constant as term_for_value for AbstractValue::Const).

Add(Box<SmtTerm>, Box<SmtTerm>)

Sub(Box<SmtTerm>, Box<SmtTerm>)

Mul(Box<SmtTerm>, Box<SmtTerm>)

Div(Box<SmtTerm>, Box<SmtTerm>)

Rem(Box<SmtTerm>, Box<SmtTerm>)

Implementations

impl SmtTerm

pub fn describe(&self) -> String

Render this term in compact source-facing form.

Trait Implementations

impl Clone for SmtTerm

fn clone(&self) -> SmtTerm

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SmtTerm

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

Formats the value using the given formatter.