Skip to content

Introduce unary_plus_exprt #2931

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Sep 11, 2018
Merged

Introduce unary_plus_exprt #2931

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8286f21
Add unary_plus_exprt
danpoe Sep 10, 2018
1f01bbf
Use unary_plus_exprt in bitvector flattening
danpoe Sep 10, 2018
083561f
Use unary_plus_exprt in smt2 conversion
danpoe Sep 10, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions src/solvers/flattening/boolbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
3 changes: 1 addition & 2 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand Down
43 changes: 43 additions & 0 deletions src/util/std_expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe add a comment saying what this is useful for.

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<const unary_plus_exprt &>(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<unary_plus_exprt &>(expr);
}

template <>
inline bool can_cast_expr<unary_plus_exprt>(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
{
Expand Down