Add array type to sort conversion

This is sufficient for supporting the conversion of the generated
expressions for non-deterministically initialised arrays. However it is
not yet straight forward to regression test without support for the
conversion of further kinds of expression. This is because the
initialisation would be sliced away if the result of the initialisation
is not read back later on.

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -89,6 +89,13 @@ static smt_sortt convert_type_to_smt_sort(const bitvector_typet &type)
   return smt_bit_vector_sortt{type.get_width()};
 }
 
+static smt_sortt convert_type_to_smt_sort(const array_typet &type)
+{
+  return smt_array_sortt{
+    convert_type_to_smt_sort(type.index_type()),
+    convert_type_to_smt_sort(type.element_type())};
+}
+
 smt_sortt convert_type_to_smt_sort(const typet &type)
 {
   if(const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
@@ -99,6 +106,10 @@ smt_sortt convert_type_to_smt_sort(const typet &type)
   {
     return convert_type_to_smt_sort(*bitvector_type);
   }
+  if(const auto array_type = type_try_dynamic_cast<array_typet>(type))
+  {
+    return convert_type_to_smt_sort(*array_type);
+  }
   UNIMPLEMENTED_FEATURE("Generation of SMT formula for type: " + type.pretty());
 }
 

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -96,6 +96,20 @@ expr_to_smt_conversion_test_environmentt::convert(const exprt &expression) const
     object_size_function.make_application);
 }
 
+TEST_CASE("\"array_typet\" to smt sort conversion", "[core][smt2_incremental]")
+{
+  auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+
+  const auto array_type =
+    array_typet{signedbv_typet{8}, from_integer(8, c_index_type())};
+  INFO("Type being converted: " + array_type.pretty(2, 0));
+  const auto conversion_result = convert_type_to_smt_sort(array_type);
+  CHECK(
+    conversion_result ==
+    smt_array_sortt{smt_bit_vector_sortt{64}, smt_bit_vector_sortt{8}});
+}
+
 TEST_CASE("\"symbol_exprt\" to smt term conversion", "[core][smt2_incremental]")
 {
   auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386);