Skip to content

Commit a07c0ab

Browse files
tautschnigtautschnig
authored
Merge pull request #7736 from tautschnig/cleanup/remove-vector-from-back-end
Remove support for vector-typed expressions from back-ends
2 parents 0834274 + 70a95a8 commit a07c0ab

10 files changed

+27
-417
lines changed

‎src/solvers/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,6 @@ SRC = $(BOOLEFORCE_SRC) \
128128
flattening/boolbv_unary_minus.cpp \
129129
flattening/boolbv_union.cpp \
130130
flattening/boolbv_update.cpp \
131-
flattening/boolbv_vector.cpp \
132131
flattening/boolbv_width.cpp \
133132
flattening/boolbv_with.cpp \
134133
flattening/bv_dimacs.cpp \

‎src/solvers/flattening/boolbv.cpp

-2
Original file line numberDiff line numberDiff line change
@@ -192,8 +192,6 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
192192
}
193193
else if(expr.id()==ID_array)
194194
return convert_array(expr);
195-
else if(expr.id()==ID_vector)
196-
return convert_vector(to_vector_expr(expr));
197195
else if(expr.id()==ID_complex)
198196
return convert_complex(to_complex_expr(expr));
199197
else if(expr.id()==ID_complex_real)

‎src/solvers/flattening/boolbv.h

-1
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,6 @@ class boolbvt:public arrayst
157157
virtual bvt convert_if(const if_exprt &expr);
158158
virtual bvt convert_struct(const struct_exprt &expr);
159159
virtual bvt convert_array(const exprt &expr);
160-
virtual bvt convert_vector(const vector_exprt &expr);
161160
virtual bvt convert_complex(const complex_exprt &expr);
162161
virtual bvt convert_complex_real(const complex_real_exprt &expr);
163162
virtual bvt convert_complex_imag(const complex_imag_exprt &expr);

‎src/solvers/flattening/boolbv_add_sub.cpp

+18-21
Original file line numberDiff line numberDiff line change
@@ -21,14 +21,13 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
2121

2222
const typet &type = expr.type();
2323

24-
if(type.id()!=ID_unsignedbv &&
25-
type.id()!=ID_signedbv &&
26-
type.id()!=ID_fixedbv &&
27-
type.id()!=ID_floatbv &&
28-
type.id()!=ID_range &&
29-
type.id()!=ID_complex &&
30-
type.id()!=ID_vector)
24+
if(
25+
type.id() != ID_unsignedbv && type.id() != ID_signedbv &&
26+
type.id() != ID_fixedbv && type.id() != ID_floatbv &&
27+
type.id() != ID_range && type.id() != ID_complex)
28+
{
3129
return conversion_failed(expr);
30+
}
3231

3332
std::size_t width=boolbv_width(type);
3433

@@ -50,9 +49,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
5049
bool no_overflow=(expr.id()=="no-overflow-plus" ||
5150
expr.id()=="no-overflow-minus");
5251

53-
typet arithmetic_type = (type.id() == ID_vector || type.id() == ID_complex)
54-
? to_type_with_subtype(type).subtype()
55-
: type;
52+
typet arithmetic_type =
53+
type.id() == ID_complex ? to_type_with_subtype(type).subtype() : type;
5654

5755
bv_utilst::representationt rep=
5856
(arithmetic_type.id()==ID_signedbv ||
@@ -68,15 +66,16 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
6866

6967
const bvt &op = convert_bv(*it, width);
7068

71-
if(type.id()==ID_vector || type.id()==ID_complex)
69+
if(type.id() == ID_complex)
7270
{
7371
std::size_t sub_width =
7472
boolbv_width(to_type_with_subtype(type).subtype());
7573

76-
INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
74+
INVARIANT(
75+
sub_width != 0, "complex elements shall have nonzero bit width");
7776
INVARIANT(
7877
width % sub_width == 0,
79-
"total vector bit width shall be a multiple of the element bit width");
78+
"total complex bit width shall be a multiple of the element bit width");
8079

8180
std::size_t size=width/sub_width;
8281
bv.resize(width);
@@ -149,8 +148,7 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
149148

150149
if(
151150
type.id() != ID_unsignedbv && type.id() != ID_signedbv &&
152-
type.id() != ID_fixedbv && type.id() != ID_complex &&
153-
type.id() != ID_vector)
151+
type.id() != ID_fixedbv && type.id() != ID_complex)
154152
{
155153
return conversion_failed(expr);
156154
}
@@ -163,9 +161,8 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
163161

164162
const bool subtract = expr.id() == ID_saturating_minus;
165163

166-
typet arithmetic_type = (type.id() == ID_vector || type.id() == ID_complex)
167-
? to_type_with_subtype(type).subtype()
168-
: type;
164+
typet arithmetic_type =
165+
type.id() == ID_complex ? to_type_with_subtype(type).subtype() : type;
169166

170167
bv_utilst::representationt rep =
171168
(arithmetic_type.id() == ID_signedbv || arithmetic_type.id() == ID_fixedbv)
@@ -175,15 +172,15 @@ bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
175172
bvt bv = convert_bv(expr.lhs(), width);
176173
const bvt &op = convert_bv(expr.rhs(), width);
177174

178-
if(type.id() != ID_vector && type.id() != ID_complex)
175+
if(type.id() != ID_complex)
179176
return bv_utils.saturating_add_sub(bv, op, subtract, rep);
180177

181178
std::size_t sub_width = boolbv_width(to_type_with_subtype(type).subtype());
182179

183-
INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
180+
INVARIANT(sub_width != 0, "complex elements shall have nonzero bit width");
184181
INVARIANT(
185182
width % sub_width == 0,
186-
"total vector bit width shall be a multiple of the element bit width");
183+
"total complex bit width shall be a multiple of the element bit width");
187184

188185
std::size_t size = width / sub_width;
189186

‎src/solvers/flattening/boolbv_floatbv_op.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,7 @@ bvt boolbvt::convert_floatbv_op(const ieee_float_op_exprt &expr)
116116
else
117117
UNREACHABLE;
118118
}
119-
else if(expr.type().id() == ID_vector || expr.type().id() == ID_complex)
119+
else if(expr.type().id() == ID_complex)
120120
{
121121
const typet &subtype = to_type_with_subtype(expr.type()).subtype();
122122

@@ -129,8 +129,8 @@ bvt boolbvt::convert_floatbv_op(const ieee_float_op_exprt &expr)
129129

130130
DATA_INVARIANT(
131131
sub_width > 0 && width % sub_width == 0,
132-
"width of a vector subtype must be positive and evenly divide the "
133-
"width of the vector");
132+
"width of a complex subtype must be positive and evenly divide the "
133+
"width of the complex expression");
134134

135135
std::size_t size=width/sub_width;
136136
bvt result_bv;
@@ -160,7 +160,7 @@ bvt boolbvt::convert_floatbv_op(const ieee_float_op_exprt &expr)
160160

161161
INVARIANT(
162162
sub_result_bv.size() == sub_width,
163-
"we constructed a new vector of the right size");
163+
"we constructed a new complex of the right size");
164164
INVARIANT(
165165
i * sub_width + sub_width - 1 < result_bv.size(),
166166
"the sub-bitvector fits into the result bitvector");

‎src/solvers/flattening/boolbv_get.cpp

-25
Original file line numberDiff line numberDiff line change
@@ -153,31 +153,6 @@ exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset)
153153
bv_get_rec(member, bv, offset),
154154
type);
155155
}
156-
else if(type.id()==ID_vector)
157-
{
158-
const std::size_t width = boolbv_width(type);
159-
160-
const auto &vector_type = to_vector_type(type);
161-
const typet &element_type = vector_type.element_type();
162-
std::size_t element_width = boolbv_width(element_type);
163-
CHECK_RETURN(element_width > 0);
164-
165-
if(element_width != 0 && width % element_width == 0)
166-
{
167-
std::size_t size = width / element_width;
168-
vector_exprt value({}, vector_type);
169-
value.reserve_operands(size);
170-
171-
for(std::size_t i=0; i<size; i++)
172-
{
173-
const index_exprt index{expr,
174-
from_integer(i, vector_type.index_type())};
175-
value.operands().push_back(bv_get_rec(index, bv, i * element_width));
176-
}
177-
178-
return std::move(value);
179-
}
180-
}
181156
else if(type.id()==ID_complex)
182157
{
183158
const std::size_t width = boolbv_width(type);

‎src/solvers/flattening/boolbv_unary_minus.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,7 @@ bvt boolbvt::convert_unary_minus(const unary_minus_exprt &expr)
3030
bvtypet bvtype=get_bvtype(type);
3131
bvtypet op_bvtype = get_bvtype(op.type());
3232

33-
if(bvtype==bvtypet::IS_UNKNOWN &&
34-
(type.id()==ID_vector || type.id()==ID_complex))
33+
if(bvtype == bvtypet::IS_UNKNOWN && type.id() == ID_complex)
3534
{
3635
const typet &subtype = to_type_with_subtype(type).subtype();
3736

‎src/solvers/flattening/boolbv_vector.cpp

-34
This file was deleted.

‎src/solvers/flattening/boolbv_width.cpp

-15
Original file line numberDiff line numberDiff line change
@@ -149,21 +149,6 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
149149
else
150150
cache_entry = defined_entryt{numeric_cast_v<std::size_t>(total)};
151151
}
152-
else if(type_id==ID_vector)
153-
{
154-
const vector_typet &vector_type=to_vector_type(type);
155-
auto sub_width = get_width_opt(vector_type.element_type());
156-
if(!sub_width.has_value())
157-
return cache_entry;
158-
159-
const auto vector_size = numeric_cast_v<mp_integer>(vector_type.size());
160-
161-
mp_integer total = vector_size * *sub_width;
162-
if(total > (1 << 30)) // realistic limit
163-
throw analysis_exceptiont("vector too large for flattening");
164-
else
165-
cache_entry = defined_entryt{numeric_cast_v<std::size_t>(total)};
166-
}
167152
else if(type_id==ID_complex)
168153
{
169154
auto sub_width = get_width_opt(to_complex_type(type).subtype());

0 commit comments

Comments
 (0)