Skip to content

Commit d3dc560

Browse files
thomasspriggsthomasspriggs
authored
Merge pull request #6256 from thomasspriggs/tas/smt_function_factories
Add incremental SMT2 sort checked construction of bit vector predicate application and application of core theory functions
2 parents 06afe80 + 686ba37 commit d3dc560

20 files changed

+891
-87
lines changed

‎src/solvers/Makefile

+2
Original file line numberDiff line numberDiff line change
@@ -192,7 +192,9 @@ SRC = $(BOOLEFORCE_SRC) \
192192
smt2/smt2_parser.cpp \
193193
smt2/smt2_tokenizer.cpp \
194194
smt2/smt2irep.cpp \
195+
smt2_incremental/smt_bit_vector_theory.cpp \
195196
smt2_incremental/smt_commands.cpp \
197+
smt2_incremental/smt_core_theory.cpp \
196198
smt2_incremental/smt_logics.cpp \
197199
smt2_incremental/smt_options.cpp \
198200
smt2_incremental/smt_sorts.cpp \

‎src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

+44
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
// Author: Diffblue Ltd.
2+
3+
#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
4+
5+
#include <util/invariant.h>
6+
7+
static void validate_bit_vector_predicate_arguments(
8+
const smt_termt &left,
9+
const smt_termt &right)
10+
{
11+
const auto left_sort = left.get_sort().cast<smt_bit_vector_sortt>();
12+
INVARIANT(left_sort, "Left operand must have bitvector sort.");
13+
const auto right_sort = right.get_sort().cast<smt_bit_vector_sortt>();
14+
INVARIANT(right_sort, "Right operand must have bitvector sort.");
15+
// The below invariant is based on the smtlib standard.
16+
// See http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV
17+
INVARIANT(
18+
left_sort->bit_width() == right_sort->bit_width(),
19+
"Left and right operands must have the same bit width.");
20+
}
21+
22+
#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name) \
23+
void smt_bit_vector_theoryt::the_name##t::validate( \
24+
const smt_termt &left, const smt_termt &right) \
25+
{ \
26+
validate_bit_vector_predicate_arguments(left, right); \
27+
} \
28+
\
29+
smt_sortt smt_bit_vector_theoryt::the_name##t::return_sort( \
30+
const smt_termt &, const smt_termt &) \
31+
{ \
32+
return smt_bool_sortt{}; \
33+
} \
34+
\
35+
const char *smt_bit_vector_theoryt::the_name##t::identifier() \
36+
{ \
37+
return #the_identifier; \
38+
} \
39+
\
40+
const smt_function_application_termt::factoryt< \
41+
smt_bit_vector_theoryt::the_name##t> \
42+
smt_bit_vector_theoryt::the_name{};
43+
#include "smt_bit_vector_theory.def"
44+
#undef SMT_BITVECTOR_THEORY_PREDICATE

‎src/solvers/smt2_incremental/smt_bit_vector_theory.def

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
/// \file
2+
/// This set of definitions is used as part of the
3+
/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
4+
/// set of bitvector theory functions which are implemented and it is used to
5+
/// automate repetitive parts of the implementation.
6+
SMT_BITVECTOR_THEORY_PREDICATE(bvult, unsigned_less_than)
7+
SMT_BITVECTOR_THEORY_PREDICATE(bvule, unsigned_less_than_or_equal)
8+
SMT_BITVECTOR_THEORY_PREDICATE(bvugt, unsigned_greater_than)
9+
SMT_BITVECTOR_THEORY_PREDICATE(bvuge, unsigned_greater_than_or_equal)
10+
SMT_BITVECTOR_THEORY_PREDICATE(bvslt, signed_less_than)
11+
SMT_BITVECTOR_THEORY_PREDICATE(bvsle, signed_less_than_or_equal)
12+
SMT_BITVECTOR_THEORY_PREDICATE(bvsgt, signed_greater_than)
13+
SMT_BITVECTOR_THEORY_PREDICATE(bvsge, signed_greater_than_or_equal)

‎src/solvers/smt2_incremental/smt_bit_vector_theory.h

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
// Author: Diffblue Ltd.
2+
3+
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
4+
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
5+
6+
#include <solvers/smt2_incremental/smt_terms.h>
7+
8+
class smt_bit_vector_theoryt
9+
{
10+
public:
11+
#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name) \
12+
/* NOLINTNEXTLINE(readability/identifiers) cpplint does not match the ## */ \
13+
struct the_name##t final \
14+
{ \
15+
static const char *identifier(); \
16+
static smt_sortt \
17+
return_sort(const smt_termt &left, const smt_termt &right); \
18+
static void validate(const smt_termt &left, const smt_termt &right); \
19+
}; \
20+
static const smt_function_application_termt::factoryt<the_name##t> the_name;
21+
#include "smt_bit_vector_theory.def"
22+
#undef SMT_BITVECTOR_THEORY_PREDICATE
23+
};
24+
25+
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

‎src/solvers/smt2_incremental/smt_commands.cpp

+48
Original file line numberDiff line numberDiff line change
@@ -198,3 +198,51 @@ void smt_commandt::accept(smt_command_const_downcast_visitort &&visitor) const
198198
{
199199
::accept(*this, id(), std::move(visitor));
200200
}
201+
202+
smt_command_functiont::smt_command_functiont(
203+
const smt_declare_function_commandt &function_declaration)
204+
: _identifier(function_declaration.identifier())
205+
{
206+
const auto sort_references = function_declaration.parameter_sorts();
207+
parameter_sorts =
208+
make_range(sort_references).collect<decltype(parameter_sorts)>();
209+
}
210+
211+
smt_command_functiont::smt_command_functiont(
212+
const smt_define_function_commandt &function_definition)
213+
: _identifier{function_definition.identifier()}
214+
{
215+
const auto parameters = function_definition.parameters();
216+
parameter_sorts =
217+
make_range(parameters)
218+
.map([](const smt_termt &term) { return term.get_sort(); })
219+
.collect<decltype(parameter_sorts)>();
220+
}
221+
222+
irep_idt smt_command_functiont::identifier() const
223+
{
224+
return _identifier.identifier();
225+
}
226+
227+
smt_sortt smt_command_functiont::return_sort(
228+
const std::vector<smt_termt> &arguments) const
229+
{
230+
return _identifier.get_sort();
231+
}
232+
233+
void smt_command_functiont::validate(
234+
const std::vector<smt_termt> &arguments) const
235+
{
236+
INVARIANT(
237+
parameter_sorts.size() == arguments.size(),
238+
"Number of parameters and number of arguments must be the same.");
239+
const auto parameter_sort_arguments =
240+
make_range(parameter_sorts).zip(make_range(arguments));
241+
for(const auto &parameter_sort_argument_pair : parameter_sort_arguments)
242+
{
243+
INVARIANT(
244+
parameter_sort_argument_pair.first ==
245+
parameter_sort_argument_pair.second.get_sort(),
246+
"Sort of argument must have the same sort as the parameter.");
247+
}
248+
}

‎src/solvers/smt2_incremental/smt_commands.h

+18
Original file line numberDiff line numberDiff line change
@@ -132,4 +132,22 @@ class smt_command_const_downcast_visitort
132132
#undef COMMAND_ID
133133
};
134134

135+
/// \brief A function generated from a command. Used for validating function
136+
/// application term arguments.
137+
class smt_command_functiont
138+
{
139+
private:
140+
std::vector<smt_sortt> parameter_sorts;
141+
smt_identifier_termt _identifier;
142+
143+
public:
144+
explicit smt_command_functiont(
145+
const smt_declare_function_commandt &function_declaration);
146+
explicit smt_command_functiont(
147+
const smt_define_function_commandt &function_definition);
148+
irep_idt identifier() const;
149+
smt_sortt return_sort(const std::vector<smt_termt> &arguments) const;
150+
void validate(const std::vector<smt_termt> &arguments) const;
151+
};
152+
135153
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H

‎src/solvers/smt2_incremental/smt_core_theory.cpp

+200
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,200 @@
1+
// Author: Diffblue Ltd.
2+
3+
#include <solvers/smt2_incremental/smt_core_theory.h>
4+
5+
const char *smt_core_theoryt::nott::identifier()
6+
{
7+
return "not";
8+
}
9+
10+
smt_sortt smt_core_theoryt::nott::return_sort(const smt_termt &operand)
11+
{
12+
return smt_bool_sortt{};
13+
}
14+
15+
void smt_core_theoryt::nott::validate(const smt_termt &operand)
16+
{
17+
INVARIANT(
18+
operand.get_sort() == smt_bool_sortt{},
19+
"\"not\" may only be applied to terms which have bool sort.");
20+
}
21+
22+
const smt_function_application_termt::factoryt<smt_core_theoryt::nott>
23+
smt_core_theoryt::make_not{};
24+
25+
const char *smt_core_theoryt::impliest::identifier()
26+
{
27+
return "=>";
28+
}
29+
30+
smt_sortt
31+
smt_core_theoryt::impliest::return_sort(const smt_termt &, const smt_termt &)
32+
{
33+
return smt_bool_sortt{};
34+
}
35+
36+
void smt_core_theoryt::impliest::validate(
37+
const smt_termt &lhs,
38+
const smt_termt &rhs)
39+
{
40+
INVARIANT(
41+
lhs.get_sort() == smt_bool_sortt{},
42+
"Left hand side of \"=>\" must have bool sort.");
43+
INVARIANT(
44+
rhs.get_sort() == smt_bool_sortt{},
45+
"Right hand side of \"=>\" must have bool sort.");
46+
}
47+
48+
const smt_function_application_termt::factoryt<smt_core_theoryt::impliest>
49+
smt_core_theoryt::implies{};
50+
51+
const char *smt_core_theoryt::andt::identifier()
52+
{
53+
return "and";
54+
}
55+
56+
smt_sortt
57+
smt_core_theoryt::andt::return_sort(const smt_termt &, const smt_termt &)
58+
{
59+
return smt_bool_sortt{};
60+
}
61+
62+
void smt_core_theoryt::andt::validate(
63+
const smt_termt &lhs,
64+
const smt_termt &rhs)
65+
{
66+
INVARIANT(
67+
lhs.get_sort() == smt_bool_sortt{},
68+
"Left hand side of \"and\" must have bool sort.");
69+
INVARIANT(
70+
rhs.get_sort() == smt_bool_sortt{},
71+
"Right hand side of \"and\" must have bool sort.");
72+
}
73+
74+
const smt_function_application_termt::factoryt<smt_core_theoryt::andt>
75+
smt_core_theoryt::make_and{};
76+
77+
const char *smt_core_theoryt::ort::identifier()
78+
{
79+
return "or";
80+
}
81+
82+
smt_sortt
83+
smt_core_theoryt::ort::return_sort(const smt_termt &, const smt_termt &)
84+
{
85+
return smt_bool_sortt{};
86+
}
87+
88+
void smt_core_theoryt::ort::validate(const smt_termt &lhs, const smt_termt &rhs)
89+
{
90+
INVARIANT(
91+
lhs.get_sort() == smt_bool_sortt{},
92+
"Left hand side of \"or\" must have bool sort.");
93+
INVARIANT(
94+
rhs.get_sort() == smt_bool_sortt{},
95+
"Right hand side of \"or\" must have bool sort.");
96+
}
97+
98+
const smt_function_application_termt::factoryt<smt_core_theoryt::ort>
99+
smt_core_theoryt::make_or{};
100+
101+
const char *smt_core_theoryt::xort::identifier()
102+
{
103+
return "xor";
104+
}
105+
106+
smt_sortt
107+
smt_core_theoryt::xort::return_sort(const smt_termt &, const smt_termt &)
108+
{
109+
return smt_bool_sortt{};
110+
}
111+
112+
void smt_core_theoryt::xort::validate(
113+
const smt_termt &lhs,
114+
const smt_termt &rhs)
115+
{
116+
INVARIANT(
117+
lhs.get_sort() == smt_bool_sortt{},
118+
"Left hand side of \"xor\" must have bool sort.");
119+
INVARIANT(
120+
rhs.get_sort() == smt_bool_sortt{},
121+
"Right hand side of \"xor\" must have bool sort.");
122+
}
123+
124+
const smt_function_application_termt::factoryt<smt_core_theoryt::xort>
125+
smt_core_theoryt::make_xor{};
126+
127+
const char *smt_core_theoryt::equalt::identifier()
128+
{
129+
return "=";
130+
}
131+
132+
smt_sortt
133+
smt_core_theoryt::equalt::return_sort(const smt_termt &, const smt_termt &)
134+
{
135+
return smt_bool_sortt{};
136+
}
137+
138+
void smt_core_theoryt::equalt::validate(
139+
const smt_termt &lhs,
140+
const smt_termt &rhs)
141+
{
142+
INVARIANT(
143+
lhs.get_sort() == rhs.get_sort(),
144+
"\"=\" may only be applied to terms which have the same sort.");
145+
}
146+
147+
const smt_function_application_termt::factoryt<smt_core_theoryt::equalt>
148+
smt_core_theoryt::equal{};
149+
150+
const char *smt_core_theoryt::distinctt::identifier()
151+
{
152+
return "distinct";
153+
}
154+
155+
smt_sortt
156+
smt_core_theoryt::distinctt::return_sort(const smt_termt &, const smt_termt &)
157+
{
158+
return smt_bool_sortt{};
159+
}
160+
161+
void smt_core_theoryt::distinctt::validate(
162+
const smt_termt &lhs,
163+
const smt_termt &rhs)
164+
{
165+
INVARIANT(
166+
lhs.get_sort() == rhs.get_sort(),
167+
"\"distinct\" may only be applied to terms which have the same sort.");
168+
}
169+
170+
const smt_function_application_termt::factoryt<smt_core_theoryt::distinctt>
171+
smt_core_theoryt::distinct{};
172+
173+
const char *smt_core_theoryt::if_then_elset::identifier()
174+
{
175+
return "ite";
176+
}
177+
178+
smt_sortt smt_core_theoryt::if_then_elset::return_sort(
179+
const smt_termt &,
180+
const smt_termt &then_term,
181+
const smt_termt &)
182+
{
183+
return then_term.get_sort();
184+
}
185+
186+
void smt_core_theoryt::if_then_elset::validate(
187+
const smt_termt &condition,
188+
const smt_termt &then_term,
189+
const smt_termt &else_term)
190+
{
191+
INVARIANT(
192+
condition.get_sort() == smt_bool_sortt{},
193+
"Condition term must have bool sort.");
194+
INVARIANT(
195+
then_term.get_sort() == else_term.get_sort(),
196+
"\"ite\" must have \"then\" and \"else\" terms of the same sort.");
197+
}
198+
199+
const smt_function_application_termt::factoryt<smt_core_theoryt::if_then_elset>
200+
smt_core_theoryt::if_then_else;

0 commit comments

Comments
 (0)