Struct BV 

pub struct BV { /* private fields */ }

A bitvector term of a known width.

Mirrors the z3::ast::BV call surface used by the semantics encoders.

Implementations

impl BV

pub fn new_const(name: impl Into<String>, width: u32) -> Self

A fresh free (symbolic) bitvector variable.

pub fn from_i64(value: i64, width: u32) -> Self

A concrete constant from a signed value (two’s-complement, masked).

pub fn from_u64(value: u64, width: u32) -> Self

A concrete constant from an unsigned value (masked to width).

pub fn get_size(&self) -> u32

Bit width of this term.

pub fn bvadd(&self, other: impl Borrow<BV>) -> BV

Modular addition.

pub fn bvsub(&self, other: impl Borrow<BV>) -> BV

Modular subtraction.

pub fn bvmul(&self, other: impl Borrow<BV>) -> BV

Modular multiplication.

pub fn bvudiv(&self, other: impl Borrow<BV>) -> BV

Unsigned division (SMT-LIB: division by zero yields all-ones).

pub fn bvsdiv(&self, other: impl Borrow<BV>) -> BV

Signed division (SMT-LIB semantics, via ordeal::lowering).

pub fn bvurem(&self, other: impl Borrow<BV>) -> BV

Unsigned remainder (via ordeal::lowering).

pub fn bvsrem(&self, other: impl Borrow<BV>) -> BV

Signed remainder (via ordeal::lowering).

pub fn bvneg(&self) -> BV

Two’s-complement negation (via ordeal::lowering).

pub fn bvand(&self, other: impl Borrow<BV>) -> BV

Bitwise AND.

pub fn bvor(&self, other: impl Borrow<BV>) -> BV

Bitwise OR.

pub fn bvxor(&self, other: impl Borrow<BV>) -> BV

Bitwise XOR.

pub fn bvnot(&self) -> BV

Bitwise NOT (via ordeal::lowering).

pub fn bvshl(&self, other: impl Borrow<BV>) -> BV

Logical shift left (SMT-LIB oversize semantics: amount >= width → 0).

pub fn bvlshr(&self, other: impl Borrow<BV>) -> BV

Logical shift right.

pub fn bvashr(&self, other: impl Borrow<BV>) -> BV

Arithmetic shift right.

pub fn bvrotl(&self, other: impl Borrow<BV>) -> BV

Rotate left by a term amount (via ordeal::lowering).

pub fn bvrotr(&self, other: impl Borrow<BV>) -> BV

Rotate right by a term amount.

pub fn extract(&self, hi: u32, lo: u32) -> BV

Bit extraction [hi:lo] (inclusive).

pub fn concat(&self, other: impl Borrow<BV>) -> BV

Concatenation: self becomes the high bits.

pub fn zero_ext(&self, by: u32) -> BV

Zero-extension by by bits.

pub fn sign_ext(&self, by: u32) -> BV

Sign-extension by by bits.

pub fn eq(&self, other: impl Borrow<BV>) -> Bool

Equality predicate (canonicalized — = is commutative).

pub fn ne(&self, other: impl Borrow<BV>) -> Bool

Disequality predicate (canonicalized — distinct is commutative).

pub fn bvult(&self, other: impl Borrow<BV>) -> Bool

Unsigned less-than.

pub fn bvule(&self, other: impl Borrow<BV>) -> Bool

Unsigned less-or-equal.

pub fn bvugt(&self, other: impl Borrow<BV>) -> Bool

Unsigned greater-than.

pub fn bvuge(&self, other: impl Borrow<BV>) -> Bool

Unsigned greater-or-equal.

pub fn bvslt(&self, other: impl Borrow<BV>) -> Bool

Signed less-than.

pub fn bvsle(&self, other: impl Borrow<BV>) -> Bool

Signed less-or-equal.

pub fn bvsgt(&self, other: impl Borrow<BV>) -> Bool

Signed greater-than.

pub fn bvsge(&self, other: impl Borrow<BV>) -> Bool

Signed greater-or-equal.

pub fn simplify(&self) -> BV

Return self unchanged; pair with BV::as_i64 / BV::as_u64, which concretely evaluate closed terms (the z3 idiom x.simplify().as_i64() keeps working).

pub fn as_i64(&self) -> Option<i64>

Concrete value of a closed (variable-free) term, as z3’s as_i64 reports it: the unsigned value when it fits in i64.

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

Concrete value of a closed (variable-free) term as u64.

Trait Implementations

impl Clone for BV

fn clone(&self) -> BV

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BV

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.