Struct BV

pub struct BV<R: Borrow<Btor> + Clone> { /* private fields */ }

A bitvector object: that is, a single symbolic value, consisting of some number of symbolic bits.

This is generic in the Btor reference type. For instance, you could use BV<Rc<Btor>> for single-threaded applications, or BV<Arc<Btor>> for multi-threaded applications.

Implementations

impl<R: Borrow<Btor> + Clone> BV<R>

pub fn new(btor: R, width: u32, symbol: Option<&str>) -> Self

Create a new unconstrained BV variable of the given width.

The symbol, if present, will be used to identify the BV when printing a model or dumping to file. It must be unique if it is present.

width must not be 0.

Example

let btor = Rc::new(Btor::new());
btor.set_opt(BtorOption::ModelGen(ModelGen::All));

// An 8-bit unconstrained `BV` with the symbol "foo"
let bv = BV::new(btor.clone(), 8, Some("foo"));

// Assert that it must be greater than `3`
bv.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert();

// Now any solution must give it a value greater than `3`
assert_eq!(btor.sat(), SolverResult::Sat);
let solution = bv.get_a_solution().as_u64().unwrap();
assert!(solution > 3);

pub fn from_bool(btor: R, b: bool) -> Self

Create a new constant BV representing the given bool (either constant true or constant false).

The resulting BV will be either constant 0 or constant 1, and will have bitwidth 1.

pub fn from_i32(btor: R, i: i32, width: u32) -> Self

Create a new constant BV representing the given signed integer. The new BV will have the width width, which must not be 0.

pub fn from_u32(btor: R, u: u32, width: u32) -> Self

Create a new constant BV representing the given unsigned integer. The new BV will have the width width, which must not be 0.

For a code example, see BV::new().

pub fn from_i64(btor: R, i: i64, width: u32) -> Self

Create a new constant BV representing the given signed integer. The new BV will have the width width, which must not be 0.

pub fn from_u64(btor: R, u: u64, width: u32) -> Self

Create a new constant BV representing the given unsigned integer. The new BV will have the width width, which must not be 0.

pub fn zero(btor: R, width: u32) -> Self

Create the constant 0 of the given width. This is equivalent to from_i32(btor, 0, width), but may be more efficient.

Example

let btor = Rc::new(Btor::new());
let zero = BV::zero(btor.clone(), 8);
assert_eq!(zero.as_u64().unwrap(), 0);

pub fn one(btor: R, width: u32) -> Self

Create the constant 1 of the given width. This is equivalent to from_i32(btor, 1, width), but may be more efficient.

Example

let btor = Rc::new(Btor::new());
let one = BV::one(btor.clone(), 8);
assert_eq!(one.as_u64().unwrap(), 1);

pub fn ones(btor: R, width: u32) -> Self

Create a bitvector constant of the given width, where all bits are set to one. This is equivalent to from_i32(btor, -1, width), but may be more efficient.

Example

let btor = Rc::new(Btor::new());
let ones = BV::ones(btor.clone(), 8);
assert_eq!(ones.as_binary_str().unwrap(), "11111111");

pub fn from_binary_str(btor: R, bits: &str) -> Self

Create a new constant BV from the given string bits representing a binary number.

bits must be non-empty and consist only of ‘0’ and/or ‘1’ characters.

The resulting BV will have bitwidth equal to the length of bits.

pub fn from_dec_str(btor: R, num: &str, width: u32) -> Self

Create a new constant BV from the given string num representing a (signed) decimal number. The new BV will have the width width, which must not be 0.

pub fn from_hex_str(btor: R, num: &str, width: u32) -> Self

Create a new constant BV from the given string num representing a hexadecimal number. The new BV will have the width width, which must not be 0.

pub fn as_binary_str(&self) -> Option<String>

Get the value of the BV as a string of ’0’s and ’1’s. This method is only effective for BVs which are constant, as indicated by BV::is_const().

This method does not require the current state to be satisfiable. To get the value of nonconstant BV objects given the current constraints, see get_a_solution(), which does require that the current state be satisfiable.

Returns None if the BV is not constant.

Example

let btor = Rc::new(Btor::new());

// This `BV` is constant, so we get a `Some`
let five = BV::from_u32(btor.clone(), 5, 8);
assert_eq!(five.as_binary_str(), Some("00000101".to_owned()));

// This `BV` is not constant, so we get `None`
let unconstrained = BV::new(btor.clone(), 8, Some("foo"));
assert_eq!(unconstrained.as_binary_str(), None);

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

Get the value of the BV as a u64. This method is only effective for BVs which are constant, as indicated by BV::is_const().

This method does not require the current state to be satisfiable. To get the value of nonconstant BV objects given the current constraints, see get_a_solution(), which does require that the current state be satisfiable.

Returns None if the BV is not constant, or if the value does not fit in 64 bits.

Example

let btor = Rc::new(Btor::new());

// This `BV` is constant, so we get a `Some`
let five = BV::from_u32(btor.clone(), 5, 8);
assert_eq!(five.as_u64(), Some(5));

// This `BV` is not constant, so we get `None`
let unconstrained = BV::new(btor.clone(), 8, Some("foo"));
assert_eq!(unconstrained.as_u64(), None);

pub fn as_bool(&self) -> Option<bool>

Get the value of the BV as a bool. This method is only effective for BVs which are constant, as indicated by BV::is_const().

Returns true if the BV has a constant nonzero value, or false if the BV has a constant zero value. Returns None if the BV is not constant.

pub fn get_a_solution(&self) -> BVSolution

Get a solution for the BV according to the current model.

This requires that model generation is enabled (see Btor::set_opt), and that the most recent call to Btor::sat() returned SolverResult::Sat.

Calling this multiple times on the same BV or different arbitrary BVs (for the same Btor instance) will produce a consistent set of solutions as long as the Btor’s state is not otherwise changed. That is, this queries an underlying model which won’t change unless the Btor state changes.

For a code example, see BV::new().

pub fn get_btor(&self) -> R

Get the Btor which this BV belongs to

pub fn get_id(&self) -> i32

Get the id of the BV

pub fn get_width(&self) -> u32

Get the bitwidth of the BV

pub fn get_symbol(&self) -> Option<&str>

Get the symbol of the BV, if one was assigned

pub fn set_symbol(&mut self, symbol: Option<&str>)

Set the symbol of the BV. See notes on BV::new().

pub fn is_const(&self) -> bool

Does the BV have a constant value?

Examples

let btor = Rc::new(Btor::new());

// This `BV` is constant
let five = BV::from_u32(btor.clone(), 5, 8);
assert!(five.is_const());

// This `BV` is not constant
let unconstrained = BV::new(btor.clone(), 8, Some("foo"));
assert!(!unconstrained.is_const());

// 5 + [unconstrained] is also not constant
let sum = five.add(&unconstrained);
assert!(!sum.is_const());

// But 5 + 5 is constant
let sum = five.add(&five);
assert!(sum.is_const());

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

Does self have the same width as other?

pub fn assert(&self)

Assert that self == 1.

self must have bitwidth 1.

Example

let btor = Rc::new(Btor::new());
btor.set_opt(BtorOption::Incremental(true));
btor.set_opt(BtorOption::ModelGen(ModelGen::All));

// Create an unconstrained `BV`
let bv = BV::new(btor.clone(), 8, Some("foo"));

// Assert that it must be greater than `3`
bv.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert();

// (you may prefer this alternate style for assertions)
BV::assert(&bv.ugt(&BV::from_u32(btor.clone(), 3, 8)));

// The state is satisfiable, and any solution we get
// for `bv` must be greater than `3`
assert_eq!(btor.sat(), SolverResult::Sat);
let solution = bv.get_a_solution().as_u64().unwrap();
assert!(solution > 3);

// Now we assert that `bv` must be less than `2`
bv.ult(&BV::from_u32(btor.clone(), 2, 8)).assert();

// The state is now unsatisfiable
assert_eq!(btor.sat(), SolverResult::Unsat);

pub fn assume(&self)

Assume that the given node == 1. Assumptions are identical to assertions except that they are discarded after each call to Btor::sat().

Requires incremental usage to be enabled via Btor::set_opt().

Example

let btor = Rc::new(Btor::new());
btor.set_opt(BtorOption::Incremental(true));

// Create an unconstrained `BV`
let bv = BV::new(btor.clone(), 8, Some("foo"));

// Assert that it must be greater than `3`
bv.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert();

// The state is satisfiable
assert_eq!(btor.sat(), SolverResult::Sat);

// Temporarily assume that the `BV` is less than `2`
bv.ult(&BV::from_u32(btor.clone(), 2, 8)).assume();

// The state is now unsatisfiable
assert_eq!(btor.sat(), SolverResult::Unsat);

// The assumption only lasts until the next `sat()`
// call, so it has been discarded now
assert_eq!(btor.sat(), SolverResult::Sat);

pub fn is_failed_assumption(&self) -> bool

Returns true if this node is an assumption that forced the input formula to become unsatisfiable.

Example

let btor = Rc::new(Btor::new());
btor.set_opt(BtorOption::Incremental(true));

// Create an unconstrained `BV` and assert that it is greater
// than `3`; the state is satisfiable
let bv = BV::new(btor.clone(), 8, Some("foo"));
bv.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert();
assert_eq!(btor.sat(), SolverResult::Sat);

// Temporarily assume that the `BV` is less than `2`
let assumption = bv.ult(&BV::from_u32(btor.clone(), 2, 8));
assumption.assume();

// The state is now unsatisfiable, and `assumption` is a
// failed assumption
assert_eq!(btor.sat(), SolverResult::Unsat);
assert!(assumption.is_failed_assumption());

pub fn _eq(&self, other: &Self) -> Self

Bitvector equality. self and other must have the same bitwidth. Resulting BV will have bitwidth 1.

pub fn _ne(&self, other: &Self) -> Self

Bitvector inequality. self and other must have the same bitwidth. Resulting BV will have bitwidth 1.

pub fn add(&self, other: &Self) -> Self

Bitvector addition. self and other must have the same bitwidth.

pub fn sub(&self, other: &Self) -> Self

Bitvector subtraction. self and other must have the same bitwidth.

pub fn mul(&self, other: &Self) -> Self

Bitvector multiplication. self and other must have the same bitwidth.

pub fn udiv(&self, other: &Self) -> Self

Unsigned division. self and other must have the same bitwidth. Division by 0 produces -1.

pub fn sdiv(&self, other: &Self) -> Self

Signed division. self and other must have the same bitwidth.

pub fn urem(&self, other: &Self) -> Self

Unsigned remainder. self and other must have the same bitwidth. If other is 0, the result will be self.

pub fn srem(&self, other: &Self) -> Self

Signed remainder. self and other must have the same bitwidth. Resulting BV will have positive sign.

pub fn smod(&self, other: &Self) -> Self

Signed remainder. self and other must have the same bitwidth. Resulting BV will have sign matching the divisor.

pub fn inc(&self) -> Self

Increment operation

pub fn dec(&self) -> Self

Decrement operation

pub fn neg(&self) -> Self

Two’s complement negation

pub fn uaddo(&self, other: &Self) -> Self

Unsigned addition overflow detection. Resulting BV will have bitwidth one, and be true if adding self and other would overflow when interpreting both self and other as unsigned.

pub fn saddo(&self, other: &Self) -> Self

Signed addition overflow detection. Resulting BV will have bitwidth one, and be true if adding self and other would overflow when interpreting both self and other as signed.

pub fn usubo(&self, other: &Self) -> Self

Unsigned subtraction overflow detection. Resulting BV will have bitwidth one, and be true if subtracting self and other would overflow when interpreting both self and other as unsigned.

pub fn ssubo(&self, other: &Self) -> Self

Signed subtraction overflow detection. Resulting BV will have bitwidth one, and be true if subtracting self and other would overflow when interpreting both self and other as signed.

pub fn umulo(&self, other: &Self) -> Self

Unsigned multiplication overflow detection. Resulting BV will have bitwidth 1, and be true if multiplying self and other would overflow when interpreting both self and other as unsigned.

pub fn smulo(&self, other: &Self) -> Self

Signed multiplication overflow detection. Resulting BV will have bitwidth 1, and be true if multiplying self and other would overflow when interpreting both self and other as signed.

pub fn sdivo(&self, other: &Self) -> Self

Signed division overflow detection. Resulting BV will have bitwidth one, and be true if dividing self by other would overflow when interpreting both self and other as signed.

Signed division can overflow if self is INT_MIN and other is -1. Note that unsigned division cannot overflow.

pub fn not(&self) -> Self

Bitwise not operation (one’s complement)

pub fn and(&self, other: &Self) -> Self

Bitwise and operation. self and other must have the same bitwidth.

pub fn or(&self, other: &Self) -> Self

Bitwise or operation. self and other must have the same bitwidth.

pub fn xor(&self, other: &Self) -> Self

Bitwise xor operation. self and other must have the same bitwidth.

pub fn nand(&self, other: &Self) -> Self

Bitwise nand operation. self and other must have the same bitwidth.

pub fn nor(&self, other: &Self) -> Self

Bitwise nor operation. self and other must have the same bitwidth.

pub fn xnor(&self, other: &Self) -> Self

Bitwise xnor operation. self and other must have the same bitwidth.

pub fn sll(&self, other: &Self) -> Self

Logical shift left: shift self left by other bits. Either self and other must have the same bitwidth, or self must have a bitwidth which is a power of two and the bitwidth of other must be log2 of the bitwidth of self.

Resulting BV will have the same bitwidth as self.

pub fn srl(&self, other: &Self) -> Self

Logical shift right: shift self right by other bits. Either self and other must have the same bitwidth, or self must have a bitwidth which is a power of two and the bitwidth of other must be log2 of the bitwidth of self.

Resulting BV will have the same bitwidth as self.

pub fn sra(&self, other: &Self) -> Self

Arithmetic shift right: shift self right by other bits. Either self and other must have the same bitwidth, or self must have a bitwidth which is a power of two and the bitwidth of other must be log2 of the bitwidth of self.

Resulting BV will have the same bitwidth as self.

pub fn rol(&self, other: &Self) -> Self

Rotate self left by other bits. self must have a bitwidth which is a power of two, and the bitwidth of other must be log2 of the bitwidth of self.

Resulting BV will have the same bitwidth as self.

pub fn ror(&self, other: &Self) -> Self

Rotate self right by other bits. self must have a bitwidth which is a power of two, and the bitwidth of other must be log2 of the bitwidth of self.

Resulting BV will have the same bitwidth as self.

pub fn redand(&self) -> Self

and reduction operation: take the Boolean and of all bits in the BV. Resulting BV will have bitwidth 1.

pub fn redor(&self) -> Self

or reduction operation: take the Boolean or of all bits in the BV. Resulting BV will have bitwidth 1.

pub fn redxor(&self) -> Self

xor reduction operation: take the Boolean xor of all bits in the BV. Resulting BV will have bitwidth 1.

pub fn ugt(&self, other: &Self) -> Self

Unsigned greater than. self and other must have the same bitwidth. Resulting BV will have bitwidth 1.

pub fn ugte(&self, other: &Self) -> Self

Unsigned greater than or equal. self and other must have the same bitwidth. Resulting BV will have bitwidth 1.

pub fn sgt(&self, other: &Self) -> Self

Signed greater than. self and other must have the same bitwidth. Resulting BV will have bitwidth 1.

pub fn sgte(&self, other: &Self) -> Self

Signed greater than or equal. self and other must have the same bitwidth. Resulting BV will have bitwidth 1.

pub fn ult(&self, other: &Self) -> Self

Unsigned less than. self and other must have the same bitwidth. Resulting BV will have bitwidth 1.

pub fn ulte(&self, other: &Self) -> Self

Unsigned less than or equal. self and other must have the same bitwidth. Resulting BV will have bitwidth 1.

pub fn slt(&self, other: &Self) -> Self

Signed less than. self and other must have the same bitwidth. Resulting BV will have bitwidth 1.

pub fn slte(&self, other: &Self) -> Self

Signed less than or equal. self and other must have the same bitwidth. Resulting BV will have bitwidth 1.

pub fn uext(&self, n: u32) -> Self

Unsigned extension (zero-extension), extending by n bits. Resulting BV will have bitwidth equal to the bitwidth of self plus n.

Example

let btor = Rc::new(Btor::new());

// Create an 8-bit `BV` with value `3`
let bv = BV::from_u32(btor.clone(), 3, 8);

// Zero-extend by 56 bits
let extended = bv.uext(56);

// Resulting `BV` is 64 bits and has value `3`
assert_eq!(extended.get_width(), 64);
assert_eq!(extended.as_u64().unwrap(), 3);

pub fn sext(&self, n: u32) -> Self

Sign-extension operation, extending by n bits. Resulting BV will have bitwidth equal to the bitwidth of self plus n.

Example

let btor = Rc::new(Btor::new());

// Create an 8-bit `BV` with value `-3`
let bv = BV::from_i32(btor.clone(), -3, 8);

// Sign-extend by 56 bits
let extended = bv.sext(56);

// Resulting `BV` is 64 bits and has value `-3`
assert_eq!(extended.get_width(), 64);
assert_eq!(extended.as_u64().unwrap() as i64, -3);

pub fn slice(&self, high: u32, low: u32) -> Self

Slicing operation: obtain bits high through low (inclusive) of self. Resulting BV will have bitwidth high - low + 1.

Requires that 0 <= low <= high < self.get_width().

Example

let btor = Rc::new(Btor::new());

// Create an 8-bit `BV` with this constant value
let bv = BV::from_binary_str(btor.clone(), "01100101");

// Slice out bits 1 through 4, inclusive
let slice = bv.slice(4, 1);

// Resulting slice has width `4` and value `"0010"`
assert_eq!(slice.get_width(), 4);
assert_eq!(slice.as_binary_str().unwrap(), "0010");

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

Concatenate two bitvectors. Resulting BV will have bitwidth equal to the sum of self and other’s bitwidths.

Example

let btor = Rc::new(Btor::new());

// Create an 8-bit `BV` with value `1`
let one = BV::one(btor.clone(), 8);

// Create an 8-bit `BV` consisting of all ones
let ones = BV::ones(btor.clone(), 8);

// The concatenation has length 16 and this value
let result = ones.concat(&one);
assert_eq!(result.get_width(), 16);
assert_eq!(result.as_binary_str().unwrap(), "1111111100000001");

// Concatenate in the other order
let result = one.concat(&ones);
assert_eq!(result.get_width(), 16);
assert_eq!(result.as_binary_str().unwrap(), "0000000111111111");

pub fn repeat(&self, n: u32) -> Self

Concatenate the BV with itself n times

pub fn iff(&self, other: &Self) -> Self

Returns the BV which is true if self <=> other, else false. self and other must have bitwidth 1.

pub fn implies(&self, other: &Self) -> Self

Returns the BV which is true if self implies other, else false. self and other must have bitwidth 1.

pub fn cond_bv(&self, truebv: &Self, falsebv: &Self) -> Self

Create an if-then-else BV node. If self is true, then truebv is returned, else falsebv is returned.

self must have bitwidth 1.

Example

let btor = Rc::new(Btor::new());
btor.set_opt(BtorOption::ModelGen(ModelGen::All));

// Create an unconstrained `BV` `x`
let x = BV::new(btor.clone(), 8, Some("x"));

// `y` will be `5` if `x > 10`, else it will be `1`
let five = BV::from_u32(btor.clone(), 5, 8);
let one = BV::one(btor.clone(), 8);
let cond = x.ugt(&BV::from_u32(btor.clone(), 10, 8));
let y = cond.cond_bv(&five, &one);
// (you may prefer this alternate style)
let _y = BV::cond_bv(&cond, &five, &one);

// Now assert that `x < 7`
x.ult(&BV::from_u32(btor.clone(), 7, 8)).assert();

// As a result, `y` must be `1`
assert_eq!(btor.sat(), SolverResult::Sat);
assert_eq!(y.get_a_solution().as_u64().unwrap(), 1);

pub fn cond_array( &self, true_array: &Array<R>, false_array: &Array<R>, ) -> Array<R>

Create an if-then-else Array node. If self is true, then true_array is returned, else false_array is returned.

self must have bitwidth 1.

Trait Implementations

impl<R: Borrow<Btor> + Clone> Clone for BV<R>

fn clone(&self) -> Self

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<R: Borrow<Btor> + Clone> Debug for BV<R>

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

Formats the value using the given formatter.

impl<R: Borrow<Btor> + Clone> Drop for BV<R>

fn drop(&mut self)

Executes the destructor for this type.

impl<R: PartialEq + Borrow<Btor> + Clone> PartialEq for BV<R>

fn eq(&self, other: &BV<R>) -> bool

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<R: Eq + Borrow<Btor> + Clone> Eq for BV<R>

impl<R: Borrow<Btor> + Clone + Send> Send for BV<R>

impl<R: Borrow<Btor> + Clone> StructuralPartialEq for BV<R>

impl<R: Borrow<Btor> + Clone + Sync> Sync for BV<R>