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
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
fn _eq(self, other: Self) -> S::Bool
Returns an SMT expression that performs an equality comparison between the two bitvectors.
fn simplify(self) -> Self
fn simplify(self) -> Self
Simplifies, if possible, the SMT expression.
Provided Methods§
fn into_dynamic(self) -> Dynamic<'a, S>
fn into_dynamic(self) -> Dynamic<'a, S>
Converts the bitvector into a Dynamic
expression.
fn swap_bytes(self, num_bytes: usize) -> Self
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
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.