Struct BV

pub struct BV<'ctx>(/* private fields */);

A Z3 bitvector.

Implementations

impl<'ctx> BV<'ctx>

pub fn from_z3(bv: BV<'ctx>) -> Self

Wraps a [z3::ast::BV].

pub fn as_z3(&self) -> &BV<'_>

Returns the wrapped [z3::ast::BV].

Trait Implementations

impl<'ctx> Add for BV<'ctx>

type Output = BV<'ctx>

The resulting type after applying the + operator.

fn add(self, rhs: Self) -> Self::Output

Performs the + operation.

impl BitAnd for BV<'_>

type Output = BV<'_>

The resulting type after applying the & operator.

fn bitand(self, rhs: Self) -> Self::Output

Performs the & operation.

impl BitOr for BV<'_>

type Output = BV<'_>

The resulting type after applying the | operator.

fn bitor(self, rhs: Self) -> Self::Output

Performs the | operation.

impl BitXor for BV<'_>

type Output = BV<'_>

The resulting type after applying the ^ operator.

fn bitxor(self, rhs: Self) -> Self::Output

Performs the ^ operation.

impl<'ctx> Clone for BV<'ctx>

fn clone(&self) -> BV<'ctx>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'ctx> Debug for BV<'ctx>

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

Formats the value using the given formatter.

impl Display for BV<'_>

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

Formats the value using the given formatter.

impl<'ctx> Mul for BV<'ctx>

type Output = BV<'ctx>

The resulting type after applying the * operator.

fn mul(self, rhs: Self) -> Self::Output

Performs the * operation.

impl Neg for BV<'_>

type Output = BV<'_>

The resulting type after applying the - operator.

fn neg(self) -> Self::Output

Performs the unary - operation.

impl Not for BV<'_>

type Output = BV<'_>

The resulting type after applying the ! operator.

fn not(self) -> Self::Output

Performs the unary ! operation.

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

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 get_size(&self) -> u32

Returns the size of the bitvector.

fn _eq(self, other: Self) -> Bool<'ctx>

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

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 bvslt(self, other: Self) -> Bool<'ctx>

fn bvsge(self, other: Self) -> Bool<'ctx>

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

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

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

Returns true if both expressions are structurally identical.

fn bvsgt(self, other: Self) -> Bool<'ctx>

fn bvugt(self, other: Self) -> Bool<'ctx>

fn bvult(self, other: Self) -> Bool<'ctx>

fn bvule(self, other: Self) -> Bool<'ctx>

fn bvuge(self, other: Self) -> Bool<'ctx>

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

Converts the bitvector to an u64, if possible.

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.

impl<'ctx> Sub for BV<'ctx>

type Output = BV<'ctx>

The resulting type after applying the - operator.

fn sub(self, rhs: Self) -> Self::Output

Performs the - operation.