Skip to content

Commit 13da8cf

Browse files
thomasspriggsthomasspriggs
committed
Separate duplicated unit test environment setup code
To avoid duplicating the same setup for every test.
1 parent 0889b84 commit 13da8cf

File tree

1 file changed

+82
-58
lines changed

1 file changed

+82
-58
lines changed

‎unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 82 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -25,33 +25,67 @@
2525

2626
class smt_mock_solver_processt : public smt_base_solver_processt
2727
{
28+
std::function<void(const smt_commandt &)> _send;
29+
std::function<smt_responset()> _receive;
30+
2831
public:
32+
smt_mock_solver_processt(
33+
std::function<void(const smt_commandt &)> send,
34+
std::function<smt_responset()> receive)
35+
: _send{std::move(send)}, _receive{std::move(receive)}
36+
{
37+
}
38+
2939
const std::string &description() override
3040
{
3141
UNREACHABLE;
3242
}
3343

3444
void send(const smt_commandt &smt_command) override
3545
{
36-
sent_commands.push_back(smt_command);
46+
_send(smt_command);
3747
}
3848

39-
std::deque<smt_responset> responses;
40-
4149
smt_responset receive_response() override
4250
{
43-
INVARIANT(
44-
!responses.empty(), "There must be responses remaining for test.");
45-
smt_responset response = responses.front();
46-
responses.pop_front();
47-
return response;
51+
return _receive();
4852
}
4953

50-
std::vector<smt_commandt> sent_commands;
51-
5254
~smt_mock_solver_processt() override = default;
5355
};
5456

57+
struct decision_procedure_test_environmentt final
58+
{
59+
void send(const smt_commandt &smt_command);
60+
smt_responset receive_response();
61+
62+
symbol_tablet symbol_table;
63+
namespacet ns{symbol_table};
64+
std::deque<smt_responset> mock_responses;
65+
std::vector<smt_commandt> sent_commands;
66+
null_message_handlert message_handler;
67+
smt2_incremental_decision_proceduret procedure{
68+
ns,
69+
util_make_unique<smt_mock_solver_processt>(
70+
[&](const smt_commandt &smt_command) { this->send(smt_command); },
71+
[&]() { return this->receive_response(); }),
72+
message_handler};
73+
};
74+
75+
void decision_procedure_test_environmentt::send(const smt_commandt &smt_command)
76+
{
77+
sent_commands.push_back(smt_command);
78+
}
79+
80+
smt_responset decision_procedure_test_environmentt::receive_response()
81+
{
82+
INVARIANT(
83+
!mock_responses.empty(), "There must be responses remaining for test.");
84+
smt_responset response = mock_responses.front();
85+
mock_responses.pop_front();
86+
return response;
87+
}
88+
5589
static symbolt make_test_symbol(irep_idt id, typet type)
5690
{
5791
symbolt new_symbol;
@@ -73,39 +107,33 @@ TEST_CASE(
73107
"smt2_incremental_decision_proceduret commands sent",
74108
"[core][smt2_incremental]")
75109
{
76-
symbol_tablet symbol_table;
77-
namespacet ns{symbol_table};
78-
auto mock_process = util_make_unique<smt_mock_solver_processt>();
79-
auto &sent_commands = mock_process->sent_commands;
80-
null_message_handlert message_handler;
110+
decision_procedure_test_environmentt test{};
81111
SECTION("Construction / solver initialisation.")
82112
{
83-
smt2_incremental_decision_proceduret procedure{
84-
ns, std::move(mock_process), message_handler};
85113
REQUIRE(
86-
sent_commands ==
114+
test.sent_commands ==
87115
std::vector<smt_commandt>{
88116
smt_set_option_commandt{smt_option_produce_modelst{true}},
89117
smt_set_logic_commandt{
90118
smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}}});
91-
sent_commands.clear();
119+
test.sent_commands.clear();
92120
SECTION("Set symbol to true.")
93121
{
94122
const symbolt foo = make_test_symbol("foo", bool_typet{});
95123
const smt_identifier_termt foo_term{"foo", smt_bool_sortt{}};
96-
procedure.set_to(foo.symbol_expr(), true);
124+
test.procedure.set_to(foo.symbol_expr(), true);
97125
REQUIRE(
98-
sent_commands ==
126+
test.sent_commands ==
99127
std::vector<smt_commandt>{smt_declare_function_commandt{foo_term, {}},
100128
smt_assert_commandt{foo_term}});
101129
}
102130
SECTION("Set symbol to false.")
103131
{
104132
const symbolt foo = make_test_symbol("foo", bool_typet{});
105133
const smt_identifier_termt foo_term{"foo", smt_bool_sortt{}};
106-
procedure.set_to(foo.symbol_expr(), false);
134+
test.procedure.set_to(foo.symbol_expr(), false);
107135
REQUIRE(
108-
sent_commands ==
136+
test.sent_commands ==
109137
std::vector<smt_commandt>{
110138
smt_declare_function_commandt{foo_term, {}},
111139
smt_assert_commandt{smt_core_theoryt::make_not(foo_term)}});
@@ -114,43 +142,43 @@ TEST_CASE(
114142
{
115143
const symbolt forty_two =
116144
make_test_symbol("forty_two", from_integer({42}, signedbv_typet{16}));
117-
symbol_table.insert(forty_two);
145+
test.symbol_table.insert(forty_two);
118146
const smt_identifier_termt forty_two_term{"forty_two",
119147
smt_bit_vector_sortt{16}};
120148
const symbolt nondet_int_a =
121149
make_test_symbol("nondet_int_a", signedbv_typet{16});
122-
symbol_table.insert(nondet_int_a);
150+
test.symbol_table.insert(nondet_int_a);
123151
const smt_identifier_termt nondet_int_a_term{"nondet_int_a",
124152
smt_bit_vector_sortt{16}};
125153
const symbolt nondet_int_b =
126154
make_test_symbol("nondet_int_b", signedbv_typet{16});
127-
symbol_table.insert(nondet_int_b);
155+
test.symbol_table.insert(nondet_int_b);
128156
const smt_identifier_termt nondet_int_b_term{"nondet_int_b",
129157
smt_bit_vector_sortt{16}};
130158
const symbolt first_comparison = make_test_symbol(
131159
"first_comparison",
132160
equal_exprt{nondet_int_a.symbol_expr(), forty_two.symbol_expr()});
133-
symbol_table.insert(first_comparison);
161+
test.symbol_table.insert(first_comparison);
134162
const symbolt second_comparison = make_test_symbol(
135163
"second_comparison",
136164
not_exprt{
137165
equal_exprt{nondet_int_b.symbol_expr(), forty_two.symbol_expr()}});
138-
symbol_table.insert(second_comparison);
166+
test.symbol_table.insert(second_comparison);
139167
const symbolt third_comparison = make_test_symbol(
140168
"third_comparison",
141169
equal_exprt{nondet_int_a.symbol_expr(), nondet_int_b.symbol_expr()});
142-
symbol_table.insert(third_comparison);
170+
test.symbol_table.insert(third_comparison);
143171
const symbolt comparison_conjunction = make_test_symbol(
144172
"comparison_conjunction",
145173
and_exprt{{first_comparison.symbol_expr(),
146174
second_comparison.symbol_expr(),
147175
third_comparison.symbol_expr()}});
148-
symbol_table.insert(comparison_conjunction);
176+
test.symbol_table.insert(comparison_conjunction);
149177
smt_identifier_termt comparison_conjunction_term{"comparison_conjunction",
150178
smt_bool_sortt{}};
151-
procedure.set_to(comparison_conjunction.symbol_expr(), true);
179+
test.procedure.set_to(comparison_conjunction.symbol_expr(), true);
152180
REQUIRE(
153-
sent_commands ==
181+
test.sent_commands ==
154182
std::vector<smt_commandt>{
155183
smt_declare_function_commandt{nondet_int_a_term, {}},
156184
smt_define_function_commandt{
@@ -183,22 +211,24 @@ TEST_CASE(
183211
{
184212
const symbolt foo = make_test_symbol("foo", bool_typet{});
185213
const smt_identifier_termt foo_term{"foo", smt_bool_sortt{}};
186-
procedure.handle(foo.symbol_expr());
214+
test.procedure.handle(foo.symbol_expr());
187215
REQUIRE(
188-
sent_commands == std::vector<smt_commandt>{
189-
smt_declare_function_commandt{foo_term, {}},
190-
smt_define_function_commandt{"B0", {}, foo_term}});
191-
sent_commands.clear();
216+
test.sent_commands ==
217+
std::vector<smt_commandt>{
218+
smt_declare_function_commandt{foo_term, {}},
219+
smt_define_function_commandt{"B0", {}, foo_term}});
220+
test.sent_commands.clear();
192221
SECTION("Handle of previously handled expression.")
193222
{
194-
procedure.handle(foo.symbol_expr());
195-
REQUIRE(sent_commands.empty());
223+
test.procedure.handle(foo.symbol_expr());
224+
REQUIRE(test.sent_commands.empty());
196225
}
197226
SECTION("Handle of new expression containing previously defined symbol.")
198227
{
199-
procedure.handle(equal_exprt{foo.symbol_expr(), foo.symbol_expr()});
228+
test.procedure.handle(
229+
equal_exprt{foo.symbol_expr(), foo.symbol_expr()});
200230
REQUIRE(
201-
sent_commands ==
231+
test.sent_commands ==
202232
std::vector<smt_commandt>{smt_define_function_commandt{
203233
"B1", {}, smt_core_theoryt::equal(foo_term, foo_term)}});
204234
}
@@ -207,10 +237,10 @@ TEST_CASE(
207237
{
208238
const symbolt bar =
209239
make_test_symbol("bar", from_integer({42}, signedbv_typet{8}));
210-
symbol_table.insert(bar);
211-
procedure.handle(bar.symbol_expr());
240+
test.symbol_table.insert(bar);
241+
test.procedure.handle(bar.symbol_expr());
212242
REQUIRE(
213-
sent_commands ==
243+
test.sent_commands ==
214244
std::vector<smt_commandt>{
215245
smt_define_function_commandt{
216246
"bar", {}, smt_bit_vector_constant_termt{42, 8}},
@@ -224,18 +254,12 @@ TEST_CASE(
224254
"smt2_incremental_decision_proceduret number of solver calls.",
225255
"[core][smt2_incremental]")
226256
{
227-
symbol_tablet symbol_table;
228-
namespacet ns{symbol_table};
229-
auto mock_process = util_make_unique<smt_mock_solver_processt>();
230-
auto &responses = mock_process->responses;
231-
null_message_handlert message_handler;
232-
smt2_incremental_decision_proceduret procedure{
233-
ns, std::move(mock_process), message_handler};
234-
REQUIRE(procedure.get_number_of_solver_calls() == 0);
235-
responses.push_back(smt_check_sat_responset{smt_unsat_responset{}});
236-
procedure();
237-
REQUIRE(procedure.get_number_of_solver_calls() == 1);
238-
responses.push_back(smt_check_sat_responset{smt_unsat_responset{}});
239-
procedure();
240-
REQUIRE(procedure.get_number_of_solver_calls() == 2);
257+
decision_procedure_test_environmentt test{};
258+
REQUIRE(test.procedure.get_number_of_solver_calls() == 0);
259+
test.mock_responses.push_back(smt_check_sat_responset{smt_unsat_responset{}});
260+
test.procedure();
261+
REQUIRE(test.procedure.get_number_of_solver_calls() == 1);
262+
test.mock_responses.push_back(smt_check_sat_responset{smt_unsat_responset{}});
263+
test.procedure();
264+
REQUIRE(test.procedure.get_number_of_solver_calls() == 2);
241265
}

0 commit comments

Comments
 (0)