Add an Array sort in the new SMT backend, along with unit tests for the sort and its printing.

Co-authored-by: Fotis Koutoulakis <[email protected]>
Co-authored-by: Enrico Steffinlongo <[email protected]>

Author: NlightNFotis

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -89,6 +89,12 @@ 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)
+{
+  UNIMPLEMENTED_FEATURE(
+    "Conversion of array type to smt sort " + type.pretty());
+}
+
 smt_sortt convert_type_to_smt_sort(const typet &type)
 {
   if(const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
@@ -99,6 +105,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());
 }
 
@@ -213,6 +223,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 +311,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,29 @@ 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(index_sort_label, index_sort);
+  add(element_sort_label, element_sort);
+}
+
+const smt_sortt &smt_array_sortt::get_index_sort() const
+{
+  const irept &index_info = find(index_sort_label);
+  const smt_sortt &index_sort = static_cast<const smt_sortt &>(index_info);
+  return index_sort;
+}
+
+const smt_sortt &smt_array_sortt::get_element_sort() const
+{
+  const irept &element_info = find(element_sort_label);
+  const smt_sortt &element_sort = static_cast<const smt_sortt &>(element_info);
+  return element_sort;
+}
+
 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,20 @@ class smt_bit_vector_sortt final : public smt_sortt
   std::size_t bit_width() const;
 };
 
+class smt_array_sortt final : public smt_sortt
+{
+private:
+  const std::string index_sort_label{"index_sort"};
+  const std::string element_sort_label{"element_sort"};
+
+public:
+  explicit smt_array_sortt(
+    const smt_sortt &index_sort,
+    const smt_sortt &element_sort);
+  const smt_sortt &get_index_sort() const;
+  const smt_sortt &get_element_sort() const;
+};
+
 class smt_sort_const_downcast_visitort
 {
 public:

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -76,6 +76,12 @@ 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 " << smt_to_smt2_string(array.get_index_sort()) << " "
+       << smt_to_smt2_string(array.get_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,49 @@ 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;
+      REQUIRE(bit_vec.bit_width() == 8);
+    }
+
+    void visit(const smt_array_sortt &) override
+    {
+      array_visited = true;
+    }
+  } visitor;
+
+  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);
 }
 
 TEST_CASE("smt_sortt equality", "[core][smt2_incremental]")
@@ -83,4 +130,9 @@ 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_sort_bv{bit_vector16, bit_vector16};
+  CHECK(array_sort_bv != array_sort);
 }

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -21,6 +21,9 @@ 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)");
 }
 
 TEST_CASE(