From 3d485f84ba556452f86e7d8fff55e1c2282ec820 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 20 Jun 2022 17:46:21 +0100 Subject: [PATCH] Add an `Array` sort in the new SMT backend, along with unit tests for the sort and its printing. Co-authored-by: Fotis Koutoulakis Co-authored-by: Enrico Steffinlongo --- .../smt2_incremental/convert_expr_to_smt.cpp | 13 +++ src/solvers/smt2_incremental/smt_sorts.cpp | 19 +++++ src/solvers/smt2_incremental/smt_sorts.def | 1 + src/solvers/smt2_incremental/smt_sorts.h | 10 +++ .../smt2_incremental/smt_to_smt2_string.cpp | 5 ++ unit/solvers/smt2_incremental/smt_sorts.cpp | 83 +++++++++++++++++++ .../smt2_incremental/smt_to_smt2_string.cpp | 12 +++ 7 files changed, 143 insertions(+) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index e74c1a5717d..5e05c1147dd 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/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) diff --git a/src/solvers/smt2_incremental/smt_sorts.cpp b/src/solvers/smt2_incremental/smt_sorts.cpp index ed06bfee629..e12fac29259 100644 --- a/src/solvers/smt2_incremental/smt_sorts.cpp +++ b/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(find(ID_index)); +} + +const smt_sortt &smt_array_sortt::element_sort() const +{ + return static_cast(find(ID_value)); +} + template void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor) { diff --git a/src/solvers/smt2_incremental/smt_sorts.def b/src/solvers/smt2_incremental/smt_sorts.def index 1bb57e4379b..374cdcba4b3 100644 --- a/src/solvers/smt2_incremental/smt_sorts.def +++ b/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) diff --git a/src/solvers/smt2_incremental/smt_sorts.h b/src/solvers/smt2_incremental/smt_sorts.h index 5d80fbc0500..307cb4a3134 100644 --- a/src/solvers/smt2_incremental/smt_sorts.h +++ b/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: diff --git a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp index 8a7c8cc70c1..789cc8118bb 100644 --- a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp +++ b/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) diff --git a/unit/solvers/smt2_incremental/smt_sorts.cpp b/unit/solvers/smt2_incremental/smt_sorts.cpp index 50c1e3ec7fb..54513f6c5e3 100644 --- a/unit/solvers/smt2_incremental/smt_sorts.cpp +++ b/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()); } diff --git a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp index 4f1475e922f..48392e20625 100644 --- a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp +++ b/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(