Skip to content

added cond_exprt #3236

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 1 commit into from
Nov 6, 2018
Merged

added cond_exprt #3236

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
4 changes: 2 additions & 2 deletions src/solvers/flattening/boolbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -207,7 +207,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
else if(expr.id()==ID_case)
return convert_case(expr);
else if(expr.id()==ID_cond)
return convert_cond(expr);
return convert_cond(to_cond_expr(expr));
else if(expr.id()==ID_if)
return convert_if(to_if_expr(expr));
else if(expr.id()==ID_constant)
Expand Down Expand Up @@ -481,7 +481,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
}
else if(expr.id()==ID_cond)
{
bvt bv=convert_cond(expr);
bvt bv = convert_cond(to_cond_expr(expr));
CHECK_RETURN(bv.size() == 1);
return bv[0];
}
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,7 +161,7 @@ class boolbvt:public arrayst
virtual bvt convert_with(const exprt &expr);
virtual bvt convert_update(const exprt &expr);
virtual bvt convert_case(const exprt &expr);
virtual bvt convert_cond(const exprt &expr);
virtual bvt convert_cond(const cond_exprt &);
virtual bvt convert_shift(const binary_exprt &expr);
virtual bvt convert_bitwise(const exprt &expr);
virtual bvt convert_unary_minus(const unary_minus_exprt &expr);
Expand Down
4 changes: 1 addition & 3 deletions src/solvers/flattening/boolbv_cond.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,8 @@ Author: Daniel Kroening, [email protected]

#include <util/invariant.h>

bvt boolbvt::convert_cond(const exprt &expr)
bvt boolbvt::convert_cond(const cond_exprt &expr)
{
PRECONDITION(expr.id() == ID_cond);

const exprt::operandst &operands=expr.operands();

std::size_t width=boolbv_width(expr.type());
Expand Down
45 changes: 45 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 @@ -4750,4 +4750,49 @@ inline void validate_expr(const popcount_exprt &value)
validate_operands(value, 1, "popcount must have one operand");
}

/// this is a parametric version of an if-expression: it returns
/// the value of the first case (using the ordering of the operands)
/// whose condition evaluates to true.
Copy link
Contributor

Choose a reason for hiding this comment

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

No else case? It's undefined if none of the conditions pass?

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes, this is bugging me as well.
The origin of this expression is SMV, where it is common to end with a 'true' case.
If you don't, you get non-determinism.

class cond_exprt : public multi_ary_exprt
Copy link
Contributor

Choose a reason for hiding this comment

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

Seems easily confused with if_exprt, how about something like nary_if_exprt or if_elseif_exprt?

Copy link
Member Author

Choose a reason for hiding this comment

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

Agreed that something like that would be better; however, ID_cond is the existing name, and renaming should be a separate job. The added class simply documents the current state.

{
public:
explicit cond_exprt(const typet &_type) : multi_ary_exprt(ID_cond, _type)
{
}

/// adds a case to a cond expression
/// \param condition: the condition for the case
/// \param value: the value for the case
void add_case(const exprt &condition, const exprt &value)
{
PRECONDITION(condition.type().id() == ID_bool);
operands().reserve(operands().size() + 2);
operands().push_back(condition);
operands().push_back(value);
}
};

/// \brief Cast an exprt to a \ref cond_exprt
///
/// \a expr must be known to be \ref cond_exprt.
///
/// \param expr: Source expression
/// \return Object of type \ref cond_exprt
inline const cond_exprt &to_cond_expr(const exprt &expr)
{
PRECONDITION(expr.id() == ID_cond);
DATA_INVARIANT(
expr.operands().size() % 2 != 0, "cond must have even number of operands");
return static_cast<const cond_exprt &>(expr);
}

/// \copydoc to_popcount_expr(const exprt &)
inline cond_exprt &to_cond_expr(exprt &expr)
{
PRECONDITION(expr.id() == ID_cond);
DATA_INVARIANT(
expr.operands().size() % 2 != 0, "cond must have even number of operands");
return static_cast<cond_exprt &>(expr);
}

#endif // CPROVER_UTIL_STD_EXPR_H