Skip to content

Commit 3c0d865

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #6615 from NlightNFotis/remove_xmacro
[Refactor] New SMT backend: Remove X-macro implementation from `smt_bit_vector_theory`
2 parents 79d7f1e + 8e9a74a commit 3c0d865

File tree

3 files changed

+262
-48
lines changed

3 files changed

+262
-48
lines changed

‎src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

Lines changed: 186 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -19,26 +19,189 @@ static void validate_bit_vector_predicate_arguments(
1919
"Left and right operands must have the same bit width.");
2020
}
2121

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
22+
// Relational operator definitions
23+
24+
const char *smt_bit_vector_theoryt::unsigned_less_thant::identifier()
25+
{
26+
return "bvult";
27+
}
28+
29+
smt_sortt smt_bit_vector_theoryt::unsigned_less_thant::return_sort(
30+
const smt_termt &lhs,
31+
const smt_termt &rhs)
32+
{
33+
return smt_bool_sortt{};
34+
}
35+
36+
void smt_bit_vector_theoryt::unsigned_less_thant::validate(
37+
const smt_termt &lhs,
38+
const smt_termt &rhs)
39+
{
40+
validate_bit_vector_predicate_arguments(lhs, rhs);
41+
}
42+
43+
const smt_function_application_termt::factoryt<
44+
smt_bit_vector_theoryt::unsigned_less_thant>
45+
smt_bit_vector_theoryt::unsigned_less_than{};
46+
47+
const char *smt_bit_vector_theoryt::unsigned_less_than_or_equalt::identifier()
48+
{
49+
return "bvule";
50+
}
51+
52+
smt_sortt smt_bit_vector_theoryt::unsigned_less_than_or_equalt::return_sort(
53+
const smt_termt &lhs,
54+
const smt_termt &rhs)
55+
{
56+
return smt_bool_sortt{};
57+
}
58+
59+
void smt_bit_vector_theoryt::unsigned_less_than_or_equalt::validate(
60+
const smt_termt &lhs,
61+
const smt_termt &rhs)
62+
{
63+
validate_bit_vector_predicate_arguments(lhs, rhs);
64+
}
65+
66+
const smt_function_application_termt::factoryt<
67+
smt_bit_vector_theoryt::unsigned_less_than_or_equalt>
68+
smt_bit_vector_theoryt::unsigned_less_than_or_equal{};
69+
70+
const char *smt_bit_vector_theoryt::unsigned_greater_thant::identifier()
71+
{
72+
return "bvugt";
73+
}
74+
75+
smt_sortt smt_bit_vector_theoryt::unsigned_greater_thant::return_sort(
76+
const smt_termt &lhs,
77+
const smt_termt &rhs)
78+
{
79+
return smt_bool_sortt{};
80+
}
81+
82+
void smt_bit_vector_theoryt::unsigned_greater_thant::validate(
83+
const smt_termt &lhs,
84+
const smt_termt &rhs)
85+
{
86+
validate_bit_vector_predicate_arguments(lhs, rhs);
87+
}
88+
89+
const smt_function_application_termt::factoryt<
90+
smt_bit_vector_theoryt::unsigned_greater_thant>
91+
smt_bit_vector_theoryt::unsigned_greater_than{};
92+
93+
const char *
94+
smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::identifier()
95+
{
96+
return "bvuge";
97+
}
98+
99+
smt_sortt smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::return_sort(
100+
const smt_termt &lhs,
101+
const smt_termt &rhs)
102+
{
103+
return smt_bool_sortt{};
104+
}
105+
106+
void smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::validate(
107+
const smt_termt &lhs,
108+
const smt_termt &rhs)
109+
{
110+
validate_bit_vector_predicate_arguments(lhs, rhs);
111+
}
112+
113+
const smt_function_application_termt::factoryt<
114+
smt_bit_vector_theoryt::unsigned_greater_than_or_equalt>
115+
smt_bit_vector_theoryt::unsigned_greater_than_or_equal{};
116+
117+
const char *smt_bit_vector_theoryt::signed_less_thant::identifier()
118+
{
119+
return "bvslt";
120+
}
121+
122+
smt_sortt smt_bit_vector_theoryt::signed_less_thant::return_sort(
123+
const smt_termt &lhs,
124+
const smt_termt &rhs)
125+
{
126+
return smt_bool_sortt{};
127+
}
128+
129+
void smt_bit_vector_theoryt::signed_less_thant::validate(
130+
const smt_termt &lhs,
131+
const smt_termt &rhs)
132+
{
133+
validate_bit_vector_predicate_arguments(lhs, rhs);
134+
}
135+
136+
const smt_function_application_termt::factoryt<
137+
smt_bit_vector_theoryt::signed_less_thant>
138+
smt_bit_vector_theoryt::signed_less_than{};
139+
140+
const char *smt_bit_vector_theoryt::signed_less_than_or_equalt::identifier()
141+
{
142+
return "bvsle";
143+
}
144+
145+
smt_sortt smt_bit_vector_theoryt::signed_less_than_or_equalt::return_sort(
146+
const smt_termt &lhs,
147+
const smt_termt &rhs)
148+
{
149+
return smt_bool_sortt{};
150+
}
151+
152+
void smt_bit_vector_theoryt::signed_less_than_or_equalt::validate(
153+
const smt_termt &lhs,
154+
const smt_termt &rhs)
155+
{
156+
validate_bit_vector_predicate_arguments(lhs, rhs);
157+
}
158+
159+
const smt_function_application_termt::factoryt<
160+
smt_bit_vector_theoryt::signed_less_than_or_equalt>
161+
smt_bit_vector_theoryt::signed_less_than_or_equal{};
162+
163+
const char *smt_bit_vector_theoryt::signed_greater_thant::identifier()
164+
{
165+
return "bvsgt";
166+
}
167+
168+
smt_sortt smt_bit_vector_theoryt::signed_greater_thant::return_sort(
169+
const smt_termt &lhs,
170+
const smt_termt &rhs)
171+
{
172+
return smt_bool_sortt{};
173+
}
174+
175+
void smt_bit_vector_theoryt::signed_greater_thant::validate(
176+
const smt_termt &lhs,
177+
const smt_termt &rhs)
178+
{
179+
validate_bit_vector_predicate_arguments(lhs, rhs);
180+
}
181+
182+
const smt_function_application_termt::factoryt<
183+
smt_bit_vector_theoryt::signed_greater_thant>
184+
smt_bit_vector_theoryt::signed_greater_than{};
185+
186+
const char *smt_bit_vector_theoryt::signed_greater_than_or_equalt::identifier()
187+
{
188+
return "bvsge";
189+
}
190+
191+
smt_sortt smt_bit_vector_theoryt::signed_greater_than_or_equalt::return_sort(
192+
const smt_termt &lhs,
193+
const smt_termt &rhs)
194+
{
195+
return smt_bool_sortt{};
196+
}
197+
198+
void smt_bit_vector_theoryt::signed_greater_than_or_equalt::validate(
199+
const smt_termt &lhs,
200+
const smt_termt &rhs)
201+
{
202+
validate_bit_vector_predicate_arguments(lhs, rhs);
203+
}
204+
205+
const smt_function_application_termt::factoryt<
206+
smt_bit_vector_theoryt::signed_greater_than_or_equalt>
207+
smt_bit_vector_theoryt::signed_greater_than_or_equal{};

‎src/solvers/smt2_incremental/smt_bit_vector_theory.def

Lines changed: 0 additions & 13 deletions
This file was deleted.

‎src/solvers/smt2_incremental/smt_bit_vector_theory.h

Lines changed: 76 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -8,18 +8,82 @@
88
class smt_bit_vector_theoryt
99
{
1010
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
11+
// Relational operator class declarations
12+
struct unsigned_less_thant final
13+
{
14+
static const char *identifier();
15+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
16+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
17+
};
18+
static const smt_function_application_termt::factoryt<unsigned_less_thant>
19+
unsigned_less_than;
20+
21+
struct unsigned_less_than_or_equalt final
22+
{
23+
static const char *identifier();
24+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
25+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
26+
};
27+
static const smt_function_application_termt::factoryt<
28+
unsigned_less_than_or_equalt>
29+
unsigned_less_than_or_equal;
30+
31+
struct unsigned_greater_thant final
32+
{
33+
static const char *identifier();
34+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
35+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
36+
};
37+
static const smt_function_application_termt::factoryt<unsigned_greater_thant>
38+
unsigned_greater_than;
39+
40+
struct unsigned_greater_than_or_equalt final
41+
{
42+
static const char *identifier();
43+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
44+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
45+
};
46+
static const smt_function_application_termt::factoryt<
47+
unsigned_greater_than_or_equalt>
48+
unsigned_greater_than_or_equal;
49+
50+
struct signed_less_thant final
51+
{
52+
static const char *identifier();
53+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
54+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
55+
};
56+
static const smt_function_application_termt::factoryt<signed_less_thant>
57+
signed_less_than;
58+
59+
struct signed_less_than_or_equalt final
60+
{
61+
static const char *identifier();
62+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
63+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
64+
};
65+
static const smt_function_application_termt::factoryt<
66+
signed_less_than_or_equalt>
67+
signed_less_than_or_equal;
68+
69+
struct signed_greater_thant final
70+
{
71+
static const char *identifier();
72+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
73+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
74+
};
75+
static const smt_function_application_termt::factoryt<signed_greater_thant>
76+
signed_greater_than;
77+
78+
struct signed_greater_than_or_equalt final
79+
{
80+
static const char *identifier();
81+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
82+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
83+
};
84+
static const smt_function_application_termt::factoryt<
85+
signed_greater_than_or_equalt>
86+
signed_greater_than_or_equal;
2387
};
2488

2589
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

0 commit comments

Comments
 (0)