Enum SymValue 

pub enum SymValue {
    Int(VerifyExpr),
    Bool(VerifyExpr),
    Chan(usize),
}

A symbolic LOGOS value: an integer (64-bit bitvector), a boolean, or a channel handle.

Variants

Int(VerifyExpr)

An integer value, as a width-64 bitvector VerifyExpr.

Bool(VerifyExpr)

A boolean value, as a Bool-sorted VerifyExpr.

Chan(usize)

A channel handle — an opaque id into [State::channels]. Not an SMT value; it is the dataflow conduit the determinate concurrency fragment threads Send/Receive through (and passes as a task argument).

Trait Implementations

impl Clone for SymValue

fn clone(&self) -> SymValue

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SymValue

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

Formats the value using the given formatter.