diff --git a/src/mc/smt.rs b/src/mc/smt.rs index 6c7f126..2981096 100644 --- a/src/mc/smt.rs +++ b/src/mc/smt.rs @@ -574,4 +574,9 @@ mod tests { "a b" ); } + + #[test] + fn test_reading_smt_scalar() { + let ctx = ContextBuilder::new().build().unwrap(); + } } diff --git a/src/sim/values.rs b/src/sim/values.rs index 5409361..af9d250 100644 --- a/src/sim/values.rs +++ b/src/sim/values.rs @@ -5,7 +5,9 @@ use crate::ir::{Type, WidthInt}; use num_bigint::BigUint; use num_traits::{Num, ToPrimitive, Zero}; +use std::collections::HashMap; use std::fmt::Debug; +use std::hash::Hash; /// Contains the initial state and the inputs over `len` cycles. #[derive(Debug, Default)] @@ -325,49 +327,79 @@ pub trait ArrayValue: Debug { fn get(&self, index: ScalarValue) -> ScalarValueRef; } -#[derive(Debug, PartialEq)] -pub struct SparseArrayValue +#[derive(Debug)] +pub struct SparseArray where - I: PartialEq + TryFromValue + Debug, + I: PartialEq + TryFromValue + Debug + Hash + Eq, D: TryFromValue + IntoValueRef + Debug, { default: D, - updates: Vec<(I, D)>, + updated: HashMap, } -impl SparseArrayValue +impl SparseArray where - I: PartialEq + TryFromValue + Debug, + I: PartialEq + TryFromValue + Debug + Hash + Eq, D: TryFromValue + IntoValueRef + Debug, { fn new(default: D) -> Self { Self { default, - updates: Vec::new(), + updated: HashMap::new(), } } } -impl ArrayValue for SparseArrayValue +impl ArrayValue for SparseArray where - I: PartialEq + TryFromValue + Debug, + I: PartialEq + TryFromValue + Debug + Hash + Eq, D: TryFromValue + IntoValueRef + Debug, { fn update(&mut self, index: ScalarValue, value: ScalarValue) { - self.updates - .push((I::try_from(index).unwrap(), D::try_from(value).unwrap())); + self.updated + .insert(I::try_from(index).unwrap(), D::try_from(value).unwrap()); } fn get(&self, index: ScalarValue) -> ScalarValueRef { - // find the latest update let raw_index = I::try_from(index).unwrap(); - for (ii, dd) in self.updates.iter().rev() { - if *ii == raw_index { - return dd.into(); - } - } - // no update found - (&self.default).into() + let value = self.updated.get(&raw_index).unwrap_or(&self.default); + value.into() + } +} + +#[derive(Debug, PartialEq)] +pub struct DenseArray +where + D: TryFromValue + IntoValueRef + Debug, +{ + values: Vec, +} + +impl DenseArray +where + D: TryFromValue + IntoValueRef + Debug, +{ + pub fn new(values: Vec) -> Self { + Self { values } + } + + pub fn len(&self) -> usize { + self.values.len() + } +} + +impl ArrayValue for DenseArray +where + D: TryFromValue + IntoValueRef + Debug, +{ + fn update(&mut self, index: ScalarValue, value: ScalarValue) { + let ii = ::try_from(index).unwrap() as usize; + self.values[ii] = D::try_from(value).unwrap(); + } + + fn get(&self, index: ScalarValue) -> ScalarValueRef { + let ii = ::try_from(index).unwrap() as usize; + (&self.values[ii]).into() } }