Enum Exp

pub enum Exp {
    Var(Sym),
    Bits(Vec<bool>),
    Bits64(B64),
    Enum(EnumMember),
    Bool(bool),
    Eq(Box<Exp>, Box<Exp>),
    Neq(Box<Exp>, Box<Exp>),
    And(Box<Exp>, Box<Exp>),
    Or(Box<Exp>, Box<Exp>),
    Not(Box<Exp>),
    Bvnot(Box<Exp>),
    Bvand(Box<Exp>, Box<Exp>),
    Bvor(Box<Exp>, Box<Exp>),
    Bvxor(Box<Exp>, Box<Exp>),
    Bvnand(Box<Exp>, Box<Exp>),
    Bvnor(Box<Exp>, Box<Exp>),
    Bvxnor(Box<Exp>, Box<Exp>),
    Bvneg(Box<Exp>),
    Bvadd(Box<Exp>, Box<Exp>),
    Bvsub(Box<Exp>, Box<Exp>),
    Bvmul(Box<Exp>, Box<Exp>),
    Bvudiv(Box<Exp>, Box<Exp>),
    Bvsdiv(Box<Exp>, Box<Exp>),
    Bvurem(Box<Exp>, Box<Exp>),
    Bvsrem(Box<Exp>, Box<Exp>),
    Bvsmod(Box<Exp>, Box<Exp>),
    Bvult(Box<Exp>, Box<Exp>),
    Bvslt(Box<Exp>, Box<Exp>),
    Bvule(Box<Exp>, Box<Exp>),
    Bvsle(Box<Exp>, Box<Exp>),
    Bvuge(Box<Exp>, Box<Exp>),
    Bvsge(Box<Exp>, Box<Exp>),
    Bvugt(Box<Exp>, Box<Exp>),
    Bvsgt(Box<Exp>, Box<Exp>),
    Extract(u32, u32, Box<Exp>),
    ZeroExtend(u32, Box<Exp>),
    SignExtend(u32, Box<Exp>),
    Bvshl(Box<Exp>, Box<Exp>),
    Bvlshr(Box<Exp>, Box<Exp>),
    Bvashr(Box<Exp>, Box<Exp>),
    Concat(Box<Exp>, Box<Exp>),
    Ite(Box<Exp>, Box<Exp>, Box<Exp>),
    App(Sym, Vec<Exp>),
    Select(Box<Exp>, Box<Exp>),
    Store(Box<Exp>, Box<Exp>, Box<Exp>),
}

Variants

Var(Sym)

Bits(Vec<bool>)

Bits64(B64)

Enum(EnumMember)

Bool(bool)

Eq(Box<Exp>, Box<Exp>)

Neq(Box<Exp>, Box<Exp>)

And(Box<Exp>, Box<Exp>)

Or(Box<Exp>, Box<Exp>)

Not(Box<Exp>)

Bvnot(Box<Exp>)

Bvand(Box<Exp>, Box<Exp>)

Bvor(Box<Exp>, Box<Exp>)

Bvxor(Box<Exp>, Box<Exp>)

Bvnand(Box<Exp>, Box<Exp>)

Bvnor(Box<Exp>, Box<Exp>)

Bvxnor(Box<Exp>, Box<Exp>)

Bvneg(Box<Exp>)

Bvadd(Box<Exp>, Box<Exp>)

Bvsub(Box<Exp>, Box<Exp>)

Bvmul(Box<Exp>, Box<Exp>)

Bvudiv(Box<Exp>, Box<Exp>)

Bvsdiv(Box<Exp>, Box<Exp>)

Bvurem(Box<Exp>, Box<Exp>)

Bvsrem(Box<Exp>, Box<Exp>)

Bvsmod(Box<Exp>, Box<Exp>)

Bvult(Box<Exp>, Box<Exp>)

Bvslt(Box<Exp>, Box<Exp>)

Bvule(Box<Exp>, Box<Exp>)

Bvsle(Box<Exp>, Box<Exp>)

Bvuge(Box<Exp>, Box<Exp>)

Bvsge(Box<Exp>, Box<Exp>)

Bvugt(Box<Exp>, Box<Exp>)

Bvsgt(Box<Exp>, Box<Exp>)

Extract(u32, u32, Box<Exp>)

ZeroExtend(u32, Box<Exp>)

SignExtend(u32, Box<Exp>)

Bvshl(Box<Exp>, Box<Exp>)

Bvlshr(Box<Exp>, Box<Exp>)

Bvashr(Box<Exp>, Box<Exp>)

Concat(Box<Exp>, Box<Exp>)

Ite(Box<Exp>, Box<Exp>, Box<Exp>)

App(Sym, Vec<Exp>)

Select(Box<Exp>, Box<Exp>)

Store(Box<Exp>, Box<Exp>, Box<Exp>)

Implementations

impl Exp

pub fn eval(self) -> Self

pub fn modify<F>(&mut self, f: &F)

where F: Fn(&mut Exp),

Recursivly apply the supplied function to each sub-expression in a bottom-up order

pub fn modify_top_down<F>(&mut self, f: &F)

where F: Fn(&mut Exp),

Recursivly apply the supplied function to each sub-expression in a top down order

pub fn commute_extract(&mut self)

pub fn subst_once_in_place(&mut self, substs: &mut HashMap<Sym, Option<Exp>>)

pub fn infer( &self, tcx: &HashMap<Sym, Ty>, ftcx: &HashMap<Sym, (Vec<Ty>, Ty)>, ) -> Option<Ty>

Infer the type of an already well-formed SMTLIB expression

Trait Implementations

impl Clone for Exp

fn clone(&self) -> Exp

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Exp

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

Formats the value using the given formatter.