Keep set of defined terms in SideCondition #2354

ana-pantilie · 2021-01-19T10:18:25Z

Part of #2351

~~Needs #2315~~

Implements the first three bullet points from #2351.

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!

…ondition

…ndition' into replacement-map-in-sidecondition

…ork/kore into replacement-map-in-sidecondition

…sidecondition

Co-authored-by: Thomas Tuegel <[email protected]>

…' into defined-terms-in-sidecondition

…decondition

kore/src/Kore/Internal/SideCondition.hs

ttuegel · 2021-02-01T22:41:54Z

kore/src/Kore/Internal/SideCondition.hs

        isBottom assumedTrue
      where
        SideCondition { assumedTrue } = sideCondition

 instance Ord variable => HasFreeVariables (SideCondition variable) variable
  where
-    freeVariables sideCondition@(SideCondition _ _) =
+    freeVariables sideCondition@(SideCondition _ _ _) =


I think this should include the free variables of the other fields.

Do you think this should include the free variables of the replacements as well? I assume you mean the free variables of the defined terms here, right?

Well, the free variables of the term replacements should be the same as from the assumedTrue right? Yes, we should definitely include the defined terms.

kore/src/Kore/Internal/SideCondition.hs

ttuegel · 2021-02-01T22:44:47Z

kore/src/Kore/Internal/SideCondition.hs

+                        generateNormalizedAcs internalMap
+                        & HashSet.map TermLike.mkInternalMap
+                 in foldMap assumeDefinedWorker definedElems
+                    <> asSet term'


Why use asSet here?

generateNormalizedAcs will not add the collection itself to the resulting HashSet. I thought it was clearer to separate the two, especially since we should check if the input collection is always defined or not before adding it. Actually, do you think we should do the same for the subcollections as well?

Sorry, I mean: Why does the collection itself need to be in the set at all? The set should have all the sub-terms required to decide that the whole collection is defined.

Done. We don't add the collection itself anymore, and I added a special case for singleton collections in isDefined.

ttuegel · 2021-02-01T22:45:53Z

kore/src/Kore/Internal/SideCondition.hs

+                 in foldMap assumeDefinedWorker definedElems
+                    <> asSet term'
+                    <> definedMaps
+            TermLike.InternalSet_ internalSet ->


Could the logic for Map and Set be combined with Kore.Builtin.AssocComm.CeilSimplifier?

I've thought about this, and I think it would only make sense if we wanted to also generate subcollections there and evaluate their ceils. Do we want to do this? At the moment, it looks like we only check the definedness of the elements and if they are unique.

At the moment, it looks like we only check the definedness of the elements and if they are unique.

Well, that's what it means to evaluate the \ceils of sub-collections.

kore/src/Kore/Internal/SideCondition.hs

This reverts commit deaf0af.

* Revert "Keep set of defined terms in SideCondition (#2354)" This reverts commit deaf0af. * Revert "Keep table of term replacements in SideCondition, use in term simplifier (#2315)" This reverts commit c427819.

ana-pantilie and others added 30 commits December 7, 2020 19:00

Add HashMap to SideCondition

ef7e6a2

Rename assumptions to replacements

acd2db2

Use simplifyConjunctionWithAssumptions to construct and combine SideC…

a5f33ef

…ondition

Hlint

4ff1717

Use to and from SideCondition to simplify Condition

3a9367c

Merge remote-tracking branch 'ana-pantilie/substitution-map-in-sideco…

4675f21

…ndition' into replacement-map-in-sidecondition

Use Changed in simplifyConjunctions again

2316fe4

Merge branch 'master' into replacement-map-in-sidecondition

aab235e

Use replacements when simplifying terms, with exception

a0548d4

Regenerate golden

e94747f

Comment out failing test, TODO fix

0615cd6

Merge branch 'replacement-map-in-sidecondition' of github.com:kframew…

50cf56a

…ork/kore into replacement-map-in-sidecondition

Simplify Pattern with SideCondition in only special cases

d9a2efd

Use simplify instead of simplifyTopConfiguration

75d5de7

Modify test which describes possibly wrong behavior

3ea5720

Merge remote-tracking branch 'origin/master' into replacement-map-in-…

99e47e0

…sidecondition

Merge branch 'master' into replacement-map-in-sidecondition

2239a98

Fixed onepath test

8427101

TermLike.simplify unit tests; simplify with all replacements

6e5da94

Remove unused imports

2d32ce3

Add Pretty instance for SideCondition

bb0deb2

Add documentation

fc82465

Add strictness to fields

d0d5a92

Add strict language pragma

be0eff9

Make lazy binding

ff4667b

Merge branch 'master' into replacement-map-in-sidecondition

319a6ca

Address review comments

82678f7

Clean-up

f8626e1

Update kore/src/Kore/Step/Simplification/Condition.hs

f2da9d1

Co-authored-by: Thomas Tuegel <[email protected]>

Update Debug.hs

b892e8f

ana-pantilie and others added 14 commits January 21, 2021 13:20

Implement assumeDefined for assoc comm collections

9199f2e

Fix

cdedaa8

Fixes and tests for generateNormalizedAcs

9d44720

Tests and fixes

294b729

Keep term and predicate replacements together as terms

6095fae

Merge branch 'master' into replacement-map-in-sidecondition

907817f

Merge branch 'master' into replacement-map-in-sidecondition

3d92b8c

Remove double import

3a98848

generateNormalizedAcs: clean-up

bfb6080

Finish isDefined, add tests and clean-up

3f80f88

Merge remote-tracking branch 'origin/replacement-map-in-sidecondition…

d7536b7

…' into defined-terms-in-sidecondition

Merge remote-tracking branch 'origin/master' into defined-terms-in-si…

756cde3

…decondition

Major test clean-up, include set tests

f478491

Fix functional application case, add tests

d180df7

ana-pantilie marked this pull request as ready for review January 29, 2021 14:06

ttuegel self-requested a review January 29, 2021 15:13

ttuegel reviewed Feb 1, 2021

View reviewed changes

ana-pantilie and others added 7 commits February 2, 2021 12:16

Review: remove TopBottom instance, toPredicate includes defined terms

93f2a81

Review: redundant case and freeVariables

848ff05

Do not add collection to defined, special case for singletons

4e09391

Refactor newly added tests

76b7856

Merge branch 'master' into defined-terms-in-sidecondition

9daf33c

Fix conflicts with master

3900cc3

Refactor and clean-up CeilSimplifier

ba60e3b

ttuegel approved these changes Feb 3, 2021

View reviewed changes

ttuegel merged commit deaf0af into master Feb 3, 2021

ttuegel deleted the defined-terms-in-sidecondition branch February 3, 2021 21:43

ttuegel added a commit that referenced this pull request Feb 4, 2021

Revert "Keep set of defined terms in SideCondition (#2354)"

eb16946

This reverts commit deaf0af.

ttuegel mentioned this pull request Feb 4, 2021

Revert #2315 #2385

Merged

4 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Keep set of defined terms in SideCondition #2354

Keep set of defined terms in SideCondition #2354

Uh oh!

ana-pantilie commented Jan 19, 2021 •

edited

Loading

Uh oh!

Uh oh!

ttuegel Feb 1, 2021

Uh oh!

ana-pantilie Feb 2, 2021

Uh oh!

ttuegel Feb 2, 2021

Uh oh!

Uh oh!

ttuegel Feb 1, 2021

Uh oh!

ana-pantilie Feb 2, 2021

Uh oh!

ttuegel Feb 2, 2021

Uh oh!

ana-pantilie Feb 3, 2021

Uh oh!

ttuegel Feb 1, 2021

Uh oh!

ana-pantilie Feb 2, 2021

Uh oh!

ttuegel Feb 2, 2021

Uh oh!

Uh oh!

Uh oh!

Keep set of defined terms in SideCondition #2354

Keep set of defined terms in SideCondition #2354

Uh oh!

Conversation

ana-pantilie commented Jan 19, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review checklist

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

ana-pantilie commented Jan 19, 2021 •

edited

Loading