From 8286f2141e03e22a4dbf9d617ab2835eb5287fcb Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 10 Sep 2018 16:07:22 +0100 Subject: [PATCH 1/3] Add unary_plus_exprt --- src/util/std_expr.h | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 85ca4a6b3a2..e879a3f3516 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -438,6 +438,49 @@ inline void validate_expr(const unary_minus_exprt &value) validate_operands(value, 1, "Unary minus must have one operand"); } +/// \brief The unary plus expression +class unary_plus_exprt : public unary_exprt +{ +public: + explicit unary_plus_exprt(const exprt &op) + : unary_exprt(ID_unary_plus, op, op.type()) + { + } +}; + +/// \brief Cast an exprt to a \ref unary_plus_exprt +/// +/// \a expr must be known to be \ref unary_plus_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref unary_plus_exprt +inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_unary_plus); + DATA_INVARIANT( + expr.operands().size() == 1, "unary plus must have one operand"); + return static_cast(expr); +} + +/// \copydoc to_unary_minus_expr(const exprt &) +inline unary_plus_exprt &to_unary_plus_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_unary_plus); + DATA_INVARIANT( + expr.operands().size() == 1, "unary plus must have one operand"); + return static_cast(expr); +} + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_unary_plus; +} +inline void validate_expr(const unary_plus_exprt &value) +{ + validate_operands(value, 1, "unary plus must have one operand"); +} + /// \brief The byte swap expression class bswap_exprt: public unary_exprt { From 1f01bbf739e8a38ba7011c3c9a0d829e3086a75d Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 10 Sep 2018 16:13:08 +0100 Subject: [PATCH 2/3] Use unary_plus_exprt in bitvector flattening --- src/solvers/flattening/boolbv.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 3c5cb3856d8..55d69c3abb9 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -249,8 +249,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr) return convert_unary_minus(to_unary_expr(expr)); else if(expr.id()==ID_unary_plus) { - assert(expr.operands().size()==1); - return convert_bitvector(expr.op0()); + return convert_bitvector(to_unary_plus_expr(expr).op()); } else if(expr.id()==ID_abs) return convert_abs(to_abs_expr(expr)); From 083561f944284d6141257f2d3401f2f342107cf1 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 10 Sep 2018 16:14:21 +0100 Subject: [PATCH 3/3] Use unary_plus_exprt in smt2 conversion --- src/solvers/smt2/smt2_conv.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 007e4fdd3d7..40a96c923eb 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1053,8 +1053,7 @@ void smt2_convt::convert_expr(const exprt &expr) else if(expr.id()==ID_unary_plus) { // A no-op (apart from type promotion) - assert(expr.operands().size()==1); - convert_expr(expr.op0()); + convert_expr(to_unary_plus_expr(expr).op()); } else if(expr.id()==ID_sign) {