Expand description
An Array
in Boolector is really just a map from BV
s to BV
s.
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
sourceimpl<R: Borrow<Btor> + Clone> Array<R>
impl<R: Borrow<Btor> + Clone> Array<R>
sourcepub fn new(
btor: R,
index_width: u32,
element_width: u32,
symbol: Option<&str>
) -> Self
pub fn new(
btor: R,
index_width: u32,
element_width: u32,
symbol: Option<&str>
) -> Self
Create a new Array
which maps BV
s of width index_width
to BV
s 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);
sourcepub fn new_initialized(
btor: R,
index_width: u32,
element_width: u32,
val: &BV<R>
) -> Self
pub fn new_initialized(
btor: R,
index_width: u32,
element_width: u32,
val: &BV<R>
) -> Self
Create a new Array
which maps BV
s of width index_width
to BV
s 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);
sourcepub fn get_index_width(&self) -> u32
pub fn get_index_width(&self) -> u32
Get the bitwidth of the index type of the Array
sourcepub fn get_element_width(&self) -> u32
pub fn get_element_width(&self) -> u32
Get the bitwidth of the element type of the Array
sourcepub fn get_symbol(&self) -> Option<&str>
pub fn get_symbol(&self) -> Option<&str>
Get the symbol of the Array
, if one was assigned
sourcepub fn has_same_widths(&self, other: &Self) -> bool
pub fn has_same_widths(&self, other: &Self) -> bool
Does self
have the same index and element widths as other
?
sourcepub fn _eq(&self, other: &Self) -> Self
pub fn _eq(&self, other: &Self) -> Self
Array equality. self
and other
must have the same index and element widths.
sourcepub fn _ne(&self, other: &Self) -> Self
pub fn _ne(&self, other: &Self) -> Self
Array inequality. self
and other
must have the same index and element widths.
Trait Implementations
impl<R: Eq + Borrow<Btor> + Clone> Eq for Array<R>
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>
Auto Trait Implementations
impl<R> RefUnwindSafe for Array<R> where
R: RefUnwindSafe,
impl<R> Unpin for Array<R> where
R: Unpin,
impl<R> UnwindSafe for Array<R> where
R: UnwindSafe,
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
sourceimpl<T> ToOwned for T where
T: Clone,
impl<T> ToOwned for T where
T: Clone,
type Owned = T
type Owned = T
The resulting type after obtaining ownership.
sourcefn clone_into(&self, target: &mut T)
fn clone_into(&self, target: &mut T)
toowned_clone_into
)Uses borrowed data to replace owned data, usually by cloning. Read more