Trait SmtBV

pub trait SmtBV<'a, S: SmtSolver<'a, BV = Self>>:
    Clone
    + Debug
    + Display
    + Add<Output = Self>
    + Sub<Output = Self>
    + Mul<Output = Self>
    + BitOr<Output = Self>
    + BitAnd<Output = Self>
    + BitXor<Output = Self>
    + Not<Output = Self>
    + Sized {
Show 28 methods    // Required methods
    fn is_identical(&self, other: &Self) -> bool;
    fn concat(self, other: Self) -> Self;
    fn extract(self, hi: u32, lo: u32) -> Self;
    fn zero_ext(self, num: u32) -> Self;
    fn sign_ext(self, num: u32) -> Self;
    fn bvshl(self, count: Self) -> Self;
    fn bvlshr(self, count: Self) -> Self;
    fn bvashr(self, count: Self) -> Self;
    fn bvurem(self, n: Self) -> Self;
    fn bvsrem(self, n: Self) -> Self;
    fn bvudiv(self, n: Self) -> Self;
    fn bvsdiv(self, n: Self) -> Self;
    fn bvrotl(self, count: Self) -> Self;
    fn bvrotr(self, count: Self) -> Self;
    fn bvslt(self, other: Self) -> S::Bool;
    fn bvsge(self, other: Self) -> S::Bool;
    fn bvsgt(self, other: Self) -> S::Bool;
    fn bvugt(self, other: Self) -> S::Bool;
    fn bvult(self, other: Self) -> S::Bool;
    fn bvule(self, other: Self) -> S::Bool;
    fn bvuge(self, other: Self) -> S::Bool;
    fn _eq(self, other: Self) -> S::Bool;
    fn simplify(self) -> Self;
    fn get_size(&self) -> u32;
    fn as_u64(&self) -> Option<u64>;

    // Provided methods
    fn into_dynamic(self) -> Dynamic<'a, S> { ... }
    fn swap_bytes(self, num_bytes: usize) -> Self { ... }
    fn swap_bytes_to_128bits(self, num_bytes: usize) -> Self { ... }
}

Expand description

BitVector expressions in the SMT solver.

Most operation names correspond directly to the SMT functions and are not documented here.

Required Methods§

fn is_identical(&self, other: &Self) -> bool

Returns true if both expressions are structurally identical.

fn concat(self, other: Self) -> Self

fn extract(self, hi: u32, lo: u32) -> Self

fn zero_ext(self, num: u32) -> Self

fn sign_ext(self, num: u32) -> Self

fn bvshl(self, count: Self) -> Self

fn bvlshr(self, count: Self) -> Self

fn bvashr(self, count: Self) -> Self

fn bvurem(self, n: Self) -> Self

fn bvsrem(self, n: Self) -> Self

fn bvudiv(self, n: Self) -> Self

fn bvsdiv(self, n: Self) -> Self

fn bvrotl(self, count: Self) -> Self

fn bvrotr(self, count: Self) -> Self

fn bvslt(self, other: Self) -> S::Bool

fn bvsge(self, other: Self) -> S::Bool

fn bvsgt(self, other: Self) -> S::Bool

fn bvugt(self, other: Self) -> S::Bool

fn bvult(self, other: Self) -> S::Bool

fn bvule(self, other: Self) -> S::Bool

fn bvuge(self, other: Self) -> S::Bool

fn _eq(self, other: Self) -> S::Bool

Returns an SMT expression that performs an equality comparison between the two bitvectors.

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

fn get_size(&self) -> u32

Returns the size of the bitvector.

fn as_u64(&self) -> Option<u64>

Converts the bitvector to an u64, if possible.

Provided Methods§

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the bitvector into a Dynamic expression.

fn swap_bytes(self, num_bytes: usize) -> Self

Swaps the lowest num_bytes in the bitvector.

fn swap_bytes_to_128bits(self, num_bytes: usize) -> Self

Swaps the lowest num_bytes in the bitvector, and zero-extends to an 128-bit bitvector.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§

§

impl<'ctx> SmtBV<'ctx, Z3Solver<'ctx>> for BV<'ctx>

§

Trait SmtBVCopy item path