added cond_exprt #3236
added cond_exprt #3236
Conversation
kroening
commented
Oct 28, 2018
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
kroening
requested review from
martin-cs,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: c4810ef).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89423884
| @@ -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. | |||
There was a problem hiding this comment.
No else case? It's undefined if none of the conditions pass?
There was a problem hiding this comment.
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.
| /// 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. | ||
| class cond_exprt : public multi_ary_exprt |
There was a problem hiding this comment.
Seems easily confused with if_exprt, how about something like nary_if_exprt or if_elseif_exprt?
There was a problem hiding this comment.
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.
