Enum 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 duplicate 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.

impl PartialEq for Var

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

Tests for self and other values to be equal, and is used by ==.

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

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