Skip to content

Simplify side conditions #2393

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 25 commits into from
Mar 2, 2021
Merged

Simplify side conditions #2393

merged 25 commits into from
Mar 2, 2021

Conversation

ana-pantilie
Copy link
Contributor

@ana-pantilie ana-pantilie commented Feb 8, 2021 •
edited
Loading

Fixes #1416

If the side condition contains multiple conditions, these changes will allow each condition to be simplified one time under the assumption that the others are true.

This PR also removes all the cases where we simplify the side condition with itself.

Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

  • Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
  • Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
  • Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
  • Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

@ttuegel ttuegel self-requested a review February 11, 2021 15:14
ttuegel
ttuegel reviewed Feb 12, 2021
View reviewed changes
Copy link
Contributor

@ttuegel ttuegel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For a test of the Pattern simplifier, I recommend simplifying something with a side condition that can be evaluated by function rules. For example, a ∧ (f(a) = b ∧ g(a) = g(b)) where the simplifier knows a function rule that says f(a) = b requires g(a) = g(b).

kore/src/Kore/Step/Simplification/Pattern.hs Outdated
Comment on lines 144 to 151
worker (pred' : rest) = do
sideCondition <- State.get
let otherConds = sideCondition <> from (MultiAnd.make rest)
result <-
simplifyCondition otherConds (Condition.fromPredicate pred')
& lift
State.put (SideCondition.andCondition sideCondition result)
worker rest
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let me make sure I understand this correctly: The SideCondition comprised of all simplified Predicates is held in the State. At each step, we combine that with the SideCondition from all (other) un-simplified Predicates, and use the combination to simplify the current Predicate. Then we update the stored SideCondition. Is that right?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's right.

@ttuegel
Copy link
Contributor

ttuegel commented Feb 16, 2021

To debug the performance regression, you can try the Kore-level profiler with speedscope: https://github.com/kframework/kore/wiki/Profiling#kore-profiling

@ana-pantilie

This comment has been minimized.

Sign in to view
@ana-pantilie ana-pantilie marked this pull request as ready for review February 24, 2021 18:23
@ana-pantilie ana-pantilie requested a review from ttuegel February 24, 2021 18:33
ttuegel
ttuegel approved these changes Mar 2, 2021
View reviewed changes
Copy link
Contributor

@ttuegel ttuegel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add some documentation for the new functions, even if it is repetitive.

I also thought about how we could name the isSimplified_ family of functions to call attention to their differences:

  • isSimplified (that has a side condition input) stays the same.
  • isFullySimplified becomes isSimplifiedAnyCondition.
  • isSimplifiedIgnoreCondition becomes isSimplifiedSomeCondition.

We don't have to do that; let me know what you think.

kore/src/Kore/Attribute/PredicatePattern.hs Outdated
@@ -97,6 +100,10 @@ isSimplified
:: SideCondition.Representation -> PredicatePattern variable -> Bool
isSimplified sideCondition = Simplified.isSimplified sideCondition . simplifiedAttribute

isSimplifiedIgnoreCondition
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add documentation similar to Kore.Attribute.Pattern.isSimplifiedIgnoreCondition.

kore/src/Kore/Attribute/Pattern.hs Outdated
@@ -156,6 +159,13 @@ isSimplified sideCondition patt@Pattern {simplified} =
assertSimplifiedConsistency patt
$ Simplified.isSimplified sideCondition simplified

isSimplifiedIgnoreCondition
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add documentation similar to Kore.Attribute.Pattern.Simplified.isSimplifiedIgnoreCondition.

kore/src/Kore/Internal/Predicate.hs Outdated
@@ -914,6 +916,9 @@ simplifiedAttribute = Attribute.simplifiedAttribute . extractAttributes
isSimplified :: SideCondition.Representation -> Predicate variable -> Bool
isSimplified condition = Attribute.isSimplified condition . extractAttributes

isSimplifiedIgnoreCondition :: Predicate variable -> Bool
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add documentation similar to Kore.Attribute.Pattern.Simplified.isSimplifiedIgnoreCondition.

kore/src/Kore/Internal/Substitution.hs Outdated
@@ -493,6 +494,11 @@ isSimplified _ (Substitution _) = False
isSimplified sideCondition (NormalizedSubstitution normalized) =
all (TermLike.isSimplified sideCondition) normalized

isSimplifiedIgnoreCondition :: Substitution variable -> Bool
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add documentation similar to Kore.Attribute.Pattern.Simplified.isSimplifiedIgnoreCondition.

kore/src/Kore/Internal/TermLike.hs Outdated
@@ -449,6 +450,10 @@ isSimplified :: SideCondition.Representation -> TermLike variable -> Bool
isSimplified sideCondition =
Attribute.isSimplified sideCondition . extractAttributes

isSimplifiedIgnoreCondition :: TermLike variable -> Bool
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add documentation.

@ana-pantilie ana-pantilie merged commit 9460590 into master Mar 2, 2021
@ana-pantilie ana-pantilie deleted the side-condition-simplification branch March 2, 2021 13:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ttuegel ttuegel ttuegel approved these changes

Assignees
No one assigned
Labels
automerge
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Include the side condition when evaluating functions in the side condition
2 participants
@ana-pantilie @ttuegel