Skip to content

Commit a5fc2df

Browse files
NlightNFotisEnrico Steffinlongo
NlightNFotis
and
Enrico Steffinlongo
committed
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]>
1 parent e78eacf commit a5fc2df

File tree

7 files changed

+144
-0
lines changed

7 files changed

+144
-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::get_index_sort() const
75+
{
76+
return static_cast<const smt_sortt &>(find(ID_index));
77+
}
78+
79+
const smt_sortt &smt_array_sortt::get_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 &get_index_sort() const;
97+
const smt_sortt &get_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: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,12 @@ 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.get_index_sort() << " " << array.get_element_sort()
83+
<< ")";
84+
}
7985
};
8086

8187
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.get_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.get_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.get_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.get_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)