[−][src]Struct boolector::BV

pub struct BV<R: AsRef<Btor> + Clone> { /* fields omitted */ }

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.

Methods

`impl<R: AsRef<Btor> + Clone> BV<R>`[src]

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

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.

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`[src]

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`[src]

Create a new constant BV representing the given signed integer. The new BV will have the width width.

`pub fn from_u32(btor: R, u: u32, width: u32) -> Self`[src]

Create a new constant BV representing the given unsigned integer. The new BV will have the width width.

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

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

Create a new constant BV representing the given signed integer. The new BV will have the width width.

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

Create a new constant BV representing the given unsigned integer. The new BV will have the width width.

`pub fn zero(btor: R, width: u32) -> Self`[src]

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`[src]

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`[src]

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`[src]

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`[src]

Create a new constant BV from the given string num representing a (signed) decimal number. The new BV will have the width width.

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

Create a new constant BV from the given string num representing a hexadecimal number. The new BV will have the width width.

`pub fn as_binary_str(&self) -> Option<String>`[src]

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>`[src]

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>`[src]

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`[src]

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`[src]

Get the Btor which this BV belongs to

`pub fn get_id(&self) -> i32`[src]

Get the id of the BV

`pub fn get_width(&self) -> u32`[src]

Get the bitwidth of the BV

`pub fn get_symbol(&self) -> Option<&str>`[src]

Get the symbol of the BV, if one was assigned

`pub fn set_symbol(&mut self, symbol: Option<&str>)`[src]

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

`pub fn is_const(&self) -> bool`[src]

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`[src]

Does self have the same width as other?

`pub fn assert(&self)`[src]

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)`[src]

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`[src]

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`[src]

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

`pub fn _ne(&self, other: &Self) -> Self`[src]

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

`pub fn add(&self, other: &Self) -> Self`[src]

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

`pub fn sub(&self, other: &Self) -> Self`[src]

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

`pub fn mul(&self, other: &Self) -> Self`[src]

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

`pub fn udiv(&self, other: &Self) -> Self`[src]

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

`pub fn sdiv(&self, other: &Self) -> Self`[src]

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

`pub fn urem(&self, other: &Self) -> Self`[src]

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`[src]

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

`pub fn smod(&self, other: &Self) -> Self`[src]

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

`pub fn inc(&self) -> Self`[src]

Increment operation

`pub fn dec(&self) -> Self`[src]

Decrement operation

`pub fn neg(&self) -> Self`[src]

Two's complement negation

`pub fn uaddo(&self, other: &Self) -> Self`[src]

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`[src]

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`[src]

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`[src]

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`[src]

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`[src]

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`[src]

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`[src]

Bitwise not operation (one's complement)

`pub fn and(&self, other: &Self) -> Self`[src]

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

`pub fn or(&self, other: &Self) -> Self`[src]

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

`pub fn xor(&self, other: &Self) -> Self`[src]

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

`pub fn nand(&self, other: &Self) -> Self`[src]

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

`pub fn nor(&self, other: &Self) -> Self`[src]

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

`pub fn xnor(&self, other: &Self) -> Self`[src]

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

`pub fn sll(&self, other: &Self) -> Self`[src]

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.