SMT.Translate.translatePattern: add fallback for translateApplication #2261
Conversation
kore/src/Kore/Step/SMT/Translate.hs
Outdated
| ApplySymbolF app | ||
| | isFunctionalPattern pat -> | ||
| translateApplication app | ||
| <|> translateUninterpreted' |
There was a problem hiding this comment.
Why can't we add this to translateApplication itself?
There was a problem hiding this comment.
Thanks for suggesting this, I made the change and added some comments on the PR about the additional things I had to modify resulting from this.
| sexpr <- maybe empty return translated | ||
| when (isNothing translated) |
There was a problem hiding this comment.
From my understanding, if translated is Nothing this gets discarded before logging the warning. My changes should fix this.
| | isFunctionalPattern original = | ||
| translateInterpretedApplication | ||
| <|> translateUninterpreted' | ||
| | otherwise = | ||
| translateInterpretedApplication |
There was a problem hiding this comment.
Before, we would fall back to translateUninterpreted for translateInt and translateBool without first checking if the pattern is functional. I assumed this wasn't correct, and fixed it here. This is reflected in the tests by the need to add some test data with the functional attribute.
Reviewer checklist
stack test --coveragestack haddock