expr: replace get_str with [...]

src/expr/context.rs

@@ -105,12 +105,6 @@ impl Context {
         ExprRef::from_index(index)
     }
 
-    pub(crate) fn get_str(&self, reference: StringRef) -> &str {
-        self.strings
-            .get_index((reference.0.get() as usize) - 1)
-            .expect("Invalid StringRef!")
-    }
-
     pub(crate) fn string(&mut self, value: std::borrow::Cow<str>) -> StringRef {
         if let Some(index) = self.strings.get_index_of(value.as_ref()) {
             StringRef::from_index(index)
@@ -135,6 +129,16 @@ impl Index<ExprRef> for Context {
     }
 }
 
+impl Index<StringRef> for Context {
+    type Output = String;
+
+    fn index(&self, index: StringRef) -> &Self::Output {
+        self.strings
+            .get_index(index.index())
+            .expect("Invalid StringRef!")
+    }
+}
+
 /// Convenience methods to construct IR nodes.
 impl Context {
     // helper functions to construct expressions

src/expr/eval.rs

@@ -257,10 +257,7 @@ fn eval_expr_internal(
             Expr::BVSymbol { name, width } => {
                 // we should not get here
                 // TODO: turn into return Err
-                panic!(
-                    "No value found for symbol: {} : bv<{width}>",
-                    ctx.get_str(*name)
-                );
+                panic!("No value found for symbol: {} : bv<{width}>", ctx[*name]);
             }
             Expr::BVLiteral(value) => bv_stack.push(value.get(ctx).into()),
             // unary
@@ -333,7 +330,7 @@ fn eval_expr_internal(
                 // TODO: turn into return Err
                 panic!(
                     "No value found for symbol: {} : bv<{index_width}> -> bv<{data_width}>",
-                    ctx.get_str(*name)
+                    ctx[*name]
                 );
             }
             Expr::ArrayConstant { index_width, .. } => {

src/expr/nodes.rs

@@ -164,7 +164,7 @@ impl Expr {
     }
 
     pub fn get_symbol_name<'a>(&self, ctx: &'a Context) -> Option<&'a str> {
-        self.get_symbol_name_ref().map(|r| ctx.get_str(r))
+        self.get_symbol_name_ref().map(|r| ctx[r].as_str())
     }
 
     pub fn is_true(&self) -> bool {

src/expr/serialize.rs

@@ -38,7 +38,7 @@ where
     W: Write,
 {
     match expr {
-        Expr::BVSymbol { name, .. } => write!(writer, "{}", ctx.get_str(*name)),
+        Expr::BVSymbol { name, .. } => write!(writer, "{}", ctx[*name]),
         Expr::BVLiteral(value) => {
             if value.width() <= 8 {
                 write!(writer, "{}'b{}", value.width(), value.get(ctx).to_bit_str())
@@ -342,7 +342,7 @@ where
             }
             write!(writer, ")")
         }
-        Expr::ArraySymbol { name, .. } => write!(writer, "{}", ctx.get_str(*name)),
+        Expr::ArraySymbol { name, .. } => write!(writer, "{}", ctx[*name]),
         Expr::ArrayConstant { e, index_width, .. } => {
             write!(writer, "([")?;
             if (serialize_child)(e, writer)? {

src/mc/smt.rs

@@ -405,7 +405,7 @@ impl UnrollSmtEncoding {
             let skip = !(filter)(info);
             if !skip {
                 let tpe = convert_tpe(smt_ctx, expr.get_type(ctx));
-                let name = name_at(ctx.get_str(info.name), step);
+                let name = name_at(&ctx[info.name], step);
                 if ctx[*expr].is_symbol() {
                     smt_ctx.declare_const(escape_smt_identifier(&name), tpe)?;
                 } else {
@@ -431,7 +431,7 @@ impl UnrollSmtEncoding {
             let name_ref = if info.is_const {
                 info.name
             } else {
-                let name = name_at(ctx.get_str(info.name), step);
+                let name = name_at(&ctx[info.name], step);
                 ctx.string(name.into())
             };
             let tpe = signal.get_type(ctx);

src/smt/serialize.rs

@@ -31,7 +31,7 @@ pub fn convert_expr(
 
     match &ctx[expr_ref] {
         Expr::BVSymbol { name, .. } => {
-            let name_str = ctx.get_str(*name);
+            let name_str = &ctx[*name];
             smt_ctx.atom(escape_smt_identifier(name_str))
         }
         Expr::BVLiteral(value) => {
@@ -220,7 +220,7 @@ pub fn convert_expr(
             let f = convert_expr(smt_ctx, ctx, *fals, patch_expr);
             smt_ctx.ite(c, t, f)
         }
-        Expr::ArraySymbol { name, .. } => smt_ctx.atom(escape_smt_identifier(ctx.get_str(*name))),
+        Expr::ArraySymbol { name, .. } => smt_ctx.atom(escape_smt_identifier(&ctx[*name])),
         Expr::ArrayConstant {
             e,
             index_width,

src/system/serialize.rs

@@ -32,7 +32,7 @@ fn serialize_transition_system<W: Write>(
             .map(|n| n.to_string())
             .unwrap_or_else(|| {
                 sys.names[root.expr]
-                    .map(|n| ctx.get_str(n).to_string())
+                    .map(|n| ctx[n].clone())
                     .unwrap_or(format!("%{}", root.expr.index()))
             });
         names[root.expr] = Some(name);