Skip to content

Commit 2b1b4e0

Browse files
committed
Remove macro-definition of signed_less_than from X-macro.
And substitute it with a concrete class implementation.
1 parent ca76cbb commit 2b1b4e0

File tree

3 files changed

+32
-1
lines changed

3 files changed

+32
-1
lines changed

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -137,3 +137,26 @@ void smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::validate(
137137
const smt_function_application_termt::factoryt<
138138
smt_bit_vector_theoryt::unsigned_greater_than_or_equalt>
139139
smt_bit_vector_theoryt::unsigned_greater_than_or_equal{};
140+
141+
const char *smt_bit_vector_theoryt::signed_less_thant::identifier()
142+
{
143+
return "bvslt";
144+
}
145+
146+
smt_sortt smt_bit_vector_theoryt::signed_less_thant::return_sort(
147+
const smt_termt &lhs,
148+
const smt_termt &rhs)
149+
{
150+
return smt_bool_sortt{};
151+
}
152+
153+
void smt_bit_vector_theoryt::signed_less_thant::validate(
154+
const smt_termt &lhs,
155+
const smt_termt &rhs)
156+
{
157+
validate_bit_vector_predicate_arguments(lhs, rhs);
158+
}
159+
160+
const smt_function_application_termt::factoryt<
161+
smt_bit_vector_theoryt::signed_less_thant>
162+
smt_bit_vector_theoryt::signed_less_than{};

src/solvers/smt2_incremental/smt_bit_vector_theory.def

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33
/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
44
/// set of bitvector theory functions which are implemented and it is used to
55
/// automate repetitive parts of the implementation.
6-
SMT_BITVECTOR_THEORY_PREDICATE(bvslt, signed_less_than)
76
SMT_BITVECTOR_THEORY_PREDICATE(bvsle, signed_less_than_or_equal)
87
SMT_BITVECTOR_THEORY_PREDICATE(bvsgt, signed_greater_than)
98
SMT_BITVECTOR_THEORY_PREDICATE(bvsge, signed_greater_than_or_equal)

src/solvers/smt2_incremental/smt_bit_vector_theory.h

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,15 @@ class smt_bit_vector_theoryt
5959
static const smt_function_application_termt::factoryt<
6060
unsigned_greater_than_or_equalt>
6161
unsigned_greater_than_or_equal;
62+
63+
struct signed_less_thant final
64+
{
65+
static const char *identifier();
66+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
67+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
68+
};
69+
static const smt_function_application_termt::factoryt<signed_less_thant>
70+
signed_less_than;
6271
};
6372

6473
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

0 commit comments

Comments
 (0)