Booster implies endpoint improvements #4026
Conversation
… #Bottom in the antecedent or condition being simplified to #Bottom
| explodeAnd other = [other] | ||
| explodeAnd :: Syntax.KorePattern -> NE.NonEmpty Syntax.KorePattern | ||
| explodeAnd Syntax.KJAnd{patterns} = case patterns of | ||
| [] -> error "malformed KJAnd" |
There was a problem hiding this comment.
I think the benefit of having this function returning NonEmpty and exploding on an invalid And is not big, as we only use the non-empty in isTop/isBottom. I think we can just as well use the normal list there and avoid the call to error?
booster/library/Booster/JsonRpc.hs
Outdated
| in runExcept $ | ||
| internalisePatternOrTopOrBottom DisallowAlias CheckSubsorts Nothing def existentials korePat | ||
|
|
||
| checkImplies patL substitutionL unsupportedL existsL patR substitutionR unsupportedR existsR = do |
There was a problem hiding this comment.
I agree with Jost that this function should be moved to a separate module.
…tion/haskell-backend into sam/implies-improvements
| pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $ | ||
| "match remainder: " | ||
| <> renderDefault | ||
| ( hsep $ | ||
| punctuate comma $ | ||
| map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ | ||
| NonEmpty.toList remainder | ||
| ) |
There was a problem hiding this comment.
This could actually return "not implied" but returns an error at the moment so that proxy will call kore-rpc (I think).
Maybe add a comment to that effect. We could also return "not implied" and change proxy to re-validate this result, but throwing an error might be better for now.
| MatchFailed{} -> | ||
| doesNotImply (sortOfPattern substPatL) antecedent.term consequent.term | ||
| MatchIndeterminate remainder -> | ||
| ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPatL >>= \case |
There was a problem hiding this comment.
Would it make sense to also simplify substPatR ?
Fixes #3941 along with a host of tests from the pyk testsuite, which exercise corner cases, such as
#Bottombeing sent as antecedent or inconsistent conditions. Whilst these haven't really been observed in practice, passing these tests should give is more confidence that the booster does the same thing as kore.