Add an Array sort in the new SMT backend

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -213,6 +213,13 @@ struct sort_based_cast_to_bit_vector_convertert final
         "Generation of SMT formula for type cast to bit vector from type: " +
         from_type.pretty());
   }
+
+  void visit(const smt_array_sortt &) override
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for type cast to bit vector from type: " +
+      from_type.pretty());
+  }
 };
 
 static smt_termt convert_bit_vector_cast(
@@ -294,6 +301,12 @@ struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort
     const auto value = bvrep2integer(member_input.get_value(), width, false);
     result = smt_bit_vector_constant_termt{value, bit_vector_sort};
   }
+
+  void visit(const smt_array_sortt &array_sort) override
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Conversion of array SMT literal " + array_sort.pretty());
+  }
 };
 
 static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)

src/solvers/smt2_incremental/smt_sorts.cpp

@@ -62,6 +62,25 @@ std::size_t smt_bit_vector_sortt::bit_width() const
   return get_size_t(ID_width);
 }
 
+smt_array_sortt::smt_array_sortt(
+  const smt_sortt &index_sort,
+  const smt_sortt &element_sort)
+  : smt_sortt{ID_smt_array_sort}
+{
+  add(ID_index, index_sort);
+  add(ID_value, element_sort);
+}
+
+const smt_sortt &smt_array_sortt::index_sort() const
+{
+  return static_cast<const smt_sortt &>(find(ID_index));
+}
+
+const smt_sortt &smt_array_sortt::element_sort() const
+{
+  return static_cast<const smt_sortt &>(find(ID_value));
+}
+
 template <typename visitort>
 void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
 {

src/solvers/smt2_incremental/smt_sorts.def

@@ -8,3 +8,4 @@
 ///  * The type of sort checks required to implement `smt_sortt::accept`.
 SORT_ID(bool)
 SORT_ID(bit_vector)
+SORT_ID(array)

src/solvers/smt2_incremental/smt_sorts.h

@@ -87,6 +87,16 @@ class smt_bit_vector_sortt final : public smt_sortt
   std::size_t bit_width() const;
 };
 
+class smt_array_sortt final : public smt_sortt
+{
+public:
+  explicit smt_array_sortt(
+    const smt_sortt &index_sort,
+    const smt_sortt &element_sort);
+  const smt_sortt &index_sort() const;
+  const smt_sortt &element_sort() const;
+};
+
 class smt_sort_const_downcast_visitort
 {
 public:

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -76,6 +76,11 @@ class smt_sort_output_visitort : public smt_sort_const_downcast_visitort
   {
     os << "(_ BitVec " << bit_vec.bit_width() << ")";
   }
+
+  void visit(const smt_array_sortt &array) override
+  {
+    os << "(Array " << array.index_sort() << " " << array.element_sort() << ")";
+  }
 };
 
 std::ostream &operator<<(std::ostream &os, const smt_sortt &sort)

unit/solvers/smt2_incremental/smt_sorts.cpp

@@ -32,6 +32,7 @@ TEST_CASE("Visiting smt_bool_sortt.", "[core][smt2_incremental]")
   public:
     bool bool_visited = false;
     bool bit_vec_visited = false;
+    bool array_visited = false;
 
     void visit(const smt_bool_sortt &) override
     {
@@ -42,10 +43,16 @@ TEST_CASE("Visiting smt_bool_sortt.", "[core][smt2_incremental]")
     {
       bit_vec_visited = true;
     }
+
+    void visit(const smt_array_sortt &) override
+    {
+      array_visited = true;
+    }
   } visitor;
   smt_bool_sortt{}.accept(visitor);
   REQUIRE(visitor.bool_visited);
   REQUIRE_FALSE(visitor.bit_vec_visited);
+  REQUIRE_FALSE(visitor.array_visited);
 }
 
 TEST_CASE("Visiting smt_bit_vec_sortt.", "[core][smt2_incremental]")
@@ -55,6 +62,7 @@ TEST_CASE("Visiting smt_bit_vec_sortt.", "[core][smt2_incremental]")
   public:
     bool bool_visited = false;
     bool bit_vec_visited = false;
+    bool array_visited = false;
 
     void visit(const smt_bool_sortt &) override
     {
@@ -66,10 +74,53 @@ TEST_CASE("Visiting smt_bit_vec_sortt.", "[core][smt2_incremental]")
       bit_vec_visited = true;
       REQUIRE(bit_vec.bit_width() == 8);
     }
+
+    void visit(const smt_array_sortt &) override
+    {
+      array_visited = true;
+    }
   } visitor;
   smt_bit_vector_sortt{8}.accept(visitor);
   REQUIRE_FALSE(visitor.bool_visited);
   REQUIRE(visitor.bit_vec_visited);
+  REQUIRE_FALSE(visitor.array_visited);
+}
+
+TEST_CASE("Visiting smt_array_sort.", "[core][smt2_incremental]")
+{
+  class : public smt_sort_const_downcast_visitort
+  {
+  public:
+    bool bool_visited = false;
+    bool bit_vec_visited = false;
+    bool array_visited = false;
+
+    void visit(const smt_bool_sortt &) override
+    {
+      bool_visited = true;
+    }
+
+    void visit(const smt_bit_vector_sortt &bit_vec) override
+    {
+      bit_vec_visited = true;
+    }
+
+    void visit(const smt_array_sortt &) override
+    {
+      array_visited = true;
+    }
+  } visitor, visitor_second;
+
+  smt_array_sortt{smt_bool_sortt{}, smt_bool_sortt{}}.accept(visitor);
+  REQUIRE_FALSE(visitor.bool_visited);
+  REQUIRE_FALSE(visitor.bit_vec_visited);
+  REQUIRE(visitor.array_visited);
+
+  smt_array_sortt{smt_bit_vector_sortt{64}, smt_bit_vector_sortt{32}}.accept(
+    visitor_second);
+  REQUIRE_FALSE(visitor_second.bool_visited);
+  REQUIRE_FALSE(visitor_second.bit_vec_visited);
+  REQUIRE(visitor_second.array_visited);
 }
 
 TEST_CASE("smt_sortt equality", "[core][smt2_incremental]")
@@ -83,4 +134,36 @@ TEST_CASE("smt_sortt equality", "[core][smt2_incremental]")
   CHECK(bit_vector8 != bool_sort1);
   const smt_bit_vector_sortt bit_vector16{16};
   CHECK(bit_vector8 != bit_vector16);
+  const smt_array_sortt array_sort{smt_bool_sortt{}, smt_bool_sortt{}};
+  CHECK(array_sort != bool_sort1);
+  CHECK(array_sort != bit_vector8);
+  const smt_array_sortt array_sort2{smt_bool_sortt{}, smt_bool_sortt{}};
+  CHECK(array_sort == array_sort2);
+  const smt_array_sortt array_sort_bv{bit_vector16, bit_vector16};
+  CHECK(array_sort_bv != array_sort);
+  const smt_array_sortt array_sort_bv2{bit_vector16, bit_vector16};
+  CHECK(array_sort_bv2 == array_sort_bv);
+}
+
+TEST_CASE(
+  "Test smt_array_sort get_index_sort getter.",
+  "[core][smt2_incremental]")
+{
+  const smt_array_sortt array_sort{smt_bool_sortt{}, smt_bool_sortt{}};
+  REQUIRE(smt_bool_sortt{} == array_sort.index_sort());
+
+  const smt_array_sortt array_sort2{smt_bit_vector_sortt{16}, smt_bool_sortt{}};
+  REQUIRE(smt_bit_vector_sortt{16} == array_sort2.index_sort());
+}
+
+TEST_CASE(
+  "Test smt_array_sort get_element_sort getter.",
+  "[core][smt2_incremental]")
+{
+  const smt_array_sortt array_sort{smt_bool_sortt{}, smt_bool_sortt{}};
+  REQUIRE(smt_bool_sortt{} == array_sort.element_sort());
+
+  const smt_array_sortt array_sort2{
+    smt_bit_vector_sortt{16}, smt_bit_vector_sortt{64}};
+  REQUIRE(smt_bit_vector_sortt{64} == array_sort2.element_sort());
 }

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -21,6 +21,18 @@ TEST_CASE("Test smt_sortt to string conversion", "[core][smt2_incremental]")
 {
   CHECK(smt_to_smt2_string(smt_bool_sortt{}) == "Bool");
   CHECK(smt_to_smt2_string(smt_bit_vector_sortt{16}) == "(_ BitVec 16)");
+  CHECK(
+    smt_to_smt2_string(smt_array_sortt{smt_bool_sortt{}, smt_bool_sortt{}}) ==
+    "(Array Bool Bool)");
+  CHECK(
+    smt_to_smt2_string(
+      smt_array_sortt(smt_bit_vector_sortt{64}, smt_bit_vector_sortt{16})) ==
+    "(Array (_ BitVec 64) (_ BitVec 16))");
+  CHECK(
+    smt_to_smt2_string(smt_array_sortt(
+      smt_bit_vector_sortt{64},
+      smt_array_sortt(smt_bool_sortt{}, smt_bit_vector_sortt{16}))) ==
+    "(Array (_ BitVec 64) (Array Bool (_ BitVec 16)))");
 }
 
 TEST_CASE(