Trait SMTNode

pub trait SMTNode: Display {
    // Required methods
    fn is_var(&self) -> bool;
    fn is_const(&self) -> bool;

    // Provided method
    fn is_fn(&self) -> bool { ... }
}

Required Methods

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

Provided Methods

fn is_fn(&self) -> bool

Returns true if the node is a function

Implementors

impl SMTNode for LIA_Fn

impl SMTNode for QF_ABV_Fn

impl SMTNode for QF_AUFBV_Fn

impl SMTNode for QF_BV_Fn

impl SMTNode for rustproof_libsmt::theories::bitvec::OpCodes

impl SMTNode for rustproof_libsmt::theories::core::OpCodes

impl SMTNode for rustproof_libsmt::theories::integer::OpCodes

impl SMTNode for rustproof_libsmt::theories::real::OpCodes

impl SMTNode for rustproof_libsmt::theories::real_ints::OpCodes

impl<X, Y, Z> SMTNode for rustproof_libsmt::theories::array_ex::OpCodes<X, Y, Z>

where X: Debug + Display + Clone, Z: Debug + Display + Clone, Y: Debug + Display + Clone,