Uh oh!
There was an error while loading. Please reload this page.
Do not sort operands as part of simplification [blocks: #3486] - #1997
Conversation
1a6002c to
44cce54Comparekroening
commented
Dec 5, 2018
Does it make a difference whether or not the number of operands is large? |
tautschnig
commented
Dec 5, 2018
It's just the plain number of compare operations. 163M |
44cce54 to
51fcd8cCompare
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 51fcd8c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106401199
tautschnig
commented
Mar 30, 2019
Combined with #1998 this increases the number of |
| return saj_table[i]; | ||
| } | ||
| bool sort_and_join(exprt &expr) |
There was a problem hiding this comment.
Because it no longer necessarily sorts! A person reading sort_and_join(x, false); might reasonably suppose that regardless of what that false means, x is certainly now sorted.
smowton
left a comment
There was a problem hiding this comment.
This roughly halved a long-running case that simplifies a very large expression
smowton
commented
Apr 17, 2019
(but do still please rename |
51fcd8c to
84baff9CompareCodecov Report
@@ Coverage Diff @@## develop #1997 +/- ##
========================================
Coverage 69.64% 69.65% ========================================
Files 1248 1248 Lines 100911 100921 +10 ========================================
+ Hits 70284 70292 +8 - Misses 30627 30629 +2
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
84baff9 to
ec4c8eeCompare
martin-cs
left a comment
There was a problem hiding this comment.
Yes but handling 'commutative but not associative' would be good.
| \[main.NaN.15\] line \d+ NaN on - in mynan - \(float\)n: SUCCESS | ||
| \[main.NaN.16\] line \d+ NaN on \* in mynan \* \(float\)n: SUCCESS | ||
| \[main.NaN.17\] line \d+ NaN on / in mynan / \(float\)n: SUCCESS | ||
| \[main.NaN.6\] line \d+ NaN on \+ in myinf \+ -myinf: FAILURE |
There was a problem hiding this comment.
Actually; this raises an interesting question. Floating-point addition and multiplication are commutative but not associative. If seems like normalising / sorting these would be worth while.
There was a problem hiding this comment.
I'm not sure I am able to follow: why would sorting (which this PR largely disables) be particularly beneficial for those operations? We surely can selectively re-enable sorting, but I don't think I understand the rationale just yet.
There was a problem hiding this comment.
float a;
float b;
if (!isnan(a) && !isnan(b)) {
assert(a + b === b + a);
}
Normalising the order of commutative-but-not-associative operations means we can resolve this at simplification, rather than an expensive solver call. It is not a massively common case but it is very cheap to implement and IIRC is a huge speed up in this case. Note that this can be purely local as it is not associative.
There was a problem hiding this comment.
It seems we didn't actually simplify such expressions before as commutative-but-not-associative operations were exempt. I have now added 375f208 to take care of this, thank you very much for raising this!
Uh oh!
There was an error while loading. Please reload this page.
ec4c8ee to
72b4c1dCompared89f368 to
67294c2Compare913d861 to
eae7a64CompareString refinement may or may not be successful (resulting in "ERROR" results rather than "FAILURE") when working on an unconstrained string (which the null dereference yields), depending on the models returned by the SAT solver.
Data for ReachSafety-BitVectors, the smallest of SV-COMP's categories, running for at most 600s per benchmark: 163M sort_operands calls, contributing to 1B irept::operator< calls, resulting in 4.5B irept::compare calls. None of these calls are actually necessary. As part of this work, also clean up naming of "sort_and_join" functions (as most of them don't actually sort or join, but instead just prepare for doing so).
eae7a64 to
9e5434bCompareTesting floating-point equality is expensive, and thus warrants handling special cases (even if they might be rare) in the simplifier. This (simplistic) test would take 5 seconds with CaDiCaL as SAT back-end when not performing simplification.
Do-not-merge as above: this needs proper profiling to confirm the effect with data.