Struct BitVec 

pub struct BitVec { /* private fields */ }

Implementation of the Lean BitVec in Rust. The Lean version is a wrapper around a Fin, a finite natural number that is guaranteed to be less than 2^width. In our implementation we use a BigUint and enforce the invariant that it is less than 2^width. Trying to create a bit-vector from a value greater than 2^width will truncate the value.

Implementations

impl BitVec

pub fn of_nat(width: Width, v: Nat) -> Self

Converts an (unsigned) Nat into a BitVec of the given width.

Silently wraps if v does not fit.

pub fn of_int(width: Width, v: Int) -> Self

Converts a (signed) Int into a BitVec of the given width.

Silently wraps if v does not fit.

pub fn of_u128(width: Width, val: u128) -> Self

Converts a u128 into a BitVec of the given width.

Silently wraps if val does not fit.

pub fn of_i128(width: Width, val: i128) -> Self

Converts an i128 into a BitVec of the given width.

Silently wraps if val does not fit.

pub fn to_nat(&self) -> Nat

Interprets a BitVec as a Nat.

pub fn as_nat(&self) -> &Nat

Interprets a BitVec as a Nat.

pub fn to_int(&self) -> Int

Interprets a BitVec as an Int.

pub fn extract_bits(&self, low: u32, high: u32) -> Result<Self, BitVecError>

Returns an integer representing the extracted bits from low to high, inclusive.

low and/or high may be 0 without causing errors. However, we must have low <= high < self.width, else we’ll get Err (not panic).

pub const fn width(&self) -> Width

Returns the bit-width of the bit-vector.

pub fn signed_min(n: Width) -> Int

Returns (as Int) the minimum signed value that fits in the given bit-width.

Compare to int_min(), which returns the minimum signed value as a BitVec.

pub fn signed_max(n: Width) -> Int

Returns the maximum signed value that fits in the given bit-width.

pub fn overflows(n: Width, i: &Int) -> bool

Checks if the given Int fits in the bit-width.

pub fn not(&self) -> Self

Bitwise not.

pub fn neg(&self) -> Self

Bit-vector negation.

pub fn int_min(width: Width) -> Self

Minimum signed value of the given bit-width, encoded as a BitVec.

Compare to signed_min(), which returns the minimum signed value as an Int.

pub fn slt(lhs: &Self, rhs: &Self) -> Result<bool, BitVecError>

Bit-vector signed less-than.

pub fn sle(lhs: &Self, rhs: &Self) -> Result<bool, BitVecError>

Bit-vector signed less-than-or-equal.

pub fn ule(lhs: &Self, rhs: &Self) -> Result<bool, BitVecError>

Bit-vector unsigned less-than-or-equal.

pub fn ult(lhs: &Self, rhs: &Self) -> Result<bool, BitVecError>

Bit-vector unsigned less-than.

pub fn add(lhs: &Self, rhs: &Self) -> Result<Self, BitVecError>

Bit-vector addition.

Only returns Err if the lhs and rhs widths mismatch. In particular, overflow is not an Err.

pub fn sub(lhs: &Self, rhs: &Self) -> Result<Self, BitVecError>

Bit-vector subtraction.

Only returns Err if the lhs and rhs widths mismatch. In particular, overflow is not an Err.

pub fn mul(lhs: &Self, rhs: &Self) -> Result<Self, BitVecError>

Bit-vector multiplication.

Only returns Err if the lhs and rhs widths mismatch. In particular, overflow is not an Err.

pub fn udiv(lhs: &Self, rhs: &Self) -> Result<Self, BitVecError>

Bit-vector unsigned division.

Semantics to match SMT bit-vector theory here: https://smt-lib.org/theories-FixedSizeBitVectors.shtml

Only returns Err if the lhs and rhs widths mismatch. In particular, overflow is not an Err.

pub fn urem(lhs: &Self, rhs: &Self) -> Result<Self, BitVecError>

Bit-vector unsigned remainder.

Semantics to match SMT bit-vector theory here: https://smt-lib.org/theories-FixedSizeBitVectors.shtml

Only returns Err if the lhs and rhs widths mismatch. In particular, overflow is not an Err.

pub fn sdiv(lhs: &Self, rhs: &Self) -> Result<Self, BitVecError>

Bit-vector signed division.

Semantics to match SMT bit-vector logic here: https://smt-lib.org/logics-all.shtml

Only returns Err if the lhs and rhs widths mismatch. In particular, overflow is not an Err.

pub fn srem(lhs: &Self, rhs: &Self) -> Result<Self, BitVecError>

Bit-vector signed remainder.

Semantics to match SMT bit-vector logic here: https://smt-lib.org/logics-all.shtml

Only returns Err if the lhs and rhs widths mismatch. In particular, overflow is not an Err.

pub fn smod(lhs: &Self, rhs: &Self) -> Result<Self, BitVecError>

Bit-vector signed modulus.

Semantics to match SMT bit-vector logic here: https://smt-lib.org/logics-all.shtml

Only returns Err if the lhs and rhs widths mismatch. In particular, overflow is not an Err.

pub fn shl(lhs: &Self, rhs: &Self) -> Result<Self, BitVecError>

Bit-vector left shift.

Returns Err if the lhs and rhs widths mismatch, or if the shift amount does not fit in a u32.

pub fn lshr(lhs: &Self, rhs: &Self) -> Result<Self, BitVecError>

Bit-vector logical right shift.

Returns Err if the lhs and rhs widths mismatch, or if the shift amount does not fit in a u32.

pub fn concat(lhs: &Self, rhs: &Self) -> Result<Self, BitVecError>

Bit-vector concatenation.

Panics if the total width exceeds u32::MAX. As of this writing, we shouldn’t ever construct any bitvector longer than 128, which is an extremely long way from u32::MAX.

pub fn zero_extend(bv: &Self, n: Width) -> Self

Bit-vector unsigned (zero) extension.

This matches the Lean implementation that just adjusts the length of the bit-vector to match n (and not the SMT-LIB implementation that zero extends the bit-vector by n bits). If n is less than the current bit-width it will truncate

Trait Implementations

impl Clone for BitVec

fn clone(&self) -> BitVec

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BitVec

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

Formats the value using the given formatter.

impl Display for BitVec

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

Formats the value using the given formatter.

impl Eq for BitVec

impl From<BitVec> for Term

fn from(bv: BitVec) -> Self

Converts to this type from the input type.

impl Hash for BitVec

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Ord for BitVec

fn cmp(&self, other: &BitVec) -> Ordering

This method returns an Ordering between self and other.

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

where Self: Sized,

Compares and returns the maximum of two values.

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

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

fn clamp_to<R>(self, range: R) -> Self

where Self: Sized, R: ClampBounds<Self>,

🔬This is a nightly-only experimental API. (clamp_to)

Restrict a value to a certain range.

impl PartialEq for BitVec

fn eq(&self, other: &BitVec) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl PartialOrd for BitVec

fn partial_cmp(&self, other: &BitVec) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl StructuralPartialEq for BitVec