wip: array value

src/btor2/witness.rs

@@ -5,7 +5,7 @@
 use crate::btor2::parse::tokenize_line;
 use crate::ir;
 use crate::ir::{SignalKind, TypeCheck};
-use crate::sim::{Value, ValueStore, Witness};
+use crate::sim::{ScalarValue, ValueStore, Witness};
 use std::io::{BufRead, Write};
 
 enum ParserState {
@@ -133,7 +133,7 @@ pub fn parse_witnesses(input: &mut impl BufRead, parse_max: usize) -> Result<Vec
     Ok(out)
 }
 
-fn parse_assignment<'a>(tokens: &'a [&'a str]) -> (u64, &'a str, Value, Option<Value>) {
+fn parse_assignment<'a>(tokens: &'a [&'a str]) -> (u64, &'a str, ScalarValue, Option<ScalarValue>) {
     let is_array = match tokens.len() {
         3 => false, // its a bit vector
         4 => true,
@@ -148,10 +148,10 @@ fn parse_assignment<'a>(tokens: &'a [&'a str]) -> (u64, &'a str, Value, Option<V
     let (value, array_index) = if is_array {
         let index_str = tokens[1];
         assert!(index_str.starts_with("[") && index_str.ends_with("]"));
-        let array_index = Value::from_bit_string(&index_str[1..index_str.len() - 1]);
-        (Value::from_bit_string(tokens[2]), Some(array_index))
+        let array_index = ScalarValue::from_bit_string(&index_str[1..index_str.len() - 1]);
+        (ScalarValue::from_bit_string(tokens[2]), Some(array_index))
     } else {
-        (Value::from_bit_string(tokens[1]), None)
+        (ScalarValue::from_bit_string(tokens[1]), None)
     };
     (index, name, value, array_index)
 }

src/mc/smt.rs

@@ -7,7 +7,7 @@ use crate::ir::{Expr, ExprRef, GetNode, SignalInfo, SignalKind, Type, TypeCheck}
 use std::borrow::Cow;
 
 use crate::ir::SignalKind::Input;
-use crate::sim::{Value, ValueStore, Witness};
+use crate::sim::{ScalarValue, ValueStore, Witness};
 use easy_smt as smt;
 
 #[derive(Debug, Clone, Copy)]
@@ -173,7 +173,7 @@ impl SmtModelChecker {
     }
 }
 
-fn get_smt_value(smt_ctx: &mut smt::Context, expr: smt::SExpr) -> Result<Value> {
+fn get_smt_value(smt_ctx: &mut smt::Context, expr: smt::SExpr) -> Result<ScalarValue> {
     let smt_value = smt_ctx.get_value(vec![expr])?[0].1;
     let atom = smt_ctx.get(smt_value);
     match atom {
@@ -190,17 +190,17 @@ fn get_smt_value(smt_ctx: &mut smt::Context, expr: smt::SExpr) -> Result<Value>
     }
 }
 
-fn smt_bit_vec_str_to_value(a: &str) -> Value {
+fn smt_bit_vec_str_to_value(a: &str) -> ScalarValue {
     if let Some(suffix) = a.strip_prefix("#b") {
-        Value::from_bit_string(suffix)
+        ScalarValue::from_bit_string(suffix)
     } else if let Some(suffix) = a.strip_prefix("#x") {
-        Value::from_hex_string(suffix)
+        ScalarValue::from_hex_string(suffix)
     } else if a == "true" {
-        Value::Long(1)
+        ScalarValue::Long(1)
     } else if a == "false" {
-        Value::Long(0)
+        ScalarValue::Long(0)
     } else {
-        Value::from_decimal_string(a)
+        ScalarValue::from_decimal_string(a)
     }
 }
 

src/sim/interpreter.rs

@@ -3,7 +3,7 @@
 // author: Kevin Laeufer <[email protected]>
 
 use crate::ir::*;
-use crate::sim::{Value, ValueStore};
+use crate::sim::{ScalarValue, ValueStore};
 
 /// Specifies how to initialize states that do not have
 #[derive(Debug, PartialEq, Copy, Clone)]
@@ -20,7 +20,7 @@ pub trait Simulator {
     fn step(&mut self);
 
     /// Change the value of an input
-    fn set_input(&mut self, input_id: usize, value: Value);
+    fn set_input(&mut self, input_id: usize, value: ScalarValue);
 }
 
 /// Interpreter based simulator for a transition system.
@@ -66,7 +66,7 @@ impl<'a> Simulator for Interpreter<'a> {
         todo!()
     }
 
-    fn set_input(&mut self, input_id: usize, value: Value) {
+    fn set_input(&mut self, input_id: usize, value: ScalarValue) {
         todo!()
     }
 }

src/sim/mod.rs

@@ -7,4 +7,4 @@ mod values;
 // author: Kevin Laeufer <[email protected]>
 pub mod interpreter;
 
-pub use values::{Value, ValueRef, ValueStore, Witness};
+pub use values::{ScalarValue, ScalarValueRef, ValueStore, Witness};

src/sim/values.rs

@@ -4,7 +4,8 @@
 
 use crate::ir::{Type, WidthInt};
 use num_bigint::BigUint;
-use num_traits::{Num, Zero};
+use num_traits::{Num, ToPrimitive, Zero};
+use std::fmt::Debug;
 
 /// Contains the initial state and the inputs over `len` cycles.
 #[derive(Debug, Default)]
@@ -98,40 +99,40 @@ impl ValueStore {
         state
     }
 
-    pub fn get(&self, index: usize) -> Option<ValueRef> {
+    pub fn get(&self, index: usize) -> Option<ScalarValueRef> {
         let meta = self.meta.get(index)?.as_ref()?;
         self.get_from_meta(meta)
     }
 
-    fn get_from_meta(&self, meta: &StorageMetaData) -> Option<ValueRef> {
+    fn get_from_meta(&self, meta: &StorageMetaData) -> Option<ScalarValueRef> {
         if !meta.is_valid {
             return None;
         }
-        let res: ValueRef = match meta.tpe {
-            StorageType::Long => ValueRef::Long(self.longs[meta.index as usize]),
-            StorageType::Big => ValueRef::Big(&self.bigs[meta.index as usize]),
+        let res: ScalarValueRef = match meta.tpe {
+            StorageType::Long => ScalarValueRef::Long(self.longs[meta.index as usize]),
+            StorageType::Big => ScalarValueRef::Big(&self.bigs[meta.index as usize]),
         };
         Some(res)
     }
 
-    pub fn update(&mut self, index: usize, value: Value) {
+    pub fn update(&mut self, index: usize, value: ScalarValue) {
         let meta = self.meta.get_mut(index).unwrap().as_mut().unwrap();
         meta.is_valid = true;
         match (meta.tpe, value) {
-            (StorageType::Long, Value::Long(value)) => {
+            (StorageType::Long, ScalarValue::Long(value)) => {
                 self.longs[meta.index as usize] = value;
             }
-            (StorageType::Big, Value::Big(value)) => {
+            (StorageType::Big, ScalarValue::Big(value)) => {
                 self.bigs[meta.index as usize] = value;
             }
-            (StorageType::Big, Value::Long(value)) => {
+            (StorageType::Big, ScalarValue::Long(value)) => {
                 self.bigs[meta.index as usize] = BigUint::from(value);
             }
             _ => panic!("Incompatible value for storage type: {:?}", meta.tpe),
         };
     }
 
-    pub fn insert(&mut self, index: usize, value: Value) {
+    pub fn insert(&mut self, index: usize, value: ScalarValue) {
         match self.meta.get(index) {
             Some(_) => self.update(index, value),
             None => {
@@ -143,13 +144,13 @@ impl ValueStore {
         };
     }
 
-    fn allocate_for_value(&mut self, value: Value) -> StorageMetaData {
+    fn allocate_for_value(&mut self, value: ScalarValue) -> StorageMetaData {
         let (tpe, index) = match value {
-            Value::Long(val) => {
+            ScalarValue::Long(val) => {
                 self.longs.push(val);
                 (StorageType::Long, self.longs.len() - 1)
             }
-            Value::Big(val) => {
+            ScalarValue::Big(val) => {
                 self.bigs.push(val);
                 (StorageType::Big, self.bigs.len() - 1)
             }
@@ -183,7 +184,7 @@ impl<'a> ValueStoreIter<'a> {
 }
 
 impl<'a> Iterator for ValueStoreIter<'a> {
-    type Item = Option<ValueRef<'a>>;
+    type Item = Option<ScalarValueRef<'a>>;
 
     fn next(&mut self) -> Option<Self::Item> {
         match self.underlying.next() {
@@ -194,49 +195,49 @@ impl<'a> Iterator for ValueStoreIter<'a> {
     }
 }
 
-#[derive(Debug, PartialEq, Clone)]
-pub enum Value {
+#[derive(Debug)]
+pub enum ScalarValue {
     Long(u64),
     Big(BigUint),
 }
 
-impl Value {
+impl ScalarValue {
     /// parses a string of 1s and 0s into a value.
     pub fn from_bit_string(value: &str) -> Self {
         if value.len() <= 64 {
-            Value::Long(u64::from_str_radix(value, 2).unwrap())
+            ScalarValue::Long(u64::from_str_radix(value, 2).unwrap())
         } else {
-            Value::Big(BigUint::from_str_radix(value, 2).unwrap())
+            ScalarValue::Big(BigUint::from_str_radix(value, 2).unwrap())
         }
     }
 
     pub fn from_hex_string(value: &str) -> Self {
         if value.len() <= (64 / 4) {
-            Value::Long(u64::from_str_radix(value, 16).unwrap())
+            ScalarValue::Long(u64::from_str_radix(value, 16).unwrap())
         } else {
-            Value::Big(BigUint::from_str_radix(value, 16).unwrap())
+            ScalarValue::Big(BigUint::from_str_radix(value, 16).unwrap())
         }
     }
 
     pub fn from_decimal_string(value: &str) -> Self {
         match u64::from_str_radix(value, 10) {
-            Ok(value) => Value::Long(value),
-            Err(_) => Value::Big(BigUint::from_str_radix(value, 10).unwrap()),
+            Ok(value) => ScalarValue::Long(value),
+            Err(_) => ScalarValue::Big(BigUint::from_str_radix(value, 10).unwrap()),
         }
     }
 
     pub fn is_zero(&self) -> bool {
         match &self {
-            Value::Long(value) => *value == 0,
-            Value::Big(value) => value.is_zero(),
+            ScalarValue::Long(value) => *value == 0,
+            ScalarValue::Big(value) => value.is_zero(),
         }
     }
 
     /// Returns the value as a fixed with bit string. Returns None if the value is an array.
     pub fn to_bit_string(&self, width: WidthInt) -> Option<String> {
         let base_str = match &self {
-            Value::Long(value) => format!("{value:b}"),
-            Value::Big(value) => value.to_str_radix(2),
+            ScalarValue::Long(value) => format!("{value:b}"),
+            ScalarValue::Big(value) => value.to_str_radix(2),
         };
         let base_len = base_str.len();
         if base_len == width as usize {
@@ -253,23 +254,23 @@ impl Value {
 }
 
 #[derive(Debug, PartialEq)]
-pub enum ValueRef<'a> {
+pub enum ScalarValueRef<'a> {
     Long(u64),
     Big(&'a BigUint),
 }
 
-impl<'a> ValueRef<'a> {
-    pub fn cloned(&self) -> Value {
+impl<'a> ScalarValueRef<'a> {
+    pub fn cloned(&self) -> ScalarValue {
         match self {
-            ValueRef::Long(value) => Value::Long(*value),
-            ValueRef::Big(value) => Value::Big((*value).clone()),
+            ScalarValueRef::Long(value) => ScalarValue::Long(*value),
+            ScalarValueRef::Big(value) => ScalarValue::Big((*value).clone()),
         }
     }
 
     pub fn is_zero(&self) -> bool {
         match self {
-            ValueRef::Long(value) => *value == 0,
-            ValueRef::Big(value) => value.is_zero(),
+            ScalarValueRef::Long(value) => *value == 0,
+            ScalarValueRef::Big(value) => value.is_zero(),
         }
     }
 
@@ -279,6 +280,97 @@ impl<'a> ValueRef<'a> {
     }
 }
 
+pub trait TryFromValue: Sized {
+    // TODO: investigate using std::convert::TryFrom<Value> instead!
+    fn try_from(value: ScalarValue) -> Option<Self>;
+}
+
+impl TryFromValue for u64 {
+    fn try_from(value: ScalarValue) -> Option<Self> {
+        match value {
+            ScalarValue::Long(v) => Some(v),
+            ScalarValue::Big(v) => v.to_u64(),
+        }
+    }
+}
+
+impl TryFromValue for BigUint {
+    fn try_from(value: ScalarValue) -> Option<Self> {
+        match value {
+            ScalarValue::Long(v) => Some(BigUint::from(v)),
+            ScalarValue::Big(v) => Some(v),
+        }
+    }
+}
+
+pub trait IntoValueRef: Sized {
+    // TODO: investigate using std::convert::Into<ValueRef> instead!
+    fn into(&self) -> ScalarValueRef<'_>;
+}
+
+impl IntoValueRef for u64 {
+    fn into(&self) -> ScalarValueRef<'_> {
+        ScalarValueRef::Long(*self)
+    }
+}
+
+impl IntoValueRef for BigUint {
+    fn into(&self) -> ScalarValueRef<'_> {
+        ScalarValueRef::Big(self)
+    }
+}
+
+pub trait ArrayValue: Debug {
+    fn update(&mut self, index: ScalarValue, value: ScalarValue);
+    fn get(&self, index: ScalarValue) -> ScalarValueRef;
+}
+
+#[derive(Debug, PartialEq)]
+pub struct SparseArrayValue<I, D>
+where
+    I: PartialEq + TryFromValue + Debug,
+    D: TryFromValue + IntoValueRef + Debug,
+{
+    default: D,
+    updates: Vec<(I, D)>,
+}
+
+impl<I, D> SparseArrayValue<I, D>
+where
+    I: PartialEq + TryFromValue + Debug,
+    D: TryFromValue + IntoValueRef + Debug,
+{
+    fn new(default: D) -> Self {
+        Self {
+            default,
+            updates: Vec::new(),
+        }
+    }
+}
+
+impl<I, D> ArrayValue for SparseArrayValue<I, D>
+where
+    I: PartialEq + TryFromValue + Debug,
+    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()));
+    }
+
+    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()
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -289,7 +381,7 @@ mod tests {
         assert_eq!(std::mem::size_of::<BigUint>(), 24);
 
         // Not sure how we are fitting that, but it's nice that Value is no bigger than a BigUInt
-        assert_eq!(std::mem::size_of::<Value>(), 24);
+        assert_eq!(std::mem::size_of::<ScalarValue>(), 24);
 
         // We store 4 bytes of meta-data for every item in the storage
         assert_eq!(std::mem::size_of::<StorageMetaData>(), 4);