add some array support

src/btor2/parse.rs

@@ -125,7 +125,7 @@ impl<'a> Parser<'a> {
         } else {
             self.require_at_least_n_tokens(line, tokens, 3)?;
             match op {
-                "ite" => {
+                "ite" | "write" => {
                     // ternary ops
                     Some(self.parse_ternary_op(line, tokens)?)
                 }
@@ -335,6 +335,7 @@ impl<'a> Parser<'a> {
                 self.check_expr_type(inner, line, tpe)?;
                 self.ctx.not(inner)
             }
+            "read" => self.ctx.array_read(a, b),
             other => panic!("unexpected binary op: {other}"),
         };
         self.check_expr_type(e, line, tpe)
@@ -354,6 +355,7 @@ impl<'a> Parser<'a> {
                     todo!("Array ITE")
                 }
             }
+            "write" => self.ctx.array_store(a, b, c),
             other => panic!("unexpected binary op: {other}"),
         };
         self.check_expr_type(res, line, tpe)
@@ -574,8 +576,10 @@ impl<'a> Parser<'a> {
             }
             "array" => {
                 self.require_at_least_n_tokens(line, tokens, 5)?;
-                let index_width = self.parse_width_int(line, tokens[3], "array index width")?;
-                let data_width = self.parse_width_int(line, tokens[4], "array data width")?;
+                let index_tpe = self.get_tpe_from_id(line, tokens[3])?;
+                let data_tpe = self.get_tpe_from_id(line, tokens[4])?;
+                let index_width = index_tpe.get_bit_vector_width().unwrap();
+                let data_width = data_tpe.get_bit_vector_width().unwrap();
                 self.type_map.insert(
                     line_id,
                     Type::Array(ArrayType {
@@ -776,11 +780,11 @@ fn str_offset(needle: &str, haystack: &str) -> usize {
 const UNARY_OPS: [&str; 10] = [
     "not", "inc", "dec", "neg", "redand", "redor", "redxor", "slice", "uext", "sext",
 ];
-const BINARY_OPS: [&str; 40] = [
+const BINARY_OPS: [&str; 41] = [
     "iff", "implies", "sgt", "ugt", "sgte", "ugte", "slt", "ult", "slte", "ulte", "and", "nand",
     "nor", "or", "xnor", "xor", "rol", "ror", "sll", "sra", "srl", "add", "mul", "sdiv", "udiv",
     "smod", "srem", "urem", "sub", "saddo", "uaddo", "sdivo", "udivo", "smulo", "umulo", "ssubo",
-    "usubo", "concat", "eq", "neq",
+    "usubo", "concat", "eq", "neq", "read",
 ];
 const TERNARY_OPS: [&str; 1] = ["ite"];
 const OTHER_OPS: [&str; 17] = [

src/ir/expr.rs

@@ -136,6 +136,19 @@ pub trait ExprNodeConstruction:
         let width = e.get_bv_type(self).unwrap() + by;
         self.add_node(Expr::BVSignExt { e, by, width })
     }
+
+    fn array_store(&mut self, array: ExprRef, index: ExprRef, data: ExprRef) -> ExprRef {
+        self.add_node(Expr::ArrayStore { array, index, data })
+    }
+
+    fn array_read(&mut self, array: ExprRef, index: ExprRef) -> ExprRef {
+        let width = array.get_type(self).get_array_data_width().unwrap();
+        self.add_node(Expr::BVArrayRead {
+            array,
+            index,
+            width,
+        })
+    }
 }
 
 pub fn bv_value_fits_width(value: BVLiteralInt, width: WidthInt) -> bool {
@@ -440,6 +453,20 @@ impl Type {
             Type::Array(_) => None,
         }
     }
+
+    pub fn get_array_data_width(&self) -> Option<WidthInt> {
+        match &self {
+            Type::BV(_) => None,
+            Type::Array(a) => Some(a.data_width),
+        }
+    }
+
+    pub fn get_array_index_width(&self) -> Option<WidthInt> {
+        match &self {
+            Type::BV(_) => None,
+            Type::Array(a) => Some(a.index_width),
+        }
+    }
 }
 
 impl std::fmt::Display for Type {

src/ir/serialize.rs

@@ -4,8 +4,7 @@
 
 use super::{Context, Expr, ExprRef, GetNode};
 use crate::ir::{
-    count_expr_uses, is_usage_root_signal, SignalInfo, SignalKind, TransitionSystem, Type,
-    TypeCheck,
+    count_expr_uses, is_usage_root_signal, SignalKind, TransitionSystem, Type, TypeCheck,
 };
 use std::io::Write;
 
@@ -441,7 +440,7 @@ impl SerializableIrNode for Type {
     }
 }
 
-fn inline_expr_for_transition_system(expr: &Expr, use_count: u32) -> bool {
+fn inline_expr_for_transition_system(expr: &Expr, _use_count: u32) -> bool {
     let always_inline = expr.is_symbol() || expr.is_bv_lit();
     // TODO: re-enable using the use_count for inlining decisions after we add a way to turn it off
     always_inline // || use_count <= 1

src/ir/type_check.rs

@@ -36,8 +36,8 @@ impl Type {
     }
     fn expect_array(&self, op: &str) -> Result<ArrayType, TypeCheckError> {
         match self {
-            Type::BV(_) => Err(TypeCheckError {
-                msg: format!("{op} only works on arrays, not bit-vectors."),
+            Type::BV(w) => Err(TypeCheckError {
+                msg: format!("{op} needs to be an array, not a bv<{w}>."),
             }),
             Type::Array(tpe) => Ok(*tpe),
         }
@@ -215,7 +215,9 @@ impl TypeCheck for Expr {
                 index,
                 width,
             } => {
-                let array_tpe = array.get_type(ctx).expect_array("array read")?;
+                let array_tpe = array
+                    .get_type(ctx)
+                    .expect_array("the first argument to the read operation")?;
                 let index_width = index.get_type(ctx).expect_bv("array read index")?;
                 if array_tpe.index_width != index_width {
                     Err(TypeCheckError {
@@ -259,11 +261,13 @@ impl TypeCheck for Expr {
                 }))
             }
             Expr::ArrayEqual(a, b) => {
-                expect_same_size_arrays(ctx, "array equals", a, b)?;
+                expect_same_size_arrays(ctx, "the array equals operation", a, b)?;
                 Ok(Type::BV(1))
             }
             Expr::ArrayStore { array, index, data } => {
-                let tpe = array.get_type(ctx).expect_array("array store")?;
+                let tpe = array
+                    .get_type(ctx)
+                    .expect_array("the first argument to the store operation")?;
                 index
                     .get_type(ctx)
                     .expect_bv_of(tpe.index_width, "array store index")?;
@@ -273,7 +277,7 @@ impl TypeCheck for Expr {
             }
             Expr::ArrayIte { cond, tru, fals } => {
                 cond.get_type(ctx).expect_bv_of(1, "ite condition")?;
-                expect_same_size_arrays(ctx, "ite branches", tru, fals)
+                expect_same_size_arrays(ctx, "both ite branches", tru, fals)
             }
         }
     }

src/mc/smt.rs

@@ -361,7 +361,11 @@ where
         Expr::BVReduceOr(_) => todo!(),
         Expr::BVReduceAnd(_) => todo!(),
         Expr::BVReduceXor(_) => todo!(),
-        Expr::BVEqual(_, _) => todo!(),
+        Expr::BVEqual(a_ref, b_ref) => {
+            let a = convert_expr(smt_ctx, ctx, *a_ref, rename_sym);
+            let b = convert_expr(smt_ctx, ctx, *b_ref, rename_sym);
+            smt_ctx.eq(a, b)
+        }
         Expr::BVImplies(a_ref, b_ref) => {
             let a = convert_expr(smt_ctx, ctx, *a_ref, rename_sym);
             let b = convert_expr(smt_ctx, ctx, *b_ref, rename_sym);
@@ -398,7 +402,11 @@ where
         Expr::BVSignedRem(_, _, _) => todo!(),
         Expr::BVUnsignedRem(_, _, _) => todo!(),
         Expr::BVSub(_, _, _) => todo!(),
-        Expr::BVArrayRead { .. } => todo!(),
+        Expr::BVArrayRead { array, index, .. } => {
+            let a = convert_expr(smt_ctx, ctx, *array, rename_sym);
+            let i = convert_expr(smt_ctx, ctx, *index, rename_sym);
+            smt_ctx.select(a, i)
+        }
         Expr::BVIte { cond, tru, fals } => {
             let c = convert_expr(smt_ctx, ctx, *cond, rename_sym);
             let t = convert_expr(smt_ctx, ctx, *tru, rename_sym);
@@ -411,7 +419,12 @@ where
         }
         Expr::ArrayConstant { .. } => todo!(),
         Expr::ArrayEqual(_, _) => todo!(),
-        Expr::ArrayStore { .. } => todo!(),
+        Expr::ArrayStore { array, index, data } => {
+            let a = convert_expr(smt_ctx, ctx, *array, rename_sym);
+            let i = convert_expr(smt_ctx, ctx, *index, rename_sym);
+            let d = convert_expr(smt_ctx, ctx, *data, rename_sym);
+            smt_ctx.store(a, i, d)
+        }
         Expr::ArrayIte { .. } => todo!(),
     }
 }

src/sim/interpreter.rs

@@ -3,30 +3,70 @@
 // author: Kevin Laeufer <[email protected]>
 
 use crate::ir::*;
-use crate::sim::ValueStore;
+use crate::sim::{Value, ValueStore};
+
+/// Specifies how to initialize states that do not have
+#[derive(Debug, PartialEq, Copy, Clone)]
+pub enum InitKind {
+    Zero,
+    Random,
+}
 
 pub trait Simulator {
+    /// Load the initial state values.
+    fn init(&mut self, kind: InitKind);
+
     /// Advance the state.
     fn step(&mut self);
+
+    /// Change the value of an input
+    fn set_input(&mut self, input_id: usize, value: Value);
 }
 
 /// Interpreter based simulator for a transition system.
 pub struct Interpreter<'a> {
     ctx: &'a Context,
     sys: &'a TransitionSystem,
     state: ValueStore,
+    meta: Vec<InterpreterMetaData>,
+}
+
+/// Meta data for each expression.
+#[derive(Debug, Clone, Copy)]
+struct InterpreterMetaData {}
+
+impl Default for InterpreterMetaData {
+    fn default() -> Self {
+        Self {}
+    }
 }
 
 impl<'a> Interpreter<'a> {
     pub fn new(ctx: &'a Context, sys: &'a TransitionSystem) -> Self {
+        let use_counts = count_expr_uses(ctx, sys);
         let types = sys.states().map(|s| s.symbol.get_type(ctx));
         let state = ValueStore::new(types);
-        Self { ctx, sys, state }
+        let mut meta = Vec::with_capacity(use_counts.len());
+        meta.resize(use_counts.len(), InterpreterMetaData::default());
+        Self {
+            ctx,
+            sys,
+            state,
+            meta,
+        }
     }
 }
 
 impl<'a> Simulator for Interpreter<'a> {
+    fn init(&mut self, kind: InitKind) {
+        todo!()
+    }
+
     fn step(&mut self) {
         todo!()
     }
+
+    fn set_input(&mut self, input_id: usize, value: Value) {
+        todo!()
+    }
 }