Simplify (T)(a?b:c) to a?(T)b:(T)c

[tautschnig]

The idea of such a rule existed ever since 7285dda, but was possibly too
costly when doing it post-order for one would have to re-process
multiple sub-expressions. A pre-order rule avoids such repeat
processing.

• 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.
• 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.

[martin-cs]

I am a little concerned about the cost of this, esp. w.r.t. non-trivial casts like double->float or int->double. Some things like integer reduction are definitely worth doing. Is it worth restricting what types this is applied to?

[codecov]

Codecov Report

Base: 78.02% // Head: 78.04% // Increases project coverage by +0.02% 🎉

Coverage data is based on head (fac7964) compared to base (b19b412).
Patch coverage: 92.78% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #5892      +/-   ##
===========================================
+ Coverage    78.02%   78.04%   +0.02%     
===========================================
  Files         1625     1624       -1     
  Lines       187427   187431       +4     
===========================================
+ Hits        146231   146274      +43     
+ Misses       41196    41157      -39     

Impacted Files	Coverage Δ
src/cprover/cprover_parse_options.cpp	56.58% <ø> (ø)
src/cprover/generalization.cpp	84.21% <ø> (ø)
src/cprover/inductiveness.cpp	78.35% <ø> (ø)
src/cprover/propagate.cpp	74.28% <ø> (ø)
src/cprover/report_properties.cpp	88.46% <ø> (ø)
src/cprover/report_traces.cpp	89.74% <ø> (ø)
src/cprover/solver.cpp	92.00% <ø> (ø)
src/cprover/solver_progress.cpp	60.00% <ø> (ø)
src/goto-symex/field_sensitivity.h	100.00% <ø> (ø)
src/util/console.cpp	29.76% <ø> (ø)
... and 15 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[tautschnig]

I am a little concerned about the cost of this, esp. w.r.t. non-trivial casts like double->float or int->double. Some things like integer reduction are definitely worth doing. Is it worth restricting what types this is applied to?

Done.

[martin-cs]

I think that will avoid the most expensive cases. Thanks.

[kroening]

Do we have any means to performance-benchmark?

[tautschnig]

@kroening:

Do we have any means to performance-benchmark?

I have run all of SV-COMP's benchmarks on this branch and compared it to develop. No difference beyond the expected jitter was observable. Therefore, I'd argue that this simplification step can in some cases permit additional constant propagation without adversely affecting other verification tasks that don't contain such expressions.