Add built-in rule for symbolic ==Int #1894
Conversation
kore/src/Kore/Builtin/Int.hs
Outdated
| _intRight <- expectBuiltinInt eqKey _intRight | ||
| _intLeft == _intRight | ||
| & Bool.asPattern resultSort | ||
| & returnPattern |
There was a problem hiding this comment.
There is no need to even consider the extra side-conditions in the concrete case.
kore/src/Kore/Builtin/Int.hs
Outdated
| (_ :< VariableF varLeft, _ :< VariableF varRight) -> | ||
| varLeft == varRight | ||
| & Bool.asPattern resultSort | ||
| & returnPattern |
There was a problem hiding this comment.
This is not right: varLeft == varRight implies that varLeft ==Int varRight, but not the other way around! We cannot say anything when varLeft /= varRight.
Because variables are always defined, there is also no need to include the side conditions here. On the other hand, if we do include the stronger side conditions above, then we do not need to restrict to variables here; we can compare any two symbolic patterns.
| concrete <|> symbolicReflexivity | ||
| where | ||
| mkCeilUnlessDefined termLike | ||
| | TermLike.isDefinedPattern termLike = Condition.topOf resultSort |
There was a problem hiding this comment.
We actually need a stronger condition here: the arguments must be functional. If the arguments could take multiple values, then we would have to return multiple values. Consider:
\or(1, 2) ==Int 1 = \or(true, false)
kore/test/Test/Kore/Builtin/Int.hs
Outdated
|
|
||
| test_reflexivity_symbolic :: TestTree | ||
| test_reflexivity_symbolic = | ||
| testPropertyWithSolver (Text.unpack name) $ do |
There was a problem hiding this comment.
This is an ordinary integration test, not a integration property test. We should use HUnit instead, to avoid running the test 100 times.
Please also add a unit (not integration) test to show that x ==Int y is inconclusive.
kore/src/Kore/Builtin/Int.hs
Outdated
| let (_ :< patternLeft) = Recursive.project _intLeft | ||
| (_ :< patternRight) = Recursive.project _intRight | ||
| in | ||
| if patternLeft == patternRight then |
There was a problem hiding this comment.
I don't think we need to project the patterns here:
| let (_ :< patternLeft) = Recursive.project _intLeft | |
| (_ :< patternRight) = Recursive.project _intRight | |
| in | |
| if patternLeft == patternRight then | |
| if _intLeft == _intRight then |
kore/src/Kore/Builtin/Int.hs
Outdated
| & Bool.asPattern resultSort | ||
| & return | ||
|
|
||
| symbolicReflexivity = |
There was a problem hiding this comment.
Even though we add side conditions to make sure the inputs are defined, we still need to make sure that the inputs are function-like patterns:
| symbolicReflexivity = | |
| symbolicReflexivity = | |
| Control.Monad.guard (TermLike.isFunctionPattern _intLeft) | |
| -- Do not need to check _intRight because we only return a result | |
| -- when _intLeft and _intRight are equal. |
There was a problem hiding this comment.
Actually, mkCeilUnlessDefined uses isFunctionalPattern. I forgot to change its name 😅 . Should I make it check only if the inputs are defined and use the guard you suggested for function-like check?
kore/src/Kore/Builtin/Int.hs
Outdated
| mkCeilUnlessDefined termLike | ||
| | TermLike.isFunctionalPattern termLike = Condition.topOf resultSort | ||
| | otherwise = | ||
| Condition.fromPredicate (makeCeilPredicate resultSort termLike) | ||
| returnPattern = return . flip Pattern.andCondition conditions | ||
| conditions = foldMap mkCeilUnlessDefined arguments |
There was a problem hiding this comment.
Let's move these closer to the definition of symbolicReflexivity because that is the only place they are used.
2 participants
Fixes #1886
Reviewer checklist
stack test --coveragestack haddock