simplifier: use new interface #4872
Conversation
kroening
commented
Jul 3, 2019
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- 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.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
kroening
requested review from
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
kroening
force-pushed
the
simplifier_new_interface2
branch
from
a8a38bf to
19bbfc6
Compare
This improves type safety.
This improves type safety.
kroening
force-pushed
the
simplifier_new_interface2
branch
from
719479d to
30c134f
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 30c134f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/117953528
Codecov Report
@@ Coverage Diff @@
## develop #4872 +/- ##
===========================================
- Coverage 69.06% 69.05% -0.02%
===========================================
Files 1297 1297
Lines 106819 106815 -4
===========================================
- Hits 73779 73760 -19
- Misses 33040 33055 +15
Continue to review full report at Codecov.
|
| @@ -1429,11 +1428,9 @@ bool simplify_exprt::get_values( | |||
| return true; | |||
| } | |||
|
|
|||
| bool simplify_exprt::simplify_lambda(exprt &) | |||
| simplify_exprt::resultt<> simplify_exprt::simplify_lambda(const exprt &expr) | |||
There was a problem hiding this comment.
If we're touching this interface, can we make it consume a const array_comprehension_exprt &expr please?
There was a problem hiding this comment.
Let's defer -- there is the very independent issue of the confusion between array comprehension and lambda expressions (as in Chruch's lambda calculus). Look at 5f0808c.
| @@ -2423,30 +2420,24 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) | |||
| return unchanged(expr); | |||
| } | |||
|
|
|||
| bool simplify_exprt::simplify_complex(exprt &expr) | |||
| simplify_exprt::resultt<> simplify_exprt::simplify_complex(const exprt &expr) | |||
| { | |||
| if(expr.id() == ID_complex_real) | |||
There was a problem hiding this comment.
Shouldn't this be two separate functions rather than branching twice on the same id in quick succession? (Once to figure out we need to call simplify_complex and then this one here. We could then have a typesafe interface.)
There was a problem hiding this comment.
Sure, can be split; will add to #4874
| if( | ||
| expr.operands().size() != 2 || | ||
| expr.operands().front().type().id() != ID_bool || | ||
| expr.operands().back().type().id() != ID_bool) |
There was a problem hiding this comment.
Could we use to_implies_expr and make sure that does the same amount of sanity checking?
There was a problem hiding this comment.
added as separate commit.
I wouldn't add the operand type checks to to_implies(). This is what the validate() methods do.
| auto new_expr = expr; | ||
| new_expr.id(ID_or); | ||
| new_expr.op0() = boolean_negate(new_expr.op0()); | ||
| simplify_node(new_expr.op0()); |
There was a problem hiding this comment.
Is this actually necessary? We don't consistently do this after boolean_negate
There was a problem hiding this comment.
Indeed, this is a no-op. Added as separate commit to #4874.
| } | ||
|
|
||
| bool simplify_exprt::simplify_not(exprt &expr) | ||
| simplify_exprt::resultt<> simplify_exprt::simplify_not(const exprt &expr) |
There was a problem hiding this comment.
Shouldn't this be a const not_exprt &expr?
| @@ -774,15 +771,15 @@ simplify_exprt::resultt<> simplify_exprt::simplify_bitwise(const exprt &expr) | |||
| return std::move(new_expr); | |||
| } | |||
|
|
|||
| bool simplify_exprt::simplify_extractbit(exprt &expr) | |||
| simplify_exprt::resultt<> simplify_exprt::simplify_extractbit(const exprt &expr) | |||
There was a problem hiding this comment.
Interface should be const extractbit_exprt &expr
| } | ||
|
|
||
| bool simplify_exprt::simplify_concatenation(exprt &expr) | ||
| simplify_exprt::resultt<> | ||
| simplify_exprt::simplify_concatenation(const exprt &expr) |
There was a problem hiding this comment.
const concatentation_exprt &expr
| } | ||
|
|
||
| bool simplify_exprt::simplify_unary_plus(exprt &expr) | ||
| simplify_exprt::resultt<> simplify_exprt::simplify_unary_plus(const exprt &expr) |
There was a problem hiding this comment.
const unary_plus_exprt &expr
| } | ||
|
|
||
| bool simplify_exprt::simplify_unary_minus(exprt &expr) | ||
| simplify_exprt::resultt<> | ||
| simplify_exprt::simplify_unary_minus(const exprt &expr) |
There was a problem hiding this comment.
const unary_minus_exprt &expr
| } | ||
|
|
||
| bool simplify_exprt::simplify_bitnot(exprt &expr) | ||
| simplify_exprt::resultt<> simplify_exprt::simplify_bitnot(const exprt &expr) |
There was a problem hiding this comment.
const bitnot_exprt &expr
Follow-up from comment in #4872. The call is a no-op.
Follow-up from comment in #4872. The call is a no-op.
Follow-up from comment in #4872. The call is a no-op.
