Skip to content

Commit 9384c1b

Browse files
author
Daniel Kroening
committed
concatenation_exprt is multi_ary
1 parent 5300a73 commit 9384c1b

File tree

1 file changed

+13
-11
lines changed

1 file changed

+13
-11
lines changed

src/util/std_expr.h

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -4541,31 +4541,33 @@ inline void validate_expr(const function_application_exprt &value)
45414541
validate_operands(value, 2, "Function application must have two operands");
45424542
}
45434543

4544-
45454544
/// \brief Concatenation of bit-vector operands
45464545
///
45474546
/// This expression takes any number of operands
4548-
/// (a restriction to make this binary will happen in the future).
4549-
/// The ordering of the operands is the same as in the _new_ SMT 1.x standard,
4547+
/// The ordering of the operands is the same as in the SMT-LIB 2 standard,
45504548
/// i.e., most-significant operands come first.
4551-
class concatenation_exprt:public exprt
4549+
class concatenation_exprt : public multi_ary_exprt
45524550
{
45534551
public:
4554-
DEPRECATED("use concatenation_exprt(op0, op1, type) instead")
4555-
concatenation_exprt():exprt(ID_concatenation)
4552+
DEPRECATED("use concatenation_exprt(op, type) instead")
4553+
concatenation_exprt() : multi_ary_exprt(ID_concatenation)
45564554
{
45574555
}
45584556

4559-
DEPRECATED("use concatenation_exprt(op0, op1, type) instead")
4560-
explicit concatenation_exprt(const typet &_type):
4561-
exprt(ID_concatenation, _type)
4557+
DEPRECATED("use concatenation_exprt(op, type) instead")
4558+
explicit concatenation_exprt(const typet &_type)
4559+
: multi_ary_exprt(ID_concatenation, _type)
45624560
{
45634561
}
45644562

45654563
concatenation_exprt(const exprt &_op0, const exprt &_op1, const typet &_type)
4566-
: exprt(ID_concatenation, _type)
4564+
: multi_ary_exprt(_op0, ID_concatenation, _op1, _type)
4565+
{
4566+
}
4567+
4568+
concatenation_exprt(operandst &&_operands, const typet &_type)
4569+
: multi_ary_exprt(ID_concatenation, std::move(_operands), _type)
45674570
{
4568-
add_to_operands(_op0, _op1);
45694571
}
45704572
};
45714573

0 commit comments

Comments
 (0)