Add index_exprt to smt conversion for array reads

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -18,6 +18,7 @@
 
 #include <solvers/prop/literal_expr.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
+#include <solvers/smt2_incremental/smt_array_theory.h>
 #include <solvers/smt2_incremental/smt_bit_vector_theory.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
 
@@ -917,11 +918,12 @@ static smt_termt convert_expr_to_smt(
 }
 
 static smt_termt convert_expr_to_smt(
-  const index_exprt &index,
+  const index_exprt &index_of,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for index expression: " + index.pretty());
+  const smt_termt &array = converted.at(index_of.array());
+  const smt_termt &index = converted.at(index_of.index());
+  return smt_array_theoryt::select(array, index);
 }
 
 template <typename factoryt, typename shiftt>

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -14,6 +14,7 @@
 
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/smt_array_theory.h>
 #include <solvers/smt2_incremental/smt_bit_vector_theory.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_terms.h>
@@ -1140,6 +1141,26 @@ TEST_CASE(
   }
 }
 
+TEST_CASE(
+  "expr to smt conversion for index_exprt expressions",
+  "[core][smt2_incremental]")
+{
+  auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+  const typet value_type = signedbv_typet{8};
+  const exprt array = symbol_exprt{
+    "my_array", array_typet{value_type, from_integer(10, signed_size_type())}};
+  const exprt index = from_integer(42, unsignedbv_typet{64});
+  const index_exprt index_expr{array, index};
+  INFO("Expression being converted: " + index_expr.pretty(2, 0));
+  const smt_termt expected = smt_array_theoryt::select(
+    smt_identifier_termt{
+      "my_array",
+      smt_array_sortt{smt_bit_vector_sortt{64}, smt_bit_vector_sortt{8}}},
+    smt_bit_vector_constant_termt{42, 64});
+  CHECK(test.convert(index_expr) == expected);
+}
+
 TEST_CASE(
   "expr to smt conversion for extract bits expressions",
   "[core][smt2_incremental]")