Skip to content

Commit 91da8ba

Browse files
thomasspriggsthomasspriggs
committed
Add smt2_incremental_decision_proceduret unit tests
1 parent 28759bc commit 91da8ba

File tree

2 files changed

+207
-0
lines changed

2 files changed

+207
-0
lines changed

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,7 @@ SRC += analyses/ai/ai.cpp \
9999
solvers/sat/satcheck_minisat2.cpp \
100100
solvers/smt2/smt2_conv.cpp \
101101
solvers/smt2_incremental/convert_expr_to_smt.cpp \
102+
solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp \
102103
solvers/smt2_incremental/smt_bit_vector_theory.cpp \
103104
solvers/smt2_incremental/smt_commands.cpp \
104105
solvers/smt2_incremental/smt_core_theory.cpp \

‎unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 206 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,206 @@
1+
// Author: Diffblue Ltd.
2+
3+
#include <testing-utils/use_catch.h>
4+
5+
#include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
6+
#include <solvers/smt2_incremental/smt_commands.h>
7+
#include <solvers/smt2_incremental/smt_core_theory.h>
8+
#include <solvers/smt2_incremental/smt_solver_process.h>
9+
#include <solvers/smt2_incremental/smt_sorts.h>
10+
#include <solvers/smt2_incremental/smt_terms.h>
11+
#include <util/arith_tools.h>
12+
#include <util/bitvector_types.h>
13+
#include <util/make_unique.h>
14+
#include <util/namespace.h>
15+
#include <util/symbol_table.h>
16+
17+
class smt_mock_solver_processt : public smt_base_solver_processt
18+
{
19+
public:
20+
const std::string &description() override
21+
{
22+
UNREACHABLE;
23+
}
24+
25+
void send(const smt_commandt &smt_command) override
26+
{
27+
sent_commands.push_back(smt_command);
28+
}
29+
30+
smt_responset receive_response() override
31+
{
32+
UNREACHABLE;
33+
}
34+
35+
std::vector<smt_commandt> sent_commands;
36+
37+
~smt_mock_solver_processt() override = default;
38+
};
39+
40+
static symbolt make_test_symbol(irep_idt id, typet type)
41+
{
42+
symbolt new_symbol;
43+
new_symbol.name = std::move(id);
44+
new_symbol.type = std::move(type);
45+
return new_symbol;
46+
}
47+
48+
static symbolt make_test_symbol(irep_idt id, exprt value)
49+
{
50+
symbolt new_symbol;
51+
new_symbol.name = std::move(id);
52+
new_symbol.type = value.type();
53+
new_symbol.value = std::move(value);
54+
return new_symbol;
55+
}
56+
57+
TEST_CASE(
58+
"smt2_incremental_decision_proceduret commands sent",
59+
"[core][smt2_incremental]")
60+
{
61+
symbol_tablet symbol_table;
62+
namespacet ns{symbol_table};
63+
auto mock_process = util_make_unique<smt_mock_solver_processt>();
64+
auto &sent_commands = mock_process->sent_commands;
65+
null_message_handlert message_handler;
66+
SECTION("Construction / solver initialisation.")
67+
{
68+
smt2_incremental_decision_proceduret procedure{
69+
ns, std::move(mock_process), message_handler};
70+
REQUIRE(
71+
sent_commands ==
72+
std::vector<smt_commandt>{
73+
smt_set_option_commandt{smt_option_produce_modelst{true}},
74+
smt_set_logic_commandt{
75+
smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}}});
76+
sent_commands.clear();
77+
SECTION("Set symbol to true.")
78+
{
79+
const symbolt foo = make_test_symbol("foo", bool_typet{});
80+
const smt_identifier_termt foo_term{"foo", smt_bool_sortt{}};
81+
procedure.set_to(foo.symbol_expr(), true);
82+
REQUIRE(
83+
sent_commands ==
84+
std::vector<smt_commandt>{smt_declare_function_commandt{foo_term, {}},
85+
smt_assert_commandt{foo_term}});
86+
}
87+
SECTION("Set symbol to false.")
88+
{
89+
const symbolt foo = make_test_symbol("foo", bool_typet{});
90+
const smt_identifier_termt foo_term{"foo", smt_bool_sortt{}};
91+
procedure.set_to(foo.symbol_expr(), false);
92+
REQUIRE(
93+
sent_commands ==
94+
std::vector<smt_commandt>{
95+
smt_declare_function_commandt{foo_term, {}},
96+
smt_assert_commandt{smt_core_theoryt::make_not(foo_term)}});
97+
}
98+
SECTION("Set using chaining of symbol expressions.")
99+
{
100+
const symbolt forty_two =
101+
make_test_symbol("forty_two", from_integer({42}, signedbv_typet{16}));
102+
symbol_table.insert(forty_two);
103+
const smt_identifier_termt forty_two_term{"forty_two",
104+
smt_bit_vector_sortt{16}};
105+
const symbolt nondet_int_a =
106+
make_test_symbol("nondet_int_a", signedbv_typet{16});
107+
symbol_table.insert(nondet_int_a);
108+
const smt_identifier_termt nondet_int_a_term{"nondet_int_a",
109+
smt_bit_vector_sortt{16}};
110+
const symbolt nondet_int_b =
111+
make_test_symbol("nondet_int_b", signedbv_typet{16});
112+
symbol_table.insert(nondet_int_b);
113+
const smt_identifier_termt nondet_int_b_term{"nondet_int_b",
114+
smt_bit_vector_sortt{16}};
115+
const symbolt first_comparison = make_test_symbol(
116+
"first_comparison",
117+
equal_exprt{nondet_int_a.symbol_expr(), forty_two.symbol_expr()});
118+
symbol_table.insert(first_comparison);
119+
const symbolt second_comparison = make_test_symbol(
120+
"second_comparison",
121+
not_exprt{
122+
equal_exprt{nondet_int_b.symbol_expr(), forty_two.symbol_expr()}});
123+
symbol_table.insert(second_comparison);
124+
const symbolt third_comparison = make_test_symbol(
125+
"third_comparison",
126+
equal_exprt{nondet_int_a.symbol_expr(), nondet_int_b.symbol_expr()});
127+
symbol_table.insert(third_comparison);
128+
const symbolt comparison_conjunction = make_test_symbol(
129+
"comparison_conjunction",
130+
and_exprt{{first_comparison.symbol_expr(),
131+
second_comparison.symbol_expr(),
132+
third_comparison.symbol_expr()}});
133+
symbol_table.insert(comparison_conjunction);
134+
smt_identifier_termt comparison_conjunction_term{"comparison_conjunction",
135+
smt_bool_sortt{}};
136+
procedure.set_to(comparison_conjunction.symbol_expr(), true);
137+
REQUIRE(
138+
sent_commands ==
139+
std::vector<smt_commandt>{
140+
smt_declare_function_commandt{nondet_int_b_term, {}},
141+
smt_declare_function_commandt{nondet_int_a_term, {}},
142+
smt_define_function_commandt{
143+
"third_comparison",
144+
{},
145+
smt_core_theoryt::equal(nondet_int_a_term, nondet_int_b_term)},
146+
smt_define_function_commandt{
147+
"forty_two", {}, smt_bit_vector_constant_termt{42, 16}},
148+
smt_define_function_commandt{
149+
"second_comparison",
150+
{},
151+
smt_core_theoryt::make_not(
152+
smt_core_theoryt::equal(nondet_int_b_term, forty_two_term))},
153+
smt_define_function_commandt{
154+
"first_comparison",
155+
{},
156+
smt_core_theoryt::equal(nondet_int_a_term, forty_two_term)},
157+
smt_define_function_commandt{
158+
"comparison_conjunction",
159+
{},
160+
smt_core_theoryt::make_and(
161+
smt_core_theoryt::make_and(
162+
smt_identifier_termt{"first_comparison", smt_bool_sortt{}},
163+
smt_identifier_termt{"second_comparison", smt_bool_sortt{}}),
164+
smt_identifier_termt{"third_comparison", smt_bool_sortt{}})},
165+
smt_assert_commandt{comparison_conjunction_term}});
166+
}
167+
SECTION("Handle of value-less symbol.")
168+
{
169+
const symbolt foo = make_test_symbol("foo", bool_typet{});
170+
const smt_identifier_termt foo_term{"foo", smt_bool_sortt{}};
171+
procedure.handle(foo.symbol_expr());
172+
REQUIRE(
173+
sent_commands == std::vector<smt_commandt>{
174+
smt_declare_function_commandt{foo_term, {}},
175+
smt_define_function_commandt{"B0", {}, foo_term}});
176+
sent_commands.clear();
177+
SECTION("Handle of previously handled expression.")
178+
{
179+
procedure.handle(foo.symbol_expr());
180+
REQUIRE(sent_commands.empty());
181+
}
182+
SECTION("Handle of new expression containing previously defined symbol.")
183+
{
184+
procedure.handle(equal_exprt{foo.symbol_expr(), foo.symbol_expr()});
185+
REQUIRE(
186+
sent_commands ==
187+
std::vector<smt_commandt>{smt_define_function_commandt{
188+
"B1", {}, smt_core_theoryt::equal(foo_term, foo_term)}});
189+
}
190+
}
191+
SECTION("Handle of symbol with value.")
192+
{
193+
const symbolt bar =
194+
make_test_symbol("bar", from_integer({42}, signedbv_typet{8}));
195+
symbol_table.insert(bar);
196+
procedure.handle(bar.symbol_expr());
197+
REQUIRE(
198+
sent_commands ==
199+
std::vector<smt_commandt>{
200+
smt_define_function_commandt{
201+
"bar", {}, smt_bit_vector_constant_termt{42, 8}},
202+
smt_define_function_commandt{
203+
"B0", {}, smt_identifier_termt{"bar", smt_bit_vector_sortt{8}}}});
204+
}
205+
}
206+
}

0 commit comments

Comments
 (0)