Enum rustproof_libsmt::theories::array_ex::OpCodes

pub enum OpCodes<X, Y, Z> where
    X: Debug + Display + Clone,
    Y: Debug + Display + Clone,
    Z: Debug + Display + Clone,  {
    Select,
    Store,
    FreeVar(String),
    Const(Sorts<X, Y>, Box<Z>),
}

Variants

SelectStoreFreeVar(String)Const(Sorts<X, Y>, Box<Z>)

Trait Implementations

impl<X: Clone, Y: Clone, Z: Clone> Clone for OpCodes<X, Y, Z> where
    X: Debug + Display + Clone,
    Y: Debug + Display + Clone,
    Z: Debug + Display + Clone, 

fn clone(&self) -> OpCodes<X, Y, Z>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<X: Debug, Y: Debug, Z: Debug> Debug for OpCodes<X, Y, Z> where
    X: Debug + Display + Clone,
    Y: Debug + Display + Clone,
    Z: Debug + Display + Clone, 

fn fmt(&self, __arg_0: &mut Formatter) -> Result

Formats the value using the given formatter.

impl<X, Y, Z> Display for OpCodes<X, Y, Z> where
    X: Debug + Display + Clone,
    Y: Debug + Display + Clone,
    Z: Debug + Display + Clone, 

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

Formats the value using the given formatter.

impl<X, Y, Z> SMTNode for OpCodes<X, Y, Z> where
    X: Debug + Display + Clone,
    Z: Debug + Display + Clone,
    Y: Debug + Display + Clone, 

fn is_var(&self) -> bool

Returns true if the node is a symbolic variable

fn is_const(&self) -> bool

Returns true if the node is a constant value

fn is_fn(&self) -> bool

Returns true if the node is a function

impl Into<QF_AUFBV_Fn> for OpCodes<QF_AUFBV_Sorts, QF_AUFBV_Sorts, QF_AUFBV_Fn>

fn into(self) -> QF_AUFBV_Fn

Performs the conversion.

impl Into<QF_ABV_Fn> for OpCodes<QF_ABV_Sorts, QF_ABV_Sorts, QF_ABV_Fn>

fn into(self) -> QF_ABV_Fn

Performs the conversion.