Overhaul predicate simplifier #2599
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ttuegel
commented
May 5, 2021
| @@ -1,6 +1,6 @@ | |||
| kore-exec: [233424] Error (ErrorException): | |||
Contributor
Author
There was a problem hiding this comment.
This test must have been silently failing for a long time...
Contributor
There was a problem hiding this comment.
I'm confused, won't this test continue to fail on other runs if its output depends on the timestamp?
Contributor
Author
There was a problem hiding this comment.
The test actually only searches the output for a particular string with grep. I will update the test in another pull request so that this is clearer.
ttuegel
force-pushed
the
overhaul-predicate
branch
from
02c8574 to
8ebd31f
Compare
|
|
docs/simplify-predicate.md
Outdated
Comment on lines
55
to
56
| Assuming the children of `\or` are in disjunctive normal form, then the clause | ||
| is already normalized. |
Contributor
There was a problem hiding this comment.
Maybe add something like "because or is associative", to anticipate normalizeOr better.
docs/simplify-predicate.md
Outdated
|
|
||
| Simplification happens recursively, upward from the bottom. Therefore, we | ||
| describe the simplification steps based on the shape of the top-most | ||
| unsimplified clause of the predicate. |
Contributor
There was a problem hiding this comment.
This phrasing is not clear for me. If we start simplifying from the bottom, wouldn't the top look the same until the end? Maybe my intuition of what is a clause is wrong.
|
|
|
ttuegel
force-pushed
the
overhaul-predicate
branch
from
36d5427 to
d727b39
Compare
|
|
Contributor
Author
|
I tested this locally and found no significant performance difference with master. It's also worth noting that the proofs which show > 5% increased allocation are all very small. |
4 tasks
ttuegel
force-pushed
the
overhaul-predicate
branch
from
3eee5f6 to
79299c2
Compare
Although the substitution is assumed to be applied to the predicate, it may also affect variables in the side condition.
ttuegel
force-pushed
the
overhaul-predicate
branch
from
88cf681 to
c2bfbd4
Compare
Comment on lines
+289
to
+290
| Note: @L@ is carried through to the right-hand side of 'Implies' to maximize | ||
| the information content of that branch. |
Contributor
There was a problem hiding this comment.
In which cases is the L necessary?
Contributor
There was a problem hiding this comment.
Actually, I'm wondering, do we ever simplify \\implies predicates (outside of the tests)?
Contributor
Author
There was a problem hiding this comment.
We simplify \implies sometimes as the result of \equals simplification, if either side is not a function-like pattern. This isn't very common. Carrying the left-hand side over improves simplification a bit in these cases; it can rule out some branches which were also carrying \not(L) from another part.
| @@ -1,6 +1,6 @@ | |||
| kore-exec: [233424] Error (ErrorException): | |||
Contributor
There was a problem hiding this comment.
I'm confused, won't this test continue to fail on other runs if its output depends on the timestamp?
| #Equals | ||
| Z:MyId in_keys ( MAP | ||
| ( Y:MyId |-> 2 ) ) | ||
| ( Y:MyId |-> 1 ) ) |
Contributor
There was a problem hiding this comment.
This doesn't look right, we have X ==K Y, and we update the value Y points to, so it should be 2 not 1, right?
Contributor
Author
There was a problem hiding this comment.
The meaning of the output is unchanged. The Map appears under in_keys, so actually the values are irrelevant.
4 tasks
|
ana-pantilie
approved these changes
Jun 16, 2021
4 tasks
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fixes #2570
Review checklist
The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.