Skip to content

Commit 1b910f8

Browse files
tautschnigDaniel Kroening
authored and
Daniel Kroening
committed
Construct plus_exprt in a non-deprecated way
The default constructor is deprecated. To facilitate construction with an arbitrary number of operands a new constructor taking a initializer list is added.
1 parent ce97967 commit 1b910f8

File tree

2 files changed

+12
-7
lines changed

2 files changed

+12
-7
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3076,13 +3076,13 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
30763076
// add component-by-component
30773077
for(mp_integer i = 0; i != size; ++i)
30783078
{
3079-
plus_exprt tmp(vector_type.subtype());
3080-
forall_operands(it, expr)
3081-
tmp.copy_to_operands(
3082-
index_exprt(
3083-
*it,
3084-
from_integer(size - i - 1, index_type),
3085-
vector_type.subtype()));
3079+
exprt::operandst summands;
3080+
summands.reserve(expr.operands().size());
3081+
for(const auto &op : expr.operands())
3082+
summands.push_back(index_exprt(
3083+
op, from_integer(size - i - 1, index_type), vector_type.subtype()));
3084+
3085+
plus_exprt tmp(std::move(summands), vector_type.subtype());
30863086

30873087
out << " ";
30883088
convert_expr(tmp);

src/util/std_expr.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1076,6 +1076,11 @@ class plus_exprt:public multi_ary_exprt
10761076
multi_ary_exprt(_lhs, ID_plus, _rhs, _type)
10771077
{
10781078
}
1079+
1080+
plus_exprt(operandst &&_operands, const typet &_type)
1081+
: multi_ary_exprt(ID_plus, std::move(_operands), _type)
1082+
{
1083+
}
10791084
};
10801085

10811086
/// \brief Cast an exprt to a \ref plus_exprt

0 commit comments

Comments
 (0)