Skip to content

Remove Defined markers in simplifyConjunctionByAssumption #2372

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

Merged
merged 6 commits into from
Jan 27, 2021
Merged

Remove Defined markers in simplifyConjunctionByAssumption #2372

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
6b8bf8b
Do not ignore antiLeft if argument is Nothing
ana-pantilie Jan 25, 2021
c199733
Add integration test
ana-pantilie Jan 26, 2021
c0af21c
Removed Defined markers in simplifyConjunctionByAssumption
ana-pantilie Jan 26, 2021
951a183
Add unit tests
ana-pantilie Jan 26, 2021
3636947
Merge branch 'master' into remove-defined-in-simplifyconj
ana-pantilie Jan 27, 2021
265f276
Address review comment
ana-pantilie Jan 27, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions kore/src/Kore/Step/Simplification/Condition.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -278,7 +278,10 @@ simplifyConjunctionByAssumption (toList -> andPredicates) =
HashMap.insert predicate makeTruePredicate
assumeEqualTerms =
case predicate of
PredicateEquals t1 t2 ->
PredicateEquals
(TermLike.unDefined -> t1)
(TermLike.unDefined -> t2)
->
case retractLocalFunction (mkEquals_ t1 t2) of
Just (Pair t1' t2') ->
Lens.over (field @"termLikeMap") $
Expand Down Expand Up @@ -342,7 +345,7 @@ simplifyConjunctionByAssumption (toList -> andPredicates) =
:: HashMap (TermLike variable) (TermLike variable)
-> TermLike variable
-> Changed (TermLike variable)
applyAssumptionsWorkerTerm assumptions original
applyAssumptionsWorkerTerm assumptions (TermLike.unDefined -> original)
| Just result <- HashMap.lookup original assumptions = Changed result

| HashMap.null assumptions' = Unchanged original
Expand Down
22 changes: 22 additions & 0 deletions kore/test/Test/Kore/Step/Simplification/Condition.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,13 +76,18 @@ test_simplify_local_functions =
, test "contradiction: \"one\" = f(x) ∧ f(x) = \"two\"" fString (Left strOne) (Right strTwo)
, test "contradiction: \"one\" = f(x) ∧ \"two\" = f(x)" fString (Left strOne) (Left strTwo)
, test "contradiction: f(x) = \"one\" ∧ \"two\" = f(x)" fString (Right strOne) (Left strTwo)
-- Ignore Defined marker
, testDefined "contradiction: f(g(x)) = a ∧ f(g(x)) = b" (Right fg) (Right a) (Right b)
, testDefined "contradiction: f(g(x)) = a ∧ f(g(x)) = b" (Left fg) (Right a) (Right b)
Comment on lines +80 to +81
Copy link
Contributor

Choose a reason for hiding this comment

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

What is the difference between Right fg and Left fg?

Copy link
Contributor Author

@ana-pantilie ana-pantilie Jan 27, 2021 •
edited
Loading

Choose a reason for hiding this comment

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

Right fg will apply mkDefined to the f(g(x) in the second equals, and Left fg to the one in the first. This makes sure we test that the Defined markers are removed when both assuming and looking up terms.

]
where
f = Mock.f (mkElemVar Mock.x)
fg = Mock.f (Mock.g (mkElemVar Mock.x))
fInt = Mock.fInt (mkElemVar Mock.xInt)
fBool = Mock.fBool (mkElemVar Mock.xBool)
fString = Mock.fString (mkElemVar Mock.xString)
defined = makeCeilPredicate f & Condition.fromPredicate
definedFg = makeCeilPredicate fg & Condition.fromPredicate

a = Mock.a
b = Mock.b
Expand All @@ -102,6 +107,11 @@ test_simplify_local_functions =
mkLocalDefn func (Left t) = makeEqualsPredicate t func
mkLocalDefn func (Right t) = makeEqualsPredicate func t

applyDefined1 (Left func) = mkDefined func
applyDefined1 (Right func) = func
applyDefined2 (Left func) = func
applyDefined2 (Right func) = mkDefined func

test name func eitherC1 eitherC2 =
testCase name $ do
let equals1 = mkLocalDefn func eitherC1 & Condition.fromPredicate
Expand All @@ -110,6 +120,18 @@ test_simplify_local_functions =
actual <- simplify condition
assertBool "Expected \\bottom" $ isBottom actual

testDefined name eitherFunc eitherC1 eitherC2 =
testCase name $ do
let equals1 =
mkLocalDefn (applyDefined1 eitherFunc) eitherC1
& Condition.fromPredicate
equals2 =
mkLocalDefn (applyDefined2 eitherFunc) eitherC2
& Condition.fromPredicate
condition = definedFg <> equals1 <> definedFg <> equals2
Copy link
Contributor

Choose a reason for hiding this comment

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

Using definedFg here actually requires that eitherFunc is Right fg or Left fg, so I would rather we not allow passing in any value there.

Copy link
Contributor Author

@ana-pantilie ana-pantilie Jan 27, 2021 •
edited
Loading

Choose a reason for hiding this comment

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

Do you mean we should remove definedFg from condition? Edit: I think this is what you meant by this comment, so I pushed a commit with this change. If you think something else should change, let me know.

actual <- simplify condition
assertBool "Expected \\bottom" $ isBottom actual

test_predicateSimplification :: [TestTree]
test_predicateSimplification =
[ testCase "Identity for top and bottom" $ do
Expand Down