Skip to content

Commit 91eac8a

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #6965 from NlightNFotis/array_declaration_conversion
Add an `Array` sort in the new SMT backend
2 parents d46627d + 3d485f8 commit 91eac8a

File tree

7 files changed

+143
-0
lines changed

7 files changed

+143
-0
lines changed

‎src/solvers/smt2_incremental/convert_expr_to_smt.cpp‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -213,6 +213,13 @@ struct sort_based_cast_to_bit_vector_convertert final
213213
"Generation of SMT formula for type cast to bit vector from type: " +
214214
from_type.pretty());
215215
}
216+
217+
void visit(const smt_array_sortt &) override
218+
{
219+
UNIMPLEMENTED_FEATURE(
220+
"Generation of SMT formula for type cast to bit vector from type: " +
221+
from_type.pretty());
222+
}
216223
};
217224

218225
static smt_termt convert_bit_vector_cast(
@@ -294,6 +301,12 @@ struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort
294301
const auto value = bvrep2integer(member_input.get_value(), width, false);
295302
result = smt_bit_vector_constant_termt{value, bit_vector_sort};
296303
}
304+
305+
void visit(const smt_array_sortt &array_sort) override
306+
{
307+
UNIMPLEMENTED_FEATURE(
308+
"Conversion of array SMT literal " + array_sort.pretty());
309+
}
297310
};
298311

299312
static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)

‎src/solvers/smt2_incremental/smt_sorts.cpp‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,25 @@ std::size_t smt_bit_vector_sortt::bit_width() const
6262
return get_size_t(ID_width);
6363
}
6464

65+
smt_array_sortt::smt_array_sortt(
66+
const smt_sortt &index_sort,
67+
const smt_sortt &element_sort)
68+
: smt_sortt{ID_smt_array_sort}
69+
{
70+
add(ID_index, index_sort);
71+
add(ID_value, element_sort);
72+
}
73+
74+
const smt_sortt &smt_array_sortt::index_sort() const
75+
{
76+
return static_cast<const smt_sortt &>(find(ID_index));
77+
}
78+
79+
const smt_sortt &smt_array_sortt::element_sort() const
80+
{
81+
return static_cast<const smt_sortt &>(find(ID_value));
82+
}
83+
6584
template <typename visitort>
6685
void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
6786
{

‎src/solvers/smt2_incremental/smt_sorts.def‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,4 @@
88
/// * The type of sort checks required to implement `smt_sortt::accept`.
99
SORT_ID(bool)
1010
SORT_ID(bit_vector)
11+
SORT_ID(array)

‎src/solvers/smt2_incremental/smt_sorts.h‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,16 @@ class smt_bit_vector_sortt final : public smt_sortt
8787
std::size_t bit_width() const;
8888
};
8989

90+
class smt_array_sortt final : public smt_sortt
91+
{
92+
public:
93+
explicit smt_array_sortt(
94+
const smt_sortt &index_sort,
95+
const smt_sortt &element_sort);
96+
const smt_sortt &index_sort() const;
97+
const smt_sortt &element_sort() const;
98+
};
99+
90100
class smt_sort_const_downcast_visitort
91101
{
92102
public:

‎src/solvers/smt2_incremental/smt_to_smt2_string.cpp‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,11 @@ class smt_sort_output_visitort : public smt_sort_const_downcast_visitort
7676
{
7777
os << "(_ BitVec " << bit_vec.bit_width() << ")";
7878
}
79+
80+
void visit(const smt_array_sortt &array) override
81+
{
82+
os << "(Array " << array.index_sort() << " " << array.element_sort() << ")";
83+
}
7984
};
8085

8186
std::ostream &operator<<(std::ostream &os, const smt_sortt &sort)

‎unit/solvers/smt2_incremental/smt_sorts.cpp‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ TEST_CASE("Visiting smt_bool_sortt.", "[core][smt2_incremental]")
3232
public:
3333
bool bool_visited = false;
3434
bool bit_vec_visited = false;
35+
bool array_visited = false;
3536

3637
void visit(const smt_bool_sortt &) override
3738
{
@@ -42,10 +43,16 @@ TEST_CASE("Visiting smt_bool_sortt.", "[core][smt2_incremental]")
4243
{
4344
bit_vec_visited = true;
4445
}
46+
47+
void visit(const smt_array_sortt &) override
48+
{
49+
array_visited = true;
50+
}
4551
} visitor;
4652
smt_bool_sortt{}.accept(visitor);
4753
REQUIRE(visitor.bool_visited);
4854
REQUIRE_FALSE(visitor.bit_vec_visited);
55+
REQUIRE_FALSE(visitor.array_visited);
4956
}
5057

5158
TEST_CASE("Visiting smt_bit_vec_sortt.", "[core][smt2_incremental]")
@@ -55,6 +62,7 @@ TEST_CASE("Visiting smt_bit_vec_sortt.", "[core][smt2_incremental]")
5562
public:
5663
bool bool_visited = false;
5764
bool bit_vec_visited = false;
65+
bool array_visited = false;
5866

5967
void visit(const smt_bool_sortt &) override
6068
{
@@ -66,10 +74,53 @@ TEST_CASE("Visiting smt_bit_vec_sortt.", "[core][smt2_incremental]")
6674
bit_vec_visited = true;
6775
REQUIRE(bit_vec.bit_width() == 8);
6876
}
77+
78+
void visit(const smt_array_sortt &) override
79+
{
80+
array_visited = true;
81+
}
6982
} visitor;
7083
smt_bit_vector_sortt{8}.accept(visitor);
7184
REQUIRE_FALSE(visitor.bool_visited);
7285
REQUIRE(visitor.bit_vec_visited);
86+
REQUIRE_FALSE(visitor.array_visited);
87+
}
88+
89+
TEST_CASE("Visiting smt_array_sort.", "[core][smt2_incremental]")
90+
{
91+
class : public smt_sort_const_downcast_visitort
92+
{
93+
public:
94+
bool bool_visited = false;
95+
bool bit_vec_visited = false;
96+
bool array_visited = false;
97+
98+
void visit(const smt_bool_sortt &) override
99+
{
100+
bool_visited = true;
101+
}
102+
103+
void visit(const smt_bit_vector_sortt &bit_vec) override
104+
{
105+
bit_vec_visited = true;
106+
}
107+
108+
void visit(const smt_array_sortt &) override
109+
{
110+
array_visited = true;
111+
}
112+
} visitor, visitor_second;
113+
114+
smt_array_sortt{smt_bool_sortt{}, smt_bool_sortt{}}.accept(visitor);
115+
REQUIRE_FALSE(visitor.bool_visited);
116+
REQUIRE_FALSE(visitor.bit_vec_visited);
117+
REQUIRE(visitor.array_visited);
118+
119+
smt_array_sortt{smt_bit_vector_sortt{64}, smt_bit_vector_sortt{32}}.accept(
120+
visitor_second);
121+
REQUIRE_FALSE(visitor_second.bool_visited);
122+
REQUIRE_FALSE(visitor_second.bit_vec_visited);
123+
REQUIRE(visitor_second.array_visited);
73124
}
74125

75126
TEST_CASE("smt_sortt equality", "[core][smt2_incremental]")
@@ -83,4 +134,36 @@ TEST_CASE("smt_sortt equality", "[core][smt2_incremental]")
83134
CHECK(bit_vector8 != bool_sort1);
84135
const smt_bit_vector_sortt bit_vector16{16};
85136
CHECK(bit_vector8 != bit_vector16);
137+
const smt_array_sortt array_sort{smt_bool_sortt{}, smt_bool_sortt{}};
138+
CHECK(array_sort != bool_sort1);
139+
CHECK(array_sort != bit_vector8);
140+
const smt_array_sortt array_sort2{smt_bool_sortt{}, smt_bool_sortt{}};
141+
CHECK(array_sort == array_sort2);
142+
const smt_array_sortt array_sort_bv{bit_vector16, bit_vector16};
143+
CHECK(array_sort_bv != array_sort);
144+
const smt_array_sortt array_sort_bv2{bit_vector16, bit_vector16};
145+
CHECK(array_sort_bv2 == array_sort_bv);
146+
}
147+
148+
TEST_CASE(
149+
"Test smt_array_sort get_index_sort getter.",
150+
"[core][smt2_incremental]")
151+
{
152+
const smt_array_sortt array_sort{smt_bool_sortt{}, smt_bool_sortt{}};
153+
REQUIRE(smt_bool_sortt{} == array_sort.index_sort());
154+
155+
const smt_array_sortt array_sort2{smt_bit_vector_sortt{16}, smt_bool_sortt{}};
156+
REQUIRE(smt_bit_vector_sortt{16} == array_sort2.index_sort());
157+
}
158+
159+
TEST_CASE(
160+
"Test smt_array_sort get_element_sort getter.",
161+
"[core][smt2_incremental]")
162+
{
163+
const smt_array_sortt array_sort{smt_bool_sortt{}, smt_bool_sortt{}};
164+
REQUIRE(smt_bool_sortt{} == array_sort.element_sort());
165+
166+
const smt_array_sortt array_sort2{
167+
smt_bit_vector_sortt{16}, smt_bit_vector_sortt{64}};
168+
REQUIRE(smt_bit_vector_sortt{64} == array_sort2.element_sort());
86169
}

‎unit/solvers/smt2_incremental/smt_to_smt2_string.cpp‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,18 @@ TEST_CASE("Test smt_sortt to string conversion", "[core][smt2_incremental]")
2121
{
2222
CHECK(smt_to_smt2_string(smt_bool_sortt{}) == "Bool");
2323
CHECK(smt_to_smt2_string(smt_bit_vector_sortt{16}) == "(_ BitVec 16)");
24+
CHECK(
25+
smt_to_smt2_string(smt_array_sortt{smt_bool_sortt{}, smt_bool_sortt{}}) ==
26+
"(Array Bool Bool)");
27+
CHECK(
28+
smt_to_smt2_string(
29+
smt_array_sortt(smt_bit_vector_sortt{64}, smt_bit_vector_sortt{16})) ==
30+
"(Array (_ BitVec 64) (_ BitVec 16))");
31+
CHECK(
32+
smt_to_smt2_string(smt_array_sortt(
33+
smt_bit_vector_sortt{64},
34+
smt_array_sortt(smt_bool_sortt{}, smt_bit_vector_sortt{16}))) ==
35+
"(Array (_ BitVec 64) (Array Bool (_ BitVec 16)))");
2436
}
2537

2638
TEST_CASE(

0 commit comments

Comments
 (0)