Enum rustproof_libsmt::theories::core::OpCodes

pub enum OpCodes {
    Not,
    Imply,
    And,
    Or,
    Xor,
    Cmp,
    Distinct,
    ITE,
    Const(bool),
    FreeVar(String),
}

Variants

NotImplyAndOrXorCmpDistinctITEConst(bool)FreeVar(String)

Trait Implementations

impl Clone for OpCodes

fn clone(&self) -> OpCodes

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for OpCodes

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

Formats the value using the given formatter.

impl Display for OpCodes

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

Formats the value using the given formatter.

impl SMTNode for OpCodes

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_BV_Fn> for OpCodes

fn into(self) -> QF_BV_Fn

Performs the conversion.

impl Into<QF_AUFBV_Fn> for OpCodes

fn into(self) -> QF_AUFBV_Fn

Performs the conversion.

impl Into<QF_ABV_Fn> for OpCodes

fn into(self) -> QF_ABV_Fn

Performs the conversion.

impl Into<LIA_Fn> for OpCodes

fn into(self) -> LIA_Fn

Performs the conversion.