Enum rsmt2::examples::print_time::Var

pub enum Var {
    NSVar(Sym),
    SVar0(Sym),
    SVar1(Sym),
}

A variable wraps a symbol.

Variants

NSVar(Sym)

Variable constant in time (Non-Stateful Var: NSVar).

SVar0(Sym)

State variable in the current step.

SVar1(Sym)

State variable in the next step.

Implementations

impl Var

pub fn sym(&self) -> &str

Symbol of a variable.

pub fn nsvar(s: &str) -> Self

Non-stateful variable constructor.

pub fn svar0(s: &str) -> Self

State variable in the current step.

pub fn svar1(s: &str) -> Self

State variable in the next step.

pub fn unroll<'a, 'b>(&'a self, off: &'b Offset) -> Unrolled<'b, &'a Var>

Given an offset, an S-expression can be unrolled.

Trait Implementations

impl Clone for Var

fn clone(&self) -> Var

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Var

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

Formats the value using the given formatter.

impl<'a> Expr2Smt<&'a Offset> for Var

fn expr_to_smt2<Writer: Write>(
    &self,
    writer: &mut Writer,
    off: &'a Offset
) -> SmtRes<()>

Prints an expression to a writer given some info.

fn to_smt_named<Sym>(self, name: Sym) -> NamedExpr<Sym, Self, Info>where
    Sym: Sym2Smt,
    Self: Sized,

Gives a name to an expression (owned version).

fn as_smt_named<Sym>(&self, name: Sym) -> NamedExpr<Sym, &Self, Info>where
    Sym: Sym2Smt,
    Self: Sized,

Gives a name to an expression (borrowed version).

impl PartialEq<Var> for Var

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

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<'a> Sym2Smt<&'a Offset> for Var

fn sym_to_smt2<Writer: Write>(
    &self,
    writer: &mut Writer,
    off: &'a Offset
) -> SmtRes<()>

Prints a symbol to a writer given some info.

impl StructuralPartialEq for Var