Enum rsmt2_zz::example::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.

Methods

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.

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: &Var) -> bool

This method tests for !=.

impl StructuralPartialEq for Var

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.