Struct boolector::Array

pub struct Array<R: AsRef<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.

Methods

impl<R: AsRef<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.

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,
    symbol: Option<&str>,
    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.

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.

Note: This function is not available in Boolector 3.0.0 as released, and will cause linker errors if you attempt to use it with the released version of Boolector 3.0.0. It was added to Boolector's git master in September 2019 (commit a1b1408), and will presumably be part of any subsequent releases of Boolector. Until the next Boolector release, to use this function you will need to build an appropriately recent version of Boolector from source.

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, Some("arr"), &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: AsRef<Btor> + Clone + Sync> Sync for Array<R>

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

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

fn drop(&mut self)

Executes the destructor for this type.

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

impl<R: AsRef<Btor> + Clone> Clone for Array<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: PartialEq + AsRef<Btor> + Clone> PartialEq<Array<R>> for Array<R>

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

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

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

This method tests for !=.

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

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

Formats the value using the given formatter.