Struct boolector::Array

pub struct Array<R: Borrow<Btor> + Clone> { /* fields omitted */ }

An Array in Boolector is really just a map from BVs to BVs.

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

Implementations

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

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

Create a new Array which maps BVs of width index_width to BVs of width element_width. All values in the Array will be unconstrained.

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

Both index_width and element_width must not be 0.

Example

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

// `arr` is an `Array` which maps 8-bit values to 8-bit values
let arr = Array::new(btor.clone(), 8, 8, Some("arr"));

// Write the value `3` to array index `7`
let three = BV::from_u32(btor.clone(), 3, 8);
let seven = BV::from_u32(btor.clone(), 7, 8);
let arr2 = arr.write(&seven, &three);

// Read back out the resulting value
let read_bv = arr2.read(&seven);

// should be the value `3`
assert_eq!(read_bv.as_u64().unwrap(), 3);

pub fn new_initialized(
    btor: R,
    index_width: u32,
    element_width: u32,
    val: &BV<R>
) -> Self

Create a new Array which maps BVs of width index_width to BVs of width element_width. The Array will be initialized so that all indices map to the same constant value val.

Both index_width and element_width must not be 0.

Example

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

// `arr` is an `Array` which maps 8-bit values to 8-bit values.
// It is initialized such that all entries are the constant `42`.
let fortytwo = BV::from_u32(btor.clone(), 42, 8);
let arr = Array::new_initialized(btor.clone(), 8, 8, &fortytwo);

// Reading the value at any index should produce `42`.
let read_bv = arr.read(&BV::from_u32(btor.clone(), 61, 8));
assert_eq!(btor.sat(), SolverResult::Sat);
assert_eq!(read_bv.get_a_solution().as_u64().unwrap(), 42);

// Write the value `3` to array index `7`
let three = BV::from_u32(btor.clone(), 3, 8);
let seven = BV::from_u32(btor.clone(), 7, 8);
let arr2 = arr.write(&seven, &three);

// Read back out the value at index `7`. It should be `3`.
let read_bv = arr2.read(&seven);
assert_eq!(read_bv.as_u64().unwrap(), 3);

// Reading the value at any other index should still produce `42`.
let read_bv = arr2.read(&BV::from_u32(btor.clone(), 99, 8));
assert_eq!(btor.sat(), SolverResult::Sat);
//assert_eq!(read_bv.get_a_solution().as_u64().unwrap(), 42);

pub fn get_index_width(&self) -> u32

Get the bitwidth of the index type of the Array

pub fn get_element_width(&self) -> u32

Get the bitwidth of the element type of the Array

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

Get the symbol of the Array, if one was assigned

pub fn is_const(&self) -> bool

Does the Array have a constant value?

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

Does self have the same index and element widths as other?

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

Array equality. self and other must have the same index and element widths.

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

Array inequality. self and other must have the same index and element widths.

pub fn read(&self, index: &BV<R>) -> BV<R>

Array read: get the value in the Array at the given index

pub fn write(&self, index: &BV<R>, value: &BV<R>) -> Self

Array write: return a new Array which has value at position index, and all other elements unchanged.

Trait Implementations

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

pub fn clone(&self) -> Self

Returns a copy of the value.

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

Performs copy-assignment from source.

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

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

Formats the value using the given formatter.

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

pub fn drop(&mut self)

Executes the destructor for this type.

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

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

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

This method tests for self and other values to be equal, and is used by ==.

pub fn ne(&self, other: &Array<R>) -> bool

This method tests for !=.

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

impl<R: Borrow<Btor> + Clone> StructuralEq for Array<R>

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

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