Add with_exprt to smt conversion for array updates

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -991,10 +991,29 @@ static smt_termt convert_expr_to_smt(
     "Generation of SMT formula for shift expression: " + shift.pretty());
 }
 
+static smt_termt convert_array_update_to_smt(
+  const exprt &old,
+  const exprt &index,
+  const exprt &new_value,
+  const sub_expression_mapt &converted)
+{
+  const smt_termt &old_array_term = converted.at(old);
+  const smt_termt &index_term = converted.at(index);
+  const smt_termt &value_term = converted.at(new_value);
+  return smt_array_theoryt::store(old_array_term, index_term, value_term);
+}
+
 static smt_termt convert_expr_to_smt(
   const with_exprt &with,
   const sub_expression_mapt &converted)
 {
+  if(const auto array_type = type_try_dynamic_cast<array_typet>(with.type()))
+  {
+    return convert_array_update_to_smt(
+      with.old(), with.where(), with.new_value(), converted);
+  }
+  // 'with' expression is also used to update struct fields, but for now we do
+  // not support them, so we fail.
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for with expression: " + with.pretty());
 }

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1161,6 +1161,32 @@ TEST_CASE(
   CHECK(test.convert(index_expr) == expected);
 }
 
+TEST_CASE(
+  "expr to smt conversion for with_exprt expressions",
+  "[core][smt2_incremental]")
+{
+  auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+  SECTION("Array types")
+  {
+    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 exprt value = from_integer(12, value_type);
+    const with_exprt with{array, index, value};
+    INFO("Expression being converted: " + with.pretty(2, 0));
+    const smt_termt expected = smt_array_theoryt::store(
+      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},
+      smt_bit_vector_constant_termt{12, 8});
+    CHECK(test.convert(with) == expected);
+  }
+}
+
 TEST_CASE(
   "expr to smt conversion for extract bits expressions",
   "[core][smt2_incremental]")